ricci_flat

formal source

  38  ∑ rho : Idx, riemann_tensor gamma dgamma rho mu rho nu
  39
  40/-- Ricci tensor vanishes for flat spacetime. -/
  41theorem ricci_flat (mu nu : Idx) :
  42    ricci_tensor (fun _ _ _ => 0) (fun _ _ _ _ => 0) mu nu = 0 := by
  43  simp [ricci_tensor, riemann_flat_vanishes]
  44
  45/-! ## Scalar Curvature -/
  46
  47/-- Scalar curvature: trace of the Ricci tensor with the inverse metric.
  48    R = g^{mu nu} R_{mu nu} = sum_{mu,nu} g^{mu nu} R_{mu nu} -/
  49noncomputable def scalar_curvature
  50    (ginv : InverseMetric)
  51    (gamma : Idx → Idx → Idx → ℝ)
  52    (dgamma : Idx → Idx → Idx → Idx → ℝ) : ℝ :=
  53  ∑ mu : Idx, ∑ nu : Idx,
  54    ginv.ginv mu nu * ricci_tensor gamma dgamma mu nu
  55
  56/-- Scalar curvature vanishes for flat spacetime. -/
  57theorem scalar_flat :
  58    scalar_curvature minkowski_inverse (fun _ _ _ => 0) (fun _ _ _ _ => 0) = 0 := by
  59  simp [scalar_curvature, ricci_flat]
  60
  61/-! ## Einstein Tensor -/
  62
  63/-- The Einstein tensor: G_{mu nu} = R_{mu nu} - (1/2) R g_{mu nu}.
  64    This is the LHS of the Einstein field equations. -/
  65noncomputable def einstein_tensor
  66    (met : MetricTensor) (ginv : InverseMetric)
  67    (gamma : Idx → Idx → Idx → ℝ)
  68    (dgamma : Idx → Idx → Idx → Idx → ℝ)
  69    (mu nu : Idx) : ℝ :=
  70  ricci_tensor gamma dgamma mu nu -
  71  (1/2) * scalar_curvature ginv gamma dgamma * met.g mu nu