CompletionFibreEquiv.lean`

5 declarations, 0 contain sorry, 0 declared as axioms

Entry-preserving completion equivalences

The finite dense draw is transported to the retained completion fibre by an equivalence preserving every table entry.

abbrev OAI.ContingencyTables.PhysicalCompletionFibres.ZeroPhysical line 22
def OAI.ContingencyTables.PhysicalCompletionFibres.zeroSupportedEquiv line 32
def OAI.ContingencyTables.PhysicalCompletionFibres.fibreLargeEquiv line 43
lemma OAI.ContingencyTables.PhysicalCompletionFibres.fibreLargeEquiv_apply line 60

def OAI.ContingencyTables.SmallGraphProfiles.referenceFibreEquiv line 89

Source documentation

Actual retained completion fibre to the fixed-reference dense block.

noncomputable def referenceFibreEquiv (r : I → ℕ) (c : J → ℕ) (U L : ℕ) (B : I → J → ℕ)
    (i₀ : LargeRows r U) (j₀ : LargeColumns c U)
    (z : PhysicalStates (firstPaperSmall r c U) B r c L)
    (hcap : ∀ i j,firstPaperSmall r c U i j=false →
      (∑ k,residualRows (firstPaperSmall r c U) B r c L z k) ≤ B i j) :
    CompletionFibre (firstPaperSmall r c U) B r
      (fun i => r i+rowLargeCount (firstPaperSmall r c U) i*L) c
      (fun j => c j+columnLargeCount (firstPaperSmall r c U) j*L)
      (physicalProfile _ B r c L z) ≃
    Table (referenceRows r c U L B i₀ z) (referenceColumns r c U L B j₀ z) := by
…

Mentions: OAI.ContingencyTables.SmallGraphProfiles.LargeRows, OAI.ContingencyTables.SmallGraphProfiles.LargeColumns, OAI.ContingencyTables.SmallGraphProfiles.PhysicalStates, OAI.ContingencyTables.SmallGraphProfiles.residualRows, OAI.ContingencyTables.SmallGraphProfiles.physicalProfile, OAI.ContingencyTables.Table, OAI.ContingencyTables.SmallGraphProfiles.referenceRows, OAI.ContingencyTables.SmallGraphProfiles.referenceColumns