InverseMetric

formal source

  41  symmetric : ∀ mu nu, g mu nu = g nu mu
  42
  43/-- The inverse metric g^{mu nu} (satisfying g^{mu rho} g_{rho nu} = delta^mu_nu). -/
  44structure InverseMetric where
  45  ginv : Idx → Idx → ℝ
  46  symmetric : ∀ mu nu, ginv mu nu = ginv nu mu
  47
  48/-- The flat Minkowski metric eta = diag(-1, +1, +1, +1). -/
  49def minkowski : MetricTensor where
  50  g := fun mu nu => if mu = nu then (if mu = 0 then -1 else 1) else 0
  51  symmetric := by intro mu nu; split_ifs <;> simp_all [eq_comm]
  52
  53/-- The Minkowski inverse equals the Minkowski metric itself. -/
  54def minkowski_inverse : InverseMetric where
  55  ginv := fun mu nu => if mu = nu then (if mu = 0 then -1 else 1) else 0
  56  symmetric := by intro mu nu; split_ifs <;> simp_all [eq_comm]
  57
  58/-! ## Christoffel Symbols -/
  59
  60/-- The Christoffel symbols of the second kind in local coordinates.
  61    Gamma^rho_{mu nu} = (1/2) g^{rho sigma} (d_mu g_{nu sigma} + d_nu g_{mu sigma} - d_sigma g_{mu nu})
  62
  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,