coordRay_zero

formal source

  23@[simp] lemma coordRay_apply (x : Fin 4 → ℝ) (μ : Fin 4) (t : ℝ) (ν : Fin 4) :
  24    coordRay x μ t ν = x ν + t * basisVec μ ν := rfl
  25
  26@[simp] lemma coordRay_zero (x : Fin 4 → ℝ) (μ : Fin 4) : coordRay x μ 0 = x := by
  27  funext ν; simp [coordRay]
  28
  29@[simp] lemma coordRay_coordRay (x : Fin 4 → ℝ) (μ : Fin 4) (s t : ℝ) :
  30    coordRay (coordRay x μ s) μ t = coordRay x μ (s + t) := by
  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 +