LogPhaseTerminal.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform terminal cancellation for logarithmic phases

lemma OAI.JointDickman.logarithmic_terminal_scale_eq line 11

theorem OAI.JointDickman.logarithmic_terminal_range_bound line 24

Source documentation

The last differenced sums have a fixed power saving. The hypotheses are only scalar size relations for the actual logarithmic phase.

theorem logarithmic_terminal_range_bound (k : ℕ) (hk : 1 ≤ k) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ (a U Z x : ℝ) (N : ℕ) (hs : List ℝ),
      2 ≤ U → hs.length+1=k →
      (∀ h ∈ hs, 1 ≤ h ∧ h ≤ U^(1/(10*(k:ℝ)))) →
      U^(-(3:ℝ)/2) ≤ |Z| *U^(-((k:ℝ)+1)) →
      |Z| *U^(-((k:ℝ)+1)) ≤ U^(-(1:ℝ)/2) →
      U ≤ x → x+(N:ℝ)+hs.sum ≤ 4*U → (N:ℝ) ≤ 3*U →
      ‖∑ j ∈ Finset.range N, ExponentialSum.phase
        (forwardDifference hs (fun y => a*y+Z*Real.log y) ((j:ℝ)+x))‖ ≤
        C*U^((4:ℝ)/5) := by
…

theorem OAI.JointDickman.logarithmic_terminal_interval_bound line 61