PaddingLiteralBins.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

The bin mass is the literal normalized sum of padding-divisor weights. Boolean selections are finite subsets, so no extra multiplicity is present.

def OAI.TwoPointCorrelations.selectedCoordinates line 16
def OAI.TwoPointCorrelations.selectionFinsetEquiv line 19
lemma OAI.TwoPointCorrelations.selection_supported_iff line 27
lemma OAI.TwoPointCorrelations.paddingTiltWeight_eq_five_pow line 32
lemma OAI.TwoPointCorrelations.paddingDivisorCoefficient_eq_four_pow line 37
def OAI.TwoPointCorrelations.paddingSelectedDivisor line 42
lemma OAI.TwoPointCorrelations.paddingSelectedDivisor_log line 45
lemma OAI.TwoPointCorrelations.paddingBinMass_normalized_sum line 52
lemma OAI.TwoPointCorrelations.paddingBinMass_subset_formula line 69
Source documentation
The finite subset formula exactly matches rho: sum the weight 4^omega(q) over available squarefree padding divisors in the bin and normalize by 5^omega_Q.
```
lemma paddingBinMass_subset_formula (Q : Finset ℕ) (a : Q → Bool)
    (η c : ℝ) (j : ℤ) :
    paddingBinMass Q a η c j = (5 : ℝ) ^ (-(selectedCoordinates Q a).card : ℤ) *
      ∑ S : Finset Q,
        if S ⊆ selectedCoordinates Q a ∧
          paddingBin η c (∑ p ∈ S, Real.log p.val) = j
        then (4 : ℝ) ^ S.card else 0 := by
…
```
Mentions: OAI.TwoPointCorrelations.paddingBinMass, OAI.TwoPointCorrelations.selectedCoordinates, OAI.TwoPointCorrelations.paddingBin