TransversalCount.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

Exact binomial/factorial cancellation in a transversal normalizer

Every small integer profile has a product of binomial numbers of label preimages. Its factorial lift contributes the inverse product, so the actual transversal normalizer is exactly the raw integer-profile sum.

def OAI.ContingencyTables.TransversalCount.Profile line 21
def OAI.ContingencyTables.TransversalCount.cardAt line 23
def OAI.ContingencyTables.TransversalCount.cardProfile line 26
def OAI.ContingencyTables.TransversalCount.display line 29
lemma OAI.ContingencyTables.TransversalCount.local_fiber line 33
lemma OAI.ContingencyTables.TransversalCount.profile_fiber line 54
theorem OAI.ContingencyTables.TransversalCount.choices_sum line 74
Source documentation
Pushforward of the actual finite labelled-choice weights is counting measure on the bounded integer profiles.
```
theorem choices_sum (H : Profile b → ℝ) :
    (∑ S : ((c : C) → Finset (Fin (b c))),H (cardProfile b S)*
      ∏ c,InitialLocalChoices.localWeight (b c) 0 0 (S c))=∑ x : Profile b,H x := by
…
```
Mentions: OAI.ContingencyTables.TransversalCount.Profile, OAI.ContingencyTables.TransversalCount.cardProfile, OAI.ContingencyTables.InitialLocalChoices.localWeight
lemma OAI.ContingencyTables.TransversalCount.count_encode line 87
lemma OAI.ContingencyTables.TransversalCount.firstLift_encode line 96
theorem OAI.ContingencyTables.TransversalCount.slotTotal_eq_profiles line 108
Source documentation
The literal factorial lift's transversal normalizer is the original integer-profile count, for arbitrary raw h and arbitrary capacities.
```
theorem slotTotal_eq_profiles (h : (C×Bool → ℕ) → ℝ) :
    slotTotal pairs (firstLift (group (cell b)) h (InitialTransversals.denominator b)) ∅=
      ∑ x : Profile b,h (display b x) := by
…
```
Mentions: OAI.ContingencyTables.InitialTransversals.denominator, OAI.ContingencyTables.TransversalCount.Profile, OAI.ContingencyTables.TransversalCount.display
theorem OAI.ContingencyTables.CompanionTransversalCount.total_eq_raw_profiles line 136
Source documentation
Exact binomial/factorial cancellation for the manuscript's literal softened completion count, including the terminal annealing parameter.
```
theorem total_eq_raw_profiles (A : Instance I J) (alpha : ℝ) :
    slotTotal pairs (f A alpha) ∅=
      ∑ x : TransversalCount.Profile (fun s : SmallCell A => A.b s.val.1 s.val.2),
        h A alpha (TransversalCount.display (fun s : SmallCell A => A.b s.val.1 s.val.2) x) := by
…
```
Mentions: OAI.ContingencyTables.TransversalCount.Profile, OAI.ContingencyTables.TransversalCount.display