Regularization of distributions

For a distribution T on an open set Ω and a test function ρ, the regularization T.translatePairing ρ is the function x ↦ T (ρ (· - x)), defined at every x for which the translate ρ (· - x) is supported in Ω; it is the convolution of T with the reflection ρ (- ·) of ρ. This file shows that it is smooth on the open set of such x, with derivatives given by the distributional derivatives of T:

∂_v (x ↦ T (ρ (· - x))) = x ↦ (∂_v T) (ρ (· - x)).

Consequently, if every distributional derivative of T vanishes, the regularization is constant on each preconnected open set of admissible translations. This is the regularization step in the classical proof that a distribution whose derivatives all vanish on a connected open set is a constant multiple of Lebesgue measure. The admissible translations form an open set by IsCompact.isOpen_setOf_mapsTo_add, since ρ has compact support.

Integrating the regularization against an integrable compactly supported function f gives T applied to the convolution f ⋆ ρ, so regularizations recover T as the kernel ρ shrinks. This commutes T with an integral of test functions. On tests supported in a fixed compact set, T is bounded by finitely many derivatives, hence by the sup norm of a jet with values in a Banach space; by Hahn–Banach each scalar functional of T extends continuously to that space, where it commutes with the Bochner integral.

Differentiability rests on the finite order of a distribution on each compact set, Distribution.exists_norm_apply_le from TauCeti.Analysis.Distribution.Order: the first-order Taylor remainder of x ↦ ρ (· - x) is supported in a fixed compact set and all of its derivatives are o(‖h‖) uniformly, so its image under T is o(‖h‖) as well.

Main declarations

• Distribution.translatePairing: the regularization x ↦ T (ρ (· - x)).
• Distribution.fderiv_translatePairing_apply: the derivative identity.
• Distribution.contDiffOn_translatePairing: the regularization is smooth.
• Distribution.translatePairing_eq_of_lineDerivOp_eq_zero: if all derivatives of T vanish, the regularization is constant on preconnected open sets of admissible translations.
• Distribution.apply_eq_integral_smul_translatePairing: pairing the regularization with an integrable compactly supported f is T applied to the convolution f ⋆ ρ, T (f ⋆ ρ) = ∫ f y • T (ρ (· - y)) dy.

References

• [L. Hörmander, The Analysis of Linear Partial Differential Operators I][hormander2003], §2.1 for the local order estimate and Theorem 4.1.1 for the smoothness of regularizations and their derivatives.

noncomputable def Distribution.translatePairing {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} (T : Distribution Ω F ⊤) (ρ : TestFunction V ℝ ⊤) (x : E) : F

The regularization of a distribution T by a test function ρ: the function x ↦ T (ρ (· - x)). Its value at x is T applied to the translate of ρ by x when this translate is supported in Ω, and 0 otherwise. It is the convolution of T with the reflection ρ (- ·) of ρ.

theorem Distribution.translatePairing_eq {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} (T : Distribution Ω F ⊤) {ρ : TestFunction V ℝ ⊤} {x : E} {φ : TestFunction Ω ℝ ⊤} (hφ : ∀ (y : E), φ y = ρ (y - x)) : T.translatePairing ρ x = T φ

The regularization at x is T applied to any test function on Ω which is the translate of ρ by x.

theorem Distribution.translatePairing_eq_zero_of_not_mapsTo {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} (T : Distribution Ω F ⊤) {ρ : TestFunction V ℝ ⊤} {x : E} (h : ¬Set.MapsTo (fun (x_1 : E) => x_1 + x) (tsupport ⇑ρ) ↑Ω) : T.translatePairing ρ x = 0

The regularization vanishes where the translate of ρ is not supported in Ω.

@[simp]

theorem Distribution.translatePairing_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} (ρ : TestFunction V ℝ ⊤) : translatePairing 0 ρ = 0

The regularization of the zero distribution vanishes.

@[simp]

theorem Distribution.translatePairing_zero_kernel {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} (T : Distribution Ω F ⊤) : T.translatePairing 0 = 0

The regularization by the zero test function vanishes.

@[simp]

theorem Distribution.translatePairing_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} (T S : Distribution Ω F ⊤) (ρ : TestFunction V ℝ ⊤) : (T + S).translatePairing ρ = T.translatePairing ρ + S.translatePairing ρ

Regularization is additive in the distribution.

@[simp]

theorem Distribution.translatePairing_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} {M : Type u_3} [Monoid M] [DistribMulAction M F] [SMulCommClass ℝ M F] [ContinuousConstSMul M F] (c : M) (T : Distribution Ω F ⊤) (ρ : TestFunction V ℝ ⊤) : (c • T).translatePairing ρ = c • T.translatePairing ρ

Regularization commutes with scalar multiplication of the distribution.

theorem Distribution.differentiableAt_translatePairing {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} (T : Distribution Ω F ⊤) (ρ : TestFunction V ℝ ⊤) {x : E} (hx : Set.MapsTo (fun (x_1 : E) => x_1 + x) (tsupport ⇑ρ) ↑Ω) : DifferentiableAt ℝ (T.translatePairing ρ) x

The regularization is differentiable at every admissible translation.

theorem Distribution.fderiv_translatePairing_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} (T : Distribution Ω F ⊤) (ρ : TestFunction V ℝ ⊤) {x : E} (hx : Set.MapsTo (fun (x_1 : E) => x_1 + x) (tsupport ⇑ρ) ↑Ω) (v : E) : (fderiv ℝ (T.translatePairing ρ) x) v = (LineDeriv.lineDerivOp v T).translatePairing ρ x

The derivative of a regularization. At every admissible translation, the derivative of x ↦ T (ρ (· - x)) in the direction v is the regularization of the distributional derivative ∂_{v} T.

theorem Distribution.contDiffOn_translatePairing {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} (T : Distribution Ω F ⊤) (ρ : TestFunction V ℝ ⊤) : ContDiffOn ℝ (↑⊤) (T.translatePairing ρ) {x : E | Set.MapsTo (fun (x_1 : E) => x_1 + x) (tsupport ⇑ρ) ↑Ω}

Regularizations are smooth. The regularization x ↦ T (ρ (· - x)) is smooth on the open set of translations for which ρ (· - x) is supported in Ω.

theorem Distribution.translatePairing_eq_of_lineDerivOp_eq_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} {T : Distribution Ω F ⊤} (hT : ∀ (v : E), LineDeriv.lineDerivOp v T = 0) (ρ : TestFunction V ℝ ⊤) {U : Set E} (hUo : IsOpen U) (hUc : IsPreconnected U) (hU : ∀ x ∈ U, Set.MapsTo (fun (x_1 : E) => x_1 + x) (tsupport ⇑ρ) ↑Ω) {x y : E} (hx : x ∈ U) (hy : y ∈ U) : T.translatePairing ρ x = T.translatePairing ρ y

Distributions with vanishing derivatives have locally constant regularizations. If every directional derivative of T vanishes, then x ↦ T (ρ (· - x)) is constant on every preconnected open set of translations for which ρ (· - x) is supported in Ω.

theorem Distribution.apply_eq_integral_smul_translatePairing {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω V : TopologicalSpace.Opens E} [FiniteDimensional ℝ E] [CompleteSpace F] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [MeasureTheory.SFinite μ] [μ.IsAddLeftInvariant] (T : Distribution Ω F ⊤) (ρ : TestFunction V ℝ ⊤) {f : E → ℝ} (hf : MeasureTheory.Integrable f μ) (hfc : HasCompactSupport f) (hfρ : ∀ y ∈ tsupport f, Set.MapsTo (fun (x : E) => x + y) (tsupport ⇑ρ) ↑Ω) {ψ : TestFunction Ω ℝ ⊤} (hψ : ⇑ψ = MeasureTheory.convolution f (⇑ρ) (ContinuousLinearMap.lsmul ℝ ℝ) μ) : T ψ = ∫ (y : E), f y • T.translatePairing ρ y ∂μ

A distribution passes under a convolution integral. Let ψ be a test function which is the convolution f ⋆ ρ, ψ x = ∫ f y * ρ (x - y) ∂μ(y), of an integrable compactly supported f with a test function ρ whose translates by the points of tsupport f are supported in Ω. Then T ψ is the integral of the regularization against f:

T ψ = ∫ f y • T (ρ (· - y)) ∂μ(y).

Pairing the regularization of T with a test function is therefore pairing T with a convolution, which is how regularizations recover a distribution as the kernel shrinks.