DenseIdealRejection.lean`

2 declarations, 0 contain sorry, 0 declared as axioms

Bounded rejection of independent actual ideal dense trials

theorem OAI.ContingencyTables.GridBoundary.dense_ideal_rejection_variation line 20

Source documentation

The finite first-success law uses the actual per-table trial masses. The sole bias after ideal trials comes from the feasible fallback.

theorem dense_ideal_rejection_variation (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) (J₀ : ℕ) (fallback : Table R P) :
    let g := rationalTableMass R P d hd hR hP e
…

Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.GridBoundary.rationalTableMass

theorem OAI.ContingencyTables.GridBoundary.dense_ideal_rejection_schedule line 66

Source documentation

With the manuscript's actual trial count, the ideal fallback error already consumes at most one quarter of the requested error budget.

theorem dense_ideal_rejection_schedule (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) (h : ℕ) (fallback : Table R P) :
    let g := rationalTableMass R P d hd hR hP e
…

Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.GridBoundary.rationalTableMass