`gradient`

definition

show as: view math explainer →

module: IndisputableMonolith.Relativity.Fields.Scalar
domain: Relativity
line: 72 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.Fields.Scalar on GitHub at line 72.

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

  69  norm_num
  70
  71/-- Gradient: collection of all directional derivatives ∂_μ ψ. -/
  72noncomputable def gradient (φ : ScalarField) (x : Fin 4 → ℝ) : Fin 4 → ℝ :=
  73  fun μ => directional_deriv φ μ x
  74
  75/-- Squared gradient g^{μν} (∂_μ ψ)(∂_ν ψ) with inverse metric. -/
  76noncomputable def gradient_squared (φ : ScalarField) (g : MetricTensor) (x : Fin 4 → ℝ) : ℝ :=
  77  Finset.sum (Finset.univ : Finset (Fin 4)) (fun μ =>
  78    Finset.sum (Finset.univ : Finset (Fin 4)) (fun ν =>
  79      (inverse_metric g) x (fun i => if (i : ℕ) = 0 then μ else ν) (fun _ => 0) *
  80      (gradient φ x μ) * (gradient φ x ν)))
  81
  82/-- Gradient squared for Minkowski metric. -/
  83theorem gradient_squared_minkowski (φ : ScalarField) (x : Fin 4 → ℝ) :
  84  gradient_squared φ minkowski_tensor x =
  85    -(gradient φ x 0)^2 + (gradient φ x 1)^2 + (gradient φ x 2)^2 + (gradient φ x 3)^2 := by
  86  unfold gradient_squared
  87  apply gradient_squared_minkowski_sum
  88
  89/-- Field squared. -/
  90noncomputable def field_squared (φ : ScalarField) (x : Fin 4 → ℝ) : ℝ :=
  91  (φ.ψ x) ^ 2
  92
  93theorem field_squared_nonneg (φ : ScalarField) (x : Fin 4 → ℝ) :
  94  field_squared φ x ≥ 0 := by
  95  simp [field_squared]
  96  exact sq_nonneg _
  97
  98end Fields
  99end Relativity
 100end IndisputableMonolith

papers checked against this theorem

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