einstein_flat

formal source

  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:
  96    G_{mu nu} + Lambda g_{mu nu} = 0 -/
  97def vacuum_efe_coord (met : MetricTensor) (ginv : InverseMetric)
  98    (gamma : Idx → Idx → Idx → ℝ)
  99    (dgamma : Idx → Idx → Idx → Idx → ℝ)
 100    (Lambda : ℝ) : Prop :=
 101  ∀ mu nu : Idx,
 102    einstein_tensor met ginv gamma dgamma mu nu + Lambda * met.g mu nu = 0
 103
 104/-- The sourced Einstein field equation: