OAI/Combinatorics/ContingencyTables/Dense/DenseTrialAcceptance.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

Acceptance probability of the actual ideal dense trial

  1. def OAI.ContingencyTables.GridBoundary.denseAcceptanceMass line 16
  2. theorem OAI.ContingencyTables.GridBoundary.goodBin_trialAccepted line 21
  3. theorem OAI.ContingencyTables.GridBoundary.denseAcceptanceMass_le_one line 28
  4. theorem OAI.ContingencyTables.GridBoundary.denseAcceptanceMass_lower line 40

    Source documentation

    Wholly feasible bins accept every integral offset, so their proved stationary mass is a lower bound on the actual trial acceptance mass.

    theorem denseAcceptanceMass_lower (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 : ℝ) ≤ denseAcceptanceMass R P d e := by
…

    Mentions: OAI.ContingencyTables.GridBoundary.denseAcceptanceMass