minkowski_inverse

formal source

  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,
  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,