Dilated cutoffs with Laplacian bounds

In a finite-dimensional real inner product space, dilating a fixed smooth bump by R gives cutoffs χ_R, equal to 1 on ball 0 R and to 0 off closedBall 0 (2R), with ‖Dχ_R‖ = O(1/R) and |Δχ_R| = O(1/R²) uniformly in R (TauCeti.exists_forall_contDiff_cutoff_ball_norm_laplacian_le). These are the truncations used to localize solutions of the Poisson equation: the error Δ(χ_R u) - χ_R Δu lives on the annulus R ≤ ‖x‖ ≤ 2R and is controlled by the decay of u and Du there.

In dimension two the bound |Δχ_R| = O(1/R²) makes ∫ |Δχ_R| bounded uniformly in R, so ∫ Δχ_R f → 0 for every f tending to 0 at infinity (TauCeti.tendsto_integral_laplacian_smul_of_tendsto_cocompact). This lets identities tested against χ_R pass to R → ∞.

theorem TauCeti.exists_forall_contDiff_cutoff_ball_norm_laplacian_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : ∃ (C : ℝ), ∀ (R : ℝ), 0 < R → ∃ (χ : E → ℝ), ContDiff ℝ (↑⊤) χ ∧ HasCompactSupport χ ∧ (∀ (x : E), ‖x‖ < R → χ =ᶠ[nhds x] fun (x : E) => 1) ∧ (∀ (x : E), 2 * R < ‖x‖ → χ =ᶠ[nhds x] fun (x : E) => 0) ∧ (∀ (x : E), ‖fderiv ℝ χ x‖ ≤ C / R) ∧ (∀ (x : E), ‖Laplacian.laplacian χ x‖ ≤ C / R ^ 2) ∧ ∀ (x : E), χ x ∈ Set.Icc 0 1

Dilated cutoffs with Laplacian bounds. There is a constant C such that for every R > 0 some smooth compactly supported χ equals 1 near every point of ball 0 R, equals 0 near every point outside closedBall 0 (2R), and satisfies 0 ≤ χ ≤ 1, ‖Dχ‖ ≤ C / R and |Δχ| ≤ C / R². The cutoff is x ↦ b (R⁻¹ • x) for a fixed smooth bump b equal to 1 on closedBall 0 1 and supported in closedBall 0 2.

theorem TauCeti.tendsto_integral_laplacian_smul_of_tendsto_cocompact {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {F : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] {ι : Type u_3} {l : Filter ι} {χ : ι → E → ℝ} {R : ι → ℝ} (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (hE : Module.finrank ℝ E = 2) {C : ℝ} (hR : Filter.Tendsto R l Filter.atTop) (hχ1 : ∀ (i : ι) (x : E), ‖x‖ < R i → χ i =ᶠ[nhds x] fun (x : E) => 1) (hχ0 : ∀ (i : ι) (x : E), 2 * R i < ‖x‖ → χ i =ᶠ[nhds x] fun (x : E) => 0) (hχΔ : ∀ (i : ι) (x : E), ‖Laplacian.laplacian (χ i) x‖ ≤ C / R i ^ 2) {f : E → F} (hf : Filter.Tendsto f (Filter.cocompact E) (nhds 0)) : Filter.Tendsto (fun (i : ι) => ∫ (x : E), Laplacian.laplacian (χ i) x • f x ∂μ) l (nhds 0)

Laplacians of planar cutoffs against decaying functions. In a two-dimensional space, let the cutoffs χ i equal 1 near ball 0 (R i) and 0 near the complement of closedBall 0 (2 * R i), with |Δ χ i| ≤ C / (R i)² and R i → ∞. Then ∫ Δ χ i • f → 0 for every f tending to 0 at infinity, since ∫ |Δ χ i| is bounded uniformly in i.