OAI/Combinatorics/ContingencyTables/Transport/TranslatedCompletionAcceptance.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.CompletionTranslation.referencePosition line 14
2. abbrev OAI.ContingencyTables.CompletionTranslation.ReferenceGood line 17
3. lemma OAI.ContingencyTables.CompletionTranslation.reference_good_nonnegative line 21
4. lemma OAI.ContingencyTables.CompletionTranslation.reference_good_card_le line 42
5. lemma OAI.ContingencyTables.CompletionTranslation.reference_cell_fraction line 54
6. lemma OAI.ContingencyTables.CompletionTranslation.reference_good_fraction line 67
7. theorem OAI.ContingencyTables.CompletionTranslation.reference_acceptance line 91

   Source documentation

   The reference row and reference column contain only |I|+|J|+1 possibly changed entries. No completion outside those entries can reject.

   theorem reference_acceptance
       (R : Option I → ℕ) (P : Option J → ℕ) (D : Option I → Option J → ℤ)
       (htotal : (∑ i,R i)=∑ j,P j)
       (hzero : ∀ i j,D (some i) (some j)=0)
       (a₀ d t : ℕ) (hd : 0 < d)
       (hrows : Fintype.card (Option I) ≤ d) (hcols : Fintype.card (Option J) ≤ d)
       (hrow : ∀ i,a₀ ≤ R i) (hcol : ∀ j,a₀ ≤ P j)
       (ha₀ : 4*d ≤ a₀) (ht : 2*t ≤ a₀)
       (hbound : ∀ i j,|D i j| ≤ (t:ℤ)) :
       1-(Fintype.card I+Fintype.card J+1:ℕ)*(4*t*(d:ℝ)^3/a₀) ≤
         (Fintype.card (Accepted R P D):ℝ)/Fintype.card (Table R P) := by
   …

   Mentions: OAI.ContingencyTables.CompletionTranslation.Accepted, OAI.ContingencyTables.Table

8. theorem OAI.ContingencyTables.CompletionTranslation.star_acceptance line 109

   Source documentation

   Applying the previous estimate to the actual signed star only needs bounds on the changes to its row and column margins.

   theorem star_acceptance
       (R : Option I → ℕ) (P : Option J → ℕ)
       (δR : Option I → ℤ) (δP : Option J → ℤ)
       (htotal : (∑ i,R i)=∑ j,P j)
       (a₀ d M t : ℕ) (hd : 0 < d)
       (hrows : Fintype.card (Option I) ≤ d) (hcols : Fintype.card (Option J) ≤ d)
       (hrow : ∀ i,a₀ ≤ R i) (hcol : ∀ j,a₀ ≤ P j)
       (ha₀ : 4*d ≤ a₀) (ht : 2*t ≤ a₀)
       (hR : ∀ i,|δR i| ≤ (M:ℤ)) (hP : ∀ j,|δP j| ≤ (M:ℤ))
       (hscale : M*(Fintype.card J+1) ≤ t) :
       1-(Fintype.card I+Fintype.card J+1:ℕ)*(4*t*(d:ℝ)^3/a₀) ≤
         (Fintype.card (Accepted R P (star δR δP)):ℝ)/Fintype.card (Table R P) := by
   …

   Mentions: OAI.ContingencyTables.CompletionTranslation.Accepted, OAI.ContingencyTables.CompletionTranslation.star, OAI.ContingencyTables.Table