From d2ddfe31e562b249b984ebf64db33c6bcfb17df8 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 10 Sep 2026 18:05:31 +0200 Subject: [PATCH 01/20] feat(Cosmology): de Sitter solution of the Friedmann equations Adds to Physlib/Cosmology/FLRW/Solutions.lean the de Sitter scale factor deSitterScaleFactor, its time derivatives, and the lemmas deSitterScaleFactor_firstOrderFriedmann, deSitterScaleFactor_secondOrderFriedmann, hubbleConstant_deSitterScaleFactor and decelerationParameter_deSitterScaleFactor, resolving the first TODO of the file. Also deriv_comp_val, the time derivative of a curve given as a function of the time coordinate. Generated with Claude Code under human supervision (see AI-POLICY.md). Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/Solutions.lean | 177 ++++++++++++++++++++++++-- 1 file changed, 169 insertions(+), 8 deletions(-) diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index e0daae992d..4a472e3f0a 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -1,27 +1,186 @@ /- Copyright (c) 2026 Jinzheng Li. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jinzheng Li +Authors: Jinzheng Li, Philippe Kevorkian -/ module public import Physlib.Meta.TODO.Basic +public import Physlib.Cosmology.FLRW.Basic /-! # Exact solutions of the Friedmann equations -Placeholder file collecting TODO items for the standard closed-form solutions of -the Friedmann equations: the de Sitter, radiation-dominated, Einstein-de Sitter -(dust) and Milne models, together with the Einstein static universe. This file -contains only TODO items; no definitions or lemmas are formalized yet. +## i. Overview + +This file collects the standard closed-form solutions of the Friedmann equations +(`FirstOrderFriedmann` and `SecondOrderFriedmann` of `Physlib.Cosmology.FLRW.Basic`) and +proves that they solve them: the de Sitter solution here, the radiation-dominated, +Einstein-de Sitter and Milne models and the Einstein static universe being still TODO items. + +Each solution is a scale factor `a : Time → ℝ` given by an explicit function of the time +coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridge +`deriv_comp_toRealCLE_of_hasDerivAt` from Mathlib's `HasDerivAt` on `ℝ`. + +## ii. Key results + +- `deSitterScaleFactor`: `a(t) = a₀ exp(σ √(Λ/3) c t)` with `σ = ±1`. +- `deSitterScaleFactor_firstOrderFriedmann`, `deSitterScaleFactor_secondOrderFriedmann`: + it solves both Friedmann equations with `ρ = 0`, `p = 0`, `k = 0` and `Λ > 0`. +- `hubbleConstant_deSitterScaleFactor`: its Hubble parameter is the constant `σ √(Λ/3) c` + (for any `σ`, `Λ`, `c`). +- `decelerationParameter_deSitterScaleFactor`: its deceleration parameter is `q = -1`. + +## iii. Table of contents + +- A. Time derivatives of curves given by a function of the coordinate +- B. The de Sitter solution + - B.1. The scale factor and its derivatives + - B.2. The Friedmann equations + - B.3. The Hubble and deceleration parameters +- C. Remaining TODO items -/ @[expose] public section -TODO "Prove that the de Sitter solution `a(t) = a₀ exp(±√(Λ/3) c t)` (with `ρ = 0`, - `K = 0`, `Λ > 0`) solves the Friedmann equations, and that its deceleration - parameter is `q = −1`." +namespace Cosmology.FLRW.FriedmannEquation + +open Real Time + +/-! + +## A. Time derivatives of curves given by a function of the coordinate + +A curve `t ↦ γ t.val` on `Time` is the pull-back through `toRealCLE` of the curve `γ` on `ℝ`; +its time derivative is the Mathlib derivative of `γ`. + +-/ + +/-- The time derivative of `t ↦ γ t.val` at `t` is the derivative of `γ` at `t.val`. -/ +lemma deriv_comp_val {γ : ℝ → ℝ} {t : Time} {v : ℝ} (h : HasDerivAt γ v t.val) : + ∂ₜ (fun s : Time => γ s.val) t = v := + deriv_comp_toRealCLE_of_hasDerivAt γ t v h + +/-! + +## B. The de Sitter solution + +-/ + +/-! + +### B.1. The scale factor and its derivatives + +-/ + +/-- The de Sitter scale factor `a(t) = a₀ exp(σ √(Λ/3) c t)`, for `σ = ±1` + (the expanding branch is `σ = 1`). -/ +noncomputable def deSitterScaleFactor (a₀ σ Λ c : ℝ) : Time → ℝ := + fun t => a₀ * Real.exp (σ * √(Λ / 3) * c * t.val) + +/-- Mathlib derivative of `y ↦ a₀ exp (K y)`. -/ +lemma hasDerivAt_mul_exp_mul (a₀ K x : ℝ) : + HasDerivAt (fun y : ℝ => a₀ * Real.exp (K * y)) (a₀ * K * Real.exp (K * x)) x := by + have h := (((hasDerivAt_id x).const_mul K).exp).const_mul a₀ + refine h.congr_deriv ?_ + simp only [id_eq] + ring + +lemma deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : + ∂ₜ (deSitterScaleFactor a₀ σ Λ c) = + fun t => a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val) := by + funext t + exact deriv_comp_val (hasDerivAt_mul_exp_mul a₀ (σ * √(Λ / 3) * c) t.val) + +lemma deriv_deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : + ∂ₜ (∂ₜ (deSitterScaleFactor a₀ σ Λ c)) = + fun t => a₀ * (σ * √(Λ / 3) * c) * (σ * √(Λ / 3) * c) * + Real.exp (σ * √(Λ / 3) * c * t.val) := by + rw [deriv_deSitterScaleFactor] + funext t + exact deriv_comp_val + (hasDerivAt_mul_exp_mul (a₀ * (σ * √(Λ / 3) * c)) (σ * √(Λ / 3) * c) t.val) + +/-- `σ² (√(Λ/3))² c² = Λ c² / 3` for `σ = ±1` and `0 ≤ Λ`. -/ +lemma sq_deSitterRate {σ Λ c : ℝ} (hΛ : 0 ≤ Λ) (hσ : σ = 1 ∨ σ = -1) : + (σ * √(Λ / 3) * c) ^ 2 = Λ * c ^ 2 / 3 := by + have hs : √(Λ / 3) ^ 2 = Λ / 3 := Real.sq_sqrt (by linarith) + rcases hσ with rfl | rfl <;> linear_combination c ^ 2 * hs + +/-! + +### B.2. The Friedmann equations + +-/ + +/-- The de Sitter scale factor solves the first-order Friedmann equation with `ρ = 0`, + `k = 0` and `Λ > 0`. -/ +lemma deSitterScaleFactor_firstOrderFriedmann {a₀ σ Λ G c : ℝ} (hΛ : 0 < Λ) + (ha₀ : a₀ ≠ 0) (hσ : σ = 1 ∨ σ = -1) (t : Time) : + FirstOrderFriedmann (deSitterScaleFactor a₀ σ Λ c) (fun _ => 0) 0 Λ G c t := by + unfold FirstOrderFriedmann + rw [deriv_deSitterScaleFactor] + simp only [deSitterScaleFactor] + have he := Real.exp_ne_zero (σ * √(Λ / 3) * c * t.val) + rw [show a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val) / + (a₀ * Real.exp (σ * √(Λ / 3) * c * t.val)) = σ * √(Λ / 3) * c by field_simp, + sq_deSitterRate hΛ.le hσ] + ring + +/-- The de Sitter scale factor solves the second-order Friedmann equation with `ρ = 0`, + `p = 0` and `Λ > 0`. -/ +lemma deSitterScaleFactor_secondOrderFriedmann {a₀ σ Λ G c : ℝ} (hΛ : 0 < Λ) + (ha₀ : a₀ ≠ 0) (hσ : σ = 1 ∨ σ = -1) (t : Time) : + SecondOrderFriedmann (deSitterScaleFactor a₀ σ Λ c) (fun _ => 0) (fun _ => 0) Λ G c t := by + unfold SecondOrderFriedmann + rw [deriv_deriv_deSitterScaleFactor] + simp only [deSitterScaleFactor] + have he := Real.exp_ne_zero (σ * √(Λ / 3) * c * t.val) + rw [show a₀ * (σ * √(Λ / 3) * c) * (σ * √(Λ / 3) * c) * + Real.exp (σ * √(Λ / 3) * c * t.val) / (a₀ * Real.exp (σ * √(Λ / 3) * c * t.val)) + = (σ * √(Λ / 3) * c) ^ 2 by field_simp, + sq_deSitterRate hΛ.le hσ] + ring + +/-! + +### B.3. The Hubble and deceleration parameters + +-/ + +/-- The Hubble parameter of the de Sitter solution is the constant `σ √(Λ/3) c`. -/ +lemma hubbleConstant_deSitterScaleFactor {a₀ σ Λ c : ℝ} (ha₀ : a₀ ≠ 0) (t : Time) : + hubbleConstant (deSitterScaleFactor a₀ σ Λ c) t = σ * √(Λ / 3) * c := by + unfold hubbleConstant + rw [deriv_deSitterScaleFactor] + simp only [deSitterScaleFactor] + have he := Real.exp_ne_zero (σ * √(Λ / 3) * c * t.val) + field_simp + +/-- The deceleration parameter of the de Sitter solution is `q = -1`. -/ +lemma decelerationParameter_deSitterScaleFactor {a₀ σ Λ c : ℝ} (hΛ : 0 < Λ) (hc : 0 < c) + (ha₀ : a₀ ≠ 0) (hσ : σ = 1 ∨ σ = -1) (t : Time) : + decelerationParameter (deSitterScaleFactor a₀ σ Λ c) t = -1 := by + unfold decelerationParameter + rw [deriv_deriv_deSitterScaleFactor, deriv_deSitterScaleFactor] + simp only [deSitterScaleFactor] + have he := Real.exp_ne_zero (σ * √(Λ / 3) * c * t.val) + have hK : σ * √(Λ / 3) * c ≠ 0 := by + have hs : 0 < √(Λ / 3) := Real.sqrt_pos.mpr (by linarith) + rcases hσ with rfl | rfl + · positivity + · have : 0 < √(Λ / 3) * c := mul_pos hs hc + linarith + have hσ0 : σ ≠ 0 := by + rcases hσ with rfl | rfl <;> norm_num + field_simp + +/-! + +## C. Remaining TODO items + +-/ TODO "Prove that the spatially flat radiation-dominated solution `a = (t/t₀)^(1/2)` solves the Friedmann equations, with `q₀ = 1` and `t₀ = 1 / (2 H₀)`." @@ -35,3 +194,5 @@ TODO "Prove that the Milne solution `a = c t` (empty universe, `K < 0`) has TODO "Define the Einstein static universe (`∂ₜ a = ∂ₜ ∂ₜ a = 0`, forcing `K > 0` and `ρ_m = 2 ρ_Λ`) and prove that it is an unstable equilibrium." + +end Cosmology.FLRW.FriedmannEquation From b8a0b43ff72632263a6272840b50c26c07f200b2 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 10 Sep 2026 18:27:26 +0200 Subject: [PATCH 02/20] feat(Cosmology): flat power-law solutions of the Friedmann equations Adds to Physlib/Cosmology/FLRW/Solutions.lean the power-law scale factor powerLawScaleFactor with its derivatives, Hubble and deceleration parameters, the density powerLawDensity it imposes, and the radiation-dominated (radiationScaleFactor, radiationDensity, radiationPressure) and Einstein-de Sitter (einsteinDeSitterScaleFactor, einsteinDeSitterDensity) instances with their Friedmann lemmas, q and H(t0), resolving two TODOs of the file. Also deriv_eq_of_hasDerivAt. Generated with Claude Code under human supervision (see AI-POLICY.md). Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/Solutions.lean | 260 +++++++++++++++++++++++++- 1 file changed, 251 insertions(+), 9 deletions(-) diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index 4a472e3f0a..9d1281450a 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -7,6 +7,7 @@ module public import Physlib.Meta.TODO.Basic public import Physlib.Cosmology.FLRW.Basic +public import Mathlib.Analysis.SpecialFunctions.Pow.Deriv /-! # Exact solutions of the Friedmann equations @@ -15,8 +16,9 @@ public import Physlib.Cosmology.FLRW.Basic This file collects the standard closed-form solutions of the Friedmann equations (`FirstOrderFriedmann` and `SecondOrderFriedmann` of `Physlib.Cosmology.FLRW.Basic`) and -proves that they solve them: the de Sitter solution here, the radiation-dominated, -Einstein-de Sitter and Milne models and the Einstein static universe being still TODO items. +proves that they solve them: the de Sitter solution and the spatially flat power-law +solutions (radiation-dominated and Einstein-de Sitter) here, the Milne model and the +Einstein static universe being still TODO items. Each solution is a scale factor `a : Time → ℝ` given by an explicit function of the time coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridge @@ -30,6 +32,17 @@ coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridg - `hubbleConstant_deSitterScaleFactor`: its Hubble parameter is the constant `σ √(Λ/3) c` (for any `σ`, `Λ`, `c`). - `decelerationParameter_deSitterScaleFactor`: its deceleration parameter is `q = -1`. +- `powerLawScaleFactor`: `a(t) = (t / t₀) ^ n`, with Hubble parameter `n / t` + (`hubbleConstant_powerLawScaleFactor`) and deceleration parameter `(1 - n) / n` + (`decelerationParameter_powerLawScaleFactor`) for `t > 0`. +- `radiationScaleFactor_firstOrderFriedmann`, `radiationScaleFactor_secondOrderFriedmann`: + `a = (t / t₀) ^ (1/2)` solves the flat (`k = 0`, `Λ = 0`) Friedmann equations with the + density `ρ = 3 / (32 π G t²)` and the radiation pressure `p = ρ c² / 3`; `q = 1` and + `H(t₀) = 1 / (2 t₀)`. +- `einsteinDeSitterScaleFactor_firstOrderFriedmann`, + `einsteinDeSitterScaleFactor_secondOrderFriedmann`: `a = (t / t₀) ^ (2/3)` solves the flat + Friedmann equations with the dust density `ρ = 1 / (6 π G t²)` and `p = 0`; `q = 1 / 2` and + `H(t₀) = 2 / (3 t₀)`. ## iii. Table of contents @@ -38,7 +51,12 @@ coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridg - B.1. The scale factor and its derivatives - B.2. The Friedmann equations - B.3. The Hubble and deceleration parameters -- C. Remaining TODO items +- C. The spatially flat power-law solutions + - C.1. The power-law scale factor and its derivatives + - C.2. The Hubble and deceleration parameters + - C.3. The radiation-dominated solution + - C.4. The Einstein-de Sitter solution +- D. Remaining TODO items -/ @@ -62,6 +80,12 @@ lemma deriv_comp_val {γ : ℝ → ℝ} {t : Time} {v : ℝ} (h : HasDerivAt γ ∂ₜ (fun s : Time => γ s.val) t = v := deriv_comp_toRealCLE_of_hasDerivAt γ t v h +/-- The time derivative of any `f : Time → ℝ` at `t` is the derivative at `t.val` of the curve + `τ ↦ f ⟨τ⟩` on `ℝ`. -/ +lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} + (h : HasDerivAt (fun τ : ℝ => f ⟨τ⟩) v t.val) : ∂ₜ f t = v := + deriv_comp_toRealCLE_of_hasDerivAt (fun τ : ℝ => f ⟨τ⟩) t v h + /-! ## B. The de Sitter solution @@ -178,16 +202,234 @@ lemma decelerationParameter_deSitterScaleFactor {a₀ σ Λ c : ℝ} (hΛ : 0 < /-! -## C. Remaining TODO items +## C. The spatially flat power-law solutions + +The radiation-dominated and Einstein-de Sitter solutions are both of the form +`a(t) = (t / t₀) ^ n` for `t > 0`; the Hubble parameter is `n / t` and the deceleration +parameter `(1 - n) / n`. Their densities are imposed by the first-order Friedmann equation with +`k = 0` and `Λ = 0`: `ρ = 3 H² / (8 π G) = 3 n² / (8 π G t²)`. + +-/ + +/-! + +### C.1. The power-law scale factor and its derivatives + +-/ + +/-- The power-law scale factor `a(t) = (t / t₀) ^ n` (real power). -/ +noncomputable def powerLawScaleFactor (t₀ n : ℝ) : Time → ℝ := + fun t => (t.val / t₀) ^ n + +/-- Mathlib derivative of `y ↦ (y / t₀) ^ n` away from `y = 0`. -/ +lemma hasDerivAt_div_rpow {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {x : ℝ} (hx : x ≠ 0) : + HasDerivAt (fun y : ℝ => (y / t₀) ^ n) (n / t₀ * (x / t₀) ^ (n - 1)) x := by + have h := ((hasDerivAt_id x).div_const t₀).rpow_const (p := n) + (Or.inl (div_ne_zero hx ht₀)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + +/-- `∂ₜ a = n / t₀ (t / t₀) ^ (n - 1)` away from `t = 0`. -/ +lemma deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} + (ht : t.val ≠ 0) : + ∂ₜ (powerLawScaleFactor t₀ n) t = n / t₀ * (t.val / t₀) ^ (n - 1) := + deriv_comp_val (hasDerivAt_div_rpow ht₀ n ht) + +/-- `∂ₜ ∂ₜ a = n (n - 1) / t₀² (t / t₀) ^ (n - 2)` for `t > 0`. The derivative `∂ₜ a` is + only known away from `t = 0`, which is enough since `t > 0` is an open condition. -/ +lemma deriv_deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} + (ht : 0 < t.val) : + ∂ₜ (∂ₜ (powerLawScaleFactor t₀ n)) t = + n / t₀ * ((n - 1) / t₀ * (t.val / t₀) ^ (n - 1 - 1)) := by + apply deriv_eq_of_hasDerivAt + have h := (hasDerivAt_div_rpow ht₀ (n - 1) ht.ne').const_mul (n / t₀) + refine h.congr_of_eventuallyEq ?_ + filter_upwards [eventually_ne_nhds ht.ne'] with τ hτ + exact deriv_powerLawScaleFactor ht₀ n (t := ⟨τ⟩) hτ + +/-! + +### C.2. The Hubble and deceleration parameters + +-/ + +/-- The Hubble parameter of the power-law solution is `n / t` for `t > 0`. -/ +lemma hubbleConstant_powerLawScaleFactor {t₀ : ℝ} (ht₀ : 0 < t₀) (n : ℝ) {t : Time} + (ht : 0 < t.val) : + hubbleConstant (powerLawScaleFactor t₀ n) t = n / t.val := by + unfold hubbleConstant + rw [deriv_powerLawScaleFactor ht₀.ne' n ht.ne', powerLawScaleFactor, + Real.rpow_sub_one (div_pos ht ht₀).ne'] + have hx : (t.val / t₀) ^ n ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) n).ne' + field_simp + +/-- The deceleration parameter of the power-law solution is `(1 - n) / n` for `t > 0`, + `n ≠ 0`. -/ +lemma decelerationParameter_powerLawScaleFactor {t₀ n : ℝ} (ht₀ : 0 < t₀) (hn : n ≠ 0) + {t : Time} (ht : 0 < t.val) : + decelerationParameter (powerLawScaleFactor t₀ n) t = (1 - n) / n := by + unfold decelerationParameter + rw [deriv_deriv_powerLawScaleFactor ht₀.ne' n ht, deriv_powerLawScaleFactor ht₀.ne' n ht.ne', + powerLawScaleFactor, Real.rpow_sub_one (div_pos ht ht₀).ne', + Real.rpow_sub_one (div_pos ht ht₀).ne'] + have hx : (t.val / t₀) ^ n ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) n).ne' + field_simp + ring + +/-- The density imposed on the flat power-law solution by the first-order Friedmann equation, + `ρ = 3 n² / (8 π G t²)`. -/ +noncomputable def powerLawDensity (G n : ℝ) : Time → ℝ := + fun t => 3 * n ^ 2 / (8 * π * G * t.val ^ 2) + +/-- The flat power-law solution solves the first-order Friedmann equation with `k = 0`, + `Λ = 0` and the density `powerLawDensity`, for `t > 0`. -/ +lemma powerLawScaleFactor_firstOrderFriedmann {t₀ G c : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) + (n : ℝ) {t : Time} (ht : 0 < t.val) : + FirstOrderFriedmann (powerLawScaleFactor t₀ n) (powerLawDensity G n) 0 0 G c t := by + unfold FirstOrderFriedmann + have hH := hubbleConstant_powerLawScaleFactor ht₀ n ht + unfold hubbleConstant at hH + rw [hH, powerLawDensity] + have hπ := Real.pi_pos + field_simp + ring + +/-- The second-order Friedmann equation for the flat power-law solution with the pressure + `p = w ρ c²`, where `1 + 3 w = 2 (1 - n) / n`, for `t > 0`. -/ +lemma powerLawScaleFactor_secondOrderFriedmann {t₀ G c n w : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) + (hc : 0 < c) (hn : n ≠ 0) (hw : 1 + 3 * w = 2 * (1 - n) / n) {t : Time} (ht : 0 < t.val) : + SecondOrderFriedmann (powerLawScaleFactor t₀ n) (powerLawDensity G n) + (fun s => w * powerLawDensity G n s * c ^ 2) 0 G c t := by + unfold SecondOrderFriedmann + simp only [powerLawDensity] + rw [deriv_deriv_powerLawScaleFactor ht₀.ne' n ht, powerLawScaleFactor, + Real.rpow_sub_one (div_pos ht ht₀).ne', Real.rpow_sub_one (div_pos ht ht₀).ne'] + have hx : (t.val / t₀) ^ n ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) n).ne' + have hπ := Real.pi_pos + rw [show w = (2 * (1 - n) / n - 1) / 3 by linarith] + field_simp + ring + +/-! + +### C.3. The radiation-dominated solution -/ -TODO "Prove that the spatially flat radiation-dominated solution `a = (t/t₀)^(1/2)` - solves the Friedmann equations, with `q₀ = 1` and `t₀ = 1 / (2 H₀)`." +/-- The radiation-dominated scale factor `a(t) = (t / t₀) ^ (1/2)`. -/ +noncomputable def radiationScaleFactor (t₀ : ℝ) : Time → ℝ := + powerLawScaleFactor t₀ (1 / 2) + +/-- The density of the flat radiation-dominated solution, `ρ = 3 / (32 π G t²)`, imposed by + the first-order Friedmann equation. -/ +noncomputable def radiationDensity (G : ℝ) : Time → ℝ := + fun t => 3 / (32 * π * G * t.val ^ 2) + +/-- The radiation pressure `p = ρ c² / 3`. -/ +noncomputable def radiationPressure (G c : ℝ) : Time → ℝ := + fun t => radiationDensity G t * c ^ 2 / 3 + +lemma radiationDensity_eq (G : ℝ) : radiationDensity G = powerLawDensity G (1 / 2) := by + funext t + simp only [radiationDensity, powerLawDensity] + ring + +/-- The radiation-dominated solution solves the first-order Friedmann equation with `k = 0`, + `Λ = 0`, for `t > 0`. -/ +lemma radiationScaleFactor_firstOrderFriedmann {t₀ G c : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) + {t : Time} (ht : 0 < t.val) : + FirstOrderFriedmann (radiationScaleFactor t₀) (radiationDensity G) 0 0 G c t := by + rw [radiationScaleFactor, radiationDensity_eq] + exact powerLawScaleFactor_firstOrderFriedmann ht₀ hG _ ht + +/-- The radiation-dominated solution solves the second-order Friedmann equation with + `p = ρ c² / 3`, `Λ = 0`, for `t > 0`. -/ +lemma radiationScaleFactor_secondOrderFriedmann {t₀ G c : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) + (hc : 0 < c) {t : Time} (ht : 0 < t.val) : + SecondOrderFriedmann (radiationScaleFactor t₀) (radiationDensity G) (radiationPressure G c) + 0 G c t := by + have h := powerLawScaleFactor_secondOrderFriedmann (w := 1 / 3) ht₀ hG hc + (by norm_num : (1 / 2 : ℝ) ≠ 0) (by norm_num) ht + rw [radiationScaleFactor, radiationDensity_eq] + convert h using 2 + simp only [radiationPressure, radiationDensity_eq] + ring + +/-- The deceleration parameter of the radiation-dominated solution is `q = 1`. -/ +lemma decelerationParameter_radiationScaleFactor {t₀ : ℝ} (ht₀ : 0 < t₀) {t : Time} + (ht : 0 < t.val) : + decelerationParameter (radiationScaleFactor t₀) t = 1 := by + rw [radiationScaleFactor, decelerationParameter_powerLawScaleFactor ht₀ (by norm_num) ht] + norm_num + +/-- `H(t₀) = 1 / (2 t₀)` for the radiation-dominated solution, that is `t₀ = 1 / (2 H₀)`. -/ +lemma hubbleConstant_radiationScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < t₀) : + hubbleConstant (radiationScaleFactor t₀) ⟨t₀⟩ = 1 / (2 * t₀) := by + rw [radiationScaleFactor, hubbleConstant_powerLawScaleFactor ht₀ _ ht₀] + ring + +/-! -TODO "Prove that the Einstein-de Sitter (spatially flat, dust) solution - `a = (t/t₀)^(2/3)` solves the Friedmann equations, with `q₀ = 1/2` and - `t₀ = 2 / (3 H₀)`." +### C.4. The Einstein-de Sitter solution + +-/ + +/-- The Einstein-de Sitter (flat, dust) scale factor `a(t) = (t / t₀) ^ (2/3)`. -/ +noncomputable def einsteinDeSitterScaleFactor (t₀ : ℝ) : Time → ℝ := + powerLawScaleFactor t₀ (2 / 3) + +/-- The dust density of the Einstein-de Sitter solution, `ρ = 1 / (6 π G t²)`, imposed by the + first-order Friedmann equation. -/ +noncomputable def einsteinDeSitterDensity (G : ℝ) : Time → ℝ := + fun t => 1 / (6 * π * G * t.val ^ 2) + +lemma einsteinDeSitterDensity_eq (G : ℝ) : + einsteinDeSitterDensity G = powerLawDensity G (2 / 3) := by + funext t + simp only [einsteinDeSitterDensity, powerLawDensity] + ring + +/-- The Einstein-de Sitter solution solves the first-order Friedmann equation with `k = 0`, + `Λ = 0`, for `t > 0`. -/ +lemma einsteinDeSitterScaleFactor_firstOrderFriedmann {t₀ G c : ℝ} (ht₀ : 0 < t₀) + (hG : 0 < G) {t : Time} (ht : 0 < t.val) : + FirstOrderFriedmann (einsteinDeSitterScaleFactor t₀) (einsteinDeSitterDensity G) + 0 0 G c t := by + rw [einsteinDeSitterScaleFactor, einsteinDeSitterDensity_eq] + exact powerLawScaleFactor_firstOrderFriedmann ht₀ hG _ ht + +/-- The Einstein-de Sitter solution solves the second-order Friedmann equation with `p = 0`, + `Λ = 0`, for `t > 0`. -/ +lemma einsteinDeSitterScaleFactor_secondOrderFriedmann {t₀ G c : ℝ} (ht₀ : 0 < t₀) + (hG : 0 < G) (hc : 0 < c) {t : Time} (ht : 0 < t.val) : + SecondOrderFriedmann (einsteinDeSitterScaleFactor t₀) (einsteinDeSitterDensity G) + (fun _ => 0) 0 G c t := by + have h := powerLawScaleFactor_secondOrderFriedmann (w := 0) ht₀ hG hc + (by norm_num : (2 / 3 : ℝ) ≠ 0) (by norm_num) ht + rw [einsteinDeSitterScaleFactor, einsteinDeSitterDensity_eq] + convert h using 2 + ring + +/-- The deceleration parameter of the Einstein-de Sitter solution is `q = 1 / 2`. -/ +lemma decelerationParameter_einsteinDeSitterScaleFactor {t₀ : ℝ} (ht₀ : 0 < t₀) {t : Time} + (ht : 0 < t.val) : + decelerationParameter (einsteinDeSitterScaleFactor t₀) t = 1 / 2 := by + rw [einsteinDeSitterScaleFactor, + decelerationParameter_powerLawScaleFactor ht₀ (by norm_num) ht] + norm_num + +/-- `H(t₀) = 2 / (3 t₀)` for the Einstein-de Sitter solution, that is `t₀ = 2 / (3 H₀)`. -/ +lemma hubbleConstant_einsteinDeSitterScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < t₀) : + hubbleConstant (einsteinDeSitterScaleFactor t₀) ⟨t₀⟩ = 2 / (3 * t₀) := by + rw [einsteinDeSitterScaleFactor, hubbleConstant_powerLawScaleFactor ht₀ _ ht₀] + ring + +/-! + +## D. Remaining TODO items + +-/ TODO "Prove that the Milne solution `a = c t` (empty universe, `K < 0`) has vanishing scalar curvature, i.e. it is Minkowski space in expanding coordinates." From 0be812ced040f3e7379a03d2e6f62946ad1e773d Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 10 Sep 2026 18:27:33 +0200 Subject: [PATCH 03/20] feat(Cosmology): Milne solution and Einstein static universe relations Adds to Physlib/Cosmology/FLRW/Solutions.lean the Milne scale factor milneScaleFactor with its Friedmann lemmas (k = -1, empty universe) and q = 0, the density cosmologicalConstantDensity, and the equilibrium relations of the Einstein static universe: einsteinStatic_density (rho = 2 rho_Lambda), einsteinStatic_curvature (k c^2 / a^2 = 4 pi G rho) and einsteinStatic_curvature_pos. The curvature of the Milne model and the instability of the static universe stay as narrowed TODOs. Generated with Claude Code under human supervision (see AI-POLICY.md). Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/Solutions.lean | 129 ++++++++++++++++++++++++-- 1 file changed, 121 insertions(+), 8 deletions(-) diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index 9d1281450a..97933c3239 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -16,9 +16,11 @@ public import Mathlib.Analysis.SpecialFunctions.Pow.Deriv This file collects the standard closed-form solutions of the Friedmann equations (`FirstOrderFriedmann` and `SecondOrderFriedmann` of `Physlib.Cosmology.FLRW.Basic`) and -proves that they solve them: the de Sitter solution and the spatially flat power-law -solutions (radiation-dominated and Einstein-de Sitter) here, the Milne model and the -Einstein static universe being still TODO items. +proves that they solve them: the de Sitter solution, the spatially flat power-law +solutions (radiation-dominated and Einstein-de Sitter), the Milne model, and the equilibrium +relations of the Einstein static universe. The vanishing of the curvature of the Milne model +and the instability of the Einstein static universe are still TODO items: neither the curvature +of the FLRW metric nor a perturbation theory of the Friedmann equations is available yet. Each solution is a scale factor `a : Time → ℝ` given by an explicit function of the time coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridge @@ -43,6 +45,12 @@ coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridg `einsteinDeSitterScaleFactor_secondOrderFriedmann`: `a = (t / t₀) ^ (2/3)` solves the flat Friedmann equations with the dust density `ρ = 1 / (6 π G t²)` and `p = 0`; `q = 1 / 2` and `H(t₀) = 2 / (3 t₀)`. +- `milneScaleFactor_firstOrderFriedmann`, `milneScaleFactor_secondOrderFriedmann`: the Milne + scale factor `a = c t` solves the empty (`ρ = 0`, `p = 0`, `Λ = 0`) Friedmann equations with + `k = -1`; `q = 0`. +- `einsteinStatic_density`, `einsteinStatic_curvature`: if `∂ₜ a = ∂ₜ ∂ₜ a = 0` at `t` and the + Friedmann equations hold there with `p = 0`, then `ρ = Λ c² / (4 π G) = 2 ρ_Λ` and + `k c² / a² = 4 π G ρ`, so that `k > 0` when `ρ > 0` (`einsteinStatic_curvature_pos`). ## iii. Table of contents @@ -56,7 +64,9 @@ coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridg - C.2. The Hubble and deceleration parameters - C.3. The radiation-dominated solution - C.4. The Einstein-de Sitter solution -- D. Remaining TODO items +- D. The Milne solution +- E. The Einstein static universe +- F. Remaining TODO items -/ @@ -427,14 +437,117 @@ lemma hubbleConstant_einsteinDeSitterScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < /-! -## D. Remaining TODO items +## D. The Milne solution + +The Milne universe is the empty (`ρ = 0`, `p = 0`, `Λ = 0`) solution with `k = -1` and +`a(t) = c t` for `t > 0`. That it is Minkowski space in expanding coordinates (vanishing +curvature) is not stated here: the FLRW metric is not yet an object of Physlib. + +-/ + +/-- The Milne scale factor `a(t) = c t`. -/ +noncomputable def milneScaleFactor (c : ℝ) : Time → ℝ := + fun t => c * t.val + +lemma deriv_milneScaleFactor (c : ℝ) : ∂ₜ (milneScaleFactor c) = fun _ => c := by + funext t + exact deriv_comp_val (((hasDerivAt_id t.val).const_mul c).congr_deriv (mul_one c)) + +lemma deriv_deriv_milneScaleFactor (c : ℝ) : ∂ₜ (∂ₜ (milneScaleFactor c)) = fun _ => 0 := by + rw [deriv_milneScaleFactor] + funext t + exact deriv_comp_val (γ := fun _ => c) (hasDerivAt_const t.val c) + +/-- The Milne solution solves the first-order Friedmann equation with `ρ = 0`, `k = -1` and + `Λ = 0`, for `t > 0`. -/ +lemma milneScaleFactor_firstOrderFriedmann {G c : ℝ} (hc : 0 < c) {t : Time} (ht : 0 < t.val) : + FirstOrderFriedmann (milneScaleFactor c) (fun _ => 0) (-1) 0 G c t := by + unfold FirstOrderFriedmann + rw [deriv_milneScaleFactor] + simp only [milneScaleFactor] + field_simp + ring + +/-- The Milne solution solves the second-order Friedmann equation with `ρ = 0`, `p = 0` and + `Λ = 0`. -/ +lemma milneScaleFactor_secondOrderFriedmann {G c : ℝ} (t : Time) : + SecondOrderFriedmann (milneScaleFactor c) (fun _ => 0) (fun _ => 0) 0 G c t := by + unfold SecondOrderFriedmann + rw [deriv_deriv_milneScaleFactor] + simp + +/-- The deceleration parameter of the Milne solution is `q = 0`. -/ +lemma decelerationParameter_milneScaleFactor (c : ℝ) (t : Time) : + decelerationParameter (milneScaleFactor c) t = 0 := by + unfold decelerationParameter + rw [deriv_deriv_milneScaleFactor, deriv_milneScaleFactor] + simp + +/-! + +## E. The Einstein static universe + +At an instant where `∂ₜ a = ∂ₜ ∂ₜ a = 0`, the two Friedmann equations with dust (`p = 0`) +force the density `ρ = Λ c² / (4 π G)`, twice the density `ρ_Λ = Λ c² / (8 π G)` associated +with the cosmological constant, and `k c² / a² = 4 π G ρ`, hence a positive curvature +parameter when `ρ > 0`. That this equilibrium is unstable is not stated here. + +-/ + +/-- The density `ρ_Λ = Λ c² / (8 π G)` associated with the cosmological constant. -/ +noncomputable def cosmologicalConstantDensity (Λ G c : ℝ) : ℝ := + Λ * c ^ 2 / (8 * π * G) + +/-- In the Einstein static universe the dust density is `ρ = Λ c² / (4 π G) = 2 ρ_Λ`. -/ +lemma einsteinStatic_density {a ρ : Time → ℝ} {Λ G c : ℝ} {t : Time} (hG : 0 < G) + (h2 : ∂ₜ (∂ₜ a) t = 0) (hF2 : SecondOrderFriedmann a ρ (fun _ => 0) Λ G c t) : + ρ t = 2 * cosmologicalConstantDensity Λ G c := by + unfold SecondOrderFriedmann at hF2 + rw [h2, zero_div] at hF2 + simp only [mul_zero, zero_div, add_zero] at hF2 + unfold cosmologicalConstantDensity + have hπ := Real.pi_pos + field_simp + linarith + +/-- In the Einstein static universe `k c² / a² = 4 π G ρ`. -/ +lemma einsteinStatic_curvature {a ρ : Time → ℝ} {k Λ G c : ℝ} {t : Time} + (h1 : ∂ₜ a t = 0) (h2 : ∂ₜ (∂ₜ a) t = 0) (hF1 : FirstOrderFriedmann a ρ k Λ G c t) + (hF2 : SecondOrderFriedmann a ρ (fun _ => 0) Λ G c t) : + k * c ^ 2 / (a t) ^ 2 = 4 * π * G * ρ t := by + unfold FirstOrderFriedmann at hF1 + unfold SecondOrderFriedmann at hF2 + rw [h1, zero_div] at hF1 + rw [h2, zero_div] at hF2 + simp only [mul_zero, zero_div, add_zero] at hF1 hF2 + linarith + +/-- In the Einstein static universe with positive density, the curvature parameter is + positive. -/ +lemma einsteinStatic_curvature_pos {a ρ : Time → ℝ} {k Λ G c : ℝ} {t : Time} (hG : 0 < G) + (hc : 0 < c) (ha : a t ≠ 0) (hρ : 0 < ρ t) (h1 : ∂ₜ a t = 0) (h2 : ∂ₜ (∂ₜ a) t = 0) + (hF1 : FirstOrderFriedmann a ρ k Λ G c t) + (hF2 : SecondOrderFriedmann a ρ (fun _ => 0) Λ G c t) : + 0 < k := by + have h := einsteinStatic_curvature h1 h2 hF1 hF2 + have hpos : 0 < k * c ^ 2 / (a t) ^ 2 := by + rw [h] + positivity + have ha2 : 0 < (a t) ^ 2 := by positivity + have hc2 : 0 < c ^ 2 := by positivity + rw [div_pos_iff_of_pos_right ha2] at hpos + exact (mul_pos_iff_of_pos_right hc2).mp hpos + +/-! + +## F. Remaining TODO items -/ -TODO "Prove that the Milne solution `a = c t` (empty universe, `K < 0`) has +TODO "Prove that the Milne solution `milneScaleFactor` (empty universe, `K < 0`) has vanishing scalar curvature, i.e. it is Minkowski space in expanding coordinates." -TODO "Define the Einstein static universe (`∂ₜ a = ∂ₜ ∂ₜ a = 0`, forcing `K > 0` - and `ρ_m = 2 ρ_Λ`) and prove that it is an unstable equilibrium." +TODO "Prove that the Einstein static universe (`∂ₜ a = ∂ₜ ∂ₜ a = 0`, `einsteinStatic_density`, + `einsteinStatic_curvature`) is an unstable equilibrium." end Cosmology.FLRW.FriedmannEquation From 9a7000fccb99b20b275f083e0b7d2f3fdc359d91 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 10 Sep 2026 20:16:21 +0200 Subject: [PATCH 04/20] feat(Cosmology): continuity equation of the cosmic fluid from the Friedmann equations Adds to Physlib/Cosmology/FLRW/MatterContent.lean the predicate ContinuityEquation, the derivative of the first-order Friedmann equation (deriv_firstOrderFriedmann), the derivation of the continuity equation from the two Friedmann equations (continuityEquation_of_friedmann) and the converse derivation of the second-order equation from the first-order and continuity equations (secondOrderFriedmann_of_continuityEquation), resolving two TODOs of the file. Also hasDerivAt_mk_of_differentiableAt, the bridge from a time derivative to HasDerivAt. Generated with Claude Code under human supervision (see AI-POLICY.md). Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/MatterContent.lean | 171 ++++++++++++++++++++-- 1 file changed, 158 insertions(+), 13 deletions(-) diff --git a/Physlib/Cosmology/FLRW/MatterContent.lean b/Physlib/Cosmology/FLRW/MatterContent.lean index 2b257245e0..6e37bf8c1d 100644 --- a/Physlib/Cosmology/FLRW/MatterContent.lean +++ b/Physlib/Cosmology/FLRW/MatterContent.lean @@ -1,34 +1,177 @@ /- Copyright (c) 2026 Jinzheng Li. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jinzheng Li +Authors: Jinzheng Li, Philippe Kevorkian -/ module public import Physlib.Meta.TODO.Basic +public import Physlib.Cosmology.FLRW.Basic /-! # Matter content of FLRW cosmology -Placeholder file collecting TODO items for the matter content of a -Friedmann-Lemaître-Robertson-Walker universe: the perfect-fluid stress-energy -tensor, the equation of state, the continuity equation, and the resulting -density scaling for the standard components (dust, radiation, vacuum energy). -This file contains only TODO items; no definitions or lemmas are formalized yet. +## i. Overview + +This file describes the matter content of a Friedmann-Lemaître-Robertson-Walker universe +through the continuity equation `∂ₜ ρ + 3 H (ρ + p / c²) = 0` of the cosmic fluid and its +relation to the two Friedmann equations of `Physlib.Cosmology.FLRW.Basic`: the continuity +equation follows from the first-order equation (holding at all times) and the second-order +equation, and conversely the second-order equation follows from the first-order equation and +the continuity equation whenever `∂ₜ a ≠ 0`. The three equations are therefore not +independent. The equation of state, the density scaling laws and the perfect-fluid +stress-energy tensor are still TODO items. + +Time derivatives of curves `Time → ℝ` are computed through the bridge +`Time.hasDerivAt_comp_toRealCLE_symm` to Mathlib's `HasDerivAt` on `ℝ`. + +## ii. Key results + +- `ContinuityEquation`: the continuity equation at an instant `t`. +- `deriv_firstOrderFriedmann`: the time derivative of the first-order Friedmann equation, + `2 H (a''/a - H²) = (8 π G / 3) ρ' + 2 k c² H / a²`. +- `continuityEquation_of_friedmann`: the continuity equation follows from the two Friedmann + equations. +- `secondOrderFriedmann_of_continuityEquation`: the second-order Friedmann equation follows + from the first-order equation and the continuity equation when `∂ₜ a ≠ 0`. + +## iii. Table of contents + +- A. Time derivatives through the coordinate +- B. The continuity equation + - B.1. The definition + - B.2. The derivative of the first-order Friedmann equation + - B.3. Continuity from the Friedmann equations + - B.4. The second-order Friedmann equation from continuity +- C. Remaining TODO items -/ @[expose] public section -TODO "Define the perfect-fluid stress-energy tensor - `T_{μν} = (ρ + P/c²) u_μ u_ν + P g_{μν}` for the FLRW metric." +namespace Cosmology.FLRW.FriedmannEquation + +open Real Time + +/-! + +## A. Time derivatives through the coordinate + +-/ + +/-- A curve `f : Time → ℝ` differentiable at `⟨τ⟩` gives the curve `σ ↦ f ⟨σ⟩` on `ℝ`, + whose Mathlib derivative at `τ` is the time derivative `∂ₜ f ⟨τ⟩`. -/ +lemma hasDerivAt_mk_of_differentiableAt {f : Time → ℝ} {τ : ℝ} + (hf : DifferentiableAt ℝ f ⟨τ⟩) : + HasDerivAt (fun σ : ℝ => f ⟨σ⟩) (∂ₜ f ⟨τ⟩) τ := + hasDerivAt_comp_toRealCLE_symm f τ hf + +/-! -TODO "Define the continuity equation `∂ₜ ρ + 3 H (ρ + P/c²) = 0` and derive it from - the first- and second-order Friedmann equations." +## B. The continuity equation -TODO "Prove that the Friedmann equation, the acceleration equation and the - continuity equation are not independent (a consequence of the Bianchi identity - `∇_ν Gᵘᵛ = 0`)." +-/ + +/-! + +### B.1. The definition + +-/ + +/-- The continuity equation of the cosmic fluid at the instant `t`: + `∂ₜ ρ + 3 H (ρ + p / c²) = 0`, with `H = hubbleConstant a`. -/ +def ContinuityEquation (a ρ p : Time → ℝ) (c : ℝ) (t : Time) : Prop := + ∂ₜ ρ t + 3 * hubbleConstant a t * (ρ t + p t / c ^ 2) = 0 + +/-! + +### B.2. The derivative of the first-order Friedmann equation + +-/ + +/-- Differentiating the first-order Friedmann equation, assumed at all times, at `⟨τ⟩`: + `2 H (a''/a - H²) = (8 π G / 3) ρ' + 2 k c² H / a²`. -/ +lemma deriv_firstOrderFriedmann {a ρ : Time → ℝ} {k Λ G c τ : ℝ} (ha : a ⟨τ⟩ ≠ 0) + (hd1 : DifferentiableAt ℝ a ⟨τ⟩) (hd2 : DifferentiableAt ℝ (∂ₜ a) ⟨τ⟩) + (hdρ : DifferentiableAt ℝ ρ ⟨τ⟩) (hF1 : ∀ s, FirstOrderFriedmann a ρ k Λ G c s) : + 2 * (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) * (∂ₜ (∂ₜ a) ⟨τ⟩ / a ⟨τ⟩ - (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) ^ 2) + = 8 * π * G / 3 * ∂ₜ ρ ⟨τ⟩ + + 2 * k * c ^ 2 * (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) / (a ⟨τ⟩) ^ 2 := by + have hA := hasDerivAt_mk_of_differentiableAt hd1 + have hA' := hasDerivAt_mk_of_differentiableAt hd2 + have hR := hasDerivAt_mk_of_differentiableAt hdρ + have hL := (hA'.div hA ha).pow 2 + have hRd := ((hR.const_mul (8 * π * G / 3)).sub + ((hasDerivAt_const τ (k * c ^ 2)).div (hA.pow 2) (pow_ne_zero 2 ha))).add_const + (Λ * c ^ 2 / 3) + have hu := hL.unique + (hRd.congr_of_eventuallyEq (Filter.Eventually.of_forall fun σ => hF1 ⟨σ⟩)) + simp only [Pi.pow_apply, Pi.div_apply, Nat.cast_ofNat, Nat.add_one_sub_one, pow_one, zero_mul, + zero_sub] at hu + field_simp at hu ⊢ + linear_combination hu + +/-! + +### B.3. Continuity from the Friedmann equations + +-/ + +/-- The continuity equation follows from the first-order Friedmann equation, assumed at all + times, and the second-order Friedmann equation at `t`; `a` must be twice differentiable and + `ρ` differentiable at `t`. -/ +lemma continuityEquation_of_friedmann {a ρ p : Time → ℝ} {k Λ G c : ℝ} {t : Time} + (hG : 0 < G) (ha : a t ≠ 0) (hd1 : DifferentiableAt ℝ a t) + (hd2 : DifferentiableAt ℝ (∂ₜ a) t) + (hdρ : DifferentiableAt ℝ ρ t) (hF1 : ∀ s, FirstOrderFriedmann a ρ k Λ G c s) + (hF2 : SecondOrderFriedmann a ρ p Λ G c t) : + ContinuityEquation a ρ p c t := by + obtain ⟨τ⟩ := t + have hd := deriv_firstOrderFriedmann ha hd1 hd2 hdρ hF1 + have h1 := hF1 ⟨τ⟩ + unfold FirstOrderFriedmann at h1 + unfold SecondOrderFriedmann at hF2 + unfold ContinuityEquation hubbleConstant + have hπ := Real.pi_pos + have hG3 : 8 * π * G / 3 ≠ 0 := by positivity + apply mul_left_cancel₀ hG3 + linear_combination -hd + 2 * (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) * hF2 + - 2 * (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) * h1 + +/-! + +### B.4. The second-order Friedmann equation from continuity + +-/ + +/-- The second-order Friedmann equation at `t` follows from the first-order Friedmann + equation, assumed at all times, and the continuity equation at `t`, provided `∂ₜ a t ≠ 0`. + Together with `continuityEquation_of_friedmann`, the three equations are not independent. -/ +lemma secondOrderFriedmann_of_continuityEquation {a ρ p : Time → ℝ} {k Λ G c : ℝ} + {t : Time} (ha : a t ≠ 0) (hd1' : ∂ₜ a t ≠ 0) (hd1 : DifferentiableAt ℝ a t) + (hd2 : DifferentiableAt ℝ (∂ₜ a) t) (hdρ : DifferentiableAt ℝ ρ t) + (hF1 : ∀ s, FirstOrderFriedmann a ρ k Λ G c s) (hC : ContinuityEquation a ρ p c t) : + SecondOrderFriedmann a ρ p Λ G c t := by + obtain ⟨τ⟩ := t + have hd := deriv_firstOrderFriedmann ha hd1 hd2 hdρ hF1 + have h1 := hF1 ⟨τ⟩ + unfold FirstOrderFriedmann at h1 + unfold ContinuityEquation hubbleConstant at hC + unfold SecondOrderFriedmann + have hH : 2 * (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) ≠ 0 := by + have : ∂ₜ a ⟨τ⟩ / a ⟨τ⟩ ≠ 0 := div_ne_zero hd1' ha + positivity + apply mul_left_cancel₀ hH + linear_combination hd + 8 * π * G / 3 * hC + 2 * (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) * h1 + +/-! + +## C. Remaining TODO items + +-/ + +TODO "Define the perfect-fluid stress-energy tensor + `T_{μν} = (ρ + P/c²) u_μ u_ν + P g_{μν}` for the FLRW metric." TODO "Define the linear (barotropic) equation of state `P = w ρ c²` and prove the density scaling law `ρ = ρ₀ a^(−3(1+w))` for constant `w`." @@ -38,3 +181,5 @@ TODO "Specialize the density scaling law to dust (`w = 0`, `ρ ∝ a⁻³`), rad TODO "Prove that the cosmological constant acts as a `w = −1` perfect fluid with `ρ_Λ = Λ c² / (8 π G)` and `P_Λ = −ρ_Λ c²`." + +end Cosmology.FLRW.FriedmannEquation From d5f24a547474a0fbcad5579ae155fe8d6b12f1ba Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 10 Sep 2026 20:16:30 +0200 Subject: [PATCH 05/20] feat(Cosmology): barotropic equation of state, density scaling laws, cosmological constant as a fluid Adds to Physlib/Cosmology/FLRW/MatterContent.lean barotropicPressure, the density scaling law density_scaling with its converse continuityEquation_of_scaling and the dust, radiation and vacuum specialisations, and cosmologicalConstantDensity and cosmologicalConstantPressure with firstOrderFriedmann_iff_lambdaFluid, secondOrderFriedmann_iff_lambdaFluid and cosmologicalConstantPressure_eq_barotropic, resolving three TODOs. Moves cosmologicalConstantDensity from Solutions.lean, which now imports MatterContent. Generated with Claude Code under human supervision (see AI-POLICY.md). Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/MatterContent.lean | 203 ++++++++++++++++++++-- Physlib/Cosmology/FLRW/Solutions.lean | 13 +- 2 files changed, 196 insertions(+), 20 deletions(-) diff --git a/Physlib/Cosmology/FLRW/MatterContent.lean b/Physlib/Cosmology/FLRW/MatterContent.lean index 6e37bf8c1d..13d5982865 100644 --- a/Physlib/Cosmology/FLRW/MatterContent.lean +++ b/Physlib/Cosmology/FLRW/MatterContent.lean @@ -7,6 +7,7 @@ module public import Physlib.Meta.TODO.Basic public import Physlib.Cosmology.FLRW.Basic +public import Mathlib.Analysis.SpecialFunctions.Pow.Deriv /-! # Matter content of FLRW cosmology @@ -19,8 +20,10 @@ relation to the two Friedmann equations of `Physlib.Cosmology.FLRW.Basic`: the c equation follows from the first-order equation (holding at all times) and the second-order equation, and conversely the second-order equation follows from the first-order equation and the continuity equation whenever `∂ₜ a ≠ 0`. The three equations are therefore not -independent. The equation of state, the density scaling laws and the perfect-fluid -stress-energy tensor are still TODO items. +independent. For a barotropic equation of state `p = w ρ c²` with constant `w`, the continuity +equation gives the density scaling law `ρ ∝ a^(-3(1+w))`, specialised to dust, radiation and +vacuum energy; and the cosmological constant is equivalent to a `w = -1` fluid of density +`ρ_Λ = Λ c² / (8 π G)`. The perfect-fluid stress-energy tensor is still a TODO item. Time derivatives of curves `Time → ℝ` are computed through the bridge `Time.hasDerivAt_comp_toRealCLE_symm` to Mathlib's `HasDerivAt` on `ℝ`. @@ -34,6 +37,15 @@ Time derivatives of curves `Time → ℝ` are computed through the bridge equations. - `secondOrderFriedmann_of_continuityEquation`: the second-order Friedmann equation follows from the first-order equation and the continuity equation when `∂ₜ a ≠ 0`. +- `barotropicPressure`: `p = w ρ c²`; `density_scaling`: under the barotropic continuity + equation at all times, `ρ t = ρ t₀ (a t / a t₀)^(-3(1+w))`; `continuityEquation_of_scaling`: + the converse; `density_scaling_dust`, `density_scaling_radiation`, + `density_scaling_vacuum`: `ρ ∝ a⁻³`, `ρ ∝ a⁻⁴`, `ρ` constant. +- `cosmologicalConstantDensity`, `cosmologicalConstantPressure`: + `ρ_Λ = Λ c² / (8 π G)`, `p_Λ = - ρ_Λ c²`; `firstOrderFriedmann_iff_lambdaFluid`, + `secondOrderFriedmann_iff_lambdaFluid`: the Friedmann equations with `Λ` are the Friedmann + equations without `Λ` for the fluid `ρ + ρ_Λ`, `p + p_Λ`; + `cosmologicalConstantPressure_eq_barotropic`: `p_Λ` is the `w = -1` barotropic pressure. ## iii. Table of contents @@ -43,7 +55,12 @@ Time derivatives of curves `Time → ℝ` are computed through the bridge - B.2. The derivative of the first-order Friedmann equation - B.3. Continuity from the Friedmann equations - B.4. The second-order Friedmann equation from continuity -- C. Remaining TODO items +- C. The barotropic equation of state and the density scaling law + - C.1. The equation of state + - C.2. The density scaling law + - C.3. Dust, radiation and vacuum energy +- D. The cosmological constant as a fluid +- E. Remaining TODO items -/ @@ -166,20 +183,182 @@ lemma secondOrderFriedmann_of_continuityEquation {a ρ p : Time → ℝ} {k Λ G /-! -## C. Remaining TODO items +## C. The barotropic equation of state and the density scaling law -/ -TODO "Define the perfect-fluid stress-energy tensor - `T_{μν} = (ρ + P/c²) u_μ u_ν + P g_{μν}` for the FLRW metric." +/-! -TODO "Define the linear (barotropic) equation of state `P = w ρ c²` and prove the - density scaling law `ρ = ρ₀ a^(−3(1+w))` for constant `w`." +### C.1. The equation of state + +-/ + +/-- The barotropic pressure `p = w ρ c²` with constant equation-of-state parameter `w`. -/ +noncomputable def barotropicPressure (w : ℝ) (ρ : Time → ℝ) (c : ℝ) : Time → ℝ := + fun t => w * ρ t * c ^ 2 + +/-- Under the barotropic continuity equation, `∂ₜ ρ = -3 (1 + w) H ρ`. -/ +lemma deriv_of_continuityEquation_barotropic {a ρ : Time → ℝ} {w c : ℝ} {t : Time} (hc : c ≠ 0) + (hC : ContinuityEquation a ρ (barotropicPressure w ρ c) c t) : + ∂ₜ ρ t = -3 * (1 + w) * hubbleConstant a t * ρ t := by + unfold ContinuityEquation barotropicPressure at hC + have h : w * ρ t * c ^ 2 / c ^ 2 = w * ρ t := by + field_simp + rw [h] at hC + linear_combination hC + +/-! + +### C.2. The density scaling law + +-/ + +/-- Under the barotropic continuity equation at all times, the curve `σ ↦ ρ ⟨σ⟩ a ⟨σ⟩^(3(1+w))` + has zero derivative. -/ +lemma hasDerivAt_mul_rpow_of_continuityEquation {a ρ : Time → ℝ} {w c : ℝ} (hc : c ≠ 0) + (hd1 : Differentiable ℝ a) (hdρ : Differentiable ℝ ρ) (hapos : ∀ s, 0 < a s) + (hC : ∀ s, ContinuityEquation a ρ (barotropicPressure w ρ c) c s) (τ : ℝ) : + HasDerivAt (fun σ : ℝ => ρ ⟨σ⟩ * a ⟨σ⟩ ^ (3 * (1 + w))) 0 τ := by + have hA := hasDerivAt_mk_of_differentiableAt (hd1 ⟨τ⟩) + have hR := hasDerivAt_mk_of_differentiableAt (hdρ ⟨τ⟩) + have hP := hA.rpow_const (p := 3 * (1 + w)) (Or.inl (hapos ⟨τ⟩).ne') + refine (hR.mul hP).congr_deriv ?_ + rw [deriv_of_continuityEquation_barotropic hc (hC ⟨τ⟩), Real.rpow_sub_one (hapos ⟨τ⟩).ne'] + unfold hubbleConstant + field_simp + ring + +/-- The density scaling law: under the barotropic continuity equation at all times, with `a` + and `ρ` differentiable and `a > 0`, `ρ t = ρ t₀ (a t / a t₀)^(-3(1+w))`. -/ +lemma density_scaling {a ρ : Time → ℝ} {w c : ℝ} (hc : c ≠ 0) (hd1 : Differentiable ℝ a) + (hdρ : Differentiable ℝ ρ) (hapos : ∀ s, 0 < a s) + (hC : ∀ s, ContinuityEquation a ρ (barotropicPressure w ρ c) c s) (t t₀ : Time) : + ρ t = ρ t₀ * (a t / a t₀) ^ (-(3 * (1 + w))) := by + have hconst := is_const_of_deriv_eq_zero + (fun τ => (hasDerivAt_mul_rpow_of_continuityEquation hc hd1 hdρ hapos hC τ).differentiableAt) + (fun τ => (hasDerivAt_mul_rpow_of_continuityEquation hc hd1 hdρ hapos hC τ).deriv) + obtain ⟨τ⟩ := t + obtain ⟨τ₀⟩ := t₀ + have h := hconst τ τ₀ + beta_reduce at h + have h1 := Real.rpow_pos_of_pos (hapos ⟨τ⟩) (3 * (1 + w)) + have h0 := Real.rpow_pos_of_pos (hapos ⟨τ₀⟩) (3 * (1 + w)) + rw [Real.rpow_neg (div_pos (hapos ⟨τ⟩) (hapos ⟨τ₀⟩)).le, + Real.div_rpow (hapos ⟨τ⟩).le (hapos ⟨τ₀⟩).le] + field_simp + linear_combination h + +/-- Conversely, `ρ = ρ₀ (a / a₀)^(-3(1+w))` satisfies the barotropic continuity equation at + all times, for `a` differentiable and positive. -/ +lemma continuityEquation_of_scaling {a : Time → ℝ} {w c ρ₀ a₀ : ℝ} (hc : c ≠ 0) (ha₀ : a₀ ≠ 0) + (hd1 : Differentiable ℝ a) (hapos : ∀ s, 0 < a s) (t : Time) : + ContinuityEquation a (fun s => ρ₀ * (a s / a₀) ^ (-(3 * (1 + w)))) + (barotropicPressure w (fun s => ρ₀ * (a s / a₀) ^ (-(3 * (1 + w)))) c) c t := by + obtain ⟨τ⟩ := t + have hA := hasDerivAt_mk_of_differentiableAt (hd1 ⟨τ⟩) + have hx : a ⟨τ⟩ / a₀ ≠ 0 := div_ne_zero (hapos ⟨τ⟩).ne' ha₀ + have hP := ((hA.div_const a₀).rpow_const (p := -(3 * (1 + w))) (Or.inl hx)).const_mul ρ₀ + have hd : ∂ₜ (fun s : Time => ρ₀ * (a s / a₀) ^ (-(3 * (1 + w)))) ⟨τ⟩ + = ρ₀ * (∂ₜ a ⟨τ⟩ / a₀ * -(3 * (1 + w)) * (a ⟨τ⟩ / a₀) ^ (-(3 * (1 + w)) - 1)) := + deriv_comp_toRealCLE_of_hasDerivAt (fun σ => ρ₀ * (a ⟨σ⟩ / a₀) ^ (-(3 * (1 + w)))) ⟨τ⟩ _ hP + unfold ContinuityEquation barotropicPressure hubbleConstant + rw [hd, Real.rpow_sub_one hx] + have ha := (hapos ⟨τ⟩).ne' + field_simp + ring + +/-! -TODO "Specialize the density scaling law to dust (`w = 0`, `ρ ∝ a⁻³`), radiation - (`w = 1/3`, `ρ ∝ a⁻⁴`) and vacuum energy (`w = −1`, `ρ` constant)." +### C.3. Dust, radiation and vacuum energy -TODO "Prove that the cosmological constant acts as a `w = −1` perfect fluid with - `ρ_Λ = Λ c² / (8 π G)` and `P_Λ = −ρ_Λ c²`." +-/ + +/-- Dust, `w = 0`: `ρ ∝ a⁻³`. -/ +lemma density_scaling_dust {a ρ : Time → ℝ} {c : ℝ} (hc : c ≠ 0) (hd1 : Differentiable ℝ a) + (hdρ : Differentiable ℝ ρ) (hapos : ∀ s, 0 < a s) + (hC : ∀ s, ContinuityEquation a ρ (barotropicPressure 0 ρ c) c s) (t t₀ : Time) : + ρ t = ρ t₀ * (a t₀ / a t) ^ 3 := by + rw [density_scaling hc hd1 hdρ hapos hC t t₀] + have hx : 0 < a t / a t₀ := div_pos (hapos t) (hapos t₀) + rw [show -(3 * (1 + (0 : ℝ))) = -((3 : ℕ) : ℝ) by norm_num, Real.rpow_neg hx.le, + Real.rpow_natCast, ← inv_pow, inv_div] + +/-- Radiation, `w = 1/3`: `ρ ∝ a⁻⁴`. -/ +lemma density_scaling_radiation {a ρ : Time → ℝ} {c : ℝ} (hc : c ≠ 0) (hd1 : Differentiable ℝ a) + (hdρ : Differentiable ℝ ρ) (hapos : ∀ s, 0 < a s) + (hC : ∀ s, ContinuityEquation a ρ (barotropicPressure (1 / 3) ρ c) c s) (t t₀ : Time) : + ρ t = ρ t₀ * (a t₀ / a t) ^ 4 := by + rw [density_scaling hc hd1 hdρ hapos hC t t₀] + have hx : 0 < a t / a t₀ := div_pos (hapos t) (hapos t₀) + rw [show -(3 * (1 + (1 / 3 : ℝ))) = -((4 : ℕ) : ℝ) by norm_num, Real.rpow_neg hx.le, + Real.rpow_natCast, ← inv_pow, inv_div] + +/-- Vacuum energy, `w = -1`: `ρ` is constant. -/ +lemma density_scaling_vacuum {a ρ : Time → ℝ} {c : ℝ} (hc : c ≠ 0) (hd1 : Differentiable ℝ a) + (hdρ : Differentiable ℝ ρ) (hapos : ∀ s, 0 < a s) + (hC : ∀ s, ContinuityEquation a ρ (barotropicPressure (-1) ρ c) c s) (t t₀ : Time) : + ρ t = ρ t₀ := by + rw [density_scaling hc hd1 hdρ hapos hC t t₀, + show -(3 * (1 + (-1 : ℝ))) = 0 by norm_num, Real.rpow_zero, mul_one] + +/-! + +## D. The cosmological constant as a fluid + +-/ + +/-- The density `ρ_Λ = Λ c² / (8 π G)` associated with the cosmological constant. -/ +noncomputable def cosmologicalConstantDensity (Λ G c : ℝ) : ℝ := + Λ * c ^ 2 / (8 * π * G) + +/-- The pressure `p_Λ = - ρ_Λ c²` associated with the cosmological constant. -/ +noncomputable def cosmologicalConstantPressure (Λ G c : ℝ) : ℝ := + -(cosmologicalConstantDensity Λ G c) * c ^ 2 + +/-- The first-order Friedmann equation with `Λ` is the first-order Friedmann equation without + `Λ` for the density `ρ + ρ_Λ`. -/ +lemma firstOrderFriedmann_iff_lambdaFluid {a ρ : Time → ℝ} {k Λ G c : ℝ} {t : Time} + (hG : G ≠ 0) : + FirstOrderFriedmann a ρ k Λ G c t ↔ + FirstOrderFriedmann a (fun s => ρ s + cosmologicalConstantDensity Λ G c) k 0 G c t := by + unfold FirstOrderFriedmann cosmologicalConstantDensity + have hπ := Real.pi_ne_zero + have key : 8 * π * G / 3 * ρ t - k * c ^ 2 / a t ^ 2 + Λ * c ^ 2 / 3 + = 8 * π * G / 3 * (ρ t + Λ * c ^ 2 / (8 * π * G)) - k * c ^ 2 / a t ^ 2 + 0 * c ^ 2 / 3 := by + field_simp + ring + rw [key] + +/-- The second-order Friedmann equation with `Λ` is the second-order Friedmann equation + without `Λ` for the density `ρ + ρ_Λ` and the pressure `p + p_Λ`. -/ +lemma secondOrderFriedmann_iff_lambdaFluid {a ρ p : Time → ℝ} {Λ G c : ℝ} {t : Time} + (hG : G ≠ 0) (hc : c ≠ 0) : + SecondOrderFriedmann a ρ p Λ G c t ↔ + SecondOrderFriedmann a (fun s => ρ s + cosmologicalConstantDensity Λ G c) + (fun s => p s + cosmologicalConstantPressure Λ G c) 0 G c t := by + unfold SecondOrderFriedmann cosmologicalConstantPressure cosmologicalConstantDensity + have hπ := Real.pi_ne_zero + have key : -(4 * π * G / 3) * (ρ t + 3 * p t / c ^ 2) + Λ * c ^ 2 / 3 + = -(4 * π * G / 3) * (ρ t + Λ * c ^ 2 / (8 * π * G) + + 3 * (p t + -(Λ * c ^ 2 / (8 * π * G)) * c ^ 2) / c ^ 2) + 0 * c ^ 2 / 3 := by + field_simp + ring + rw [key] + +/-- `p_Λ` is the barotropic pressure of `ρ_Λ` with `w = -1`. -/ +lemma cosmologicalConstantPressure_eq_barotropic (Λ G c : ℝ) (t : Time) : + cosmologicalConstantPressure Λ G c + = barotropicPressure (-1) (fun _ => cosmologicalConstantDensity Λ G c) c t := by + unfold cosmologicalConstantPressure barotropicPressure + ring + +/-! + +## E. Remaining TODO items + +-/ + +TODO "Define the perfect-fluid stress-energy tensor + `T_{μν} = (ρ + P/c²) u_μ u_ν + P g_{μν}` for the FLRW metric." end Cosmology.FLRW.FriedmannEquation diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index 97933c3239..e06b2ae50e 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -6,7 +6,7 @@ Authors: Jinzheng Li, Philippe Kevorkian module public import Physlib.Meta.TODO.Basic -public import Physlib.Cosmology.FLRW.Basic +public import Physlib.Cosmology.FLRW.MatterContent public import Mathlib.Analysis.SpecialFunctions.Pow.Deriv /-! @@ -488,16 +488,13 @@ lemma decelerationParameter_milneScaleFactor (c : ℝ) (t : Time) : ## E. The Einstein static universe At an instant where `∂ₜ a = ∂ₜ ∂ₜ a = 0`, the two Friedmann equations with dust (`p = 0`) -force the density `ρ = Λ c² / (4 π G)`, twice the density `ρ_Λ = Λ c² / (8 π G)` associated -with the cosmological constant, and `k c² / a² = 4 π G ρ`, hence a positive curvature -parameter when `ρ > 0`. That this equilibrium is unstable is not stated here. +force the density `ρ = Λ c² / (4 π G)`, twice the density `cosmologicalConstantDensity` +(`ρ_Λ = Λ c² / (8 π G)`, defined in `Physlib.Cosmology.FLRW.MatterContent`), and +`k c² / a² = 4 π G ρ`, hence a positive curvature parameter when `ρ > 0`. That this +equilibrium is unstable is not stated here. -/ -/-- The density `ρ_Λ = Λ c² / (8 π G)` associated with the cosmological constant. -/ -noncomputable def cosmologicalConstantDensity (Λ G c : ℝ) : ℝ := - Λ * c ^ 2 / (8 * π * G) - /-- In the Einstein static universe the dust density is `ρ = Λ c² / (4 π G) = 2 ρ_Λ`. -/ lemma einsteinStatic_density {a ρ : Time → ℝ} {Λ G c : ℝ} {t : Time} (hG : 0 < G) (h2 : ∂ₜ (∂ₜ a) t = 0) (hF2 : SecondOrderFriedmann a ρ (fun _ => 0) Λ G c t) : From 4c6ea7f9db98c53753673aa1b684d810341d3c23 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 11 Sep 2026 09:30:20 +0200 Subject: [PATCH 06/20] chore(Cosmology): order authors alphabetically by last name Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/Solutions.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index 9d1281450a..465deb296d 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026 Jinzheng Li. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jinzheng Li, Philippe Kevorkian +Authors: Philippe Kevorkian, Jinzheng Li -/ module From 7ec56a8b8bc2304e4c95ab4e0f8ea64cb3ea2e6d Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 11 Sep 2026 09:30:20 +0200 Subject: [PATCH 07/20] chore(Cosmology): order authors alphabetically by last name Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/Solutions.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index 97933c3239..8480c23310 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026 Jinzheng Li. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jinzheng Li, Philippe Kevorkian +Authors: Philippe Kevorkian, Jinzheng Li -/ module From 6b52a4e65eec42c3f69b54addfac4ae6851416bb Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 11 Sep 2026 09:30:20 +0200 Subject: [PATCH 08/20] chore(Cosmology): order authors alphabetically by last name Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/MatterContent.lean | 2 +- Physlib/Cosmology/FLRW/Solutions.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Physlib/Cosmology/FLRW/MatterContent.lean b/Physlib/Cosmology/FLRW/MatterContent.lean index 6e37bf8c1d..a8cd19661d 100644 --- a/Physlib/Cosmology/FLRW/MatterContent.lean +++ b/Physlib/Cosmology/FLRW/MatterContent.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026 Jinzheng Li. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jinzheng Li, Philippe Kevorkian +Authors: Philippe Kevorkian, Jinzheng Li -/ module diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index 97933c3239..8480c23310 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026 Jinzheng Li. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jinzheng Li, Philippe Kevorkian +Authors: Philippe Kevorkian, Jinzheng Li -/ module From 0ed56f1b2a4e502e62f2dab10d3db532f110e459 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 11 Sep 2026 09:30:20 +0200 Subject: [PATCH 09/20] chore(Cosmology): order authors alphabetically by last name Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/MatterContent.lean | 2 +- Physlib/Cosmology/FLRW/Solutions.lean | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/Physlib/Cosmology/FLRW/MatterContent.lean b/Physlib/Cosmology/FLRW/MatterContent.lean index 13d5982865..f31b32b1e3 100644 --- a/Physlib/Cosmology/FLRW/MatterContent.lean +++ b/Physlib/Cosmology/FLRW/MatterContent.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026 Jinzheng Li. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jinzheng Li, Philippe Kevorkian +Authors: Philippe Kevorkian, Jinzheng Li -/ module diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index e06b2ae50e..d89d88d9c6 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2026 Jinzheng Li. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jinzheng Li, Philippe Kevorkian +Authors: Philippe Kevorkian, Jinzheng Li -/ module From 171e458745cd9699043dd5f8787364939e09eade Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 11 Sep 2026 10:58:30 +0200 Subject: [PATCH 10/20] style(Cosmology): inline one-off helper lemmas, move the Time derivative bridges next to their definition Applies the review remarks of #1642 across the series: no isolated general-purpose lemma, and lemmas about the time derivative live in SpaceAndTime/Time/Derivatives.lean. Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/Solutions.lean | 116 +++++++++------------ Physlib/SpaceAndTime/Time/Derivatives.lean | 11 ++ 2 files changed, 63 insertions(+), 64 deletions(-) diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index 465deb296d..05326f6124 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -46,17 +46,16 @@ coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridg ## iii. Table of contents -- A. Time derivatives of curves given by a function of the coordinate -- B. The de Sitter solution - - B.1. The scale factor and its derivatives - - B.2. The Friedmann equations - - B.3. The Hubble and deceleration parameters -- C. The spatially flat power-law solutions - - C.1. The power-law scale factor and its derivatives - - C.2. The Hubble and deceleration parameters - - C.3. The radiation-dominated solution - - C.4. The Einstein-de Sitter solution -- D. Remaining TODO items +- A. The de Sitter solution + - A.1. The scale factor and its derivatives + - A.2. The Friedmann equations + - A.3. The Hubble and deceleration parameters +- B. The spatially flat power-law solutions + - B.1. The power-law scale factor and its derivatives + - B.2. The Hubble and deceleration parameters + - B.3. The radiation-dominated solution + - B.4. The Einstein-de Sitter solution +- C. Remaining TODO items -/ @@ -68,33 +67,13 @@ open Real Time /-! -## A. Time derivatives of curves given by a function of the coordinate - -A curve `t ↦ γ t.val` on `Time` is the pull-back through `toRealCLE` of the curve `γ` on `ℝ`; -its time derivative is the Mathlib derivative of `γ`. - --/ - -/-- The time derivative of `t ↦ γ t.val` at `t` is the derivative of `γ` at `t.val`. -/ -lemma deriv_comp_val {γ : ℝ → ℝ} {t : Time} {v : ℝ} (h : HasDerivAt γ v t.val) : - ∂ₜ (fun s : Time => γ s.val) t = v := - deriv_comp_toRealCLE_of_hasDerivAt γ t v h - -/-- The time derivative of any `f : Time → ℝ` at `t` is the derivative at `t.val` of the curve - `τ ↦ f ⟨τ⟩` on `ℝ`. -/ -lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} - (h : HasDerivAt (fun τ : ℝ => f ⟨τ⟩) v t.val) : ∂ₜ f t = v := - deriv_comp_toRealCLE_of_hasDerivAt (fun τ : ℝ => f ⟨τ⟩) t v h - -/-! - -## B. The de Sitter solution +## A. The de Sitter solution -/ /-! -### B.1. The scale factor and its derivatives +### A.1. The scale factor and its derivatives -/ @@ -103,19 +82,17 @@ lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} noncomputable def deSitterScaleFactor (a₀ σ Λ c : ℝ) : Time → ℝ := fun t => a₀ * Real.exp (σ * √(Λ / 3) * c * t.val) -/-- Mathlib derivative of `y ↦ a₀ exp (K y)`. -/ -lemma hasDerivAt_mul_exp_mul (a₀ K x : ℝ) : - HasDerivAt (fun y : ℝ => a₀ * Real.exp (K * y)) (a₀ * K * Real.exp (K * x)) x := by - have h := (((hasDerivAt_id x).const_mul K).exp).const_mul a₀ - refine h.congr_deriv ?_ - simp only [id_eq] - ring - lemma deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : ∂ₜ (deSitterScaleFactor a₀ σ Λ c) = fun t => a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val) := by funext t - exact deriv_comp_val (hasDerivAt_mul_exp_mul a₀ (σ * √(Λ / 3) * c) t.val) + have h : HasDerivAt (fun y : ℝ => a₀ * Real.exp (σ * √(Λ / 3) * c * y)) + (a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val)) t.val := by + have h := (((hasDerivAt_id t.val).const_mul (σ * √(Λ / 3) * c)).exp).const_mul a₀ + refine h.congr_deriv ?_ + simp only [id_eq] + ring + exact deriv_comp_val h lemma deriv_deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : ∂ₜ (∂ₜ (deSitterScaleFactor a₀ σ Λ c)) = @@ -123,8 +100,15 @@ lemma deriv_deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : Real.exp (σ * √(Λ / 3) * c * t.val) := by rw [deriv_deSitterScaleFactor] funext t - exact deriv_comp_val - (hasDerivAt_mul_exp_mul (a₀ * (σ * √(Λ / 3) * c)) (σ * √(Λ / 3) * c) t.val) + have h : HasDerivAt (fun y : ℝ => a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * y)) + (a₀ * (σ * √(Λ / 3) * c) * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val)) + t.val := by + have h := (((hasDerivAt_id t.val).const_mul (σ * √(Λ / 3) * c)).exp).const_mul + (a₀ * (σ * √(Λ / 3) * c)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + exact deriv_comp_val h /-- `σ² (√(Λ/3))² c² = Λ c² / 3` for `σ = ±1` and `0 ≤ Λ`. -/ lemma sq_deSitterRate {σ Λ c : ℝ} (hΛ : 0 ≤ Λ) (hσ : σ = 1 ∨ σ = -1) : @@ -134,7 +118,7 @@ lemma sq_deSitterRate {σ Λ c : ℝ} (hΛ : 0 ≤ Λ) (hσ : σ = 1 ∨ σ = -1 /-! -### B.2. The Friedmann equations +### A.2. The Friedmann equations -/ @@ -169,7 +153,7 @@ lemma deSitterScaleFactor_secondOrderFriedmann {a₀ σ Λ G c : ℝ} (hΛ : 0 < /-! -### B.3. The Hubble and deceleration parameters +### A.3. The Hubble and deceleration parameters -/ @@ -202,7 +186,7 @@ lemma decelerationParameter_deSitterScaleFactor {a₀ σ Λ c : ℝ} (hΛ : 0 < /-! -## C. The spatially flat power-law solutions +## B. The spatially flat power-law solutions The radiation-dominated and Einstein-de Sitter solutions are both of the form `a(t) = (t / t₀) ^ n` for `t > 0`; the Hubble parameter is `n / t` and the deceleration @@ -213,7 +197,7 @@ parameter `(1 - n) / n`. Their densities are imposed by the first-order Friedman /-! -### C.1. The power-law scale factor and its derivatives +### B.1. The power-law scale factor and its derivatives -/ @@ -221,20 +205,17 @@ parameter `(1 - n) / n`. Their densities are imposed by the first-order Friedman noncomputable def powerLawScaleFactor (t₀ n : ℝ) : Time → ℝ := fun t => (t.val / t₀) ^ n -/-- Mathlib derivative of `y ↦ (y / t₀) ^ n` away from `y = 0`. -/ -lemma hasDerivAt_div_rpow {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {x : ℝ} (hx : x ≠ 0) : - HasDerivAt (fun y : ℝ => (y / t₀) ^ n) (n / t₀ * (x / t₀) ^ (n - 1)) x := by - have h := ((hasDerivAt_id x).div_const t₀).rpow_const (p := n) - (Or.inl (div_ne_zero hx ht₀)) - refine h.congr_deriv ?_ - simp only [id_eq] - ring - /-- `∂ₜ a = n / t₀ (t / t₀) ^ (n - 1)` away from `t = 0`. -/ lemma deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} (ht : t.val ≠ 0) : - ∂ₜ (powerLawScaleFactor t₀ n) t = n / t₀ * (t.val / t₀) ^ (n - 1) := - deriv_comp_val (hasDerivAt_div_rpow ht₀ n ht) + ∂ₜ (powerLawScaleFactor t₀ n) t = n / t₀ * (t.val / t₀) ^ (n - 1) := by + have h : HasDerivAt (fun y : ℝ => (y / t₀) ^ n) (n / t₀ * (t.val / t₀) ^ (n - 1)) t.val := by + have h := ((hasDerivAt_id t.val).div_const t₀).rpow_const (p := n) + (Or.inl (div_ne_zero ht ht₀)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + exact deriv_comp_val h /-- `∂ₜ ∂ₜ a = n (n - 1) / t₀² (t / t₀) ^ (n - 2)` for `t > 0`. The derivative `∂ₜ a` is only known away from `t = 0`, which is enough since `t > 0` is an open condition. -/ @@ -243,14 +224,21 @@ lemma deriv_deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ ∂ₜ (∂ₜ (powerLawScaleFactor t₀ n)) t = n / t₀ * ((n - 1) / t₀ * (t.val / t₀) ^ (n - 1 - 1)) := by apply deriv_eq_of_hasDerivAt - have h := (hasDerivAt_div_rpow ht₀ (n - 1) ht.ne').const_mul (n / t₀) + have h₁ : HasDerivAt (fun y : ℝ => (y / t₀) ^ (n - 1)) + ((n - 1) / t₀ * (t.val / t₀) ^ (n - 1 - 1)) t.val := by + have h := ((hasDerivAt_id t.val).div_const t₀).rpow_const (p := n - 1) + (Or.inl (div_ne_zero ht.ne' ht₀)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + have h := h₁.const_mul (n / t₀) refine h.congr_of_eventuallyEq ?_ filter_upwards [eventually_ne_nhds ht.ne'] with τ hτ exact deriv_powerLawScaleFactor ht₀ n (t := ⟨τ⟩) hτ /-! -### C.2. The Hubble and deceleration parameters +### B.2. The Hubble and deceleration parameters -/ @@ -313,7 +301,7 @@ lemma powerLawScaleFactor_secondOrderFriedmann {t₀ G c n w : ℝ} (ht₀ : 0 < /-! -### C.3. The radiation-dominated solution +### B.3. The radiation-dominated solution -/ @@ -371,7 +359,7 @@ lemma hubbleConstant_radiationScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < t₀) : /-! -### C.4. The Einstein-de Sitter solution +### B.4. The Einstein-de Sitter solution -/ @@ -427,7 +415,7 @@ lemma hubbleConstant_einsteinDeSitterScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < /-! -## D. Remaining TODO items +## C. Remaining TODO items -/ diff --git a/Physlib/SpaceAndTime/Time/Derivatives.lean b/Physlib/SpaceAndTime/Time/Derivatives.lean index 75d6e60020..41e6234c80 100644 --- a/Physlib/SpaceAndTime/Time/Derivatives.lean +++ b/Physlib/SpaceAndTime/Time/Derivatives.lean @@ -115,6 +115,17 @@ lemma deriv_comp_toRealCLE_of_hasDerivAt [NormedAddCommGroup M] [NormedSpace ℝ fderiv_eq_smul_deriv, h.deriv] exact Eq.trans (by rfl) (Time.one_val ▸ one_smul _ v) +/-- The time derivative of `t ↦ γ t.val` at `t` is the derivative of `γ` at `t.val`. -/ +lemma deriv_comp_val {γ : ℝ → ℝ} {t : Time} {v : ℝ} (h : HasDerivAt γ v t.val) : + ∂ₜ (fun s : Time => γ s.val) t = v := + deriv_comp_toRealCLE_of_hasDerivAt γ t v h + +/-- The time derivative of any `f : Time → ℝ` at `t` is the derivative at `t.val` of the curve + `τ ↦ f ⟨τ⟩` on `ℝ`. -/ +lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} + (h : HasDerivAt (fun τ : ℝ => f ⟨τ⟩) v t.val) : ∂ₜ f t = v := + deriv_comp_toRealCLE_of_hasDerivAt (fun τ : ℝ => f ⟨τ⟩) t v h + /-! ### A.3. Derivatives of functions into manifolds From 78428d25730cd41ff3ee8d87bce84377c8e3fd13 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 11 Sep 2026 11:03:30 +0200 Subject: [PATCH 11/20] style(Cosmology): inline one-off helper lemmas, move the Time derivative bridges next to their definition Applies the review remarks of #1642 across the series: no isolated general-purpose lemma, and lemmas about the time derivative live in SpaceAndTime/Time/Derivatives.lean. Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/Solutions.lean | 124 ++++++++++----------- Physlib/SpaceAndTime/Time/Derivatives.lean | 11 ++ 2 files changed, 67 insertions(+), 68 deletions(-) diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index 8480c23310..2627f1dc6a 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -54,19 +54,18 @@ coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridg ## iii. Table of contents -- A. Time derivatives of curves given by a function of the coordinate -- B. The de Sitter solution - - B.1. The scale factor and its derivatives - - B.2. The Friedmann equations - - B.3. The Hubble and deceleration parameters -- C. The spatially flat power-law solutions - - C.1. The power-law scale factor and its derivatives - - C.2. The Hubble and deceleration parameters - - C.3. The radiation-dominated solution - - C.4. The Einstein-de Sitter solution -- D. The Milne solution -- E. The Einstein static universe -- F. Remaining TODO items +- A. The de Sitter solution + - A.1. The scale factor and its derivatives + - A.2. The Friedmann equations + - A.3. The Hubble and deceleration parameters +- B. The spatially flat power-law solutions + - B.1. The power-law scale factor and its derivatives + - B.2. The Hubble and deceleration parameters + - B.3. The radiation-dominated solution + - B.4. The Einstein-de Sitter solution +- C. The Milne solution +- D. The Einstein static universe +- E. Remaining TODO items -/ @@ -78,33 +77,13 @@ open Real Time /-! -## A. Time derivatives of curves given by a function of the coordinate - -A curve `t ↦ γ t.val` on `Time` is the pull-back through `toRealCLE` of the curve `γ` on `ℝ`; -its time derivative is the Mathlib derivative of `γ`. - --/ - -/-- The time derivative of `t ↦ γ t.val` at `t` is the derivative of `γ` at `t.val`. -/ -lemma deriv_comp_val {γ : ℝ → ℝ} {t : Time} {v : ℝ} (h : HasDerivAt γ v t.val) : - ∂ₜ (fun s : Time => γ s.val) t = v := - deriv_comp_toRealCLE_of_hasDerivAt γ t v h - -/-- The time derivative of any `f : Time → ℝ` at `t` is the derivative at `t.val` of the curve - `τ ↦ f ⟨τ⟩` on `ℝ`. -/ -lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} - (h : HasDerivAt (fun τ : ℝ => f ⟨τ⟩) v t.val) : ∂ₜ f t = v := - deriv_comp_toRealCLE_of_hasDerivAt (fun τ : ℝ => f ⟨τ⟩) t v h - -/-! - -## B. The de Sitter solution +## A. The de Sitter solution -/ /-! -### B.1. The scale factor and its derivatives +### A.1. The scale factor and its derivatives -/ @@ -113,19 +92,17 @@ lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} noncomputable def deSitterScaleFactor (a₀ σ Λ c : ℝ) : Time → ℝ := fun t => a₀ * Real.exp (σ * √(Λ / 3) * c * t.val) -/-- Mathlib derivative of `y ↦ a₀ exp (K y)`. -/ -lemma hasDerivAt_mul_exp_mul (a₀ K x : ℝ) : - HasDerivAt (fun y : ℝ => a₀ * Real.exp (K * y)) (a₀ * K * Real.exp (K * x)) x := by - have h := (((hasDerivAt_id x).const_mul K).exp).const_mul a₀ - refine h.congr_deriv ?_ - simp only [id_eq] - ring - lemma deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : ∂ₜ (deSitterScaleFactor a₀ σ Λ c) = fun t => a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val) := by funext t - exact deriv_comp_val (hasDerivAt_mul_exp_mul a₀ (σ * √(Λ / 3) * c) t.val) + have h : HasDerivAt (fun y : ℝ => a₀ * Real.exp (σ * √(Λ / 3) * c * y)) + (a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val)) t.val := by + have h := (((hasDerivAt_id t.val).const_mul (σ * √(Λ / 3) * c)).exp).const_mul a₀ + refine h.congr_deriv ?_ + simp only [id_eq] + ring + exact deriv_comp_val h lemma deriv_deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : ∂ₜ (∂ₜ (deSitterScaleFactor a₀ σ Λ c)) = @@ -133,8 +110,15 @@ lemma deriv_deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : Real.exp (σ * √(Λ / 3) * c * t.val) := by rw [deriv_deSitterScaleFactor] funext t - exact deriv_comp_val - (hasDerivAt_mul_exp_mul (a₀ * (σ * √(Λ / 3) * c)) (σ * √(Λ / 3) * c) t.val) + have h : HasDerivAt (fun y : ℝ => a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * y)) + (a₀ * (σ * √(Λ / 3) * c) * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val)) + t.val := by + have h := (((hasDerivAt_id t.val).const_mul (σ * √(Λ / 3) * c)).exp).const_mul + (a₀ * (σ * √(Λ / 3) * c)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + exact deriv_comp_val h /-- `σ² (√(Λ/3))² c² = Λ c² / 3` for `σ = ±1` and `0 ≤ Λ`. -/ lemma sq_deSitterRate {σ Λ c : ℝ} (hΛ : 0 ≤ Λ) (hσ : σ = 1 ∨ σ = -1) : @@ -144,7 +128,7 @@ lemma sq_deSitterRate {σ Λ c : ℝ} (hΛ : 0 ≤ Λ) (hσ : σ = 1 ∨ σ = -1 /-! -### B.2. The Friedmann equations +### A.2. The Friedmann equations -/ @@ -179,7 +163,7 @@ lemma deSitterScaleFactor_secondOrderFriedmann {a₀ σ Λ G c : ℝ} (hΛ : 0 < /-! -### B.3. The Hubble and deceleration parameters +### A.3. The Hubble and deceleration parameters -/ @@ -212,7 +196,7 @@ lemma decelerationParameter_deSitterScaleFactor {a₀ σ Λ c : ℝ} (hΛ : 0 < /-! -## C. The spatially flat power-law solutions +## B. The spatially flat power-law solutions The radiation-dominated and Einstein-de Sitter solutions are both of the form `a(t) = (t / t₀) ^ n` for `t > 0`; the Hubble parameter is `n / t` and the deceleration @@ -223,7 +207,7 @@ parameter `(1 - n) / n`. Their densities are imposed by the first-order Friedman /-! -### C.1. The power-law scale factor and its derivatives +### B.1. The power-law scale factor and its derivatives -/ @@ -231,20 +215,17 @@ parameter `(1 - n) / n`. Their densities are imposed by the first-order Friedman noncomputable def powerLawScaleFactor (t₀ n : ℝ) : Time → ℝ := fun t => (t.val / t₀) ^ n -/-- Mathlib derivative of `y ↦ (y / t₀) ^ n` away from `y = 0`. -/ -lemma hasDerivAt_div_rpow {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {x : ℝ} (hx : x ≠ 0) : - HasDerivAt (fun y : ℝ => (y / t₀) ^ n) (n / t₀ * (x / t₀) ^ (n - 1)) x := by - have h := ((hasDerivAt_id x).div_const t₀).rpow_const (p := n) - (Or.inl (div_ne_zero hx ht₀)) - refine h.congr_deriv ?_ - simp only [id_eq] - ring - /-- `∂ₜ a = n / t₀ (t / t₀) ^ (n - 1)` away from `t = 0`. -/ lemma deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} (ht : t.val ≠ 0) : - ∂ₜ (powerLawScaleFactor t₀ n) t = n / t₀ * (t.val / t₀) ^ (n - 1) := - deriv_comp_val (hasDerivAt_div_rpow ht₀ n ht) + ∂ₜ (powerLawScaleFactor t₀ n) t = n / t₀ * (t.val / t₀) ^ (n - 1) := by + have h : HasDerivAt (fun y : ℝ => (y / t₀) ^ n) (n / t₀ * (t.val / t₀) ^ (n - 1)) t.val := by + have h := ((hasDerivAt_id t.val).div_const t₀).rpow_const (p := n) + (Or.inl (div_ne_zero ht ht₀)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + exact deriv_comp_val h /-- `∂ₜ ∂ₜ a = n (n - 1) / t₀² (t / t₀) ^ (n - 2)` for `t > 0`. The derivative `∂ₜ a` is only known away from `t = 0`, which is enough since `t > 0` is an open condition. -/ @@ -253,14 +234,21 @@ lemma deriv_deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ ∂ₜ (∂ₜ (powerLawScaleFactor t₀ n)) t = n / t₀ * ((n - 1) / t₀ * (t.val / t₀) ^ (n - 1 - 1)) := by apply deriv_eq_of_hasDerivAt - have h := (hasDerivAt_div_rpow ht₀ (n - 1) ht.ne').const_mul (n / t₀) + have h₁ : HasDerivAt (fun y : ℝ => (y / t₀) ^ (n - 1)) + ((n - 1) / t₀ * (t.val / t₀) ^ (n - 1 - 1)) t.val := by + have h := ((hasDerivAt_id t.val).div_const t₀).rpow_const (p := n - 1) + (Or.inl (div_ne_zero ht.ne' ht₀)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + have h := h₁.const_mul (n / t₀) refine h.congr_of_eventuallyEq ?_ filter_upwards [eventually_ne_nhds ht.ne'] with τ hτ exact deriv_powerLawScaleFactor ht₀ n (t := ⟨τ⟩) hτ /-! -### C.2. The Hubble and deceleration parameters +### B.2. The Hubble and deceleration parameters -/ @@ -323,7 +311,7 @@ lemma powerLawScaleFactor_secondOrderFriedmann {t₀ G c n w : ℝ} (ht₀ : 0 < /-! -### C.3. The radiation-dominated solution +### B.3. The radiation-dominated solution -/ @@ -381,7 +369,7 @@ lemma hubbleConstant_radiationScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < t₀) : /-! -### C.4. The Einstein-de Sitter solution +### B.4. The Einstein-de Sitter solution -/ @@ -437,7 +425,7 @@ lemma hubbleConstant_einsteinDeSitterScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < /-! -## D. The Milne solution +## C. The Milne solution The Milne universe is the empty (`ρ = 0`, `p = 0`, `Λ = 0`) solution with `k = -1` and `a(t) = c t` for `t > 0`. That it is Minkowski space in expanding coordinates (vanishing @@ -485,7 +473,7 @@ lemma decelerationParameter_milneScaleFactor (c : ℝ) (t : Time) : /-! -## E. The Einstein static universe +## D. The Einstein static universe At an instant where `∂ₜ a = ∂ₜ ∂ₜ a = 0`, the two Friedmann equations with dust (`p = 0`) force the density `ρ = Λ c² / (4 π G)`, twice the density `ρ_Λ = Λ c² / (8 π G)` associated @@ -540,7 +528,7 @@ lemma einsteinStatic_curvature_pos {a ρ : Time → ℝ} {k Λ G c : ℝ} {t : T /-! -## F. Remaining TODO items +## E. Remaining TODO items -/ diff --git a/Physlib/SpaceAndTime/Time/Derivatives.lean b/Physlib/SpaceAndTime/Time/Derivatives.lean index 75d6e60020..41e6234c80 100644 --- a/Physlib/SpaceAndTime/Time/Derivatives.lean +++ b/Physlib/SpaceAndTime/Time/Derivatives.lean @@ -115,6 +115,17 @@ lemma deriv_comp_toRealCLE_of_hasDerivAt [NormedAddCommGroup M] [NormedSpace ℝ fderiv_eq_smul_deriv, h.deriv] exact Eq.trans (by rfl) (Time.one_val ▸ one_smul _ v) +/-- The time derivative of `t ↦ γ t.val` at `t` is the derivative of `γ` at `t.val`. -/ +lemma deriv_comp_val {γ : ℝ → ℝ} {t : Time} {v : ℝ} (h : HasDerivAt γ v t.val) : + ∂ₜ (fun s : Time => γ s.val) t = v := + deriv_comp_toRealCLE_of_hasDerivAt γ t v h + +/-- The time derivative of any `f : Time → ℝ` at `t` is the derivative at `t.val` of the curve + `τ ↦ f ⟨τ⟩` on `ℝ`. -/ +lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} + (h : HasDerivAt (fun τ : ℝ => f ⟨τ⟩) v t.val) : ∂ₜ f t = v := + deriv_comp_toRealCLE_of_hasDerivAt (fun τ : ℝ => f ⟨τ⟩) t v h + /-! ### A.3. Derivatives of functions into manifolds From 6f82dc08177a37abbb182051dbe60ba892972706 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 11 Sep 2026 11:06:42 +0200 Subject: [PATCH 12/20] style(Cosmology): inline one-off helper lemmas, move the Time derivative bridges next to their definition Applies the review remarks of #1642 across the series: no isolated general-purpose lemma, and lemmas about the time derivative live in SpaceAndTime/Time/Derivatives.lean. Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/MatterContent.lean | 38 ++----- Physlib/Cosmology/FLRW/Solutions.lean | 124 ++++++++++----------- Physlib/SpaceAndTime/Time/Derivatives.lean | 18 +++ 3 files changed, 86 insertions(+), 94 deletions(-) diff --git a/Physlib/Cosmology/FLRW/MatterContent.lean b/Physlib/Cosmology/FLRW/MatterContent.lean index a8cd19661d..9dff827dc5 100644 --- a/Physlib/Cosmology/FLRW/MatterContent.lean +++ b/Physlib/Cosmology/FLRW/MatterContent.lean @@ -37,13 +37,12 @@ Time derivatives of curves `Time → ℝ` are computed through the bridge ## iii. Table of contents -- A. Time derivatives through the coordinate -- B. The continuity equation - - B.1. The definition - - B.2. The derivative of the first-order Friedmann equation - - B.3. Continuity from the Friedmann equations - - B.4. The second-order Friedmann equation from continuity -- C. Remaining TODO items +- A. The continuity equation + - A.1. The definition + - A.2. The derivative of the first-order Friedmann equation + - A.3. Continuity from the Friedmann equations + - A.4. The second-order Friedmann equation from continuity +- B. Remaining TODO items -/ @@ -55,26 +54,13 @@ open Real Time /-! -## A. Time derivatives through the coordinate - --/ - -/-- A curve `f : Time → ℝ` differentiable at `⟨τ⟩` gives the curve `σ ↦ f ⟨σ⟩` on `ℝ`, - whose Mathlib derivative at `τ` is the time derivative `∂ₜ f ⟨τ⟩`. -/ -lemma hasDerivAt_mk_of_differentiableAt {f : Time → ℝ} {τ : ℝ} - (hf : DifferentiableAt ℝ f ⟨τ⟩) : - HasDerivAt (fun σ : ℝ => f ⟨σ⟩) (∂ₜ f ⟨τ⟩) τ := - hasDerivAt_comp_toRealCLE_symm f τ hf - -/-! - -## B. The continuity equation +## A. The continuity equation -/ /-! -### B.1. The definition +### A.1. The definition -/ @@ -85,7 +71,7 @@ def ContinuityEquation (a ρ p : Time → ℝ) (c : ℝ) (t : Time) : Prop := /-! -### B.2. The derivative of the first-order Friedmann equation +### A.2. The derivative of the first-order Friedmann equation -/ @@ -113,7 +99,7 @@ lemma deriv_firstOrderFriedmann {a ρ : Time → ℝ} {k Λ G c τ : ℝ} (ha : /-! -### B.3. Continuity from the Friedmann equations +### A.3. Continuity from the Friedmann equations -/ @@ -140,7 +126,7 @@ lemma continuityEquation_of_friedmann {a ρ p : Time → ℝ} {k Λ G c : ℝ} { /-! -### B.4. The second-order Friedmann equation from continuity +### A.4. The second-order Friedmann equation from continuity -/ @@ -166,7 +152,7 @@ lemma secondOrderFriedmann_of_continuityEquation {a ρ p : Time → ℝ} {k Λ G /-! -## C. Remaining TODO items +## B. Remaining TODO items -/ diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index 8480c23310..2627f1dc6a 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -54,19 +54,18 @@ coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridg ## iii. Table of contents -- A. Time derivatives of curves given by a function of the coordinate -- B. The de Sitter solution - - B.1. The scale factor and its derivatives - - B.2. The Friedmann equations - - B.3. The Hubble and deceleration parameters -- C. The spatially flat power-law solutions - - C.1. The power-law scale factor and its derivatives - - C.2. The Hubble and deceleration parameters - - C.3. The radiation-dominated solution - - C.4. The Einstein-de Sitter solution -- D. The Milne solution -- E. The Einstein static universe -- F. Remaining TODO items +- A. The de Sitter solution + - A.1. The scale factor and its derivatives + - A.2. The Friedmann equations + - A.3. The Hubble and deceleration parameters +- B. The spatially flat power-law solutions + - B.1. The power-law scale factor and its derivatives + - B.2. The Hubble and deceleration parameters + - B.3. The radiation-dominated solution + - B.4. The Einstein-de Sitter solution +- C. The Milne solution +- D. The Einstein static universe +- E. Remaining TODO items -/ @@ -78,33 +77,13 @@ open Real Time /-! -## A. Time derivatives of curves given by a function of the coordinate - -A curve `t ↦ γ t.val` on `Time` is the pull-back through `toRealCLE` of the curve `γ` on `ℝ`; -its time derivative is the Mathlib derivative of `γ`. - --/ - -/-- The time derivative of `t ↦ γ t.val` at `t` is the derivative of `γ` at `t.val`. -/ -lemma deriv_comp_val {γ : ℝ → ℝ} {t : Time} {v : ℝ} (h : HasDerivAt γ v t.val) : - ∂ₜ (fun s : Time => γ s.val) t = v := - deriv_comp_toRealCLE_of_hasDerivAt γ t v h - -/-- The time derivative of any `f : Time → ℝ` at `t` is the derivative at `t.val` of the curve - `τ ↦ f ⟨τ⟩` on `ℝ`. -/ -lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} - (h : HasDerivAt (fun τ : ℝ => f ⟨τ⟩) v t.val) : ∂ₜ f t = v := - deriv_comp_toRealCLE_of_hasDerivAt (fun τ : ℝ => f ⟨τ⟩) t v h - -/-! - -## B. The de Sitter solution +## A. The de Sitter solution -/ /-! -### B.1. The scale factor and its derivatives +### A.1. The scale factor and its derivatives -/ @@ -113,19 +92,17 @@ lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} noncomputable def deSitterScaleFactor (a₀ σ Λ c : ℝ) : Time → ℝ := fun t => a₀ * Real.exp (σ * √(Λ / 3) * c * t.val) -/-- Mathlib derivative of `y ↦ a₀ exp (K y)`. -/ -lemma hasDerivAt_mul_exp_mul (a₀ K x : ℝ) : - HasDerivAt (fun y : ℝ => a₀ * Real.exp (K * y)) (a₀ * K * Real.exp (K * x)) x := by - have h := (((hasDerivAt_id x).const_mul K).exp).const_mul a₀ - refine h.congr_deriv ?_ - simp only [id_eq] - ring - lemma deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : ∂ₜ (deSitterScaleFactor a₀ σ Λ c) = fun t => a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val) := by funext t - exact deriv_comp_val (hasDerivAt_mul_exp_mul a₀ (σ * √(Λ / 3) * c) t.val) + have h : HasDerivAt (fun y : ℝ => a₀ * Real.exp (σ * √(Λ / 3) * c * y)) + (a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val)) t.val := by + have h := (((hasDerivAt_id t.val).const_mul (σ * √(Λ / 3) * c)).exp).const_mul a₀ + refine h.congr_deriv ?_ + simp only [id_eq] + ring + exact deriv_comp_val h lemma deriv_deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : ∂ₜ (∂ₜ (deSitterScaleFactor a₀ σ Λ c)) = @@ -133,8 +110,15 @@ lemma deriv_deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : Real.exp (σ * √(Λ / 3) * c * t.val) := by rw [deriv_deSitterScaleFactor] funext t - exact deriv_comp_val - (hasDerivAt_mul_exp_mul (a₀ * (σ * √(Λ / 3) * c)) (σ * √(Λ / 3) * c) t.val) + have h : HasDerivAt (fun y : ℝ => a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * y)) + (a₀ * (σ * √(Λ / 3) * c) * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val)) + t.val := by + have h := (((hasDerivAt_id t.val).const_mul (σ * √(Λ / 3) * c)).exp).const_mul + (a₀ * (σ * √(Λ / 3) * c)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + exact deriv_comp_val h /-- `σ² (√(Λ/3))² c² = Λ c² / 3` for `σ = ±1` and `0 ≤ Λ`. -/ lemma sq_deSitterRate {σ Λ c : ℝ} (hΛ : 0 ≤ Λ) (hσ : σ = 1 ∨ σ = -1) : @@ -144,7 +128,7 @@ lemma sq_deSitterRate {σ Λ c : ℝ} (hΛ : 0 ≤ Λ) (hσ : σ = 1 ∨ σ = -1 /-! -### B.2. The Friedmann equations +### A.2. The Friedmann equations -/ @@ -179,7 +163,7 @@ lemma deSitterScaleFactor_secondOrderFriedmann {a₀ σ Λ G c : ℝ} (hΛ : 0 < /-! -### B.3. The Hubble and deceleration parameters +### A.3. The Hubble and deceleration parameters -/ @@ -212,7 +196,7 @@ lemma decelerationParameter_deSitterScaleFactor {a₀ σ Λ c : ℝ} (hΛ : 0 < /-! -## C. The spatially flat power-law solutions +## B. The spatially flat power-law solutions The radiation-dominated and Einstein-de Sitter solutions are both of the form `a(t) = (t / t₀) ^ n` for `t > 0`; the Hubble parameter is `n / t` and the deceleration @@ -223,7 +207,7 @@ parameter `(1 - n) / n`. Their densities are imposed by the first-order Friedman /-! -### C.1. The power-law scale factor and its derivatives +### B.1. The power-law scale factor and its derivatives -/ @@ -231,20 +215,17 @@ parameter `(1 - n) / n`. Their densities are imposed by the first-order Friedman noncomputable def powerLawScaleFactor (t₀ n : ℝ) : Time → ℝ := fun t => (t.val / t₀) ^ n -/-- Mathlib derivative of `y ↦ (y / t₀) ^ n` away from `y = 0`. -/ -lemma hasDerivAt_div_rpow {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {x : ℝ} (hx : x ≠ 0) : - HasDerivAt (fun y : ℝ => (y / t₀) ^ n) (n / t₀ * (x / t₀) ^ (n - 1)) x := by - have h := ((hasDerivAt_id x).div_const t₀).rpow_const (p := n) - (Or.inl (div_ne_zero hx ht₀)) - refine h.congr_deriv ?_ - simp only [id_eq] - ring - /-- `∂ₜ a = n / t₀ (t / t₀) ^ (n - 1)` away from `t = 0`. -/ lemma deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} (ht : t.val ≠ 0) : - ∂ₜ (powerLawScaleFactor t₀ n) t = n / t₀ * (t.val / t₀) ^ (n - 1) := - deriv_comp_val (hasDerivAt_div_rpow ht₀ n ht) + ∂ₜ (powerLawScaleFactor t₀ n) t = n / t₀ * (t.val / t₀) ^ (n - 1) := by + have h : HasDerivAt (fun y : ℝ => (y / t₀) ^ n) (n / t₀ * (t.val / t₀) ^ (n - 1)) t.val := by + have h := ((hasDerivAt_id t.val).div_const t₀).rpow_const (p := n) + (Or.inl (div_ne_zero ht ht₀)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + exact deriv_comp_val h /-- `∂ₜ ∂ₜ a = n (n - 1) / t₀² (t / t₀) ^ (n - 2)` for `t > 0`. The derivative `∂ₜ a` is only known away from `t = 0`, which is enough since `t > 0` is an open condition. -/ @@ -253,14 +234,21 @@ lemma deriv_deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ ∂ₜ (∂ₜ (powerLawScaleFactor t₀ n)) t = n / t₀ * ((n - 1) / t₀ * (t.val / t₀) ^ (n - 1 - 1)) := by apply deriv_eq_of_hasDerivAt - have h := (hasDerivAt_div_rpow ht₀ (n - 1) ht.ne').const_mul (n / t₀) + have h₁ : HasDerivAt (fun y : ℝ => (y / t₀) ^ (n - 1)) + ((n - 1) / t₀ * (t.val / t₀) ^ (n - 1 - 1)) t.val := by + have h := ((hasDerivAt_id t.val).div_const t₀).rpow_const (p := n - 1) + (Or.inl (div_ne_zero ht.ne' ht₀)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + have h := h₁.const_mul (n / t₀) refine h.congr_of_eventuallyEq ?_ filter_upwards [eventually_ne_nhds ht.ne'] with τ hτ exact deriv_powerLawScaleFactor ht₀ n (t := ⟨τ⟩) hτ /-! -### C.2. The Hubble and deceleration parameters +### B.2. The Hubble and deceleration parameters -/ @@ -323,7 +311,7 @@ lemma powerLawScaleFactor_secondOrderFriedmann {t₀ G c n w : ℝ} (ht₀ : 0 < /-! -### C.3. The radiation-dominated solution +### B.3. The radiation-dominated solution -/ @@ -381,7 +369,7 @@ lemma hubbleConstant_radiationScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < t₀) : /-! -### C.4. The Einstein-de Sitter solution +### B.4. The Einstein-de Sitter solution -/ @@ -437,7 +425,7 @@ lemma hubbleConstant_einsteinDeSitterScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < /-! -## D. The Milne solution +## C. The Milne solution The Milne universe is the empty (`ρ = 0`, `p = 0`, `Λ = 0`) solution with `k = -1` and `a(t) = c t` for `t > 0`. That it is Minkowski space in expanding coordinates (vanishing @@ -485,7 +473,7 @@ lemma decelerationParameter_milneScaleFactor (c : ℝ) (t : Time) : /-! -## E. The Einstein static universe +## D. The Einstein static universe At an instant where `∂ₜ a = ∂ₜ ∂ₜ a = 0`, the two Friedmann equations with dust (`p = 0`) force the density `ρ = Λ c² / (4 π G)`, twice the density `ρ_Λ = Λ c² / (8 π G)` associated @@ -540,7 +528,7 @@ lemma einsteinStatic_curvature_pos {a ρ : Time → ℝ} {k Λ G c : ℝ} {t : T /-! -## F. Remaining TODO items +## E. Remaining TODO items -/ diff --git a/Physlib/SpaceAndTime/Time/Derivatives.lean b/Physlib/SpaceAndTime/Time/Derivatives.lean index 75d6e60020..872bb1af6d 100644 --- a/Physlib/SpaceAndTime/Time/Derivatives.lean +++ b/Physlib/SpaceAndTime/Time/Derivatives.lean @@ -115,6 +115,24 @@ lemma deriv_comp_toRealCLE_of_hasDerivAt [NormedAddCommGroup M] [NormedSpace ℝ fderiv_eq_smul_deriv, h.deriv] exact Eq.trans (by rfl) (Time.one_val ▸ one_smul _ v) +/-- The time derivative of `t ↦ γ t.val` at `t` is the derivative of `γ` at `t.val`. -/ +lemma deriv_comp_val {γ : ℝ → ℝ} {t : Time} {v : ℝ} (h : HasDerivAt γ v t.val) : + ∂ₜ (fun s : Time => γ s.val) t = v := + deriv_comp_toRealCLE_of_hasDerivAt γ t v h + +/-- The time derivative of any `f : Time → ℝ` at `t` is the derivative at `t.val` of the curve + `τ ↦ f ⟨τ⟩` on `ℝ`. -/ +lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} + (h : HasDerivAt (fun τ : ℝ => f ⟨τ⟩) v t.val) : ∂ₜ f t = v := + deriv_comp_toRealCLE_of_hasDerivAt (fun τ : ℝ => f ⟨τ⟩) t v h + +/-- A curve `f : Time → ℝ` differentiable at `⟨τ⟩` gives the curve `σ ↦ f ⟨σ⟩` on `ℝ`, + whose Mathlib derivative at `τ` is the time derivative `∂ₜ f ⟨τ⟩`. -/ +lemma hasDerivAt_mk_of_differentiableAt {f : Time → ℝ} {τ : ℝ} + (hf : DifferentiableAt ℝ f ⟨τ⟩) : + HasDerivAt (fun σ : ℝ => f ⟨σ⟩) (∂ₜ f ⟨τ⟩) τ := + hasDerivAt_comp_toRealCLE_symm f τ hf + /-! ### A.3. Derivatives of functions into manifolds From 3a83e2c8784e3930373d783203f484cad8e2683f Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Fri, 11 Sep 2026 11:08:43 +0200 Subject: [PATCH 13/20] style(Cosmology): inline one-off helper lemmas, move the Time derivative bridges next to their definition Applies the review remarks of #1642 across the series: no isolated general-purpose lemma, and lemmas about the time derivative live in SpaceAndTime/Time/Derivatives.lean. Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/MatterContent.lean | 58 ++++------ Physlib/Cosmology/FLRW/Solutions.lean | 124 ++++++++++----------- Physlib/SpaceAndTime/Time/Derivatives.lean | 18 +++ 3 files changed, 96 insertions(+), 104 deletions(-) diff --git a/Physlib/Cosmology/FLRW/MatterContent.lean b/Physlib/Cosmology/FLRW/MatterContent.lean index f31b32b1e3..c016f549e7 100644 --- a/Physlib/Cosmology/FLRW/MatterContent.lean +++ b/Physlib/Cosmology/FLRW/MatterContent.lean @@ -49,18 +49,17 @@ Time derivatives of curves `Time → ℝ` are computed through the bridge ## iii. Table of contents -- A. Time derivatives through the coordinate -- B. The continuity equation - - B.1. The definition - - B.2. The derivative of the first-order Friedmann equation - - B.3. Continuity from the Friedmann equations - - B.4. The second-order Friedmann equation from continuity -- C. The barotropic equation of state and the density scaling law - - C.1. The equation of state - - C.2. The density scaling law - - C.3. Dust, radiation and vacuum energy -- D. The cosmological constant as a fluid -- E. Remaining TODO items +- A. The continuity equation + - A.1. The definition + - A.2. The derivative of the first-order Friedmann equation + - A.3. Continuity from the Friedmann equations + - A.4. The second-order Friedmann equation from continuity +- B. The barotropic equation of state and the density scaling law + - B.1. The equation of state + - B.2. The density scaling law + - B.3. Dust, radiation and vacuum energy +- C. The cosmological constant as a fluid +- D. Remaining TODO items -/ @@ -72,26 +71,13 @@ open Real Time /-! -## A. Time derivatives through the coordinate - --/ - -/-- A curve `f : Time → ℝ` differentiable at `⟨τ⟩` gives the curve `σ ↦ f ⟨σ⟩` on `ℝ`, - whose Mathlib derivative at `τ` is the time derivative `∂ₜ f ⟨τ⟩`. -/ -lemma hasDerivAt_mk_of_differentiableAt {f : Time → ℝ} {τ : ℝ} - (hf : DifferentiableAt ℝ f ⟨τ⟩) : - HasDerivAt (fun σ : ℝ => f ⟨σ⟩) (∂ₜ f ⟨τ⟩) τ := - hasDerivAt_comp_toRealCLE_symm f τ hf - -/-! - -## B. The continuity equation +## A. The continuity equation -/ /-! -### B.1. The definition +### A.1. The definition -/ @@ -102,7 +88,7 @@ def ContinuityEquation (a ρ p : Time → ℝ) (c : ℝ) (t : Time) : Prop := /-! -### B.2. The derivative of the first-order Friedmann equation +### A.2. The derivative of the first-order Friedmann equation -/ @@ -130,7 +116,7 @@ lemma deriv_firstOrderFriedmann {a ρ : Time → ℝ} {k Λ G c τ : ℝ} (ha : /-! -### B.3. Continuity from the Friedmann equations +### A.3. Continuity from the Friedmann equations -/ @@ -157,7 +143,7 @@ lemma continuityEquation_of_friedmann {a ρ p : Time → ℝ} {k Λ G c : ℝ} { /-! -### B.4. The second-order Friedmann equation from continuity +### A.4. The second-order Friedmann equation from continuity -/ @@ -183,13 +169,13 @@ lemma secondOrderFriedmann_of_continuityEquation {a ρ p : Time → ℝ} {k Λ G /-! -## C. The barotropic equation of state and the density scaling law +## B. The barotropic equation of state and the density scaling law -/ /-! -### C.1. The equation of state +### B.1. The equation of state -/ @@ -209,7 +195,7 @@ lemma deriv_of_continuityEquation_barotropic {a ρ : Time → ℝ} {w c : ℝ} { /-! -### C.2. The density scaling law +### B.2. The density scaling law -/ @@ -269,7 +255,7 @@ lemma continuityEquation_of_scaling {a : Time → ℝ} {w c ρ₀ a₀ : ℝ} (h /-! -### C.3. Dust, radiation and vacuum energy +### B.3. Dust, radiation and vacuum energy -/ @@ -303,7 +289,7 @@ lemma density_scaling_vacuum {a ρ : Time → ℝ} {c : ℝ} (hc : c ≠ 0) (hd1 /-! -## D. The cosmological constant as a fluid +## C. The cosmological constant as a fluid -/ @@ -354,7 +340,7 @@ lemma cosmologicalConstantPressure_eq_barotropic (Λ G c : ℝ) (t : Time) : /-! -## E. Remaining TODO items +## D. Remaining TODO items -/ diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index d89d88d9c6..3ebc57c2d3 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -54,19 +54,18 @@ coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridg ## iii. Table of contents -- A. Time derivatives of curves given by a function of the coordinate -- B. The de Sitter solution - - B.1. The scale factor and its derivatives - - B.2. The Friedmann equations - - B.3. The Hubble and deceleration parameters -- C. The spatially flat power-law solutions - - C.1. The power-law scale factor and its derivatives - - C.2. The Hubble and deceleration parameters - - C.3. The radiation-dominated solution - - C.4. The Einstein-de Sitter solution -- D. The Milne solution -- E. The Einstein static universe -- F. Remaining TODO items +- A. The de Sitter solution + - A.1. The scale factor and its derivatives + - A.2. The Friedmann equations + - A.3. The Hubble and deceleration parameters +- B. The spatially flat power-law solutions + - B.1. The power-law scale factor and its derivatives + - B.2. The Hubble and deceleration parameters + - B.3. The radiation-dominated solution + - B.4. The Einstein-de Sitter solution +- C. The Milne solution +- D. The Einstein static universe +- E. Remaining TODO items -/ @@ -78,33 +77,13 @@ open Real Time /-! -## A. Time derivatives of curves given by a function of the coordinate - -A curve `t ↦ γ t.val` on `Time` is the pull-back through `toRealCLE` of the curve `γ` on `ℝ`; -its time derivative is the Mathlib derivative of `γ`. - --/ - -/-- The time derivative of `t ↦ γ t.val` at `t` is the derivative of `γ` at `t.val`. -/ -lemma deriv_comp_val {γ : ℝ → ℝ} {t : Time} {v : ℝ} (h : HasDerivAt γ v t.val) : - ∂ₜ (fun s : Time => γ s.val) t = v := - deriv_comp_toRealCLE_of_hasDerivAt γ t v h - -/-- The time derivative of any `f : Time → ℝ` at `t` is the derivative at `t.val` of the curve - `τ ↦ f ⟨τ⟩` on `ℝ`. -/ -lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} - (h : HasDerivAt (fun τ : ℝ => f ⟨τ⟩) v t.val) : ∂ₜ f t = v := - deriv_comp_toRealCLE_of_hasDerivAt (fun τ : ℝ => f ⟨τ⟩) t v h - -/-! - -## B. The de Sitter solution +## A. The de Sitter solution -/ /-! -### B.1. The scale factor and its derivatives +### A.1. The scale factor and its derivatives -/ @@ -113,19 +92,17 @@ lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} noncomputable def deSitterScaleFactor (a₀ σ Λ c : ℝ) : Time → ℝ := fun t => a₀ * Real.exp (σ * √(Λ / 3) * c * t.val) -/-- Mathlib derivative of `y ↦ a₀ exp (K y)`. -/ -lemma hasDerivAt_mul_exp_mul (a₀ K x : ℝ) : - HasDerivAt (fun y : ℝ => a₀ * Real.exp (K * y)) (a₀ * K * Real.exp (K * x)) x := by - have h := (((hasDerivAt_id x).const_mul K).exp).const_mul a₀ - refine h.congr_deriv ?_ - simp only [id_eq] - ring - lemma deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : ∂ₜ (deSitterScaleFactor a₀ σ Λ c) = fun t => a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val) := by funext t - exact deriv_comp_val (hasDerivAt_mul_exp_mul a₀ (σ * √(Λ / 3) * c) t.val) + have h : HasDerivAt (fun y : ℝ => a₀ * Real.exp (σ * √(Λ / 3) * c * y)) + (a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val)) t.val := by + have h := (((hasDerivAt_id t.val).const_mul (σ * √(Λ / 3) * c)).exp).const_mul a₀ + refine h.congr_deriv ?_ + simp only [id_eq] + ring + exact deriv_comp_val h lemma deriv_deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : ∂ₜ (∂ₜ (deSitterScaleFactor a₀ σ Λ c)) = @@ -133,8 +110,15 @@ lemma deriv_deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : Real.exp (σ * √(Λ / 3) * c * t.val) := by rw [deriv_deSitterScaleFactor] funext t - exact deriv_comp_val - (hasDerivAt_mul_exp_mul (a₀ * (σ * √(Λ / 3) * c)) (σ * √(Λ / 3) * c) t.val) + have h : HasDerivAt (fun y : ℝ => a₀ * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * y)) + (a₀ * (σ * √(Λ / 3) * c) * (σ * √(Λ / 3) * c) * Real.exp (σ * √(Λ / 3) * c * t.val)) + t.val := by + have h := (((hasDerivAt_id t.val).const_mul (σ * √(Λ / 3) * c)).exp).const_mul + (a₀ * (σ * √(Λ / 3) * c)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + exact deriv_comp_val h /-- `σ² (√(Λ/3))² c² = Λ c² / 3` for `σ = ±1` and `0 ≤ Λ`. -/ lemma sq_deSitterRate {σ Λ c : ℝ} (hΛ : 0 ≤ Λ) (hσ : σ = 1 ∨ σ = -1) : @@ -144,7 +128,7 @@ lemma sq_deSitterRate {σ Λ c : ℝ} (hΛ : 0 ≤ Λ) (hσ : σ = 1 ∨ σ = -1 /-! -### B.2. The Friedmann equations +### A.2. The Friedmann equations -/ @@ -179,7 +163,7 @@ lemma deSitterScaleFactor_secondOrderFriedmann {a₀ σ Λ G c : ℝ} (hΛ : 0 < /-! -### B.3. The Hubble and deceleration parameters +### A.3. The Hubble and deceleration parameters -/ @@ -212,7 +196,7 @@ lemma decelerationParameter_deSitterScaleFactor {a₀ σ Λ c : ℝ} (hΛ : 0 < /-! -## C. The spatially flat power-law solutions +## B. The spatially flat power-law solutions The radiation-dominated and Einstein-de Sitter solutions are both of the form `a(t) = (t / t₀) ^ n` for `t > 0`; the Hubble parameter is `n / t` and the deceleration @@ -223,7 +207,7 @@ parameter `(1 - n) / n`. Their densities are imposed by the first-order Friedman /-! -### C.1. The power-law scale factor and its derivatives +### B.1. The power-law scale factor and its derivatives -/ @@ -231,20 +215,17 @@ parameter `(1 - n) / n`. Their densities are imposed by the first-order Friedman noncomputable def powerLawScaleFactor (t₀ n : ℝ) : Time → ℝ := fun t => (t.val / t₀) ^ n -/-- Mathlib derivative of `y ↦ (y / t₀) ^ n` away from `y = 0`. -/ -lemma hasDerivAt_div_rpow {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {x : ℝ} (hx : x ≠ 0) : - HasDerivAt (fun y : ℝ => (y / t₀) ^ n) (n / t₀ * (x / t₀) ^ (n - 1)) x := by - have h := ((hasDerivAt_id x).div_const t₀).rpow_const (p := n) - (Or.inl (div_ne_zero hx ht₀)) - refine h.congr_deriv ?_ - simp only [id_eq] - ring - /-- `∂ₜ a = n / t₀ (t / t₀) ^ (n - 1)` away from `t = 0`. -/ lemma deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} (ht : t.val ≠ 0) : - ∂ₜ (powerLawScaleFactor t₀ n) t = n / t₀ * (t.val / t₀) ^ (n - 1) := - deriv_comp_val (hasDerivAt_div_rpow ht₀ n ht) + ∂ₜ (powerLawScaleFactor t₀ n) t = n / t₀ * (t.val / t₀) ^ (n - 1) := by + have h : HasDerivAt (fun y : ℝ => (y / t₀) ^ n) (n / t₀ * (t.val / t₀) ^ (n - 1)) t.val := by + have h := ((hasDerivAt_id t.val).div_const t₀).rpow_const (p := n) + (Or.inl (div_ne_zero ht ht₀)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + exact deriv_comp_val h /-- `∂ₜ ∂ₜ a = n (n - 1) / t₀² (t / t₀) ^ (n - 2)` for `t > 0`. The derivative `∂ₜ a` is only known away from `t = 0`, which is enough since `t > 0` is an open condition. -/ @@ -253,14 +234,21 @@ lemma deriv_deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ ∂ₜ (∂ₜ (powerLawScaleFactor t₀ n)) t = n / t₀ * ((n - 1) / t₀ * (t.val / t₀) ^ (n - 1 - 1)) := by apply deriv_eq_of_hasDerivAt - have h := (hasDerivAt_div_rpow ht₀ (n - 1) ht.ne').const_mul (n / t₀) + have h₁ : HasDerivAt (fun y : ℝ => (y / t₀) ^ (n - 1)) + ((n - 1) / t₀ * (t.val / t₀) ^ (n - 1 - 1)) t.val := by + have h := ((hasDerivAt_id t.val).div_const t₀).rpow_const (p := n - 1) + (Or.inl (div_ne_zero ht.ne' ht₀)) + refine h.congr_deriv ?_ + simp only [id_eq] + ring + have h := h₁.const_mul (n / t₀) refine h.congr_of_eventuallyEq ?_ filter_upwards [eventually_ne_nhds ht.ne'] with τ hτ exact deriv_powerLawScaleFactor ht₀ n (t := ⟨τ⟩) hτ /-! -### C.2. The Hubble and deceleration parameters +### B.2. The Hubble and deceleration parameters -/ @@ -323,7 +311,7 @@ lemma powerLawScaleFactor_secondOrderFriedmann {t₀ G c n w : ℝ} (ht₀ : 0 < /-! -### C.3. The radiation-dominated solution +### B.3. The radiation-dominated solution -/ @@ -381,7 +369,7 @@ lemma hubbleConstant_radiationScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < t₀) : /-! -### C.4. The Einstein-de Sitter solution +### B.4. The Einstein-de Sitter solution -/ @@ -437,7 +425,7 @@ lemma hubbleConstant_einsteinDeSitterScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < /-! -## D. The Milne solution +## C. The Milne solution The Milne universe is the empty (`ρ = 0`, `p = 0`, `Λ = 0`) solution with `k = -1` and `a(t) = c t` for `t > 0`. That it is Minkowski space in expanding coordinates (vanishing @@ -485,7 +473,7 @@ lemma decelerationParameter_milneScaleFactor (c : ℝ) (t : Time) : /-! -## E. The Einstein static universe +## D. The Einstein static universe At an instant where `∂ₜ a = ∂ₜ ∂ₜ a = 0`, the two Friedmann equations with dust (`p = 0`) force the density `ρ = Λ c² / (4 π G)`, twice the density `cosmologicalConstantDensity` @@ -537,7 +525,7 @@ lemma einsteinStatic_curvature_pos {a ρ : Time → ℝ} {k Λ G c : ℝ} {t : T /-! -## F. Remaining TODO items +## E. Remaining TODO items -/ diff --git a/Physlib/SpaceAndTime/Time/Derivatives.lean b/Physlib/SpaceAndTime/Time/Derivatives.lean index 75d6e60020..872bb1af6d 100644 --- a/Physlib/SpaceAndTime/Time/Derivatives.lean +++ b/Physlib/SpaceAndTime/Time/Derivatives.lean @@ -115,6 +115,24 @@ lemma deriv_comp_toRealCLE_of_hasDerivAt [NormedAddCommGroup M] [NormedSpace ℝ fderiv_eq_smul_deriv, h.deriv] exact Eq.trans (by rfl) (Time.one_val ▸ one_smul _ v) +/-- The time derivative of `t ↦ γ t.val` at `t` is the derivative of `γ` at `t.val`. -/ +lemma deriv_comp_val {γ : ℝ → ℝ} {t : Time} {v : ℝ} (h : HasDerivAt γ v t.val) : + ∂ₜ (fun s : Time => γ s.val) t = v := + deriv_comp_toRealCLE_of_hasDerivAt γ t v h + +/-- The time derivative of any `f : Time → ℝ` at `t` is the derivative at `t.val` of the curve + `τ ↦ f ⟨τ⟩` on `ℝ`. -/ +lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} + (h : HasDerivAt (fun τ : ℝ => f ⟨τ⟩) v t.val) : ∂ₜ f t = v := + deriv_comp_toRealCLE_of_hasDerivAt (fun τ : ℝ => f ⟨τ⟩) t v h + +/-- A curve `f : Time → ℝ` differentiable at `⟨τ⟩` gives the curve `σ ↦ f ⟨σ⟩` on `ℝ`, + whose Mathlib derivative at `τ` is the time derivative `∂ₜ f ⟨τ⟩`. -/ +lemma hasDerivAt_mk_of_differentiableAt {f : Time → ℝ} {τ : ℝ} + (hf : DifferentiableAt ℝ f ⟨τ⟩) : + HasDerivAt (fun σ : ℝ => f ⟨σ⟩) (∂ₜ f ⟨τ⟩) τ := + hasDerivAt_comp_toRealCLE_symm f τ hf + /-! ### A.3. Derivatives of functions into manifolds From 8580455fe530ea4428692419875fcb7dee5228dd Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Sat, 12 Sep 2026 11:48:07 +0200 Subject: [PATCH 14/20] refactor(Cosmology): inline the power-law scaffolding of the flat solutions The general power-law solution a = (t / t0) ^ n is stated inline in the lemmas, quantified over n; the defs powerLawScaleFactor, powerLawDensity, radiationDensity, radiationPressure and einsteinDeSitterDensity and the two _eq glue lemmas are removed, the densities and the pressure now appear in the theorem statements, and radiationScaleFactor and einsteinDeSitterScaleFactor are defined directly. Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/Solutions.lean | 220 ++++++++++++-------------- 1 file changed, 104 insertions(+), 116 deletions(-) diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index 05326f6124..d8cbefe5b1 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -32,12 +32,14 @@ coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridg - `hubbleConstant_deSitterScaleFactor`: its Hubble parameter is the constant `σ √(Λ/3) c` (for any `σ`, `Λ`, `c`). - `decelerationParameter_deSitterScaleFactor`: its deceleration parameter is `q = -1`. -- `powerLawScaleFactor`: `a(t) = (t / t₀) ^ n`, with Hubble parameter `n / t` - (`hubbleConstant_powerLawScaleFactor`) and deceleration parameter `(1 - n) / n` - (`decelerationParameter_powerLawScaleFactor`) for `t > 0`. +- `hubbleConstant_powerLaw`, `decelerationParameter_powerLaw`, `powerLaw_firstOrderFriedmann`, + `powerLaw_secondOrderFriedmann`: the flat power-law solutions `a = (t / t₀) ^ n`, stated + inline, have Hubble parameter `n / t` and deceleration parameter `(1 - n) / n`, and solve the + flat (`k = 0`, `Λ = 0`) Friedmann equations with the density `ρ = 3 n² / (8 π G t²)` and the + pressure `p = w ρ c²`, `1 + 3 w = 2 (1 - n) / n`, for `t > 0`. - `radiationScaleFactor_firstOrderFriedmann`, `radiationScaleFactor_secondOrderFriedmann`: - `a = (t / t₀) ^ (1/2)` solves the flat (`k = 0`, `Λ = 0`) Friedmann equations with the - density `ρ = 3 / (32 π G t²)` and the radiation pressure `p = ρ c² / 3`; `q = 1` and + `a = (t / t₀) ^ (1/2)` solves the flat Friedmann equations with the density + `ρ = 3 / (32 π G t²)` and the radiation pressure `p = ρ c² / 3`; `q = 1` and `H(t₀) = 1 / (2 t₀)`. - `einsteinDeSitterScaleFactor_firstOrderFriedmann`, `einsteinDeSitterScaleFactor_secondOrderFriedmann`: `a = (t / t₀) ^ (2/3)` solves the flat @@ -51,7 +53,7 @@ coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridg - A.2. The Friedmann equations - A.3. The Hubble and deceleration parameters - B. The spatially flat power-law solutions - - B.1. The power-law scale factor and its derivatives + - B.1. Derivatives of the power-law scale factor - B.2. The Hubble and deceleration parameters - B.3. The radiation-dominated solution - B.4. The Einstein-de Sitter solution @@ -189,27 +191,24 @@ lemma decelerationParameter_deSitterScaleFactor {a₀ σ Λ c : ℝ} (hΛ : 0 < ## B. The spatially flat power-law solutions The radiation-dominated and Einstein-de Sitter solutions are both of the form -`a(t) = (t / t₀) ^ n` for `t > 0`; the Hubble parameter is `n / t` and the deceleration -parameter `(1 - n) / n`. Their densities are imposed by the first-order Friedmann equation with -`k = 0` and `Λ = 0`: `ρ = 3 H² / (8 π G) = 3 n² / (8 π G t²)`. +`a(t) = (t / t₀) ^ n`; the Hubble parameter is `n / t` and the deceleration parameter +`(1 - n) / n`. Their densities are imposed by the first-order Friedmann equation with `k = 0` +and `Λ = 0`: `ρ = 3 H² / (8 π G) = 3 n² / (8 π G t²)`. The general power-law solution is +stated inline, only the two named solutions get a definition. -/ /-! -### B.1. The power-law scale factor and its derivatives +### B.1. Derivatives of the power-law scale factor -/ -/-- The power-law scale factor `a(t) = (t / t₀) ^ n` (real power). -/ -noncomputable def powerLawScaleFactor (t₀ n : ℝ) : Time → ℝ := - fun t => (t.val / t₀) ^ n - -/-- `∂ₜ a = n / t₀ (t / t₀) ^ (n - 1)` away from `t = 0`. -/ -lemma deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} - (ht : t.val ≠ 0) : - ∂ₜ (powerLawScaleFactor t₀ n) t = n / t₀ * (t.val / t₀) ^ (n - 1) := by - have h : HasDerivAt (fun y : ℝ => (y / t₀) ^ n) (n / t₀ * (t.val / t₀) ^ (n - 1)) t.val := by +/-- `∂ₜ (t / t₀) ^ n = n / t₀ (t / t₀) ^ (n - 1)` away from `t.val = 0`. -/ +lemma deriv_powerLaw {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} (ht : t.val ≠ 0) : + ∂ₜ (fun s : Time => (s.val / t₀) ^ n) t = n / t₀ * (t.val / t₀) ^ (n - 1) := by + have h : HasDerivAt (fun y : ℝ => (y / t₀) ^ n) + (n / t₀ * (t.val / t₀) ^ (n - 1)) t.val := by have h := ((hasDerivAt_id t.val).div_const t₀).rpow_const (p := n) (Or.inl (div_ne_zero ht ht₀)) refine h.congr_deriv ?_ @@ -217,11 +216,12 @@ lemma deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : ring exact deriv_comp_val h -/-- `∂ₜ ∂ₜ a = n (n - 1) / t₀² (t / t₀) ^ (n - 2)` for `t > 0`. The derivative `∂ₜ a` is - only known away from `t = 0`, which is enough since `t > 0` is an open condition. -/ -lemma deriv_deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} +/-- `∂ₜ ∂ₜ (t / t₀) ^ n = n (n - 1) / t₀² (t / t₀) ^ (n - 2)` for `0 < t.val`. The first + derivative is only known away from `t.val = 0`, which is enough since `0 < t.val` is an open + condition. -/ +lemma deriv_deriv_powerLaw {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} (ht : 0 < t.val) : - ∂ₜ (∂ₜ (powerLawScaleFactor t₀ n)) t = + ∂ₜ (∂ₜ (fun s : Time => (s.val / t₀) ^ n)) t = n / t₀ * ((n - 1) / t₀ * (t.val / t₀) ^ (n - 1 - 1)) := by apply deriv_eq_of_hasDerivAt have h₁ : HasDerivAt (fun y : ℝ => (y / t₀) ^ (n - 1)) @@ -234,7 +234,7 @@ lemma deriv_deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ have h := h₁.const_mul (n / t₀) refine h.congr_of_eventuallyEq ?_ filter_upwards [eventually_ne_nhds ht.ne'] with τ hτ - exact deriv_powerLawScaleFactor ht₀ n (t := ⟨τ⟩) hτ + exact deriv_powerLaw ht₀ n (t := ⟨τ⟩) hτ /-! @@ -242,57 +242,51 @@ lemma deriv_deriv_powerLawScaleFactor {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ -/ -/-- The Hubble parameter of the power-law solution is `n / t` for `t > 0`. -/ -lemma hubbleConstant_powerLawScaleFactor {t₀ : ℝ} (ht₀ : 0 < t₀) (n : ℝ) {t : Time} +/-- The Hubble parameter of the power-law solution is `n / t` for `0 < t.val`. -/ +lemma hubbleConstant_powerLaw {t₀ : ℝ} (ht₀ : 0 < t₀) (n : ℝ) {t : Time} (ht : 0 < t.val) : - hubbleConstant (powerLawScaleFactor t₀ n) t = n / t.val := by + hubbleConstant (fun s : Time => (s.val / t₀) ^ n) t = n / t.val := by unfold hubbleConstant - rw [deriv_powerLawScaleFactor ht₀.ne' n ht.ne', powerLawScaleFactor, - Real.rpow_sub_one (div_pos ht ht₀).ne'] + rw [deriv_powerLaw ht₀.ne' n ht.ne', Real.rpow_sub_one (div_pos ht ht₀).ne'] have hx : (t.val / t₀) ^ n ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) n).ne' field_simp -/-- The deceleration parameter of the power-law solution is `(1 - n) / n` for `t > 0`, +/-- The deceleration parameter of the power-law solution is `(1 - n) / n` for `0 < t.val`, `n ≠ 0`. -/ -lemma decelerationParameter_powerLawScaleFactor {t₀ n : ℝ} (ht₀ : 0 < t₀) (hn : n ≠ 0) +lemma decelerationParameter_powerLaw {t₀ : ℝ} {n : ℝ} (ht₀ : 0 < t₀) (hn : n ≠ 0) {t : Time} (ht : 0 < t.val) : - decelerationParameter (powerLawScaleFactor t₀ n) t = (1 - n) / n := by + decelerationParameter (fun s : Time => (s.val / t₀) ^ n) t = (1 - n) / n := by unfold decelerationParameter - rw [deriv_deriv_powerLawScaleFactor ht₀.ne' n ht, deriv_powerLawScaleFactor ht₀.ne' n ht.ne', - powerLawScaleFactor, Real.rpow_sub_one (div_pos ht ht₀).ne', - Real.rpow_sub_one (div_pos ht ht₀).ne'] + rw [deriv_deriv_powerLaw ht₀.ne' n ht, deriv_powerLaw ht₀.ne' n ht.ne', + Real.rpow_sub_one (div_pos ht ht₀).ne', Real.rpow_sub_one (div_pos ht ht₀).ne'] have hx : (t.val / t₀) ^ n ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) n).ne' field_simp ring -/-- The density imposed on the flat power-law solution by the first-order Friedmann equation, - `ρ = 3 n² / (8 π G t²)`. -/ -noncomputable def powerLawDensity (G n : ℝ) : Time → ℝ := - fun t => 3 * n ^ 2 / (8 * π * G * t.val ^ 2) - /-- The flat power-law solution solves the first-order Friedmann equation with `k = 0`, - `Λ = 0` and the density `powerLawDensity`, for `t > 0`. -/ -lemma powerLawScaleFactor_firstOrderFriedmann {t₀ G c : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) + `Λ = 0` and the density `ρ = 3 n² / (8 π G t²)` that it imposes, for `0 < t.val`. -/ +lemma powerLaw_firstOrderFriedmann {t₀ : ℝ} {G c : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) (n : ℝ) {t : Time} (ht : 0 < t.val) : - FirstOrderFriedmann (powerLawScaleFactor t₀ n) (powerLawDensity G n) 0 0 G c t := by + FirstOrderFriedmann (fun s : Time => (s.val / t₀) ^ n) + (fun s => 3 * n ^ 2 / (8 * π * G * s.val ^ 2)) 0 0 G c t := by unfold FirstOrderFriedmann - have hH := hubbleConstant_powerLawScaleFactor ht₀ n ht + have hH := hubbleConstant_powerLaw ht₀ n ht unfold hubbleConstant at hH - rw [hH, powerLawDensity] + rw [hH] have hπ := Real.pi_pos field_simp ring /-- The second-order Friedmann equation for the flat power-law solution with the pressure - `p = w ρ c²`, where `1 + 3 w = 2 (1 - n) / n`, for `t > 0`. -/ -lemma powerLawScaleFactor_secondOrderFriedmann {t₀ G c n w : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) + `p = w ρ c²`, where `1 + 3 w = 2 (1 - n) / n`, for `0 < t.val`. -/ +lemma powerLaw_secondOrderFriedmann {t₀ : ℝ} {G c n w : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) (hc : 0 < c) (hn : n ≠ 0) (hw : 1 + 3 * w = 2 * (1 - n) / n) {t : Time} (ht : 0 < t.val) : - SecondOrderFriedmann (powerLawScaleFactor t₀ n) (powerLawDensity G n) - (fun s => w * powerLawDensity G n s * c ^ 2) 0 G c t := by + SecondOrderFriedmann (fun s : Time => (s.val / t₀) ^ n) + (fun s => 3 * n ^ 2 / (8 * π * G * s.val ^ 2)) + (fun s => w * (3 * n ^ 2 / (8 * π * G * s.val ^ 2)) * c ^ 2) 0 G c t := by unfold SecondOrderFriedmann - simp only [powerLawDensity] - rw [deriv_deriv_powerLawScaleFactor ht₀.ne' n ht, powerLawScaleFactor, - Real.rpow_sub_one (div_pos ht ht₀).ne', Real.rpow_sub_one (div_pos ht ht₀).ne'] + rw [deriv_deriv_powerLaw ht₀.ne' n ht, Real.rpow_sub_one (div_pos ht ht₀).ne', + Real.rpow_sub_one (div_pos ht ht₀).ne'] have hx : (t.val / t₀) ^ n ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) n).ne' have hπ := Real.pi_pos rw [show w = (2 * (1 - n) / n - 1) / 3 by linarith] @@ -307,54 +301,50 @@ lemma powerLawScaleFactor_secondOrderFriedmann {t₀ G c n w : ℝ} (ht₀ : 0 < /-- The radiation-dominated scale factor `a(t) = (t / t₀) ^ (1/2)`. -/ noncomputable def radiationScaleFactor (t₀ : ℝ) : Time → ℝ := - powerLawScaleFactor t₀ (1 / 2) - -/-- The density of the flat radiation-dominated solution, `ρ = 3 / (32 π G t²)`, imposed by - the first-order Friedmann equation. -/ -noncomputable def radiationDensity (G : ℝ) : Time → ℝ := - fun t => 3 / (32 * π * G * t.val ^ 2) - -/-- The radiation pressure `p = ρ c² / 3`. -/ -noncomputable def radiationPressure (G c : ℝ) : Time → ℝ := - fun t => radiationDensity G t * c ^ 2 / 3 + fun t => (t.val / t₀) ^ (1 / 2 : ℝ) -lemma radiationDensity_eq (G : ℝ) : radiationDensity G = powerLawDensity G (1 / 2) := by - funext t - simp only [radiationDensity, powerLawDensity] +/-- The radiation-dominated solution solves the first-order Friedmann equation with `k = 0`, + `Λ = 0` and the density `ρ = 3 / (32 π G t²)`, for `0 < t.val`. -/ +lemma radiationScaleFactor_firstOrderFriedmann {t₀ : ℝ} {G c : ℝ} (ht₀ : 0 < t₀) + (hG : 0 < G) {t : Time} (ht : 0 < t.val) : + FirstOrderFriedmann (radiationScaleFactor t₀) (fun s => 3 / (32 * π * G * s.val ^ 2)) + 0 0 G c t := by + unfold FirstOrderFriedmann radiationScaleFactor + have hH := hubbleConstant_powerLaw ht₀ (1 / 2) ht + unfold hubbleConstant at hH + rw [hH] + have hπ := Real.pi_pos + field_simp ring -/-- The radiation-dominated solution solves the first-order Friedmann equation with `k = 0`, - `Λ = 0`, for `t > 0`. -/ -lemma radiationScaleFactor_firstOrderFriedmann {t₀ G c : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) - {t : Time} (ht : 0 < t.val) : - FirstOrderFriedmann (radiationScaleFactor t₀) (radiationDensity G) 0 0 G c t := by - rw [radiationScaleFactor, radiationDensity_eq] - exact powerLawScaleFactor_firstOrderFriedmann ht₀ hG _ ht - -/-- The radiation-dominated solution solves the second-order Friedmann equation with - `p = ρ c² / 3`, `Λ = 0`, for `t > 0`. -/ -lemma radiationScaleFactor_secondOrderFriedmann {t₀ G c : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) - (hc : 0 < c) {t : Time} (ht : 0 < t.val) : - SecondOrderFriedmann (radiationScaleFactor t₀) (radiationDensity G) (radiationPressure G c) - 0 G c t := by - have h := powerLawScaleFactor_secondOrderFriedmann (w := 1 / 3) ht₀ hG hc - (by norm_num : (1 / 2 : ℝ) ≠ 0) (by norm_num) ht - rw [radiationScaleFactor, radiationDensity_eq] - convert h using 2 - simp only [radiationPressure, radiationDensity_eq] +/-- The radiation-dominated solution solves the second-order Friedmann equation with the + density `ρ = 3 / (32 π G t²)`, the pressure `p = ρ c² / 3` and `Λ = 0`, for `0 < t.val`. -/ +lemma radiationScaleFactor_secondOrderFriedmann {t₀ : ℝ} {G c : ℝ} (ht₀ : 0 < t₀) + (hG : 0 < G) (hc : 0 < c) {t : Time} (ht : 0 < t.val) : + SecondOrderFriedmann (radiationScaleFactor t₀) (fun s => 3 / (32 * π * G * s.val ^ 2)) + (fun s => 3 / (32 * π * G * s.val ^ 2) * c ^ 2 / 3) 0 G c t := by + unfold SecondOrderFriedmann radiationScaleFactor + rw [deriv_deriv_powerLaw ht₀.ne' (1 / 2) ht, Real.rpow_sub_one (div_pos ht ht₀).ne', + Real.rpow_sub_one (div_pos ht ht₀).ne'] + have hx : (t.val / t₀) ^ (1 / 2 : ℝ) ≠ 0 := + (Real.rpow_pos_of_pos (div_pos ht ht₀) _).ne' + have hπ := Real.pi_pos + field_simp ring /-- The deceleration parameter of the radiation-dominated solution is `q = 1`. -/ lemma decelerationParameter_radiationScaleFactor {t₀ : ℝ} (ht₀ : 0 < t₀) {t : Time} (ht : 0 < t.val) : decelerationParameter (radiationScaleFactor t₀) t = 1 := by - rw [radiationScaleFactor, decelerationParameter_powerLawScaleFactor ht₀ (by norm_num) ht] + unfold radiationScaleFactor + rw [decelerationParameter_powerLaw ht₀ (by norm_num) ht] norm_num /-- `H(t₀) = 1 / (2 t₀)` for the radiation-dominated solution, that is `t₀ = 1 / (2 H₀)`. -/ lemma hubbleConstant_radiationScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < t₀) : hubbleConstant (radiationScaleFactor t₀) ⟨t₀⟩ = 1 / (2 * t₀) := by - rw [radiationScaleFactor, hubbleConstant_powerLawScaleFactor ht₀ _ ht₀] + unfold radiationScaleFactor + rw [hubbleConstant_powerLaw ht₀ _ ht₀] ring /-! @@ -365,52 +355,50 @@ lemma hubbleConstant_radiationScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < t₀) : /-- The Einstein-de Sitter (flat, dust) scale factor `a(t) = (t / t₀) ^ (2/3)`. -/ noncomputable def einsteinDeSitterScaleFactor (t₀ : ℝ) : Time → ℝ := - powerLawScaleFactor t₀ (2 / 3) - -/-- The dust density of the Einstein-de Sitter solution, `ρ = 1 / (6 π G t²)`, imposed by the - first-order Friedmann equation. -/ -noncomputable def einsteinDeSitterDensity (G : ℝ) : Time → ℝ := - fun t => 1 / (6 * π * G * t.val ^ 2) - -lemma einsteinDeSitterDensity_eq (G : ℝ) : - einsteinDeSitterDensity G = powerLawDensity G (2 / 3) := by - funext t - simp only [einsteinDeSitterDensity, powerLawDensity] - ring + fun t => (t.val / t₀) ^ (2 / 3 : ℝ) /-- The Einstein-de Sitter solution solves the first-order Friedmann equation with `k = 0`, - `Λ = 0`, for `t > 0`. -/ -lemma einsteinDeSitterScaleFactor_firstOrderFriedmann {t₀ G c : ℝ} (ht₀ : 0 < t₀) + `Λ = 0` and the dust density `ρ = 1 / (6 π G t²)`, for `0 < t.val`. -/ +lemma einsteinDeSitterScaleFactor_firstOrderFriedmann {t₀ : ℝ} {G c : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) {t : Time} (ht : 0 < t.val) : - FirstOrderFriedmann (einsteinDeSitterScaleFactor t₀) (einsteinDeSitterDensity G) + FirstOrderFriedmann (einsteinDeSitterScaleFactor t₀) (fun s => 1 / (6 * π * G * s.val ^ 2)) 0 0 G c t := by - rw [einsteinDeSitterScaleFactor, einsteinDeSitterDensity_eq] - exact powerLawScaleFactor_firstOrderFriedmann ht₀ hG _ ht + unfold FirstOrderFriedmann einsteinDeSitterScaleFactor + have hH := hubbleConstant_powerLaw ht₀ (2 / 3) ht + unfold hubbleConstant at hH + rw [hH] + have hπ := Real.pi_pos + field_simp + ring -/-- The Einstein-de Sitter solution solves the second-order Friedmann equation with `p = 0`, - `Λ = 0`, for `t > 0`. -/ -lemma einsteinDeSitterScaleFactor_secondOrderFriedmann {t₀ G c : ℝ} (ht₀ : 0 < t₀) +/-- The Einstein-de Sitter solution solves the second-order Friedmann equation with the dust + density `ρ = 1 / (6 π G t²)`, `p = 0` and `Λ = 0`, for `0 < t.val`. -/ +lemma einsteinDeSitterScaleFactor_secondOrderFriedmann {t₀ : ℝ} {G c : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) (hc : 0 < c) {t : Time} (ht : 0 < t.val) : - SecondOrderFriedmann (einsteinDeSitterScaleFactor t₀) (einsteinDeSitterDensity G) + SecondOrderFriedmann (einsteinDeSitterScaleFactor t₀) (fun s => 1 / (6 * π * G * s.val ^ 2)) (fun _ => 0) 0 G c t := by - have h := powerLawScaleFactor_secondOrderFriedmann (w := 0) ht₀ hG hc - (by norm_num : (2 / 3 : ℝ) ≠ 0) (by norm_num) ht - rw [einsteinDeSitterScaleFactor, einsteinDeSitterDensity_eq] - convert h using 2 + unfold SecondOrderFriedmann einsteinDeSitterScaleFactor + rw [deriv_deriv_powerLaw ht₀.ne' (2 / 3) ht, Real.rpow_sub_one (div_pos ht ht₀).ne', + Real.rpow_sub_one (div_pos ht ht₀).ne'] + have hx : (t.val / t₀) ^ (2 / 3 : ℝ) ≠ 0 := + (Real.rpow_pos_of_pos (div_pos ht ht₀) _).ne' + have hπ := Real.pi_pos + field_simp ring /-- The deceleration parameter of the Einstein-de Sitter solution is `q = 1 / 2`. -/ -lemma decelerationParameter_einsteinDeSitterScaleFactor {t₀ : ℝ} (ht₀ : 0 < t₀) {t : Time} - (ht : 0 < t.val) : +lemma decelerationParameter_einsteinDeSitterScaleFactor {t₀ : ℝ} (ht₀ : 0 < t₀) + {t : Time} (ht : 0 < t.val) : decelerationParameter (einsteinDeSitterScaleFactor t₀) t = 1 / 2 := by - rw [einsteinDeSitterScaleFactor, - decelerationParameter_powerLawScaleFactor ht₀ (by norm_num) ht] + unfold einsteinDeSitterScaleFactor + rw [decelerationParameter_powerLaw ht₀ (by norm_num) ht] norm_num /-- `H(t₀) = 2 / (3 t₀)` for the Einstein-de Sitter solution, that is `t₀ = 2 / (3 H₀)`. -/ lemma hubbleConstant_einsteinDeSitterScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < t₀) : hubbleConstant (einsteinDeSitterScaleFactor t₀) ⟨t₀⟩ = 2 / (3 * t₀) := by - rw [einsteinDeSitterScaleFactor, hubbleConstant_powerLawScaleFactor ht₀ _ ht₀] + unfold einsteinDeSitterScaleFactor + rw [hubbleConstant_powerLaw ht₀ _ ht₀] ring /-! From 1a2cb0d1e827063c3dfc2169713122008cfb8549 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Sat, 12 Sep 2026 11:48:53 +0200 Subject: [PATCH 15/20] refactor(Cosmology): the normalisation epoch of the power-law solutions is a Time t0 : Time instead of a real number in the power-law, radiation-dominated and Einstein-de Sitter solutions (so H(t0) is stated at t0 itself), and docstrings saying that t0 is the normalisation epoch a(t0) = 1, that the Big Bang sits at the origin t.val = 0 of the time chart, and that the values for t.val <= 0 are junk. Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/Solutions.lean | 94 +++++++++++++++------------ 1 file changed, 53 insertions(+), 41 deletions(-) diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index d8cbefe5b1..7434803095 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -46,6 +46,9 @@ coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridg Friedmann equations with the dust density `ρ = 1 / (6 π G t²)` and `p = 0`; `q = 1 / 2` and `H(t₀) = 2 / (3 t₀)`. +In the power-law solutions `t₀ : Time` is the normalisation epoch (`a(t₀) = 1`) and the Big +Bang is at the origin `t.val = 0` of the time chart. + ## iii. Table of contents - A. The de Sitter solution @@ -196,6 +199,11 @@ The radiation-dominated and Einstein-de Sitter solutions are both of the form and `Λ = 0`: `ρ = 3 H² / (8 π G) = 3 n² / (8 π G t²)`. The general power-law solution is stated inline, only the two named solutions get a definition. +Throughout, `t₀` is the normalisation epoch, `a(t₀) = 1`, the Big Bang sits at the origin +`t.val = 0` of the time chart (`Time` has no distinguished origin by itself), and the values +for `t.val ≤ 0` are junk (`Real.rpow` on a non-positive base); every statement therefore +assumes `0 < t.val`. + -/ /-! @@ -205,11 +213,11 @@ stated inline, only the two named solutions get a definition. -/ /-- `∂ₜ (t / t₀) ^ n = n / t₀ (t / t₀) ^ (n - 1)` away from `t.val = 0`. -/ -lemma deriv_powerLaw {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} (ht : t.val ≠ 0) : - ∂ₜ (fun s : Time => (s.val / t₀) ^ n) t = n / t₀ * (t.val / t₀) ^ (n - 1) := by - have h : HasDerivAt (fun y : ℝ => (y / t₀) ^ n) - (n / t₀ * (t.val / t₀) ^ (n - 1)) t.val := by - have h := ((hasDerivAt_id t.val).div_const t₀).rpow_const (p := n) +lemma deriv_powerLaw {t₀ : Time} (ht₀ : t₀.val ≠ 0) (n : ℝ) {t : Time} (ht : t.val ≠ 0) : + ∂ₜ (fun s : Time => (s.val / t₀.val) ^ n) t = n / t₀.val * (t.val / t₀.val) ^ (n - 1) := by + have h : HasDerivAt (fun y : ℝ => (y / t₀.val) ^ n) + (n / t₀.val * (t.val / t₀.val) ^ (n - 1)) t.val := by + have h := ((hasDerivAt_id t.val).div_const t₀.val).rpow_const (p := n) (Or.inl (div_ne_zero ht ht₀)) refine h.congr_deriv ?_ simp only [id_eq] @@ -219,19 +227,19 @@ lemma deriv_powerLaw {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} (ht /-- `∂ₜ ∂ₜ (t / t₀) ^ n = n (n - 1) / t₀² (t / t₀) ^ (n - 2)` for `0 < t.val`. The first derivative is only known away from `t.val = 0`, which is enough since `0 < t.val` is an open condition. -/ -lemma deriv_deriv_powerLaw {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time} +lemma deriv_deriv_powerLaw {t₀ : Time} (ht₀ : t₀.val ≠ 0) (n : ℝ) {t : Time} (ht : 0 < t.val) : - ∂ₜ (∂ₜ (fun s : Time => (s.val / t₀) ^ n)) t = - n / t₀ * ((n - 1) / t₀ * (t.val / t₀) ^ (n - 1 - 1)) := by + ∂ₜ (∂ₜ (fun s : Time => (s.val / t₀.val) ^ n)) t = + n / t₀.val * ((n - 1) / t₀.val * (t.val / t₀.val) ^ (n - 1 - 1)) := by apply deriv_eq_of_hasDerivAt - have h₁ : HasDerivAt (fun y : ℝ => (y / t₀) ^ (n - 1)) - ((n - 1) / t₀ * (t.val / t₀) ^ (n - 1 - 1)) t.val := by - have h := ((hasDerivAt_id t.val).div_const t₀).rpow_const (p := n - 1) + have h₁ : HasDerivAt (fun y : ℝ => (y / t₀.val) ^ (n - 1)) + ((n - 1) / t₀.val * (t.val / t₀.val) ^ (n - 1 - 1)) t.val := by + have h := ((hasDerivAt_id t.val).div_const t₀.val).rpow_const (p := n - 1) (Or.inl (div_ne_zero ht.ne' ht₀)) refine h.congr_deriv ?_ simp only [id_eq] ring - have h := h₁.const_mul (n / t₀) + have h := h₁.const_mul (n / t₀.val) refine h.congr_of_eventuallyEq ?_ filter_upwards [eventually_ne_nhds ht.ne'] with τ hτ exact deriv_powerLaw ht₀ n (t := ⟨τ⟩) hτ @@ -243,31 +251,31 @@ lemma deriv_deriv_powerLaw {t₀ : ℝ} (ht₀ : t₀ ≠ 0) (n : ℝ) {t : Time -/ /-- The Hubble parameter of the power-law solution is `n / t` for `0 < t.val`. -/ -lemma hubbleConstant_powerLaw {t₀ : ℝ} (ht₀ : 0 < t₀) (n : ℝ) {t : Time} +lemma hubbleConstant_powerLaw {t₀ : Time} (ht₀ : 0 < t₀.val) (n : ℝ) {t : Time} (ht : 0 < t.val) : - hubbleConstant (fun s : Time => (s.val / t₀) ^ n) t = n / t.val := by + hubbleConstant (fun s : Time => (s.val / t₀.val) ^ n) t = n / t.val := by unfold hubbleConstant rw [deriv_powerLaw ht₀.ne' n ht.ne', Real.rpow_sub_one (div_pos ht ht₀).ne'] - have hx : (t.val / t₀) ^ n ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) n).ne' + have hx : (t.val / t₀.val) ^ n ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) n).ne' field_simp /-- The deceleration parameter of the power-law solution is `(1 - n) / n` for `0 < t.val`, `n ≠ 0`. -/ -lemma decelerationParameter_powerLaw {t₀ : ℝ} {n : ℝ} (ht₀ : 0 < t₀) (hn : n ≠ 0) +lemma decelerationParameter_powerLaw {t₀ : Time} {n : ℝ} (ht₀ : 0 < t₀.val) (hn : n ≠ 0) {t : Time} (ht : 0 < t.val) : - decelerationParameter (fun s : Time => (s.val / t₀) ^ n) t = (1 - n) / n := by + decelerationParameter (fun s : Time => (s.val / t₀.val) ^ n) t = (1 - n) / n := by unfold decelerationParameter rw [deriv_deriv_powerLaw ht₀.ne' n ht, deriv_powerLaw ht₀.ne' n ht.ne', Real.rpow_sub_one (div_pos ht ht₀).ne', Real.rpow_sub_one (div_pos ht ht₀).ne'] - have hx : (t.val / t₀) ^ n ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) n).ne' + have hx : (t.val / t₀.val) ^ n ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) n).ne' field_simp ring /-- The flat power-law solution solves the first-order Friedmann equation with `k = 0`, `Λ = 0` and the density `ρ = 3 n² / (8 π G t²)` that it imposes, for `0 < t.val`. -/ -lemma powerLaw_firstOrderFriedmann {t₀ : ℝ} {G c : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) +lemma powerLaw_firstOrderFriedmann {t₀ : Time} {G c : ℝ} (ht₀ : 0 < t₀.val) (hG : 0 < G) (n : ℝ) {t : Time} (ht : 0 < t.val) : - FirstOrderFriedmann (fun s : Time => (s.val / t₀) ^ n) + FirstOrderFriedmann (fun s : Time => (s.val / t₀.val) ^ n) (fun s => 3 * n ^ 2 / (8 * π * G * s.val ^ 2)) 0 0 G c t := by unfold FirstOrderFriedmann have hH := hubbleConstant_powerLaw ht₀ n ht @@ -279,15 +287,15 @@ lemma powerLaw_firstOrderFriedmann {t₀ : ℝ} {G c : ℝ} (ht₀ : 0 < t₀) ( /-- The second-order Friedmann equation for the flat power-law solution with the pressure `p = w ρ c²`, where `1 + 3 w = 2 (1 - n) / n`, for `0 < t.val`. -/ -lemma powerLaw_secondOrderFriedmann {t₀ : ℝ} {G c n w : ℝ} (ht₀ : 0 < t₀) (hG : 0 < G) +lemma powerLaw_secondOrderFriedmann {t₀ : Time} {G c n w : ℝ} (ht₀ : 0 < t₀.val) (hG : 0 < G) (hc : 0 < c) (hn : n ≠ 0) (hw : 1 + 3 * w = 2 * (1 - n) / n) {t : Time} (ht : 0 < t.val) : - SecondOrderFriedmann (fun s : Time => (s.val / t₀) ^ n) + SecondOrderFriedmann (fun s : Time => (s.val / t₀.val) ^ n) (fun s => 3 * n ^ 2 / (8 * π * G * s.val ^ 2)) (fun s => w * (3 * n ^ 2 / (8 * π * G * s.val ^ 2)) * c ^ 2) 0 G c t := by unfold SecondOrderFriedmann rw [deriv_deriv_powerLaw ht₀.ne' n ht, Real.rpow_sub_one (div_pos ht ht₀).ne', Real.rpow_sub_one (div_pos ht ht₀).ne'] - have hx : (t.val / t₀) ^ n ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) n).ne' + have hx : (t.val / t₀.val) ^ n ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) n).ne' have hπ := Real.pi_pos rw [show w = (2 * (1 - n) / n - 1) / 3 by linarith] field_simp @@ -299,13 +307,15 @@ lemma powerLaw_secondOrderFriedmann {t₀ : ℝ} {G c n w : ℝ} (ht₀ : 0 < t -/ -/-- The radiation-dominated scale factor `a(t) = (t / t₀) ^ (1/2)`. -/ -noncomputable def radiationScaleFactor (t₀ : ℝ) : Time → ℝ := - fun t => (t.val / t₀) ^ (1 / 2 : ℝ) +/-- The radiation-dominated scale factor `a(t) = (t / t₀) ^ (1/2)`, normalised by `a(t₀) = 1`. + The Big Bang is at the origin `t.val = 0` of the time chart; the values for `t.val ≤ 0` are + junk. -/ +noncomputable def radiationScaleFactor (t₀ : Time) : Time → ℝ := + fun t => (t.val / t₀.val) ^ (1 / 2 : ℝ) /-- The radiation-dominated solution solves the first-order Friedmann equation with `k = 0`, `Λ = 0` and the density `ρ = 3 / (32 π G t²)`, for `0 < t.val`. -/ -lemma radiationScaleFactor_firstOrderFriedmann {t₀ : ℝ} {G c : ℝ} (ht₀ : 0 < t₀) +lemma radiationScaleFactor_firstOrderFriedmann {t₀ : Time} {G c : ℝ} (ht₀ : 0 < t₀.val) (hG : 0 < G) {t : Time} (ht : 0 < t.val) : FirstOrderFriedmann (radiationScaleFactor t₀) (fun s => 3 / (32 * π * G * s.val ^ 2)) 0 0 G c t := by @@ -319,21 +329,21 @@ lemma radiationScaleFactor_firstOrderFriedmann {t₀ : ℝ} {G c : ℝ} (ht₀ : /-- The radiation-dominated solution solves the second-order Friedmann equation with the density `ρ = 3 / (32 π G t²)`, the pressure `p = ρ c² / 3` and `Λ = 0`, for `0 < t.val`. -/ -lemma radiationScaleFactor_secondOrderFriedmann {t₀ : ℝ} {G c : ℝ} (ht₀ : 0 < t₀) +lemma radiationScaleFactor_secondOrderFriedmann {t₀ : Time} {G c : ℝ} (ht₀ : 0 < t₀.val) (hG : 0 < G) (hc : 0 < c) {t : Time} (ht : 0 < t.val) : SecondOrderFriedmann (radiationScaleFactor t₀) (fun s => 3 / (32 * π * G * s.val ^ 2)) (fun s => 3 / (32 * π * G * s.val ^ 2) * c ^ 2 / 3) 0 G c t := by unfold SecondOrderFriedmann radiationScaleFactor rw [deriv_deriv_powerLaw ht₀.ne' (1 / 2) ht, Real.rpow_sub_one (div_pos ht ht₀).ne', Real.rpow_sub_one (div_pos ht ht₀).ne'] - have hx : (t.val / t₀) ^ (1 / 2 : ℝ) ≠ 0 := + have hx : (t.val / t₀.val) ^ (1 / 2 : ℝ) ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) _).ne' have hπ := Real.pi_pos field_simp ring /-- The deceleration parameter of the radiation-dominated solution is `q = 1`. -/ -lemma decelerationParameter_radiationScaleFactor {t₀ : ℝ} (ht₀ : 0 < t₀) {t : Time} +lemma decelerationParameter_radiationScaleFactor {t₀ : Time} (ht₀ : 0 < t₀.val) {t : Time} (ht : 0 < t.val) : decelerationParameter (radiationScaleFactor t₀) t = 1 := by unfold radiationScaleFactor @@ -341,8 +351,8 @@ lemma decelerationParameter_radiationScaleFactor {t₀ : ℝ} (ht₀ : 0 < t₀) norm_num /-- `H(t₀) = 1 / (2 t₀)` for the radiation-dominated solution, that is `t₀ = 1 / (2 H₀)`. -/ -lemma hubbleConstant_radiationScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < t₀) : - hubbleConstant (radiationScaleFactor t₀) ⟨t₀⟩ = 1 / (2 * t₀) := by +lemma hubbleConstant_radiationScaleFactor_t₀ {t₀ : Time} (ht₀ : 0 < t₀.val) : + hubbleConstant (radiationScaleFactor t₀) t₀ = 1 / (2 * t₀.val) := by unfold radiationScaleFactor rw [hubbleConstant_powerLaw ht₀ _ ht₀] ring @@ -353,13 +363,15 @@ lemma hubbleConstant_radiationScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < t₀) : -/ -/-- The Einstein-de Sitter (flat, dust) scale factor `a(t) = (t / t₀) ^ (2/3)`. -/ -noncomputable def einsteinDeSitterScaleFactor (t₀ : ℝ) : Time → ℝ := - fun t => (t.val / t₀) ^ (2 / 3 : ℝ) +/-- The Einstein-de Sitter (flat, dust) scale factor `a(t) = (t / t₀) ^ (2/3)`, normalised by + `a(t₀) = 1`. The Big Bang is at the origin `t.val = 0` of the time chart; the values for + `t.val ≤ 0` are junk. -/ +noncomputable def einsteinDeSitterScaleFactor (t₀ : Time) : Time → ℝ := + fun t => (t.val / t₀.val) ^ (2 / 3 : ℝ) /-- The Einstein-de Sitter solution solves the first-order Friedmann equation with `k = 0`, `Λ = 0` and the dust density `ρ = 1 / (6 π G t²)`, for `0 < t.val`. -/ -lemma einsteinDeSitterScaleFactor_firstOrderFriedmann {t₀ : ℝ} {G c : ℝ} (ht₀ : 0 < t₀) +lemma einsteinDeSitterScaleFactor_firstOrderFriedmann {t₀ : Time} {G c : ℝ} (ht₀ : 0 < t₀.val) (hG : 0 < G) {t : Time} (ht : 0 < t.val) : FirstOrderFriedmann (einsteinDeSitterScaleFactor t₀) (fun s => 1 / (6 * π * G * s.val ^ 2)) 0 0 G c t := by @@ -373,21 +385,21 @@ lemma einsteinDeSitterScaleFactor_firstOrderFriedmann {t₀ : ℝ} {G c : ℝ} ( /-- The Einstein-de Sitter solution solves the second-order Friedmann equation with the dust density `ρ = 1 / (6 π G t²)`, `p = 0` and `Λ = 0`, for `0 < t.val`. -/ -lemma einsteinDeSitterScaleFactor_secondOrderFriedmann {t₀ : ℝ} {G c : ℝ} (ht₀ : 0 < t₀) +lemma einsteinDeSitterScaleFactor_secondOrderFriedmann {t₀ : Time} {G c : ℝ} (ht₀ : 0 < t₀.val) (hG : 0 < G) (hc : 0 < c) {t : Time} (ht : 0 < t.val) : SecondOrderFriedmann (einsteinDeSitterScaleFactor t₀) (fun s => 1 / (6 * π * G * s.val ^ 2)) (fun _ => 0) 0 G c t := by unfold SecondOrderFriedmann einsteinDeSitterScaleFactor rw [deriv_deriv_powerLaw ht₀.ne' (2 / 3) ht, Real.rpow_sub_one (div_pos ht ht₀).ne', Real.rpow_sub_one (div_pos ht ht₀).ne'] - have hx : (t.val / t₀) ^ (2 / 3 : ℝ) ≠ 0 := + have hx : (t.val / t₀.val) ^ (2 / 3 : ℝ) ≠ 0 := (Real.rpow_pos_of_pos (div_pos ht ht₀) _).ne' have hπ := Real.pi_pos field_simp ring /-- The deceleration parameter of the Einstein-de Sitter solution is `q = 1 / 2`. -/ -lemma decelerationParameter_einsteinDeSitterScaleFactor {t₀ : ℝ} (ht₀ : 0 < t₀) +lemma decelerationParameter_einsteinDeSitterScaleFactor {t₀ : Time} (ht₀ : 0 < t₀.val) {t : Time} (ht : 0 < t.val) : decelerationParameter (einsteinDeSitterScaleFactor t₀) t = 1 / 2 := by unfold einsteinDeSitterScaleFactor @@ -395,8 +407,8 @@ lemma decelerationParameter_einsteinDeSitterScaleFactor {t₀ : ℝ} (ht₀ : 0 norm_num /-- `H(t₀) = 2 / (3 t₀)` for the Einstein-de Sitter solution, that is `t₀ = 2 / (3 H₀)`. -/ -lemma hubbleConstant_einsteinDeSitterScaleFactor_t₀ {t₀ : ℝ} (ht₀ : 0 < t₀) : - hubbleConstant (einsteinDeSitterScaleFactor t₀) ⟨t₀⟩ = 2 / (3 * t₀) := by +lemma hubbleConstant_einsteinDeSitterScaleFactor_t₀ {t₀ : Time} (ht₀ : 0 < t₀.val) : + hubbleConstant (einsteinDeSitterScaleFactor t₀) t₀ = 2 / (3 * t₀.val) := by unfold einsteinDeSitterScaleFactor rw [hubbleConstant_powerLaw ht₀ _ ht₀] ring From 076b0e508bd5e6efd93c1914dc4947fa3e878e53 Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Sat, 12 Sep 2026 11:59:57 +0200 Subject: [PATCH 16/20] docs(Cosmology): the Milne scale factor puts the Big Bang at the origin of the time chart Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/Solutions.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index 9a2d36cbad..7cc9915ee2 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -434,7 +434,8 @@ curvature) is not stated here: the FLRW metric is not yet an object of Physlib. -/ -/-- The Milne scale factor `a(t) = c t`. -/ +/-- The Milne scale factor `a(t) = c t`. The Big Bang is at the origin `t.val = 0` of the time + chart; the values for `t.val ≤ 0` are not part of the model. -/ noncomputable def milneScaleFactor (c : ℝ) : Time → ℝ := fun t => c * t.val From 9e97b70fe5654968af29720718b5b349f35e471e Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Sat, 12 Sep 2026 12:00:40 +0200 Subject: [PATCH 17/20] refactor(Cosmology): state the Einstein static density directly The density of the Einstein static universe is stated as rho = Lambda c^2 / (4 pi G); the def cosmologicalConstantDensity is dropped from this file, the cosmological constant as a w = -1 fluid being the matter-content TODO of Physlib.Cosmology.FLRW.MatterContent. Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/Solutions.lean | 16 ++++++---------- 1 file changed, 6 insertions(+), 10 deletions(-) diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index 7cc9915ee2..d7edead1d4 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -52,7 +52,7 @@ coordinate `t.val`. Its time derivative `∂ₜ a` is computed through the bridg scale factor `a = c t` solves the empty (`ρ = 0`, `p = 0`, `Λ = 0`) Friedmann equations with `k = -1`; `q = 0`. - `einsteinStatic_density`, `einsteinStatic_curvature`: if `∂ₜ a = ∂ₜ ∂ₜ a = 0` at `t` and the - Friedmann equations hold there with `p = 0`, then `ρ = Λ c² / (4 π G) = 2 ρ_Λ` and + Friedmann equations hold there with `p = 0`, then `ρ = Λ c² / (4 π G)` and `k c² / a² = 4 π G ρ`, so that `k > 0` when `ρ > 0` (`einsteinStatic_curvature_pos`). In the power-law solutions `t₀ : Time` is the normalisation epoch (`a(t₀) = 1`) and the Big @@ -478,24 +478,20 @@ lemma decelerationParameter_milneScaleFactor (c : ℝ) (t : Time) : ## D. The Einstein static universe At an instant where `∂ₜ a = ∂ₜ ∂ₜ a = 0`, the two Friedmann equations with dust (`p = 0`) -force the density `ρ = Λ c² / (4 π G)`, twice the density `ρ_Λ = Λ c² / (8 π G)` associated -with the cosmological constant, and `k c² / a² = 4 π G ρ`, hence a positive curvature +force the density `ρ = Λ c² / (4 π G)` (twice the density `Λ c² / (8 π G)` that the +cosmological constant carries as a `w = -1` fluid, a matter-content statement that belongs to +`Physlib.Cosmology.FLRW.MatterContent`) and `k c² / a² = 4 π G ρ`, hence a positive curvature parameter when `ρ > 0`. That this equilibrium is unstable is not stated here. -/ -/-- The density `ρ_Λ = Λ c² / (8 π G)` associated with the cosmological constant. -/ -noncomputable def cosmologicalConstantDensity (Λ G c : ℝ) : ℝ := - Λ * c ^ 2 / (8 * π * G) - -/-- In the Einstein static universe the dust density is `ρ = Λ c² / (4 π G) = 2 ρ_Λ`. -/ +/-- In the Einstein static universe the dust density is `ρ = Λ c² / (4 π G)`. -/ lemma einsteinStatic_density {a ρ : Time → ℝ} {Λ G c : ℝ} {t : Time} (hG : 0 < G) (h2 : ∂ₜ (∂ₜ a) t = 0) (hF2 : SecondOrderFriedmann a ρ (fun _ => 0) Λ G c t) : - ρ t = 2 * cosmologicalConstantDensity Λ G c := by + ρ t = Λ * c ^ 2 / (4 * π * G) := by unfold SecondOrderFriedmann at hF2 rw [h2, zero_div] at hF2 simp only [mul_zero, zero_div, add_zero] at hF2 - unfold cosmologicalConstantDensity have hπ := Real.pi_pos field_simp linarith From e29b83e8ebe2e21668d49959290f95849534b10a Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 17 Sep 2026 11:08:18 +0200 Subject: [PATCH 18/20] refactor(Time, Cosmology): state the HasDerivAt bridge and deriv_firstOrderFriedmann at t : Time MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Review of #1635 by doxtor6. Time.hasDerivAt_mk_of_differentiableAt is stated at t : Time (derivative at t.val) instead of at the constructor form with a real parameter, so that callers no longer destructure t; deriv_firstOrderFriedmann is stated at t : Time as well and destructures inside its proof, and the two theorems of MatterContent.lean no longer do. Time.deriv_comp_val is dropped: it is the special case f := fun s => g s.val of Time.deriv_eq_of_hasDerivAt, which replaces it in Solutions.lean (its only user). The two surviving bridges are listed in the key results of Time/Derivatives.lean. Nits: continuityEquation_of_friedmann only needs G ≠ 0; the non-vanishing hypothesis of secondOrderFriedmann_of_continuityEquation is named ha'; the overview names the bridge the proofs actually use. Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/MatterContent.lean | 36 ++++++++++------------ Physlib/Cosmology/FLRW/Solutions.lean | 10 +++--- Physlib/SpaceAndTime/Time/Derivatives.lean | 19 +++++------- 3 files changed, 29 insertions(+), 36 deletions(-) diff --git a/Physlib/Cosmology/FLRW/MatterContent.lean b/Physlib/Cosmology/FLRW/MatterContent.lean index 9dff827dc5..52c5204ff6 100644 --- a/Physlib/Cosmology/FLRW/MatterContent.lean +++ b/Physlib/Cosmology/FLRW/MatterContent.lean @@ -23,7 +23,7 @@ independent. The equation of state, the density scaling laws and the perfect-flu stress-energy tensor are still TODO items. Time derivatives of curves `Time → ℝ` are computed through the bridge -`Time.hasDerivAt_comp_toRealCLE_symm` to Mathlib's `HasDerivAt` on `ℝ`. +`Time.hasDerivAt_mk_of_differentiableAt` to Mathlib's `HasDerivAt` on `ℝ`. ## ii. Key results @@ -75,14 +75,14 @@ def ContinuityEquation (a ρ p : Time → ℝ) (c : ℝ) (t : Time) : Prop := -/ -/-- Differentiating the first-order Friedmann equation, assumed at all times, at `⟨τ⟩`: +/-- Differentiating the first-order Friedmann equation, assumed at all times, at `t`: `2 H (a''/a - H²) = (8 π G / 3) ρ' + 2 k c² H / a²`. -/ -lemma deriv_firstOrderFriedmann {a ρ : Time → ℝ} {k Λ G c τ : ℝ} (ha : a ⟨τ⟩ ≠ 0) - (hd1 : DifferentiableAt ℝ a ⟨τ⟩) (hd2 : DifferentiableAt ℝ (∂ₜ a) ⟨τ⟩) - (hdρ : DifferentiableAt ℝ ρ ⟨τ⟩) (hF1 : ∀ s, FirstOrderFriedmann a ρ k Λ G c s) : - 2 * (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) * (∂ₜ (∂ₜ a) ⟨τ⟩ / a ⟨τ⟩ - (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) ^ 2) - = 8 * π * G / 3 * ∂ₜ ρ ⟨τ⟩ - + 2 * k * c ^ 2 * (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) / (a ⟨τ⟩) ^ 2 := by +lemma deriv_firstOrderFriedmann {a ρ : Time → ℝ} {k Λ G c : ℝ} {t : Time} (ha : a t ≠ 0) + (hd1 : DifferentiableAt ℝ a t) (hd2 : DifferentiableAt ℝ (∂ₜ a) t) + (hdρ : DifferentiableAt ℝ ρ t) (hF1 : ∀ s, FirstOrderFriedmann a ρ k Λ G c s) : + 2 * (∂ₜ a t / a t) * (∂ₜ (∂ₜ a) t / a t - (∂ₜ a t / a t) ^ 2) + = 8 * π * G / 3 * ∂ₜ ρ t + 2 * k * c ^ 2 * (∂ₜ a t / a t) / (a t) ^ 2 := by + obtain ⟨τ⟩ := t have hA := hasDerivAt_mk_of_differentiableAt hd1 have hA' := hasDerivAt_mk_of_differentiableAt hd2 have hR := hasDerivAt_mk_of_differentiableAt hdρ @@ -107,22 +107,19 @@ lemma deriv_firstOrderFriedmann {a ρ : Time → ℝ} {k Λ G c τ : ℝ} (ha : times, and the second-order Friedmann equation at `t`; `a` must be twice differentiable and `ρ` differentiable at `t`. -/ lemma continuityEquation_of_friedmann {a ρ p : Time → ℝ} {k Λ G c : ℝ} {t : Time} - (hG : 0 < G) (ha : a t ≠ 0) (hd1 : DifferentiableAt ℝ a t) + (hG : G ≠ 0) (ha : a t ≠ 0) (hd1 : DifferentiableAt ℝ a t) (hd2 : DifferentiableAt ℝ (∂ₜ a) t) (hdρ : DifferentiableAt ℝ ρ t) (hF1 : ∀ s, FirstOrderFriedmann a ρ k Λ G c s) (hF2 : SecondOrderFriedmann a ρ p Λ G c t) : ContinuityEquation a ρ p c t := by - obtain ⟨τ⟩ := t have hd := deriv_firstOrderFriedmann ha hd1 hd2 hdρ hF1 - have h1 := hF1 ⟨τ⟩ + have h1 := hF1 t unfold FirstOrderFriedmann at h1 unfold SecondOrderFriedmann at hF2 unfold ContinuityEquation hubbleConstant - have hπ := Real.pi_pos have hG3 : 8 * π * G / 3 ≠ 0 := by positivity apply mul_left_cancel₀ hG3 - linear_combination -hd + 2 * (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) * hF2 - - 2 * (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) * h1 + linear_combination -hd + 2 * (∂ₜ a t / a t) * hF2 - 2 * (∂ₜ a t / a t) * h1 /-! @@ -134,21 +131,20 @@ lemma continuityEquation_of_friedmann {a ρ p : Time → ℝ} {k Λ G c : ℝ} { equation, assumed at all times, and the continuity equation at `t`, provided `∂ₜ a t ≠ 0`. Together with `continuityEquation_of_friedmann`, the three equations are not independent. -/ lemma secondOrderFriedmann_of_continuityEquation {a ρ p : Time → ℝ} {k Λ G c : ℝ} - {t : Time} (ha : a t ≠ 0) (hd1' : ∂ₜ a t ≠ 0) (hd1 : DifferentiableAt ℝ a t) + {t : Time} (ha : a t ≠ 0) (ha' : ∂ₜ a t ≠ 0) (hd1 : DifferentiableAt ℝ a t) (hd2 : DifferentiableAt ℝ (∂ₜ a) t) (hdρ : DifferentiableAt ℝ ρ t) (hF1 : ∀ s, FirstOrderFriedmann a ρ k Λ G c s) (hC : ContinuityEquation a ρ p c t) : SecondOrderFriedmann a ρ p Λ G c t := by - obtain ⟨τ⟩ := t have hd := deriv_firstOrderFriedmann ha hd1 hd2 hdρ hF1 - have h1 := hF1 ⟨τ⟩ + have h1 := hF1 t unfold FirstOrderFriedmann at h1 unfold ContinuityEquation hubbleConstant at hC unfold SecondOrderFriedmann - have hH : 2 * (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) ≠ 0 := by - have : ∂ₜ a ⟨τ⟩ / a ⟨τ⟩ ≠ 0 := div_ne_zero hd1' ha + have hH : 2 * (∂ₜ a t / a t) ≠ 0 := by + have : ∂ₜ a t / a t ≠ 0 := div_ne_zero ha' ha positivity apply mul_left_cancel₀ hH - linear_combination hd + 8 * π * G / 3 * hC + 2 * (∂ₜ a ⟨τ⟩ / a ⟨τ⟩) * h1 + linear_combination hd + 8 * π * G / 3 * hC + 2 * (∂ₜ a t / a t) * h1 /-! diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index d7edead1d4..62f98fbe52 100644 --- a/Physlib/Cosmology/FLRW/Solutions.lean +++ b/Physlib/Cosmology/FLRW/Solutions.lean @@ -108,7 +108,7 @@ lemma deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : refine h.congr_deriv ?_ simp only [id_eq] ring - exact deriv_comp_val h + exact deriv_eq_of_hasDerivAt h lemma deriv_deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : ∂ₜ (∂ₜ (deSitterScaleFactor a₀ σ Λ c)) = @@ -124,7 +124,7 @@ lemma deriv_deriv_deSitterScaleFactor (a₀ σ Λ c : ℝ) : refine h.congr_deriv ?_ simp only [id_eq] ring - exact deriv_comp_val h + exact deriv_eq_of_hasDerivAt h /-- `σ² (√(Λ/3))² c² = Λ c² / 3` for `σ = ±1` and `0 ≤ Λ`. -/ lemma sq_deSitterRate {σ Λ c : ℝ} (hΛ : 0 ≤ Λ) (hσ : σ = 1 ∨ σ = -1) : @@ -233,7 +233,7 @@ lemma deriv_powerLaw {t₀ : Time} (ht₀ : t₀.val ≠ 0) (n : ℝ) {t : Time} refine h.congr_deriv ?_ simp only [id_eq] ring - exact deriv_comp_val h + exact deriv_eq_of_hasDerivAt h /-- `∂ₜ ∂ₜ (t / t₀) ^ n = n (n - 1) / t₀² (t / t₀) ^ (n - 2)` for `0 < t.val`. The first derivative is only known away from `t.val = 0`, which is enough since `0 < t.val` is an open @@ -441,12 +441,12 @@ noncomputable def milneScaleFactor (c : ℝ) : Time → ℝ := lemma deriv_milneScaleFactor (c : ℝ) : ∂ₜ (milneScaleFactor c) = fun _ => c := by funext t - exact deriv_comp_val (((hasDerivAt_id t.val).const_mul c).congr_deriv (mul_one c)) + exact deriv_eq_of_hasDerivAt (((hasDerivAt_id t.val).const_mul c).congr_deriv (mul_one c)) lemma deriv_deriv_milneScaleFactor (c : ℝ) : ∂ₜ (∂ₜ (milneScaleFactor c)) = fun _ => 0 := by rw [deriv_milneScaleFactor] funext t - exact deriv_comp_val (γ := fun _ => c) (hasDerivAt_const t.val c) + exact deriv_eq_of_hasDerivAt (f := fun _ => c) (hasDerivAt_const t.val c) /-- The Milne solution solves the first-order Friedmann equation with `ρ = 0`, `k = -1` and `Λ = 0`, for `t > 0`. -/ diff --git a/Physlib/SpaceAndTime/Time/Derivatives.lean b/Physlib/SpaceAndTime/Time/Derivatives.lean index 872bb1af6d..0463d86fdb 100644 --- a/Physlib/SpaceAndTime/Time/Derivatives.lean +++ b/Physlib/SpaceAndTime/Time/Derivatives.lean @@ -28,6 +28,8 @@ In this module we define and prove basic lemmas about derivatives of functions o reparametrised through the canonical equivalence `toRealCLE.symm : ℝ ≃L[ℝ] Time`. - `deriv_comp_toRealCLE_of_hasDerivAt` : Its converse, a `HasDerivAt` on `ℝ` read as the time derivative of the curve pulled back to `Time` through `toRealCLE`. +- `hasDerivAt_mk_of_differentiableAt` and `deriv_eq_of_hasDerivAt` : The same two bridges for a + real-valued curve `f : Time → ℝ`, stated at `t : Time` through the curve `τ ↦ f ⟨τ⟩` on `ℝ`. - `deriv_comp_neg` and `deriv_deriv_comp_neg` : The first and second time derivatives under the reversal of time `t ↦ -t`. @@ -115,23 +117,18 @@ lemma deriv_comp_toRealCLE_of_hasDerivAt [NormedAddCommGroup M] [NormedSpace ℝ fderiv_eq_smul_deriv, h.deriv] exact Eq.trans (by rfl) (Time.one_val ▸ one_smul _ v) -/-- The time derivative of `t ↦ γ t.val` at `t` is the derivative of `γ` at `t.val`. -/ -lemma deriv_comp_val {γ : ℝ → ℝ} {t : Time} {v : ℝ} (h : HasDerivAt γ v t.val) : - ∂ₜ (fun s : Time => γ s.val) t = v := - deriv_comp_toRealCLE_of_hasDerivAt γ t v h - /-- The time derivative of any `f : Time → ℝ` at `t` is the derivative at `t.val` of the curve `τ ↦ f ⟨τ⟩` on `ℝ`. -/ lemma deriv_eq_of_hasDerivAt {f : Time → ℝ} {t : Time} {v : ℝ} (h : HasDerivAt (fun τ : ℝ => f ⟨τ⟩) v t.val) : ∂ₜ f t = v := deriv_comp_toRealCLE_of_hasDerivAt (fun τ : ℝ => f ⟨τ⟩) t v h -/-- A curve `f : Time → ℝ` differentiable at `⟨τ⟩` gives the curve `σ ↦ f ⟨σ⟩` on `ℝ`, - whose Mathlib derivative at `τ` is the time derivative `∂ₜ f ⟨τ⟩`. -/ -lemma hasDerivAt_mk_of_differentiableAt {f : Time → ℝ} {τ : ℝ} - (hf : DifferentiableAt ℝ f ⟨τ⟩) : - HasDerivAt (fun σ : ℝ => f ⟨σ⟩) (∂ₜ f ⟨τ⟩) τ := - hasDerivAt_comp_toRealCLE_symm f τ hf +/-- A curve `f : Time → ℝ` differentiable at `t` gives the curve `σ ↦ f ⟨σ⟩` on `ℝ`, + whose Mathlib derivative at `t.val` is the time derivative `∂ₜ f t`. -/ +lemma hasDerivAt_mk_of_differentiableAt {f : Time → ℝ} {t : Time} + (hf : DifferentiableAt ℝ f t) : + HasDerivAt (fun σ : ℝ => f ⟨σ⟩) (∂ₜ f t) t.val := + hasDerivAt_comp_toRealCLE_symm f t.val hf /-! From 0235ed41afba8a2804b8483210994c3a0856688b Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 17 Sep 2026 11:08:30 +0200 Subject: [PATCH 19/20] doc(Cosmology/FLRW): TODOs for the Bianchi identity and the fluid energy equation, API map Review of #1635 by doxtor6. The non-independence TODO is narrowed rather than deleted (derive it from the contracted Bianchi identity once the FLRW metric exists), and a TODO records the bridge to fluid dynamics: ContinuityEquation is the fluid energy equation for the Hubble flow, which needs an energy equation in Physlib.FluidDynamics first. The FLRW TODO of Basic.lean and the overview of MatterContent.lean record the design point that the two Friedmann equations are the primitive pair (where the scale factor is stationary, the first-order and continuity equations leave the pressure unconstrained). API-map.yaml: the continuity-equation requirement is split from the equation of state and marked done. Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/API-map.yaml | 32 +++++++++++++++-------- Physlib/Cosmology/FLRW/Basic.lean | 6 ++++- Physlib/Cosmology/FLRW/MatterContent.lean | 19 ++++++++++++-- 3 files changed, 43 insertions(+), 14 deletions(-) diff --git a/Physlib/Cosmology/FLRW/API-map.yaml b/Physlib/Cosmology/FLRW/API-map.yaml index 324fd49aea..84df1de327 100644 --- a/Physlib/Cosmology/FLRW/API-map.yaml +++ b/Physlib/Cosmology/FLRW/API-map.yaml @@ -19,15 +19,16 @@ Overview: | scale factor, the Hubble parameter, and the deceleration parameter with the relation ∂ₜ H = -H^2 (1 + q). The FLRW type itself is a placeholder; the file records a TODO to replace it with a structure bundling a positive scale - factor and a spatial geometry. Six further modules, ConformalTime.lean, - DensityParameters.lean, Distances.lean, Dynamics.lean, MatterContent.lean and - Solutions.lean, contain only TODO items: conformal time and the conformal - Hubble factor, the critical density and density parameters, cosmological - distances and redshift, energy conditions and the Big-Bang singularity, the - matter content with its continuity equation and scaling laws, and the exact - de Sitter, radiation-dominated, Einstein-de Sitter, Milne and Einstein static - solutions. The requirements below record the two most basic of those open - items. Cosmology/Basic.lean is a placeholder module doc with no declarations. + factor and a spatial geometry. MatterContent.lean contains the continuity + equation of the cosmic fluid and its relation to the two Friedmann equations, + the equation of state and the scaling laws being TODO items there. + Solutions.lean contains the exact de Sitter, radiation-dominated, Einstein-de + Sitter, Milne and Einstein static solutions. Four further modules, + ConformalTime.lean, DensityParameters.lean, Distances.lean and Dynamics.lean, + contain only TODO items: conformal time and the conformal Hubble factor, the + critical density and density parameters, cosmological distances and redshift, + energy conditions and the Big-Bang singularity. Cosmology/Basic.lean is a + placeholder module doc with no declarations. ParentAPIs: - Time (Physlib/SpaceAndTime/Time) @@ -89,8 +90,17 @@ Requirements: location: "Physlib/Cosmology/FLRW/Basic.lean (decelerationParameter, deriv_hubbleConstant, decelerationParameter_eq_one_plus_hubbleConstant, deriv_hubbleConstant_eq_neg_sq_mul, deriv_hubbleConstant_neg_iff, exists_deriv_hubbleConstant_neg_iff)" - description: > - The continuity equation ∂ₜ ρ + 3 H (ρ + P/c^2) = 0 of the cosmic fluid, the - barotropic equation of state P = w ρ c^2, and the density scaling law + The continuity equation ∂ₜ ρ + 3 H (ρ + P/c^2) = 0 of the cosmic fluid is + defined as a proposition at an instant, and the API relates it to the two + Friedmann equations: it follows from the first-order equation holding at all + times together with the second-order equation, and conversely the + second-order equation follows from the first-order equation and the + continuity equation wherever ∂ₜ a ≠ 0. + done: true + location: "Physlib/Cosmology/FLRW/MatterContent.lean (ContinuityEquation, deriv_firstOrderFriedmann, continuityEquation_of_friedmann, secondOrderFriedmann_of_continuityEquation)" + + - description: > + The barotropic equation of state P = w ρ c^2, and the density scaling law ρ ∝ a^(-3(1+w)) with its dust, radiation and vacuum-energy special cases. Recorded as TODO items in Physlib/Cosmology/FLRW/MatterContent.lean; no declarations exist yet. diff --git a/Physlib/Cosmology/FLRW/Basic.lean b/Physlib/Cosmology/FLRW/Basic.lean index 94baa13f9d..aa20617181 100644 --- a/Physlib/Cosmology/FLRW/Basic.lean +++ b/Physlib/Cosmology/FLRW/Basic.lean @@ -103,7 +103,11 @@ def FLRW : Type := sorry TODO "Replace the placeholder `FLRW` type with a concrete structure bundling a positive scale factor `a : Time → ℝ` (smooth, or at least twice differentiable) together with an - element of `SpatialGeometry`." + element of `SpatialGeometry`. If the structure also bundles the dynamics, it should carry the + first- and second-order Friedmann equations as fields and obtain the continuity equation as a + lemma through `FriedmannEquation.continuityEquation_of_friedmann`, never the other way round: + where `∂ₜ a = 0` the first-order and continuity equations leave the pressure unconstrained, + whereas the second-order equation fixes `ρ + 3 p / c²` (the Einstein static universe)." namespace FLRW diff --git a/Physlib/Cosmology/FLRW/MatterContent.lean b/Physlib/Cosmology/FLRW/MatterContent.lean index 52c5204ff6..d10748e5f9 100644 --- a/Physlib/Cosmology/FLRW/MatterContent.lean +++ b/Physlib/Cosmology/FLRW/MatterContent.lean @@ -19,8 +19,12 @@ relation to the two Friedmann equations of `Physlib.Cosmology.FLRW.Basic`: the c equation follows from the first-order equation (holding at all times) and the second-order equation, and conversely the second-order equation follows from the first-order equation and the continuity equation whenever `∂ₜ a ≠ 0`. The three equations are therefore not -independent. The equation of state, the density scaling laws and the perfect-fluid -stress-energy tensor are still TODO items. +independent, but not symmetrically so: where `∂ₜ a = 0` the first-order and the continuity +equations leave `p` unconstrained, while the second-order equation still fixes +`ρ + 3 p / c²` (the Einstein static universe of `Physlib.Cosmology.FLRW.Solutions`). The two +Friedmann equations are the primitive pair, and the continuity equation is derived from them. +The equation of state, the density scaling laws and the perfect-fluid stress-energy tensor +are still TODO items. Time derivatives of curves `Time → ℝ` are computed through the bridge `Time.hasDerivAt_mk_of_differentiableAt` to Mathlib's `HasDerivAt` on `ℝ`. @@ -155,6 +159,10 @@ lemma secondOrderFriedmann_of_continuityEquation {a ρ p : Time → ℝ} {k Λ G TODO "Define the perfect-fluid stress-energy tensor `T_{μν} = (ρ + P/c²) u_μ u_ν + P g_{μν}` for the FLRW metric." +TODO "Derive the non-independence of the two Friedmann equations and the continuity equation + (`continuityEquation_of_friedmann`, `secondOrderFriedmann_of_continuityEquation`) from the + contracted Bianchi identity `∇_ν Gᵘᵛ = 0`, once the FLRW metric is defined." + TODO "Define the linear (barotropic) equation of state `P = w ρ c²` and prove the density scaling law `ρ = ρ₀ a^(−3(1+w))` for constant `w`." @@ -164,4 +172,11 @@ TODO "Specialize the density scaling law to dust (`w = 0`, `ρ ∝ a⁻³`), rad TODO "Prove that the cosmological constant acts as a `w = −1` perfect fluid with `ρ_Λ = Λ c² / (8 π G)` and `P_Λ = −ρ_Λ c²`." +TODO "Relate `ContinuityEquation` to fluid dynamics: for the Hubble flow `u = H x` on `Space 3` + with homogeneous `ρ` and `p`, one has `∇ ⬝ u = 3 H` and `∇ ⬝ (ρ u) = 3 H ρ`, so that + `ContinuityEquation a ρ p c` is the fluid energy equation + `∂ₜ ρ + ∇ ⬝ (ρ u) + (p / c²) ∇ ⬝ u = 0` (Newtonian cosmology with pressure). This needs an + energy equation in `Physlib.FluidDynamics` first, which currently has only the mass equation + `FluidFlow.ClassicalContinuityEquation`, without the pressure work term." + end Cosmology.FLRW.FriedmannEquation From c68ff5e5ff6e4a1b1e9155686936a9f35a0b163a Mon Sep 17 00:00:00 2001 From: Philippe Kevorkian Date: Thu, 17 Sep 2026 11:40:53 +0200 Subject: [PATCH 20/20] refactor(Cosmology/FLRW): inline the one-off HasDerivAt helper of density_scaling, API map Follows the review of #1635: no statement of the API exposes the constructor form of a time any more. hasDerivAt_mul_rpow_of_continuityEquation, a helper stated on the real curve obtained through the time chart and used once, is inlined into density_scaling. API-map.yaml: the equation-of-state requirement is marked done and the cosmological constant as a fluid is recorded. Co-authored-by: Claude Fable 5.1 --- Physlib/Cosmology/FLRW/API-map.yaml | 37 ++++++++++++++--------- Physlib/Cosmology/FLRW/MatterContent.lean | 33 +++++++++----------- 2 files changed, 37 insertions(+), 33 deletions(-) diff --git a/Physlib/Cosmology/FLRW/API-map.yaml b/Physlib/Cosmology/FLRW/API-map.yaml index 84df1de327..59c5a3f631 100644 --- a/Physlib/Cosmology/FLRW/API-map.yaml +++ b/Physlib/Cosmology/FLRW/API-map.yaml @@ -21,14 +21,15 @@ Overview: | records a TODO to replace it with a structure bundling a positive scale factor and a spatial geometry. MatterContent.lean contains the continuity equation of the cosmic fluid and its relation to the two Friedmann equations, - the equation of state and the scaling laws being TODO items there. - Solutions.lean contains the exact de Sitter, radiation-dominated, Einstein-de - Sitter, Milne and Einstein static solutions. Four further modules, - ConformalTime.lean, DensityParameters.lean, Distances.lean and Dynamics.lean, - contain only TODO items: conformal time and the conformal Hubble factor, the - critical density and density parameters, cosmological distances and redshift, - energy conditions and the Big-Bang singularity. Cosmology/Basic.lean is a - placeholder module doc with no declarations. + the barotropic equation of state with the density scaling laws, and the + cosmological constant as a fluid. Solutions.lean contains the exact de + Sitter, radiation-dominated, Einstein-de Sitter, Milne and Einstein static + solutions. Four further modules, ConformalTime.lean, DensityParameters.lean, + Distances.lean and Dynamics.lean, contain only TODO items: conformal time and + the conformal Hubble factor, the critical density and density parameters, + cosmological distances and redshift, energy conditions and the Big-Bang + singularity. Cosmology/Basic.lean is a placeholder module doc with no + declarations. ParentAPIs: - Time (Physlib/SpaceAndTime/Time) @@ -100,9 +101,17 @@ Requirements: location: "Physlib/Cosmology/FLRW/MatterContent.lean (ContinuityEquation, deriv_firstOrderFriedmann, continuityEquation_of_friedmann, secondOrderFriedmann_of_continuityEquation)" - description: > - The barotropic equation of state P = w ρ c^2, and the density scaling law - ρ ∝ a^(-3(1+w)) with its dust, radiation and vacuum-energy special cases. - Recorded as TODO items in Physlib/Cosmology/FLRW/MatterContent.lean; no - declarations exist yet. - done: false - location: "N/A" + The barotropic equation of state P = w ρ c^2 is defined, and the API + contains the density scaling law ρ t = ρ t₀ (a t / a t₀)^(-3(1+w)) under the + barotropic continuity equation holding at all times, its converse, and its + dust, radiation and vacuum-energy special cases. + done: true + location: "Physlib/Cosmology/FLRW/MatterContent.lean (barotropicPressure, deriv_of_continuityEquation_barotropic, density_scaling, continuityEquation_of_scaling, density_scaling_dust, density_scaling_radiation, density_scaling_vacuum)" + + - description: > + The cosmological constant as a fluid: the density ρ_Λ = Λ c^2 / (8πG) and + the pressure p_Λ = -ρ_Λ c^2 are defined, each Friedmann equation with Λ is + equivalent to the same equation without Λ for the fluid ρ + ρ_Λ, p + p_Λ, + and p_Λ is the w = -1 barotropic pressure of ρ_Λ. + done: true + location: "Physlib/Cosmology/FLRW/MatterContent.lean (cosmologicalConstantDensity, cosmologicalConstantPressure, firstOrderFriedmann_iff_lambdaFluid, secondOrderFriedmann_iff_lambdaFluid, cosmologicalConstantPressure_eq_barotropic)" diff --git a/Physlib/Cosmology/FLRW/MatterContent.lean b/Physlib/Cosmology/FLRW/MatterContent.lean index 891b034126..7dc66d3857 100644 --- a/Physlib/Cosmology/FLRW/MatterContent.lean +++ b/Physlib/Cosmology/FLRW/MatterContent.lean @@ -199,30 +199,25 @@ lemma deriv_of_continuityEquation_barotropic {a ρ : Time → ℝ} {w c : ℝ} { -/ -/-- Under the barotropic continuity equation at all times, the curve `σ ↦ ρ ⟨σ⟩ a ⟨σ⟩^(3(1+w))` - has zero derivative. -/ -lemma hasDerivAt_mul_rpow_of_continuityEquation {a ρ : Time → ℝ} {w c : ℝ} (hc : c ≠ 0) - (hd1 : Differentiable ℝ a) (hdρ : Differentiable ℝ ρ) (hapos : ∀ s, 0 < a s) - (hC : ∀ s, ContinuityEquation a ρ (barotropicPressure w ρ c) c s) (τ : ℝ) : - HasDerivAt (fun σ : ℝ => ρ ⟨σ⟩ * a ⟨σ⟩ ^ (3 * (1 + w))) 0 τ := by - have hA := hasDerivAt_mk_of_differentiableAt (hd1 ⟨τ⟩) - have hR := hasDerivAt_mk_of_differentiableAt (hdρ ⟨τ⟩) - have hP := hA.rpow_const (p := 3 * (1 + w)) (Or.inl (hapos ⟨τ⟩).ne') - refine (hR.mul hP).congr_deriv ?_ - rw [deriv_of_continuityEquation_barotropic hc (hC ⟨τ⟩), Real.rpow_sub_one (hapos ⟨τ⟩).ne'] - unfold hubbleConstant - field_simp - ring - /-- The density scaling law: under the barotropic continuity equation at all times, with `a` - and `ρ` differentiable and `a > 0`, `ρ t = ρ t₀ (a t / a t₀)^(-3(1+w))`. -/ + and `ρ` differentiable and `a > 0`, `ρ t = ρ t₀ (a t / a t₀)^(-3(1+w))`. The proof shows that + `ρ a^(3(1+w))` has zero derivative along the time chart. -/ lemma density_scaling {a ρ : Time → ℝ} {w c : ℝ} (hc : c ≠ 0) (hd1 : Differentiable ℝ a) (hdρ : Differentiable ℝ ρ) (hapos : ∀ s, 0 < a s) (hC : ∀ s, ContinuityEquation a ρ (barotropicPressure w ρ c) c s) (t t₀ : Time) : ρ t = ρ t₀ * (a t / a t₀) ^ (-(3 * (1 + w))) := by - have hconst := is_const_of_deriv_eq_zero - (fun τ => (hasDerivAt_mul_rpow_of_continuityEquation hc hd1 hdρ hapos hC τ).differentiableAt) - (fun τ => (hasDerivAt_mul_rpow_of_continuityEquation hc hd1 hdρ hapos hC τ).deriv) + have hderiv : ∀ τ : ℝ, HasDerivAt (fun σ : ℝ => ρ ⟨σ⟩ * a ⟨σ⟩ ^ (3 * (1 + w))) 0 τ := by + intro τ + have hA := hasDerivAt_mk_of_differentiableAt (hd1 ⟨τ⟩) + have hR := hasDerivAt_mk_of_differentiableAt (hdρ ⟨τ⟩) + have hP := hA.rpow_const (p := 3 * (1 + w)) (Or.inl (hapos ⟨τ⟩).ne') + refine (hR.mul hP).congr_deriv ?_ + rw [deriv_of_continuityEquation_barotropic hc (hC ⟨τ⟩), Real.rpow_sub_one (hapos ⟨τ⟩).ne'] + unfold hubbleConstant + field_simp + ring + have hconst := is_const_of_deriv_eq_zero (fun τ => (hderiv τ).differentiableAt) + (fun τ => (hderiv τ).deriv) obtain ⟨τ⟩ := t obtain ⟨τ₀⟩ := t₀ have h := hconst τ τ₀