module module

`IndisputableMonolith.Thermodynamics.PartitionFunction`

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

depends on (2)

Lean names referenced from this declaration's body.

IndisputableMonolith.Constants module_import
IndisputableMonolith.Cost module_import

declarations in this module (21)

def k_B L34
def beta L37
structure DiscreteSystem L42
def partitionFunction L55
theorem partition_function_positive L59
def freeEnergy L75
def averageEnergy L79
def entropy L85
def heatCapacity L89
theorem partition_from_ledger_sum L107
def ledgerProperties L118
def energyFromJCost L133
theorem temperature_controls_fluctuations L140
def twoLevelPartition L153
theorem twoLevel_gt_one L157
theorem twoLevel_at_zero L164
def harmonicOscillatorPartition L177
theorem classical_limit L188
theorem quantum_statistics_from_8tick L203
def implications L216
structure PartitionFunctionFalsifier L229