Cutting a locally smooth function off to a globally smooth one

The interior-regularity chain runs on a FullEllipticOp, whose coefficients are global on EuclideanSpace ℝ (Fin d), essentially bounded, and asked for no more. A datum smooth on an open set U alone, or coefficients smooth on U alone with no bound off it, do not meet that shape directly. Multiplying by a smooth cutoff supported in U and equal to 1 near the region of interest repairs this: the product is globally smooth, compactly supported, and so lies in W^{k,∞} at every order, with no bound needed on the factor itself.

This file supplies that cutting-off step in general, for a single scalar function; LocalOp applies it entrywise to build a global operator out of one with coefficients smooth on U alone.

Main declarations

• contDiff_mul_of_contDiffOn: a function smooth on U, cut off by a test function of U, is globally smooth.
• hasCompactSupport_mul: the product has compact support.
• exists_iteratedFDeriv_bound: a smooth compactly supported function has every iterated derivative uniformly bounded.
• exists_iteratedFDeriv_bound_const_add: the same for a constant shift of one, at every positive order.
• nonempty_isWkInfty: a smooth compactly supported function lies in W^{k,∞} at every order.

theorem EllipticPdes.Regularity.contDiff_mul_of_contDiffOn {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} (hU : IsOpen U) {χ g : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) (hg : ContDiffOn ℝ (↑⊤) g U) : ContDiff ℝ ↑⊤ fun (x : EuclideanSpace ℝ (Fin d)) => χ x * g x

A function smooth on an open U, multiplied by a test function supported in U, is globally smooth: away from the topological support of the cutoff the product is eventually zero, and on that support the cutoff itself is smooth wherever g is, since the support sits inside U.

theorem EllipticPdes.Regularity.hasCompactSupport_mul {d : ℕ} {U : Set (EuclideanSpace ℝ (Fin d))} {χ g : EuclideanSpace ℝ (Fin d) → ℝ} (hχ : Sobolev.IsTestFn U χ) : HasCompactSupport fun (x : EuclideanSpace ℝ (Fin d)) => χ x * g x

The product of a test function with any function has compact support: the topological support of the product sits inside that of the cutoff.

theorem EllipticPdes.Regularity.exists_iteratedFDeriv_bound {d : ℕ} {g : EuclideanSpace ℝ (Fin d) → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hc : HasCompactSupport g) : ∃ (B : ℕ → ℝ), (∀ (m : ℕ), 0 ≤ B m) ∧ ∀ (m : ℕ) (x : EuclideanSpace ℝ (Fin d)), ‖iteratedFDeriv ℝ m g x‖ ≤ B m

A smooth compactly supported function has every iterated derivative bounded, with a nonnegative bound at each order: the derivative is continuous and vanishes off a compact set, so it is bounded, and the bound is truncated at 0 to be usable at every order uniformly.

theorem EllipticPdes.Regularity.exists_iteratedFDeriv_bound_const_add {d : ℕ} {g : EuclideanSpace ℝ (Fin d) → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hc : HasCompactSupport g) (c : ℝ) : ∃ (B : ℕ → ℝ), (∀ (m : ℕ), 0 ≤ B m) ∧ ∀ (m : ℕ), 1 ≤ m → ∀ (x : EuclideanSpace ℝ (Fin d)), ‖iteratedFDeriv ℝ m (fun (y : EuclideanSpace ℝ (Fin d)) => c + g y) x‖ ≤ B m

A constant plus a smooth compactly supported function has every iterated derivative of positive order bounded: the constant contributes nothing past order zero, so the bound of exists_iteratedFDeriv_bound for the compactly supported part serves unchanged.

theorem EllipticPdes.Regularity.nonempty_isWkInfty {d : ℕ} {g : EuclideanSpace ℝ (Fin d) → ℝ} (hg : ContDiff ℝ (↑⊤) g) (hc : HasCompactSupport g) (k : ℕ) : Nonempty (IsWkInfty g k)

A smooth compactly supported function lies in W^{k,∞} at every order: its classical iterated partials serve as the weak-derivative family, and exists_iteratedFDeriv_bound supplies the uniform bound each order needs.