Coarse-graining support: Support.Sobolev.Foundations.Cutoff.DerivativeBounds

Imported from the Apache-2.0 CoarseGraining development at commit c7ddd76c08ade64fed1b8d2ca51be14dfee8deb4.

Compact-support derivative bounds

This file contains small reusable analytic lemmas for smooth compactly supported functions on Vec d. They are intentionally independent of the specific cutoff formulas.

theorem HCPolySupport.norm_clm_le_sum_basisVec_apply {d : ℕ} (L : Vec d →L[ℝ] ℝ) : ‖L‖ ≤ ∑ i : Fin d, ‖L (basisVec i)‖

Operator norm bound for scalar continuous linear maps on Vec d, using the coordinate basis and the default product/sup norm on Vec d.

theorem HCPolySupport.fderiv_coord_sub_const_apply_basisVec {d : ℕ} (i j : Fin d) (c x : Vec d) : (fderiv ℝ (fun (y : Vec d) => y i - c i) x) (basisVec j) = if j = i then 1 else 0

Directional derivative of a shifted coordinate in a coordinate direction.

theorem HCPolySupport.norm_fderiv_coord_sub_const_le_one {d : ℕ} (i : Fin d) (c x : Vec d) : ‖fderiv ℝ (fun (y : Vec d) => y i - c i) x‖ ≤ 1

The operator norm of a shifted coordinate derivative is at most 1 in the default product/sup norm on Vec d.

theorem HCPolySupport.fderiv_coord_sub_const_eq_proj {d : ℕ} (i : Fin d) (c x : Vec d) : fderiv ℝ (fun (y : Vec d) => y i - c i) x = ContinuousLinearMap.proj i

The derivative of a shifted coordinate is constant in the base point.

theorem HCPolySupport.fderiv_coord_sub_const_sq_apply_basisVec {d : ℕ} (i j : Fin d) (c x : Vec d) : (fderiv ℝ (fun (y : Vec d) => (y i - c i) ^ 2) x) (basisVec j) = 2 * (x i - c i) * if j = i then 1 else 0

Directional derivative of a shifted coordinate square in a coordinate direction.

theorem HCPolySupport.iteratedFDeriv_two_coord_sub_const_eq_zero {d : ℕ} (i : Fin d) (c : Vec d) : (iteratedFDeriv ℝ 2 fun (y : Vec d) => y i - c i) = 0

A shifted coordinate is affine, so its second Fréchet derivative vanishes.

theorem HCPolySupport.norm_iteratedFDeriv_two_coord_sub_const_sq_le {d : ℕ} (i : Fin d) (c x : Vec d) : ‖iteratedFDeriv ℝ 2 (fun (y : Vec d) => (y i - c i) ^ 2) x‖ ≤ 2

Uniform second-derivative bound for the square of a shifted coordinate.

theorem HCPolySupport.norm_iteratedFDeriv_two_euclideanSqDist_le {d : ℕ} (x₀ x : Vec d) : ‖iteratedFDeriv ℝ 2 (fun (y : Vec d) => euclideanSqDist y x₀) x‖ ≤ 2 * ↑d

Euclidean squared distance has second derivative bounded by 2 d in the default product/sup norm on Vec d.

theorem HCPolySupport.fderiv_euclideanSqDist_apply_basisVec {d : ℕ} (x₀ x : Vec d) (j : Fin d) : (fderiv ℝ (fun (y : Vec d) => euclideanSqDist y x₀) x) (basisVec j) = 2 * (x j - x₀ j)

Coordinate-direction derivative of Euclidean squared distance on Vec d.

theorem HCPolySupport.norm_fderiv_profile_comp_le {d : ℕ} (θ : QuantitativeTransitionProfile) {g : Vec d → ℝ} {x : Vec d} (hg : DifferentiableAt ℝ g x) : ‖fderiv ℝ (fun (y : Vec d) => θ.toFun (g y)) x‖ ≤ θ.derivBound * ‖fderiv ℝ g x‖

Chain-rule bound for composing a quantitative one-dimensional transition profile with a scalar function on Vec d.

theorem HCPolySupport.norm_iteratedFDeriv_two_profile_comp_le {d : ℕ} (θ : QuantitativeTransitionProfile) {g : Vec d → ℝ} {x : Vec d} {D : ℝ} (hg : ContDiff ℝ (↑2) g) (hD_one : ‖iteratedFDeriv ℝ 1 g x‖ ≤ D) (hD_two : ‖iteratedFDeriv ℝ 2 g x‖ ≤ D ^ 2) : ‖iteratedFDeriv ℝ 2 (fun (y : Vec d) => θ.toFun (g y)) x‖ ≤ 2 * max 1 (max θ.derivBound θ.secondDerivBound) * D ^ 2

Chain-rule Hessian bound for composing a quantitative one-dimensional transition profile with a scalar function. The argument is measured through a single scale D controlling both the first and second derivatives in the form required by Mathlib's quantitative composition estimate.

theorem HCPolySupport.exists_bound_fderiv_of_contDiff_hasCompactSupport {d : ℕ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_comp : HasCompactSupport η) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Vec d), ‖fderiv ℝ η x‖ ≤ C

A smooth compactly supported scalar function has a global first-derivative bound.

theorem HCPolySupport.exists_bound_iteratedFDeriv_two_of_contDiff_hasCompactSupport {d : ℕ} {η : Vec d → ℝ} (hη : ContDiff ℝ (↑⊤) η) (hη_comp : HasCompactSupport η) : ∃ (C : ℝ), 0 ≤ C ∧ ∀ (x : Vec d), ‖iteratedFDeriv ℝ 2 η x‖ ≤ C

A smooth compactly supported scalar function has a global second-derivative bound, expressed through iteratedFDeriv.