OAI/Combinatorics/ContingencyTables/Rooted/RootedPhaseTrial.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

A complete finite-word selected-root phase trial

The trajectory and its weight queries use disjoint words. The output is the actual guarded rational multiplier and count update.

  1. lemma OAI.ContingencyTables.RootedPhaseTrial.paired_average_bound line 23
  2. abbrev OAI.ContingencyTables.RootedPhaseTrial.TrialWords line 40
  3. def OAI.ContingencyTables.RootedPhaseTrial.trial line 44
  4. def OAI.ContingencyTables.RootedPhaseTrial.ValidOutput line 51
  5. theorem OAI.ContingencyTables.RootedPhaseTrial.trial_success line 59
  6. theorem OAI.ContingencyTables.RootedPhaseTrial.calls_failure_indicator line 74
  7. theorem OAI.ContingencyTables.RootedPhaseTrial.trial_failure line 97

    Source documentation

    Actual guarded output failure is bounded by trajectory concentration, the proved weight-call error, and the distance of its incoming law from the exact warm reference.

    theorem trial_failure (A : Instance I J) (R : RootedCompletion.Selection A.T)
    (C : ℕ) (hC : 0 < C) (K j k N : ℕ)
    (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C)
    (hj : j+1 ≤ rationalHeight A C) (xi : ℚ) (hx0 : 0 < xi) (hx1 : xi ≤ 1/4)
    (hPL : PublishedInputs.FiniteBoxPrekopaLeindler (dimension A))
    (hCheeger : PublishedInputs.FiniteCheeger (Grid (I := Fin (dimension A)) K))
…

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger