DenseTrialWeights.lean`

8 declarations, 0 contain sorry, 0 declared as axioms

Equal weight of all accepted dense trials

The bin is sampled with its stationary weight, and the integral offset uniformly. The unique trial producing any given table lies in a bin of weight one. Conditioning this finite law on acceptance is therefore exactly uniform on the actual tables.

def OAI.ContingencyTables.GridBoundary.trialReal line 22
theorem OAI.ContingencyTables.GridBoundary.trialReal_closed line 27
theorem OAI.ContingencyTables.GridBoundary.trialReal_feasible_iff line 52
theorem OAI.ContingencyTables.GridBoundary.acceptedTrial_binWeight_one line 66
def OAI.ContingencyTables.GridBoundary.denseTrialMass line 76
theorem OAI.ContingencyTables.GridBoundary.denseTrialMass_pos line 82
theorem OAI.ContingencyTables.GridBoundary.denseTrialMass_sum line 95

theorem OAI.ContingencyTables.GridBoundary.denseTrial_conditional_uniform line 114

Source documentation

Conditioning the actual stationary-bin/uniform-offset trial law on acceptance assigns each table exactly the reciprocal of the table count.

theorem denseTrial_conditional_uniform (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)
    (hfree : Fintype.card (I × J) ≤ d) (e : I × J ≃ Fin q) (X : Table R P) :
    denseTrialMass R P d e (tableTrial R P d hd hR hP e X) /
      (∑ Y : Table R P, denseTrialMass R P d e (tableTrial R P d hd hR hP e Y)) =
        1 / Fintype.card (Table R P) := by
…

Mentions: OAI.ContingencyTables.Table, OAI.ContingencyTables.GridBoundary.denseTrialMass, OAI.ContingencyTables.GridBoundary.tableTrial