RootedReturnWords.lean`

10 declarations, 0 contain sorry, 0 declared as axioms

A fixed Boolean word for selected-root repeated capped returns

The restart routine iterates the actual defaulted return experiment. Every iteration receives a disjoint block, and an optional initial finite-word draw receives its own disjoint block as well.

theorem OAI.ContingencyTables.RootedReturnWords.walkLaw_cast_power line 27
def OAI.ContingencyTables.RootedReturnWords.booleanReturns line 43
def OAI.ContingencyTables.RootedReturnWords.booleanReturnsLaw line 52
theorem OAI.ContingencyTables.RootedReturnWords.booleanReturnsLaw_eq line 60
theorem OAI.ContingencyTables.RootedReturnWords.booleanReturnsLaw_cast line 76
def OAI.ContingencyTables.RootedReturnWords.initializedReturns line 85
def OAI.ContingencyTables.RootedReturnWords.initializedReturnsLaw line 94
theorem OAI.ContingencyTables.RootedReturnWords.initializedReturnsLaw_eq line 102
theorem OAI.ContingencyTables.RootedReturnWords.initializedReturnsLaw_cast line 118

theorem OAI.ContingencyTables.RootedReturnWords.initializedReturns_distance line 132

Source documentation

The initial word need only be close in total variation to a warm reference law. No pointwise warmness of the actual initial word law is assumed.

theorem initializedReturns_distance (A : Instance I J) (R : RootedCompletion.Selection A.T) (C : ℕ) (hC : 0<C)
    (K H L j k n t r : ℕ) (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