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

free_energy_antitone

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)

 245theorem free_energy_antitone (sys : RecognitionSystem) (X : Ω → ℝ)
 246    (R : JDescentOperator (gibbsPD sys X)) (q₀ : ProbabilityDistribution Ω) :
 247    Antitone (fun n : ℕ => recognition_free_energy sys (R.evolve n q₀).p X) := by

proof body

Term-mode proof.

 248  intro n m hnm
 249  exact free_energy_le_of_le sys X R q₀ hnm
 250
 251/-- Free energy along the evolution is bounded below by the equilibrium
 252    value.  The variational principle: Gibbs minimizes `F_R`. -/

used by (3)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (13)

Lean names referenced from this declaration's body.