IndisputableMonolith.Relativity.GW.TensorDecomposition

   1import Mathlib
   2import IndisputableMonolith.Relativity.Geometry
   3import IndisputableMonolith.Relativity.Cosmology.FRWMetric
   4
   5namespace IndisputableMonolith
   6namespace Relativity
   7namespace GW
   8
   9open Geometry
  10open Cosmology
  11
  12structure TensorPerturbation where
  13  h_TT : ℝ → (Fin 3 → Fin 3 → ℝ)
  14  transverse : ∀ t i, Finset.sum (Finset.range 3) (fun j =>
  15    if hj : j < 3 then h_TT t i ⟨j, hj⟩ else 0) = 0
  16  traceless : ∀ t, Finset.sum (Finset.range 3) (fun i =>
  17    if hi : i < 3 then h_TT t ⟨i, hi⟩ ⟨i, hi⟩ else 0) = 0
  18
  19/-- Decomposition of a general spatial metric perturbation into TT part and other sectors. -/
  20def decompose_perturbation (h : Fin 3 → Fin 3 → ℝ) : Prop :=
  21  ∃ (tp : TensorPerturbation) (scalar : ℝ) (vector : Fin 3 → ℝ),
  22    h = (fun i j => tp.h_TT 0 i j + (if i = j then scalar else 0) + (vector i + vector j))
  23
  24/-- Existence of a TT projection operator. -/
  25def projection_operator_TT : Prop :=
  26  ∃ P : (Fin 3 → Fin 3 → ℝ) → (Fin 3 → Fin 3 → ℝ),
  27    ∀ h, ∃ tp : TensorPerturbation, P h = tp.h_TT 0
  28
  29/-- Uniqueness of the TT decomposition. -/
  30def decomposition_unique : Prop :=
  31  ∀ tp1 tp2 : TensorPerturbation, tp1.h_TT = tp2.h_TT → tp1 = tp2
  32
  33theorem decomposition_unique_holds : decomposition_unique := by
  34  intro tp1 tp2 h
  35  cases tp1; cases tp2; simp at h; subst h
  36  rfl
  37
  38
  39end GW
  40end Relativity
  41end IndisputableMonolith
  42