def definition def or abbrev

`partitionFunction`

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

formal statement (Lean)

  39def partitionFunction (E : ι → ℝ) (β : ℝ) : ℝ :=

proof body

Definition body.

  40  ∑ i, Real.exp (-β * E i)
  41

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
partitionFunction 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_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 (4)

Lean names referenced from this declaration's body.

E in IndisputableMonolith.Foundation.SpectralEmergence decl_use
partitionFunction in IndisputableMonolith.Thermodynamics.BoltzmannDistribution decl_use
partitionFunction in IndisputableMonolith.Thermodynamics.JCostThermoBridge decl_use
partitionFunction in IndisputableMonolith.Thermodynamics.PartitionFunction decl_use