OAI/Combinatorics/ContingencyTables/Counting/CompanionReturnIteration.lean

GitHub source file

3 declarations, 0 contain sorry, 0 declared as axioms

Repeated bounded returns to the literal companion law

Only the exact reference trajectory is required to remain warm. The actual finite-word return kernel can accumulate its error without any additional warmness hypothesis on its output.

  1. theorem OAI.ContingencyTables.CompanionReturnIteration.reference_mixing_distance line 25
  2. theorem OAI.ContingencyTables.CompanionReturnIteration.repeated_return_distance line 50
  3. theorem OAI.ContingencyTables.CompanionReturnIteration.repeated_return_stationary line 82

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