Moving a cutoff across two derivatives

The mixed-term estimate of lem:aniso:closure controls χ ∇²v, while the elliptic bounds of eq:aniso:closure:elliptic control ∇²(χ v). This file is the bridge between the two: for a cutoff χ that is smooth and compactly supported inside an open set U and a field v smooth on U,

∫ χ² |∇²v|² ≤ 4 ∫ |∇²(χ v)|² + 16 N² ∫ |∇χ|² + 16 N² ∫ |∇²χ|²,

where N bounds the full first-order jet |v|² + |∇v|² of v on the support of ∇χ.

The proof is pointwise plus one monotonicity step. Twice applying the Leibniz rule on U gives

χ ∂_k∂_j v_i = ∂_k∂_j(χ v_i) - (∂_kχ)(∂_j v_i) - (∂_jχ)(∂_k v_i) - (∂_k∂_jχ) v_i,

and (a - b - c - d)² ≤ 4(a² + b² + c² + d²) turns this into a pointwise bound whose three error terms carry a derivative of χ, hence are supported where the jet bound applies. Off U the cutoff vanishes, so the left-hand side is zero there and the pointwise bound is trivial.

Only the majorant has to be integrable: the bound is applied through integral_mono_of_nonneg, whose left-hand function need not be assumed integrable.

Vanishing near a point outside the support

theorem CIV.eventuallyEq_zero_nhds_of_notMem_tsupport {M : Type u_1} [Zero M] (f : CKN.Foundation.Parabolic.Vec3 → M) {x : CKN.Foundation.Parabolic.Vec3} (hx : x ∉ tsupport f) : f =ᶠ[nhds x] fun (x : CKN.Foundation.Parabolic.Vec3) => 0

A function vanishes on a whole neighbourhood of any point outside its support.

Smoothness of the first derivatives

theorem CIV.contDiffOn_fderiv_comp_apply {V : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3} {U : Set CKN.Foundation.Parabolic.Vec3} (hU : IsOpen U) (hV : ContDiffOn ℝ (↑⊤) V U) (i j : Fin 3) : ContDiffOn ℝ (↑⊤) (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => V z i) y) (CKN.basisVec j)) U

A coordinate derivative of a component of a field smooth on an open set is smooth there.

theorem CIV.contDiff_fderiv_apply_scalar (G : CKN.Foundation.Parabolic.Vec3 → ℝ) (hG : ContDiff ℝ (↑⊤) G) (j : Fin 3) : ContDiff ℝ ↑⊤ fun (x : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ G x) (CKN.basisVec j)

A coordinate derivative of a smooth scalar is smooth.

theorem CIV.continuous_fderiv_apply_scalar (G : CKN.Foundation.Parabolic.Vec3 → ℝ) (hG : ContDiff ℝ (↑⊤) G) (j : Fin 3) : Continuous fun (x : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ G x) (CKN.basisVec j)

A coordinate derivative of a smooth scalar is continuous.

The Leibniz rule, once and twice

The pointwise commutator inequality

Integrability of the majorant

theorem CIV.integrable_sum_sq_gradVec_cutoff (w : CKN.Foundation.Parabolic.Vec3 → ℝ) (hw : ContDiff ℝ (↑⊤) w) (hws : HasCompactSupport w) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, gradVec w x i ^ 2) MeasureTheory.volume

|∇χ|² is integrable for a smooth compactly supported cutoff.

theorem CIV.integrable_sum_sq_fderiv_gradVec_cutoff (w : CKN.Foundation.Parabolic.Vec3 → ℝ) (hw : ContDiff ℝ (↑⊤) w) (hws : HasCompactSupport w) : MeasureTheory.Integrable (fun (x : CKN.Foundation.Parabolic.Vec3) => ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => gradVec w y i) x) (CKN.basisVec j) ^ 2) MeasureTheory.volume

|∇²χ|² is integrable for a smooth compactly supported cutoff.

The second-order cutoff commutator bound

theorem CIV.integral_cutoff_sq_fderiv_fderiv_le (w : CKN.Foundation.Parabolic.Vec3 → ℝ) (V : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (U : Set CKN.Foundation.Parabolic.Vec3) (N : ℝ) (hU : IsOpen U) (hw : ContDiff ℝ (↑⊤) w) (hws : HasCompactSupport w) (hsupp : tsupport w ⊆ U) (hV : ContDiffOn ℝ (↑⊤) V U) (hjet : ∀ x ∈ tsupport (gradVec w), ∑ i : Fin 3, V x i ^ 2 + ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => V y i) x) (CKN.basisVec j) ^ 2 ≤ N ^ 2) : ∫ (x : CKN.Foundation.Parabolic.Vec3), w x ^ 2 * ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => V z i) y) (CKN.basisVec j)) x) (CKN.basisVec k) ^ 2 ≤ ((4 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, ∑ k : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (fderiv ℝ (fun (z : CKN.Foundation.Parabolic.Vec3) => (w z • V z) i) y) (CKN.basisVec j)) x) (CKN.basisVec k) ^ 2) + 16 * N ^ 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, gradVec w x i ^ 2) + 16 * N ^ 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => gradVec w y i) x) (CKN.basisVec j) ^ 2

The second-order cutoff commutator bound. For a cutoff χ smooth and compactly supported inside an open set U, a field v smooth on U, and N bounding the first-order jet of v on the support of ∇χ,

∫ χ² |∇²v|² ≤ 4 ∫ |∇²(χ v)|² + 16 N² ∫ |∇χ|² + 16 N² ∫ |∇²χ|².

This is the second-order counterpart of the first-order commutator step that moves the cutoff inside one derivative, and it is what lem:aniso:closure needs in order to convert the elliptic bound on ∇²(χ v) into a bound on χ ∇²v.

The first-order cutoff commutator bound

theorem CIV.integral_cutoff_sq_fderiv_le (w : CKN.Foundation.Parabolic.Vec3 → ℝ) (V : CKN.Foundation.Parabolic.Vec3 → CKN.Foundation.Parabolic.Vec3) (U : Set CKN.Foundation.Parabolic.Vec3) (N : ℝ) (hU : IsOpen U) (hw : ContDiff ℝ (↑⊤) w) (hws : HasCompactSupport w) (hsupp : tsupport w ⊆ U) (hV : ContDiffOn ℝ (↑⊤) V U) (hbd : ∀ x ∈ tsupport (gradVec w), ∑ i : Fin 3, V x i ^ 2 ≤ N ^ 2) : ∫ (x : CKN.Foundation.Parabolic.Vec3), w x ^ 2 * ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => V y i) x) (CKN.basisVec j) ^ 2 ≤ (2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, ∑ j : Fin 3, (fderiv ℝ (fun (y : CKN.Foundation.Parabolic.Vec3) => (w y • V y) i) x) (CKN.basisVec j) ^ 2) + 2 * N ^ 2 * ∫ (x : CKN.Foundation.Parabolic.Vec3), ∑ i : Fin 3, gradVec w x i ^ 2

The first-order cutoff commutator bound. For a cutoff χ smooth and compactly supported inside an open set U, a field v smooth on U, and N bounding |v| on the support of ∇χ,

∫ χ² |∇v|² ≤ 2 ∫ |∇(χ v)|² + 2 N² ∫ |∇χ|².