PaddingBinMassTotal.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

The actual finite harmonic mass in the manuscript's half-open bins. Its lower bound follows from the proved reciprocal padding law and its upper bound simply removes the two restrictions.

def OAI.TwoPointCorrelations.paddingPairHarmonicMass line 14
def OAI.TwoPointCorrelations.totalPaddingBinMass line 21
Source documentation
This is the literal S₀: the index restriction is on the left endpoint of each bin, exactly as in q:bins.
```
noncomputable def totalPaddingBinMass (D Q : Finset ℕ) (L η : ℝ) : ℝ :=
…
```
lemma OAI.TwoPointCorrelations.padding_bin_weight_sum line 28
lemma OAI.TwoPointCorrelations.totalPaddingBinMass_eq line 47
lemma OAI.TwoPointCorrelations.paddingPairHarmonicMass_probability line 58
lemma OAI.TwoPointCorrelations.paddingPairHarmonicMass_bounds line 90
theorem OAI.TwoPointCorrelations.totalPaddingBinMass_bounds line 106

theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_totalPaddingBinMass line 137

Source documentation

The manuscript's retained bin mass bound, uniform over every finite centered divisor family with the proved logarithmic size restriction.

theorem ModFiveThetaInput.eventually_totalPaddingBinMass (hP : ModFiveThetaInput)
    (E : Finset ℕ) :
    ∀ᶠ L : ℝ in atTop, ∀ (D : Finset ℕ) (η : ℝ), 0 < η →
      (∀ d ∈ D, 0 < d ∧ Real.log d ≤ 2 * L) →
      (1 / 2 : ℝ) * paddingTiltNormalizer (paddingPrimeSupply E L) *
          (∑ d ∈ D, 1 / (d : ℝ)) ≤ totalPaddingBinMass D (paddingPrimeSupply E L) L η ∧
        totalPaddingBinMass D (paddingPrimeSupply E L) L η ≤
          paddingTiltNormalizer (paddingPrimeSupply E L) * (∑ d ∈ D, 1 / (d : ℝ)) := by
…

Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.paddingTiltNormalizer, OAI.TwoPointCorrelations.paddingPrimeSupply, OAI.TwoPointCorrelations.totalPaddingBinMass