`vfeCert_holds`

proved

show as: view math explainer →

module: IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL
domain: Statistics
line: 216 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL on GitHub at line 216.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

formal source

 213  boltz_minimizes : ∀ {ι : Type*} [Fintype ι] [Nonempty ι] (E : ι → ℝ) (β : ℝ),
 214      0 < β → ∀ q : ProbDist ι, VFE (boltzmannDist E β) E β ≤ VFE q E β
 215
 216theorem vfeCert_holds : VFECert :=
 217{ vfe_at_boltz := @vfe_at_boltzmann_eq_helmholtzF
 218  boltz_minimizes := @boltzmann_minimizes_vfe }
 219
 220end
 221
 222end IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.