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)

def Cosmology.SpatialGeometry.limit_S_sphere : InformalLemma

The limit of S (Sphere k) r as k → ∞ is equal to S (Flat) r.

Equations

• Cosmology.SpatialGeometry.limit_S_sphere = { deps := [], tag := "62A4R" }

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.hubbleConstant : InformalDefinition

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.hubbleConstant = { deps := [], tag := "6Z2NB" }

def Cosmology.FLRW.decelerationParameter : InformalDefinition

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.decelerationParameter = { deps := [], tag := "6Z2UE" }

def Cosmology.FLRW.decelerationParameter_eq_one_plus_hubbleConstant : InformalLemma

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

Equations

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

def Cosmology.FLRW.time_evolution_hubbleConstant : InformalLemma

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

Equations

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

def Cosmology.FLRW.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.hubbleConstant_decrease_iff = { deps := [], tag := "6Z3FS" }