  89  exact deriv_const_mul c h2
  90
  91/-- Second derivative linearity (scalar multiplication). -/
  92lemma secondDeriv_smul (f : (Fin 4 → ℝ) → ℝ) (c : ℝ) (μ ν : Fin 4)
  93    (x : Fin 4 → ℝ)
  94    (h1 : ∀ y, DifferentiableAt ℝ (fun t => f (coordRay y μ t)) 0)
  95    (h2 : DifferentiableAt ℝ (fun s => partialDeriv_v2 f μ (coordRay x ν s)) 0) :
  96  secondDeriv (fun y => c * f y) μ ν x = c * secondDeriv f μ ν x := by
  97  unfold secondDeriv
  98  have h_partial : ∀ y, partialDeriv_v2 (fun z => c * f z) μ y = c * partialDeriv_v2 f μ y := by
  99    intro y
 100    exact partialDeriv_v2_smul f c μ y (h1 y)
 101  simp only [h_partial]
 102  exact deriv_const_mul c h2
 103
 104/-- Laplacian linearity (scalar multiplication). -/
 105lemma laplacian_smul (f : (Fin 4 → ℝ) → ℝ) (c : ℝ) (x : Fin 4 → ℝ)
 106    (h1 : ∀ μ y, DifferentiableAt ℝ (fun t => f (coordRay y μ t)) 0)
 107    (h2 : ∀ μ ν, DifferentiableAt ℝ (fun s => partialDeriv_v2 f μ (coordRay x ν s)) 0) :
 108  laplacian (fun y => c * f y) x = c * laplacian f x := by
 109  unfold laplacian
 110  simp only [secondDeriv_smul f c _ _ x (h1 _) (h2 _ _)]
 111  ring
 112
 113/-- Product rule for directional derivative. -/
 114lemma partialDeriv_v2_mul (f g : (Fin 4 → ℝ) → ℝ) (μ : Fin 4)
 115    (x : Fin 4 → ℝ) (hf : DifferentiableAt ℝ (fun t => f (coordRay x μ t)) 0)
 116    (hg : DifferentiableAt ℝ (fun t => g (coordRay x μ t)) 0) :
 117  partialDeriv_v2 (fun y => f y * g y) μ x =
 118    f x * partialDeriv_v2 g μ x + g x * partialDeriv_v2 f μ x := by
 119  unfold partialDeriv_v2
 120  have h_mul : deriv (fun ε => f (coordRay x μ ε) * g (coordRay x μ ε)) 0 =
 121               deriv (fun ε => f (coordRay x μ ε)) 0 * g (coordRay x μ 0) +
 122               f (coordRay x μ 0) * deriv (fun ε => g (coordRay x μ ε)) 0 :=

papers checked against this theorem

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