`partialDeriv_v2`

definition

show as: view math explainer →

module: IndisputableMonolith.Relativity.Calculus.Derivatives
domain: Relativity
line: 34 · github
papers citing: none yet

open explainer

Generate a durable explainer page for this declaration.

open lean source

IndisputableMonolith.Relativity.Calculus.Derivatives on GitHub at line 34.

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

  31  funext ν; simp [coordRay]; ring
  32
  33/-- Directional derivative `∂_μ f(x)` via real derivative along the coordinate ray. -/
  34noncomputable def partialDeriv_v2 (f : (Fin 4 → ℝ) → ℝ) (μ : Fin 4)
  35    (x : Fin 4 → ℝ) : ℝ :=
  36  deriv (fun t => f (coordRay x μ t)) 0
  37
  38/-- The derivative of a constant function is zero. -/
  39lemma partialDeriv_v2_const {f : (Fin 4 → ℝ) → ℝ} {c : ℝ} (h : ∀ y, f y = c) (μ : Fin 4) (x : Fin 4 → ℝ) :
  40    partialDeriv_v2 f μ x = 0 := by
  41  unfold partialDeriv_v2
  42  have h_const : (fun t => f (coordRay x μ t)) = (fun _ => c) := by
  43    funext t
  44    rw [h]
  45  rw [h_const]
  46  exact deriv_const (0 : ℝ) c
  47
  48/-- Second derivative `∂_μ∂_ν f(x)` as iterated directional derivatives. -/
  49noncomputable def secondDeriv (f : (Fin 4 → ℝ) → ℝ) (μ ν : Fin 4)
  50    (x : Fin 4 → ℝ) : ℝ :=
  51  deriv (fun s => partialDeriv_v2 f μ (coordRay x ν s)) 0
  52
  53/-- Laplacian `∇² = Σ_{i=1}^3 ∂²/∂xᵢ²`. -/
  54noncomputable def laplacian (f : (Fin 4 → ℝ) → ℝ) (x : Fin 4 → ℝ) : ℝ :=
  55  secondDeriv f ⟨1, by decide⟩ ⟨1, by decide⟩ x +
  56  secondDeriv f ⟨2, by decide⟩ ⟨2, by decide⟩ x +
  57  secondDeriv f ⟨3, by decide⟩ ⟨3, by decide⟩ x
  58
  59/-- Linearity of the directional derivative. -/
  60lemma deriv_add_lin (f g : (Fin 4 → ℝ) → ℝ) (μ : Fin 4)
  61    (x : Fin 4 → ℝ) (hf : DifferentiableAt ℝ (fun t => f (coordRay x μ t)) 0)
  62    (hg : DifferentiableAt ℝ (fun t => g (coordRay x μ t)) 0) :
  63  partialDeriv_v2 (fun y => f y + g y) μ x =
  64    partialDeriv_v2 f μ x + partialDeriv_v2 g μ x := by

papers checked against this theorem

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