structure
definition
VFECert
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL on GitHub at line 210.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
used by
formal source
207
208/-! ## Master cert -/
209
210structure VFECert where
211 vfe_at_boltz : ∀ {ι : Type*} [Fintype ι] [Nonempty ι] (E : ι → ℝ) (β : ℝ),
212 0 < β → VFE (boltzmannDist E β) E β = helmholtzF E β
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