OAI/Combinatorics/ContingencyTables/Rooted/RootedPhaseExperiment.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.RootedPhaseExperiment.wordWalk_position line 22
2. lemma OAI.ContingencyTables.RootedPhaseExperiment.full_prefix line 38
3. def OAI.ContingencyTables.RootedPhaseExperiment.observedStates line 46
4. theorem OAI.ContingencyTables.RootedPhaseExperiment.observedStates_list line 53
5. lemma OAI.ContingencyTables.RootedPhaseExperiment.accuratePath_iff line 66
6. theorem OAI.ContingencyTables.RootedPhaseExperiment.reference_failure line 80
7. theorem OAI.ContingencyTables.RootedPhaseExperiment.observed_failure line 104

   Source documentation

   The actual recorded finite-word trajectory satisfies the source concentration bound plus the accumulated proved one-step error.

   theorem observed_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≤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