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
    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