The differential operator norm and the coordinate gradient energy

The three coordinate derivatives control the operator norm of the full derivative. These pointwise estimates do not require differentiability: Lean's totalized fderiv is a continuous linear map for every function.

theorem NavierStokesR3.GradientOperator.gradientSq_nonneg (w : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) : 0 ≤ Comparison.gradientSq w x

theorem NavierStokesR3.GradientOperator.partial_norm_le_sqrt_gradientSq (w : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) (i : Fin 3) : ‖Comparison.partialD i w x‖ ≤ √(Comparison.gradientSq w x)

theorem NavierStokesR3.GradientOperator.fderiv_apply_eq_sum (w : ProblemStatement.Space → ProblemStatement.Space) (x v : ProblemStatement.Space) : (fderiv ℝ w x) v = ∑ i : Fin 3, v.ofLp i • Comparison.partialD i w x

The derivative applied to a vector, expanded in the standard coordinate basis.

theorem NavierStokesR3.GradientOperator.norm_fderiv_le_three_mul_sqrt_gradientSq (w : ProblemStatement.Space → ProblemStatement.Space) (x : ProblemStatement.Space) : ‖fderiv ℝ w x‖ ≤ 3 * √(Comparison.gradientSq w x)

theorem NavierStokesR3.GradientOperator.continuous_gradientSq {w : ProblemStatement.Space → ProblemStatement.Space} (hw : ContDiff ℝ 1 w) : Continuous (Comparison.gradientSq w)