TupleOccurrences.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Identify the singleton count and reciprocal weight of actual tuple slots.

lemma OAI.TwoPointCorrelations.tupleSlotLabel_occurrences line 13
lemma OAI.TwoPointCorrelations.tupleSlotLabel_singletons line 30
lemma OAI.TwoPointCorrelations.tupleSlotLabel_image line 36
lemma OAI.TwoPointCorrelations.tupleSlotLabel_reciprocal line 52
Source documentation
The baseline from singleton integration is exactly the columnwise weight used in the universal pattern and padding sum.
```
lemma tupleSlotLabel_reciprocal {J R : ℕ} {P : Fin J → Finset ℕ}
    (w : ColumnPrimeAssignment J R P) :
    (∏ c ∈ univ.image (tupleSlotLabel w), (c.2.val : ℝ)⁻¹) = columnReciprocalWeight w := by
…
```
Mentions: OAI.TwoPointCorrelations.ColumnPrimeAssignment, OAI.TwoPointCorrelations.tupleSlotLabel, OAI.TwoPointCorrelations.columnReciprocalWeight