SmallRepairCapacity.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

A positive physical defect repairs inside the literal small box

theorem OAI.ContingencyTables.SmallGraphProfiles.repair_small_capacity line 20

Source documentation

Positive hard marginal supplies an actual full completion. Its preserved residual bounds force each repaired small entry below U.

theorem repair_small_capacity (r : I → ℕ) (c : J → ℕ) (U L : ℕ) (B : I → J → ℕ)
    (hB : ∀ i j,firstPaperSmall r c U i j=true → B i j=U)
    (z : SmallProfile (firstPaperSmall r c U))
    (hz : ∀ a,z a ≤ B a.1.val.1 a.1.val.2) (s t : I×J)
    (hs : firstPaperSmall r c U s.1 s.2=true) (ht : firstPaperSmall r c U t.1 t.2=true)
    (hd : IsDefect (smallView (firstPaperSmall r c U) z false)
      (smallQ (firstPaperSmall r c U) B z) s t)
    (hf : 0 < hardMarginal (firstPaperSmall r c U) B r c L z) :
    ∀ a : Cells (firstPaperSmall r c U),
      repairMatrix (smallView (firstPaperSmall r c U) z false) s t a.val.1 a.val.2 ≤ B a.val.1 a.val.2 := by
…

Mentions: OAI.ContingencyTables.IsDefect, OAI.ContingencyTables.repairMatrix