ScaledCoefficientLaw.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

The scaled coefficient law with explicit oscillatory savings

theorem OAI.JointDickman.coefficient_scaled_oscillatory_test line 17

Source documentation

The analytic estimate in equation (1), before evaluating the finite unit-phase sum. The expansion order is independent of the smooth test.

theorem coefficient_scaled_oscillatory_test
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ c : ℕ → ℝ, c 0 = squarefreeLeadingConstant (1 / 2) ∧ 0 < c 0 ∧
      ∃ H : ℕ, ∃ K : ℝ, 0 ≤ K ∧ ∀ᶠ B : ℕ in atTop,
      ∀ a b X : ℝ, 0 < a → a ≤ b → 0 < X → 9 ≤ a * X →
      (B : ℝ) ^ (89 / 100 : ℝ) ≤ Real.log (a * X) →
      ∀ (q : ℕ) [NeZero q], (q : ℝ) ≤ (B : ℝ) ^ (15 : ℝ) →
      ∀ ψ : ZMod q → ℂ, (∀ r : (ZMod q)ˣ, ‖ψ r‖ ≤ 1) →
      ∀ (w w' : ℝ → ℝ) (M N ξ : ℝ), 0 ≤ M → 0 ≤ N →
      (∀ t, HasDerivAt w (w' t) t) → Continuous w' →
…

Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.squarefreeLeadingConstant