Imports
/-
Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Matteo Cipollina, Joseph Tooby-Smith
-/
module
public import Physlib.StatisticalMechanics.CanonicalEnsemble.Finite
public import Physlib.Meta.Informal.BasicTwo-state canonical ensemble
This module contains the definitions and properties related to the two-state canonical ensemble.
@[expose] public sectioninstance {E₀ E₁} : IsFinite (twoState E₀ E₁) where
μ_eq_count := rfl
dof_eq_zero := rfl
phase_space_unit_eq_one := rflE₀:ℝE₁:ℝT:Temperature⊢ ∑ i,
rexp
(-↑T.β *
{
energy := fun x =>
match x with
| 0 => E₀
| 1 => E₁,
dof := 0, hPos := twoState._proof_1, energy_measurable := ⋯, μ := Measure.count,
μ_sigmaFinite := twoState._proof_3 }.energy
i) =
rexp (-↑T.β * E₀) + rexp (-↑T.β * E₁)
All goals completed! 🐙E₀:ℝE₁:ℝT:Temperature⊢ rexp (-↑T.β * E₀) + rexp (-↑T.β * E₁) =
2 * rexp (-↑T.β * (E₀ + E₁) / 2) * ((rexp (↑T.β * (E₁ - E₀) / 2) + rexp (-(↑T.β * (E₁ - E₀) / 2))) / 2)
E₀:ℝE₁:ℝT:Temperature⊢ rexp (-(↑T.β * E₀)) + rexp (-(↑T.β * E₁)) =
rexp (-(↑T.β * (E₀ + E₁) / 2)) * (rexp (↑T.β * (E₁ - E₀) / 2) + rexp (-(↑T.β * (E₁ - E₀) / 2)))
E₀:ℝE₁:ℝT:Temperature⊢ rexp (-(↑T.β * E₀)) + rexp (-(↑T.β * E₁)) =
rexp (-((↑T.β * E₀ + ↑T.β * E₁) / 2) + ↑T.β * (E₁ - E₀) / 2) +
rexp (-((↑T.β * E₀ + ↑T.β * E₁) / 2) + -(↑T.β * (E₁ - E₀) / 2))
All goals completed! 🐙@[simp]
lemma twoState_energy_fst (E₀ E₁ : ℝ) : (twoState E₀ E₁).energy 0 = E₀ := E₀:ℝE₁:ℝ⊢ (twoState E₀ E₁).energy 0 = E₀
All goals completed! 🐙@[simp]
lemma twoState_energy_snd (E₀ E₁ : ℝ) : (twoState E₀ E₁).energy 1 = E₁ := E₀:ℝE₁:ℝ⊢ (twoState E₀ E₁).energy 1 = E₁
All goals completed! 🐙
Probability of the first state (energy E₀) in closed form.
E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (x - C) / (rexp (x - C) + rexp (-x - C)) = 1 / 2 * (1 + (rexp x - rexp (-x)) / 2 / ((rexp x + rexp (-x)) / 2))
E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp x / rexp C / (rexp x / rexp C + (rexp x)⁻¹ / rexp C) =
1 / 2 * (1 + (rexp x - (rexp x)⁻¹) / 2 / ((rexp x + (rexp x)⁻¹) / 2))
E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp x ^ 2 * 2 = rexp x ^ 2 + 1 + (rexp x ^ 2 - 1)
All goals completed! 🐙
Probability of the second state (energy E₁) in closed form.
E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-x - C) / (rexp (x - C) + rexp (-x - C)) = 1 / 2 * (1 - (rexp x - rexp (-x)) / 2 / ((rexp x + rexp (-x)) / 2))
E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ (rexp x)⁻¹ / rexp C / (rexp x / rexp C + (rexp x)⁻¹ / rexp C) =
1 / 2 * (1 - (rexp x - (rexp x)⁻¹) / 2 / ((rexp x + (rexp x)⁻¹) / 2))
E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ 2 = rexp x ^ 2 + 1 - (rexp x ^ 2 - 1)
All goals completed! 🐙E₀:ℝE₁:ℝT:Temperature⊢ ∑ i, (twoState E₀ E₁).energy i * (twoState E₀ E₁).probability T i =
(E₀ + E₁) / 2 - (E₁ - E₀) / 2 * tanh (↑T.β * (E₁ - E₀) / 2)
E₀:ℝE₁:ℝT:Temperature⊢ E₀ * (2⁻¹ * (1 + tanh (↑T.β * (E₁ - E₀) / 2))) + E₁ * (2⁻¹ * (1 - tanh (↑T.β * (E₁ - E₀) / 2))) =
(E₀ + E₁) / 2 - (E₁ - E₀) / 2 * tanh (↑T.β * (E₁ - E₀) / 2)
All goals completed! 🐙
A simplification of the entropy of the two-state canonical ensemble.
informal_lemma twoState_entropy_eq where
tag := "EVJJI"
deps := [``twoState, ``thermodynamicEntropy]
A simplification of the helmholtzFreeEnergy of the two-state canonical ensemble.