OAI/Combinatorics/ContingencyTables/Rooted/RootedReturnIteration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.RootedReturnIteration.reference_mixing_distance line 21
2. theorem OAI.ContingencyTables.RootedReturnIteration.repeated_return_distance line 46
3. theorem OAI.ContingencyTables.RootedReturnIteration.repeated_return_stationary line 78

   Source documentation

   The terminal law after repeated actual Boolean returns. The first term is the accumulated implementation error; the second is mixing of the exact literal trace.

   theorem repeated_return_stationary (A : Instance I J) (R : RootedCompletion.Selection A.T) (C : ℕ) (hC : 0<C)
       (K H L j k n : ℕ) (hK : 1≤K) (hW : 100*A.d*K≤A.W)
       (hB : (K:ℝ)=binWidth A C) (hj : j≤rationalHeight A C) (hjH : j≤H)
       (hbox : (∏ s : SmallCell A,((A.b s.val.1 s.val.2:ℝ)+1))≤(2:ℝ)^L)
       (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