OAI/NumberTheory/EgyptianFractions/ReciprocalDerivatives.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.Problem337.reciprocal_phase_iteratedDeriv line 9

   Source documentation

   Explicit derivatives of the reciprocal phase used in deterministic cancellation.

   theorem reciprocal_phase_iteratedDeriv (k : ℕ) (Z x : ℝ) :
       iteratedDeriv k (fun y : ℝ => Z / y) x =
         (-1 : ℝ) ^ k * (k.factorial : ℝ) * Z / x ^ (k + 1) := by
   …

2. theorem OAI.Problem337.abs_reciprocal_phase_iteratedDeriv line 17
3. theorem OAI.Problem337.reciprocal_phase_derivative_bounds line 24

   Source documentation

   Uniform derivative bounds on a dyadic interval.

   theorem reciprocal_phase_derivative_bounds (k : ℕ) (Z : ℝ) {U x : ℝ}
       (hU : 0 < U) (hx : U ≤ x) (hx2 : x ≤ 2 * U) :
       (k.factorial : ℝ) * |Z| / (2 * U) ^ (k + 1) ≤
           |iteratedDeriv k (fun y : ℝ => Z / y) x| ∧
         |iteratedDeriv k (fun y : ℝ => Z / y) x| ≤
           (k.factorial : ℝ) * |Z| / U ^ (k + 1) := by
   …

4. theorem OAI.Problem337.reciprocal_phase_derivative_bounds_interval line 40

   Source documentation

   The same derivative estimate on an arbitrary positive interval. The flexible upper endpoint allows the extra samples used in a second-derivative test.

   theorem reciprocal_phase_derivative_bounds_interval (k : ℕ) (Z : ℝ) {U V x : ℝ}
       (hU : 0 < U) (hx : U ≤ x) (hxV : x ≤ V) :
       (k.factorial : ℝ) * |Z| / V ^ (k + 1) ≤
           |iteratedDeriv k (fun y : ℝ => Z / y) x| ∧
         |iteratedDeriv k (fun y : ℝ => Z / y) x| ≤
           (k.factorial : ℝ) * |Z| / U ^ (k + 1) := by
   …