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)
76noncomputable def partitionFunction (sys : System) (beta : ℝ) : ℝ :=
proof body
Definition body.
77 (sys.levels.map (fun l => boltzmannFactor l beta)).sum
78
79/-- Helper: Boltzmann factor is positive. -/
used by (27)
From the project-wide theorem graph. These declarations reference this one in their body.
-
boltzmann_minimizes_vfe
in IndisputableMonolith.Statistics.VariationalFreeEnergyFromRCL
decl_use
-
averageEnergy
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
entropy
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
entropy_nonneg_of_Z_ge_one
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
freeEnergy
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
partition_ge_ground
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
partition_positive
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
probability
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
prob_normalized
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
boltzmannProb
in IndisputableMonolith.Thermodynamics.HelmholtzReal
decl_use
-
boltzmannProb_sum_one
in IndisputableMonolith.Thermodynamics.HelmholtzReal
decl_use
-
F_eq_E_minus_TS
in IndisputableMonolith.Thermodynamics.HelmholtzReal
decl_use
-
helmholtzF
in IndisputableMonolith.Thermodynamics.HelmholtzReal
decl_use
-
helmholtzF_well_defined
in IndisputableMonolith.Thermodynamics.HelmholtzReal
decl_use
-
HelmholtzRealCert
in IndisputableMonolith.Thermodynamics.HelmholtzReal
decl_use
-
partitionFunction
in IndisputableMonolith.Thermodynamics.HelmholtzReal
decl_use
-
partitionFunction_pos
in IndisputableMonolith.Thermodynamics.HelmholtzReal
decl_use
-
freeEnergy
in IndisputableMonolith.Thermodynamics.JCostThermoBridge
decl_use
-
partitionFunction
in IndisputableMonolith.Thermodynamics.JCostThermoBridge
decl_use
-
partition_pos
in IndisputableMonolith.Thermodynamics.JCostThermoBridge
decl_use
-
stateProbability
in IndisputableMonolith.Thermodynamics.JCostThermoBridge
decl_use
-
averageEnergy
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use
-
entropy
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use
-
freeEnergy
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use
-
heatCapacity
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use
-
partitionFunction
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use
-
partition_function_positive
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use
depends on (15)
Lean names referenced from this declaration's body.
-
boltzmannFactor
in IndisputableMonolith.Chemistry.ActivationEnergy
decl_use
-
boltzmannFactor
in IndisputableMonolith.Chemistry.EnzymeCatalysis
decl_use
-
is
in IndisputableMonolith.Foundation.OptionAEmpiricalProgram
decl_use
-
is
in IndisputableMonolith.Foundation.SimplicialLedger.EdgeLengthFromPsi
decl_use
-
is
in IndisputableMonolith.GameTheory.MechanismDesignFromSigma
decl_use
-
boltzmannFactor
in IndisputableMonolith.Information.ShannonEntropy
decl_use
-
is
in IndisputableMonolith.Mathematics.RamanujanBridge.MockThetaPhantom
decl_use
-
map
in IndisputableMonolith.Measurement.RSNative.Core
decl_use
-
beta
in IndisputableMonolith.Relativity.ILG.PPN
decl_use
-
boltzmannFactor
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
System
in IndisputableMonolith.Thermodynamics.BoltzmannDistribution
decl_use
-
partitionFunction
in IndisputableMonolith.Thermodynamics.HelmholtzReal
decl_use
-
partitionFunction
in IndisputableMonolith.Thermodynamics.JCostThermoBridge
decl_use
-
beta
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use
-
partitionFunction
in IndisputableMonolith.Thermodynamics.PartitionFunction
decl_use