IndisputableMonolith.Relativity.Geometry.Metric

   1import Mathlib
   2import IndisputableMonolith.Relativity.Geometry.Tensor
   3import IndisputableMonolith.Relativity.Calculus.Derivatives
   4
   5namespace IndisputableMonolith
   6namespace Relativity
   7namespace Geometry
   8
   9open Calculus
  10
  11structure MetricTensor where
  12  g : BilinearForm
  13  symmetric : ∀ x up low, g x up low = g x up (fun i => if (i : ℕ) = 0 then low 1 else low 0)
  14
  15@[ext]
  16lemma MetricTensor.ext (g1 g2 : MetricTensor) (h : g1.g = g2.g) : g1 = g2 := by
  17  cases g1; cases g2; simp_all
  18
  19noncomputable def eta : BilinearForm := fun _ _ low =>
  20  if low 0 = low 1 then (if (low 0 : ℕ) = 0 then -1 else 1) else 0
  21
  22noncomputable def minkowski_tensor : MetricTensor :=
  23  { g := eta
  24    symmetric := by
  25      intro x up low
  26      unfold eta
  27      dsimp
  28      by_cases h : low 0 = low 1
  29      · have h_rev : low 1 = low 0 := h.symm
  30        rw [if_pos h, if_pos h_rev]
  31        rw [h]
  32      · have h_rev : low 1 ≠ low 0 := fun heq => h heq.symm
  33        rw [if_neg h, if_neg h_rev] }
  34
  35noncomputable def metric_from_rrf (psi : (Fin 4 → ℝ) → ℝ) (k : ℝ) : MetricTensor :=
  36  { g := fun x _ low =>
  37      eta x (fun _ => 0) low + k * psi x * (if low 0 = low 1 then 1 else 0)
  38    symmetric := by
  39      intro x up low
  40      unfold eta
  41      dsimp
  42      by_cases h : low 0 = low 1
  43      · have h_rev : low 1 = low 0 := h.symm
  44        rw [if_pos h, if_pos h, if_pos h_rev, if_pos h_rev]
  45        rw [h]
  46      · have h_rev : low 1 ≠ low 0 := fun heq => h heq.symm
  47        rw [if_neg h, if_neg h, if_neg h_rev, if_neg h_rev] }
  48
  49noncomputable def metric_to_matrix (g : MetricTensor) (x : Fin 4 → ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=
  50  fun i j => g.g x (fun _ => 0) (fun k => if (k : ℕ) = 0 then i else j)
  51
  52/-- The metric matrix is symmetric because the metric tensor is symmetric. -/
  53lemma metric_to_matrix_symmetric (g : MetricTensor) (x : Fin 4 → ℝ) :
  54    (metric_to_matrix g x).transpose = metric_to_matrix g x := by
  55  ext i j
  56  unfold metric_to_matrix Matrix.transpose
  57  dsimp
  58  -- Apply the metric tensor symmetry: g x up low = g x up (swap low)
  59  have h := g.symmetric x (fun _ => 0) (fun k => if (k : ℕ) = 0 then j else i)
  60  -- The RHS evaluates to (fun k => if k.val = 0 then i else j) since 1 ≠ 0 and 0 = 0
  61  simp only [Fin.val_one, Fin.val_zero, one_ne_zero, ite_false, ite_true] at h
  62  exact h
  63
  64noncomputable def metric_det (g : MetricTensor) (x : Fin 4 → ℝ) : ℝ :=
  65  (metric_to_matrix g x).det
  66
  67noncomputable def inverse_metric (g : MetricTensor) : ContravariantBilinear :=
  68  fun x up _ =>
  69    (metric_to_matrix g x)⁻¹ (up 0) (up 1)
  70
  71/-- Inverse Minkowski metric components. -/
  72lemma inverse_minkowski_apply (x : Fin 4 → ℝ) (μ ν : Fin 4) :
  73    inverse_metric minkowski_tensor x (fun i => if (i : ℕ) = 0 then μ else ν) (fun _ => 0) =
  74    if μ = ν then (if (μ : ℕ) = 0 then -1 else 1) else 0 := by
  75  unfold inverse_metric
  76  dsimp
  77  have h_mat : metric_to_matrix minkowski_tensor x = Matrix.diagonal (fun i : Fin 4 => if (i : ℕ) = 0 then (-1 : ℝ) else 1) := by
  78    ext i j
  79    unfold metric_to_matrix minkowski_tensor eta
  80    dsimp
  81    by_cases h : i = j
  82    · rw [if_pos h, h]
  83      simp
  84    · rw [if_neg h]
  85      simp [h]
  86  rw [h_mat]
  87  have h_inv : (Matrix.diagonal (fun i : Fin 4 => if (i : ℕ) = 0 then (-1 : ℝ) else 1))⁻¹ =
  88               Matrix.diagonal (fun i : Fin 4 => if (i : ℕ) = 0 then (-1 : ℝ) else 1) := by
  89    apply Matrix.inv_eq_left_inv
  90    rw [Matrix.diagonal_mul_diagonal]
  91    ext i j
  92    rw [Matrix.one_apply]
  93    unfold Matrix.diagonal
  94    dsimp
  95    by_cases h : i = j
  96    · rw [if_pos h]
  97      split_ifs <;> norm_num
  98    · rw [if_neg h]
  99      simp [h]
 100  rw [h_inv]
 101  unfold Matrix.diagonal
 102  dsimp
 103
 104lemma finset_sum_fin_4 {α : Type*} [AddCommMonoid α] (f : Fin 4 → α) :
 105    Finset.sum Finset.univ f = f 0 + f 1 + f 2 + f 3 := by
 106  have : Finset.univ = ({0, 1, 2, 3} : Finset (Fin 4)) := by decide
 107  rw [this]
 108  simp
 109  abel
 110
 111/-- Squared gradient helper for Minkowski metric. -/
 112lemma gradient_squared_minkowski_sum (grad : Fin 4 → ℝ) (x : Fin 4 → ℝ) :
 113    Finset.sum Finset.univ (fun μ => Finset.sum Finset.univ (fun ν =>
 114      inverse_metric minkowski_tensor x (fun i => if (i : ℕ) = 0 then μ else ν) (fun _ => 0) *
 115      grad μ * grad ν)) =
 116    -(grad 0)^2 + (grad 1)^2 + (grad 2)^2 + (grad 3)^2 := by
 117  rw [finset_sum_fin_4]
 118  simp only [finset_sum_fin_4, inverse_minkowski_apply]
 119  simp
 120  ring
 121
 122end Geometry
 123end Relativity
 124end IndisputableMonolith
 125