Physlib.StatisticalMechanics.CanonicalEnsemble.TwoState

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

Two-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 := rfl

lemma twoState_partitionFunction_apply (E₀ E₁ : ℝ) (T : Temperature) :
    (twoState E₀ E₁).partitionFunction T = exp (- β T * E₀) + exp (- β T * E₁) := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).partitionFunction T = rexp (-↑T.β * E₀) + rexp (-↑T.β * E₁)
  rw [partitionFunction_of_fintype,E₀:ℝE₁:ℝT:Temperature⊢ ∑ i, rexp (-↑T.β * (twoState E₀ E₁).energy i) = rexp (-↑T.β * E₀) + rexp (-↑T.β * E₁)E₀:ℝ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₁) twoStateE₀:ℝ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₁)E₀:ℝ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₁)]E₀:ℝ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₁)
  simp [Fin.sum_univ_two]All goals completed! 🐙

lemma twoState_partitionFunction_apply_eq_cosh (E₀ E₁ : ℝ) (T : Temperature) :
    (twoState E₀ E₁).partitionFunction T =
    2 * exp (- β T * (E₀ + E₁) / 2) * cosh (β T * (E₁ - E₀) / 2) := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).partitionFunction T = 2 * rexp (-↑T.β * (E₀ + E₁) / 2) * cosh (↑T.β * (E₁ - E₀) / 2)
  rw [twoState_partitionFunction_apply,E₀:ℝE₁:ℝT:Temperature⊢ rexp (-↑T.β * E₀) + rexp (-↑T.β * E₁) = 2 * rexp (-↑T.β * (E₀ + E₁) / 2) * cosh (↑T.β * (E₁ - E₀) / 2)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) Real.cosh_eqE₀:ℝ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₁) =
  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₁) =
  2 * rexp (-↑T.β * (E₀ + E₁) / 2) * ((rexp (↑T.β * (E₁ - E₀) / 2) + rexp (-(↑T.β * (E₁ - E₀) / 2))) / 2)
  field_simpE₀:ℝE₁:ℝT:Temperature⊢ rexp (-(↑T.β * E₀)) + rexp (-(↑T.β * E₁)) =
  rexp (-(↑T.β * (E₀ + E₁) / 2)) * (rexp (↑T.β * (E₁ - E₀) / 2) + rexp (-(↑T.β * (E₁ - E₀) / 2)))
  simp only [mul_add, ← exp_add]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))
  ring_nfAll goals completed! 🐙@[simp]
lemma twoState_energy_fst (E₀ E₁ : ℝ) : (twoState E₀ E₁).energy 0 = E₀ := byE₀:ℝE₁:ℝ⊢ (twoState E₀ E₁).energy 0 = E₀
  rflAll goals completed! 🐙@[simp]
lemma twoState_energy_snd (E₀ E₁ : ℝ) : (twoState E₀ E₁).energy 1 = E₁ := byE₀:ℝE₁:ℝ⊢ (twoState E₀ E₁).energy 1 = E₁
  rflAll goals completed! 🐙

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


lemma twoState_probability_fst (E₀ E₁ : ℝ) (T : Temperature) :
    (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + Real.tanh (β T * (E₁ - E₀) / 2)) := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh (↑T.β * (E₁ - E₀) / 2))
  set x := β T * (E₁ - E₀) / 2E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh x)
  set C := β T * (E₀ + E₁) / 2E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh x)
  have hE0 : - β T * E₀ = x - C := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh (↑T.β * (E₁ - E₀) / 2))E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - C⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh x)
    simp [x, C]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2⊢ -(↑T.β * E₀) = ↑T.β * (E₁ - E₀) / 2 - ↑T.β * (E₀ + E₁) / 2E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - C⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh x); ringE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - C⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh x)E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - C⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh x)
  have hE1 : - β T * E₁ = -x - C := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh (↑T.β * (E₁ - E₀) / 2))E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh x)
    simp [x, C]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - C⊢ -(↑T.β * E₁) = -(↑T.β * (E₁ - E₀) / 2) - ↑T.β * (E₀ + E₁) / 2E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh x); ringE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh x)E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ (twoState E₀ E₁).probability T 0 = 1 / 2 * (1 + tanh x)
  rw [probability,E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * (twoState E₀ E₁).energy 0) / (twoState E₀ E₁).mathematicalPartitionFunction T = 1 / 2 * (1 + tanh x)E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * (twoState E₀ E₁).energy 0) / ∑ i, rexp (-↑T.β * (twoState E₀ E₁).energy i) = 1 / 2 * (1 + tanh x) mathematicalPartitionFunction_of_fintypeE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * (twoState E₀ E₁).energy 0) / ∑ i, rexp (-↑T.β * (twoState E₀ E₁).energy i) = 1 / 2 * (1 + tanh x)E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * (twoState E₀ E₁).energy 0) / ∑ i, rexp (-↑T.β * (twoState E₀ E₁).energy i) = 1 / 2 * (1 + tanh x)]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * (twoState E₀ E₁).energy 0) / ∑ i, rexp (-↑T.β * (twoState E₀ E₁).energy i) = 1 / 2 * (1 + tanh x)
  simp only [twoState, Fin.sum_univ_two, Fin.isValue]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * E₀) / (rexp (-↑T.β * E₀) + rexp (-↑T.β * E₁)) = 1 / 2 * (1 + tanh x)
  rw [hE0,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 (-↑T.β * E₁)) = 1 / 2 * (1 + tanh x)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 + tanh x) hE1E₀:ℝ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 + tanh x)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 + tanh x)]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 + tanh x)
  rw [Real.tanh_eq_sinh_div_cosh,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 + sinh x / cosh x)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)) Real.sinh_eq,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 / cosh x)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)) Real.cosh_eqE₀:ℝ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 - 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 - C) / (rexp (x - C) + rexp (-x - C)) = 1 / 2 * (1 + (rexp x - rexp (-x)) / 2 / ((rexp x + rexp (-x)) / 2))
  simp only [Real.exp_sub, Real.exp_neg]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))
  field_simpE₀:ℝ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)
  ringAll goals completed! 🐙

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


lemma twoState_probability_snd (E₀ E₁ : ℝ) (T : Temperature) :
    (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - Real.tanh (β T * (E₁ - E₀) / 2)) := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh (↑T.β * (E₁ - E₀) / 2))
  set x := β T * (E₁ - E₀) / 2E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh x)
  set C := β T * (E₀ + E₁) / 2E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh x)
  have hE0 : - β T * E₀ = x - C := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh (↑T.β * (E₁ - E₀) / 2))E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - C⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh x)
    simp [x, C]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2⊢ -(↑T.β * E₀) = ↑T.β * (E₁ - E₀) / 2 - ↑T.β * (E₀ + E₁) / 2E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - C⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh x); ringE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - C⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh x)E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - C⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh x)
  have hE1 : - β T * E₁ = -x - C := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh (↑T.β * (E₁ - E₀) / 2))E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh x)
    simp [x, C]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - C⊢ -(↑T.β * E₁) = -(↑T.β * (E₁ - E₀) / 2) - ↑T.β * (E₀ + E₁) / 2E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh x); ringE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh x)E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ (twoState E₀ E₁).probability T 1 = 1 / 2 * (1 - tanh x)
  rw [probability,E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * (twoState E₀ E₁).energy 1) / (twoState E₀ E₁).mathematicalPartitionFunction T = 1 / 2 * (1 - tanh x)E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * (twoState E₀ E₁).energy 1) / ∑ i, rexp (-↑T.β * (twoState E₀ E₁).energy i) = 1 / 2 * (1 - tanh x) mathematicalPartitionFunction_of_fintypeE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * (twoState E₀ E₁).energy 1) / ∑ i, rexp (-↑T.β * (twoState E₀ E₁).energy i) = 1 / 2 * (1 - tanh x)E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * (twoState E₀ E₁).energy 1) / ∑ i, rexp (-↑T.β * (twoState E₀ E₁).energy i) = 1 / 2 * (1 - tanh x)]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * (twoState E₀ E₁).energy 1) / ∑ i, rexp (-↑T.β * (twoState E₀ E₁).energy i) = 1 / 2 * (1 - tanh x)
  simp only [twoState, Fin.sum_univ_two, Fin.isValue]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * E₁) / (rexp (-↑T.β * E₀) + rexp (-↑T.β * E₁)) = 1 / 2 * (1 - tanh x)
  rw [hE0,E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x - ChE1:-↑T.β * E₁ = -x - C⊢ rexp (-↑T.β * E₁) / (rexp (x - C) + rexp (-↑T.β * E₁)) = 1 / 2 * (1 - tanh x)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 - tanh x) hE1E₀:ℝ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 - tanh x)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 - tanh x)]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 - tanh x)
  rw [Real.tanh_eq_sinh_div_cosh,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 - sinh x / cosh x)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)) Real.sinh_eq,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 / cosh x)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)) Real.cosh_eqE₀:ℝ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 - 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 - C) / (rexp (x - C) + rexp (-x - C)) = 1 / 2 * (1 - (rexp x - rexp (-x)) / 2 / ((rexp x + rexp (-x)) / 2))
  simp only [Real.exp_sub, Real.exp_neg]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))
  field_simpE₀:ℝ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)
  ringAll goals completed! 🐙



lemma twoState_meanEnergy_eq (E₀ E₁ : ℝ) (T : Temperature) :
    (twoState E₀ E₁).meanEnergy T =
    (E₀ + E₁) / 2 - (E₁ - E₀) / 2 * Real.tanh (β T * (E₁ - E₀) / 2) := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).meanEnergy T = (E₀ + E₁) / 2 - (E₁ - E₀) / 2 * tanh (↑T.β * (E₁ - E₀) / 2)
  rw [meanEnergy_of_fintypeE₀:ℝ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⊢ ∑ 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⊢ ∑ i, (twoState E₀ E₁).energy i * (twoState E₀ E₁).probability T i =
  (E₀ + E₁) / 2 - (E₁ - E₀) / 2 * tanh (↑T.β * (E₁ - E₀) / 2)
  simp [Fin.sum_univ_two, twoState_probability_fst, twoState_probability_snd]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)
  ringAll 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.


lemma twoState_helmholtzFreeEnergy_eq (E₀ E₁ : ℝ) (T : Temperature) :
    (twoState E₀ E₁).helmholtzFreeEnergy T =
      (β T  * (E₀ + E₁) / 2 - Real.log
          (2 * Real.cosh (β T * (E₁ - E₀) / 2))) / β T  := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (↑T.β * (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2))) / ↑T.β
  set x := β T * (E₁ - E₀) / 2E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (↑T.β * (E₀ + E₁) / 2 - log (2 * cosh x)) / ↑T.β
  set C := β T * (E₀ + E₁) / 2E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (C - log (2 * cosh x)) / ↑T.β
  have hE0 : -β T * E₀ = x +(- C) := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (↑T.β * (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2))) / ↑T.βE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -C⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (C - log (2 * cosh x)) / ↑T.β
    simp [x, C]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2⊢ -(↑T.β * E₀) = ↑T.β * (E₁ - E₀) / 2 + -(↑T.β * (E₀ + E₁) / 2)E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -C⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (C - log (2 * cosh x)) / ↑T.β
    ringE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -C⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (C - log (2 * cosh x)) / ↑T.βE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -C⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (C - log (2 * cosh x)) / ↑T.β
  have hE1 : -β T * E₁ = -x + (- C) := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (↑T.β * (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2))) / ↑T.βE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (C - log (2 * cosh x)) / ↑T.β
    simp [x, C]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -C⊢ -(↑T.β * E₁) = -(↑T.β * (E₁ - E₀) / 2) + -(↑T.β * (E₀ + E₁) / 2)E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (C - log (2 * cosh x)) / ↑T.β
    ringE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (C - log (2 * cosh x)) / ↑T.βE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (C - log (2 * cosh x)) / ↑T.β
  rw [helmholtzFreeEnergy,E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ -Constants.kB * ↑T.val * log ((twoState E₀ E₁).partitionFunction T) = (C - log (2 * cosh x)) / ↑T.βE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β twoState_partitionFunction_apply,E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ -Constants.kB * ↑T.val * log (rexp (-↑T.β * E₀) + rexp (-↑T.β * E₁)) = (C - log (2 * cosh x)) / ↑T.βE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β
    show (T.val : ℝ) = T.toReal byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (↑T.β * (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2))) / ↑T.βE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β rflAll goals completed! 🐙E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β,hE0,E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-↑T.β * E₁)) = (C - log (2 * cosh x)) / ↑T.βE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β hE1E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.βE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -C⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β
  have hfactor :
      Real.exp (x + (- C)) + Real.exp (-x + (- C)) = Real.exp (-C) * (2 * Real.cosh x) := byE₀:ℝE₁:ℝT:Temperature⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (↑T.β * (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2))) / ↑T.βE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β
    rw [Real.exp_add,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 + -C) = rexp (-C) * (2 * cosh x)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 (-C) * (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 + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β Real.exp_add,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 (-C) * (2 * cosh x)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 (-C) * (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 + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β Real.cosh_eqE₀:ℝ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 (-C) * (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 (-C) * (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 + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β]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 (-C) * (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 + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β
    ringE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.βE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * log (rexp (x + -C) + rexp (-x + -C)) = (C - log (2 * cosh x)) / ↑T.β
  rw [hfactor,E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * log (rexp (-C) * (2 * cosh x)) = (C - log (2 * cosh x)) / ↑T.βE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * (log (rexp (-C)) + log (2 * cosh x)) = (C - log (2 * cosh x)) / ↑T.β Real.log_mul
        (Real.exp_pos _).ne'
        (byE₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ 2 * cosh x ≠ 0E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * (log (rexp (-C)) + log (2 * cosh x)) = (C - log (2 * cosh x)) / ↑T.β positivityAll goals completed! 🐙E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * (log (rexp (-C)) + log (2 * cosh x)) = (C - log (2 * cosh x)) / ↑T.β : 2 * Real.cosh x ≠ 0)]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * (log (rexp (-C)) + log (2 * cosh x)) = (C - log (2 * cosh x)) / ↑T.β
  simp only [Real.log_exp,Temperature.β_toReal,div_eq_mul_inv, one_mul, inv_inv]E₀:ℝE₁:ℝT:Temperaturex:ℝ := ↑T.β * (E₁ - E₀) / 2C:ℝ := ↑T.β * (E₀ + E₁) / 2hE0:-↑T.β * E₀ = x + -ChE1:-↑T.β * E₁ = -x + -Chfactor:rexp (x + -C) + rexp (-x + -C) = rexp (-C) * (2 * cosh x)⊢ -Constants.kB * T.toReal * (-C + log (2 * cosh x)) = (C - log (2 * cosh x)) * (Constants.kB * T.toReal)
  ringAll goals completed! 🐙

An instance of twoState_helmholtzFreeEnergy_eq assuming T ≠ 0


lemma twoState_helmholtzFreeEnergy_eq_T_neq_zero (E₀ E₁ : ℝ) (T : Temperature) (Th : T ≠ 0) :
    (twoState E₀ E₁).helmholtzFreeEnergy T =
      (E₀ + E₁) / 2 - Real.log (2 * Real.cosh (β T * (E₁ - E₀) / 2)) / β T  := byE₀:ℝE₁:ℝT:TemperatureTh:T ≠ 0⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2)) / ↑T.β
  have hTval : T.val ≠ 0 := fun h => Th (Temperature.ext h)E₀:ℝE₁:ℝT:TemperatureTh:T ≠ 0hTval:T.val ≠ 0⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2)) / ↑T.β
  have hβne : (β T : ℝ) ≠ 0 := (Temperature.beta_pos T (pos_iff_ne_zero.mpr hTval)).ne'E₀:ℝE₁:ℝT:TemperatureTh:T ≠ 0hTval:T.val ≠ 0hβne:↑T.β ≠ 0⊢ (twoState E₀ E₁).helmholtzFreeEnergy T = (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2)) / ↑T.β
  rw [twoState_helmholtzFreeEnergy_eqE₀:ℝE₁:ℝT:TemperatureTh:T ≠ 0hTval:T.val ≠ 0hβne:↑T.β ≠ 0⊢ (↑T.β * (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2))) / ↑T.β =
  (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2)) / ↑T.βE₀:ℝE₁:ℝT:TemperatureTh:T ≠ 0hTval:T.val ≠ 0hβne:↑T.β ≠ 0⊢ (↑T.β * (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2))) / ↑T.β =
  (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2)) / ↑T.β]E₀:ℝE₁:ℝT:TemperatureTh:T ≠ 0hTval:T.val ≠ 0hβne:↑T.β ≠ 0⊢ (↑T.β * (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2))) / ↑T.β =
  (E₀ + E₁) / 2 - log (2 * cosh (↑T.β * (E₁ - E₀) / 2)) / ↑T.β
  field_simpAll goals completed! 🐙