einstein_tensor

formal source

 107      inverse_metric g x (fun _ => mu) (fun _ => nu) * ricci_tensor g x (fun _ => 0) (fun i => if i.val = 0 then mu else nu)))
 108
 109/-- **Einstein Tensor** $G_{\mu\nu} = R_{\mu\nu} - \frac{1}{2} g_{\mu\nu} R$. -/
 110noncomputable def einstein_tensor (g : MetricTensor) : BilinearForm :=
 111  fun x up low =>
 112    ricci_tensor g x up low - (1/2 : ℝ) * g.g x up low * ricci_scalar g x
 113
 114/-! The previous `ricci_tensor_symmetric'` wrapper depended on the deleted
 115`ricci_tensor_symmetric` axiom.  Use `RiemannSymmetries.ricci_tensor_symmetric_proof`
 116(which takes the trace-vanishing hypothesis explicitly) or
 117`RiemannSymmetries.curvature_axioms_hold` (bundled). -/
 118
 119/-! ## Minkowski Space Theorems -/
 120
 121/-- The Minkowski metric η doesn't depend on x, so its derivatives vanish. -/
 122lemma eta_deriv_zero (μ ν κ : Fin 4) (x : Fin 4 → ℝ) :
 123    partialDeriv_v2 (fun y => eta y (fun _ => 0) (fun i => if i.val = 0 then μ else ν)) κ x = 0 := by
 124  apply partialDeriv_v2_const (c := eta x (fun _ => 0) (fun i => if i.val = 0 then μ else ν))
 125  intro y; unfold eta; rfl
 126
 127/-- Christoffel symbols vanish for the Minkowski metric. -/
 128theorem minkowski_christoffel_zero_proper (x : Fin 4 → ℝ) (ρ μ ν : Fin 4) :
 129    christoffel minkowski_tensor x ρ μ ν = 0 := by
 130  unfold christoffel minkowski_tensor
 131  dsimp
 132  simp only [eta_deriv_zero, add_zero, sub_zero, mul_zero, Finset.sum_const_zero]
 133
 134/-- Riemann tensor vanishes for Minkowski space. -/
 135theorem minkowski_riemann_zero (x : Fin 4 → ℝ) (up : Fin 1 → Fin 4) (low : Fin 3 → Fin 4) :
 136    riemann_tensor minkowski_tensor x up low = 0 := by
 137  unfold riemann_tensor
 138  have hΓ : ∀ y r m n, christoffel minkowski_tensor y r m n = 0 := by
 139    intro y r m n; exact minkowski_christoffel_zero_proper y r m n
 140  have h_deriv : ∀ f μ x, (∀ y, f y = 0) → partialDeriv_v2 f μ x = 0 := by