inverse_minkowski_apply

formal source

  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