OAI/Combinatorics/ContingencyTables/Sampling/PhysicalResidualMargins.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.SmallGraphProfiles.residualRows line 17
2. def OAI.ContingencyTables.SmallGraphProfiles.residualColumns line 21
3. lemma OAI.ContingencyTables.SmallGraphProfiles.physical_weight_completions line 25
4. lemma OAI.ContingencyTables.SmallGraphProfiles.physical_completions_nonempty line 41
5. lemma OAI.ContingencyTables.SmallGraphProfiles.physical_residual_totals line 53
6. lemma OAI.ContingencyTables.SmallGraphProfiles.physical_residual_row_zero line 66

   Source documentation

   Rows outside the large-margin rectangle have zero residual, as forced by the actual positive completion count.

   lemma physical_residual_row_zero (r : I → ℕ) (c : J → ℕ) (U L : ℕ) (B : I → J → ℕ)
       (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)
       (i : I) (hi : ¬U ≤ r i) :
       residualRows (firstPaperSmall r c U) B r c L z i=0 := by
   …

   Mentions: OAI.ContingencyTables.SmallGraphProfiles.PhysicalStates, OAI.ContingencyTables.SmallGraphProfiles.residualRows

7. lemma OAI.ContingencyTables.SmallGraphProfiles.physical_residual_column_zero line 81
8. theorem OAI.ContingencyTables.SmallGraphProfiles.physical_weight_rectangle line 98

   Source documentation

   Thus the marginal used by the variance proof is exactly the number of ordinary tables on the large rectangle, including empty rectangles.

   theorem physical_weight_rectangle (r : I → ℕ) (c : J → ℕ) (U L : ℕ) (B : I → J → ℕ)
       (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
           (fun i : {i // U ≤ r i} => residualRows (firstPaperSmall r c U) B r c L z i.val)
           (fun j : {j // U ≤ c j} => residualColumns (firstPaperSmall r c U) B r c L z j.val)):ℝ) := by
   …

   Mentions: OAI.ContingencyTables.SmallGraphProfiles.PhysicalStates, OAI.ContingencyTables.SmallGraphProfiles.residualRows, OAI.ContingencyTables.SmallGraphProfiles.physicalProfile, OAI.ContingencyTables.Table, OAI.ContingencyTables.SmallGraphProfiles.residualColumns