`MetricTensor`

definition

show as: view math explainer →

module: IndisputableMonolith.Gravity.Connection
domain: Gravity
line: 39 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Gravity.Connection on GitHub at line 39.

browse module

All declarations in this module, on Recognition.

explainer page

Tracked in the explainer inventory; generation is lazy so crawlers do not trigger LLM jobs.

open explainer

depends on

used by

formal source

  36
  37/-- A metric tensor in local coordinates: a symmetric 4x4 matrix
  38    at each spacetime point (here abstracted as just the components). -/
  39structure MetricTensor where
  40  g : Idx → Idx → ℝ
  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.

papers checked against this theorem

No papers in the current corpus map onto this theorem yet.