OAI/NumberTheory/EgyptianFractions/ReciprocalPhaseRegularity.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.forwardDifference_iteratedDeriv_contDiffOn line 12

   Source documentation

   Every derivative of a smooth forward difference stays smooth on the positive half-line.

   theorem forwardDifference_iteratedDeriv_contDiffOn (k : ℕ) (hs : List ℝ)
       (hhs : ∀ h ∈ hs, 0 ≤ h) {f : ℝ → ℝ}
       (hf : ContDiffOn ℝ ∞ f (Ioi 0)) :
       ContDiffOn ℝ ∞ (iteratedDeriv k (forwardDifference hs f)) (Ioi 0) := by
   …

   Mentions: OAI.Problem337.forwardDifference

2. theorem OAI.Problem337.forwardDifference_iteratedDeriv_hasDerivAt line 24

   Source documentation

   Local regularity in the exact pointwise form used by a second derivative test. No global smoothness at zero is asserted.

   theorem forwardDifference_iteratedDeriv_hasDerivAt (k : ℕ) (hs : List ℝ)
       (hhs : ∀ h ∈ hs, 0 ≤ h) {f : ℝ → ℝ}
       (hf : ContDiffOn ℝ ∞ f (Ioi 0)) {x : ℝ} (hx : 0 < x) :
       HasDerivAt (iteratedDeriv k (forwardDifference hs f))
         (iteratedDeriv (k + 1) (forwardDifference hs f) x) x := by
   …

   Mentions: OAI.Problem337.forwardDifference

3. theorem OAI.Problem337.reciprocal_forwardDifference_hasDerivAt line 34

   Source documentation

   Pointwise derivatives of every order of a differenced reciprocal phase.

   theorem reciprocal_forwardDifference_hasDerivAt (k : ℕ) (hs : List ℝ)
       (hhs : ∀ h ∈ hs, 0 ≤ h) (Z : ℝ) {x : ℝ} (hx : 0 < x) :
       HasDerivAt (iteratedDeriv k (forwardDifference hs (fun y => Z / y)))
         (iteratedDeriv (k + 1) (forwardDifference hs (fun y => Z / y)) x) x := by
   …

   Mentions: OAI.Problem337.forwardDifference

4. theorem OAI.Problem337.reciprocal_forwardDifference_second_derivative_data line 42

   Source documentation

   Paired first and second derivatives for the continuous second derivative test.

   theorem reciprocal_forwardDifference_second_derivative_data (hs : List ℝ)
       (hhs : ∀ h ∈ hs, 0 ≤ h) (Z : ℝ) {x : ℝ} (hx : 0 < x) :
       HasDerivAt (forwardDifference hs (fun y => Z / y))
         (iteratedDeriv 1 (forwardDifference hs (fun y => Z / y)) x) x ∧
       HasDerivAt (iteratedDeriv 1 (forwardDifference hs (fun y => Z / y)))
         (iteratedDeriv 2 (forwardDifference hs (fun y => Z / y)) x) x := by
   …

   Mentions: OAI.Problem337.forwardDifference