partialDeriv_v2_mul

formal source

 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 :=
 123    deriv_mul hf hg
 124  rw [h_mul]
 125  simp only [coordRay_zero]
 126  ring
 127
 128/-- Spatial norm squared `x₁² + x₂² + x₃²`. -/
 129def spatialNormSq (x : Fin 4 → ℝ) : ℝ := x 1 ^ 2 + x 2 ^ 2 + x 3 ^ 2
 130
 131theorem spatialNormSq_nonneg (x : Fin 4 → ℝ) : 0 ≤ spatialNormSq x := by
 132  unfold spatialNormSq
 133  positivity
 134
 135theorem spatialNormSq_eq_zero_iff (x : Fin 4 → ℝ) : spatialNormSq x = 0 ↔ x 1 = 0 ∧ x 2 = 0 ∧ x 3 = 0 := by
 136  unfold spatialNormSq
 137  constructor
 138  · intro h
 139    have h1 := sq_nonneg (x 1)
 140    have h2 := sq_nonneg (x 2)
 141    have h3 := sq_nonneg (x 3)
 142    have h1_zero : x 1 ^ 2 = 0 := by linarith
 143    have h2_zero : x 2 ^ 2 = 0 := by linarith
 144    have h3_zero : x 3 ^ 2 = 0 := by linarith