The Friedmann-Lemaître-Robertson-Walker metric

Parts of this file is currently informal or semiformal.

inductive Cosmology.SpatialGeometry : Type

The inductive type with three constructors:

• Spherical (k : ℝ)
• Flat
• Saddle (k : ℝ)

• Spherical (k : ℝ) (h : k < 0) : SpatialGeometry
• Flat : SpatialGeometry
• Saddle (k : ℝ) (h : k > 0) : SpatialGeometry

noncomputable def Cosmology.SpatialGeometry.S (s : SpatialGeometry) : ℝ → ℝ

For s corresponding to

• Spherical k, S s r = k * sin (r / k)
• Flat, S s r = r,
• Saddle k, S s r = k * sinh (r / k).

Equations

• (Cosmology.SpatialGeometry.Spherical k h).S r = k * Real.sin (r / k)
• Cosmology.SpatialGeometry.Flat.S r = r
• (Cosmology.SpatialGeometry.Saddle k h).S r = k * Real.sinh (r / k)

theorem Cosmology.SpatialGeometry.mul_sinh_as_div (r k : ℝ) : k * Real.sinh (r / k) = Real.sinh (r / k) / (1 / k)

The limit of S (Saddle k) r as k → ∞ is equal to S (Flat) r. First show that k * sinh(r / k) = sinh(r / k) / (1 / k) pointwise.

theorem Cosmology.SpatialGeometry.tendsto_sinh_rx_over_x (r : ℝ) : Filter.Tendsto (fun (x : ℝ) => Real.sinh (r * x) / x) (nhdsWithin 0 {0}ᶜ) (nhds r)

First, show that limit of sinh(r * x) / x is r at the limit x goes to zero. Then the next theorem will address the rewrite using Filter.Tendsto.comp

theorem Cosmology.SpatialGeometry.limit_S_saddle (r : ℝ) : Filter.Tendsto (fun (k : ℝ) => k * Real.sinh (r / k)) Filter.atTop (nhds r)

theorem Cosmology.SpatialGeometry.mul_sin_as_div (r k : ℝ) : k * Real.sin (r / k) = Real.sin (r / k) / (1 / k)

The limit of S (Sphere k) r as k → ∞ is equal to S (Flat) r. First show that k * sinh(r / k) = sin(r / k) / (1 / k) pointwise.

theorem Cosmology.SpatialGeometry.tendsto_sin_rx_over_x (r : ℝ) : Filter.Tendsto (fun (x : ℝ) => Real.sin (r * x) / x) (nhdsWithin 0 {0}ᶜ) (nhds r)

First, show that limit of sin(r * x) / x is r at the limit x goes to zero. Then the next theorem will address the rewrite using Filter.Tendsto.comp

theorem Cosmology.SpatialGeometry.limit_S_sphere (r : ℝ) : Filter.Tendsto (fun (k : ℝ) => k * Real.sin (r / k)) Filter.atTop (nhds r)

def Cosmology.FLRW : Type

The structure FLRW is defined to contain the physical parameters of the Friedmann-Lemaître-Robertson-Walker metric. That is, it contains

• The scale factor a(t)
• An element of SpatialGeometry.

Semiformal implementation note: It is possible that we should restrict a(t) to be smooth or at least twice differentiable.

Equations

• Cosmology.FLRW = sorry

def Cosmology.FLRW.FriedmannEquation.FirstOrderFriedmann (a ρ : ℝ → ℝ) (k Λ G c t : ℝ) : Prop

The first-order Friedmann equation.

• a : ℝ → ℝ is the FLRW scale factor as a function of cosmic time t.
• ρ : ℝ → ℝ is the total energy density as a function of cosmic time t.
• k : ℝ is the spatial curvature parameter.
• Λ : ℝ is the cosmological constant.
• G : ℝ is Newton's constant.
• c : ℝ is the speed of light. It may be set to 1 for convenience.

Note: We will leave c explicit for generality and accounting purposes.

At time t the equation reads: (a'(t) / a(t))^2 = (8πG/3) ρ(t) − k c^2 / a(t)^2 + Λ c^2 / 3.

Equations

• Cosmology.FLRW.FriedmannEquation.FirstOrderFriedmann a ρ k Λ G c t = ((deriv a t / a t) ^ 2 = 8 * Real.pi * G / 3 * ρ t - k * c ^ 2 / a t ^ 2 + Λ * c ^ 2 / 3)

def Cosmology.FLRW.FriedmannEquation.SecondOrderFriedmann (a ρ p : ℝ → ℝ) (Λ G c t : ℝ) : Prop

The second-order Friedmann equation. Note: Other sources may call this the Raychaudhuri equation. We choose not to use that terminology to avoid the Raychaudhuri equation related to describing congruences of geodesics in general relativity.

• a : ℝ → ℝ is the FLRW scale factor as a function of cosmic time t.
• ρ : ℝ → ℝ is the total energy density as a function of cosmic time t.
• p : ℝ → ℝ is the pressure. It is related to ρ via p = w * ρ
• w is the equation of state. We will introduce this later.
• Λ : ℝ is the cosmological constant.
• G : ℝ is Newton's constant.
• c : ℝ is the speed of light. It may be set to 1 for convenience.

Note: We will leave c explicit for generality and accounting purposes.

At time t the equation reads: (a''(t) / a (t)) = - (4πG/3) * (ρ(t) + 3 * p(t) / c^2) + Λ * c^2 / 3.

Equations

• Cosmology.FLRW.FriedmannEquation.SecondOrderFriedmann a ρ p Λ G c t = (deriv (deriv a) t / a t = -(4 * Real.pi * G / 3) * (ρ t + 3 * p t / c ^ 2) + Λ * c ^ 2 / 3)

noncomputable def Cosmology.FLRW.FriedmannEquation.hubbleConstant (a : ℝ → ℝ) (t : ℝ) : ℝ

The hubble constant defined in terms of the scale factor as (dₜ a) / a.

The notation H is used for the hubbleConstant.

Semiformal implementation note: Implement also scoped notation.

Equations

• Cosmology.FLRW.FriedmannEquation.hubbleConstant a t = deriv a t / a t

noncomputable def Cosmology.FLRW.FriedmannEquation.decelerationParameter (a : ℝ → ℝ) (t : ℝ) : ℝ

The deceleration parameter defined in terms of the scale factor as - (dₜdₜ a) a / (dₜ a)^2.

The notation q is used for the decelerationParameter.

Semiformal implementation note: Implement also scoped notation.

Equations

• Cosmology.FLRW.FriedmannEquation.decelerationParameter a t = -(deriv (deriv a) t * a t) / deriv a t ^ 2

def Cosmology.FLRW.FriedmannEquation.decelerationParameter_eq_one_plus_hubbleConstant : InformalLemma

The deceleration parameter is equal to - (1 + (dₜ H)/H^2).

Equations

• Cosmology.FLRW.FriedmannEquation.decelerationParameter_eq_one_plus_hubbleConstant = { deps := [], tag := "6Z23H" }

def Cosmology.FLRW.FriedmannEquation.time_evolution_hubbleConstant : InformalLemma

The time evolution of the hubble parameter is equal to dₜ H = - H^2 (1 + q).

Equations

• Cosmology.FLRW.FriedmannEquation.time_evolution_hubbleConstant = { deps := [], tag := "6Z3BS" }

def Cosmology.FLRW.FriedmannEquation.hubbleConstant_decrease_iff : InformalLemma

There exists a time at which the hubble constant decreases if and only if there exists a time where the deceleration parameter is less then -1.

Equations

• Cosmology.FLRW.FriedmannEquation.hubbleConstant_decrease_iff = { deps := [], tag := "6Z3FS" }