OAI/Combinatorics/ContingencyTables/Sampling/SmallContextCount.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. abbrev OAI.ContingencyTables.SmallContextFibres.BalancedPairs line 20
2. def OAI.ContingencyTables.SmallContextFibres.balancedPairChild line 25
3. lemma OAI.ContingencyTables.SmallContextFibres.balancedPairChild_injective line 43
4. lemma OAI.ContingencyTables.SmallContextFibres.balancedPairChild_surjective line 62

   Source documentation

   Every residual table has exactly one balanced retained profile and one large completion, provided the declared capacities exclude none.

   lemma balancedPairChild_surjective {small : I → J → Bool} {B : I → J → ℕ}
       {r rbar : I → ℕ} {c cbar : J → ℕ} {s : I×J} {σ : I×J → ℕ} {k : ℕ}
       (hs : small s.1 s.2=true)
       (hcap : ∀ T : ResidualTables small r c rbar cbar, ∀ i j, T.val.val i j ≤ B i j) :
       Function.Surjective (balancedPairChild (B := B) (r := r) (rbar := rbar)
   …

   Mentions: OAI.ContingencyTables.ResidualTables, OAI.ContingencyTables.SmallContextFibres.balancedPairChild

5. theorem OAI.ContingencyTables.SmallContextFibres.balanced_mass_eq_child_card line 106

   Source documentation

   A contextual child mass is the exact cardinality of full residual tables in that child, including all large completion multiplicities.

   theorem balanced_mass_eq_child_card (small : I → J → Bool) (B : I → J → ℕ)
       (r : I → ℕ) (c : J → ℕ) (L : ℕ) (s : I×J) (σ : I×J → ℕ) (k : ℕ)
       (hs : small s.1 s.2=true)
       (hcap : ∀ T : ResidualTables small r c
         (fun i => r i+rowLargeCount small i*L) (fun j => c j+columnLargeCount small j*L),
         ∀ i j, T.val.val i j ≤ B i j) :
       (∑ z : BalancedProfiles small B s σ k,
         hardMarginal small B r c L (naturalProfile z.val))=
         (Fintype.card (SmallResidualChild small r (fun i => r i+rowLargeCount small i*L)
           c (fun j => c j+columnLargeCount small j*L) s σ k):ℝ) := by
   …

   Mentions: OAI.ContingencyTables.ResidualTables, OAI.ContingencyTables.SmallContextFibres.BalancedProfiles, OAI.ContingencyTables.SmallContextFibres.naturalProfile, OAI.ContingencyTables.SmallContextFibres.SmallResidualChild

6. def OAI.ContingencyTables.SmallContextFibres.defectPairContext line 122
7. lemma OAI.ContingencyTables.SmallContextFibres.defectPairContext_injective line 136
8. theorem OAI.ContingencyTables.SmallContextFibres.conditional_defect_mass_le line 149

   Source documentation

   Conditional repair domination for the actual weighted finite sums.

   theorem conditional_defect_mass_le
       (small : I → J → Bool) (B : I → J → ℕ) (r : I → ℕ) (c : J → ℕ)
       (L : ℕ) (s t : I×J) (σ : I×J → ℕ) (l : ℕ)
       (hs : small s.1 s.2=true) (ht : small t.1 t.2=true) (hst : RowMajorBefore s t)
       (hcap : ∀ T : ResidualTables small r c
         (fun i => r i+rowLargeCount small i*L) (fun j => c j+columnLargeCount small j*L),
         ∀ i j, T.val.val i j ≤ B i j) :
       (∑ z : DefectProfiles small B s t σ l,
         hardMarginal small B r c L (naturalProfile z.val)) ≤
         ∑ z : BalancedProfiles small B s σ (l-1+if t.1=s.1 then 1 else 0),
           hardMarginal small B r c L (naturalProfile z.val) := by
   …

   Mentions: OAI.ContingencyTables.RowMajorBefore, OAI.ContingencyTables.ResidualTables, OAI.ContingencyTables.SmallContextFibres.DefectProfiles, OAI.ContingencyTables.SmallContextFibres.naturalProfile, OAI.ContingencyTables.SmallContextFibres.BalancedProfiles

9. theorem OAI.ContingencyTables.SmallContextFibres.paper_residual_capacity line 170

   Source documentation

   The manuscript's actual capacity excludes no residual table.

   theorem paper_residual_capacity (r : I → ℕ) (c : J → ℕ) (d L U : ℕ)
       (hd : Fintype.card I*Fintype.card J ≤ d)
       (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 : I) (j : J) :
       T.val.val i j ≤ paperCapacity (firstPaperSmall r c U) r d L U i j := by
   …

   Mentions: OAI.ContingencyTables.ResidualTables

10. theorem OAI.ContingencyTables.SmallContextFibres.firstPaper_conditional_defect_mass_le line 196

    Source documentation

    The literal first-paper contextual repair bound has no capacity hypothesis: its formal C excludes no full padded completion.

    theorem firstPaper_conditional_defect_mass_le (r : I → ℕ) (c : J → ℕ)
        (s t : I×J) (σ : I×J → ℕ) (l : ℕ)
        (hs : paperSmall r c s.1 s.2=true) (ht : paperSmall r c t.1 t.2=true)
        (hst : RowMajorBefore s t) :
        let d := dimensionAllowance (I := I) (J := J)
    …

    Mentions: OAI.ContingencyTables.RowMajorBefore