christoffel

formal source

  10open Calculus
  11
  12/-- **Christoffel Symbols** derived from the metric. -/
  13noncomputable def christoffel (g : MetricTensor) : (Fin 4 → ℝ) → Fin 4 → Fin 4 → Fin 4 → ℝ :=
  14  fun x rho mu nu =>
  15    (1/2 : ℝ) * Finset.univ.sum (fun (lambda : Fin 4) =>
  16      (inverse_metric g) x (fun _ => rho) (fun _ => lambda) * (
  17        (partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then mu else lambda)) nu x) +
  18        (partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then nu else lambda)) mu x) -
  19        (partialDeriv_v2 (fun y => g.g y (fun _ => 0) (fun i => if i.val = 0 then mu else nu)) lambda x)
  20      ))
  21
  22/-- Christoffel symbols are symmetric in the lower indices (torsion-free). -/
  23theorem christoffel_symmetric (g : MetricTensor) (x : Fin 4 → ℝ) (rho mu nu : Fin 4) :
  24    christoffel g x rho mu nu = christoffel g x rho nu mu := by
  25  unfold christoffel
  26  congr 1
  27  apply Finset.sum_congr rfl
  28  intro lambda _
  29  ring_nf
  30  -- Symmetry of g indices: ∂_ν g_{μλ} + ∂_μ g_{νλ} - ∂_λ g_{μν} = ∂_μ g_{νλ} + ∂_ν g_{μλ} - ∂_λ g_{νμ}
  31  have h_sym : (fun y => g.g y (fun _ => 0) (fun i : Fin 2 => if i.val = 0 then mu else nu)) =
  32               (fun y => g.g y (fun _ => 0) (fun i : Fin 2 => if i.val = 0 then nu else mu)) := by
  33    funext y
  34    exact g.symmetric y (fun _ => 0) (fun i : Fin 2 => if i.val = 0 then mu else nu)
  35  rw [h_sym]
  36
  37/-- **Riemann Curvature Tensor** $R^{\rho}_{\sigma\mu\nu}$. -/
  38noncomputable def riemann_tensor (g : MetricTensor) : Tensor 1 3 :=
  39  fun x up low =>
  40    let rho := up 0
  41    let sigma := low 0
  42    let mu := low 1
  43    let nu := low 2