Basic

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

Statistics

Metric	Count
Definitions `CanonicalEnsemble`, `congr`, `differentialEntropy`, `dof`, `empty`, `energy`, `energyVariance`, `helmholtzFreeEnergy`, `instHAddProd`, `mathematicalPartitionFunction`, `meanEnergy`, `meanSquareEnergy`, `microstates`, `nsmul`, `partitionFunction`, `phaseSpaceunit`, `physicalProbability`, `probability`, `thermodynamicEntropy`, `μ`, `μBolt`, `μProd`	22
Theorems `congr_energy_comp_symmm`, `differentialEntropy_nonneg_of_prob_le_one`, `dof_add`, `dof_congr`, `dof_nsmul`, `energy_add_apply`, `energy_congr_apply`, `energy_measurable`, `energy_measurable'`, `energy_nsmul_apply`, `ext`, `ext_iff`, `hPos`, `helmholtzFreeEnergy_add`, `helmholtzFreeEnergy_congr`, `helmholtzFreeEnergy_def`, `helmholtzFreeEnergy_dof_zero`, `helmholtzFreeEnergy_nsmul`, `helmholtzFreeEnergy_phase_space_unit_one`, `instIsFiniteMeasureForallFinμBoltNsmul`, `instIsFiniteMeasureProdμBoltHAdd`, `instIsFiniteMeasureμProd`, `instIsProbabilityMeasureμProdOfIsFiniteMeasureμBoltOfNeZeroMeasureμ`, `instNeZeroMeasureForallFinμNsmul`, `instNeZeroMeasureProdμHAdd`, `instNeZeroMeasureμBoltOfμ`, `instSigmaFiniteμ`, `instSigmaFiniteμBolt`, `instSigmaFiniteμProd`, `integrable_energy_add`, `integrable_energy_congr`, `integrable_energy_nsmul`, `integral_physicalProbability_base`, `integral_probability`, `log_mathematicalPartitionFunction_eq`, `log_partitionFunction`, `log_partitionFunction_ofβ`, `log_physicalProbability`, `mathematicalPartitionFunction_add`, `mathematicalPartitionFunction_comp_ofβ_apply`, `mathematicalPartitionFunction_congr`, `mathematicalPartitionFunction_eq_integral`, `mathematicalPartitionFunction_eq_zero_iff`, `mathematicalPartitionFunction_nonneg`, `mathematicalPartitionFunction_nsmul`, `mathematicalPartitionFunction_pos`, `meanEnergy_add`, `meanEnergy_congr`, `meanEnergy_nsmul`, `nsmul_succ`, `partitionFunction_add`, `partitionFunction_congr`, `partitionFunction_def`, `partitionFunction_dof_zero`, `partitionFunction_nsmul`, `partitionFunction_phase_space_unit_one`, `partitionFunction_pos`, `phase_space_unit_add`, `phase_space_unit_congr`, `phase_space_unit_nsmul`, `physicalProbability_add`, `physicalProbability_congr`, `physicalProbability_def`, `physicalProbability_dof_zero`, `physicalProbability_measurable`, `physicalProbability_nonneg`, `physicalProbability_phase_space_unit_one`, `physicalProbability_pos`, `probability_add`, `probability_congr`, `probability_nonneg`, `probability_nsmul`, `probability_pos`, `thermodynamicEntropy_def`, `μBolt_add`, `μBolt_congr`, `μBolt_ne_zero_of_μ_ne_zero`, `μBolt_nsmul`, `μProd_add`, `μProd_congr`, `μProd_nsmul`, `μ_add`, `μ_neZero_congr`, `μ_nsmul`, `μ_nsmul_zero_eq`, `μ_sigmaFinite`	86
Total	108

CanonicalEnsemble

Definitions

Name	Category	Theorems
`congr` 📖	CompOp	16 math math: `energy_congr_apply`, `μ_neZero_congr`, `mathematicalPartitionFunction_congr`, `phase_space_unit_congr`, `μBolt_congr`, `integrable_energy_congr`, `instIsFiniteCongr`, `congr_energy_comp_symmm`, `partitionFunction_congr`, `dof_congr`, `nsmul_succ`, `helmholtzFreeEnergy_congr`, `probability_congr`, `meanEnergy_congr`, `μProd_congr`, `physicalProbability_congr`
`differentialEntropy` 📖	CompOp	8 math math: `differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp_add_correction`, `shannonEntropy_eq_differentialEntropy`, `differentialEntropy_nonneg_of_prob_le_one`, `differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp`, `thermodynamicEntropy_eq_differentialEntropy_of_dof_zero`, `thermodynamicEntropy_eq_differentialEntropy_of_phase_space_unit_one`, `differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ`, `thermodynamicEntropy_eq_differentialEntropy_sub_correction`
`dof` 📖	CompOp	15 math math: `log_partitionFunction_ofβ`, `physicalProbability_def`, `dof_nsmul`, `IsFinite.dof_eq_zero`, `differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp_add_correction`, `dof_congr`, `dof_add`, `partitionFunction_def`, `log_partitionFunction`, `log_phys_eq_log_math_sub_const_on_Ioi`, `log_physicalProbability`, `ext_iff`, `helmholtzFreeEnergy_eq_helmholtzMathematicalFreeEnergy_add_correction`, `integral_physicalProbability_base`, `thermodynamicEntropy_eq_differentialEntropy_sub_correction`
`empty` 📖	CompOp	—
`energy` 📖	CompOp	26 math math: `energy_congr_apply`, `meanSquareEnergy_of_fintype`, `log_probability`, `energy_add_apply`, `deriv_meanEnergyNumerator`, `deriv_meanEnergyBetaReal`, `mathematicalPartitionFunction_eq_integral`, `twoState_energy_snd`, `integral_energy_bolt`, `energy_measurable`, `meanEnergy_eq_ratio_of_integrals`, `energy_measurable'`, `twoState_energy_fst`, `congr_energy_comp_symmm`, `μBolt_of_fintype`, `mathematicalPartitionFunction_comp_ofβ_apply`, `energy_nsmul_apply`, `log_phys_eq_log_math_sub_const_on_Ioi`, `energyVariance_of_fintype`, `partitionFunction_of_fintype`, `mathematicalPartitionFunction_of_fintype`, `integral_bolt_eq_integral_mul_exp`, `ext_iff`, `log_mathematicalPartitionFunction_eq`, `meanEnergy_of_fintype`, `derivWithin_log_phys_eq_derivWithin_log_math`
`energyVariance` 📖	CompOp	4 math math: `fluctuation_dissipation_theorem_finite`, `energyVariance_eq_meanSquareEnergy_sub_meanEnergy_sq`, `energyVariance_of_fintype`, `derivWithin_meanEnergy_Beta_eq_neg_variance`
`helmholtzFreeEnergy` 📖	CompOp	10 math math: `helmholtzFreeEnergy_add`, `differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp_add_correction`, `differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp`, `helmholtzFreeEnergy_phase_space_unit_one`, `helmholtzFreeEnergy_nsmul`, `helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy`, `helmholtzFreeEnergy_def`, `helmholtzFreeEnergy_dof_zero`, `helmholtzFreeEnergy_congr`, `helmholtzFreeEnergy_eq_helmholtzMathematicalFreeEnergy_add_correction`
`instHAddProd` 📖	CompOp	17 math math: `energy_add_apply`, `phase_space_unit_add`, `helmholtzFreeEnergy_add`, `μ_add`, `integrable_energy_add`, `instIsFiniteProdHAdd`, `instNeZeroMeasureProdμHAdd`, `mathematicalPartitionFunction_add`, `meanEnergy_add`, `μBolt_add`, `probability_add`, `dof_add`, `nsmul_succ`, `physicalProbability_add`, `μProd_add`, `partitionFunction_add`, `instIsFiniteMeasureProdμBoltHAdd`
`mathematicalPartitionFunction` 📖	CompOp	20 math math: `log_partitionFunction_ofβ`, `log_probability`, `mathematicalPartitionFunction_congr`, `mathematicalPartitionFunction_eq_integral`, `partitionFunction_dof_zero`, `helmholtzFreeEnergy_phase_space_unit_one`, `mathematicalPartitionFunction_add`, `mathematicalPartitionFunction_comp_ofβ_apply`, `partitionFunction_def`, `partitionFunction_phase_space_unit_one`, `helmholtzFreeEnergy_dof_zero`, `log_partitionFunction`, `mathematicalPartitionFunction_nsmul`, `mathematicalPartitionFunction_pos`, `mathematicalPartitionFunction_of_fintype`, `mathematicalPartitionFunction_pos_finite`, `mathematicalPartitionFunction_eq_zero_iff`, `differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ`, `log_mathematicalPartitionFunction_eq`, `mathematicalPartitionFunction_nonneg`
`meanEnergy` 📖	CompOp	14 math math: `differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp_add_correction`, `meanEnergy_eq_neg_deriv_log_mathZ_of_beta`, `meanEnergy_eq_neg_deriv_log_Z_of_beta`, `twoState_meanEnergy_eq`, `energyVariance_eq_meanSquareEnergy_sub_meanEnergy_sq`, `differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp`, `meanEnergy_eq_ratio_of_integrals`, `helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy`, `meanEnergy_add`, `energyVariance_of_fintype`, `meanEnergy_congr`, `differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ`, `meanEnergy_nsmul`, `meanEnergy_of_fintype`
`meanSquareEnergy` 📖	CompOp	2 math math: `meanSquareEnergy_of_fintype`, `energyVariance_eq_meanSquareEnergy_sub_meanEnergy_sq`
`microstates` 📖	CompOp	—
`nsmul` 📖	CompOp	17 math math: `dof_nsmul`, `instIsFiniteForallFinNsmul`, `integrable_energy_nsmul`, `probability_nsmul`, `helmholtzFreeEnergy_nsmul`, `partitionFunction_nsmul`, `μ_nsmul_zero_eq`, `μ_nsmul`, `instIsFiniteMeasureForallFinμBoltNsmul`, `nsmul_succ`, `energy_nsmul_apply`, `mathematicalPartitionFunction_nsmul`, `μProd_nsmul`, `μBolt_nsmul`, `instNeZeroMeasureForallFinμNsmul`, `phase_space_unit_nsmul`, `meanEnergy_nsmul`
`partitionFunction` 📖	CompOp	17 math math: `log_partitionFunction_ofβ`, `meanEnergy_eq_neg_deriv_log_Z_of_beta`, `partitionFunction_pos`, `partitionFunction_dof_zero`, `partitionFunction_nsmul`, `twoState_partitionFunction_apply_eq_cosh`, `partitionFunction_congr`, `helmholtzFreeEnergy_def`, `partitionFunction_def`, `partitionFunction_phase_space_unit_one`, `log_partitionFunction`, `log_phys_eq_log_math_sub_const_on_Ioi`, `partitionFunction_of_fintype`, `partitionFunction_add`, `twoState_partitionFunction_apply`, `partitionFunction_pos_finite`, `derivWithin_log_phys_eq_derivWithin_log_math`
`phaseSpaceunit` 📖	CompOp	16 math math: `log_partitionFunction_ofβ`, `physicalProbability_def`, `phase_space_unit_add`, `differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp_add_correction`, `phase_space_unit_congr`, `hPos`, `partitionFunction_def`, `log_partitionFunction`, `log_phys_eq_log_math_sub_const_on_Ioi`, `log_physicalProbability`, `IsFinite.phase_space_unit_eq_one`, `ext_iff`, `helmholtzFreeEnergy_eq_helmholtzMathematicalFreeEnergy_add_correction`, `phase_space_unit_nsmul`, `integral_physicalProbability_base`, `thermodynamicEntropy_eq_differentialEntropy_sub_correction`
`physicalProbability` 📖	CompOp	11 math math: `physicalProbability_measurable`, `physicalProbability_def`, `physicalProbability_dof_zero`, `thermodynamicEntropy_def`, `physicalProbability_nonneg`, `physicalProbability_phase_space_unit_one`, `physicalProbability_pos`, `physicalProbability_add`, `log_physicalProbability`, `physicalProbability_congr`, `integral_physicalProbability_base`
`probability` 📖	CompOp	21 math math: `meanSquareEnergy_of_fintype`, `log_probability`, `physicalProbability_def`, `physicalProbability_dof_zero`, `μProd_of_fintype`, `entropy_of_fintype`, `probability_nsmul`, `physicalProbability_phase_space_unit_one`, `probability_add`, `twoState_probability_snd`, `twoState_probability_fst`, `probability_congr`, `energyVariance_of_fintype`, `sum_probability_eq_one`, `log_physicalProbability`, `probability_nonneg_finite`, `probability_pos`, `probability_nonneg`, `meanEnergy_of_fintype`, `probability_le_one`, `integral_probability`
`thermodynamicEntropy` 📖	CompOp	6 math math: `thermodynamicEntropy_def`, `thermodynamicEntropy_eq_shannonEntropy`, `thermodynamicEntropy_eq_differentialEntropy_of_dof_zero`, `helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy`, `thermodynamicEntropy_eq_differentialEntropy_of_phase_space_unit_one`, `thermodynamicEntropy_eq_differentialEntropy_sub_correction`
`μ` 📖	CompOp	23 math math: `IsFinite.μ_eq_count`, `μ_neZero_congr`, `μ_add`, `mathematicalPartitionFunction_eq_integral`, `μ_sigmaFinite`, `integral_energy_bolt`, `meanEnergy_eq_ratio_of_integrals`, `instNeZeroMeasureProdμHAdd`, `μ_nsmul_zero_eq`, `μ_nsmul`, `mathematicalPartitionFunction_comp_ofβ_apply`, `instNeZeroMeasureμOfIsFiniteOfNonempty`, `instSigmaFiniteμ`, `log_phys_eq_log_math_sub_const_on_Ioi`, `instIsFiniteMeasureμOfIsFinite`, `mathematicalPartitionFunction_eq_zero_iff`, `integral_bolt_eq_integral_mul_exp`, `ext_iff`, `instNeZeroMeasureForallFinμNsmul`, `log_mathematicalPartitionFunction_eq`, `integral_physicalProbability_base`, `derivWithin_log_phys_eq_derivWithin_log_math`, `integral_probability`
`μBolt` 📖	CompOp	11 math math: `instIsFiniteMeasureμBoltOfIsFinite`, `μBolt_congr`, `integral_energy_bolt`, `μBolt_of_fintype`, `instIsFiniteMeasureForallFinμBoltNsmul`, `μBolt_add`, `instNeZeroMeasureμBoltOfμ`, `instSigmaFiniteμBolt`, `integral_bolt_eq_integral_mul_exp`, `instIsFiniteMeasureProdμBoltHAdd`, `μBolt_nsmul`
`μProd` 📖	CompOp	8 math math: `instIsFiniteMeasureμProd`, `instIsProbabilityMeasureμProdOfIsFiniteMeasureμBoltOfNeZeroMeasureμ`, `μProd_of_fintype`, `thermodynamicEntropy_def`, `μProd_add`, `μProd_congr`, `μProd_nsmul`, `instSigmaFiniteμProd`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`congr_energy_comp_symmm` 📖	mathematical	—	`energy` `congr`	—	—
`differentialEntropy_nonneg_of_prob_le_one` 📖	mathematical	`probability` `μProd`	`differentialEntropy`	—	`probability_pos` `instIsFiniteMeasureμProd` `Constants.kB_nonneg`
`dof_add` 📖	mathematical	—	`dof` `CanonicalEnsemble` `instHAddProd`	—	—
`dof_congr` 📖	mathematical	—	`dof` `congr`	—	—
`dof_nsmul` 📖	mathematical	—	`dof` `nsmul`	—	—
`energy_add_apply` 📖	mathematical	—	`energy` `CanonicalEnsemble` `instHAddProd`	—	—
`energy_congr_apply` 📖	mathematical	—	`energy` `congr`	—	—
`energy_measurable` 📖	mathematical	—	`energy`	—	—
`energy_measurable'` 📖	mathematical	—	`energy`	—	`energy_measurable`
`energy_nsmul_apply` 📖	mathematical	—	`energy` `nsmul`	—	—
`ext` 📖	—	`energy` `dof` `phaseSpaceunit` `μ`	—	—	—
`ext_iff` 📖	mathematical	—	`energy` `dof` `phaseSpaceunit` `μ`	—	`ext`
`hPos` 📖	mathematical	—	`phaseSpaceunit`	—	—
`helmholtzFreeEnergy_add` 📖	mathematical	`phaseSpaceunit`	`helmholtzFreeEnergy` `CanonicalEnsemble` `instHAddProd`	—	`partitionFunction_add` `partitionFunction_pos`
`helmholtzFreeEnergy_congr` 📖	mathematical	—	`helmholtzFreeEnergy` `congr`	—	`mathematicalPartitionFunction_congr`
`helmholtzFreeEnergy_def` 📖	mathematical	—	`helmholtzFreeEnergy` `Constants.kB` `Temperature.val` `partitionFunction`	—	—
`helmholtzFreeEnergy_dof_zero` 📖	mathematical	`dof`	`helmholtzFreeEnergy` `Constants.kB` `Temperature.val` `mathematicalPartitionFunction`	—	—
`helmholtzFreeEnergy_nsmul` 📖	mathematical	—	`helmholtzFreeEnergy` `nsmul`	—	`partitionFunction_nsmul`
`helmholtzFreeEnergy_phase_space_unit_one` 📖	mathematical	`phaseSpaceunit`	`helmholtzFreeEnergy` `Constants.kB` `Temperature.val` `mathematicalPartitionFunction`	—	—
`instIsFiniteMeasureForallFinμBoltNsmul` 📖	mathematical	—	`μBolt` `nsmul`	—	`μBolt_nsmul` `instSigmaFiniteμ`
`instIsFiniteMeasureProdμBoltHAdd` 📖	mathematical	—	`μBolt` `CanonicalEnsemble` `instHAddProd`	—	`μBolt_add`
`instIsFiniteMeasureμProd` 📖	mathematical	—	`μProd`	—	`μProd.eq_1`
`instIsProbabilityMeasureμProdOfIsFiniteMeasureμBoltOfNeZeroMeasureμ` 📖	mathematical	—	`μProd`	—	`instNeZeroMeasureμBoltOfμ`
`instNeZeroMeasureForallFinμNsmul` 📖	mathematical	—	`μ` `nsmul`	—	`μ_nsmul_zero_eq` `nsmul_succ` `instSigmaFiniteμ` `μ_neZero_congr` `instNeZeroMeasureProdμHAdd`
`instNeZeroMeasureProdμHAdd` 📖	mathematical	—	`μ` `CanonicalEnsemble` `instHAddProd`	—	`instSigmaFiniteμ`
`instNeZeroMeasureμBoltOfμ` 📖	mathematical	—	`μBolt`	—	`μBolt_ne_zero_of_μ_ne_zero`
`instSigmaFiniteμ` 📖	mathematical	—	`μ`	—	`μ_sigmaFinite`
`instSigmaFiniteμBolt` 📖	mathematical	—	`μBolt`	—	`instSigmaFiniteμ`
`instSigmaFiniteμProd` 📖	mathematical	—	`μProd`	—	—
`integrable_energy_add` 📖	mathematical	`energy` `μProd`	`CanonicalEnsemble` `instHAddProd`	—	`μProd_add` `instIsFiniteMeasureμProd`
`integrable_energy_congr` 📖	mathematical	`energy` `μProd`	`congr`	—	`μProd_congr` `congr_energy_comp_symmm`
`integrable_energy_nsmul` 📖	mathematical	`energy` `μProd`	`nsmul`	—	`hPos` `instIsFiniteMeasureμProd` `nsmul_succ` `instSigmaFiniteμ` `integrable_energy_congr` `integrable_energy_add` `instIsFiniteMeasureForallFinμBoltNsmul`
`integral_physicalProbability_base` 📖	mathematical	—	`μ` `physicalProbability` `phaseSpaceunit` `dof`	—	`integral_probability`
`integral_probability` 📖	mathematical	—	`μ` `probability`	—	`mathematicalPartitionFunction_eq_integral` `mathematicalPartitionFunction_pos`
`log_mathematicalPartitionFunction_eq` 📖	mathematical	—	`mathematicalPartitionFunction` `μ` `Temperature.β` `energy`	—	`mathematicalPartitionFunction_eq_integral`
`log_partitionFunction` 📖	mathematical	—	`partitionFunction` `mathematicalPartitionFunction` `dof` `phaseSpaceunit`	—	`mathematicalPartitionFunction_pos` `hPos`
`log_partitionFunction_ofβ` 📖	mathematical	—	`partitionFunction` `Temperature.ofβ` `mathematicalPartitionFunction` `dof` `phaseSpaceunit`	—	`log_partitionFunction`
`log_physicalProbability` 📖	mathematical	—	`physicalProbability` `probability` `dof` `phaseSpaceunit`	—	`probability_pos` `hPos`
`mathematicalPartitionFunction_add` 📖	mathematical	—	`mathematicalPartitionFunction` `CanonicalEnsemble` `instHAddProd`	—	`μBolt_add` `instSigmaFiniteμBolt`
`mathematicalPartitionFunction_comp_ofβ_apply` 📖	mathematical	—	`mathematicalPartitionFunction` `Temperature.ofβ` `μ` `energy`	—	`Temperature.β_ofβ`
`mathematicalPartitionFunction_congr` 📖	mathematical	—	`mathematicalPartitionFunction` `congr`	—	`mathematicalPartitionFunction_eq_integral`
`mathematicalPartitionFunction_eq_integral` 📖	mathematical	—	`mathematicalPartitionFunction` `μ` `Temperature.β` `energy`	—	`μBolt.eq_1` `energy_measurable'`
`mathematicalPartitionFunction_eq_zero_iff` 📖	mathematical	—	`mathematicalPartitionFunction` `μ`	—	`μBolt.eq_1` `energy_measurable'`
`mathematicalPartitionFunction_nonneg` 📖	mathematical	—	`mathematicalPartitionFunction`	—	`mathematicalPartitionFunction.eq_1`
`mathematicalPartitionFunction_nsmul` 📖	mathematical	—	`mathematicalPartitionFunction` `nsmul`	—	`μBolt_nsmul` `instSigmaFiniteμ` `instSigmaFiniteμBolt`
`mathematicalPartitionFunction_pos` 📖	mathematical	—	`mathematicalPartitionFunction`	—	`instNeZeroMeasureμBoltOfμ`
`meanEnergy_add` 📖	mathematical	`energy` `μProd`	`meanEnergy` `CanonicalEnsemble` `instHAddProd`	—	`meanEnergy.eq_1` `μProd_add` `instSigmaFiniteμProd` `integrable_energy_add` `instIsFiniteMeasureμProd` `instIsProbabilityMeasureμProdOfIsFiniteMeasureμBoltOfNeZeroMeasureμ`
`meanEnergy_congr` 📖	mathematical	—	`meanEnergy` `congr`	—	`μProd_congr`
`meanEnergy_nsmul` 📖	mathematical	`energy` `μProd`	`meanEnergy` `nsmul`	—	`hPos` `nsmul_succ` `instSigmaFiniteμ` `meanEnergy_congr` `meanEnergy_add` `instIsFiniteMeasureForallFinμBoltNsmul` `instNeZeroMeasureForallFinμNsmul` `integrable_energy_nsmul`
`nsmul_succ` 📖	mathematical	—	`nsmul` `congr` `CanonicalEnsemble` `instHAddProd`	—	`ext`
`partitionFunction_add` 📖	mathematical	`phaseSpaceunit`	`partitionFunction` `CanonicalEnsemble` `instHAddProd`	—	`mathematicalPartitionFunction_add`
`partitionFunction_congr` 📖	mathematical	—	`partitionFunction` `congr`	—	`mathematicalPartitionFunction_congr`
`partitionFunction_def` 📖	mathematical	—	`partitionFunction` `mathematicalPartitionFunction` `phaseSpaceunit` `dof`	—	—
`partitionFunction_dof_zero` 📖	mathematical	`dof`	`partitionFunction` `mathematicalPartitionFunction`	—	—
`partitionFunction_nsmul` 📖	mathematical	—	`partitionFunction` `nsmul`	—	`mathematicalPartitionFunction_nsmul`
`partitionFunction_phase_space_unit_one` 📖	mathematical	`phaseSpaceunit`	`partitionFunction` `mathematicalPartitionFunction`	—	—
`partitionFunction_pos` 📖	mathematical	—	`partitionFunction`	—	`mathematicalPartitionFunction_pos` `hPos`
`phase_space_unit_add` 📖	mathematical	—	`phaseSpaceunit` `CanonicalEnsemble` `instHAddProd`	—	—
`phase_space_unit_congr` 📖	mathematical	—	`phaseSpaceunit` `congr`	—	—
`phase_space_unit_nsmul` 📖	mathematical	—	`phaseSpaceunit` `nsmul`	—	—
`physicalProbability_add` 📖	mathematical	`phaseSpaceunit`	`physicalProbability` `CanonicalEnsemble` `instHAddProd`	—	`probability_add`
`physicalProbability_congr` 📖	mathematical	—	`physicalProbability` `congr`	—	`mathematicalPartitionFunction_congr`
`physicalProbability_def` 📖	mathematical	—	`physicalProbability` `probability` `phaseSpaceunit` `dof`	—	—
`physicalProbability_dof_zero` 📖	mathematical	`dof`	`physicalProbability` `probability`	—	—
`physicalProbability_measurable` 📖	mathematical	—	`physicalProbability`	—	`energy_measurable`
`physicalProbability_nonneg` 📖	mathematical	—	`physicalProbability`	—	`probability_nonneg` `hPos`
`physicalProbability_phase_space_unit_one` 📖	mathematical	`phaseSpaceunit`	`physicalProbability` `probability`	—	—
`physicalProbability_pos` 📖	mathematical	—	`physicalProbability`	—	`probability_pos` `hPos`
`probability_add` 📖	mathematical	—	`probability` `CanonicalEnsemble` `instHAddProd`	—	`mathematicalPartitionFunction_add`
`probability_congr` 📖	mathematical	—	`probability` `congr`	—	`mathematicalPartitionFunction_congr`
`probability_nonneg` 📖	mathematical	—	`probability`	—	`mathematicalPartitionFunction_pos`
`probability_nsmul` 📖	mathematical	—	`probability` `nsmul`	—	`mathematicalPartitionFunction_nsmul` `nsmul_succ` `instSigmaFiniteμ` `probability_congr` `probability_add`
`probability_pos` 📖	mathematical	—	`probability`	—	`mathematicalPartitionFunction_pos`
`thermodynamicEntropy_def` 📖	mathematical	—	`thermodynamicEntropy` `Constants.kB` `μProd` `physicalProbability`	—	—
`μBolt_add` 📖	mathematical	—	`μBolt` `CanonicalEnsemble` `instHAddProd`	—	`instSigmaFiniteμ` `energy_measurable'`
`μBolt_congr` 📖	mathematical	—	`μBolt` `congr`	—	`energy_measurable'`
`μBolt_ne_zero_of_μ_ne_zero` 📖	—	—	—	—	`energy_measurable'`
`μBolt_nsmul` 📖	mathematical	—	`μBolt` `nsmul`	—	`hPos` `nsmul_succ` `μBolt_congr` `μBolt_add` `instSigmaFiniteμBolt`
`μProd_add` 📖	mathematical	—	`μProd` `CanonicalEnsemble` `instHAddProd`	—	`μProd.eq_1` `μBolt_add` `instSigmaFiniteμBolt`
`μProd_congr` 📖	mathematical	—	`μProd` `congr`	—	`μBolt_congr`
`μProd_nsmul` 📖	mathematical	—	`μProd` `nsmul`	—	`hPos` `nsmul_succ` `instSigmaFiniteμ` `μProd_congr` `μProd_add` `instIsFiniteMeasureForallFinμBoltNsmul` `instSigmaFiniteμProd`
`μ_add` 📖	mathematical	—	`μ` `CanonicalEnsemble` `instHAddProd`	—	—
`μ_neZero_congr` 📖	mathematical	—	`μ` `congr`	—	—
`μ_nsmul` 📖	mathematical	—	`μ` `nsmul`	—	—
`μ_nsmul_zero_eq` 📖	mathematical	—	`μ` `nsmul`	—	`hPos`
`μ_sigmaFinite` 📖	mathematical	—	`μ`	—	—

(root)

Definitions

Name	Category	Theorems
`CanonicalEnsemble` 📖	CompData	17 math math: `CanonicalEnsemble.energy_add_apply`, `CanonicalEnsemble.phase_space_unit_add`, `CanonicalEnsemble.helmholtzFreeEnergy_add`, `CanonicalEnsemble.μ_add`, `CanonicalEnsemble.integrable_energy_add`, `CanonicalEnsemble.instIsFiniteProdHAdd`, `CanonicalEnsemble.instNeZeroMeasureProdμHAdd`, `CanonicalEnsemble.mathematicalPartitionFunction_add`, `CanonicalEnsemble.meanEnergy_add`, `CanonicalEnsemble.μBolt_add`, `CanonicalEnsemble.probability_add`, `CanonicalEnsemble.dof_add`, `CanonicalEnsemble.nsmul_succ`, `CanonicalEnsemble.physicalProbability_add`, `CanonicalEnsemble.μProd_add`, `CanonicalEnsemble.partitionFunction_add`, `CanonicalEnsemble.instIsFiniteMeasureProdμBoltHAdd`

---

← Back to Index