OAI/Combinatorics/ContingencyTables/Sampling/FirstPaperIdealRejection.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

The actual stationary outer rejection law and its polynomial trial budget

  1. abbrev OAI.ContingencyTables.SmallGraphProfiles.stateTrial line 21

    Source documentation

    Read balance and padding, then return the unique unpadded table.

    abbrev stateTrial : PaperStateJoint r c → Option (Table r c) :=
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStateJoint, OAI.ContingencyTables.Table

  2. theorem OAI.ContingencyTables.SmallGraphProfiles.stationary_trial_mass line 24
  3. theorem OAI.ContingencyTables.SmallGraphProfiles.ideal_outer_variation line 34

    Source documentation

    No approximate draw is conditioned on success. Ideal complete trials have fallback error exactly bounded by their geometric failure tail.

    theorem ideal_outer_variation [Nonempty (PaperStates r c)] [Nonempty (Table r c)]
    (i₀ : LargeRows r ((dimensionAllowance (I := I) (J := J))^20))
…

    Mentions: OAI.ContingencyTables.SmallGraphProfiles.PaperStates, OAI.ContingencyTables.Table, OAI.ContingencyTables.SmallGraphProfiles.LargeRows