lemma
proved
term proof
partialDeriv_v2_mul
show as:
view Lean formalization →
formal statement (Lean)
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
proof body
Term-mode proof.
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 :=
123 deriv_mul hf hg
124 rw [h_mul]
125 simp only [coordRay_zero]
126 ring
127
128/-- Spatial norm squared `x₁² + x₂² + x₃²`. -/