Iterated Derivative Helpers

Bounds on iterated derivatives of continuous linear maps and quadratic forms, used in the Schwartz decay proof for the equilibrium Maxwellian.

theorem VML.iteratedFDeriv_clm_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (n : ℕ) (hn : 2 ≤ n) (x : E) : iteratedFDeriv 𝕜 n (⇑f) x = 0

The iterated derivative of a continuous linear map vanishes at order ≥ 2.

theorem VML.norm_iteratedFDeriv_one_clm {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E →L[𝕜] F) (x : E) : ‖iteratedFDeriv 𝕜 1 (⇑f) x‖ = ‖f‖

The norm of the first iterated derivative of a CLM equals the operator norm.

theorem VML.norm_fderiv_eq_iteratedFDeriv_one {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] (f : E → F) (v : E) : ‖fderiv 𝕜 f v‖ = ‖iteratedFDeriv 𝕜 1 f v‖

‖fderiv f v‖ = ‖iteratedFDeriv 1 f v‖. Converts between the ContinuousLinearMap norm and the ContinuousMultilinearMap norm at order 1.

theorem VML.norm_sq_le_normSq (v : Fin 3 → ℝ) : ‖v‖ ^ 2 ≤ normSq v

For Fin 3 → ℝ with sup norm: ‖v‖² ≤ normSq v = ∑ vᵢ².

theorem VML.contDiff_negNormSq_div (T : ℝ) : ContDiff ℝ ⊤ fun (v : Fin 3 → ℝ) => -normSq v / (2 * T)

theorem VML.norm_iteratedFDeriv_proj_sq_le (j : Fin 3) (i : ℕ) (hi : 1 ≤ i) (v : Fin 3 → ℝ) : ‖iteratedFDeriv ℝ i (fun (w : Fin 3 → ℝ) => w j * w j) v‖ ≤ 2 * (1 + ‖v‖)

‖iteratedFDeriv i (v_j²) v‖ ≤ 2(1+‖v‖) for i ≥ 1, via Leibniz on proj_j * proj_j.

theorem VML.quadratic_iteratedFDeriv_bound (T : ℝ) (hT : 0 < T) (k : ℕ) : ∃ c > 0, ∀ (v : Fin 3 → ℝ) (i : ℕ), 1 ≤ i → i ≤ k → ‖iteratedFDeriv ℝ i (fun (v : Fin 3 → ℝ) => -normSq v / (2 * T)) v‖ ≤ (c * (1 + ‖v‖)) ^ i

Derivative bound for the quadratic form q(v) = -normSq(v)/(2T). Since q is a degree-2 polynomial: fderiv is O(1+‖v‖), second derivative is constant, and all higher derivatives vanish.