CompanionReturnWords.lean`

11 declarations, 0 contain sorry, 0 declared as axioms

A fixed Boolean word for 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.CompanionReturnWords.walkLaw_cast_power line 24
def OAI.ContingencyTables.CompanionReturnWords.returnBits line 40
def OAI.ContingencyTables.CompanionReturnWords.booleanReturns line 43
def OAI.ContingencyTables.CompanionReturnWords.booleanReturnsLaw line 52
theorem OAI.ContingencyTables.CompanionReturnWords.booleanReturnsLaw_eq line 60
theorem OAI.ContingencyTables.CompanionReturnWords.booleanReturnsLaw_cast line 76
def OAI.ContingencyTables.CompanionReturnWords.initializedReturns line 85
def OAI.ContingencyTables.CompanionReturnWords.initializedReturnsLaw line 94
theorem OAI.ContingencyTables.CompanionReturnWords.initializedReturnsLaw_eq line 102
theorem OAI.ContingencyTables.CompanionReturnWords.initializedReturnsLaw_cast line 118

theorem OAI.ContingencyTables.CompanionReturnWords.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) (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.PublishedInputs.FiniteBoxPrekopaLeindler, OAI.ContingencyTables.PublishedInputs.FiniteCheeger