OAI/Combinatorics/ContingencyTables/Rooted/RootedTargetMixing.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. theorem OAI.ContingencyTables.RootedTargetMixing.trace_exit_congr line 21
2. def OAI.ContingencyTables.RootedTargetMixing.literalTrace line 33
3. theorem OAI.ContingencyTables.RootedTargetMixing.literalTrace_eq_completed line 40
4. lemma OAI.ContingencyTables.RootedTargetMixing.literalTrace_poincare line 59
5. theorem OAI.ContingencyTables.RootedTargetMixing.targetTrace_poincare line 69
6. theorem OAI.ContingencyTables.RootedTargetMixing.target_point_mixing line 88
7. theorem OAI.ContingencyTables.RootedTargetMixing.restart_warm line 118

   Source documentation

   The exact dyadic trace reaches the required two-warm law at the explicit doubled schedule, including subprobability incoming laws.

   theorem restart_warm (A : Instance I J) (R : RootedCompletion.Selection A.T) (H K j : ℕ) (hj : j≤H)
       (hB : (∏ s : SmallCell A,((A.b s.val.1 s.val.2:ℝ)+1))≤(2:ℝ)^K)
       (hp : 0<Fintype.card (Labels A)) (w : Pair A → Pair A → ℚ) (hw : ∀ p q,0<w p q)
       (hgood : GoodMultipliers pairs (weight A R j) (fun p q => (w p q:ℝ)))
       (nu : PlainIndex (pairs : List (Pair A)) → ℝ) (hnu : ∀ S,0≤nu S)
       (hmass : ∑ S,nu S≤1) (y : PlainIndex (pairs : List (Pair A))) :
       ((RootedTargetTrace.actualTrace A R j hp w hw).kernel.power (restartTime A H K)).push nu y≤
         2*law A R j y.val.val := by
   …

   Mentions: OAI.ContingencyTables.RootedCompletion.Selection, OAI.ContingencyTables.RootedTargetTrace.actualTrace