ProjectedMass.lean`

3 declarations, 0 contain sorry, 0 declared as axioms

Uniform summation over the possible common prime prefixes.

def OAI.TotientAsymptotic.projectedPrimeFactor line 14
lemma OAI.TotientAsymptotic.projectedPrimeFactor_tendsto line 17
theorem OAI.TotientAsymptotic.projected_mass_le_G line 30
Source documentation
Uniformly over every late truncation, the whole projected prime mass is at most the normalizing full-dimensional volume. This includes the empty prime prefix, whose mass is one.
```
theorem projected_mass_le_G (hbox : FordUnitPrimeBoxInput) (hren : FordRenewalInput) :
    ∀ᶠ H : ℕ in atTop, ∀ᶠ x : ℝ in atTop, ∀ K : ℕ, H ≤ K → K ≤ m x →
    ∀ Q : Finset (Fin (R x K) → ℕ),
    (∀ p ∈ Q, (∀ j, (p j).Prime) ∧ primePrefixCoord p ∈ prefixBandRegion x K ∧
      primePrefixCoord p ∈ enlargedSimplex (R x K) (B x) (xi x 0) (fun j => xi x (j.val+1))) →
    (∑ p ∈ Q, reciprocalShiftWeight p) ≤ G x (m x) := by
…
```
Mentions: OAI.TotientAsymptotic.FordUnitPrimeBoxInput, OAI.TotientAsymptotic.FordRenewalInput, OAI.TotientAsymptotic.m, OAI.TotientAsymptotic.R, OAI.TotientAsymptotic.primePrefixCoord, OAI.TotientAsymptotic.prefixBandRegion, OAI.TotientAsymptotic.enlargedSimplex, OAI.TotientAsymptotic.B, OAI.TotientAsymptotic.xi, OAI.TotientAsymptotic.reciprocalShiftWeight, OAI.TotientAsymptotic.G