feat: Thermodynamics (and some minor changes to StatisticalMechanics)

[ichxorya]

TODO. Refer to #860 #861 #862

[jstoobysmith]

Please can you let me know when you want this reviewing, or post on https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/PR.20reviews/with/575446226

[ichxorya]

Please can you let me know when you want this reviewing, or post on https://leanprover.zulipchat.com/#narrow/channel/479953-PhysLean/topic/PR.20reviews/with/575446226

Thank you, for now I would like to clarify few minor problems (notes).

From Thermodynamics/Temperature/Basic.lean

/-- Function for `Temperature`:

Calculate the inverse temperature `β` corresponding to a given temperature `T`.

- Note:

1. This has dimensions equivalent to `Energy` to the power `-1`. Refer to the concept of
"thermodynamic beta" in thermodynamics for more details.

2. Currently this formula allows for "non-negative" temperatures, which includes absolute zero in
the denominator. In physical terms, absolute zero is a limit that cannot be reached, and the formula
for `β` is not well-defined at `T = 0`. Therefore, while the type `Temperature` allows for `T = 0`,
we should refactor this definition in the future to exclude absolute zero, either by refining the
domain or by defining `β` as a partial function that is only defined for strictly positive
temperatures.
-/
noncomputable def β (T : Temperature) : ℝ≥0 :=
  -- Given the formula `(1 / (kB * (T : ℝ))) : ℝ≥0`, we need to show that this is non-negative to
  -- fit the type `ℝ≥0`.
  ⟨1 / (kB * (T : ℝ)), by
    -- To show that `1 / (kB * (T : ℝ))` is non-negative, we apply `div_nonneg`, which requires us
    -- to show that the numerator is non-negative and the denominator is non-negative [See Note 2].
    apply div_nonneg
    -- `case ha`: The goal is `⊢ 0 ≤ 1`, which is true by `zero_le_one`, since `1` is a non-negative
    -- real number. QED for this case.
    · exact zero_le_one
    -- `case hb`: The goal is `⊢ 0 ≤ kB * (T : ℝ)`, which we can show by applying `mul_nonneg` to
    -- the product `kB * (T : ℝ)`.
    · apply mul_nonneg
      -- `case hb.ha`: The goal is `⊢ 0 ≤ kB`, which is true by the lemma `kB_nonneg`, since the
      -- Boltzmann constant is a positive physical constant. QED for this case.
      · exact kB_nonneg
      -- `case hb.hb`: The goal is `⊢ 0 ≤ (T : ℝ)`, which is true by `zero_le_real T`, since the
      -- real number representation of a `Temperature` is non-negative. QED for this case.
      -- All cases have been proven. QED.
      · exact zero_le_real T⟩

And in Thermodynamics/Temperature/Calculus.lean (which was offloaded from Basic since it was too lengthy)

/-- Function for `Temperature`:

Map a real number `t` to the inverse temperature `β` corresponding to
the temperature `Real.toNNReal t` (`max t 0`), returned as a real number.

- Note:

1. Why `ℝ` instead of `ℝ≥0`, if `β` is of type `ℝ≥0`?
-/
noncomputable def βFromReal (t : ℝ) : ℝ := ((Temperature.ofNNReal (Real.toNNReal t)).β)

/-- Lemma for `Temperature`:

Explicit closed-form for `βFromReal t` when `t > 0`: `βFromReal t = 1 / (kB * t)`.
-/
lemma β_fun_T_formula (t : ℝ) (h_t_pos : 0 < t) :
    βFromReal t = (1 :  ℝ) / (kB * t) := by
  -- We derive `h_t_nonneg : 0 ≤ t` from `h_t_pos` by weakening strict
  -- inequality to non-strict inequality.
  have h_t_nonneg : (0 : ℝ) ≤ t := h_t_pos.le
  -- We derive `h_beta_formula` which states that the explicit formula
  -- for `β` applied to `Real.toNNReal t` equals `1 / (kB * t)`,
  -- by simplifying using the definitions of `β`, `ofNNReal`, `toReal`,
  -- and the fact that `Real.toNNReal t = t` when `t ≥ 0`.
  have h_beta_formula :
      ((Temperature.ofNNReal (Real.toNNReal t)).β : ℝ) = (1 :  ℝ) / (kB * t) := by
    simp [Temperature.β, Temperature.ofNNReal, Temperature.toReal,
          Real.toNNReal_of_nonneg h_t_nonneg, one_div, mul_comm]
  -- We conclude by simplifying the definition of `βFromReal` and
  -- applying `h_beta_formula`. QED.
  simpa [βFromReal] using h_beta_formula

[jstoobysmith]

I agree with your comments about Temperature should likely be excluded from being zero. If we do this, do you know if we can still get the limit as T goes to zero to work? Maybe including some documentation of how that works out would be nice.

Is βFromReal used anywhere? If not we should likely remove it.

[jstoobysmith]

(FYI just checking you got my email, it bounced from one of the cced addresses)

[ichxorya]

(FYI just checking you got my email, it bounced from one of the cced addresses)

I'm really sorry for not replying the moment I received the email. I should have sent a thank you message, yet I thought it would be better to continue the email conversation with more updates if we worked fast enough (we unfortunately didn't make it in time 🥲).

[jstoobysmith]

No don't worry at all - was just checking because of the email bounce. No obligation to responded in any time frame.

[ichxorya]

I agree with your comments about Temperature should likely be excluded from being zero. If we do this, do you know if we can still get the limit as T goes to zero to work? Maybe including some documentation of how that works out would be nice.

Is βFromReal used anywhere? If not we should likely remove it.

βFromReal is used in proofs on Temperature calculus (ie differentiable); and even in Lemma of StatisticalMechanics/CanonicalEnsembles/Lemmas.lean

About Temperature, I might try experiencing with non Zero value, however it might be a breaking change. Hopefully we can resolve the βFromReal problem first.

[ichxorya]

I'm working on this alternative, seems good. Many things to do before moving to Ideal gas.

https://github.com/SEhumantics/PhysLean/blob/feat%2Fnghiabt%2Fpostemp/PhysLean%2FThermodynamics%2FTemperature%2FBasic.lean

[jstoobysmith]

Agreed, I think introducing PositiveTemperature as a different data structure now is a great idea - if it ends up that we essentially always end up using PositiveTemperature then doing a name shuffle might be good.

[jstoobysmith]

BTW when it comes to finally merging this into PhysLean, it may be easier to split this up into smaller PRs - it makes the process of reviewing a lot easier and quicker.

[ichxorya]

BTW when it comes to finally merging this into PhysLean, it may be easier to split this up into smaller PRs - it makes the process of reviewing a lot easier and quicker.

Thank you, I will resubmit a smaller Temperature pr for this fix of type R>0!