FirstPaperStationaryMass.lean`

4 declarations, 0 contain sorry, 0 declared as axioms

Completion-retaining repair bounds the stationary normalizer

lemma OAI.ContingencyTables.SmallGraphProfiles.physical_mass_eq_profiles line 18
lemma OAI.ContingencyTables.SmallGraphProfiles.physical_mass_eq_words_defects line 32

lemma OAI.ContingencyTables.SmallGraphProfiles.defect_mass_le_words line 50

Source documentation

The repair preserves all completions and has at most one preimage per ordered defect label. Thus defect mass costs at most |S| squared.

lemma defect_mass_le_words (r : I → ℕ) (c : J → ℕ) (U L : ℕ) (B : I → J → ℕ)
    (hB : ∀ i j,firstPaperSmall r c U i j=true → B i j=U)
    (hcap : ∀ T : ResidualTables (firstPaperSmall r c U) r c
      (fun i => r i+rowLargeCount (firstPaperSmall r c U) i*L)
      (fun j => c j+columnLargeCount (firstPaperSmall r c U) j*L),∀ i j,T.val.val i j ≤ B i j) :
    (∑ z : PositiveDefects (firstPaperSmall r c U) B r c L,
      hardMarginal (firstPaperSmall r c U) B r c L (naturalProfile z.val)) ≤
      (Fintype.card (Cells (firstPaperSmall r c U)×Cells (firstPaperSmall r c U)):ℝ)*
        ∑ a,wordWeight (firstPaperSmall r c U) B r c L U a := by
…

Mentions: OAI.ContingencyTables.ResidualTables, OAI.ContingencyTables.SmallGraphProfiles.PositiveDefects

theorem OAI.ContingencyTables.SmallGraphProfiles.state_mass_le_balanced line 69
Source documentation
The normalizer of the actual small chain is bounded by balanced completion mass times the manuscript's polynomial defect factor.
```
theorem state_mass_le_balanced (r : I → ℕ) (c : J → ℕ) :
    (∑ z,stateWeight r c z) ≤
      (1+(dimensionAllowance (I := I) (J := J):ℝ)^2)*
…
```
Mentions: OAI.ContingencyTables.SmallGraphProfiles.stateWeight