ChristoffelData

formal source

  63    We represent these as a function of three indices.
  64    The partial derivatives d_mu g_{nu sigma} are provided as input
  65    (they depend on the coordinate system and the point). -/
  66structure ChristoffelData where
  67  gamma : Idx → Idx → Idx → ℝ
  68
  69/-- Construct Christoffel symbols from metric, inverse metric, and metric derivatives.
  70    dg mu nu sigma = d_mu g_{nu sigma} (partial derivative of g_{nu sigma} w.r.t. x^mu). -/
  71noncomputable def christoffel_from_metric
  72    (ginv : InverseMetric) (dg : Idx → Idx → Idx → ℝ) : ChristoffelData where
  73  gamma := fun rho mu nu =>
  74    (1/2) * ∑ sigma : Idx,
  75      ginv.ginv rho sigma * (dg mu nu sigma + dg nu mu sigma - dg sigma mu nu)
  76
  77/-- Christoffel symbols are symmetric in the lower two indices (torsion-free).
  78    This follows from the symmetry of the metric derivatives:
  79    dg mu nu sigma = d_mu g_{nu sigma} is symmetric in (nu, sigma) because
  80    g_{nu sigma} = g_{sigma nu}. -/
  81theorem christoffel_symmetric (ginv : InverseMetric)
  82    (dg : Idx → Idx → Idx → ℝ)
  83    (dg_metric_sym : ∀ mu nu sigma, dg mu nu sigma = dg mu sigma nu) :
  84    ∀ rho mu nu,
  85      (christoffel_from_metric ginv dg).gamma rho mu nu =
  86      (christoffel_from_metric ginv dg).gamma rho nu mu := by
  87  intro rho mu nu
  88  simp only [christoffel_from_metric]
  89  congr 1
  90  apply Finset.sum_congr rfl
  91  intro sigma _
  92  congr 1
  93  rw [dg_metric_sym mu nu sigma, dg_metric_sym nu mu sigma,
  94      dg_metric_sym sigma mu nu, dg_metric_sym sigma nu mu]
  95  ring
  96