The dilated radius-1-to-2 bump cutoff

This family supports localization arguments in real inner-product spaces: one fixed ContDiffBump that equals one on the closed unit ball and vanishes outside the ball of radius two, dilated to cutoff E R x = χ (R⁻¹ • x). Because every member of the family is a dilation of the same bump, its derivative bounds have R-independent constants: ‖iteratedFDeriv ℝ n (cutoff E R) x‖ ≤ derivativeConstant E n / R ^ n, and the scale-invariant ‖fderiv ℝ (cutoff E R) x‖ * ‖x‖ ≤ 2 * derivativeConstant E 1.

The space is an explicit argument of the definitions so that partial applications such as cutoff E R elaborate without an expected type. The derivative constant is accessed through its positivity and bound lemmas; its choice is private.

def NavierStokesAndEuler.SmoothCutoff.baseBump (E : Type u_1) [NormedAddCommGroup E] : ContDiffBump 0

The fixed bump with inner radius one and outer radius two.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def NavierStokesAndEuler.SmoothCutoff.baseCutoff (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : ℝ

The unscaled cutoff.

Equations

• NavierStokesAndEuler.SmoothCutoff.baseCutoff E x = ↑(NavierStokesAndEuler.SmoothCutoff.baseBump E) x

noncomputable def NavierStokesAndEuler.SmoothCutoff.cutoff (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] (R : ℝ) (x : E) : ℝ

The cutoff at spatial radius R; its estimates are stated for 0 < R.

Equations

• NavierStokesAndEuler.SmoothCutoff.cutoff E R x = NavierStokesAndEuler.SmoothCutoff.baseCutoff E (R⁻¹ • x)

theorem NavierStokesAndEuler.SmoothCutoff.baseCutoff_smooth {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] : ContDiff ℝ (↑⊤) (baseCutoff E)

theorem NavierStokesAndEuler.SmoothCutoff.baseCutoff_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : 0 ≤ baseCutoff E x

theorem NavierStokesAndEuler.SmoothCutoff.baseCutoff_le_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : baseCutoff E x ≤ 1

theorem NavierStokesAndEuler.SmoothCutoff.baseCutoff_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} (hx : ‖x‖ ≤ 1) : baseCutoff E x = 1

theorem NavierStokesAndEuler.SmoothCutoff.baseCutoff_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {x : E} (hx : 2 ≤ ‖x‖) : baseCutoff E x = 0

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_smooth {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (R : ℝ) : ContDiff ℝ (↑⊤) (cutoff E R)

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_nonneg {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (R : ℝ) (x : E) : 0 ≤ cutoff E R x

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_le_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (R : ℝ) (x : E) : cutoff E R x ≤ 1

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_mem_Icc {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (R : ℝ) (x : E) : cutoff E R x ∈ Set.Icc 0 1

theorem NavierStokesAndEuler.SmoothCutoff.norm_cutoff_le_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (R : ℝ) (x : E) : ‖cutoff E R x‖ ≤ 1

theorem NavierStokesAndEuler.SmoothCutoff.norm_inv_smul {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {R : ℝ} (hR : 0 < R) (x : E) : ‖R⁻¹ • x‖ = ‖x‖ / R

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {R : ℝ} (hR : 0 < R) {x : E} (hx : ‖x‖ ≤ R) : cutoff E R x = 1

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_eq_zero {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {R : ℝ} (hR : 0 < R) {x : E} (hx : 2 * R ≤ ‖x‖) : cutoff E R x = 0

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_support_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {R : ℝ} (hR : 0 < R) : Function.support (cutoff E R) ⊆ Metric.ball 0 (2 * R)

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_tsupport_subset {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {R : ℝ} (hR : 0 < R) : tsupport (cutoff E R) ⊆ Metric.closedBall 0 (2 * R)

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_eventuallyEq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {R : ℝ} (hR : 0 < R) {x : E} (hx : ‖x‖ < R) : cutoff E R =ᶠ[nhds x] 1

Near any point of the open ball of radius R the cutoff is identically one.

Plateaus

theorem NavierStokesAndEuler.SmoothCutoff.bounded_plateau {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : Set E} (hK : Bornology.IsBounded K) : ∃ R₀ > 0, ∀ R ≥ R₀, Set.EqOn (cutoff E R) (fun (x : E) => 1) K

Every bounded set lies in the plateau of all sufficiently large cutoffs.

theorem NavierStokesAndEuler.SmoothCutoff.eventually_bounded_plateau {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : Set E} (hK : Bornology.IsBounded K) : ∀ᶠ (R : ℝ) in Filter.atTop, Set.EqOn (cutoff E R) (fun (x : E) => 1) K

On a fixed bounded set the cutoffs eventually agree with the constant one.

theorem NavierStokesAndEuler.SmoothCutoff.compact_plateau {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : Set E} (hK : IsCompact K) : ∃ R₀ > 0, ∀ R ≥ R₀, Set.EqOn (cutoff E R) (fun (x : E) => 1) K

Every fixed compact set lies in the plateau of all sufficiently large cutoffs.

theorem NavierStokesAndEuler.SmoothCutoff.eventually_compact_plateau {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] {K : Set E} (hK : IsCompact K) : ∀ᶠ (R : ℝ) in Filter.atTop, Set.EqOn (cutoff E R) (fun (x : E) => 1) K

theorem NavierStokesAndEuler.SmoothCutoff.eventually_cutoff_eq_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : ∀ᶠ (R : ℝ) in Filter.atTop, cutoff E R x = 1

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_tendsto_one {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] (x : E) : Filter.Tendsto (fun (R : ℝ) => cutoff E R x) Filter.atTop (nhds 1)

Derivative bounds under dilation

theorem NavierStokesAndEuler.SmoothCutoff.iteratedFDeriv_comp_inv_smul_le {D : Type u_2} {F : Type u_3} [NormedAddCommGroup D] [NormedSpace ℝ D] [NormedAddCommGroup F] [NormedSpace ℝ F] {χ : D → F} {n : ℕ} (hχ : ContDiff ℝ (↑n) χ) {C : ℝ} (hC : ∀ (y : D), ‖iteratedFDeriv ℝ n χ y‖ ≤ C) {R : ℝ} (hR : 0 < R) (x : D) : ‖iteratedFDeriv ℝ n (fun (y : D) => χ (R⁻¹ • y)) x‖ ≤ C / R ^ n

Dilating a smooth function by R⁻¹ divides a uniform bound on its nth derivative by R ^ n.

Compact support

From here on the space is finite-dimensional, so the closed balls containing the supports are compact and every derivative of the bump is bounded.

theorem NavierStokesAndEuler.SmoothCutoff.baseCutoff_hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] : HasCompactSupport (baseCutoff E)

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_hasCompactSupport {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {R : ℝ} (hR : 0 < R) : HasCompactSupport (cutoff E R)

noncomputable def NavierStokesAndEuler.SmoothCutoff.derivativeConstant (E : Type u_1) [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (n : ℕ) : ℝ

A fixed positive bound for the nth derivative of the unscaled bump.

Equations

• NavierStokesAndEuler.SmoothCutoff.derivativeConstant E n = Classical.choose ⋯

theorem NavierStokesAndEuler.SmoothCutoff.derivativeConstant_pos {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (n : ℕ) : 0 < derivativeConstant E n

theorem NavierStokesAndEuler.SmoothCutoff.baseCutoff_iteratedFDeriv_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (baseCutoff E) x‖ ≤ derivativeConstant E n

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_iteratedFDeriv_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {R : ℝ} (hR : 0 < R) (n : ℕ) (x : E) : ‖iteratedFDeriv ℝ n (cutoff E R) x‖ ≤ derivativeConstant E n / R ^ n

Each spatial derivative contributes precisely one inverse power of the radius.

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_fderiv_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {R : ℝ} (hR : 0 < R) (x : E) : ‖fderiv ℝ (cutoff E R) x‖ ≤ derivativeConstant E 1 / R

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_second_fderiv_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {R : ℝ} (hR : 0 < R) (x : E) : ‖fderiv ℝ (fderiv ℝ (cutoff E R)) x‖ ≤ derivativeConstant E 2 / R ^ 2

theorem NavierStokesAndEuler.SmoothCutoff.cutoff_fderiv_mul_norm_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] {R : ℝ} (hR : 0 < R) (x : E) : ‖fderiv ℝ (cutoff E R) x‖ * ‖x‖ ≤ 2 * derivativeConstant E 1

The scale-invariant derivative bound: the gradient of cutoff E R is of size R⁻¹ and lives where ‖x‖ ≤ 2 R, so the product is bounded independently of R.