OAI/Combinatorics/ContingencyTables/Sampling/PhysicalRepairMass.lean

GitHub source file

5 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.SmallGraphProfiles.completionJointDefect line 17
2. lemma OAI.ContingencyTables.SmallGraphProfiles.jointRepair_small_entry line 24
3. def OAI.ContingencyTables.SmallGraphProfiles.repairedCompletion line 36
4. lemma OAI.ContingencyTables.SmallGraphProfiles.repairedCompletion_injective line 59
5. theorem OAI.ContingencyTables.SmallGraphProfiles.physical_repair_weight_le line 78

   Source documentation

   The repair is the manuscript's actual profile map, and the weight inequality counts all completions through its explicit injective map.

   theorem physical_repair_weight_le (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)
       (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)
       (hf : 0 < hardMarginal (firstPaperSmall r c U) B r c L z) :
       hardMarginal (firstPaperSmall r c U) B r c L z ≤
   …

   Mentions: OAI.ContingencyTables.IsDefect, OAI.ContingencyTables.ResidualTables