Scalar coordinate product rules for the localized harmonic estimates.

theorem EulerMeanHarmonic.partialDerivative_add {f g : EulerSmoothLimit.Space → ℝ} {x : EulerSmoothLimit.Space} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (i : Fin 3) : EulerVectorCalculus.partialDerivative (f + g) i x = EulerVectorCalculus.partialDerivative f i x + EulerVectorCalculus.partialDerivative g i x

theorem EulerMeanHarmonic.partialDerivative_mul {f g : EulerSmoothLimit.Space → ℝ} {x : EulerSmoothLimit.Space} (hf : DifferentiableAt ℝ f x) (hg : DifferentiableAt ℝ g x) (i : Fin 3) : EulerVectorCalculus.partialDerivative (f * g) i x = g x * EulerVectorCalculus.partialDerivative f i x + f x * EulerVectorCalculus.partialDerivative g i x

theorem EulerMeanHarmonic.secondPartial_mul (f g : EulerSmoothLimit.Space → ℝ) (hf : ContDiff ℝ (↑⊤) f) (hg : ContDiff ℝ (↑⊤) g) (i : Fin 3) (x : EulerSmoothLimit.Space) : EulerVectorCalculus.partialDerivative (EulerVectorCalculus.partialDerivative (f * g) i) i x = g x * EulerVectorCalculus.partialDerivative (EulerVectorCalculus.partialDerivative f i) i x + 2 * EulerVectorCalculus.partialDerivative f i x * EulerVectorCalculus.partialDerivative g i x + f x * EulerVectorCalculus.partialDerivative (EulerVectorCalculus.partialDerivative g i) i x

theorem EulerMeanHarmonic.sq_add_three_le (a b c : ℝ) : (a + b + c) ^ 2 ≤ 3 * (a ^ 2 + b ^ 2 + c ^ 2)