scalar_flat

formal source

  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
  72
  73/-- Einstein tensor vanishes for flat spacetime. -/
  74theorem einstein_flat (mu nu : Idx) :
  75    einstein_tensor minkowski minkowski_inverse
  76      (fun _ _ _ => 0) (fun _ _ _ _ => 0) mu nu = 0 := by
  77  simp [einstein_tensor, ricci_flat, scalar_flat]
  78
  79/-- Einstein tensor is symmetric when the Ricci tensor is symmetric
  80    (which holds when the connection is torsion-free). -/
  81theorem einstein_symmetric
  82    (met : MetricTensor) (ginv : InverseMetric)
  83    (gamma : Idx → Idx → Idx → ℝ)
  84    (dgamma : Idx → Idx → Idx → Idx → ℝ)
  85    (h_ricci_sym : ∀ mu nu, ricci_tensor gamma dgamma mu nu =
  86                            ricci_tensor gamma dgamma nu mu)
  87    (mu nu : Idx) :