SmallCompletionAcceptance.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Half acceptance at the paper's actual padding scale

lemma OAI.ContingencyTables.CompletionTranslation.padding_ge_twenty_dimension line 15

theorem OAI.ContingencyTables.CompletionTranslation.reference_acceptance_half line 23

Source documentation

Only the literal reference row and column are union bounded.

theorem reference_acceptance_half
    (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)
    (d : ℕ) (hd : 14 ≤ d)
    (hrows : Fintype.card (Option I) ≤ d) (hcols : Fintype.card (Option J) ≤ d)
    (hcross : Fintype.card I+Fintype.card J+1 ≤ d)
    (hrow : ∀ i,d^12 ≤ R i) (hcol : ∀ j,d^12 ≤ P j)
    (hbound : ∀ i j,|D i j| ≤ (10*d:ℕ)) :
    (Fintype.card (Table R P):ℝ)/2 ≤ Fintype.card (Accepted R P D) := by
…

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