ricci_tensor

formal source

  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
  69  unfold riemann_tensor
  70  -- Simplify the index functions - the pattern is:
  71  -- LHS: low 0 = σ, low 1 = μ, low 2 = ν
  72  -- RHS: low 0 = σ, low 1 = ν, low 2 = μ
  73  -- The Riemann structure: ∂_{low 1} Γ_{low 2, low 0} - ∂_{low 2} Γ_{low 1, low 0} + quadratic terms
  74  -- Swapping low 1 ↔ low 2 negates the expression
  75  simp only [Fin.val_zero, Fin.val_one, Fin.val_two,
  76             show (0 : ℕ) ≠ 1 from by decide,
  77             show (1 : ℕ) ≠ 0 from by decide,
  78             show (2 : ℕ) ≠ 0 from by decide, show (2 : ℕ) ≠ 1 from by decide,
  79             if_true, if_false]
  80  ring
  81