Cutting a test function against a cutoff

The localised moves of EllipticPdes.Regularity.DifferentiatedEquation are stated for test functions supported inside the region V where the weak-derivative data lives. The terms of higher interior regularity (Evans, Partial Differential Equations (2nd ed.), §6.3.1, Theorem 2) instead pair against a test function on the whole domain, each term with a factor supported inside a compact K ⊆ V. Replacing the test function φ by χ · φ for a cutoff χ identically 1 near K and supported in V brings the two shapes together.

The replacement is invisible to any factor supported in K: there χ = 1 and ∂ⱼχ = 0, so the Leibniz expansion of ∂ⱼ(χ φ) collapses to ∂ⱼφ. Both facts need χ = 1 on a neighbourhood of K, which is the form CutoffTower (EllipticPdes.Regularity.CutoffTower) records its three cutoffs in.

Main declarations

• partialD_eq_zero_of_eventually_one: a function identically 1 near K has vanishing partials on K.
• isTestFn_cut: χ · φ is a test function on V whenever χ is a compactly supported smooth function with tsupport χ ⊆ V and φ is smooth.
• mul_cut_eq, mul_partialD_cut_eq: the pointwise cutting identities.
• setIntegral_mul_cut_eq, setIntegral_mul_partialD_cut_eq: their integral forms, for a weight vanishing almost everywhere off K.

Two pointwise facts

theorem EllipticPdes.Regularity.partialD_eq_zero_of_eventually_one {d : ℕ} {K : Set (EuclideanSpace ℝ (Fin d))} {χ : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : ∀ᶠ (x : EuclideanSpace ℝ (Fin d)) in nhdsSet K, χ x = 1) {x : EuclideanSpace ℝ (Fin d)} (hx : x ∈ K) (j : Fin d) : Sobolev.partialD j χ x = 0

Vanishing partials on K of a cutoff identically 1 near it. At a point of K the function agrees with the constant 1 on a whole neighbourhood, so its Fréchet derivative is the derivative of a constant.

theorem EllipticPdes.Regularity.isTestFn_cut {d : ℕ} {V : Set (EuclideanSpace ℝ (Fin d))} {χ φ : EuclideanSpace ℝ (Fin d) → ℝ} (hχc : ContDiff ℝ (↑⊤) χ) (hχcs : HasCompactSupport χ) (hχV : tsupport χ ⊆ V) (hφc : ContDiff ℝ (↑⊤) φ) : Sobolev.IsTestFn V fun (x : EuclideanSpace ℝ (Fin d)) => χ x * φ x

Cut of a smooth function as a test function on V. Smoothness is ContDiff.mul, compact support comes from χ, and the support inclusion is the one χ has. Unlike isTestFn_mul, the second factor need not be compactly supported.

theorem EllipticPdes.Regularity.mul_cut_eq {d : ℕ} {K : Set (EuclideanSpace ℝ (Fin d))} {χ φ w : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : ∀ᶠ (x : EuclideanSpace ℝ (Fin d)) in nhdsSet K, χ x = 1) (hw : tsupport w ⊆ K) (x : EuclideanSpace ℝ (Fin d)) : w x * (χ x * φ x) = w x * φ x

Cutting is invisible to a weight supported in K, at the level of the function itself: w · (χ φ) = w · φ pointwise, because χ = 1 on K ⊇ tsupport w and w vanishes off its support.

theorem EllipticPdes.Regularity.mul_partialD_cut_eq {d : ℕ} {K : Set (EuclideanSpace ℝ (Fin d))} {χ φ w : EuclideanSpace ℝ (Fin d) → ℝ} (hχd : Differentiable ℝ χ) (hφd : Differentiable ℝ φ) (hχ : ∀ᶠ (x : EuclideanSpace ℝ (Fin d)) in nhdsSet K, χ x = 1) (hw : tsupport w ⊆ K) (j : Fin d) (x : EuclideanSpace ℝ (Fin d)) : w x * Sobolev.partialD j (fun (y : EuclideanSpace ℝ (Fin d)) => χ y * φ y) x = w x * Sobolev.partialD j φ x

Cutting is invisible to a weight supported in K, at the level of the gradient: w · ∂ⱼ(χ φ) = w · ∂ⱼφ pointwise. The Leibniz rule splits ∂ⱼ(χ φ) into χ ∂ⱼφ + (∂ⱼχ) φ, and on K the first factor is ∂ⱼφ while the second vanishes.

Integral forms for an almost-everywhere supported weight

theorem EllipticPdes.Regularity.setIntegral_mul_cut_eq {d : ℕ} {S K : Set (EuclideanSpace ℝ (Fin d))} {χ φ w : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : ∀ᶠ (x : EuclideanSpace ℝ (Fin d)) in nhdsSet K, χ x = 1) (hw : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict S, x ∉ K → w x = 0) : ∫ (x : EuclideanSpace ℝ (Fin d)) in S, w x * (χ x * φ x) = ∫ (x : EuclideanSpace ℝ (Fin d)) in S, w x * φ x

Integral form of mul_cut_eq. The weight is only required to vanish almost everywhere off K, which is the form an L² class supported in K supplies.

theorem EllipticPdes.Regularity.setIntegral_mul_partialD_cut_eq {d : ℕ} {S K : Set (EuclideanSpace ℝ (Fin d))} {χ φ w : EuclideanSpace ℝ (Fin d) → ℝ} (hχd : Differentiable ℝ χ) (hφd : Differentiable ℝ φ) (hχ : ∀ᶠ (x : EuclideanSpace ℝ (Fin d)) in nhdsSet K, χ x = 1) (hw : ∀ᵐ (x : EuclideanSpace ℝ (Fin d)) ∂MeasureTheory.volume.restrict S, x ∉ K → w x = 0) (j : Fin d) : ∫ (x : EuclideanSpace ℝ (Fin d)) in S, w x * Sobolev.partialD j (fun (y : EuclideanSpace ℝ (Fin d)) => χ y * φ y) x = ∫ (x : EuclideanSpace ℝ (Fin d)) in S, w x * Sobolev.partialD j φ x

Integral form of mul_partialD_cut_eq. The weight is only required to vanish almost everywhere off K.