OAI/NumberTheory/TotientAsymptotic/ValueMass.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TotientAsymptotic.value_mass_approximation line 13

   Source documentation

   Actual distinct values and the common-endpoint arithmetic mass.

   theorem value_mass_approximation (hscale : FordScaleBounds)
       (hstruct : ExtractedStructureInput) (hpnt : PrimeNumberTheoremInput)
       (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
       (h26 : FordLemma26Input) (h51 : FordLemma51Input) {a : ℝ} (ha : 0 < a) :
       ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
         ∀ᶠ H : ℕ in atTop, ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℝ in atTop,
         ∀ t : ℝ, a*x ≤ t → t ≤ x →
           |V t/tupleNormalization x-(t/x)*(M x H (fun _ => 1)/G x (m x))| ≤ δ H+ε := by
   …

   Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.ExtractedStructureInput, OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.a, OAI.TotientAsymptotic.V, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m

2. lemma OAI.TotientAsymptotic.massError_eq_normalized line 36
3. theorem OAI.TotientAsymptotic.common_endpoint_comparison line 44

   Source documentation

   The common-endpoint estimate is proved from published inputs, rather than assumed as an internal comparison.

   theorem common_endpoint_comparison (hscale : FordScaleBounds)
       (hstruct : ExtractedStructureInput) (hpnt : PrimeNumberTheoremInput)
       (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
       (h26 : FordLemma26Input) (h51 : FordLemma51Input) {c : ℝ} (hc : 1 ≤ c) :
       CommonEndpointComparison c := by
   …

   Mentions: OAI.TotientAsymptotic.FordScaleBounds, OAI.TotientAsymptotic.ExtractedStructureInput, OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.FordLemma26Input, OAI.TotientAsymptotic.FordLemma51Input, OAI.TotientAsymptotic.CommonEndpointComparison