Compact support approximation in Schwartz space

Multiplying a Schwartz function by the fixed smooth cutoff at radius R gives a compactly supported Schwartz function. Each seminorm of its error is bounded by a fixed constant divided by R. Consequently compactly supported Schwartz functions are dense, and continuous identities extend from compact tests.

noncomputable def NavierStokesR3.SchwartzCompactApproximation.truncate (ψ : SchwartzMap ProblemStatement.Space ℂ) (R : ℝ) (hR : 0 < R) : SchwartzMap ProblemStatement.Space ℂ

Multiplication by a compactly supported smooth cutoff.

Equations

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

@[simp]

theorem NavierStokesR3.SchwartzCompactApproximation.truncate_apply (ψ : SchwartzMap ProblemStatement.Space ℂ) (R : ℝ) (hR : 0 < R) (x : ProblemStatement.Space) : (truncate ψ R hR) x = ComparisonCutoffs.cutoff R x • ψ x

theorem NavierStokesR3.SchwartzCompactApproximation.truncate_hasCompactSupport (ψ : SchwartzMap ProblemStatement.Space ℂ) (R : ℝ) (hR : 0 < R) : HasCompactSupport ⇑(truncate ψ R hR)

theorem NavierStokesR3.SchwartzCompactApproximation.weighted_tail_le (ψ : SchwartzMap ProblemStatement.Space ℂ) {R : ℝ} (hR : 0 < R) (k m : ℕ) {x : ProblemStatement.Space} (hx : R ≤ ‖x‖) : ‖x‖ ^ k * ‖iteratedFDeriv ℝ m (⇑ψ) x‖ ≤ (SchwartzMap.seminorm ℂ (k + 1) m) ψ / R

One extra power in a Schwartz seminorm gives a uniform tail estimate.

theorem NavierStokesR3.SchwartzCompactApproximation.uniform_cutoff_derivative_bound {R : ℝ} (hR : 0 < R) (hRone : 1 ≤ R) (m : ℕ) (x : ProblemStatement.Space) : ‖iteratedFDeriv ℝ m (ComparisonCutoffs.cutoff R) x‖ ≤ ComparisonCutoffs.derivativeConstant m

All derivatives of the cutoffs are bounded uniformly for radii at least one.

noncomputable def NavierStokesR3.SchwartzCompactApproximation.productTailBound (ψ : SchwartzMap ProblemStatement.Space ℂ) (k m : ℕ) : ℝ

The fixed constant in the product's weighted tail estimate.

Equations

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

theorem NavierStokesR3.SchwartzCompactApproximation.productTailBound_nonneg (ψ : SchwartzMap ProblemStatement.Space ℂ) (k m : ℕ) : 0 ≤ productTailBound ψ k m

noncomputable def NavierStokesR3.SchwartzCompactApproximation.errorTailBound (ψ : SchwartzMap ProblemStatement.Space ℂ) (k m : ℕ) : ℝ

The fixed constant controlling the cutoff error.

Equations

• NavierStokesR3.SchwartzCompactApproximation.errorTailBound ψ k m = NavierStokesR3.SchwartzCompactApproximation.productTailBound ψ k m + (SchwartzMap.seminorm ℂ (k + 1) m) ψ

theorem NavierStokesR3.SchwartzCompactApproximation.errorTailBound_nonneg (ψ : SchwartzMap ProblemStatement.Space ℂ) (k m : ℕ) : 0 ≤ errorTailBound ψ k m

theorem NavierStokesR3.SchwartzCompactApproximation.truncate_weighted_derivative_le (ψ : SchwartzMap ProblemStatement.Space ℂ) {R : ℝ} (hR : 0 < R) (hRone : 1 ≤ R) (k m : ℕ) {x : ProblemStatement.Space} (hx : R ≤ ‖x‖) : ‖x‖ ^ k * ‖iteratedFDeriv ℝ m (⇑(truncate ψ R hR)) x‖ ≤ productTailBound ψ k m / R

The Leibniz estimate for the cutoff product on the spatial tail.

theorem NavierStokesR3.SchwartzCompactApproximation.truncate_error_weighted_le (ψ : SchwartzMap ProblemStatement.Space ℂ) {R : ℝ} (hR : 0 < R) (hRone : 1 ≤ R) (k m : ℕ) (x : ProblemStatement.Space) : ‖x‖ ^ k * ‖iteratedFDeriv ℝ m (⇑(truncate ψ R hR - ψ)) x‖ ≤ errorTailBound ψ k m / R

The cutoff error vanishes locally inside the plateau and is small outside it.

theorem NavierStokesR3.SchwartzCompactApproximation.seminorm_truncate_sub_le (ψ : SchwartzMap ProblemStatement.Space ℂ) {R : ℝ} (hR : 0 < R) (hRone : 1 ≤ R) (k m : ℕ) : (SchwartzMap.seminorm ℂ k m) (truncate ψ R hR - ψ) ≤ errorTailBound ψ k m / R

Every Schwartz seminorm of the cutoff error tends to zero at rate 1/R.

noncomputable def NavierStokesR3.SchwartzCompactApproximation.approximate (ψ : SchwartzMap ProblemStatement.Space ℂ) (n : ℕ) : SchwartzMap ProblemStatement.Space ℂ

A sequence of compactly supported smooth approximations.

Equations

• NavierStokesR3.SchwartzCompactApproximation.approximate ψ n = NavierStokesR3.SchwartzCompactApproximation.truncate ψ (↑n + 1) ⋯

@[simp]

theorem NavierStokesR3.SchwartzCompactApproximation.approximate_apply (ψ : SchwartzMap ProblemStatement.Space ℂ) (n : ℕ) (x : ProblemStatement.Space) : (approximate ψ n) x = ComparisonCutoffs.cutoff (↑n + 1) x • ψ x

theorem NavierStokesR3.SchwartzCompactApproximation.approximate_hasCompactSupport (ψ : SchwartzMap ProblemStatement.Space ℂ) (n : ℕ) : HasCompactSupport ⇑(approximate ψ n)

theorem NavierStokesR3.SchwartzCompactApproximation.tendsto_approximate (ψ : SchwartzMap ProblemStatement.Space ℂ) : Filter.Tendsto (approximate ψ) Filter.atTop (nhds ψ)

The cutoff approximations converge in the full Schwartz topology.

theorem NavierStokesR3.SchwartzCompactApproximation.dense_hasCompactSupport : Dense {ψ : SchwartzMap ProblemStatement.Space ℂ | HasCompactSupport ⇑ψ}

Compactly supported smooth tests are dense in Schwartz space.

theorem NavierStokesR3.SchwartzCompactApproximation.continuous_zero_of_compactSupport (F : SchwartzMap ProblemStatement.Space ℂ → ℂ) (hF : Continuous F) (hzero : ∀ (ψ : SchwartzMap ProblemStatement.Space ℂ), HasCompactSupport ⇑ψ → F ψ = 0) (ψ : SchwartzMap ProblemStatement.Space ℂ) : F ψ = 0

A continuous functional vanishing on compact tests vanishes on every Schwartz test.

theorem NavierStokesR3.SchwartzCompactApproximation.eq_zero_of_compactSupport (F : SchwartzMap ProblemStatement.Space ℂ →L[ℂ] ℂ) (hzero : ∀ (ψ : SchwartzMap ProblemStatement.Space ℂ), HasCompactSupport ⇑ψ → F ψ = 0) (ψ : SchwartzMap ProblemStatement.Space ℂ) : F ψ = 0

The continuous linear form version of compact-test extension.

theorem NavierStokesR3.SchwartzCompactApproximation.comp_eq_zero_of_compactSupport (F : SchwartzMap ProblemStatement.Space ℂ →L[ℂ] ℂ) (L : SchwartzMap ProblemStatement.Space ℂ →L[ℂ] SchwartzMap ProblemStatement.Space ℂ) (hzero : ∀ (ψ : SchwartzMap ProblemStatement.Space ℂ), HasCompactSupport ⇑ψ → F (L ψ) = 0) (ψ : SchwartzMap ProblemStatement.Space ℂ) : F (L ψ) = 0

In particular, an identity tested after a continuous differential operator extends.