Finite

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

Statistics

Metric	Count
Definitions `IsFinite`, `mathematicalPartitionFunctionBetaReal`, `meanEnergyBetaReal`, `meanEnergyNumerator`, `probabilityBetaReal`, `shannonEntropy`	6
Theorems `dof_eq_zero`, `phase_space_unit_eq_one`, `μ_eq_count`, `derivWithin_meanEnergy_Beta_eq_neg_variance`, `deriv_mathematicalPartitionFunctionBetaReal`, `deriv_meanEnergyBetaReal`, `deriv_meanEnergyNumerator`, `differentiable_mathematicalPartitionFunctionBetaReal`, `differentiable_meanEnergyBetaReal`, `differentiable_meanEnergyNumerator`, `energyVariance_of_fintype`, `entropy_nonneg`, `entropy_of_fintype`, `fluctuation_dissipation_theorem_finite`, `instIsFiniteCongr`, `instIsFiniteForallFinNsmul`, `instIsFiniteMeasureμBoltOfIsFinite`, `instIsFiniteMeasureμOfIsFinite`, `instIsFiniteProdHAdd`, `instNeZeroMeasureμOfIsFiniteOfNonempty`, `mathematicalPartitionFunctionBetaReal_pos`, `mathematicalPartitionFunction_of_fintype`, `mathematicalPartitionFunction_pos_finite`, `meanEnergy_Beta_eq_finite`, `meanEnergy_of_fintype`, `meanSquareEnergy_of_fintype`, `partitionFunction_of_fintype`, `partitionFunction_pos_finite`, `probability_le_one`, `probability_nonneg_finite`, `shannonEntropy_eq_differentialEntropy`, `sum_probability_eq_one`, `thermodynamicEntropy_eq_shannonEntropy`, `μBolt_of_fintype`, `μProd_of_fintype`	35
Total	41

CanonicalEnsemble

Definitions

Name	Category	Theorems
`IsFinite` 📖	CompData	4 math math: `instIsFiniteProdHAdd`, `instIsFiniteForallFinNsmul`, `instIsFiniteCongr`, `instIsFiniteFinOfNatNatTwoState`
`mathematicalPartitionFunctionBetaReal` 📖	CompOp	3 math math: `differentiable_mathematicalPartitionFunctionBetaReal`, `deriv_mathematicalPartitionFunctionBetaReal`, `mathematicalPartitionFunctionBetaReal_pos`
`meanEnergyBetaReal` 📖	CompOp	3 math math: `deriv_meanEnergyBetaReal`, `meanEnergy_Beta_eq_finite`, `differentiable_meanEnergyBetaReal`
`meanEnergyNumerator` 📖	CompOp	3 math math: `deriv_meanEnergyNumerator`, `differentiable_meanEnergyNumerator`, `deriv_mathematicalPartitionFunctionBetaReal`
`probabilityBetaReal` 📖	CompOp	1 math math: `deriv_meanEnergyBetaReal`
`shannonEntropy` 📖	CompOp	4 math math: `shannonEntropy_eq_differentialEntropy`, `entropy_of_fintype`, `entropy_nonneg`, `thermodynamicEntropy_eq_shannonEntropy`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`derivWithin_meanEnergy_Beta_eq_neg_variance` 📖	mathematical	`Temperature.val`	`meanEnergyBeta` `Temperature.β` `energyVariance`	—	`Temperature.beta_pos` `meanEnergy_Beta_eq_finite` `differentiable_meanEnergyBetaReal` `deriv_meanEnergyBetaReal` `Temperature.ofβ_β` `mathematicalPartitionFunction_of_fintype` `energyVariance_of_fintype`
`deriv_mathematicalPartitionFunctionBetaReal` 📖	mathematical	—	`mathematicalPartitionFunctionBetaReal` `meanEnergyNumerator`	—	—
`deriv_meanEnergyBetaReal` 📖	mathematical	—	`meanEnergyBetaReal` `energy` `probabilityBetaReal`	—	`differentiable_mathematicalPartitionFunctionBetaReal` `differentiable_meanEnergyNumerator` `mathematicalPartitionFunctionBetaReal_pos` `deriv_meanEnergyNumerator` `deriv_mathematicalPartitionFunctionBetaReal`
`deriv_meanEnergyNumerator` 📖	mathematical	—	`meanEnergyNumerator` `energy`	—	—
`differentiable_mathematicalPartitionFunctionBetaReal` 📖	mathematical	—	`mathematicalPartitionFunctionBetaReal`	—	—
`differentiable_meanEnergyBetaReal` 📖	mathematical	—	`meanEnergyBetaReal`	—	`mathematicalPartitionFunctionBetaReal_pos`
`differentiable_meanEnergyNumerator` 📖	mathematical	—	`meanEnergyNumerator`	—	—
`energyVariance_of_fintype` 📖	mathematical	—	`energyVariance` `energy` `probability` `meanEnergy`	—	`instIsFiniteMeasureμProd` `energyVariance_eq_meanSquareEnergy_sub_meanEnergy_sq` `instIsProbabilityMeasureμProdOfIsFiniteMeasureμBoltOfNeZeroMeasureμ` `instIsFiniteMeasureμBoltOfIsFinite` `instNeZeroMeasureμOfIsFiniteOfNonempty` `meanSquareEnergy_of_fintype`
`entropy_nonneg` 📖	mathematical	—	`shannonEntropy`	—	`probability_le_one` `mathematicalPartitionFunction_pos_finite` `Constants.kB_pos`
`entropy_of_fintype` 📖	mathematical	—	`shannonEntropy` `Constants.kB` `probability`	—	—
`fluctuation_dissipation_theorem_finite` 📖	mathematical	`Temperature.val`	`heatCapacity` `energyVariance` `Constants.kB`	—	`Temperature.beta_pos` `meanEnergy_Beta_eq_finite` `differentiable_meanEnergyBetaReal` `derivWithin_meanEnergy_Beta_eq_neg_variance` `fluctuation_dissipation_energy_parametric`
`instIsFiniteCongr` 📖	mathematical	—	`IsFinite` `congr`	—	`IsFinite.μ_eq_count` `IsFinite.dof_eq_zero` `IsFinite.phase_space_unit_eq_one`
`instIsFiniteForallFinNsmul` 📖	mathematical	—	`IsFinite` `nsmul`	—	`hPos` `IsFinite.μ_eq_count` `instIsFiniteCongr` `instIsFiniteProdHAdd` `IsFinite.dof_eq_zero` `IsFinite.phase_space_unit_eq_one` `nsmul_succ` `instSigmaFiniteμ`
`instIsFiniteMeasureμBoltOfIsFinite` 📖	mathematical	—	`μBolt`	—	`μBolt.eq_1` `instIsFiniteMeasureμOfIsFinite`
`instIsFiniteMeasureμOfIsFinite` 📖	mathematical	—	`μ`	—	`IsFinite.μ_eq_count`
`instIsFiniteProdHAdd` 📖	mathematical	—	`IsFinite` `CanonicalEnsemble` `instHAddProd`	—	`μ_add` `IsFinite.μ_eq_count` `IsFinite.dof_eq_zero` `IsFinite.phase_space_unit_eq_one`
`instNeZeroMeasureμOfIsFiniteOfNonempty` 📖	mathematical	—	`μ`	—	`IsFinite.μ_eq_count`
`mathematicalPartitionFunctionBetaReal_pos` 📖	mathematical	—	`mathematicalPartitionFunctionBetaReal`	—	—
`mathematicalPartitionFunction_of_fintype` 📖	mathematical	—	`mathematicalPartitionFunction` `Temperature.β` `energy`	—	`mathematicalPartitionFunction_eq_integral` `IsFinite.μ_eq_count`
`mathematicalPartitionFunction_pos_finite` 📖	mathematical	—	`mathematicalPartitionFunction`	—	`mathematicalPartitionFunction_pos` `instIsFiniteMeasureμBoltOfIsFinite` `instNeZeroMeasureμOfIsFiniteOfNonempty`
`meanEnergy_Beta_eq_finite` 📖	mathematical	—	`meanEnergyBeta` `meanEnergyBetaReal`	—	`Temperature.β_ofβ` `meanEnergyBeta.eq_1` `meanEnergy_of_fintype` `meanEnergyBetaReal.eq_1` `mathematicalPartitionFunction_of_fintype`
`meanEnergy_of_fintype` 📖	mathematical	—	`meanEnergy` `energy` `probability`	—	`instIsFiniteMeasureμProd` `μProd_of_fintype`
`meanSquareEnergy_of_fintype` 📖	mathematical	—	`meanSquareEnergy` `energy` `probability`	—	`instIsFiniteMeasureμProd` `μProd_of_fintype`
`partitionFunction_of_fintype` 📖	mathematical	—	`partitionFunction` `Temperature.β` `energy`	—	`mathematicalPartitionFunction_of_fintype` `IsFinite.phase_space_unit_eq_one` `IsFinite.dof_eq_zero`
`partitionFunction_pos_finite` 📖	mathematical	—	`partitionFunction`	—	`IsFinite.phase_space_unit_eq_one` `IsFinite.dof_eq_zero` `mathematicalPartitionFunction_pos_finite`
`probability_le_one` 📖	mathematical	—	`probability`	—	`mathematicalPartitionFunction_of_fintype`
`probability_nonneg_finite` 📖	mathematical	—	`probability`	—	`mathematicalPartitionFunction_pos_finite`
`shannonEntropy_eq_differentialEntropy` 📖	mathematical	—	`shannonEntropy` `differentialEntropy`	—	`instIsFiniteMeasureμProd` `μProd_of_fintype`
`sum_probability_eq_one` 📖	mathematical	—	`probability`	—	`mathematicalPartitionFunction_of_fintype` `mathematicalPartitionFunction_pos_finite`
`thermodynamicEntropy_eq_shannonEntropy` 📖	mathematical	—	`thermodynamicEntropy` `shannonEntropy`	—	`IsFinite.phase_space_unit_eq_one` `IsFinite.dof_eq_zero` `shannonEntropy_eq_differentialEntropy`
`μBolt_of_fintype` 📖	mathematical	—	`μBolt` `Temperature.β` `energy`	—	`μBolt.eq_1` `IsFinite.μ_eq_count`
`μProd_of_fintype` 📖	mathematical	—	`μProd` `probability`	—	`μProd.eq_1` `μBolt_of_fintype`

CanonicalEnsemble.IsFinite

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`dof_eq_zero` 📖	mathematical	—	`CanonicalEnsemble.dof`	—	—
`phase_space_unit_eq_one` 📖	mathematical	—	`CanonicalEnsemble.phaseSpaceunit`	—	—
`μ_eq_count` 📖	mathematical	—	`CanonicalEnsemble.μ`	—	—

---

← Back to Index