Documentation

TauCeti.Analysis.Distribution.TestFunction.Convolution

Mollification in the test-function topology #

A test function may be convolved with a normalized smooth bump whenever the enlarged support stays inside its open domain. Every derivative commutes with this operation. For shrinking bumps, the mollifications converge in the native LF topology, so every distribution can be evaluated along this approximation.

The codomain is any real Banach space, including the finite-dimensional spaces of alternating forms used to test currents in coordinates.

References #

source
noncomputable def TestFunction.mollify {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (ρ : ContDiffBump 0) (h : Metric.closedBall 0 ρ.rOut + tsupport ⇑φ ⊆ ↑Ω) :
TestFunction Ω F ⊤

Mollify a test function by a normalized bump whose support enlargement stays in Ω.

Instances For
    source
    @[simp]
    theorem TestFunction.coe_mollify {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (ρ : ContDiffBump 0) (h : Metric.closedBall 0 ρ.rOut + tsupport ⇑φ ⊆ ↑Ω) :
    ⇑(φ.mollify μ ρ h) = MeasureTheory.convolution (ρ.normed μ) (⇑φ) (ContinuousLinearMap.lsmul ℝ ℝ) μ

    A mollified test function is the usual normalized-bump convolution.

    source
    theorem TestFunction.mollify_apply {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (ρ : ContDiffBump 0) (h : Metric.closedBall 0 ρ.rOut + tsupport ⇑φ ⊆ ↑Ω) (x : E) :
    (φ.mollify μ ρ h) x = MeasureTheory.convolution (ρ.normed μ) (⇑φ) (ContinuousLinearMap.lsmul ℝ ℝ) μ x

    Evaluation of a mollified test function is the usual normalized-bump convolution.

    source
    @[simp]
    theorem TestFunction.mollify_zero {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (ρ : ContDiffBump 0) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (h : Metric.closedBall 0 ρ.rOut + tsupport ⇑0 ⊆ ↑Ω) :
    mollify 0 μ ρ h = 0

    Mollifying the zero test function gives zero.

    source
    theorem TestFunction.mollify_add {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ ψ : TestFunction Ω F ⊤) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (ρ : ContDiffBump 0) (hφ : Metric.closedBall 0 ρ.rOut + tsupport ⇑φ ⊆ ↑Ω) (hψ : Metric.closedBall 0 ρ.rOut + tsupport ⇑ψ ⊆ ↑Ω) (h : Metric.closedBall 0 ρ.rOut + tsupport ⇑(φ + ψ) ⊆ ↑Ω) :
    (φ + ψ).mollify μ ρ h = φ.mollify μ ρ hφ + ψ.mollify μ ρ hψ

    Mollification is additive whenever all three support enlargements stay in the domain.

    source
    theorem TestFunction.mollify_smul {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (c : ℝ) (ρ : ContDiffBump 0) (hφ : Metric.closedBall 0 ρ.rOut + tsupport ⇑φ ⊆ ↑Ω) (h : Metric.closedBall 0 ρ.rOut + tsupport ⇑(c • φ) ⊆ ↑Ω) :
    (c • φ).mollify μ ρ h = c • φ.mollify μ ρ hφ

    Mollification commutes with real scalar multiplication.

    source
    theorem TestFunction.iteratedFDeriv_mollify {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} (φ : TestFunction Ω F ⊤) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] (ρ : ContDiffBump 0) (h : Metric.closedBall 0 ρ.rOut + tsupport ⇑φ ⊆ ↑Ω) (n : ℕ) :
    iteratedFDeriv ℝ n ⇑(φ.mollify μ ρ h) = MeasureTheory.convolution (ρ.normed μ) (iteratedFDeriv ℝ n ⇑φ) (ContinuousLinearMap.lsmul ℝ ℝ) μ

    Every Fréchet derivative commutes with mollification of test functions.

    source
    theorem TestFunction.tendsto_mollify {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {Ω : TopologicalSpace.Opens E} [CompleteSpace F] {ι : Type u_3} {l : Filter ι} (φ : TestFunction Ω F ⊤) (μ : MeasureTheory.Measure E) [μ.IsAddHaarMeasure] {ρ : ι → ContDiffBump 0} (hρ : Filter.Tendsto (fun (i : ι) => (ρ i).rOut) l (nhds 0)) (h : ∀ (i : ι), Metric.closedBall 0 (ρ i).rOut + tsupport ⇑φ ⊆ ↑Ω) :
    Filter.Tendsto (fun (i : ι) => φ.mollify μ (ρ i) ⋯) l (nhds φ)

    Shrinking normalized bumps approximate a test function in its LF topology whenever the closed rOut-enlargement of tsupport φ stays inside Ω for every index.