`eta`

definition

show as: view math explainer →

module: IndisputableMonolith.Relativity.Geometry.Metric
domain: Relativity
line: 19 · 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 19.

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

  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
  42      by_cases h : low 0 = low 1
  43      · have h_rev : low 1 = low 0 := h.symm
  44        rw [if_pos h, if_pos h, if_pos h_rev, if_pos h_rev]
  45        rw [h]
  46      · have h_rev : low 1 ≠ low 0 := fun heq => h heq.symm
  47        rw [if_neg h, if_neg h, if_neg h_rev, if_neg h_rev] }
  48
  49noncomputable def metric_to_matrix (g : MetricTensor) (x : Fin 4 → ℝ) : Matrix (Fin 4) (Fin 4) ℝ :=

papers checked against this theorem

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