OAI/Combinatorics/ContingencyTables/Rooted/RootedRestartTrial.lean

GitHub source file

4 declarations, 0 contain sorry, 0 declared as axioms

An actual initialized restart followed by the finite phase update

  1. lemma OAI.ContingencyTables.RootedRestartTrial.replace_distance line 23
  2. abbrev OAI.ContingencyTables.RootedRestartTrial.Words line 28
  3. def OAI.ContingencyTables.RootedRestartTrial.run line 31
  4. theorem OAI.ContingencyTables.RootedRestartTrial.failure line 41

    Source documentation

    All source conditions concern the learned prefix. The words for initialization, successive restarts, observations and weight calls are independent, and all are part of this single finite experiment.

    theorem failure (A : Instance I J) (R : RootedCompletion.Selection A.T)
    (C : ℕ) (hC : 0 < C) (K H L j k n N h : ℕ)
    (hK : 1 ≤ K) (hW : 100*A.d*K ≤ A.W) (hB : (K:ℝ)=binWidth A C)
    (hH : H ≤ rationalHeight A C) (hj : 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