OAI/Combinatorics/ContingencyTables/Rooted/RootedTraceWords.lean

GitHub source file

8 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.RootedTraceWords.sourceKilled line 21
2. def OAI.ContingencyTables.RootedTraceWords.targetKilled line 28
3. lemma OAI.ContingencyTables.RootedTraceWords.targetKilled_matches line 34
4. def OAI.ContingencyTables.RootedTraceWords.returnWord line 43

   Source documentation

   The search consumes a fixed cap worth of disjoint words even when the first return occurs before the last word.

   def returnWord (A : Instance I J) (R : RootedCompletion.Selection A.T) (C K j k N : ℕ)
       (hK : 1≤K) (hW : 100*A.d*K≤A.W) (xi : ℚ)
       (v : Grid (I := Fin (dimension A)) K) (w : Pair A → Pair A → ℚ) (S : State A)
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection

5. lemma OAI.ContingencyTables.RootedTraceWords.arithmetic_event_eq line 51
6. theorem OAI.ContingencyTables.RootedTraceWords.arithmetic_recorded_event_bound line 71
7. theorem OAI.ContingencyTables.RootedTraceWords.returnWord_event line 89

   Source documentation

   The concrete bounded return experiment has the capped trace event bound plus one implementation error per used step.

   theorem returnWord_event (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

8. theorem OAI.ContingencyTables.RootedTraceWords.returnWord_failure line 113

   Source documentation

   Capping the concrete word experiment adds the exact reference nonreturn probability and the accumulated step-implementation error.

   theorem returnWord_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