PeriodicCoefficientLaw.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Coefficient estimates against bounded periodic phases

theorem OAI.JointDickman.coefficientWeight_isUnit line 13

theorem OAI.JointDickman.coefficient_periodic_smooth_test line 23

Source documentation

Summing unit progressions costs at most the modulus. The bounded periodic phase is arbitrary, so additive phases are included.

theorem coefficient_periodic_smooth_test
    (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,
      ∀ a b : ℝ, 9 ≤ a → a ≤ b → (B : ℝ) ^ (89 / 100 : ℝ) ≤ Real.log a →
      ∀ (q : ℕ) [NeZero q], (q : ℝ) ≤ (B : ℝ) ^ (100 : ℝ) →
      ∀ ψ : ZMod q → ℂ, (∀ r : (ZMod q)ˣ, ‖ψ r‖ ≤ 1) →
      ∀ φ φ' : ℝ → ℂ, ∀ M N : ℝ, 0 ≤ M → 0 ≤ N →
      (∀ t ∈ Set.Icc a b, HasDerivAt φ (φ' t) t) → ContinuousOn φ' (Set.Icc a b) →
…

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