IndisputableMonolith.Relativity.Cosmology.FRWMetric

   1import Mathlib
   2import IndisputableMonolith.Relativity.Geometry
   3import IndisputableMonolith.Relativity.Calculus
   4
   5namespace IndisputableMonolith
   6namespace Relativity
   7namespace Cosmology
   8
   9open Geometry
  10open Calculus
  11
  12structure ScaleFactor where
  13  a : ℝ → ℝ
  14  a_positive : ∀ t, 0 < a t
  15
  16noncomputable def metric_FRW (scale : ScaleFactor) : MetricTensor where
  17  g := fun x _ low =>
  18    let μ := low 0
  19    let ν := low 1
  20    let t := x 0
  21    if μ = 0 ∧ ν = 0 then -1
  22    else if μ = ν ∧ μ.val > 0 then (scale.a t)^2
  23    else 0
  24  symmetric := by
  25    intro x μ ν
  26    simp only []
  27    -- Case analysis on the if-then-else structure
  28    by_cases h1 : μ = 0 ∧ ν = 0
  29    · by_cases h2 : ν = 0 ∧ μ = 0
  30      · rfl
  31      · simp [h1, h2]
  32    · by_cases h2 : μ = ν ∧ μ.val > 0
  33      · by_cases h3 : ν = μ ∧ ν.val > 0
  34        · rfl
  35        · cases h2; cases h3; simp_all
  36      · by_cases h3 : ν = μ ∧ ν.val > 0
  37        · cases h2; cases h3; simp_all
  38        · rfl
  39
  40noncomputable def christoffel_FRW (scale : ScaleFactor) (t : ℝ) (μ ρ σ : Fin 4) : ℝ :=
  41  let H := deriv scale.a t / scale.a t
  42  if μ = 0 ∧ ρ.val > 0 ∧ σ.val > 0 ∧ ρ = σ then
  43    H * (scale.a t)^2
  44  else if μ.val > 0 ∧ ρ = 0 ∧ σ = μ then H
  45  else if μ.val > 0 ∧ ρ = μ ∧ σ = 0 then H
  46  else 0
  47
  48/-!
  49Christoffel symbols for FRW (documentation / TODO).
  50
  51Intended claim: `christoffel_FRW` matches the standard FRW Christoffel symbols.
  52-/
  53
  54noncomputable def ricci_FRW_00 (scale : ScaleFactor) (t : ℝ) : ℝ :=
  55  -3 * deriv (deriv scale.a) t / scale.a t
  56
  57noncomputable def ricci_FRW_ij (scale : ScaleFactor) (t : ℝ) : ℝ :=
  58  let H := deriv scale.a t / scale.a t
  59  let a_ddot := deriv (deriv scale.a) t
  60  (scale.a t)^2 * (a_ddot / scale.a t + 2 * H^2)
  61
  62/-!
  63Ricci tensor formulas for FRW (documentation / TODO).
  64
  65Intended claim: `ricci_FRW_00` and `ricci_FRW_ij` match the standard FRW Ricci components.
  66-/
  67
  68end Cosmology
  69end Relativity
  70end IndisputableMonolith
  71