OAI/NumberTheory/JointDickman/Analysis/LogPhaseDerivatives.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.JointDickman.logarithmic_phase_smooth line 10
2. lemma OAI.JointDickman.logarithmic_phase_iteratedDeriv line 14
3. lemma OAI.JointDickman.abs_logarithmic_phase_iteratedDeriv line 24
4. theorem OAI.JointDickman.logarithmic_forwardDifference_second_bounds line 32

   Source documentation

   After finitely many positive differences, the second derivative retains its explicit size throughout the original interval and all shifts.

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

5. lemma OAI.JointDickman.logarithmic_linear_phase_smooth line 56
6. lemma OAI.JointDickman.logarithmic_linear_phase_iteratedDeriv line 60
7. lemma OAI.JointDickman.abs_logarithmic_linear_phase_iteratedDeriv line 73
8. lemma OAI.JointDickman.logarithmic_linear_forwardDifference_second_bounds line 80