OAI/NumberTheory/JointDickman/Counting/CoefficientWeights.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.coefficientScale line 13
2. def OAI.JointDickman.coefficientWeight line 16
3. def OAI.JointDickman.coefficientModel line 19
4. def OAI.JointDickman.coefficientDensity line 24
5. theorem OAI.JointDickman.coefficientScale_nonneg line 27
6. theorem OAI.JointDickman.coefficientWeight_nonneg line 32
7. theorem OAI.JointDickman.coefficientScale_eventually_le line 38
8. theorem OAI.JointDickman.coefficientProgression_eq line 49
9. theorem OAI.JointDickman.hasDerivAt_coefficientModel line 58
10. theorem OAI.JointDickman.coefficientProgression_expansion line 72

    Source documentation

    The progression expansion for the actual A₀ weight, retaining an arbitrary prescribed polynomial saving after normalization.

    theorem coefficientProgression_expansion
        (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
        (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
        (hM : PublishedInputs.PrimeReciprocalMertensInput)
        {D : ℝ} (hD : 0 ≤ D) :
        ∃ c : ℕ → ℝ, c 0 = squarefreeLeadingConstant (1 / 2) ∧ 0 < c 0 ∧
          ∃ H : ℕ, ∃ K : ℝ, 0 ≤ K ∧ ∀ᶠ B : ℕ in atTop, ∀ Y : ℝ,
            (B : ℝ) ^ (89 / 100 : ℝ) ≤ Real.log Y → 9 ≤ Y →
            ∀ (q : ℕ) [NeZero q], (q : ℝ) ≤ (B : ℝ) ^ (100 : ℝ) → ∀ r : (ZMod q)ˣ,
            |progressionSum (Ioc 0 ⌊Y⌋₊) (coefficientWeight B) (r : ZMod q) -
              coefficientModel c H B Y / q.totient| ≤ K * Y * (B : ℝ) ^ (-D) := by
    …

    Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.squarefreeLeadingConstant, OAI.JointDickman.progressionSum, OAI.JointDickman.coefficientWeight, OAI.JointDickman.coefficientModel