Total variation of a convolution

Convolving with an integrable kernel ρ averages the translates u (· - t) of a function with weights ρ t. Each translate has total variation at most |Du|(Ω) on an open set Ω' with Ω' - tsupport ρ ⊆ Ω, so the convolution satisfies the convolution estimate

|D(ρ ⋆ u)|(Ω') ≤ ‖ρ‖₁ |Du|(Ω).

For a normalized smooth bump the factor ‖ρ‖₁ is one. On the whole space the estimate combines with lower semicontinuity under L¹_loc convergence: the variations of the mollifications of a locally integrable function converge to its variation. Since a mollification is smooth, its variation is the integral of the norm of its gradient. Thus every locally integrable function u on the whole space satisfies |Du|(E) = lim ∫ ‖∇(ρ_ε ⋆ u)‖, where |Du|(E) is the variational supremum TauCeti.totalVariationOn, finite or infinite. For integrable u the mollifications also converge to u in L¹ (TauCeti.tendsto_eLpNorm_normed_convolution_sub), so they are a strict approximation of u by smooth functions on the whole space.

The convolution estimate holds for every s-finite right-invariant measure. The limit statements use an additive Haar measure, against which the normalized bumps have integral one.

Main results

• TauCeti.totalVariationOn_convolution_le: the convolution estimate |D(ρ ⋆ u)|(Ω') ≤ ‖ρ‖₁ |Du|(Ω) when Ω' - tsupport ρ ⊆ Ω.
• ContDiffBump.totalVariationOn_normed_convolution_le: mollification by a normalized bump of outer radius r does not increase variation from Ω to any open set whose closed r-neighbourhood lies in Ω.
• TauCeti.exists_mollifier_seq_of_isCompact_closure: local smooth approximation with an eventual variation bound on an open set whose closure is a compact subset of the domain.
• TauCeti.tendsto_totalVariationOn_normed_convolution: on the whole space, the variations of mollifications with shrinking radii converge to the variation of the function.
• TauCeti.tendsto_lintegral_enorm_fderiv_normed_convolution: the same limit written as the integrals ∫ ‖∇(ρ_ε ⋆ u)‖ of the smooth mollifications.

References

• L. Ambrosio, N. Fusco, D. Pallara, Functions of Bounded Variation and Free Discontinuity Problems, §3.1.
• L. C. Evans, R. F. Gariepy, Measure Theory and Fine Properties of Functions, §5.2.2.

theorem TauCeti.totalVariationOn_convolution_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω Ω' : TopologicalSpace.Opens E} {u ρ : E → ℝ} [MeasureTheory.SFinite μ] [μ.IsAddRightInvariant] (hρ : MeasureTheory.Integrable ρ μ) (hρc : HasCompactSupport ρ) (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hΩ : ∀ t ∈ tsupport ρ, ∀ x ∈ Ω', x - t ∈ Ω) : totalVariationOn μ Ω' (MeasureTheory.convolution ρ u (ContinuousLinearMap.lsmul ℝ ℝ) μ) ≤ (∫⁻ (t : E), ‖ρ t‖ₑ ∂μ) * totalVariationOn μ Ω u

The convolution estimate for total variation. If ρ is integrable with compact support and every translate Ω' - t with t ∈ tsupport ρ lies in Ω, then convolving a function locally integrable on Ω with ρ gives |D(ρ ⋆ u)|(Ω') ≤ ‖ρ‖₁ |Du|(Ω).

theorem ContDiffBump.totalVariationOn_normed_convolution_le {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω Ω' : TopologicalSpace.Opens E} {u : E → ℝ} [μ.IsAddHaarMeasure] (φ : ContDiffBump 0) (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hΩ : ∀ x ∈ Ω', Metric.closedBall x φ.rOut ⊆ ↑Ω) : TauCeti.totalVariationOn μ Ω' (MeasureTheory.convolution (φ.normed μ) u (ContinuousLinearMap.lsmul ℝ ℝ) μ) ≤ TauCeti.totalVariationOn μ Ω u

Mollification does not increase variation. For a normalized smooth bump φ of outer radius r, if the closed ball of radius r about every point of Ω' lies in Ω, then |D(φ ⋆ u)|(Ω') ≤ |Du|(Ω) for every u locally integrable on Ω.

theorem TauCeti.exists_mollifier_seq_of_isCompact_closure {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {Ω Ω' : TopologicalSpace.Opens E} {u : E → ℝ} [μ.IsAddHaarMeasure] (hu : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ) (hc : IsCompact (closure ↑Ω')) (hsub : closure ↑Ω' ⊆ ↑Ω) : ∃ (w : ℕ → E → ℝ), (∀ (n : ℕ), ContDiff ℝ 1 (w n)) ∧ (∀ (A : Set E), IsCompact A → A ⊆ closure ↑Ω' → Filter.Tendsto (fun (n : ℕ) => ∫⁻ (x : E) in A, ‖w n x - u x‖ₑ ∂μ) Filter.atTop (nhds 0)) ∧ ∀ᶠ (n : ℕ) in Filter.atTop, totalVariationOn μ Ω' (w n) ≤ totalVariationOn μ Ω u

On an open set with compact closure inside Ω, a locally integrable function admits C¹ approximations converging in L¹ on each compact subset of that closure, with variation eventually bounded by its variation on Ω. The construction localizes the function to a compact neighbourhood before mollifying it, as in the scalar coarea proof.

theorem TauCeti.tendsto_totalVariationOn_normed_convolution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {u : E → ℝ} [μ.IsAddHaarMeasure] {ι : Type u_2} {l : Filter ι} {φ : ι → ContDiffBump 0} (hφ : Filter.Tendsto (fun (i : ι) => (φ i).rOut) l (nhds 0)) (hu : MeasureTheory.LocallyIntegrable u μ) : Filter.Tendsto (fun (i : ι) => totalVariationOn μ ⊤ (MeasureTheory.convolution ((φ i).normed μ) u (ContinuousLinearMap.lsmul ℝ ℝ) μ)) l (nhds (totalVariationOn μ ⊤ u))

Mollification approximates the variation on the whole space. For a locally integrable function u and normalized smooth bumps φ i whose outer radii tend to zero, the variations of the mollifications φ i ⋆ u on the whole space converge to the variation of u, finite or infinite.

theorem TauCeti.tendsto_lintegral_enorm_fderiv_normed_convolution {E : Type u_1} [NormedAddCommGroup E] [InnerProductSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} {u : E → ℝ} [μ.IsAddHaarMeasure] {ι : Type u_2} {l : Filter ι} {φ : ι → ContDiffBump 0} (hφ : Filter.Tendsto (fun (i : ι) => (φ i).rOut) l (nhds 0)) (hu : MeasureTheory.LocallyIntegrable u μ) : Filter.Tendsto (fun (i : ι) => ∫⁻ (x : E), ‖fderiv ℝ (MeasureTheory.convolution ((φ i).normed μ) u (ContinuousLinearMap.lsmul ℝ ℝ) μ) x‖ₑ ∂μ) l (nhds (totalVariationOn μ ⊤ u))

The variation as a limit of gradient integrals. For a locally integrable function u on the whole space and normalized smooth bumps φ i whose outer radii tend to zero, the integrals ∫ ‖∇(φ i ⋆ u)‖ of the smooth mollifications converge to the variation |Du|(E), finite or infinite.