`MetricTensor`

definition

show as: view math explainer →

module: IndisputableMonolith.Relativity.Geometry.Metric
domain: Relativity
line: 11 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.Geometry.Metric on GitHub at line 11.

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

   8
   9open Calculus
  10
  11structure MetricTensor where
  12  g : BilinearForm
  13  symmetric : ∀ x up low, g x up low = g x up (fun i => if (i : ℕ) = 0 then low 1 else low 0)
  14
  15@[ext]
  16lemma MetricTensor.ext (g1 g2 : MetricTensor) (h : g1.g = g2.g) : g1 = g2 := by
  17  cases g1; cases g2; simp_all
  18
  19noncomputable def eta : BilinearForm := fun _ _ low =>
  20  if low 0 = low 1 then (if (low 0 : ℕ) = 0 then -1 else 1) else 0
  21
  22noncomputable def minkowski_tensor : MetricTensor :=
  23  { g := eta
  24    symmetric := by
  25      intro x up low
  26      unfold eta
  27      dsimp
  28      by_cases h : low 0 = low 1
  29      · have h_rev : low 1 = low 0 := h.symm
  30        rw [if_pos h, if_pos h_rev]
  31        rw [h]
  32      · have h_rev : low 1 ≠ low 0 := fun heq => h heq.symm
  33        rw [if_neg h, if_neg h_rev] }
  34
  35noncomputable def metric_from_rrf (psi : (Fin 4 → ℝ) → ℝ) (k : ℝ) : MetricTensor :=
  36  { g := fun x _ low =>
  37      eta x (fun _ => 0) low + k * psi x * (if low 0 = low 1 then 1 else 0)
  38    symmetric := by
  39      intro x up low
  40      unfold eta
  41      dsimp

papers checked against this theorem

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