diff --git a/PhysLean.lean b/PhysLean.lean index a60765a40..6c3be4834 100644 --- a/PhysLean.lean +++ b/PhysLean.lean @@ -388,6 +388,10 @@ import PhysLean.StringTheory.FTheory.SU5.Quanta.TenQuanta import PhysLean.Thermodynamics.Basic import PhysLean.Thermodynamics.IdealGas.Basic import PhysLean.Thermodynamics.Temperature.Basic +import PhysLean.Thermodynamics.Temperature.Calculus +import PhysLean.Thermodynamics.Temperature.Convergence +import PhysLean.Thermodynamics.Temperature.Regularity +import PhysLean.Thermodynamics.Temperature.TemperatureScales import PhysLean.Thermodynamics.Temperature.TemperatureUnits import PhysLean.Units.Basic import PhysLean.Units.Dimension diff --git a/PhysLean/Meta/Types/PosReal.lean b/PhysLean/Meta/Types/PosReal.lean new file mode 100644 index 000000000..414256a1c --- /dev/null +++ b/PhysLean/Meta/Types/PosReal.lean @@ -0,0 +1,11 @@ +import Mathlib.Data.Real.Basic + +/-- The type of strictly positive real numbers. -/ +abbrev PosReal := { x : ℝ // 0 < x } + +notation "ℝ>0" => PosReal + +/-- The type of extended strictly positive real numbers (ℝ>0 ∪ {∞}). -/ +abbrev EPosReal := WithTop PosReal + +notation "ℝ>0∞" => EPosReal diff --git a/PhysLean/StatisticalMechanics/BoltzmannConstant.lean b/PhysLean/StatisticalMechanics/BoltzmannConstant.lean index 5ddf4e05a..0d5482367 100644 --- a/PhysLean/StatisticalMechanics/BoltzmannConstant.lean +++ b/PhysLean/StatisticalMechanics/BoltzmannConstant.lean @@ -1,9 +1,10 @@ /- -Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Joseph Tooby-Smith -/ import Mathlib.Data.NNReal.Defs +import PhysLean.Meta.Types.PosReal /-! # Boltzmann constant @@ -21,17 +22,17 @@ namespace Constants /-- The Boltzmann constant in units of `m ^ 2 kg s ^ (-2) K ^ (-1)`. As long as one does not use the underlying value of this quantity, then it can be used as Boltzmann's constant in an arbitrary set of units. -/ -def kBAx : {p : ℝ | 0 < p} := ⟨1.380649e-23, by norm_num⟩ +def kBAx : ℝ>0 := ⟨1.380649e-23, by norm_num⟩ /-- The Boltzmann constant in a given but arbitrary set of units. Boltzman's constant has dimension equivalent to `Energy/Temperature`. -/ -noncomputable def kB : ℝ := kBAx.1 +noncomputable def kB : ℝ := kBAx.val /-- The Boltzmann constant is positive. -/ -lemma kB_pos : 0 < kB := kBAx.2 +lemma kB_pos : 0 < kB := kBAx.property /-- The Boltzmann constant is non-negative. -/ -lemma kB_nonneg : 0 ≤ kB := le_of_lt kBAx.2 +lemma kB_nonneg : 0 ≤ kB := le_of_lt kBAx.property /-- The Boltzmann constant is not equal to zero. -/ lemma kB_ne_zero : kB ≠ 0 := by diff --git a/PhysLean/StatisticalMechanics/CanonicalEnsemble/Basic.lean b/PhysLean/StatisticalMechanics/CanonicalEnsemble/Basic.lean index 31bfc4909..1d16866b4 100644 --- a/PhysLean/StatisticalMechanics/CanonicalEnsemble/Basic.lean +++ b/PhysLean/StatisticalMechanics/CanonicalEnsemble/Basic.lean @@ -370,7 +370,8 @@ lemma μBolt_ne_zero_of_μ_ne_zero (T : Temperature) (h : 𝓒.μ ≠ 0) : simp [μBolt] at ⊢ h rw [Measure.ext_iff'] at ⊢ h simp only [Measure.coe_zero, Pi.zero_apply] - have hs : {x | ENNReal.ofReal (rexp (-(↑T.β * 𝓒.energy x))) ≠ 0} = Set.univ := by + have hs : {x | ENNReal.ofReal + (rexp (-(T.toReal⁻¹ * Constants.kB⁻¹ * 𝓒.energy x))) ≠ 0} = Set.univ := by ext i simp only [ne_eq, ENNReal.ofReal_eq_zero, not_le, Set.mem_setOf_eq, Set.mem_univ, iff_true] exact exp_pos _ @@ -454,7 +455,7 @@ lemma mathematicalPartitionFunction_eq_zero_iff (T : Temperature) [IsFiniteMeasu have h : s = Set.univ := by ext i simp [s] - exact exp_pos (-(T.β * 𝓒.energy i)) + exact exp_pos (-(T.toReal⁻¹ * Constants.kB⁻¹ * 𝓒.energy i)) change 𝓒.μ s = 0 ↔ 𝓒.μ = 0 rw [h] simp only [Measure.measure_univ_eq_zero] diff --git a/PhysLean/StatisticalMechanics/CanonicalEnsemble/Finite.lean b/PhysLean/StatisticalMechanics/CanonicalEnsemble/Finite.lean index faeb73508..e5c586993 100644 --- a/PhysLean/StatisticalMechanics/CanonicalEnsemble/Finite.lean +++ b/PhysLean/StatisticalMechanics/CanonicalEnsemble/Finite.lean @@ -293,8 +293,18 @@ lemma sum_probability_eq_one have hZdef := mathematicalPartitionFunction_of_fintype (𝓒:=𝓒) T have hZpos := mathematicalPartitionFunction_pos_finite (𝓒:=𝓒) (T:=T) have hZne : 𝓒.mathematicalPartitionFunction T ≠ 0 := hZpos.ne' - simp [hZdef] - simp_all only [neg_mul, ne_eq, not_false_eq_true] + have hZdef' : 𝓒.mathematicalPartitionFunction T = + ∑ x, rexp (-(T.toReal⁻¹ * kB⁻¹ * 𝓒.energy x)) := by + simpa [Temperature.β, one_div, mul_comm, mul_left_comm, mul_assoc] using hZdef + have hZne' : ∑ x, rexp (-(T.toReal⁻¹ * kB⁻¹ * 𝓒.energy x)) ≠ 0 := by + rw [← hZdef'] + exact hZne + have hnum : + ∑ x, rexp (-↑T.β * 𝓒.energy x) = ∑ x, rexp (-(T.toReal⁻¹ * kB⁻¹ * 𝓒.energy x)) := by + simp [Temperature.β, one_div, mul_comm, mul_assoc] + rw [hZdef'] + rw [hnum] + field_simp [hZne'] /-- The entropy of a finite canonical ensemble (Shannon entropy) is non-negative. -/ lemma entropy_nonneg [MeasurableSingletonClass ι] [IsFinite 𝓒] [Nonempty ι] (T : Temperature) : @@ -409,11 +419,29 @@ lemma meanEnergy_Beta_eq_finite [MeasurableSingletonClass ι] [IsFinite 𝓒] (b 𝓒.meanEnergyBeta b = 𝓒.meanEnergyBetaReal b := by let T := Temperature.ofβ (Real.toNNReal b) have hT_beta : (T.β : ℝ) = b := by - simp [T, Real.toNNReal_of_nonneg hb.le] + change ((Temperature.ofβ (Real.toNNReal b)).β : ℝ) = b + simpa [Real.toNNReal_of_nonneg hb.le] using + congrArg (fun x : NNReal => (x : ℝ)) (Temperature.β_ofβ (Real.toNNReal b)) + have hT_beta' : T.toReal⁻¹ * kB⁻¹ = b := by + simpa [Temperature.β, one_div, mul_comm, mul_left_comm, mul_assoc] using hT_beta rw [meanEnergyBeta, meanEnergy_of_fintype 𝓒 T, meanEnergyBetaReal] refine Finset.sum_congr rfl fun i _ => ?_ - simp [CanonicalEnsemble.probability, probabilityBetaReal, - mathematicalPartitionFunction_of_fintype, mathematicalPartitionFunctionBetaReal, hT_beta] + have hden : 𝓒.mathematicalPartitionFunction T = 𝓒.mathematicalPartitionFunctionBetaReal b := by + rw [mathematicalPartitionFunction_of_fintype, mathematicalPartitionFunctionBetaReal] + refine Finset.sum_congr rfl ?_ + intro j hj + simp [hT_beta'] + have hprob : + rexp (-(T.toReal⁻¹ * kB⁻¹ * 𝓒.energy i)) / 𝓒.mathematicalPartitionFunction T + = rexp (-(b * 𝓒.energy i)) / 𝓒.mathematicalPartitionFunctionBetaReal b := by + calc + rexp (-(T.toReal⁻¹ * kB⁻¹ * 𝓒.energy i)) / 𝓒.mathematicalPartitionFunction T + = rexp (-(b * 𝓒.energy i)) / 𝓒.mathematicalPartitionFunction T := by + simp [hT_beta'] + _ = rexp (-(b * 𝓒.energy i)) / 𝓒.mathematicalPartitionFunctionBetaReal b := by + rw [hden] + simpa [CanonicalEnsemble.probability, probabilityBetaReal] using + congrArg (fun p => 𝓒.energy i * p) hprob lemma differentiable_meanEnergyBetaReal [Nonempty ι] : Differentiable ℝ 𝓒.meanEnergyBetaReal := by @@ -568,7 +596,7 @@ lemma derivWithin_meanEnergy_Beta_eq_neg_variance [MeasurableSingletonClass ι][𝓒.IsFinite] (T : Temperature) (hT_pos : 0 < T.val) : derivWithin 𝓒.meanEnergyBeta (Set.Ioi 0) (T.β : ℝ) = - 𝓒.energyVariance T := by let β₀ := (T.β : ℝ) - have hβ₀_pos : 0 < β₀ := beta_pos T hT_pos + have hβ₀_pos : 0 < β₀ := β_pos T hT_pos have h_eq_on : Set.EqOn 𝓒.meanEnergyBeta 𝓒.meanEnergyBetaReal (Set.Ioi 0) := by intro b hb; exact meanEnergy_Beta_eq_finite 𝓒 b hb rw [derivWithin_congr h_eq_on (h_eq_on hβ₀_pos)] @@ -578,8 +606,11 @@ lemma derivWithin_meanEnergy_Beta_eq_neg_variance rw [deriv_meanEnergyBetaReal 𝓒 β₀] have h_U_eq : 𝓒.meanEnergyBetaReal β₀ = 𝓒.meanEnergy T := by rw [← meanEnergy_Beta_eq_finite 𝓒 β₀ hβ₀_pos] - simp [meanEnergyBeta] - simp_all only [NNReal.coe_pos, toNNReal_coe, ofβ_β, β₀] + change 𝓒.meanEnergy (Temperature.ofβ (Real.toNNReal β₀)) = 𝓒.meanEnergy T + have hβ₀_toNNReal : Real.toNNReal β₀ = T.β := by + change Real.toNNReal ((T.β : ℝ)) = T.β + simpa using (show Real.toNNReal ((T.β : ℝ)) = T.β from Real.toNNReal_coe) + rw [hβ₀_toNNReal, Temperature.ofβ_β] have h_prob_eq (i : ι) : 𝓒.probabilityBetaReal β₀ i = 𝓒.probability T i := by unfold probabilityBetaReal CanonicalEnsemble.probability congr 1 @@ -594,7 +625,7 @@ lemma derivWithin_meanEnergy_Beta_eq_neg_variance theorem fluctuation_dissipation_theorem_finite [MeasurableSingletonClass ι] [𝓒.IsFinite] (T : Temperature) (hT_pos : 0 < T.val) : 𝓒.heatCapacity T = 𝓒.energyVariance T / (kB * (T.val : ℝ)^2) := by - have hβ₀_pos : 0 < (T.β : ℝ) := beta_pos T hT_pos + have hβ₀_pos : 0 < (T.β : ℝ) := β_pos T hT_pos let β₀ := (T.β : ℝ) have h_diff_U_beta : DifferentiableWithinAt ℝ 𝓒.meanEnergyBeta (Set.Ioi 0) β₀ := by have h_eq_on : Set.EqOn 𝓒.meanEnergyBeta 𝓒.meanEnergyBetaReal (Set.Ioi 0) := by diff --git a/PhysLean/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean b/PhysLean/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean index ef1c14fcf..70a45d31c 100644 --- a/PhysLean/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean +++ b/PhysLean/StatisticalMechanics/CanonicalEnsemble/Lemmas.lean @@ -4,6 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Matteo Cipollina, Joseph Tooby-Smith -/ import PhysLean.StatisticalMechanics.CanonicalEnsemble.Basic +import PhysLean.Thermodynamics.Temperature.Calculus /-! # Canonical Ensemble: Thermodynamic Identities and Relations @@ -266,7 +267,10 @@ theorem helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy _ = _ := by simp [add_comm, sub_eq_add_neg, mul_comm, mul_left_comm, mul_assoc] have hkβT : T.val * (kB * (T.β : ℝ)) = 1 := by - simp [hkβ, hTne] + rw [hkβ] + field_simp [hTne] + have hkβT' : T.val * (kB * (kB⁻¹ * T.toReal⁻¹)) = 1 := by + simpa [Temperature.β, one_div, mul_comm, mul_left_comm, mul_assoc] using hkβT have h_rhs : 𝓒.meanEnergy T - T.val * 𝓒.thermodynamicEntropy T = -kB * T.val * @@ -289,7 +293,7 @@ theorem helmholtzFreeEnergy_eq_meanEnergy_sub_temp_mul_thermodynamicEntropy _ = 𝓒.meanEnergy T - 1 * 𝓒.meanEnergy T - T.val * kB * Real.log (𝓒.mathematicalPartitionFunction T) + T.val * kB * 𝓒.dof * Real.log 𝓒.phaseSpaceunit := by - simp [hkβT, mul_comm, mul_assoc] + simp [hkβT', mul_comm, mul_assoc] _ = -kB * T.val * (Real.log (𝓒.mathematicalPartitionFunction T) - (𝓒.dof : ℝ) * Real.log 𝓒.phaseSpaceunit) := by @@ -518,12 +522,11 @@ lemma meanEnergy_eq_neg_deriv_log_mathZ_of_beta (fun β : ℝ => Real.log (∫ i, Real.exp (-β * 𝓒.energy i) ∂𝓒.μ)) (Set.Ioi 0) (T.β : ℝ)) := by set f : ℝ → ℝ := fun β => ∫ i, Real.exp (-β * 𝓒.energy i) ∂𝓒.μ - have hβ_pos : 0 < (T.β : ℝ) := beta_pos T hT_pos + have hβ_pos : 0 < (T.β : ℝ) := β_pos T hT_pos have hZpos : 0 < f (T.β : ℝ) := by have hZ := mathematicalPartitionFunction_pos (𝓒:=𝓒) (T:=T) - have hEq : f (T.β : ℝ) = 𝓒.mathematicalPartitionFunction T := by - simp [f, mathematicalPartitionFunction_eq_integral (𝓒:=𝓒) (T:=T)] - simpa [hEq] using hZ + simpa [f, mathematicalPartitionFunction_eq_integral (𝓒:=𝓒) (T:=T), + Temperature.β, one_div, mul_comm, mul_left_comm, mul_assoc] using hZ have h_log : HasDerivWithinAt (fun β : ℝ => Real.log (f β)) @@ -548,14 +551,12 @@ lemma meanEnergy_eq_neg_deriv_log_mathZ_of_beta = (1 / f (T.β : ℝ)) * (- ∫ i, 𝓒.energy i * Real.exp (-(T.β : ℝ) * 𝓒.energy i) ∂𝓒.μ) := h_log.derivWithin hUD - have h_f_eval : - f (T.β : ℝ) = ∫ i, Real.exp (-(T.β : ℝ) * 𝓒.energy i) ∂𝓒.μ := rfl have h_ratio : (∫ i, 𝓒.energy i * Real.exp (-(T.β : ℝ) * 𝓒.energy i) ∂𝓒.μ) / (∫ i, Real.exp (-(T.β : ℝ) * 𝓒.energy i) ∂𝓒.μ) = (1 / f (T.β : ℝ)) * (∫ i, 𝓒.energy i * Real.exp (-(T.β : ℝ) * 𝓒.energy i) ∂𝓒.μ) := by - simp [h_f_eval, div_eq_mul_inv, mul_comm] + simp [f, div_eq_mul_inv, mul_comm, mul_left_comm, mul_assoc] calc 𝓒.meanEnergy T = _ := h_mean_ratio _ = (1 / f (T.β : ℝ)) * @@ -611,16 +612,29 @@ lemma log_phys_eq_log_math_sub_const_on_Ioi Real.log (𝓒.partitionFunction (Temperature.ofβ (Real.toNNReal β))) = -((𝓒.dof : ℝ) * Real.log 𝓒.phaseSpaceunit) + Real.log (∫ i, Real.exp (-β * 𝓒.energy i) ∂ 𝓒.μ) := by - have h_integral_pos : 0 < ∫ i, Real.exp (-β * 𝓒.energy i) ∂ 𝓒.μ := by - have h_eq : ∫ i, Real.exp (-β * 𝓒.energy i) ∂ 𝓒.μ = - ∫ i, Real.exp (-(Real.toNNReal β).val * 𝓒.energy i) ∂ 𝓒.μ := by - simp [hβnn] - rw [h_eq] - simp [mathematicalPartitionFunction_eq_integral - (𝓒:=𝓒) (T:=Temperature.ofβ (Real.toNNReal β))] at hZpos - simp [hZpos] have h_beta_eq : (Temperature.ofβ (Real.toNNReal β)).β = Real.toNNReal β := by - simp_all only [gt_iff_lt, mem_Ioi, coe_toNNReal', sup_eq_left, log_pow, neg_mul, β_ofβ] + simp_all only [gt_iff_lt, mem_Ioi, coe_toNNReal', sup_eq_left, log_pow, β_ofβ] + have h_integral_pos : 0 < ∫ i, Real.exp (-β * 𝓒.energy i) ∂ 𝓒.μ := by + have h_int_eq0 : + ∫ i, Real.exp (-((Temperature.ofβ (Real.toNNReal β)).β : ℝ) * 𝓒.energy i) ∂ 𝓒.μ = + 𝓒.mathematicalPartitionFunction (Temperature.ofβ (Real.toNNReal β)) := by + exact (mathematicalPartitionFunction_eq_integral + (𝓒:=𝓒) (T:=Temperature.ofβ (Real.toNNReal β))).symm + have h_int_eq : ∫ i, Real.exp (-β * 𝓒.energy i) ∂ 𝓒.μ = + 𝓒.mathematicalPartitionFunction (Temperature.ofβ (Real.toNNReal β)) := by + have h_int_eq1 : + ∫ i, Real.exp (-(β * (kB * (kB⁻¹ * 𝓒.energy i)))) ∂ 𝓒.μ = + 𝓒.mathematicalPartitionFunction (Temperature.ofβ (Real.toNNReal β)) := by + simpa [Temperature.β, hβnn, one_div, mul_comm, mul_left_comm, mul_assoc] using h_int_eq0 + have h_int_eq2 : + ∫ i, Real.exp (-(β * (kB * (kB⁻¹ * 𝓒.energy i)))) ∂ 𝓒.μ = + ∫ i, Real.exp (-β * 𝓒.energy i) ∂ 𝓒.μ := by + refine integral_congr_ae ?_ + filter_upwards with i + field_simp [kB_ne_zero] + exact h_int_eq2.symm.trans h_int_eq1 + rw [h_int_eq] + exact hZpos rw [partitionFunction_def, mathematicalPartitionFunction_eq_integral (𝓒:=𝓒) (T:=Temperature.ofβ (Real.toNNReal β)), h_beta_eq, @@ -663,7 +677,7 @@ lemma derivWithin_log_phys_eq_derivWithin_log_math have h_eq' : Set.EqOn F_phys (fun β => F_math β - C) (Set.Ioi (0:ℝ)) := by simpa [F_phys, F_math] using h_eq - have h_mem : (T.β : ℝ) ∈ Set.Ioi (0:ℝ) := beta_pos T hT_pos + have h_mem : (T.β : ℝ) ∈ Set.Ioi (0:ℝ) := β_pos T hT_pos have h_congr : derivWithin F_phys (Set.Ioi 0) (T.β : ℝ) = derivWithin (fun β => F_math β - C) (Set.Ioi 0) (T.β : ℝ) := by @@ -769,12 +783,11 @@ lemma heatCapacity_eq_deriv_meanEnergyBeta = (derivWithin (𝓒.meanEnergyBeta) (Set.Ioi 0) (T.β : ℝ)) * (-1 / (kB * (T.val : ℝ)^2)) := by unfold heatCapacity meanEnergy_T - have h_U_eq_comp : (𝓒.meanEnergy_T) = fun t : ℝ => (𝓒.meanEnergyBeta) (betaFromReal t) := by + have h_U_eq_comp : (𝓒.meanEnergy_T) = fun t : ℝ => (𝓒.meanEnergyBeta) (βFromReal t) := by funext t - dsimp [meanEnergy_T, meanEnergyBeta, betaFromReal] - simp + simp only [meanEnergy_T, meanEnergyBeta, βFromReal, Real.toNNReal_coe, Temperature.ofβ_β] let dUdβ := derivWithin (𝓒.meanEnergyBeta) (Set.Ioi 0) (T.β : ℝ) - have h_chain := chain_rule_T_beta (F:=𝓒.meanEnergyBeta) (F':=dUdβ) T hT_pos hU_deriv + have h_chain := chain_rule_T_β (F:=𝓒.meanEnergyBeta) (F':=dUdβ) T hT_pos hU_deriv have h_UD : UniqueDiffWithinAt ℝ (Set.Ioi (0 : ℝ)) (T.val : ℝ) := (isOpen_Ioi : IsOpen (Set.Ioi (0 : ℝ))).uniqueDiffWithinAt hT_pos diff --git a/PhysLean/Thermodynamics/Basic.lean b/PhysLean/Thermodynamics/Basic.lean index f58a0b4de..2f7e82d23 100644 --- a/PhysLean/Thermodynamics/Basic.lean +++ b/PhysLean/Thermodynamics/Basic.lean @@ -1,7 +1,7 @@ /- -Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Tooby-Smith +Authors: Trong-Nghia Be, Tan-Phuoc-Hung Le, Joseph Tooby-Smith -/ /-! diff --git a/PhysLean/Thermodynamics/Temperature/Basic.lean b/PhysLean/Thermodynamics/Temperature/Basic.lean index ef6109dea..d18ab5942 100644 --- a/PhysLean/Thermodynamics/Temperature/Basic.lean +++ b/PhysLean/Thermodynamics/Temperature/Basic.lean @@ -1,355 +1,468 @@ /- -Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Matteo Cipollina, Joseph Tooby-Smith +Authors: Trong-Nghia Be, Matteo Cipollina, Tan-Phuoc-Hung Le, Joseph Tooby-Smith -/ -import Mathlib.Analysis.Calculus.Deriv.Inv import Mathlib.Analysis.InnerProductSpace.Basic import PhysLean.StatisticalMechanics.BoltzmannConstant -import PhysLean.Meta.TODO.Basic -/-! +import PhysLean.Meta.Types.PosReal +/-! # Temperature -In this module we define the type `Temperature`, corresponding to the temperature in a given -(but arbitrary) set of units which have absolute zero at zero. +In this module we define the types `Temperature` and `PositiveTemperature` to represent +absolute thermodynamic temperature in kelvin. +This is the version of temperature most often used in undergraduate and non-mathematical physics. + +We also define the inverse temperature `β` (thermodynamic beta/coldness) +and its inverse function `ofβ`, which are commonly used in statistical mechanics and thermodynamics. -This is the version of temperature most often used in undergraduate and -non-mathematical physics. +For affine display scales with offsets (such as Celsius and Fahrenheit), see +`PhysLean.Thermodynamics.Temperature.TemperatureScales`. -The choice of units can be made on a case-by-case basis, as long as they are done consistently. +For regularity properties of `ofβ`, see +`PhysLean.Thermodynamics.Temperature.Regularity`. +For convergence results, see +`PhysLean.Thermodynamics.Temperature.Convergence`. + +For calculus relating T and β, see +`PhysLean.Thermodynamics.Temperature.Calculus`. -/ open NNReal -/-- The type `Temperature` represents the temperature in a given (but arbitrary) set of units - (preserving zero). It currently wraps `ℝ≥0`, i.e., absolute temperature in nonnegative reals. -/ +/-- The type `Temperature` represents absolute thermodynamic temperature in kelvin. +-/ structure Temperature where - /-- The nonnegative real value of the temperature. -/ val : ℝ≥0 +/-- The type `PositiveTemperature` represents strictly positive absolute thermodynamic temperature +in kelvin. + +It is defined as a subtype of `Temperature` where the `val` field is strictly positive. +-/ +def PositiveTemperature := { T : Temperature // 0 < T.val } + +/-! +## Basic instances and definitions for `Temperature` +-/ namespace Temperature open Constants -/-- Coercion to `ℝ≥0`. -/ -instance : Coe Temperature ℝ≥0 := ⟨fun T => T.val⟩ +/-- Type coercion (implicit casting) from `Temperature` to `ℝ≥0`. -/-- The underlying real-number associated with the temperature. -/ -noncomputable def toReal (T : Temperature) : ℝ := NNReal.toReal T.val +Defined as a function that takes a `Temperature` and returns its underlying `ℝ≥0` value (by +accessing the `val` field). +-/ +instance : Coe Temperature ℝ≥0 := ⟨fun (T : Temperature) => T.val⟩ -/-- Coercion to `ℝ`. -/ -noncomputable instance : Coe Temperature ℝ := ⟨toReal⟩ +/-- Function for `Temperature`: -/-- Topology on `Temperature` induced from `ℝ≥0`. -/ -instance : TopologicalSpace Temperature := - TopologicalSpace.induced (fun T : Temperature => (T.val : ℝ≥0)) inferInstance +Convert a `Temperature` to a real number in `ℝ`. +-/ +def toReal (T : Temperature) : ℝ := NNReal.toReal T.val +/-- Type coercion (implicit casting) from `Temperature` to `ℝ`. + +Defined as a function that takes a `Temperature` and returns the `val` field converted to `ℝ`. +-/ +instance : Coe Temperature ℝ := ⟨fun (T : Temperature) => Temperature.toReal T⟩ + +/-- Topology on `Temperature` induced from `ℝ≥0`. + +Defined using the `induced` topology from the coercion function that maps a `Temperature` to its +real number representation in `ℝ≥0`. +-/ +instance : TopologicalSpace Temperature := TopologicalSpace.induced + (fun (T : Temperature) => (T : ℝ≥0)) inferInstance + +/-- The zero temperature (absolute zero) in kelvin. -/ instance : Zero Temperature := ⟨⟨0⟩⟩ -@[ext] lemma ext {T₁ T₂ : Temperature} (h : T₁.val = T₂.val) : T₁ = T₂ := by - cases T₁; cases T₂; cases h; rfl +/-- Extensionality lemma for `Temperature`. -/-- The inverse temperature defined as `1/(kB * T)` in a given, but arbitrary set of units. - This has dimensions equivalent to `Energy`. -/ -noncomputable def β (T : Temperature) : ℝ≥0 := - ⟨1 / (kB * (T : ℝ)), by - apply div_nonneg - · exact zero_le_one - · apply mul_nonneg - · exact kB_nonneg - · simp [toReal]⟩ - -/-- The temperature associated with a given inverse temperature `β`. -/ -noncomputable def ofβ (β : ℝ≥0) : Temperature := - ⟨⟨1 / (kB * β), by - apply div_nonneg - · exact zero_le_one - · apply mul_nonneg - · exact kB_nonneg - · exact β.2⟩⟩ - -lemma ofβ_eq : ofβ = fun β => ⟨⟨1 / (kB * β), by - apply div_nonneg - · exact zero_le_one - · apply mul_nonneg - · exact kB_nonneg - · exact β.2⟩⟩ := by +Two `Temperature` instances are equal if their underlying `val` fields are equal. +-/ +@[ext] +lemma ext {T₁ T₂ : Temperature} (h_eq : T₁.val = T₂.val) : T₁ = T₂ := by + cases T₁ with + | mk T₁val + cases T₂ with + | mk T₂val + cases h_eq rfl +/-- Simplification lemma for `Temperature`: + +Zero is less than or equal to the real number representation of a `Temperature` in `ℝ≥0`. +-/ @[simp] -lemma β_ofβ (β' : ℝ≥0) : β (ofβ β') = β' := by - ext - simp [β, ofβ, toReal] - field_simp [kB_ne_zero] +lemma zero_le_nnreal (T : Temperature) : 0 ≤ (T : ℝ≥0) := by + exact T.val.property + +/-- Simplification lemma for `Temperature`: + +The real number representation of a `Temperature` is greater or equal to zero in `ℝ≥0`. +-/ +@[to_dual existing zero_le_nnreal] +lemma nnreal_ge_zero (T : Temperature) : (T : ℝ≥0) ≥ 0 := by + exact zero_le_nnreal T +/-- Simplification lemma for `Temperature`: + +Zero is less than or equal to the real number representation of a `Temperature` in `ℝ`. +-/ @[simp] -lemma ofβ_β (T : Temperature) : ofβ (β T) = T := by - ext - change ((1 : ℝ) / (kB * ((β T : ℝ)))) = (T : ℝ) - have : (β T : ℝ) = (1 : ℝ) / (kB * (T : ℝ)) := rfl - simpa [this] using - show (1 / (kB * (1 / (kB * (T : ℝ))))) = (T : ℝ) from by - field_simp [kB_ne_zero] - -/-- Positivity of `β` from positivity of temperature. -/ -lemma beta_pos (T : Temperature) (hT_pos : 0 < T.val) : 0 < (T.β : ℝ) := by - unfold Temperature.β - have h_prod : 0 < (kB : ℝ) * T.val := mul_pos kB_pos hT_pos - simpa [Temperature.β] using inv_pos.mpr h_prod - -/-! ### Regularity of `ofβ` -/ - -open Filter Topology - -lemma ofβ_continuousOn : ContinuousOn (ofβ : ℝ≥0 → Temperature) (Set.Ioi 0) := by - rw [ofβ_eq] - refine continuousOn_of_forall_continuousAt ?_ - intro x hx - have h1 : ContinuousAt (fun t : ℝ => 1 / (kB * t)) x.1 := by - refine ContinuousAt.div₀ ?_ ?_ ?_ - · fun_prop - · fun_prop - · simp - constructor - · exact kB_ne_zero - · exact ne_of_gt hx - have hℝ : ContinuousAt (fun b : ℝ≥0 => (1 : ℝ) / (kB * (b : ℝ))) x := - h1.comp (continuous_subtype_val.continuousAt) - have hNN : - ContinuousAt (fun b : ℝ≥0 => - (⟨(1 : ℝ) / (kB * (b : ℝ)), - by - have hb : 0 ≤ kB * (b : ℝ) := - mul_nonneg kB_nonneg (by exact_mod_cast (show 0 ≤ b from b.2)) - exact div_nonneg zero_le_one hb⟩ : ℝ≥0)) x := - hℝ.codRestrict (fun b => by - have hb : 0 ≤ kB * (b : ℝ) := - mul_nonneg kB_nonneg (by exact_mod_cast (show 0 ≤ b from b.2)) - exact div_nonneg zero_le_one hb) - have hind : Topology.IsInducing (fun T : Temperature => (T.val : ℝ≥0)) := ⟨rfl⟩ - have : Tendsto (fun b : ℝ≥0 => ofβ b) (𝓝 x) (𝓝 (ofβ x)) := by - simp [hind.nhds_eq_comap, ofβ_eq] - simp_all only [Set.mem_Ioi, one_div, mul_inv_rev, val_eq_coe] - exact hNN - exact this - -lemma ofβ_differentiableOn : - DifferentiableOn ℝ (fun (x : ℝ) => ((ofβ (Real.toNNReal x)).val : ℝ)) (Set.Ioi 0) := by - refine DifferentiableOn.congr (f := fun x => 1 / (kB * x)) ?_ ?_ - · refine DifferentiableOn.fun_div ?_ ?_ ?_ - · fun_prop - · fun_prop - · intro x hx - have hx0 : x ≠ 0 := ne_of_gt (by simpa using hx) - simp [mul_eq_zero, kB_ne_zero, hx0] - · intro x hx - simp at hx - have hx' : 0 < x := by simpa using hx - simp [ofβ_eq, hx'.le, Real.toNNReal, NNReal.coe_mk] - -/-! ### Convergence -/ - -open Filter Topology - -/-- Eventually, `ofβ β` is positive as β → ∞`. -/ -lemma eventually_pos_ofβ : ∀ᶠ b : ℝ≥0 in atTop, ((Temperature.ofβ b : Temperature) : ℝ) > 0 := by - have hge : ∀ᶠ b : ℝ≥0 in atTop, (1 : ℝ≥0) ≤ b := Filter.eventually_ge_atTop 1 - refine hge.mono ?_ - intro b hb - have hbpos : 0 < (b : ℝ) := (zero_lt_one.trans_le hb) - have hden : 0 < kB * (b : ℝ) := mul_pos kB_pos hbpos - have : 0 < (1 : ℝ) / (kB * (b : ℝ)) := one_div_pos.mpr hden - simpa [Temperature.ofβ, one_div, Temperature.toReal] using this - -/-- General helper: for any `a > 0`, we have `1 / (a * b) → 0` as `b → ∞` in `ℝ≥0`. -/ -private lemma tendsto_const_inv_mul_atTop (a : ℝ) (ha : 0 < a) : - Tendsto (fun b : ℝ≥0 => (1 : ℝ) / (a * (b : ℝ))) atTop (𝓝 (0 : ℝ)) := by - refine Metric.tendsto_nhds.2 ?_ - intro ε hε - have hεpos : 0 < ε := hε - let Breal : ℝ := (1 / (a * ε)) + 1 - have hBpos : 0 < Breal := by - have : 0 < (1 / (a * ε)) := by - have : 0 < a * ε := mul_pos ha hεpos - exact one_div_pos.mpr this - linarith - let B : ℝ≥0 := ⟨Breal, le_of_lt hBpos⟩ - have h_ev : ∀ᶠ b : ℝ≥0 in atTop, b ≥ B := Filter.eventually_ge_atTop B - refine h_ev.mono ?_ - intro b hb - have hBposR : 0 < (B : ℝ) := hBpos - have hbposR : 0 < (b : ℝ) := by - have hBB : (B : ℝ) ≤ (b : ℝ) := by exact_mod_cast hb - exact lt_of_lt_of_le hBposR hBB - have hb0 : 0 < (a * (b : ℝ)) := mul_pos ha hbposR - have hB0 : 0 < (a * (B : ℝ)) := mul_pos ha hBposR - have hmono : (1 : ℝ) / (a * (b : ℝ)) ≤ (1 : ℝ) / (a * (B : ℝ)) := by - have hBB : (B : ℝ) ≤ (b : ℝ) := by exact_mod_cast hb - have hden_le : (a * (B : ℝ)) ≤ (a * (b : ℝ)) := - mul_le_mul_of_nonneg_left hBB (le_of_lt ha) - simpa [one_div] using one_div_le_one_div_of_le hB0 hden_le - have hB_gt_base : (1 / (a * ε)) < (B : ℝ) := by - simp [B, Breal] - have hden_gt : (1 / ε) < (a * (B : ℝ)) := by - have h' := mul_lt_mul_of_pos_left hB_gt_base ha - have hane : a ≠ 0 := ne_of_gt ha - have hx' : a * (ε⁻¹ * a⁻¹) = (1 / ε) := by - have : a * (ε⁻¹ * a⁻¹) = ε⁻¹ := by - simp [mul_comm, hane] - simpa [one_div] using this - simpa [hx'] using h' - have hpos : 0 < (1 / ε) := by simpa [one_div] using inv_pos.mpr hεpos - have hBbound : (1 : ℝ) / (a * (B : ℝ)) < ε := by - have := one_div_lt_one_div_of_lt hpos hden_gt - simpa [one_div, inv_div] using this - set A : ℝ := (1 : ℝ) / (a * (b : ℝ)) with hA - have hA_nonneg : 0 ≤ A := by - have : 0 ≤ a * (b : ℝ) := - mul_nonneg (le_of_lt ha) (by exact_mod_cast (show 0 ≤ b from b.2)) - simpa [hA] using div_nonneg zero_le_one this - have hxlt : A < ε := by - have := lt_of_le_of_lt hmono hBbound - simpa [hA] using this - have hAbs : |A| < ε := by - simpa [abs_of_nonneg hA_nonneg] using hxlt - have hAbs' : |A - 0| < ε := by simpa [sub_zero] using hAbs - have hdist : dist A 0 < ε := by simpa [Real.dist_eq] using hAbs' - simpa [Real.dist_eq, hA, one_div, mul_comm, mul_left_comm, mul_assoc] using hdist - -/-- Core convergence: as β → ∞, `toReal (ofβ β) → 0` in `ℝ`. -/ -lemma tendsto_toReal_ofβ_atTop : - Tendsto (fun b : ℝ≥0 => (Temperature.ofβ b : ℝ)) - atTop (𝓝 (0 : ℝ)) := by - have hform : - (fun b : ℝ≥0 => (Temperature.ofβ b : ℝ)) - = (fun b : ℝ≥0 => (1 : ℝ) / (kB * (b : ℝ))) := by - funext b; simp [Temperature.ofβ, Temperature.toReal] - have hsrc : - Tendsto (fun b : ℝ≥0 => (1 : ℝ) / (kB * (b : ℝ))) atTop (𝓝 (0 : ℝ)) := - tendsto_const_inv_mul_atTop kB kB_pos - simpa [hform] using hsrc - -/-- As β → ∞, T = ofβ β → 0+ in ℝ (within Ioi 0). -/ -lemma tendsto_ofβ_atTop : - Tendsto (fun b : ℝ≥0 => (Temperature.ofβ b : ℝ)) - atTop (nhdsWithin 0 (Set.Ioi 0)) := by - have h_to0 := tendsto_toReal_ofβ_atTop - have h_into : - Tendsto (fun b : ℝ≥0 => (Temperature.ofβ b : ℝ)) atTop (𝓟 (Set.Ioi (0 : ℝ))) := - tendsto_principal.2 (by simpa using Temperature.eventually_pos_ofβ) - have : Tendsto (fun b : ℝ≥0 => (Temperature.ofβ b : ℝ)) - atTop ((nhds (0 : ℝ)) ⊓ 𝓟 (Set.Ioi (0 : ℝ))) := - tendsto_inf.2 ⟨h_to0, h_into⟩ - simpa [nhdsWithin] using this +lemma zero_le_real (T : Temperature) : 0 ≤ (T : ℝ) := by + exact zero_le_nnreal T + +/-- Simplification lemma for `Temperature`: + +The real number representation of a `Temperature` is greater or equal to zero. +-/ +@[to_dual existing zero_le_real] +lemma real_ge_zero (T : Temperature) : (T : ℝ) ≥ 0 := by + exact zero_le_real T /-! ### Conversion to and from `ℝ≥0` -/ -open Constants +/-- Simplification function for `Temperature`: + +Build a `Temperature` from a nonnegative real number. +-/ +@[simp] +def ofNNReal (t : ℝ≥0) : Temperature := + ⟨t⟩ + +/-- Simplification lemma for `Temperature`: -/-- Build a `Temperature` directly from a nonnegative real. -/ -@[simp] def ofNNReal (t : ℝ≥0) : Temperature := ⟨t⟩ +The `val` field of a temperature constructed from a nonnegative real number `t` is equal to `t`. +-/ +@[simp] +lemma ofNNReal_val (t : ℝ≥0) : (ofNNReal t).val = t := by + rfl + +/-- Simplification lemma for `Temperature`: + +Coercing a temperature constructed from a nonnegative real number `t` back to `ℝ≥0` returns `t`. +-/ +@[simp] +lemma coe_ofNNReal_coe (t : ℝ≥0) : ((ofNNReal t : Temperature) : ℝ≥0) = t := by + rfl + +/-- Simplification lemma for `Temperature`: + +Coercing a temperature constructed from a nonnegative real number `t` to `ℝ` returns `t`. +-/ +@[simp] +lemma coe_ofNNReal_real (t : ℝ≥0) : ((⟨t⟩ : Temperature) : ℝ) = t := by + rfl + +/-- Simplification function for `Temperature`: + +Build a temperature from a real number, given a proof that it is nonnegative. +-/ +@[simp] +noncomputable def ofRealNonneg (t : ℝ) (h_zero_le_t : 0 ≤ t) : Temperature := by + exact ofNNReal ⟨t, h_zero_le_t⟩ + +/-- Simplification lemma for `Temperature`: + +The `val` field of a temperature constructed from a nonnegative real number `t` +is equal to `⟨t, h_zero_le_t⟩`. +-/ +@[simp] +lemma ofRealNonneg_val {t : ℝ} (h_zero_le_t : 0 ≤ t) : + (ofRealNonneg t h_zero_le_t).val = ⟨t, h_zero_le_t⟩ := by + rfl + +/-! ### Linear order -/ +/-- `Temperature` has a linear order inherited from `ℝ≥0` via the `val` field. + +The ordering corresponds to the physical ordering of temperatures: +`T₁ ≤ T₂` if and only if `T₁.val ≤ T₂.val` in `ℝ≥0`. +-/ +noncomputable instance : LinearOrder Temperature where + le T₁ T₂ := T₁.val ≤ T₂.val + lt T₁ T₂ := T₁.val < T₂.val + le_refl T := le_refl T.val + le_trans _ _ _ h₁ h₂ := le_trans h₁ h₂ + lt_iff_le_not_ge _ _ := lt_iff_le_not_ge + le_antisymm _ _ h₁ h₂ := ext (le_antisymm h₁ h₂) + le_total T₁ T₂ := le_total T₁.val T₂.val + toDecidableLE T₁ T₂ := inferInstanceAs (Decidable (T₁.val ≤ T₂.val)) + +/-- `Temperature` has a bottom element (absolute zero). -/ +noncomputable instance : OrderBot Temperature where + bot := 0 + bot_le T := zero_le T.val + +/-- Simplification lemma for `Temperature`: + +`T₁ ≤ T₂` if and only if `T₁.val ≤ T₂.val` in `ℝ≥0`. +-/ +@[simp] +lemma le_def {T₁ T₂ : Temperature} : T₁ ≤ T₂ ↔ T₁.val ≤ T₂.val := by + exact Iff.rfl + +/-- Simplification lemma for `Temperature`: + +`T₁ < T₂` if and only if `T₁.val < T₂.val` in `ℝ≥0`. +-/ +@[simp] +lemma lt_def {T₁ T₂ : Temperature} : T₁ < T₂ ↔ T₁.val < T₂.val := by + exact Iff.rfl + +/-- Simplification lemma for `Temperature`: + +`⟨a⟩ ≤ ⟨b⟩` if and only if `a ≤ b` in `ℝ≥0`. +-/ +@[simp] +lemma mk_le_mk {a b : ℝ≥0} : Temperature.mk a ≤ Temperature.mk b ↔ a ≤ b := by + exact Iff.rfl + +/-- Simplification lemma for `Temperature`: + +`⟨a⟩ < ⟨b⟩` if and only if `a < b` in `ℝ≥0`. +-/ +@[simp] +lemma mk_lt_mk {a b : ℝ≥0} : Temperature.mk a < Temperature.mk b ↔ a < b := by + exact Iff.rfl + +/-- Simplification lemma for `Temperature`: + +Absolute zero is the minimum temperature. +-/ +@[simp] +lemma zero_le (T : Temperature) : (0 : Temperature) ≤ T := by + exact bot_le + +/-- Simplification lemma for `Temperature`: + +No temperature is strictly less than absolute zero. +-/ @[simp] -lemma ofNNReal_val (t : ℝ≥0) : (ofNNReal t).val = t := rfl +lemma not_lt_zero (T : Temperature) : ¬ T < 0 := by + exact not_lt_bot +/-- Lemma for `Temperature`: + +The coercion to `ℝ` preserves `≤`. +-/ +lemma toReal_le_toReal {T₁ T₂ : Temperature} (h_le : T₁ ≤ T₂) : (T₁ : ℝ) ≤ (T₂ : ℝ) := by + exact NNReal.coe_le_coe.mpr h_le + +/-- Lemma for `Temperature`: + +The coercion to `ℝ` preserves `<`. +-/ +lemma toReal_lt_toReal {T₁ T₂ : Temperature} (h_lt : T₁ < T₂) : (T₁ : ℝ) < (T₂ : ℝ) := by + exact NNReal.coe_lt_coe.mpr h_lt + +/-- Lemma for `Temperature`: + +If the coercion to `ℝ` satisfies `≤`, then the temperatures satisfy `≤`. +-/ +lemma le_of_toReal_le {T₁ T₂ : Temperature} (h_le : (T₁ : ℝ) ≤ (T₂ : ℝ)) : T₁ ≤ T₂ := by + exact NNReal.coe_le_coe.mp h_le + +/-- Lemma for `Temperature`: + +If the coercion to `ℝ` satisfies `<`, then the temperatures satisfy `<`. +-/ +lemma lt_of_toReal_lt {T₁ T₂ : Temperature} (h_lt : (T₁ : ℝ) < (T₂ : ℝ)) : T₁ < T₂ := by + exact NNReal.coe_lt_coe.mp h_lt + +/-- Simplification lemma for `Temperature`: + +`ofNNReal` preserves `≤`. +-/ @[simp] -lemma coe_ofNNReal_coe (t : ℝ≥0) : ((ofNNReal t : Temperature) : ℝ≥0) = t := rfl +lemma ofNNReal_le_ofNNReal {a b : ℝ≥0} : ofNNReal a ≤ ofNNReal b ↔ a ≤ b := by + exact Iff.rfl + +/-- Simplification lemma for `Temperature`: +`ofNNReal` preserves `<`. +-/ @[simp] -lemma coe_ofNNReal_real (t : ℝ≥0) : ((⟨t⟩ : Temperature) : ℝ) = t := rfl +lemma ofNNReal_lt_ofNNReal {a b : ℝ≥0} : ofNNReal a < ofNNReal b ↔ a < b := by + exact Iff.rfl + +/-- Simplification lemma for `Temperature`: -/-- Convenience: build a temperature from a real together with a proof of nonnegativity. -/ +The `val` of `min T₁ T₂` is `min T₁.val T₂.val`. +-/ @[simp] -noncomputable def ofRealNonneg (t : ℝ) (ht : 0 ≤ t) : Temperature := - ofNNReal ⟨t, ht⟩ +lemma val_min (T₁ T₂ : Temperature) : (min T₁ T₂).val = min T₁.val T₂.val := by + simp only [min_def, le_def] + split <;> rfl +/-- Simplification lemma for `Temperature`: + +The `val` of `max T₁ T₂` is `max T₁.val T₂.val`. +-/ @[simp] -lemma ofRealNonneg_val {t : ℝ} (ht : 0 ≤ t) : - (ofRealNonneg t ht).val = ⟨t, ht⟩ := rfl - -/-! ### Calculus relating T and β -/ - -open Set -open scoped ENNReal - -/-- Map a real `t` to the inverse temperature `β` corresponding to the temperature `Real.toNNReal t` -(`max t 0`), returned as a real number. -/ -noncomputable def betaFromReal (t : ℝ) : ℝ := - ((Temperature.ofNNReal (Real.toNNReal t)).β : ℝ) - -/-- Explicit closed-form for `Beta_fun_T t` when `t > 0`. -/ -lemma beta_fun_T_formula (t : ℝ) (ht : 0 < t) : - betaFromReal t = 1 / (kB * t) := by - have ht0 : (0 : ℝ) ≤ t := ht.le - have : ((Temperature.ofNNReal (Real.toNNReal t)).β : ℝ) = 1 / (kB * t) := by - simp [Temperature.β, Temperature.ofNNReal, Temperature.toReal, - Real.toNNReal_of_nonneg ht0, one_div, mul_comm] - simpa [betaFromReal] using this - -/-- On `Ioi 0`, `Beta_fun_T t` equals `1 / (kB * t)`. -/ -lemma beta_fun_T_eq_on_Ioi : - EqOn betaFromReal (fun t : ℝ => 1 / (kB * t)) (Set.Ioi 0) := by - intro t ht - exact beta_fun_T_formula t ht - -lemma deriv_beta_wrt_T (T : Temperature) (hT_pos : 0 < T.val) : - HasDerivWithinAt betaFromReal (-1 / (kB * (T.val : ℝ)^2)) (Set.Ioi 0) (T.val : ℝ) := by - let f : ℝ → ℝ := fun t => 1 / (kB * t) - have h_eq : EqOn betaFromReal f (Set.Ioi 0) := beta_fun_T_eq_on_Ioi - have hTne : (T.val : ℝ) ≠ 0 := ne_of_gt hT_pos - have hf_def : f = fun t : ℝ => (kB)⁻¹ * t⁻¹ := by - funext t - by_cases ht : t = 0 - · simp [f, ht] - · simp [f, one_div, *] at * - ring - have h_inv : - HasDerivAt (fun t : ℝ => t⁻¹) - (-((T.val : ℝ) ^ 2)⁻¹) (T.val : ℝ) := by - simpa using (hasDerivAt_inv (x := (T.val : ℝ)) hTne) - have h_deriv_aux : - HasDerivAt (fun t : ℝ => (kB)⁻¹ * t⁻¹) - ((kB)⁻¹ * (-((T.val : ℝ) ^ 2)⁻¹)) (T.val : ℝ) := - h_inv.const_mul ((kB)⁻¹) - have h_pow_simp : - (kB)⁻¹ * (-((T.val : ℝ) ^ 2)⁻¹) = -1 / (kB * (T.val : ℝ)^2) := by - calc - (kB)⁻¹ * (-((T.val : ℝ) ^ 2)⁻¹) - = -((kB)⁻¹ * ((T.val : ℝ) ^ 2)⁻¹) := by - ring - _ = -(1 / kB * (1 / (T.val : ℝ) ^ 2)) := by - simp [one_div] - _ = -1 / (kB * (T.val : ℝ) ^ 2) := by - rw [one_div] - field_simp [pow_two, mul_comm, mul_left_comm, mul_assoc, kB_ne_zero, hTne] - have h_deriv_f : - HasDerivAt f (-1 / (kB * (T.val : ℝ)^2)) (T.val : ℝ) := by - simpa [hf_def, h_pow_simp] using h_deriv_aux - have h_mem : (T.val : ℝ) ∈ Set.Ioi (0 : ℝ) := hT_pos - exact (h_deriv_f.hasDerivWithinAt).congr h_eq (h_eq h_mem) - -/-- Chain rule for β(T) : d/dT F(β(T)) = F'(β(T)) * (-1 / (kB * T^2)), within `Ioi 0`. -/ -lemma chain_rule_T_beta {F : ℝ → ℝ} {F' : ℝ} - (T : Temperature) (hT_pos : 0 < T.val) - (hF_deriv : HasDerivWithinAt F F' (Set.Ioi 0) (T.β : ℝ)) : - HasDerivWithinAt (fun t : ℝ => F (betaFromReal t)) - (F' * (-1 / (kB * (T.val : ℝ)^2))) (Set.Ioi 0) (T.val : ℝ) := by - have hβ_deriv := deriv_beta_wrt_T (T:=T) hT_pos - have h_map : Set.MapsTo betaFromReal (Set.Ioi 0) (Set.Ioi 0) := by - intro t ht - have ht_pos : 0 < t := ht - have : 0 < 1 / (kB * t) := by - have : 0 < kB * t := mul_pos kB_pos ht_pos - exact one_div_pos.mpr this - have h_eqt : betaFromReal t = 1 / (kB * t) := beta_fun_T_eq_on_Ioi ht - simpa [h_eqt] using this - have h_beta_at_T : betaFromReal (T.val : ℝ) = (T.β : ℝ) := by - have hTposR : 0 < (T.val : ℝ) := hT_pos - have h_eqt := beta_fun_T_eq_on_Ioi hTposR - simpa [Temperature.β, Temperature.toReal] using h_eqt - have hF_deriv' : HasDerivWithinAt F F' (Set.Ioi 0) (betaFromReal (T.val : ℝ)) := by - simpa [h_beta_at_T] using hF_deriv - have h_comp := hF_deriv'.comp (T.val : ℝ) hβ_deriv h_map - simpa [mul_comm] using h_comp +lemma val_max (T₁ T₂ : Temperature) : (max T₁ T₂).val = max T₁.val T₂.val := by + simp only [max_def, le_def] + split <;> rfl end Temperature + +/-! +## Basic instances and definitions for `PositiveTemperature` +-/ +namespace PositiveTemperature +open Constants + +/-- Type coercion (implicit casting) from `PositiveTemperature` to `Temperature`. + +Defined as a function that takes a `PositiveTemperature` and returns the underlying `Temperature`. +-/ +instance : Coe PositiveTemperature Temperature := ⟨fun (T : PositiveTemperature) => T.1⟩ + +/-- Type coercion (implicit casting) from `PositiveTemperature` to `ℝ≥0`. + +Defined as a function that takes a `PositiveTemperature` and returns the underlying `ℝ≥0` value. +-/ +instance : Coe PositiveTemperature ℝ≥0 := ⟨fun (T : PositiveTemperature) => T.1.val⟩ + +/-- Type coercion (implicit casting) from `PositiveTemperature` to `ℝ>0`. + +Defined as a function that takes a `PositiveTemperature` and returns the underlying `ℝ>0` value, +which is the `val` field of the underlying `Temperature` along with the proof that +it is strictly positive. +-/ +instance : Coe PositiveTemperature ℝ>0 := ⟨fun (T : PositiveTemperature) => ⟨T.1.val, T.2⟩⟩ + +/-- Function for `PositiveTemperature`: + +Convert a `PositiveTemperature` to a real number in `ℝ`. +-/ +def toReal (T : PositiveTemperature) : ℝ := Temperature.toReal T.1 + +/-- Type coercion (implicit casting) from `PositiveTemperature` to `ℝ`. + +Defined as a function that takes a `PositiveTemperature` and returns the value converted to `ℝ`. +-/ +instance : Coe PositiveTemperature ℝ := ⟨fun (T : PositiveTemperature) => T.toReal⟩ + +/-- Topology on `PositiveTemperature` induced as a subtype of `Temperature`. -/ +instance : TopologicalSpace PositiveTemperature := instTopologicalSpaceSubtype + +/-- Extensionality lemma for `PositiveTemperature`. + +Two `PositiveTemperature` instances are equal if their underlying `Temperature` values are equal. +-/ +@[ext] +lemma ext {T₁ T₂ : PositiveTemperature} (h : T₁.1 = T₂.1) : T₁ = T₂ := by + exact Subtype.ext h + +/-- Simplification lemma for `PositiveTemperature`: + +The `val` field (of type `ℝ≥0`) of the underlying `Temperature` is strictly positive. +-/ +@[simp] +lemma val_pos (T : PositiveTemperature) : 0 < T.1.val := by + exact T.2 + +/-- Simplification lemma for `PositiveTemperature`: + +The real number representation of a `PositiveTemperature` is strictly positive. +-/ +@[simp] +lemma zero_lt_toReal (T : PositiveTemperature) : 0 < (T : ℝ) := by + exact T.2 + +/-- Function for `PositiveTemperature`: + +Calculate the inverse temperature `β` corresponding to a given positive 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. +-/ +noncomputable def β (T : PositiveTemperature) : ℝ>0 := + ⟨1 / (kB * (T : ℝ)), by + apply div_pos + · exact one_pos + · apply mul_pos + · exact kB_pos + · exact zero_lt_toReal T⟩ + +/-- Simplification lemma for `PositiveTemperature`: + +The definition of `β T` unfolds to its explicit formula in terms of `kB` and `T`. +-/ +@[simp] +lemma β_eq (T : PositiveTemperature) : β T = + ⟨1 / (kB * (T : ℝ)), by + apply div_pos + · exact one_pos + · apply mul_pos + · exact kB_pos + · exact zero_lt_toReal T⟩ := by + rfl + +/-- Simplification lemma for `PositiveTemperature`: + +Coercing `β T` from `ℝ≥0` to `ℝ` gives the explicit formula `1 / (kB * (T : ℝ))`. +-/ +@[simp] +lemma β_toReal (T : PositiveTemperature) : (β T : ℝ) = (1 : ℝ) / (kB * (T : ℝ)) := by + rfl + +/-- Lemma for `PositiveTemperature`: + +The inverse temperature `β` is strictly positive for positive temperatures. +-/ +lemma β_pos (T : PositiveTemperature) : 0 < (T.β : ℝ) := by + exact (β T).2 + +/-- Function for `PositiveTemperature`: + +Construct a `PositiveTemperature` from a positive inverse temperature `β`. +-/ +noncomputable def ofβ (β : ℝ>0): PositiveTemperature := + ⟨⟨⟨1 / (kB * β), by + apply div_nonneg + · exact zero_le_one + · apply mul_nonneg + · exact kB_nonneg + · exact le_of_lt β.property⟩⟩, + by + exact div_pos one_pos (mul_pos kB_pos β.property)⟩ + +/-- Simplification lemma for `PositiveTemperature`: + +Applying `β` to the temperature constructed from `β'` returns `β'`. +-/ +@[simp] +lemma β_ofβ (β' : ℝ>0) : β (ofβ β') = β' := by + ext + simp only [PositiveTemperature.β, PositiveTemperature.ofβ, PositiveTemperature.toReal, + Temperature.toReal] + simp only [NNReal.coe_mk] + field_simp [kB_ne_zero] + +/-- Simplification lemma for `PositiveTemperature`: + +Rebuilding a positive temperature `T` from its inverse temperature `β` gives back the original. +-/ +@[simp] +lemma ofβ_β (T : PositiveTemperature) : ofβ (β T) = T := by + ext + simp [β, ofβ, Temperature.toReal, PositiveTemperature.toReal] + field_simp [kB_ne_zero] + +/-- The thermodynamic equivalence between positive temperature and positive inverse temperature. +-/ +noncomputable def equiv_β : PositiveTemperature ≃ ℝ>0 where + toFun := β + invFun := ofβ + left_inv := ofβ_β + right_inv := β_ofβ + +end PositiveTemperature diff --git a/PhysLean/Thermodynamics/Temperature/Calculus.lean b/PhysLean/Thermodynamics/Temperature/Calculus.lean new file mode 100644 index 000000000..62766b629 --- /dev/null +++ b/PhysLean/Thermodynamics/Temperature/Calculus.lean @@ -0,0 +1,71 @@ +/- +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Trong-Nghia Be, Matteo Cipollina, Tan-Phuoc-Hung Le, Joseph Tooby-Smith +-/ +import Mathlib.Analysis.Calculus.Deriv.Inv +import PhysLean.Thermodynamics.Temperature.Basic +import PhysLean.Meta.Types.PosReal + +/-! +# Calculus relating temperature and inverse temperature + +This file establishes the derivative of `β` with respect to (positive) temperature `T`, +and provides a chain rule for composing functions of `β` with the +temperature-to-beta map, leveraging `PositiveTemperature`. + +## Main results + +* `PositiveTemperature.deriv_β_wrt_T` : The derivative of the `β` formula is `-1 / (kB * T²)`. +* `PositiveTemperature.chain_rule_T_β` : Chain rule for composing through the `β` formula. +-/ + +open NNReal + +namespace PositiveTemperature +open Constants +open Set + + +/-- Lemma for `PositiveTemperature`: + +The real-valued function mapping `t ↦ 1 / (kB * t)` has the full derivative +`-1 / (kB * T²)` at the evaluation point `(T : ℝ)`. + +Note that `t` is a positive real variable, since it represents positive temperature. +-/ +lemma deriv_β_wrt_T (T : PositiveTemperature) : HasDerivAt (fun (t : ℝ) => (1 : ℝ) / (kB * t)) + (-1 / (kB * (T : ℝ)^2)) (T : ℝ) := by + have h_T_ne_zero : (T : ℝ) ≠ 0 := by + exact ne_of_gt T.zero_lt_toReal + have h_f_def : (fun (t : ℝ) => (1 : ℝ) / (kB * t)) = fun (t : ℝ) => (kB)⁻¹ * t⁻¹ := by + simp only [one_div, mul_inv_rev] + funext T + ring + have h_t_inv_deriv : HasDerivAt (fun (t : ℝ) => t⁻¹) + (-((T : ℝ) ^ 2)⁻¹) (T : ℝ) := by + exact (hasDerivAt_inv (x := (T : ℝ)) h_T_ne_zero) + have h_deriv_aux : HasDerivAt (fun (t : ℝ) => (kB)⁻¹ * t⁻¹) + ((kB)⁻¹ * (-((T : ℝ) ^ 2)⁻¹)) (T : ℝ) := by + exact h_t_inv_deriv.const_mul ((kB)⁻¹) + rw [h_f_def] + convert h_deriv_aux using 1 + ring + +/-- Lemma for `PositiveTemperature`: + +Chain rule for `β(T)`: + +- If `F` is a real-valued function of a real variable, +and `F` has a derivative `F'` at the point `β(T)`, +then the composition function `F(β(T))` or `t ↦ F(1 / (kB * t))` has a derivative +`F' * (-1 / (kB * T²))` at the evaluation point `(T : ℝ)`. +-/ +lemma chain_rule_T_β {F : ℝ → ℝ} {F' : ℝ} (T : PositiveTemperature) + (h_F_deriv : HasDerivAt F F' (β T : ℝ)) : HasDerivAt (fun (t : ℝ) => F ((1 : ℝ) / (kB * t))) + (F' * (-1 / (kB * (T : ℝ)^2))) (T : ℝ) := by + have h_β_deriv := deriv_β_wrt_T T + have h_comp := h_F_deriv.comp (T : ℝ) h_β_deriv + convert h_comp using 1 + +end PositiveTemperature diff --git a/PhysLean/Thermodynamics/Temperature/Convergence.lean b/PhysLean/Thermodynamics/Temperature/Convergence.lean new file mode 100644 index 000000000..13b156e17 --- /dev/null +++ b/PhysLean/Thermodynamics/Temperature/Convergence.lean @@ -0,0 +1,78 @@ +/- +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Trong-Nghia Be, Matteo Cipollina, Tan-Phuoc-Hung Le, Joseph Tooby-Smith +-/ +import PhysLean.Thermodynamics.Temperature.Basic + +/-! +# Convergence of inverse temperature maps + +This file proves that as the inverse temperature `β` tends to infinity, +the temperature `ofβ β` tends to zero. + +## Main results + +* `PositiveTemperature.eventually_pos_ofβ`: `ofβ` always produces positive temperatures. +* `PositiveTemperature.tendsto_toReal_ofβ_atTop` : The real representation of `ofβ β` + tends to `0` as `β → ∞`. +* `PositiveTemperature.tendsto_ofβ_atTop` : `ofβ β` tends to `0` from above as `β → ∞`. +-/ + +open NNReal + +namespace PositiveTemperature +open Constants +open Filter Topology + +/-- Lemma for `PositiveTemperature`: + +The function `ofβ` will eventually produce positive temperatures as `β` tends to infinity in `ℝ>0`. +-/ +lemma eventually_pos_ofβ : ∀ᶠ (β : ℝ>0) in atTop, (PositiveTemperature.ofβ β : ℝ) > 0 := by + filter_upwards [] with β + exact PositiveTemperature.zero_lt_toReal _ + +/-- Helper lemma for `PositiveTemperature`: + +As `b` tends to infinity in `ℝ>0`, the function value `1 / (a * b)` tends to `0`. +-/ +private lemma tendsto_const_inv_mul_atTop (a : ℝ) (h_a_pos : 0 < a) : + Tendsto (fun (b : ℝ>0) => (1 : ℝ) / (a * (b : ℝ))) atTop (𝓝 (0 : ℝ)) := by + have h_val_atTop : Tendsto (Subtype.val : ℝ>0 → ℝ) atTop atTop := + Filter.tendsto_atTop_atTop_of_monotone (fun a b h => h) + (fun b => ⟨⟨max b 1, lt_max_of_lt_right one_pos⟩, le_max_left _ _⟩) + simp_rw [one_div] + exact (Filter.Tendsto.const_mul_atTop h_a_pos h_val_atTop).inv_tendsto_atTop + +/-- Lemma for `PositiveTemperature`: + +As the inverse temperature `β` tends to infinity, +the real-valued representation of the temperature `ofβ β` tends to `0` +in the sense of the metric space distance. +-/ +lemma tendsto_toReal_ofβ_atTop : + Tendsto (fun (β : ℝ>0) => (PositiveTemperature.ofβ β : ℝ)) atTop (𝓝 (0 : ℝ)) := by + exact tendsto_const_inv_mul_atTop kB kB_pos + +/-- Lemma for `PositiveTemperature`: + +As the inverse temperature `β` tends to infinity, +the real-valued representation of the temperature `ofβ β` +tends to `0` from above (within the interval `(0, ∞)`). +-/ +lemma tendsto_ofβ_atTop : Tendsto (fun (β : ℝ>0) => (PositiveTemperature.ofβ β : ℝ)) + atTop (nhdsWithin 0 (Set.Ioi 0)) := by + have h_tendsto_nhds_zero := tendsto_toReal_ofβ_atTop + have h_tendsto_principal_Ioi : Tendsto (fun (β : ℝ>0) => (PositiveTemperature.ofβ β : ℝ)) + atTop (𝓟 (Set.Ioi (0 : ℝ))) := tendsto_principal.mpr eventually_pos_ofβ + have h_tendsto_inf : + Tendsto (fun (β : ℝ>0) => + (PositiveTemperature.ofβ β : ℝ)) + atTop + ((nhds (0 : ℝ)) ⊓ 𝓟 (Set.Ioi (0 : ℝ))) := + tendsto_inf.mpr + ⟨h_tendsto_nhds_zero, h_tendsto_principal_Ioi⟩ + simpa [nhdsWithin] using h_tendsto_inf + +end PositiveTemperature diff --git a/PhysLean/Thermodynamics/Temperature/Regularity.lean b/PhysLean/Thermodynamics/Temperature/Regularity.lean new file mode 100644 index 000000000..0e34853fc --- /dev/null +++ b/PhysLean/Thermodynamics/Temperature/Regularity.lean @@ -0,0 +1,50 @@ +/- +Copyright (c) 2026 Joseph Tooby-Smith. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Trong-Nghia Be, Matteo Cipollina, Tan-Phuoc-Hung Le, Joseph Tooby-Smith +-/ +import Mathlib.Analysis.Calculus.Deriv.Inv +import PhysLean.Thermodynamics.Temperature.Basic + +/-! +# Regularity of the inverse temperature map + +This file proves continuity and differentiability properties of +`PositiveTemperature.ofβ : ℝ>0 → PositiveTemperature`. + +## Main results + +* `PositiveTemperature.ofβ_continuous` : `ofβ` is continuous. +* `PositiveTemperature.ofβ_differentiableOn` : the real-valued formula underlying `ofβ` is + differentiable on `(0, ∞)`. +-/ + +open NNReal + +namespace PositiveTemperature +open Constants + +/-! ### Regularity of `ofβ` -/ + +/-- The function `ofβ` is continuous. -/ +lemma ofβ_continuous : Continuous ofβ := by + have h_ind : Topology.IsInducing (fun (T : PositiveTemperature) => (T : ℝ)) := + Topology.IsInducing.subtypeVal.comp + ((show Topology.IsInducing (fun (T : Temperature) => T.val) from ⟨rfl⟩).comp + Topology.IsInducing.subtypeVal) + apply h_ind.continuous_iff.mpr + simp only [PositiveTemperature.toReal, Temperature.toReal] + exact continuous_const.div₀ (continuous_const.mul continuous_subtype_val) + (fun (β : ℝ>0) => mul_ne_zero kB_ne_zero (ne_of_gt β.2)) + +/-- The real-valued formula underlying `ofβ` is differentiable on `(0, ∞)`. +-/ +lemma ofβ_differentiableOn : + DifferentiableOn ℝ (fun (β : ℝ) => (1 : ℝ) / (kB * β)) (Set.Ioi 0) := by + apply DifferentiableOn.fun_div + · fun_prop + · fun_prop + · intro x hx + exact mul_ne_zero kB_ne_zero (Set.mem_Ioi.mp hx).ne' + +end PositiveTemperature diff --git a/PhysLean/Thermodynamics/Temperature/TemperatureScales.lean b/PhysLean/Thermodynamics/Temperature/TemperatureScales.lean new file mode 100644 index 000000000..fefe15237 --- /dev/null +++ b/PhysLean/Thermodynamics/Temperature/TemperatureScales.lean @@ -0,0 +1,521 @@ +/- +Copyright (c) 2026 Trong-Nghia Be. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Authors: Trong-Nghia Be, Tan-Phuoc-Hung Le +-/ +import PhysLean.Thermodynamics.Temperature.Basic +import PhysLean.Thermodynamics.Temperature.TemperatureUnits +/-! +# Affine temperature scales === TODO TIL THE END OF THE FILE + +`Temperature` stores absolute temperature in kelvin (`ℝ≥0`), which +is the physically meaningful quantity used by thermodynamics and +statistical mechanics. + +This file introduces affine display scales (such as Celsius and +Fahrenheit), where the reading is allowed to be negative while the +corresponding absolute temperature remains nonnegative. +-/ + +open NNReal + +/-- The type `TemperatureScale` represents an affine temperature + scale, such as Celsius or Fahrenheit. + - `unit` of type `TemperatureUnit`: The size of one degree on + this scale as a multiplicative temperature interval. + - `absoluteZero` of type `ℝ`: The reading on this scale + corresponding to `0 K`. For example, on the Celsius scale this + is `-273.15`. +-/ +structure TemperatureScale where + /-- The multiplicative interval unit for one degree on this + scale. -/ + unit : TemperatureUnit + /-- The reading corresponding to absolute zero (`0 K`). -/ + absoluteZero : ℝ + +namespace TemperatureScale + +/-- Function for `TemperatureScale`: + +Convert a reading in an affine temperature scale into kelvin as a +real number. +-/ +noncomputable def toKelvinReal + (s : TemperatureScale) (reading : ℝ) : ℝ := + (reading - s.absoluteZero) * + (s.unit / TemperatureUnit.kelvin : ℝ) + +/-- Function for `TemperatureScale`: + +Convert a kelvin value into a reading in an affine temperature scale +as a real number. +-/ +noncomputable def fromKelvinReal + (s : TemperatureScale) (k : ℝ) : ℝ := + s.absoluteZero + + k * (TemperatureUnit.kelvin / s.unit : ℝ) + +/-- Lemma for `TemperatureScale`: + +Converting to kelvin and back to the affine scale is the identity. +-/ +lemma fromKelvinReal_toKelvinReal + (s : TemperatureScale) (reading : ℝ) : + fromKelvinReal s (toKelvinReal s reading) = + reading := by + -- We unfold the definitions of `fromKelvinReal` and + -- `toKelvinReal` to expose the underlying expressions. + unfold fromKelvinReal toKelvinReal + -- We derive `hmul` which states that the product of the + -- unit ratio and its inverse equals `1`, using the chain + -- rule for division `div_mul_div_coe`. + have hmul : + (s.unit / TemperatureUnit.kelvin : ℝ) * + (TemperatureUnit.kelvin / s.unit : ℝ) = 1 := by + calc + (s.unit / TemperatureUnit.kelvin : ℝ) * + (TemperatureUnit.kelvin / s.unit : ℝ) + = (s.unit / s.unit : ℝ) := + TemperatureUnit.div_mul_div_coe + s.unit TemperatureUnit.kelvin s.unit + _ = 1 := by simp + -- We conclude by algebraic simplification using `hmul` + -- to replace the product of ratios with `1`. QED. + calc + s.absoluteZero + + ((reading - s.absoluteZero) * + (s.unit / TemperatureUnit.kelvin : ℝ)) * + (TemperatureUnit.kelvin / s.unit : ℝ) + = s.absoluteZero + + (reading - s.absoluteZero) * + ((s.unit / TemperatureUnit.kelvin : ℝ) * + (TemperatureUnit.kelvin / s.unit : ℝ)) := + by ring + _ = s.absoluteZero + + (reading - s.absoluteZero) * 1 := by + rw [hmul] + _ = reading := by ring + +/-- Lemma for `TemperatureScale`: + +Converting from kelvin to the affine scale and back to kelvin is the +identity. +-/ +lemma toKelvinReal_fromKelvinReal + (s : TemperatureScale) (k : ℝ) : + toKelvinReal s (fromKelvinReal s k) = k := by + -- We unfold the definitions of `fromKelvinReal` and + -- `toKelvinReal` to expose the underlying expressions. + unfold fromKelvinReal toKelvinReal + -- We derive `hmul` which states that the product of the + -- unit ratio and its inverse equals `1`, using the chain + -- rule for division `div_mul_div_coe`. + have hmul : + (TemperatureUnit.kelvin / s.unit : ℝ) * + (s.unit / TemperatureUnit.kelvin : ℝ) = 1 := by + calc + (TemperatureUnit.kelvin / s.unit : ℝ) * + (s.unit / TemperatureUnit.kelvin : ℝ) + = (TemperatureUnit.kelvin / + TemperatureUnit.kelvin : ℝ) := + TemperatureUnit.div_mul_div_coe + TemperatureUnit.kelvin s.unit + TemperatureUnit.kelvin + _ = 1 := by simp + -- We conclude by algebraic simplification using `hmul` + -- to replace the product of ratios with `1`. QED. + calc + (s.absoluteZero + + k * (TemperatureUnit.kelvin / s.unit : ℝ) - + s.absoluteZero) * + (s.unit / TemperatureUnit.kelvin : ℝ) + = (k * + (TemperatureUnit.kelvin / s.unit : ℝ)) * + (s.unit / TemperatureUnit.kelvin : ℝ) := + by ring + _ = k * + ((TemperatureUnit.kelvin / s.unit : ℝ) * + (s.unit / TemperatureUnit.kelvin : ℝ)) := + by ring + _ = k * 1 := by rw [hmul] + _ = k := by ring + +/-- Function for `TemperatureScale`: + +The kelvin scale, with unit size equal to one kelvin and zero +offset. +-/ +def kelvin : TemperatureScale := + ⟨TemperatureUnit.kelvin, 0⟩ + +/-- Function for `TemperatureScale`: + +The Celsius scale, with unit size equal to one kelvin and absolute +zero at `-273.15`. +-/ +noncomputable def celsius : TemperatureScale := + ⟨TemperatureUnit.kelvin, -(27315 : ℝ) / 100⟩ + +/-- Function for `TemperatureScale`: + +The Rankine scale, with unit size equal to one rankine degree and +zero offset. +-/ +noncomputable def rankine : TemperatureScale := + ⟨TemperatureUnit.rankine, 0⟩ + +/-- Function for `TemperatureScale`: + +The Fahrenheit scale, with unit size equal to one rankine degree and +absolute zero at `-459.67`. +-/ +noncomputable def fahrenheit : TemperatureScale := + ⟨TemperatureUnit.rankine, -(45967 : ℝ) / 100⟩ + +/-- Simplification lemma for `TemperatureScale`: + +Converting a kelvin reading to kelvin is the identity. +-/ +@[simp] +lemma toKelvinReal_kelvin (k : ℝ) : + toKelvinReal kelvin k = k := by + -- We simplify using the definitions of `toKelvinReal` + -- and `kelvin`. QED. + simp [toKelvinReal, kelvin] + +/-- Simplification lemma for `TemperatureScale`: + +Converting a kelvin value to a kelvin reading is the identity. +-/ +@[simp] +lemma fromKelvinReal_kelvin (k : ℝ) : + fromKelvinReal kelvin k = k := by + -- We simplify using the definitions of `fromKelvinReal` + -- and `kelvin`. QED. + simp [fromKelvinReal, kelvin] + +/-- Simplification lemma for `TemperatureScale`: + +Converting a Celsius reading `c` to kelvin yields +`c + 273.15`. +-/ +@[simp] +lemma toKelvinReal_celsius (c : ℝ) : + toKelvinReal celsius c = + c + (27315 : ℝ) / 100 := by + -- We compute `toKelvinReal celsius c` step by step. + calc + toKelvinReal celsius c + = (c - (-(27315 : ℝ) / 100)) * + (TemperatureUnit.kelvin / + TemperatureUnit.kelvin : ℝ) := by + rfl + -- We simplify `kelvin / kelvin` to `1` and the + -- subtraction of a negative to addition. + _ = c - (-(27315 : ℝ) / 100) := by simp + -- We conclude by the algebraic identity + -- `c - (-273.15) = c + 273.15`. QED. + _ = c + (27315 : ℝ) / 100 := by ring + +/-- Simplification lemma for `TemperatureScale`: + +Converting a kelvin value to Celsius yields +`-273.15 + k`. +-/ +@[simp] +lemma fromKelvinReal_celsius (k : ℝ) : + fromKelvinReal celsius k = + -(27315 : ℝ) / 100 + k := by + -- We simplify using the definitions of `fromKelvinReal`, + -- `celsius`, and commutativity of addition. QED. + simp [fromKelvinReal, celsius, add_comm] + +/-- Simplification lemma for `TemperatureScale`: + +Converting a Fahrenheit reading `f` to kelvin yields +`(f + 459.67) * (5 / 9)`. +-/ +@[simp] +lemma toKelvinReal_fahrenheit (f : ℝ) : + toKelvinReal fahrenheit f = + (f + (45967 : ℝ) / 100) * (5 / 9 : ℝ) := by + -- We compute `toKelvinReal fahrenheit f` step by step. + calc + toKelvinReal fahrenheit f + = (f - (-(45967 : ℝ) / 100)) * + (TemperatureUnit.rankine / + TemperatureUnit.kelvin : ℝ) := by + rfl + -- We simplify the subtraction of a negative to + -- addition and evaluate `rankine / kelvin = 5/9`. + _ = (f + (45967 : ℝ) / 100) * + (5 / 9 : ℝ) := by + -- We derive that `f - (-459.67) = f + 459.67`. + have hneg : + f - (-(45967 : ℝ) / 100) = + f + (45967 : ℝ) / 100 := by ring + -- We rewrite using `hneg` and simplify the rankine + -- to kelvin ratio. QED. + rw [hneg] + simp [TemperatureUnit.rankine, + TemperatureUnit.scale_div_self] + +/-- Simplification lemma for `TemperatureScale`: + +Converting a kelvin value to Fahrenheit yields +`-459.67 + k * (9 / 5)`. +-/ +@[simp] +lemma fromKelvinReal_fahrenheit (k : ℝ) : + fromKelvinReal fahrenheit k = + -(45967 : ℝ) / 100 + k * (9 / 5 : ℝ) := by + -- We simplify using the definitions of `fromKelvinReal`, + -- `fahrenheit`, `rankine`, `self_div_scale`, and + -- commutativity of addition. QED. + simp [fromKelvinReal, fahrenheit, + TemperatureUnit.rankine, + TemperatureUnit.self_div_scale, add_comm] + +/-- Lemma for `TemperatureScale`: + +The kelvin value of a Celsius reading is nonnegative if and only if +the reading is at or above `-273.15`. +-/ +lemma zero_le_toKelvinReal_celsius_iff (c : ℝ) : + 0 ≤ toKelvinReal celsius c ↔ + (-(27315 : ℝ) / 100) ≤ c := by + -- We rewrite the goal using `toKelvinReal_celsius` to + -- get the explicit formula. + rw [toKelvinReal_celsius] + -- We prove both directions using `linarith`. QED. + constructor <;> intro h <;> linarith + +/-- Lemma for `TemperatureScale`: + +The kelvin value of a Fahrenheit reading is nonnegative if and only +if the reading is at or above `-459.67`. +-/ +lemma zero_le_toKelvinReal_fahrenheit_iff (f : ℝ) : + 0 ≤ toKelvinReal fahrenheit f ↔ + (-(45967 : ℝ) / 100) ≤ f := by + -- We rewrite the goal using `toKelvinReal_fahrenheit` + -- to get the explicit formula. + rw [toKelvinReal_fahrenheit] + -- We prove the forward direction. + constructor + · intro h + -- We derive `h'` stating that `f + 459.67 ≥ 0` + -- from the product being nonnegative with the + -- positive factor `5/9`. + have h' : 0 ≤ f + (45967 : ℝ) / 100 := + (mul_nonneg_iff_of_pos_right + (show (0 : ℝ) < 5 / 9 by norm_num)).1 h + -- We conclude by linear arithmetic. QED for this + -- case. + linarith + -- We prove the reverse direction. + · intro h + -- We derive `h'` stating that `f + 459.67 ≥ 0` + -- from the hypothesis. + have h' : 0 ≤ f + (45967 : ℝ) / 100 := by + linarith + -- We conclude by `mul_nonneg` since both factors + -- are nonnegative. QED for this case. + -- All cases have been proven. QED. + exact mul_nonneg h' (by norm_num) + +end TemperatureScale + +namespace Temperature + +/-- Function for `Temperature`: + +Convert an absolute temperature to a reading in an affine scale. +-/ +noncomputable def toScale + (T : Temperature) (s : TemperatureScale) : ℝ := + TemperatureScale.fromKelvinReal s (T : ℝ) + +/-- Function for `Temperature`: + +Build an absolute temperature from an affine scale reading and a +proof it is physically valid. +-/ +noncomputable def ofScale (s : TemperatureScale) + (x : ℝ) + (hx : 0 ≤ TemperatureScale.toKelvinReal s x) : + Temperature := + Temperature.ofRealNonneg + (TemperatureScale.toKelvinReal s x) hx + +/-- Function for `Temperature`: + +Build an absolute temperature from an affine scale reading, +returning `none` below absolute zero. +-/ +noncomputable def ofScale? + (s : TemperatureScale) (x : ℝ) : + Option Temperature := + if hx : 0 ≤ TemperatureScale.toKelvinReal s x then + some (ofScale s x hx) + else none + +/-- Function for `Temperature`: + +Convert an absolute temperature to Celsius. +-/ +noncomputable def toCelsius (T : Temperature) : ℝ := + toScale T TemperatureScale.celsius + +/-- Function for `Temperature`: + +Convert an absolute temperature to Fahrenheit. +-/ +noncomputable def toFahrenheit + (T : Temperature) : ℝ := + toScale T TemperatureScale.fahrenheit + +/-- Function for `Temperature`: + +Build an absolute temperature from Celsius. +-/ +noncomputable def ofCelsius (c : ℝ) + (hc : (-(27315 : ℝ) / 100) ≤ c) : Temperature := + ofScale TemperatureScale.celsius c + ((TemperatureScale.zero_le_toKelvinReal_celsius_iff + c).2 hc) + +/-- Function for `Temperature`: + +Build an absolute temperature from Fahrenheit. +-/ +noncomputable def ofFahrenheit (f : ℝ) + (hf : (-(45967 : ℝ) / 100) ≤ f) : Temperature := + ofScale TemperatureScale.fahrenheit f + ((TemperatureScale.zero_le_toKelvinReal_fahrenheit_iff + f).2 hf) + +/-- Function for `Temperature`: + +Build an absolute temperature from Celsius, returning `none` below +absolute zero. +-/ +noncomputable def ofCelsius? (c : ℝ) : + Option Temperature := + ofScale? TemperatureScale.celsius c + +/-- Function for `Temperature`: + +Build an absolute temperature from Fahrenheit, returning `none` +below absolute zero. +-/ +noncomputable def ofFahrenheit? (f : ℝ) : + Option Temperature := + ofScale? TemperatureScale.fahrenheit f + +/-- Lemma for `Temperature`: + +Converting to a scale and back recovers the original reading. +-/ +lemma toScale_ofScale (s : TemperatureScale) (x : ℝ) + (hx : 0 ≤ TemperatureScale.toKelvinReal s x) : + toScale (ofScale s x hx) s = x := by + -- We simplify using the definitions of `toScale`, + -- `ofScale`, `ofRealNonneg`, `ofNNReal`, `toReal`, + -- and the round-trip lemma + -- `fromKelvinReal_toKelvinReal`. QED. + simp [toScale, ofScale, Temperature.ofRealNonneg, + Temperature.ofNNReal, Temperature.toReal, + TemperatureScale.fromKelvinReal_toKelvinReal] + +/-- Simplification lemma for `Temperature`: + +Absolute zero in Celsius is `-273.15`. +-/ +@[simp] +lemma toCelsius_zero : + toCelsius (0 : Temperature) = + (-(27315 : ℝ) / 100) := by + -- We change the goal to unfold `toCelsius` and + -- `toScale` into `fromKelvinReal` applied to `0`. + change TemperatureScale.fromKelvinReal + TemperatureScale.celsius + (((0 : Temperature).val : ℝ)) = + (-(27315 : ℝ) / 100) + -- We derive that the real value of zero temperature + -- is `0`. + have hzero : (((0 : Temperature).val : ℝ)) = 0 := + by rfl + -- We simplify using `hzero` and the definitions of + -- `fromKelvinReal` and `celsius`. QED. + simp [hzero, TemperatureScale.fromKelvinReal, + TemperatureScale.celsius] + +/-- Simplification lemma for `Temperature`: + +Absolute zero in Fahrenheit is `-459.67`. +-/ +@[simp] +lemma toFahrenheit_zero : + toFahrenheit (0 : Temperature) = + (-(45967 : ℝ) / 100) := by + -- We change the goal to unfold `toFahrenheit` and + -- `toScale` into `fromKelvinReal` applied to `0`. + change TemperatureScale.fromKelvinReal + TemperatureScale.fahrenheit + (((0 : Temperature).val : ℝ)) = + (-(45967 : ℝ) / 100) + -- We derive that the real value of zero temperature + -- is `0`. + have hzero : (((0 : Temperature).val : ℝ)) = 0 := + by rfl + -- We simplify using `hzero` and the definitions of + -- `fromKelvinReal` and `fahrenheit`. QED. + simp [hzero, TemperatureScale.fromKelvinReal, + TemperatureScale.fahrenheit] + +/-- Simplification lemma for `Temperature`: + +`ofCelsius?` returns `none` below absolute zero. +-/ +@[simp] +lemma ofCelsius?_below_absoluteZero : + ofCelsius? ((-(27315 : ℝ) / 100) - 1) = + none := by + -- We simplify using the definitions of `ofCelsius?` + -- and `ofScale?`. + simp [ofCelsius?, ofScale?] + -- We conclude by linear arithmetic, since the kelvin + -- value is negative below absolute zero. QED. + linarith + +/-- Simplification lemma for `Temperature`: + +`ofFahrenheit?` returns `none` below absolute zero. +-/ +@[simp] +lemma ofFahrenheit?_below_absoluteZero : + ofFahrenheit? ((-(45967 : ℝ) / 100) - 1) = + none := by + -- We simplify using the definitions of `ofFahrenheit?` + -- and `ofScale?`. + simp [ofFahrenheit?, ofScale?] + -- We conclude by linear arithmetic, since the kelvin + -- value is negative below absolute zero. QED. + linarith + +/-- Lemma for `Temperature`: + +`-40` degrees Celsius equals `-40` degrees Fahrenheit. +-/ +lemma minusForty_celsius_eq_minusForty_fahrenheit : + toFahrenheit (ofCelsius (-40) (by norm_num)) = + (-40 : ℝ) := by + -- We simplify using the definitions of `toFahrenheit`, + -- `toScale`, `ofCelsius`, and `ofScale`. + simp [toFahrenheit, toScale, ofCelsius, ofScale] + -- We conclude by numerical computation. QED. + norm_num + +end Temperature diff --git a/PhysLean/Thermodynamics/Temperature/TemperatureUnits.lean b/PhysLean/Thermodynamics/Temperature/TemperatureUnits.lean index cff880aba..9d6f975a7 100644 --- a/PhysLean/Thermodynamics/Temperature/TemperatureUnits.lean +++ b/PhysLean/Thermodynamics/Temperature/TemperatureUnits.lean @@ -1,157 +1,311 @@ /- Copyright (c) 2025 Joseph Tooby-Smith. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Joseph Tooby-Smith +Authors: Trong-Nghia Be, Tan-Phuoc-Hung Le, Joseph Tooby-Smith -/ import Mathlib.Geometry.Manifold.Diffeomorph import PhysLean.SpaceAndTime.Time.Basic /-! +# Units on Temperature === TODO TIL THE END OF THE FILE -# Units on Temperature +A unit of temperature interval corresponds to a choice of +translationally-invariant metric on the temperature manifold (to be +defined diffeomorphic to `ℝ≥0`). Such a choice is (non-canonically) +equivalent to a choice of positive real number. We define the type +`TemperatureUnit` to be equivalent to the positive reals. -A unit of temperature corresponds to a choice of translationally-invariant -metric on the temperature manifold (to be defined diffeomorphic to `ℝ≥0`). -Such a choice is (non-canonically) equivalent to a -choice of positive real number. We define the type `TemperatureUnit` to be equivalent to the -positive reals. - -On `TemperatureUnit` there is an instance of division giving a real number, corresponding to the -ratio of the two scales of temperature unit. - -To define specific temperature units, we first state the existence of a -a given temperature unit, and then construct all other temperature units from it. -We choose to state the -existence of the temperature unit of kelvin, and construct all other temperature units from that. +On `TemperatureUnit` there is an instance of division giving a real +number, corresponding to the ratio of the two interval scales. +To define specific temperature units, we first state the existence of +a given temperature unit, and then construct all other temperature +units from it. We choose to state the existence of the temperature +unit of kelvin, and construct all other temperature units from that. -/ open NNReal -/-- The choices of translationally-invariant metrics on the temperature-manifold. - Such a choice corresponds to a choice of units for temperature. -/ +/-- The type `TemperatureUnit` represents a choice of + translationally-invariant metric on the temperature-manifold, + corresponding to a multiplicative choice of unit scale for + temperature intervals. + - `val` of type `ℝ`: The underlying scale of the unit. + - `property` of type `0 < val`: Proof that the scale is strictly + positive. +-/ structure TemperatureUnit where /-- The underlying scale of the unit. -/ val : ℝ + /-- Proof that the scale is strictly positive. -/ property : 0 < val namespace TemperatureUnit +/-- Simplification lemma for `TemperatureUnit`: + +The value of a temperature unit is nonzero. +-/ @[simp] lemma val_ne_zero (x : TemperatureUnit) : x.val ≠ 0 := by + -- Since `x.val > 0` (by `x.property`), it follows that + -- `x.val ≠ 0` by `Ne.symm` applied to `ne_of_lt x.property`. + -- QED. exact Ne.symm (ne_of_lt x.property) -lemma val_pos (x : TemperatureUnit) : 0 < x.val := x.property +/-- Lemma for `TemperatureUnit`: +The value of a temperature unit is strictly positive. +-/ +lemma val_pos (x : TemperatureUnit) : 0 < x.val := + x.property + +/-- Default instance for `TemperatureUnit`, set to scale `1`. +-/ instance : Inhabited TemperatureUnit where default := ⟨1, by norm_num⟩ /-! - ## Division of TemperatureUnit +-/ +/-- Division of two `TemperatureUnit` values, yielding a nonnegative +ratio in `ℝ≥0`. -/ +noncomputable instance : + HDiv TemperatureUnit TemperatureUnit ℝ≥0 where + hDiv x t := + ⟨x.val / t.val, + div_nonneg (le_of_lt x.val_pos) (le_of_lt t.val_pos)⟩ -noncomputable instance : HDiv TemperatureUnit TemperatureUnit ℝ≥0 where - hDiv x t := ⟨x.val / t.val, div_nonneg (le_of_lt x.val_pos) (le_of_lt t.val_pos)⟩ +/-- Lemma for `TemperatureUnit`: +Division unfolds to the ratio of underlying values. +-/ lemma div_eq_val (x y : TemperatureUnit) : - x / y = (⟨x.val / y.val, div_nonneg (le_of_lt x.val_pos) (le_of_lt y.val_pos)⟩ : ℝ≥0) := rfl + x / y = + (⟨x.val / y.val, + div_nonneg (le_of_lt x.val_pos) + (le_of_lt y.val_pos)⟩ : ℝ≥0) := rfl + +/-- Simplification lemma for `TemperatureUnit`: +The division of two temperature units is nonzero. +-/ @[simp] -lemma div_ne_zero (x y : TemperatureUnit) : ¬ x / y = (0 : ℝ≥0) := by +lemma div_ne_zero (x y : TemperatureUnit) : + ¬ x / y = (0 : ℝ≥0) := by + -- We rewrite the goal using the definition of division + -- from `div_eq_val`, which unfolds the division into the + -- ratio of underlying values. rw [div_eq_val] + -- We refine the goal using `coe_ne_zero.mp`, which + -- reduces the nonzero condition on `ℝ≥0` to a condition + -- on the underlying `ℝ` values. refine coe_ne_zero.mp ?_ + -- We simplify to conclude, since `x.val / y.val ≠ 0` + -- follows from both values being strictly positive. QED. simp +/-- Simplification lemma for `TemperatureUnit`: + +The division of two temperature units is strictly positive. +-/ @[simp] -lemma div_pos (x y : TemperatureUnit) : (0 : ℝ≥0) < x/ y := by +lemma div_pos (x y : TemperatureUnit) : + (0 : ℝ≥0) < x / y := by + -- We apply `lt_of_le_of_ne` to show strict positivity + -- from nonnegativity and the fact that the division is + -- nonzero. apply lt_of_le_of_ne + -- `case ha`: The goal is `⊢ 0 ≤ x / y`, which is true + -- since `x / y : ℝ≥0` is nonnegative by definition. + -- QED for this case. · exact zero_le (x / y) + -- `case hb`: The goal is `⊢ 0 ≠ x / y`, which follows + -- from `div_ne_zero x y` by symmetry. QED for this case. + -- All cases have been proven. QED. · exact Ne.symm (div_ne_zero x y) +/-- Simplification lemma for `TemperatureUnit`: + +Dividing a temperature unit by itself yields `1`. +-/ @[simp] lemma div_self (x : TemperatureUnit) : x / x = (1 : ℝ≥0) := by + -- We simplify using the definition of division and the + -- fact that `x.val ≠ 0`. QED. simp [div_eq_val, x.val_ne_zero] +/-- Lemma for `TemperatureUnit`: + +Division is the inverse of the reverse division. +-/ lemma div_symm (x y : TemperatureUnit) : x / y = (y / x)⁻¹ := NNReal.eq <| by + -- We rewrite both sides using `div_eq_val` and + -- `inv_eq_one_div` to express them in terms of + -- underlying values. rw [div_eq_val, inv_eq_one_div, div_eq_val] + -- We simplify to conclude, since the algebraic identity + -- `x / y = (y / x)⁻¹` holds for positive reals. QED. simp +/-- Simplification lemma for `TemperatureUnit`: + +Chain rule for division: `(x / y) * (y / z) = x / z` when coerced +to `ℝ`. +-/ @[simp] lemma div_mul_div_coe (x y z : TemperatureUnit) : - (x / y : ℝ) * (y /z : ℝ) = x /z := by + (x / y : ℝ) * (y / z : ℝ) = x / z := by + -- We simplify using the definition of division. simp [div_eq_val] + -- We apply `field_simp` to clear denominators and + -- conclude by algebraic simplification. QED. field_simp /-! - ## The scaling of a temperature unit - -/ -/-- The scaling of a temperature unit by a positive real. -/ -def scale (r : ℝ) (x : TemperatureUnit) (hr : 0 < r := by norm_num) : TemperatureUnit := +/-- Function for `TemperatureUnit`: + +Scale a temperature unit by a positive real number. +-/ +def scale (r : ℝ) (x : TemperatureUnit) + (hr : 0 < r := by norm_num) : TemperatureUnit := ⟨r * x.val, mul_pos hr x.val_pos⟩ +/-- Simplification lemma for `TemperatureUnit`: + +Scaling a unit and dividing by the original yields the scale factor. +-/ @[simp] -lemma scale_div_self (x : TemperatureUnit) (r : ℝ) (hr : 0 < r) : +lemma scale_div_self (x : TemperatureUnit) (r : ℝ) + (hr : 0 < r) : scale r x hr / x = (⟨r, le_of_lt hr⟩ : ℝ≥0) := by + -- We simplify using the definitions of `scale` and + -- `div_eq_val`. QED. simp [scale, div_eq_val] +/-- Simplification lemma for `TemperatureUnit`: + +Dividing a unit by its scaled version yields the reciprocal of the +scale factor. +-/ @[simp] -lemma self_div_scale (x : TemperatureUnit) (r : ℝ) (hr : 0 < r) : - x / scale r x hr = (⟨1/r, _root_.div_nonneg (by simp) (le_of_lt hr)⟩ : ℝ≥0) := by +lemma self_div_scale (x : TemperatureUnit) (r : ℝ) + (hr : 0 < r) : + x / scale r x hr = + (⟨1 / r, + _root_.div_nonneg (by simp) + (le_of_lt hr)⟩ : ℝ≥0) := by + -- We simplify using the definitions of `scale` and + -- `div_eq_val`. simp [scale, div_eq_val] + -- We apply extensionality to reduce the goal to + -- equality of underlying values. ext + -- We simplify the coercion from `ℝ≥0` to `ℝ`. simp only [coe_mk] + -- We apply `field_simp` to clear denominators and + -- conclude by algebraic simplification. QED. field_simp +/-- Simplification lemma for `TemperatureUnit`: + +Scaling by `1` is the identity. +-/ @[simp] -lemma scale_one (x : TemperatureUnit) : scale 1 x = x := by +lemma scale_one (x : TemperatureUnit) : + scale 1 x = x := by + -- We simplify using the definition of `scale`, since + -- `1 * x.val = x.val`. QED. simp [scale] +/-- Simplification lemma for `TemperatureUnit`: + +The ratio of two scaled units factors into the product of scale +ratios and unit ratios. +-/ @[simp] -lemma scale_div_scale (x1 x2 : TemperatureUnit) {r1 r2 : ℝ} (hr1 : 0 < r1) (hr2 : 0 < r2) : - scale r1 x1 hr1 / scale r2 x2 hr2 = (⟨r1, le_of_lt hr1⟩ / ⟨r2, le_of_lt hr2⟩) * (x1 / x2) := by +lemma scale_div_scale (x1 x2 : TemperatureUnit) + {r1 r2 : ℝ} (hr1 : 0 < r1) (hr2 : 0 < r2) : + scale r1 x1 hr1 / scale r2 x2 hr2 = + (⟨r1, le_of_lt hr1⟩ / ⟨r2, le_of_lt hr2⟩) * + (x1 / x2) := by + -- We refine the goal using `NNReal.eq`, which reduces + -- equality of `ℝ≥0` values to equality of their + -- underlying `ℝ` values. refine NNReal.eq ?_ + -- We simplify using the definitions of `scale` and + -- `div_eq_val`. simp [scale, div_eq_val] + -- We apply `field_simp` to clear denominators and + -- conclude by algebraic simplification. QED. field_simp +/-- Simplification lemma for `TemperatureUnit`: + +Double scaling is equivalent to scaling by the product. +-/ @[simp] -lemma scale_scale (x : TemperatureUnit) (r1 r2 : ℝ) (hr1 : 0 < r1) (hr2 : 0 < r2) : - scale r1 (scale r2 x hr2) hr1 = scale (r1 * r2) x (mul_pos hr1 hr2) := by +lemma scale_scale (x : TemperatureUnit) (r1 r2 : ℝ) + (hr1 : 0 < r1) (hr2 : 0 < r2) : + scale r1 (scale r2 x hr2) hr1 = + scale (r1 * r2) x (mul_pos hr1 hr2) := by + -- We simplify using the definition of `scale`. simp [scale] + -- We conclude by the algebraic identity + -- `r1 * (r2 * x.val) = (r1 * r2) * x.val`. QED. ring /-! - ## Specific choices of temperature units -To define a specific temperature units. -We first define the notion of a kelvin to correspond to the temperature unit with underlying value -equal to `1`. This is really down to a choice in the isomorphism between the set of metrics -on the temperature manifold and the positive reals. - -Once we have defined kelvin, we can define other temperature units by scaling kelvin. +To define specific temperature units, we first define the notion of +a kelvin to correspond to the temperature unit with underlying value +equal to `1`. This is really down to a choice in the isomorphism +between the set of metrics on the temperature manifold and the +positive reals. +Once we have defined kelvin, we can define other temperature units +by scaling kelvin. -/ -/-- The definition of a temperature unit of kelvin. -/ +/-- Function for `TemperatureUnit`: + +The definition of a temperature unit of kelvin. +-/ def kelvin : TemperatureUnit := ⟨1, by norm_num⟩ -/-- The temperature unit of degrees nanokelvin (10^(-9) kelvin). -/ -noncomputable def nanokelvin : TemperatureUnit := scale (1e-9) kelvin +/-- Function for `TemperatureUnit`: + +The temperature unit of degrees nanokelvin (`10^(-9) kelvin`). +-/ +noncomputable def nanokelvin : TemperatureUnit := + scale (1e-9) kelvin + +/-- Function for `TemperatureUnit`: + +The temperature unit of degrees microkelvin (`10^(-6) kelvin`). +-/ +noncomputable def microkelvin : TemperatureUnit := + scale (1e-6) kelvin + +/-- Function for `TemperatureUnit`: -/-- The temperature unit of degrees microkelvin (10^(-6) kelvin). -/ -noncomputable def microkelvin : TemperatureUnit := scale (1e-6) kelvin +The temperature unit of degrees millikelvin (`10^(-3) kelvin`). +-/ +noncomputable def millikelvin : TemperatureUnit := + scale (1e-3) kelvin -/-- The temperature unit of degrees millikelvin (10^(-3) kelvin). -/ -noncomputable def millikelvin : TemperatureUnit := scale (1e-3) kelvin +/-- Function for `TemperatureUnit`: -/-- The temperature unit of degrees fahrenheit ((5/9) of a kelvin). - Note, this is fahrenheit starting at `0` absolute temperature. -/ -noncomputable def absoluteFahrenheit : TemperatureUnit := scale (5 / 9) kelvin +The temperature unit of degrees rankine (`(5/9)` of a kelvin). +-/ +noncomputable def rankine : TemperatureUnit := + scale (5 / 9) kelvin end TemperatureUnit