einstein_tensor

formal source

  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) :
  88    einstein_tensor met ginv gamma dgamma mu nu =
  89    einstein_tensor met ginv gamma dgamma nu mu := by
  90  simp only [einstein_tensor]
  91  rw [h_ricci_sym mu nu, met.symmetric mu nu]
  92
  93/-! ## The Einstein Field Equation (Structural Form) -/
  94
  95/-- The vacuum Einstein field equation in coordinates: