OAI/NumberTheory/JointDickman/Amplification/PublishedRampProfile.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.JointDickman.primeRampCell line 13
2. theorem OAI.JointDickman.primeRampProfile_from_published line 24

   Source documentation

   Uniform bounded Lipschitz profiles and their actual weighted cell law. The constants may depend on the fixed ramp, never on the partition or B.

   theorem primeRampProfile_from_published
       (hSD : PublishedInputs.SquarefreeSelbergDelangeInput)
       (hSW : PublishedInputs.SquarefreeCharacterEstimateInput)
       (hM : PublishedInputs.PrimeReciprocalMertensInput)
       (hMP : PublishedInputs.PrimeProductMertensInput) :
       ∃ v : ℕ → ℝ, v 0 = squarefreeLeadingConstant (1 / 4) ∧
         ∃ H : ℕ, ∃ C : ℝ, 0 < C ∧ ∀ lo hi : ℝ, 0 < lo → lo < hi →
         ∃ M L : ℝ≥0, ∀ᶠ B : ℕ in atTop,
           (∀ x, |rampDensity (scaledRoughDensity v (1 / 4) H B) lo hi x| ≤ M) ∧
           LipschitzWith L (rampDensity (scaledRoughDensity v (1 / 4) H B) lo hi) ∧
           ∀ (D : Type*) [DecidableEq D], ∀ (q : ℕ) [NeZero q], (q : ℝ) ≤ (B : ℝ) ^ (100 : ℝ) →
           ∀ lower upper : D → ℝ,
   …

   Mentions: OAI.JointDickman.PublishedInputs.SquarefreeSelbergDelangeInput, OAI.JointDickman.PublishedInputs.SquarefreeCharacterEstimateInput, OAI.JointDickman.PublishedInputs.PrimeReciprocalMertensInput, OAI.JointDickman.PublishedInputs.PrimeProductMertensInput, OAI.JointDickman.squarefreeLeadingConstant, OAI.JointDickman.rampDensity, OAI.JointDickman.scaledRoughDensity

3. theorem OAI.JointDickman.primeRampCell_normalized_error line 66

   Source documentation

   The integral profile can be evaluated at a cell endpoint after normalization, with explicit local-law and mesh errors.

   theorem primeRampCell_normalized_error {D : Type*} [DecidableEq D]
       {v : ℕ → ℝ} {H B q : ℕ} {lower upper : D → ℝ} {lo hi : ℝ} {L : ℝ≥0} {ε : ℝ}
       (hφ : 0 < (q.totient : ℝ))
       (hLip : LipschitzWith L (rampDensity (scaledRoughDensity v (1 / 4) H B) lo hi))
       (c : auxiliaryPrimes B → Bool) (d : D) (r : (ZMod q)ˣ)
       (horder : lower d < upper d)
       (hlocal : |primeRampCell B q lower upper lo hi c (d, r) -
         (∫ x in lower d..upper d,
           rampDensity (scaledRoughDensity v (1 / 4) H B) lo hi
             (x - Real.log (retainedPrimeProduct (auxiliaryPrimes B) c) / B)) / q.totient| ≤ ε) :
       |primeRampCell B q lower upper lo hi c (d, r) / ((upper d - lower d) / q.totient) -
         rampDensity (scaledRoughDensity v (1 / 4) H B) lo hi
   …

   Mentions: OAI.JointDickman.rampDensity, OAI.JointDickman.scaledRoughDensity, OAI.JointDickman.auxiliaryPrimes, OAI.JointDickman.primeRampCell, OAI.JointDickman.retainedPrimeProduct