OAI/NumberTheory/JointDickman/Analysis/MellinWeightedLogPhase.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

Logarithmic cancellation with the two Mellin profile weights

  1. lemma OAI.JointDickman.mellinSieveFunction_dilate line 12
  2. lemma OAI.JointDickman.linear_log_phase_sum_bound line 29
  3. lemma OAI.JointDickman.mellinSieveFunction_left_sum line 40
  4. lemma OAI.JointDickman.mellinSieveFunction_right_sum line 62
  5. theorem OAI.JointDickman.angular_log_phase_uniform line 86

    Source documentation

    Logarithmic phase cancellation in the angular convention.

    theorem angular_log_phase_uniform (B : ℝ) (hB : 1/2 ≤ B) :
    ∃ A δ : ℝ, 0 < A ∧ 0 < δ ∧
      ∀ᶠ U : ℝ in atTop, ∀ (t : ℝ) (L R : ℤ),
        U^(1/2:ℝ) ≤ |t/(2*Real.pi)| → |t/(2*Real.pi)| ≤ U^B →
        U ≤ (L:ℝ) → (R:ℝ) ≤ 2*U →
        ‖∑ n ∈ Icc L R, (n:ℂ)^(-((t:ℂ)*I))‖ ≤ A*U^(1-δ) := by
…