Documentation Verification Report

TwoState

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

Statistics

Metric	Count
Definitions `twoState`, `twoState_entropy_eq`, `twoState_helmholtzFreeEnergy_eq`	3
Theorems `instIsFiniteFinOfNatNatTwoState`, `twoState_energy_fst`, `twoState_energy_snd`, `twoState_meanEnergy_eq`, `twoState_partitionFunction_apply`, `twoState_partitionFunction_apply_eq_cosh`, `twoState_probability_fst`, `twoState_probability_snd`	8
Total	11

CanonicalEnsemble

Definitions

Name	Category	Theorems
`twoState` 📖	CompOp	8 math math: `twoState_energy_snd`, `twoState_meanEnergy_eq`, `twoState_energy_fst`, `twoState_partitionFunction_apply_eq_cosh`, `instIsFiniteFinOfNatNatTwoState`, `twoState_probability_snd`, `twoState_probability_fst`, `twoState_partitionFunction_apply`
`twoState_entropy_eq` 📖	CompOp	—
`twoState_helmholtzFreeEnergy_eq` 📖	CompOp	—

Theorems

Name	Kind	Assumes	Proves	Validates	Depends On
`instIsFiniteFinOfNatNatTwoState` 📖	mathematical	—	`IsFinite` `twoState`	—	—
`twoState_energy_fst` 📖	mathematical	—	`energy` `twoState`	—	—
`twoState_energy_snd` 📖	mathematical	—	`energy` `twoState`	—	—
`twoState_meanEnergy_eq` 📖	mathematical	—	`meanEnergy` `twoState` `Temperature.β`	—	`meanEnergy_of_fintype` `instIsFiniteFinOfNatNatTwoState` `twoState_energy_fst` `twoState_probability_fst` `twoState_energy_snd` `twoState_probability_snd`
`twoState_partitionFunction_apply` 📖	mathematical	—	`partitionFunction` `twoState` `Temperature.β`	—	`partitionFunction_of_fintype` `instIsFiniteFinOfNatNatTwoState` `twoState.eq_1`
`twoState_partitionFunction_apply_eq_cosh` 📖	mathematical	—	`partitionFunction` `twoState` `Temperature.β`	—	`twoState_partitionFunction_apply`
`twoState_probability_fst` 📖	mathematical	—	`probability` `twoState` `Temperature.β`	—	`probability.eq_1` `mathematicalPartitionFunction_of_fintype` `instIsFiniteFinOfNatNatTwoState`
`twoState_probability_snd` 📖	mathematical	—	`probability` `twoState` `Temperature.β`	—	`probability.eq_1` `mathematicalPartitionFunction_of_fintype` `instIsFiniteFinOfNatNatTwoState`

---

← Back to Index