PhysicalCompletionFibres.lean`

9 declarations, 0 contain sorry, 0 declared as axioms

Completion-retaining fibres of the literal hard marginal

Each physical large-cell assignment with zero penalty is exactly one pair of full row and column views. The retained small profile is prescribed, while large entries agree. No completion multiplicity is discarded.

abbrev OAI.ContingencyTables.PhysicalCompletionFibres.SmallProfile line 21
def OAI.ContingencyTables.PhysicalCompletionFibres.CompletionFibre line 25
Source documentation
Full row/column views with one prescribed small profile.
```
def CompletionFibre (small : I → J → Bool) (B : I → J → ℕ)
    (r rbar : I → ℕ) (c cbar : J → ℕ) (z : SmallProfile small) :=
…
```
Mentions: OAI.ContingencyTables.PhysicalCompletionFibres.SmallProfile
instance OAI.ContingencyTables.PhysicalCompletionFibres.completionFibreFintype line 36
lemma OAI.ContingencyTables.PhysicalCompletionFibres.physical_inBox line 43
def OAI.ContingencyTables.PhysicalCompletionFibres.fibreAssignment line 57
lemma OAI.ContingencyTables.PhysicalCompletionFibres.fibreAssignment_views line 64
def OAI.ContingencyTables.PhysicalCompletionFibres.zeroPhysicalEquiv line 86

theorem OAI.ContingencyTables.PhysicalCompletionFibres.hardMarginal_eq_fibre_card line 129

Source documentation

Exact equality, including all completion multiplicities.

theorem hardMarginal_eq_fibre_card (small : I → J → Bool) (B : I → J → ℕ)
    (r : I → ℕ) (c : J → ℕ) (L : ℕ) (z : SmallProfile small)
    (hz : ∀ u, z u ≤ B u.1.val.1 u.1.val.2) :
    hardMarginal small B r c L z=
      (Fintype.card (CompletionFibre small B r (fun i => r i+rowLargeCount small i*L)
        c (fun j => c j+columnLargeCount small j*L) z):ℝ) := by
…

Mentions: OAI.ContingencyTables.PhysicalCompletionFibres.SmallProfile, OAI.ContingencyTables.PhysicalCompletionFibres.CompletionFibre

theorem OAI.ContingencyTables.PhysicalCompletionFibres.fibre_projection_injective line 142
Source documentation
Forgetting the retained profile loses no information on a bounded injective family of profiles. In particular all later fibre sums count full state/completion pairs exactly once.
```
theorem fibre_projection_injective {S : Type*}
    (small : I → J → Bool) (B : I → J → ℕ)
    (r rbar : I → ℕ) (c cbar : J → ℕ) (p : S → SmallProfile small)
    (hp : Function.Injective p) (hbox : ∀ s u, p s u ≤ B u.1.val.1 u.1.val.2) :
    Function.Injective (fun a : (s : S) × CompletionFibre small B r rbar c cbar (p s) =>
      a.2.val) := by
…
```
Mentions: OAI.ContingencyTables.PhysicalCompletionFibres.SmallProfile, OAI.ContingencyTables.PhysicalCompletionFibres.CompletionFibre