OAI/Combinatorics/ContingencyTables/Counting/CompanionTargetMixing.lean

GitHub source file

9 declarations, 0 contain sorry, 0 declared as axioms

Mixing of the literal dyadic trace

The original and degree-completed state chains agree. Their traces therefore agree as well, and the dyadic holding factor costs at most two in the trace Poincare estimate.

  1. theorem OAI.ContingencyTables.CompanionTargetMixing.trace_exit_congr line 23
  2. def OAI.ContingencyTables.CompanionTargetMixing.literalTrace line 35
  3. theorem OAI.ContingencyTables.CompanionTargetMixing.literalTrace_eq_completed line 42
  4. lemma OAI.ContingencyTables.CompanionTargetMixing.literalTrace_poincare line 61
  5. theorem OAI.ContingencyTables.CompanionTargetMixing.targetTrace_poincare line 71
  6. theorem OAI.ContingencyTables.CompanionTargetMixing.target_point_mixing line 90
  7. def OAI.ContingencyTables.CompanionTargetMixing.restartTime line 118
  8. theorem OAI.ContingencyTables.CompanionTargetMixing.restart_schedule line 120
  9. theorem OAI.ContingencyTables.CompanionTargetMixing.restart_warm line 137

    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) (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 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))) :
    ((CompanionTargetTrace.actualTrace A j hp w hw).kernel.power (restartTime A H K)).push nu y≤
      2*law A j y.val.val := by
…

    Mentions: OAI.ContingencyTables.CompanionTargetTrace.actualTrace, OAI.ContingencyTables.CompanionTargetMixing.restartTime