diff --git a/Physlib/Cosmology/FLRW/API-map.yaml b/Physlib/Cosmology/FLRW/API-map.yaml index 324fd49ae..59c5a3f63 100644 --- a/Physlib/Cosmology/FLRW/API-map.yaml +++ b/Physlib/Cosmology/FLRW/API-map.yaml @@ -19,15 +19,17 @@ 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 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) @@ -89,10 +91,27 @@ 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 - ρ ∝ 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 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 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/Basic.lean b/Physlib/Cosmology/FLRW/Basic.lean index 94baa13f9..aa2061718 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 2b257245e..7dc66d385 100644 --- a/Physlib/Cosmology/FLRW/MatterContent.lean +++ b/Physlib/Cosmology/FLRW/MatterContent.lean @@ -1,40 +1,356 @@ /- Copyright (c) 2026 Jinzheng Li. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jinzheng Li +Authors: Philippe Kevorkian, Jinzheng Li -/ 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 -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, 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. +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_mk_of_differentiableAt` 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`. +- `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 + +- 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 -/ @[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 + +/-! -TODO "Define the continuity equation `∂ₜ ρ + 3 H (ρ + P/c²) = 0` and derive it from - the first- and second-order Friedmann equations." +## A. The continuity equation + +-/ + +/-! + +### A.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 + +/-! -TODO "Prove that the Friedmann equation, the acceleration equation and the - continuity equation are not independent (a consequence of the Bianchi identity - `∇_ν Gᵘᵛ = 0`)." +### A.2. The derivative of the first-order Friedmann equation + +-/ + +/-- 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 : ℝ} {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ρ + 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 + +/-! + +### A.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 : 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 + have hd := deriv_firstOrderFriedmann ha hd1 hd2 hdρ hF1 + have h1 := hF1 t + unfold FirstOrderFriedmann at h1 + unfold SecondOrderFriedmann at hF2 + unfold ContinuityEquation hubbleConstant + have hG3 : 8 * π * G / 3 ≠ 0 := by positivity + apply mul_left_cancel₀ hG3 + linear_combination -hd + 2 * (∂ₜ a t / a t) * hF2 - 2 * (∂ₜ a t / a t) * h1 + +/-! + +### A.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) (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 + have hd := deriv_firstOrderFriedmann ha hd1 hd2 hdρ hF1 + have h1 := hF1 t + unfold FirstOrderFriedmann at h1 + unfold ContinuityEquation hubbleConstant at hC + unfold SecondOrderFriedmann + 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 t / a t) * h1 + +/-! + +## B. The barotropic equation of state and the density scaling law + +-/ + +/-! + +### B.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 + +/-! + +### B.2. The density scaling law + +-/ + +/-- 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))`. 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 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 τ τ₀ + 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 + +/-! + +### B.3. Dust, radiation and vacuum energy + +-/ + +/-- 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] + +/-! + +## C. 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 + +/-! + +## D. 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`." +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 "Specialize the density scaling law to dust (`w = 0`, `ρ ∝ a⁻³`), radiation - (`w = 1/3`, `ρ ∝ a⁻⁴`) and vacuum energy (`w = −1`, `ρ` constant)." +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." -TODO "Prove that the cosmological constant acts as a `w = −1` perfect fluid with - `ρ_Λ = Λ c² / (8 π G)` and `P_Λ = −ρ_Λ c²`." +end Cosmology.FLRW.FriedmannEquation diff --git a/Physlib/Cosmology/FLRW/Solutions.lean b/Physlib/Cosmology/FLRW/Solutions.lean index d7edead1d..62f98fbe5 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 41e6234c8..0463d86fd 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,17 +117,19 @@ 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 `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 + /-! ### A.3. Derivatives of functions into manifolds