Lemmas

📁 Source: PhysLean/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean

Statistics

Metric	Count
Definitions `heatCapacity`, `mathematicalHelmholtzFreeEnergy`, `meanEnergyBeta`, `meanEnergy_T`	4
Theorems `derivWithin_log_phys_eq_derivWithin_log_math`, `differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ`, `differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp`, `differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp_add_correction`, `energyVariance_eq_meanSquareEnergy_sub_meanEnergy_sq`, `fluctuation_dissipation_energy_parametric`, `hasDerivWithinAt_log_comp`, `hasDerivWithinAt_log_comp'`, `heatCapacity_eq_deriv_meanEnergyBeta`, `helmholtzFreeEnergy_eq_helmholtzMathematicalFreeEnergy_add_correction`, `helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy`, `integral_bolt_eq_integral_mul_exp`, `integral_energy_bolt`, `kB_mul_beta`, `log_phys_eq_log_math_sub_const_on_Ioi`, `log_probability`, `meanEnergy_eq_neg_deriv_log_Z_of_beta`, `meanEnergy_eq_neg_deriv_log_mathZ_of_beta`, `meanEnergy_eq_ratio_of_integrals`, `thermodynamicEntropy_eq_differentialEntropy_of_dof_zero`, `thermodynamicEntropy_eq_differentialEntropy_of_phase_space_unit_one`, `thermodynamicEntropy_eq_differentialEntropy_sub_correction`	22
Total	26

CanonicalEnsemble

Definitions

Name	Category	Theorems
`heatCapacity` 📖	CompOp	3 math math: `fluctuation_dissipation_theorem_finite`, `heatCapacity_eq_deriv_meanEnergyBeta`, `fluctuation_dissipation_energy_parametric`
`mathematicalHelmholtzFreeEnergy` 📖	CompOp	1 math math: `helmholtzFreeEnergy_eq_helmholtzMathematicalFreeEnergy_add_correction`
`meanEnergyBeta` 📖	CompOp	2 math math: `meanEnergy_Beta_eq_finite`, `derivWithin_meanEnergy_Beta_eq_neg_variance`
`meanEnergy_T` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`derivWithin_log_phys_eq_derivWithin_log_math` 📖	mathematical	`Temperature.val` `μBolt` `Temperature.ofβ`	`partitionFunction` `Temperature.β` `μ` `energy`	—	`log_phys_eq_log_math_sub_const_on_Ioi` `Temperature.beta_pos`
`differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ` 📖	mathematical	`energy` `μProd`	`differentialEntropy` `Constants.kB` `Temperature.β` `meanEnergy` `mathematicalPartitionFunction`	—	`mathematicalPartitionFunction_pos` `probability.eq_1` `instIsFiniteMeasureμProd` `meanEnergy.eq_1` `instIsProbabilityMeasureμProdOfIsFiniteMeasureμBoltOfNeZeroMeasureμ`
`differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp` 📖	mathematical	`Temperature.val` `energy` `μProd` `dof` `phaseSpaceunit`	`differentialEntropy` `meanEnergy` `helmholtzFreeEnergy`	—	`differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp_add_correction`
`differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp_add_correction` 📖	mathematical	`Temperature.val` `energy` `μProd`	`differentialEntropy` `meanEnergy` `helmholtzFreeEnergy` `Constants.kB` `dof` `phaseSpaceunit`	—	`differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ` `hPos` `mathematicalPartitionFunction_pos`
`energyVariance_eq_meanSquareEnergy_sub_meanEnergy_sq` 📖	mathematical	`energy` `μProd`	`energyVariance` `meanSquareEnergy` `meanEnergy`	—	`instIsFiniteMeasureμProd`
`fluctuation_dissipation_energy_parametric` 📖	mathematical	`Temperature.val` `energyVariance` `meanEnergyBeta` `Temperature.β`	`heatCapacity` `Constants.kB`	—	`heatCapacity_eq_deriv_meanEnergyBeta` `Constants.kB_neq_zero`
`hasDerivWithinAt_log_comp` 📖	—	—	—	—	—
`hasDerivWithinAt_log_comp'` 📖	—	—	—	—	`hasDerivWithinAt_log_comp`
`heatCapacity_eq_deriv_meanEnergyBeta` 📖	mathematical	`Temperature.val` `meanEnergyBeta` `Temperature.β`	`heatCapacity` `Constants.kB`	—	`Temperature.ofβ_β` `Temperature.chain_rule_T_beta`
`helmholtzFreeEnergy_eq_helmholtzMathematicalFreeEnergy_add_correction` 📖	mathematical	—	`helmholtzFreeEnergy` `mathematicalHelmholtzFreeEnergy` `Constants.kB` `Temperature.val` `dof` `phaseSpaceunit`	—	`mathematicalPartitionFunction_pos` `hPos`
`helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy` 📖	mathematical	`Temperature.val` `energy` `μProd`	`helmholtzFreeEnergy` `meanEnergy` `thermodynamicEntropy`	—	`differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ` `thermodynamicEntropy_eq_differentialEntropy_sub_correction` `kB_mul_beta` `mathematicalPartitionFunction_pos` `hPos`
`integral_bolt_eq_integral_mul_exp` 📖	mathematical	—	`μBolt` `μ` `Temperature.β` `energy`	—	`energy_measurable'`
`integral_energy_bolt` 📖	mathematical	—	`μBolt` `energy` `μ` `Temperature.β`	—	`integral_bolt_eq_integral_mul_exp`
`kB_mul_beta` 📖	mathematical	`Temperature.val`	`Constants.kB` `Temperature.β`	—	`Constants.kB_neq_zero`
`log_phys_eq_log_math_sub_const_on_Ioi` 📖	mathematical	`μBolt` `Temperature.ofβ`	`partitionFunction` `μ` `energy` `dof` `phaseSpaceunit`	—	`mathematicalPartitionFunction_pos` `hPos` `mathematicalPartitionFunction_eq_integral` `Temperature.β_ofβ` `partitionFunction_def`
`log_probability` 📖	mathematical	—	`probability` `Temperature.β` `energy` `mathematicalPartitionFunction`	—	`mathematicalPartitionFunction_pos`
`meanEnergy_eq_neg_deriv_log_Z_of_beta` 📖	mathematical	`Temperature.val` `μBolt` `Temperature.ofβ` `μ` `energy` `Temperature.β`	`meanEnergy` `partitionFunction`	—	`meanEnergy_eq_neg_deriv_log_mathZ_of_beta` `derivWithin_log_phys_eq_derivWithin_log_math`
`meanEnergy_eq_neg_deriv_log_mathZ_of_beta` 📖	mathematical	`Temperature.val` `μ` `energy` `Temperature.β`	`meanEnergy`	—	`Temperature.beta_pos` `mathematicalPartitionFunction_pos` `mathematicalPartitionFunction_eq_integral` `hasDerivWithinAt_log_comp'` `meanEnergy_eq_ratio_of_integrals`
`meanEnergy_eq_ratio_of_integrals` 📖	mathematical	—	`meanEnergy` `μ` `energy` `Temperature.β`	—	`integral_energy_bolt` `mathematicalPartitionFunction_eq_integral`
`thermodynamicEntropy_eq_differentialEntropy_of_dof_zero` 📖	mathematical	`energy` `μProd` `dof`	`thermodynamicEntropy` `differentialEntropy`	—	`thermodynamicEntropy_eq_differentialEntropy_sub_correction`
`thermodynamicEntropy_eq_differentialEntropy_of_phase_space_unit_one` 📖	mathematical	`energy` `μProd` `phaseSpaceunit`	`thermodynamicEntropy` `differentialEntropy`	—	`thermodynamicEntropy_eq_differentialEntropy_sub_correction`
`thermodynamicEntropy_eq_differentialEntropy_sub_correction` 📖	mathematical	`energy` `μProd`	`thermodynamicEntropy` `differentialEntropy` `Constants.kB` `dof` `phaseSpaceunit`	—	`mathematicalPartitionFunction_pos` `log_physicalProbability` `instIsFiniteMeasureμProd` `instIsProbabilityMeasureμProdOfIsFiniteMeasureμBoltOfNeZeroMeasureμ`

---

← Back to Index