273theorem second_law (sys : RecognitionSystem) (X : Ω → ℝ) 274 (R : JDescentOperator (gibbsPD sys X)) (q₀ : ProbabilityDistribution Ω) : 275 Antitone (fun n : ℕ => 276 kl_divergence (R.evolve n q₀).p (gibbs_measure sys X)) ∧ 277 Antitone (fun n : ℕ => 278 recognition_free_energy sys (R.evolve n q₀).p X) ∧ 279 (∀ n : ℕ, 280 recognition_free_energy sys (gibbs_measure sys X) X ≤ 281 recognition_free_energy sys (R.evolve n q₀).p X) := by
proof body
Term-mode proof.
282 refine ⟨?_, ?_, ?_⟩ 283 · have h := kl_divergence_antitone (R := R) q₀ 284 simpa [gibbsPD_p] using h 285 · exact free_energy_antitone sys X R q₀ 286 · exact free_energy_ge_equilibrium sys X R q₀ 287 288/-! ## §6. The Lyapunov / one-statement form -/ 289 290/-- **THE SECOND LAW — LYAPUNOV (ONE-STATEMENT) FORM.** 291 292 There is a non-negative quantity `H_RS(qₙ) := F_R(qₙ) − F_R(peq)` that is 293 294 * bounded below by `0` (variational principle), 295 * monotone non-increasing along the J-descent evolution (second law). 296 297 `H_RS` is the recognition-science analogue of Boltzmann's `H` function. 298 It collapses to `0` exactly at equilibrium and provides a quantitative 299 convergence rate for the dynamics. -/
used by (1)
From the project-wide theorem graph. These declarations reference this one in their body.