OAI/Combinatorics/ContingencyTables/Rooted/RootedRestartWords.lean

GitHub source file

10 declarations, 0 contain sorry, 0 declared as axioms

1. def OAI.ContingencyTables.RootedRestartWords.stageWidth line 21
2. def OAI.ContingencyTables.RootedRestartWords.stageStep line 24
3. def OAI.ContingencyTables.RootedRestartWords.stages line 32
4. theorem OAI.ContingencyTables.RootedRestartWords.stages_law line 42
5. lemma OAI.ContingencyTables.RootedRestartWords.stageStep_law line 52
6. theorem OAI.ContingencyTables.RootedRestartWords.stageLaw_cast line 61
7. def OAI.ContingencyTables.RootedRestartWords.initialStageBits line 75
8. def OAI.ContingencyTables.RootedRestartWords.initializedStages line 79
9. theorem OAI.ContingencyTables.RootedRestartWords.initializedStages_law line 89
10. theorem OAI.ContingencyTables.RootedRestartWords.initializedStages_distance line 124

    Source documentation

    The actual initialized finite word is close to the exact warm restart reference; it includes every fresh stage and initializer word.

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