eta_deriv_zero

formal source

 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
 141    intro f μ x h; apply partialDeriv_v2_const (c := 0); exact h
 142  simp [hΓ, h_deriv, Finset.sum_const_zero]
 143
 144/-- Ricci tensor vanishes for Minkowski space. -/
 145theorem minkowski_ricci_zero (x : Fin 4 → ℝ) (up : Fin 0 → Fin 4) (low : Fin 2 → Fin 4) :
 146    ricci_tensor minkowski_tensor x up low = 0 := by
 147  unfold ricci_tensor
 148  simp [minkowski_riemann_zero, Finset.sum_const_zero]
 149
 150/-- Ricci scalar vanishes for Minkowski space. -/
 151theorem minkowski_ricci_scalar_zero (x : Fin 4 → ℝ) : ricci_scalar minkowski_tensor x = 0 := by
 152  unfold ricci_scalar