DenseAcceptance.lean`

1 declarations, 0 contain sorry, 0 declared as axioms

Constant stationary mass of wholly feasible dense bins

theorem OAI.ContingencyTables.GridBoundary.dense_good_bin_probability line 19

Source documentation

Every within-bin offset in these bins is feasible. Their stationary mass is at least 1/32, and hence at least the paper's claimed 1/64.

theorem dense_good_bin_probability (R : Option I → ℕ) (P : Option J → ℕ)
    (d : ℕ) (hd : 14 ≤ d) (hR : ∀ i, d ^ 12 ≤ R i) (hP : ∀ j, d ^ 12 ≤ P j)
    (hRmax : ∀ i, R (some i) ≤ R none) (hPmax : ∀ j, P (some j) ≤ P none)
    (hdimR : Fintype.card (Option I) ≤ d) (hdimP : Fintype.card (Option J) ≤ d)
    (hfree : Fintype.card (I × J) ≤ d) (htotal : ∑ i, R i = ∑ j, P j)
    (e : I × J ≃ Fin q) :
    (1 / 32 : ℝ) ≤
      (∑ a ∈ goodBins R P d e (K := 4 * d ^ 8), denseBinWeight R P d e a) /
…

Mentions: OAI.ContingencyTables.GridBoundary.goodBins, OAI.ContingencyTables.GridBoundary.denseBinWeight