theorem ConvolutionDensity.integrable_one_add_norm_sub_rpow {n : ℕ} (x₀ : EuclideanSpace ℝ (Fin n)) : MeasureTheory.Integrable (fun (y : EuclideanSpace ℝ (Fin n)) => (1 + ‖x₀ - y‖) ^ (-(↑n + 1))) MeasureTheory.volume

The shifted Peetre weight y ↦ (1 + ‖x₀ - y‖)^{-(n+1)} is Lebesgue integrable on EuclideanSpace ℝ (Fin n).

theorem ConvolutionDensity.schwartz_norm_le_of_mem_ball {n : ℕ} (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) (EuclideanSpace ℝ (Fin n) →L[ℝ] ℂ)) (x₀ x y : EuclideanSpace ℝ (Fin n)) (hx : x ∈ Metric.ball x₀ 1) : ‖φ (x - y)‖ ≤ ((SchwartzMap.seminorm ℝ 0 0) φ + (SchwartzMap.seminorm ℝ (n + 1) 0) φ) * 3 ^ (n + 1) * (1 + ‖x₀ - y‖) ^ (-(↑n + 1))

Peetre-type bound for a derivative-valued Schwartz function: for x in the unit ball around x₀, the norm of φ(x - y) is bounded by C · (1 + ‖x₀ - y‖)^{-(n+1)} with C expressed in terms of the Schwartz seminorms of φ.

theorem ConvolutionDensity.schwartz_norm_le_of_mem_ball_gen {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] (φ : SchwartzMap (EuclideanSpace ℝ (Fin n)) F) (x₀ x y : EuclideanSpace ℝ (Fin n)) (hx : x ∈ Metric.ball x₀ 1) : ‖φ (x - y)‖ ≤ ((SchwartzMap.seminorm ℝ 0 0) φ + (SchwartzMap.seminorm ℝ (n + 1) 0) φ) * 3 ^ (n + 1) * (1 + ‖x₀ - y‖) ^ (-(↑n + 1))

Generic Peetre-type bound for a Schwartz function valued in an arbitrary normed space F: for x in the unit ball around x₀, ‖φ(x - y)‖ is bounded by C · (1 + ‖x₀ - y‖)^{-(n+1)} with C expressed in terms of Schwartz seminorms of φ.

theorem ConvolutionDensity.hasFDerivAt_smul_convolution_schwartz {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℂ F] [SMulCommClass ℝ ℂ F] [SecondCountableTopology F] (v : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) F) (x₀₀ : EuclideanSpace ℝ (Fin n)) : HasFDerivAt (fun (x : EuclideanSpace ℝ (Fin n)) => ∫ (y : EuclideanSpace ℝ (Fin n)), v y • ψ (x - y)) (∫ (y : EuclideanSpace ℝ (Fin n)), v y • ((SchwartzMap.fderivCLM ℝ (EuclideanSpace ℝ (Fin n)) F) ψ) (x₀₀ - y)) x₀₀

The smul-convolution x ↦ ∫ v(y) • ψ(x - y) dy of a C₀ function v with a Schwartz function ψ valued in F is Fréchet-differentiable at every x₀, with derivative given by differentiating under the integral sign.

theorem ConvolutionDensity.contDiff_smul_convolution_schwartz {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedSpace ℂ F] [SMulCommClass ℝ ℂ F] [SecondCountableTopology F] (v : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) F) (k : ℕ) : ContDiff ℝ ↑k fun (x : EuclideanSpace ℝ (Fin n)) => ∫ (y : EuclideanSpace ℝ (Fin n)), v y • ψ (x - y)

The smul-convolution x ↦ ∫ v(y) • ψ(x - y) dy of a C₀ function v with a Schwartz function ψ valued in F is Cᵏ for every natural number k.

theorem ConvolutionDensity.contDiff_convolution_zeroAtInfty_schwartz {n : ℕ} (v : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : ContDiff ℝ ↑⊤ fun (x : EuclideanSpace ℝ (Fin n)) => ∫ (y : EuclideanSpace ℝ (Fin n)), v y * ψ (x - y)

The convolution (v ⋆ ψ)(x) = ∫ v(y) ψ(x - y) dy of a C₀ function v with a complex-valued Schwartz function ψ is C^∞ (Melrose Prop. 8.1, smoothness part).

instance ConvolutionDensity.isCountablyGenerated_cocompact_euclidean {n : ℕ} : (Filter.cocompact (EuclideanSpace ℝ (Fin n))).IsCountablyGenerated

The cocompact filter on EuclideanSpace ℝ (Fin n) is countably generated, with complements of closed balls of integer radii as a basis.

theorem ConvolutionDensity.tendsto_convolution_zeroAtInfty_schwartz {n : ℕ} (v : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ∫ (y : EuclideanSpace ℝ (Fin n)), v y * ψ (x - y)) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

The convolution (v ⋆ ψ)(x) = ∫ v(y) ψ(x - y) dy of a C₀ function v with a Schwartz function ψ vanishes at infinity (Melrose Prop. 8.1, decay part).

theorem ConvolutionDensity.prop_8_1_smooth_zeroAtInfty {n : ℕ} (v : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : (ContDiff ℝ ↑⊤ fun (x : EuclideanSpace ℝ (Fin n)) => ∫ (y : EuclideanSpace ℝ (Fin n)), v y * ψ (x - y)) ∧ Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ∫ (y : EuclideanSpace ℝ (Fin n)), v y * ψ (x - y)) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

Melrose's Proposition 8.1: the convolution of a C₀ function with a Schwartz function is smooth and vanishes at infinity.