riemann_tensor

formal source

  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
  44    let Γ := christoffel g
  45    (partialDeriv_v2 (fun y => Γ y rho nu sigma) mu x) -
  46    (partialDeriv_v2 (fun y => Γ y rho mu sigma) nu x) +
  47    Finset.univ.sum (fun (lambda : Fin 4) => Γ x rho mu lambda * Γ x lambda nu sigma) -
  48    Finset.univ.sum (fun (lambda : Fin 4) => Γ x rho nu lambda * Γ x lambda mu sigma)
  49
  50/-- **Ricci Tensor** $R_{\mu\nu} = R^{\rho}_{\mu\rho\nu}$. -/
  51noncomputable def ricci_tensor (g : MetricTensor) : BilinearForm :=
  52  fun x _ low =>
  53    let mu := low 0
  54    let nu := low 1
  55    Finset.univ.sum (fun (rho : Fin 4) =>
  56      riemann_tensor g x (fun _ => rho) (fun i => if i.val = 0 then mu else if i.val = 1 then rho else nu))
  57
  58/-- **THEOREM (Riemann Antisymmetry)**: The Riemann tensor is antisymmetric in its last two indices.
  59    R^ρ_{σμν} = -R^ρ_{σνμ}
  60
  61    This follows directly from the definition of the Riemann tensor in terms of
  62    Christoffel symbols. -/
  63theorem riemann_antisymmetric_last_two (g : MetricTensor) (x : Fin 4 → ℝ) (ρ σ μ ν : Fin 4) :
  64    riemann_tensor g x (fun _ => ρ) (fun i => if i.val = 0 then σ else if i.val = 1 then μ else ν) =
  65    -riemann_tensor g x (fun _ => ρ) (fun i => if i.val = 0 then σ else if i.val = 1 then ν else μ) := by
  66  -- The Riemann tensor definition: ∂μ Γ^ρ_νσ - ∂ν Γ^ρ_μσ + Γ^ρ_μλ Γ^λ_νσ - Γ^ρ_νλ Γ^λ_μσ
  67  -- Swapping μ ↔ ν gives: ∂ν Γ^ρ_μσ - ∂μ Γ^ρ_νσ + Γ^ρ_νλ Γ^λ_μσ - Γ^ρ_μλ Γ^λ_νσ
  68  -- Which is exactly the negation of the original