@[reducible, inline]

noncomputable abbrev ConvolutionSmooth.mulBilin : ℂ →L[ℝ] ℂ →L[ℝ] ℂ

The complex multiplication bilinear map ℂ × ℂ → ℂ viewed as an ℝ-bilinear continuous map; used as the bilinear pairing for convolutions in this file.

noncomputable def ConvolutionSmooth.c0ConvSchwartz {n : ℕ} (v : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) : EuclideanSpace ℝ (Fin n) → ℂ

The convolution v ⋆ ψ of a C₀ function v (continuous, vanishing at infinity) with a Schwartz function ψ, as a function on Euclidean space.

theorem ConvolutionSmooth.hasFDerivAt_convolution_bdd_schwartz {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] (L : ℂ →L[ℝ] F →L[ℝ] G) (v : EuclideanSpace ℝ (Fin n) → ℂ) (hv_bdd : BddAbove (Set.range fun (x : EuclideanSpace ℝ (Fin n)) => ‖v x‖)) (hv_cont : Continuous v) (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) F) (x₀ : EuclideanSpace ℝ (Fin n)) : HasFDerivAt (MeasureTheory.convolution v (⇑ψ) L MeasureTheory.volume) (MeasureTheory.convolution v (fun (y : EuclideanSpace ℝ (Fin n)) => fderiv ℝ (⇑ψ) y) (ContinuousLinearMap.precompR (EuclideanSpace ℝ (Fin n)) L) MeasureTheory.volume x₀) x₀

The convolution of a bounded continuous function v with a Schwartz function ψ, using a bilinear pairing L, is differentiable, and its Fréchet derivative is the convolution of v with the derivative fderiv ψ. Step toward Melrose's Prop. 8.1.

theorem ConvolutionSmooth.contDiff_convolution_bdd_schwartz {n : ℕ} {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℝ F] {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] (L : ℂ →L[ℝ] F →L[ℝ] G) (v : EuclideanSpace ℝ (Fin n) → ℂ) (hv_bdd : BddAbove (Set.range fun (x : EuclideanSpace ℝ (Fin n)) => ‖v x‖)) (hv_cont : Continuous v) (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) F) (k : ℕ) : ContDiff ℝ (↑k) (MeasureTheory.convolution v (⇑ψ) L MeasureTheory.volume)

The convolution of a bounded continuous function v with a Schwartz function ψ, using a bilinear pairing L, is Cᵏ for every k : ℕ. Iterates the FDeriv lemma.

theorem ConvolutionSmooth.convolution_c0_schwartz_contDiff {n : ℕ} (v : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (k : ℕ) : ContDiff ℝ (↑k) (c0ConvSchwartz v ψ)

The convolution of a C₀ function v with a Schwartz function ψ is Cᵏ for every k : ℕ. Specialisation of contDiff_convolution_bdd_schwartz to mulBilin.

theorem ConvolutionSmooth.tendsto_sub_cocompact {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [ProperSpace E] (t : E) : Filter.Tendsto (fun (x : E) => x - t) (Filter.cocompact E) (Filter.cocompact E)

Translation x ↦ x - t is a proper map on a finite-dimensional normed space, so it pushes the cocompact filter to itself.

instance ConvolutionSmooth.cocompact_isCountablyGenerated (d : ℕ) : (Filter.cocompact (EuclideanSpace ℝ (Fin d))).IsCountablyGenerated

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

theorem ConvolutionSmooth.tendsto_convolution_bdd_schwartz_zero {n : ℕ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (L : ℂ →L[ℝ] F →L[ℝ] G) (v : EuclideanSpace ℝ (Fin n) → ℂ) (hv_bdd : BddAbove (Set.range fun (x : EuclideanSpace ℝ (Fin n)) => ‖v x‖)) (hv_cont : Continuous v) (hv_zero : Filter.Tendsto v (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)) (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) F) : Filter.Tendsto (MeasureTheory.convolution v (⇑ψ) L MeasureTheory.volume) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

If a bounded continuous function v vanishes at infinity, then its convolution with a Schwartz function ψ (via a bilinear pairing L) vanishes at infinity.

theorem ConvolutionSmooth.iteratedFDeriv_convolution_bdd_schwartz_zeroAtInfty {n : ℕ} {F : Type u_1} {G : Type u_2} [NormedAddCommGroup F] [NormedSpace ℝ F] [NormedAddCommGroup G] [NormedSpace ℝ G] (L : ℂ →L[ℝ] F →L[ℝ] G) (v : EuclideanSpace ℝ (Fin n) → ℂ) (hv_bdd : BddAbove (Set.range fun (x : EuclideanSpace ℝ (Fin n)) => ‖v x‖)) (hv_cont : Continuous v) (hv_zero : Filter.Tendsto v (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)) (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) F) (m : ℕ) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ‖iteratedFDeriv ℝ m (MeasureTheory.convolution v (⇑ψ) L MeasureTheory.volume) x‖) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

Every iterated Fréchet derivative of the convolution v ⋆ ψ (for v bounded continuous, vanishing at infinity, and ψ Schwartz) tends to zero at infinity.

theorem ConvolutionSmooth.convolution_c0_schwartz_iteratedFDeriv_zeroAtInfty {n : ℕ} (v : ZeroAtInftyContinuousMap (EuclideanSpace ℝ (Fin n)) ℂ) (ψ : SchwartzMap (EuclideanSpace ℝ (Fin n)) ℂ) (m : ℕ) : Filter.Tendsto (fun (x : EuclideanSpace ℝ (Fin n)) => ‖iteratedFDeriv ℝ m (c0ConvSchwartz v ψ) x‖) (Filter.cocompact (EuclideanSpace ℝ (Fin n))) (nhds 0)

Every iterated derivative of the convolution v ⋆ ψ of a C₀ function v with a Schwartz function ψ tends to zero at infinity.