PhysLean Documentation

PhysLean.StatisticalMechanics.CanonicalEnsemble.TwoState

Two-state canonical ensemble #

This module contains the definitions and properties related to the two-state canonical ensemble.

source
noncomputable def CanonicalEnsemble.twoState (E₀ E₁ : ℝ) :
CanonicalEnsemble (Fin 2)

The canonical ensemble corresponding to state system, with one state of energy E₀ and the other state of energy E₁.

Equations
  • One or more equations did not get rendered due to their size.
Instances For
    source
    instance CanonicalEnsemble.instIsFiniteFinOfNatNatTwoState {E₀ E₁ : ℝ} :
    (twoState E₀ E₁).IsFinite
    source
    theorem CanonicalEnsemble.twoState_partitionFunction_apply (E₀ E₁ : ℝ) (T : Temperature) :
    (twoState E₀ E₁).partitionFunction T = Real.exp (-↑T.β * E₀) + Real.exp (-↑T.β * E₁)
    source
    theorem CanonicalEnsemble.twoState_partitionFunction_apply_eq_cosh (E₀ E₁ : ℝ) (T : Temperature) :
    (twoState E₀ E₁).partitionFunction T = 2 * Real.exp (-↑T.β * (E₀ + E₁) / 2) * Real.cosh (↑T.β * (E₁ - E₀) / 2)
    source
    @[simp]
    theorem CanonicalEnsemble.twoState_energy_fst (E₀ E₁ : ℝ) :
    (twoState E₀ E₁).energy 0 = E₀
    source
    @[simp]
    theorem CanonicalEnsemble.twoState_energy_snd (E₀ E₁ : ℝ) :
    (twoState E₀ E₁).energy 1 = E₁
    source
    theorem CanonicalEnsemble.twoState_probability_fst (E₀ E₁ : ℝ) (T : Temperature) :
    (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + Real.tanh (↑T.β * (E₁ - E₀) / 2))

    Probability of the first state (energy E₀) in closed form.

    source
    theorem CanonicalEnsemble.twoState_probability_snd (E₀ E₁ : ℝ) (T : Temperature) :
    (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - Real.tanh (↑T.β * (E₁ - E₀) / 2))

    Probability of the second state (energy E₁) in closed form.

    source
    theorem CanonicalEnsemble.twoState_meanEnergy_eq (E₀ E₁ : ℝ) (T : Temperature) :
    (twoState E₀ E₁).meanEnergy T = (E₀ + E₁) / 2 - (E₁ - E₀) / 2 * Real.tanh (↑T.β * (E₁ - E₀) / 2)
    source
    def CanonicalEnsemble.twoState_entropy_eq :
    InformalLemma

    A simplification of the entropy of the two-state canonical ensemble.

    Equations
    Instances For
      source
      def CanonicalEnsemble.twoState_helmholtzFreeEnergy_eq :
      InformalLemma

      A simplification of the helmholtzFreeEnergy of the two-state canonical ensemble.

      Equations
      Instances For