ReferenceCompletionBlock.lean`

GitHub source file

6 declarations, 0 contain sorry, 0 declared as axioms

Fixed reference row and column for the physical completion blocks

abbrev OAI.ContingencyTables.SmallGraphProfiles.LargeRows line 17
abbrev OAI.ContingencyTables.SmallGraphProfiles.LargeColumns line 18
def OAI.ContingencyTables.SmallGraphProfiles.referenceRows line 20
def OAI.ContingencyTables.SmallGraphProfiles.referenceColumns line 25
lemma OAI.ContingencyTables.SmallGraphProfiles.reference_totals line 30
theorem OAI.ContingencyTables.SmallGraphProfiles.physical_weight_reference_block line 60
Source documentation
A single pair of reference indices, fixed independently of the state, reindexes every actual completion block and retains its exact count.
```
theorem physical_weight_reference_block (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) :
    hardMarginal (firstPaperSmall r c U) B r c L (physicalProfile _ B r c L z)=
      (Fintype.card (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