OAI/NumberTheory/JointDickman/Analysis/LogPhaseSecondDerivative.lean

GitHub source file

1 declarations, 0 contain sorry, 0 declared as axioms

The second-derivative bound after logarithmic differencing

  1. theorem OAI.JointDickman.logarithmic_difference_sum_bound line 13

    Source documentation

    All derivative information is proved for the actual logarithmic phase. The interval includes the full displacement introduced by differencing.

    theorem logarithmic_difference_sum_bound (hs : List ℝ)
    (hhs : ∀ h ∈ hs, 0 < h) (a Z U x : ℝ) (N : ℕ)
    (hZ : Z ≠ 0) (hU : 0 < U) (hx : U ≤ x)
    (hend : x+(N:ℝ)+hs.sum ≤ 4*U) :
    let lam : ℝ := hs.prod*((hs.length+1).factorial:ℝ)*|Z|/(4*U)^(hs.length+2)
…