minkowski_tensor

formal source

  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. -/