OAI/NumberTheory/EgyptianFractions/ForwardDifference.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.Problem337.forwardDifference line 11

   Source documentation

   Iterated forward differences, with the shifts in list order.

   def forwardDifference : List ℝ → (ℝ → ℝ) → ℝ → ℝ
     | [], f => f
     | h :: hs, f => fun x => forwardDifference hs f (x + h) - forwardDifference hs f x

2. theorem OAI.Problem337.forwardDifference_contDiffOn line 15
3. theorem OAI.Problem337.deriv_forwardDifference line 32
4. theorem OAI.Problem337.forwardDifference_eq_derivative line 57

   Source documentation

   Repeated mean value theorem for positive shifts. The witness remains in the interval swept out by all shifts.

   theorem forwardDifference_eq_derivative (hs : List ℝ)
       (hhs : ∀ h ∈ hs, 0 < h) {f : ℝ → ℝ}
       (hf : ContDiffOn ℝ ∞ f (Ioi 0)) {x : ℝ} (hx : 0 < x) :
       ∃ ξ : ℝ, x ≤ ξ ∧ ξ ≤ x + hs.sum ∧
         forwardDifference hs f x = hs.prod * iteratedDeriv hs.length f ξ := by
   …

   Mentions: OAI.Problem337.forwardDifference

5. theorem OAI.Problem337.iteratedDeriv_forwardDifference line 92
6. theorem OAI.Problem337.smooth_iteratedDeriv_Ioi line 106
7. theorem OAI.Problem337.iteratedDeriv_order_add line 114
8. theorem OAI.Problem337.iteratedDeriv_forwardDifference_eq line 122

   Source documentation

   The derivative of an iterated difference is a scaled higher derivative at an intermediate point. This avoids a multi-dimensional integral in the phase estimate.

   theorem iteratedDeriv_forwardDifference_eq (k : ℕ) (hs : List ℝ)
       (hhs : ∀ h ∈ hs, 0 < h) {f : ℝ → ℝ}
       (hf : ContDiffOn ℝ ∞ f (Ioi 0)) {x : ℝ} (hx : 0 < x) :
       ∃ ξ : ℝ, x ≤ ξ ∧ ξ ≤ x + hs.sum ∧
         iteratedDeriv k (forwardDifference hs f) x =
           hs.prod * iteratedDeriv (hs.length + k) f ξ := by
   …

   Mentions: OAI.Problem337.forwardDifference

9. theorem OAI.Problem337.reciprocal_forwardDifference_derivative_bounds line 136

   Source documentation

   Uniform bounds for the derivatives of a differenced reciprocal phase on its untruncated support. In particular k=2 is the input to a second-derivative test.

   theorem reciprocal_forwardDifference_derivative_bounds (k : ℕ) (hs : List ℝ)
       (hhs : ∀ h ∈ hs, 0 < h) (Z : ℝ) {U x : ℝ}
       (hU : 0 < U) (hx : U ≤ x) (hxend : x + hs.sum ≤ 2 * U) :
       hs.prod * ((hs.length + k).factorial : ℝ) * |Z| /
           (2 * U) ^ (hs.length + k + 1) ≤
         |iteratedDeriv k (forwardDifference hs (fun y => Z / y)) x| ∧
       |iteratedDeriv k (forwardDifference hs (fun y => Z / y)) x| ≤
         hs.prod * ((hs.length + k).factorial : ℝ) * |Z| /
           U ^ (hs.length + k + 1) := by
   …

   Mentions: OAI.Problem337.forwardDifference

10. theorem OAI.Problem337.reciprocal_forwardDifference_derivative_bounds_interval line 158

    Source documentation

    Endpoint-flexible version, allowing the upper endpoint to extend beyond an exponential sum's support by the one or two derivative-test samples.

    theorem reciprocal_forwardDifference_derivative_bounds_interval (k : ℕ) (hs : List ℝ)
        (hhs : ∀ h ∈ hs, 0 < h) (Z : ℝ) {U V x : ℝ}
        (hU : 0 < U) (hx : U ≤ x) (hxend : x + hs.sum ≤ V) :
        hs.prod * ((hs.length + k).factorial : ℝ) * |Z| /
            V ^ (hs.length + k + 1) ≤
          |iteratedDeriv k (forwardDifference hs (fun y => Z / y)) x| ∧
        |iteratedDeriv k (forwardDifference hs (fun y => Z / y)) x| ≤
          hs.prod * ((hs.length + k).factorial : ℝ) * |Z| /
            U ^ (hs.length + k + 1) := by
    …

    Mentions: OAI.Problem337.forwardDifference