The Friedmann-Lemaître-Robertson-Walker metric

Everything in this file is currently informal or semiformal.

def Cosmology.SpatialGeometry : Type

The inductive type with three constructors:

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

Equations

• Cosmology.SpatialGeometry = sorry

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 * sin (r / k).

Semiformal implementation note: There is likely a better name for this function.

Equations

• s.S = sorry

def Cosmology.SpatialGeometry.limit_S_saddle : InformalLemma

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

Equations

• Cosmology.SpatialGeometry.limit_S_saddle = { deps := [], tag := "6ZZ3D" }

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 restirct 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" }