Expanding ordinary-space cutoffs and their actual first derivative controls.

noncomputable def EulerLpTranslation.cutoff (n : ℕ) (x : EulerSmoothLimit.Space) : ℝ

Cutoff, given by spatialBump (cutoffScale n • x).

Equations

• EulerLpTranslation.cutoff n x = ↑EulerNoncompactTransport.spatialBump (EulerNoncompactTransport.cutoffScale n • x)

theorem EulerLpTranslation.cutoff_smooth (n : ℕ) : ContDiff ℝ (↑⊤) (cutoff n)

theorem EulerLpTranslation.cutoff_compact (n : ℕ) : HasCompactSupport (cutoff n)

theorem EulerLpTranslation.cutoff_bounds (n : ℕ) (x : EulerSmoothLimit.Space) : 0 ≤ cutoff n x ∧ cutoff n x ≤ 1

theorem EulerLpTranslation.cutoff_sub_one_norm (n : ℕ) (x : EulerSmoothLimit.Space) : ‖cutoff n x - 1‖ ≤ 1

theorem EulerLpTranslation.cutoff_tendsto (x : EulerSmoothLimit.Space) : Filter.Tendsto (fun (n : ℕ) => cutoff n x) Filter.atTop (nhds 1)

theorem EulerLpTranslation.cutoff_derivative_bound : ∃ (M : ℝ), 0 ≤ M ∧ ∀ (n : ℕ) (x : EulerSmoothLimit.Space), ‖fderiv ℝ (cutoff n) x‖ ≤ M * EulerNoncompactTransport.cutoffScale n

theorem EulerLpTranslation.cutoff_derivative_tendsto (x : EulerSmoothLimit.Space) : Filter.Tendsto (fun (n : ℕ) => fderiv ℝ (cutoff n) x) Filter.atTop (nhds 0)

noncomputable def EulerLpTranslation.cutoffField {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (n : ℕ) (x : EulerSmoothLimit.Space) : V

Cutoff field, given by cutoff n x • f x.

Equations

• EulerLpTranslation.cutoffField f n x = EulerLpTranslation.cutoff n x • f x

theorem EulerLpTranslation.cutoffField_smooth {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) : ContDiff ℝ (↑⊤) (cutoffField f n)

theorem EulerLpTranslation.cutoffField_compact {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (n : ℕ) : HasCompactSupport (cutoffField f n)

theorem EulerLpTranslation.cutoffField_fderiv {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (n : ℕ) (x : EulerSmoothLimit.Space) : fderiv ℝ (cutoffField f n) x = cutoff n x • fderiv ℝ f x + (fderiv ℝ (cutoff n) x).smulRight (f x)

theorem EulerLpTranslation.cutoffField_tendsto {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (x : EulerSmoothLimit.Space) : Filter.Tendsto (fun (n : ℕ) => cutoffField f n x) Filter.atTop (nhds (f x))

theorem EulerLpTranslation.cutoffField_fderiv_tendsto {V : Type u_1} [NormedAddCommGroup V] [NormedSpace ℝ V] (f : EulerSmoothLimit.Space → V) (hf : ContDiff ℝ (↑⊤) f) (x : EulerSmoothLimit.Space) : Filter.Tendsto (fun (n : ℕ) => fderiv ℝ (cutoffField f n) x) Filter.atTop (nhds (fderiv ℝ f x))