vacuum_efe_coord

formal source

  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:
 105    G_{mu nu} + Lambda g_{mu nu} = kappa T_{mu nu} -/
 106def sourced_efe_coord (met : MetricTensor) (ginv : InverseMetric)
 107    (gamma : Idx → Idx → Idx → ℝ)
 108    (dgamma : Idx → Idx → Idx → Idx → ℝ)
 109    (Lambda kappa : ℝ)
 110    (T : Idx → Idx → ℝ) : Prop :=
 111  ∀ mu nu : Idx,
 112    einstein_tensor met ginv gamma dgamma mu nu + Lambda * met.g mu nu =
 113    kappa * T mu nu
 114
 115/-- Flat Minkowski metric satisfies the vacuum EFE with Lambda = 0. -/
 116theorem minkowski_is_vacuum_solution :
 117    vacuum_efe_coord minkowski minkowski_inverse
 118      (fun _ _ _ => 0) (fun _ _ _ _ => 0) 0 := by
 119  intro mu nu
 120  simp [einstein_flat]
 121
 122/-! ## Certificate -/
 123
 124structure RicciCert where
 125  ricci_flat : ∀ mu nu, ricci_tensor (fun _ _ _ => 0) (fun _ _ _ _ => 0) mu nu = 0
 126  scalar_flat : scalar_curvature minkowski_inverse (fun _ _ _ => 0) (fun _ _ _ _ => 0) = 0
 127  einstein_flat : ∀ mu nu, einstein_tensor minkowski minkowski_inverse