WeightedMass.lean`

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

def OAI.TotientAsymptotic.candidateMass line 12
lemma OAI.TotientAsymptotic.mass_eq_prefix_denominators line 16
lemma OAI.TotientAsymptotic.candidate_mass_perturbation line 22
theorem OAI.TotientAsymptotic.candidate_prime_mass_relative line 41
Source documentation
Summation of the actual least-preimage prime intervals, before replacing its prefix ratio by the tail ratio.
```
theorem candidate_prime_mass_relative (hpnt : PrimeNumberTheoremInput) :
    ∀ᶠ H : ℕ in atTop, ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℝ in atTop,
      ∀ k : ℕ, 1 ≤ k →
      |((candidateTuples x H k).card : ℝ)-(x/Real.log x)*candidateMass x H k| ≤
        ε*(x/Real.log x)*M x H (fun _ => 1) := by
…
```
Mentions: OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.candidateTuples, OAI.TotientAsymptotic.candidateMass, OAI.TotientAsymptotic.M
theorem OAI.TotientAsymptotic.candidate_mass_normalized line 79
Source documentation
The weighted counting error vanishes with the discrete tail cutoff.
```
theorem candidate_mass_normalized (hpnt : PrimeNumberTheoremInput)
    (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) (hmertens : MertensProductInput)
    (k : ℕ) (hk : 1 ≤ k) :
    ∃ δ : ℕ → ℝ, Tendsto δ atTop (nhds 0) ∧
      ∀ᶠ H : ℕ in atTop, ∀ ε : ℝ, 0 < ε → ∀ᶠ x : ℝ in atTop,
        |((candidateTuples x H k).card : ℝ)/tupleNormalization x-
          M x H (fk k)/G x (m x)| ≤ δ H+ε := by
…
```
Mentions: OAI.TotientAsymptotic.PrimeNumberTheoremInput, OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.MertensProductInput, OAI.TotientAsymptotic.candidateTuples, OAI.TotientAsymptotic.M, OAI.TotientAsymptotic.fk, OAI.TotientAsymptotic.G, OAI.TotientAsymptotic.m