pith. machine review for the scientific record. sign in
theorem proved term proof

evolve_equilibrium_eq

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

 163theorem evolve_equilibrium_eq {peq : ProbabilityDistribution Ω}
 164    (R : JDescentOperator peq) (n : ℕ) :
 165    R.evolve n peq = peq := by

proof body

Term-mode proof.

 166  induction n with
 167  | zero => rfl
 168  | succ n ih =>
 169      simp [evolve_succ, ih, R.fixes_equilibrium]
 170
 171end JDescentOperator
 172
 173/-! ## §3. KL is monotone non-increasing along the evolution -/
 174
 175omit [Nonempty Ω] in
 176/-- Single-step KL contraction: `D_KL(qₙ₊₁ ‖ peq) ≤ D_KL(qₙ ‖ peq)`. -/

depends on (11)

Lean names referenced from this declaration's body.