partialDeriv_v2_const

formal source

  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
  65  unfold partialDeriv_v2
  66  exact deriv_add hf hg
  67
  68/-- Linearity of directional derivative (scalar multiplication). -/
  69lemma partialDeriv_v2_smul (f : (Fin 4 → ℝ) → ℝ) (c : ℝ) (μ : Fin 4)