OAI/NumberTheory/TotientAsymptotic/WeightedCoefficient.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.TotientAsymptotic.weighted_value_mass_approximation line 11

   Source documentation

   The weighted mass comparison includes every exceptional value and tuple.

   theorem weighted_value_mass_approximation (hscale : FordScaleBounds)
       (hstruct : ExtractedStructureInput) (hpnt : PrimeNumberTheoremInput)
       (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
       (h26 : FordLemma26Input) (h51 : FordLemma51Input) (k : ℕ) (hk : 1 ≤ k) :
       ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
         ∀ᶠ H : ℕ in atTop, ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℝ in atTop,
           |normalizedCount (N k) x-M x H (fk k)/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.normalizedCount, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.fk, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m

2. theorem OAI.TotientAsymptotic.weighted_value_coefficient_approximation line 32
3. theorem OAI.TotientAsymptotic.conditional_companion_additive line 61

   Source documentation

   The additive weighted asymptotic and its uniform arithmetic coefficient.

   theorem conditional_companion_additive (hscale : FordScaleBounds)
       (hstruct : ExtractedStructureInput) (hpnt : PrimeNumberTheoremInput)
       (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
       (h26 : FordLemma26Input) (h51 : FordLemma51Input) (hconc : FordCoordinateConcentrationInput)
       (k : ℕ) (hk : 1 ≤ k) :
       TendstoUniformlyOn (fun H => AH H (fk k)) (A (fk k)) atTop (Set.Ico (0 : ℝ) 1) ∧
         Tendsto (fun x => normalizedCount (N k) x-A (fk k) (theta x)) atTop (nhds 0) := 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.FordCoordinateConcentrationInput, OAI.TotientAsymptotic.AH, OAI.TotientAsymptotic.fk, OAI.TotientAsymptotic.A, OAI.TotientAsymptotic.normalizedCount, OAI.TotientAsymptotic.N, OAI.TotientAsymptotic.theta