LargePairEnumeration.lean`

14 declarations, 0 contain sorry, 0 declared as axioms

Physical indexing of all balanced large-cell pairs

The recursively added pairs are identified with the actual finite cells, and their assignments with the dependent product of the physical finite intervals. No extra coordinate or assignment multiplicity is introduced.

def OAI.ContingencyTables.LargePairEnumeration.widths line 22
Source documentation
Widths in the explicit order supplied by a finite cell enumeration.
```
def widths : {n : ℕ} → (Fin n → ℕ) → List ℕ
  | 0,_ => []
  | _+1,M => M 0::widths (fun i => M i.succ)
```
lemma OAI.ContingencyTables.LargePairEnumeration.widths_lower line 26
def OAI.ContingencyTables.LargePairEnumeration.pairSuccEquiv line 37

def OAI.ContingencyTables.LargePairEnumeration.coordinateEquiv line 51

Source documentation

The nested coordinate sums contain exactly the retained coordinates and one doubled coordinate for each physical large cell.

def coordinateEquiv (S : Type u) : {n : ℕ} → (M : Fin n → ℕ) →
    Coordinates S (widths M) ≃ S⊕(Fin n×Bool)
  | 0,_ => (Equiv.sumEmpty S (Fin 0×Bool)).symm
  | n+1,M =>
    (Equiv.sumCongr (coordinateEquiv S (fun i => M i.succ)) (Equiv.refl Bool)).trans
      ((Equiv.sumAssoc S (Fin n×Bool) Bool).trans
        (Equiv.sumCongr (Equiv.refl S) (pairSuccEquiv n)))

/-- Balanced choices are the dependent product of the actual intervals. -/

Mentions: OAI.ContingencyTables.LargePairEnumeration.widths, OAI.ContingencyTables.LargePairEnumeration.pairSuccEquiv

def OAI.ContingencyTables.LargePairEnumeration.assignmentEquiv line 60
Source documentation
Balanced choices are the dependent product of the actual intervals.
```
def assignmentEquiv : {n : ℕ} → (M : Fin n → ℕ) →
    Assignments (widths M) ≃ ((i : Fin n) → Fin (M i+1))
  | 0,_ =>
    { toFun := fun _ i => Fin.elim0 i
…
```
Mentions: OAI.ContingencyTables.LargePairEnumeration.widths
def OAI.ContingencyTables.LargePairEnumeration.joinedProfile line 79
lemma OAI.ContingencyTables.LargePairEnumeration.embedding_coordinate line 84
theorem OAI.ContingencyTables.LargePairEnumeration.eliminate_eq_physical_sum line 109
Source documentation
The recursively proved marginal is the direct finite sum over the actual physical intervals.
```
theorem eliminate_eq_physical_sum {S : Type*} {n : ℕ} (M : Fin n → ℕ)
    (F : (S⊕(Fin n×Bool) → ℕ) → ℝ) (z : S → ℕ) :
    eliminate (widths M) (fun q => F (q ∘ (coordinateEquiv S M).symm)) z=
      ∑ a : ((i : Fin n) → Fin (M i+1)), F (joinedProfile M z a) := by
…
```
Mentions: OAI.ContingencyTables.LargePairEnumeration.widths, OAI.ContingencyTables.LargePairEnumeration.coordinateEquiv, OAI.ContingencyTables.LargePairEnumeration.joinedProfile
def OAI.ContingencyTables.LargePairEnumeration.SmallView line 123
def OAI.ContingencyTables.LargePairEnumeration.LargeCell line 125
def OAI.ContingencyTables.LargePairEnumeration.partitionEquiv line 129
Source documentation
This is the actual partition of doubled cells into small views and large pairs.
```
noncomputable def partitionEquiv (small : C → Bool) :
    SmallView small⊕(LargeCell small×Bool) ≃ C×Bool where
…
```
Mentions: OAI.ContingencyTables.LargePairEnumeration.SmallView, OAI.ContingencyTables.LargePairEnumeration.LargeCell
def OAI.ContingencyTables.LargePairEnumeration.physicalJoinEquiv line 144
def OAI.ContingencyTables.LargePairEnumeration.physicalCoordinateEquiv line 151
Source documentation
Every finite enumeration of the large cells gives the same physical coordinate space, with each original doubled cell appearing once.
```
noncomputable def physicalCoordinateEquiv (small : C → Bool) {n : ℕ}
    (e : Fin n ≃ LargeCell small) (M : Fin n → ℕ) :
    Coordinates (SmallView small) (widths M) ≃ C×Bool :=
…
```
Mentions: OAI.ContingencyTables.LargePairEnumeration.LargeCell, OAI.ContingencyTables.LargePairEnumeration.SmallView, OAI.ContingencyTables.LargePairEnumeration.widths
theorem OAI.ContingencyTables.LargePairEnumeration.eliminate_eq_actual_cells line 156