pith. machine review for the scientific record. sign in
def definition def or abbrev

secondLawCert

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)

 406noncomputable def secondLawCert (sys : RecognitionSystem) (X : Ω → ℝ) :
 407    SecondLawCert sys X where
 408  gibbs_inequality q :=

proof body

Definition body.

 409    kl_divergence_nonneg q.p (gibbs_measure sys X) q.nonneg
 410      (fun ω => gibbs_measure_pos sys X ω)
 411      q.sum_one
 412      (gibbs_measure_sum_one sys X)
 413  gibbs_minimizes q := gibbs_minimizes_free_energy_basic sys X q
 414  fe_kl_identity q := free_energy_kl_identity sys X q
 415  kl_monotone R q₀ := by
 416    have h := kl_divergence_antitone (R := R) q₀
 417    simpa [gibbsPD_p] using h
 418  free_energy_monotone R q₀ := free_energy_antitone sys X R q₀
 419  entropy_monotone_under_conservation R q₀ h_conserve :=
 420    second_law_entropy_form sys X R q₀ h_conserve
 421

used by (1)

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

depends on (12)

Lean names referenced from this declaration's body.