The Friedmann-Lemaître-Robertson-Walker metric

Everything in this file is currently informal or semiformal.

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