IntegratedCoefficientLaw.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

The integrated major-arc coefficient law from the published arithmetic inputs

theorem OAI.JointDickman.majorArc_error_power line 12

theorem OAI.JointDickman.coefficient_majorArc_integral_law line 28

Source documentation

The coefficient is replaced inside the full major-arc integral, with a uniform O(B^-13) error. The three hypotheses are exactly the published Selberg--Delange, squarefree-character and reciprocal-Mertens inputs.

theorem coefficient_majorArc_integral_law
    (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
    (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
    (hM : PublishedInputs.PrimeReciprocalMertensInput) :
    ∃ c : ℕ → ℝ, c 0 = squarefreeLeadingConstant (1/2) ∧ 0 < c 0 ∧
      ∃ H : ℕ, ∃ K : ℝ, 0 ≤ K ∧ ∀ a b : ℝ, 0 < a → a ≤ b →
      ∀ᶠ B : ℕ in atTop, ∀ X : ℝ, 0 < X →
      Real.log X ∈ Set.Icc ((9/10 : ℝ)*B) ((11/5 : ℝ)*B) →
      ∀ j : ℕ, ∀ (_ : NeZero j),
      ∀ (w w' : ℝ → ℝ) (M N : ℝ), 0 ≤ M → 0 ≤ N →
      (∀ x, HasDerivAt w (w' x) x) → Continuous w' →
      (∀ x, |w x| ≤ M) → (∀ x, |w' x| ≤ N) →
…

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