OAI/Combinatorics/ContingencyTables/Rooted/RootedWarmStart.lean

GitHub source file

17 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.ContingencyTables.RootedWarmStart.zero_weight_eq line 19

   Source documentation

   The initial factorial weight is independent of the selected root.

   lemma zero_weight_eq (A : Instance I J) (R : RootedCompletion.Selection A.T) :
       weight A R 0=CompanionAnnealing.weight A 0 := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.CompanionAnnealing.weight

2. lemma OAI.ContingencyTables.RootedWarmStart.total_zero line 28
3. def OAI.ContingencyTables.RootedWarmStart.total line 35
4. lemma OAI.ContingencyTables.RootedWarmStart.total_positive line 37
5. def OAI.ContingencyTables.RootedWarmStart.law line 40
6. lemma OAI.ContingencyTables.RootedWarmStart.free_positive line 43
7. theorem OAI.ContingencyTables.RootedWarmStart.law_adjacent line 50

   Source documentation

   The exact phase-j transversal law is two-warm for phase j+1. The statement applies in particular to every actual paired transversal.

   theorem law_adjacent (A : Instance I J) (R : RootedCompletion.Selection A.T) (j : ℕ) (S : Set (Labels A×Bool)) :
       law A R j S≤2*law A R (j+1) S := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedWarmStart.law

8. theorem OAI.ContingencyTables.RootedWarmStart.weight_bounds_zero line 64
9. theorem OAI.ContingencyTables.RootedWarmStart.total_bounds_zero line 75
10. lemma OAI.ContingencyTables.RootedWarmStart.zero_weight_lower line 83
11. theorem OAI.ContingencyTables.RootedWarmStart.law_lower line 91

    Source documentation

    An explicit positive minimum mass for the actual transversal law. Its binary size depends on j and the bounded small-cell capacities.

    theorem law_lower (A : Instance I J) (R : RootedCompletion.Selection A.T) (j : ℕ) (S : Set (Labels A×Bool)) :
        (1/2:ℝ)^j/(CompanionFactorialApplication.denominator A*
          ∏ s : SmallCell A,((A.b s.val.1 s.val.2:ℝ)+1))≤ law A R j S := by
    …

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.CompanionFactorialApplication.denominator, OAI.ContingencyTables.RootedWarmStart.law

12. lemma OAI.ContingencyTables.RootedWarmStart.law_zero_eq line 119

    Source documentation

    The existing executed initializer is exactly the selected-root phase-zero law.

    lemma law_zero_eq (A : Instance I J) (R : RootedCompletion.Selection A.T)
        (S : Set (Labels A×Bool)) :
        law A R 0 S=CompanionWarmStart.law A 0 S := by
    …

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedWarmStart.law, OAI.ContingencyTables.CompanionWarmStart.law

13. lemma OAI.ContingencyTables.RootedWarmStart.ideal_initial_mass line 125
14. theorem OAI.ContingencyTables.RootedWarmStart.initial_distance line 131
15. lemma OAI.ContingencyTables.RootedWarmStart.actual_degree line 141
16. lemma OAI.ContingencyTables.RootedWarmStart.initial_weight_lower line 150
17. theorem OAI.ContingencyTables.RootedWarmStart.plain_law_lower line 157

    Source documentation

    The sharp source minimum mass uses only the original bounded-cell label count.

    theorem plain_law_lower (A : Instance I J) (R : RootedCompletion.Selection A.T) (K j : ℕ)
        (hB : (∏ s : SmallCell A,((A.b s.val.1 s.val.2:ℝ)+1))≤(2:ℝ)^K)
        (S : Set (Labels A×Bool)) (hS : PlainState pairs S) :
        (1/2:ℝ)^(j+Fintype.card (Labels A)+K)≤ law A R j S := by
    …

    Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedWarmStart.law