PrimeReciprocalLaw.lean`

6 declarations, 0 contain sorry, 0 declared as axioms

Restore the harmonic mass after using the normalized prime law.

def OAI.TwoPointCorrelations.primeHarmonicMass line 12
def OAI.TwoPointCorrelations.primeReciprocalLaw line 15
lemma OAI.TwoPointCorrelations.primeReciprocalLaw_atom_le line 22
lemma OAI.TwoPointCorrelations.primeReciprocalLaw_mass_product line 34
lemma OAI.TwoPointCorrelations.primeReciprocalLaw_restore line 47
Source documentation
Every abstract label keeps its reciprocal factor, even when distinct labels receive the same numerical prime.
```
lemma primeReciprocalLaw_restore (P : Finset ℕ) (hV : 0 < primeHarmonicMass P)
    (E : (α → P) → Prop) :
    (∑ x : α → P, if E x then ∏ z, ((x z).val : ℝ)⁻¹ else 0) =
      primeHarmonicMass P ^ Fintype.card α *
        (FiniteLaw.independent (fun _ : α => primeReciprocalLaw P hV)).probability E := by
…
```
Mentions: OAI.TwoPointCorrelations.primeHarmonicMass, OAI.TwoPointCorrelations.FiniteLaw.independent, OAI.TwoPointCorrelations.primeReciprocalLaw
lemma OAI.TwoPointCorrelations.primeReciprocalLaw_restore_bound line 61