ActualPaddingCuts.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Loss of padding mass from the actual graph density and degree cutoffs. The second moment is applied before discarding the large bins.

lemma OAI.TwoPointCorrelations.FiniteLaw.weighted_large_bin_cut line 13
theorem OAI.TwoPointCorrelations.ModFiveThetaInput.actual_family_padding_large_bin_cut line 34
lemma OAI.TwoPointCorrelations.actualPaddingDensity_sum_le_one line 71
Source documentation
The bin densities form a subprobability distribution even after restricting the available padding divisors.
```
lemma actualPaddingDensity_sum_le_one (Q : Finset ℕ)
    (hQ : ∀ p ∈ Q, p.Prime) (D : Finset ℕ)
    (hD : D ⊆ retainedPrimeDivisors Q) (n : ℤ)
    (η c : ℝ) (hη : 0 < η) (bins : Finset ℤ) :
    (∑ j ∈ bins, paddingDensity D actualPaddingCoefficient (actualPaddingBin η c j)
      (actualPaddingVertex Q) n) ≤ 1 := by
…
```
Mentions: OAI.TwoPointCorrelations.retainedPrimeDivisors, OAI.TwoPointCorrelations.paddingDensity, OAI.TwoPointCorrelations.actualPaddingCoefficient, OAI.TwoPointCorrelations.actualPaddingBin, OAI.TwoPointCorrelations.actualPaddingVertex
lemma OAI.TwoPointCorrelations.actualPadding_keep_loss line 103

theorem OAI.TwoPointCorrelations.ModFiveThetaInput.eventually_actual_padding_keep_loss line 133

Source documentation

Both literal vertex cutoffs together remove only O(1/K) + L⁻¹⁰⁰ of the normalized, padding-weighted mass, summed over all selected bins.

theorem ModFiveThetaInput.eventually_actual_padding_keep_loss
    (hP : ModFiveThetaInput) (E : Finset ℕ) :
    ∃ C : ℝ, 0 < C ∧ ∀ᶠ L : ℝ in atTop,
      ∀ (η c K : ℝ) (h J M B : ℕ) (data : ProhibitedPrimeFamily h J M),
      data.Q = paddingPrimeSupply E L →
      ∀ (site : ℤ) (bins : Finset ℤ), 0 < η → η ≤ 1 → 0 < K →
      ∀ (hB : ∀ p ∈ data.P ∪ data.Q, p ≤ B)
        (D : Finset ℕ), D ⊆ retainedPrimeDivisors data.Q →
      (data.residueLaw B hB).average (fun x =>
        (actualPaddingVertex data.Q (data.residueOrigin x + site)) ^ 2 *
          ∑ j ∈ bins, if ¬integerEdgeKeep D actualPaddingCoefficient
            (actualPaddingBin η c j) (actualPaddingVertex data.Q) L K
…

Mentions: OAI.TwoPointCorrelations.ModFiveThetaInput, OAI.TwoPointCorrelations.ProhibitedPrimeFamily, OAI.TwoPointCorrelations.paddingPrimeSupply, OAI.TwoPointCorrelations.retainedPrimeDivisors, OAI.TwoPointCorrelations.actualPaddingVertex, OAI.TwoPointCorrelations.integerEdgeKeep, OAI.TwoPointCorrelations.actualPaddingCoefficient, OAI.TwoPointCorrelations.actualPaddingBin