BoltzmannConstant

📁 Source: PhysLean/StatisticalMechanics/BoltzmannConstant.lean

Statistics

Metric	Count
Definitions kB, kBAx	2
Theorems kB_neq_zero, kB_nonneg, kB_pos	3
Total	5

Constants

Definitions

Name	Category	Theorems
kB 📖	CompOp	20 math math: CanonicalEnsemble.fluctuation_dissipation_theorem_finite, Temperature.chain_rule_T_beta, CanonicalEnsemble.heatCapacity_eq_deriv_meanEnergyBeta, Temperature.deriv_beta_wrt_T, CanonicalEnsemble.differentialEntropy_eq_meanEnergy_sub_helmholtz_div_temp_add_correction, kB_nonneg, CanonicalEnsemble.thermodynamicEntropy_def, Temperature.ofβ_eq, CanonicalEnsemble.entropy_of_fintype, Temperature.beta_fun_T_eq_on_Ioi, CanonicalEnsemble.helmholtzFreeEnergy_phase_space_unit_one, CanonicalEnsemble.helmholtzFreeEnergy_def, CanonicalEnsemble.fluctuation_dissipation_energy_parametric, CanonicalEnsemble.helmholtzFreeEnergy_dof_zero, CanonicalEnsemble.kB_mul_beta, Temperature.beta_fun_T_formula, kB_pos, CanonicalEnsemble.differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ, CanonicalEnsemble.helmholtzFreeEnergy_eq_helmholtzMathematicalFreeEnergy_add_correction, CanonicalEnsemble.thermodynamicEntropy_eq_differentialEntropy_sub_correction
kBAx 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
kB_neq_zero 📖	—	—	—	—	kB_pos
kB_nonneg 📖	mathematical	—	kB	—	—
kB_pos 📖	mathematical	—	kB	—	—

---

← Back to Index