IndisputableMonolith.Relativity.Geometry.CovariantDerivative

   1import Mathlib
   2import IndisputableMonolith.Relativity.Geometry.Tensor
   3import IndisputableMonolith.Relativity.Geometry.Curvature
   4import IndisputableMonolith.Relativity.Calculus.Derivatives
   5
   6namespace IndisputableMonolith
   7namespace Relativity
   8namespace Geometry
   9
  10open Calculus
  11
  12/-- **Covariant Derivative** of a (1,2) tensor $T^\lambda_{\mu\nu}$.
  13    $\nabla_\rho T^\lambda_{\mu\nu} = \partial_\rho T^\lambda_{\mu\nu} + \Gamma^\lambda_{\rho\sigma} T^\sigma_{\mu\nu} - \Gamma^\sigma_{\rho\mu} T^\lambda_{\sigma\nu} - \Gamma^\sigma_{\rho\nu} T^\lambda_{\mu\sigma}$. -/
  14noncomputable def cov_deriv_1_2 (g : MetricTensor) (T : (Fin 4 → ℝ) → Fin 4 → Fin 4 → Fin 4 → ℝ)
  15    (x : Fin 4 → ℝ) (rho lambda mu nu : Fin 4) : ℝ :=
  16  let Γ := christoffel g x
  17  partialDeriv_v2 (fun y => T y lambda mu nu) rho x +
  18  Finset.univ.sum (fun sigma => Γ lambda rho sigma * T x sigma mu nu) -
  19  Finset.univ.sum (fun sigma => Γ sigma rho mu * T x lambda sigma nu) -
  20  Finset.univ.sum (fun sigma => Γ sigma rho nu * T x lambda mu sigma)
  21
  22end Geometry
  23end Relativity
  24end IndisputableMonolith
  25