Documentation Verification Report

Basic

📁 Source: PhysLean/Thermodynamics/Temperature/Basic.lean

Statistics

Metric	Count
Definitions `Temperature`, `betaFromReal`, `instCoeNNReal`, `instCoeReal`, `instTopologicalSpace`, `instZero`, `ofNNReal`, `ofRealNonneg`, `ofβ`, `toReal`, `val`, `β`	12
Theorems `beta_fun_T_eq_on_Ioi`, `beta_fun_T_formula`, `beta_pos`, `chain_rule_T_beta`, `coe_ofNNReal_coe`, `coe_ofNNReal_real`, `deriv_beta_wrt_T`, `eventually_pos_ofβ`, `ext`, `ext_iff`, `ofNNReal_val`, `ofRealNonneg_val`, `ofβ_continuousOn`, `ofβ_differentiableOn`, `ofβ_eq`, `ofβ_β`, `tendsto_ofβ_atTop`, `tendsto_toReal_ofβ_atTop`, `β_ofβ`	19
Total	31

Temperature

Definitions

Name	Category	Theorems
`betaFromReal` 📖	CompOp	4 math math: `chain_rule_T_beta`, `deriv_beta_wrt_T`, `beta_fun_T_eq_on_Ioi`, `beta_fun_T_formula`
`instCoeNNReal` 📖	CompOp	—
`instCoeReal` 📖	CompOp	—
`instTopologicalSpace` 📖	CompOp	1 math math: `ofβ_continuousOn`
`instZero` 📖	CompOp	—
`ofNNReal` 📖	CompOp	2 math math: `ofNNReal_val`, `coe_ofNNReal_coe`
`ofRealNonneg` 📖	CompOp	1 math math: `ofRealNonneg_val`
`ofβ` 📖	CompOp	10 math math: `CanonicalEnsemble.log_partitionFunction_ofβ`, `ofβ_eq`, `β_ofβ`, `CanonicalEnsemble.mathematicalPartitionFunction_comp_ofβ_apply`, `ofβ_differentiableOn`, `eventually_pos_ofβ`, `ofβ_β`, `ofβ_continuousOn`, `tendsto_ofβ_atTop`, `tendsto_toReal_ofβ_atTop`
`toReal` 📖	CompOp	4 math math: `coe_ofNNReal_real`, `eventually_pos_ofβ`, `tendsto_ofβ_atTop`, `tendsto_toReal_ofβ_atTop`
`val` 📖	CompOp	9 math math: `ext_iff`, `CanonicalEnsemble.helmholtzFreeEnergy_phase_space_unit_one`, `ofRealNonneg_val`, `ofβ_differentiableOn`, `CanonicalEnsemble.helmholtzFreeEnergy_def`, `CanonicalEnsemble.helmholtzFreeEnergy_dof_zero`, `ofNNReal_val`, `coe_ofNNReal_coe`, `CanonicalEnsemble.helmholtzFreeEnergy_eq_helmholtzMathematicalFreeEnergy_add_correction`
`β` 📖	CompOp	21 math math: `CanonicalEnsemble.log_probability`, `CanonicalEnsemble.mathematicalPartitionFunction_eq_integral`, `CanonicalEnsemble.integral_energy_bolt`, `CanonicalEnsemble.twoState_meanEnergy_eq`, `CanonicalEnsemble.meanEnergy_eq_ratio_of_integrals`, `β_ofβ`, `CanonicalEnsemble.μBolt_of_fintype`, `CanonicalEnsemble.twoState_partitionFunction_apply_eq_cosh`, `CanonicalEnsemble.twoState_probability_snd`, `beta_pos`, `CanonicalEnsemble.twoState_probability_fst`, `ofβ_β`, `CanonicalEnsemble.kB_mul_beta`, `CanonicalEnsemble.partitionFunction_of_fintype`, `CanonicalEnsemble.mathematicalPartitionFunction_of_fintype`, `CanonicalEnsemble.differentialEntropy_eq_kB_beta_meanEnergy_add_kB_log_mathZ`, `CanonicalEnsemble.twoState_partitionFunction_apply`, `CanonicalEnsemble.integral_bolt_eq_integral_mul_exp`, `CanonicalEnsemble.derivWithin_meanEnergy_Beta_eq_neg_variance`, `CanonicalEnsemble.log_mathematicalPartitionFunction_eq`, `CanonicalEnsemble.derivWithin_log_phys_eq_derivWithin_log_math`

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`beta_fun_T_eq_on_Ioi` 📖	mathematical	—	`betaFromReal` `Constants.kB`	—	`beta_fun_T_formula`
`beta_fun_T_formula` 📖	mathematical	—	`betaFromReal` `Constants.kB`	—	—
`beta_pos` 📖	mathematical	`val`	`β`	—	`Constants.kB_pos`
`chain_rule_T_beta` 📖	mathematical	`val` `β`	`betaFromReal` `Constants.kB`	—	`deriv_beta_wrt_T` `Constants.kB_pos` `beta_fun_T_eq_on_Ioi`
`coe_ofNNReal_coe` 📖	mathematical	—	`val` `ofNNReal`	—	—
`coe_ofNNReal_real` 📖	mathematical	—	`toReal`	—	—
`deriv_beta_wrt_T` 📖	mathematical	`val`	`betaFromReal` `Constants.kB`	—	`beta_fun_T_eq_on_Ioi`
`eventually_pos_ofβ` 📖	mathematical	—	`toReal` `ofβ`	—	`Constants.kB_pos`
`ext` 📖	—	`val`	—	—	—
`ext_iff` 📖	mathematical	—	`val`	—	`ext`
`ofNNReal_val` 📖	mathematical	—	`val` `ofNNReal`	—	—
`ofRealNonneg_val` 📖	mathematical	—	`val` `ofRealNonneg`	—	—
`ofβ_continuousOn` 📖	mathematical	—	`Temperature` `instTopologicalSpace` `ofβ`	—	`Constants.kB_nonneg` `ofβ_eq` `Constants.kB_neq_zero`
`ofβ_differentiableOn` 📖	mathematical	—	`val` `ofβ`	—	`Constants.kB_nonneg` `ofβ_eq`
`ofβ_eq` 📖	mathematical	—	`ofβ` `Constants.kB` `Constants.kB_nonneg`	—	—
`ofβ_β` 📖	mathematical	—	`ofβ` `β`	—	`ext`
`tendsto_ofβ_atTop` 📖	mathematical	—	`toReal` `ofβ`	—	`tendsto_toReal_ofβ_atTop` `eventually_pos_ofβ`
`tendsto_toReal_ofβ_atTop` 📖	mathematical	—	`toReal` `ofβ`	—	`Constants.kB_pos`
`β_ofβ` 📖	mathematical	—	`β` `ofβ`	—	—

(root)

Definitions

Name	Category	Theorems
`Temperature` 📖	CompData	1 math math: `Temperature.ofβ_continuousOn`

---

← Back to Index