Uniform approximation by normalized bumps

Convolution with normalized smooth bumps whose radii tend to zero converges uniformly to any uniformly continuous Banach-valued function. For uniformly continuous functions, this upgrades the pointwise convergence of Mathlib's ContDiffBump.convolution_tendsto_right_of_continuous to uniform convergence, and allows simultaneous approximation of the derivatives of a compactly supported smooth function. Normalized-bump convolution also preserves a uniform bound on a function (ContDiffBump.norm_normed_convolution_le) and its Lipschitz constant, since it averages the differences of translates (ContDiffBump.dist_normed_convolution_le_of_dist_sub_le).

Along an arbitrary filter of bump indices, convolution with normalized bumps also converges uniformly on a neighbourhood filter of a point of continuity of the function.

The file also bounds the topological support of ρ.normed μ ⋆ g by the Minkowski sum closedBall 0 ρ.rOut + tsupport g, and provides the standard shrinking sequence of bumps ContDiffBump.shrinking, of radii R / (n + 1) and R / (2 * (n + 1)). These bumps are all rescalings of the first one (ContDiffBump.shrinking_apply_eq), so integrals against their normalized forms reduce to one kernel (ContDiffBump.integral_shrinking_normed_mul).

noncomputable def ContDiffBump.shrinking {X : Type u_1} {c : X} {R : ℝ} (hR : 0 < R) (n : ℕ) : ContDiffBump c

The bumps of outer radius R / (n + 1) and inner radius half of that. Their radii shrink to zero while the outer radius stays twice the inner one, as Lebesgue differentiation along normalized bump convolutions requires.

@[simp]

theorem ContDiffBump.rIn_shrinking {X : Type u_1} {c : X} {R : ℝ} (hR : 0 < R) (n : ℕ) : (shrinking hR n).rIn = R / (2 * (↑n + 1))

The inner radius of ContDiffBump.shrinking.

@[simp]

theorem ContDiffBump.rOut_shrinking {X : Type u_1} {c : X} {R : ℝ} (hR : 0 < R) (n : ℕ) : (shrinking hR n).rOut = R / (↑n + 1)

The outer radius of ContDiffBump.shrinking.

theorem ContDiffBump.rOut_shrinking_eq_two_mul_rIn {X : Type u_1} {c : X} {R : ℝ} (hR : 0 < R) (n : ℕ) : (shrinking hR n).rOut = 2 * (shrinking hR n).rIn

The outer radius of ContDiffBump.shrinking is twice its inner radius.

theorem ContDiffBump.tendsto_rOut_shrinking {X : Type u_1} {c : X} {R : ℝ} (hR : 0 < R) : Filter.Tendsto (fun (n : ℕ) => (shrinking hR n).rOut) Filter.atTop (nhds 0)

The radii of ContDiffBump.shrinking tend to zero.

theorem ContDiffBump.exists_seq_sub_tsupport_subset {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {W Ω : TopologicalSpace.Opens E} (hWc : IsCompact (closure ↑W)) (hWΩ : closure ↑W ⊆ ↑Ω) : ∃ (φ : ℕ → ContDiffBump 0), Filter.Tendsto (fun (n : ℕ) => (φ n).rOut) Filter.atTop (nhds 0) ∧ ∀ (n : ℕ), ∀ x ∈ ↑W, ∀ y ∈ tsupport ((φ n).normed μ), x - y ∈ Ω

On a relatively compact open subdomain, a shrinking sequence of normalized bump kernels has every translated support inside the ambient open domain.

theorem ContDiffBump.shrinking_apply_eq {R : ℝ} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [HasContDiffBump E] (hR : 0 < R) (n : ℕ) (x : E) : ↑(shrinking hR n) x = ↑(shrinking hR 0) ((↑n + 1) • x)

ContDiffBump.shrinking hR n is ContDiffBump.shrinking hR 0 rescaled by the factor n + 1, so all the bumps of the sequence are rescalings of one kernel.

theorem ContDiffBump.tsupport_normed_convolution_subset {G : Type u_1} {F : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [NormedAddCommGroup F] [NormedSpace ℝ F] {g : G → F} [MeasureTheory.IsLocallyFiniteMeasure μ] [μ.IsOpenPosMeasure] (ρ : ContDiffBump 0) : tsupport (MeasureTheory.convolution (ρ.normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ) ⊆ Metric.closedBall 0 ρ.rOut + tsupport g

The support of a normalized-bump convolution lies in the closed radius-neighborhood of the support of the other factor, expressed as a Minkowski sum.

theorem ContDiffBump.integral_shrinking_normed_mul {G : Type u_1} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddHaarMeasure] {R : ℝ} (hR : 0 < R) (n : ℕ) (f : G → ℝ) : ∫ (t : G), (shrinking hR n).normed μ t * f t ∂μ = ∫ (s : G), (shrinking hR 0).normed μ s * f ((↑n + 1)⁻¹ • s) ∂μ

Integrating against the normalized bump ContDiffBump.shrinking hR n is integrating against the normalized bump ContDiffBump.shrinking hR 0 after rescaling the variable by (n + 1)⁻¹.

theorem ContDiffBump.tendstoUniformly_normed_convolution {G : Type u_1} {F : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [NormedAddCommGroup F] [NormedSpace ℝ F] {g : G → F} [μ.IsAddHaarMeasure] [CompleteSpace F] {ι : Type u_3} {l : Filter ι} {ρ : ι → ContDiffBump 0} (hρ : Filter.Tendsto (fun (i : ι) => (ρ i).rOut) l (nhds 0)) (hg : UniformContinuous g) : TendstoUniformly (fun (i : ι) => MeasureTheory.convolution ((ρ i).normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ) g l

Normalized bumps of shrinking radius approximate a uniformly continuous function uniformly on the whole space.

theorem ContDiffBump.tendstoUniformlyOnFilter_normed_convolution {G : Type u_1} {F : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [NormedAddCommGroup F] [NormedSpace ℝ F] {g : G → F} [μ.IsAddHaarMeasure] [CompleteSpace F] {ι : Type u_3} {l : Filter ι} {x : G} {ρ : ι → ContDiffBump 0} (hρ : Filter.Tendsto (fun (i : ι) => (ρ i).rOut) l (nhds 0)) (hgm : MeasureTheory.AEStronglyMeasurable g μ) (hgx : ContinuousAt g x) : TendstoUniformlyOnFilter (fun (i : ι) => MeasureTheory.convolution ((ρ i).normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ) g l (nhds x)

Normalized bumps of radius tending to zero along a filter approximate a function that is continuous at x uniformly on a neighbourhood filter of x. This upgrades Mathlib's joint convergence ContDiffBump.convolution_tendsto_right to the form needed for limit theorems of derivatives such as hasFDerivAt_of_tendstoUniformlyOnFilter.

theorem ContDiffBump.normed_convolution_mem_Icc {G : Type u_1} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddHaarMeasure] (φ : ContDiffBump 0) {w : G → ℝ} {a b : ℝ} (hw : MeasureTheory.LocallyIntegrable w μ) (hwab : ∀ (x : G), w x ∈ Set.Icc a b) (x : G) : MeasureTheory.convolution (φ.normed μ) w (ContinuousLinearMap.lsmul ℝ ℝ) μ x ∈ Set.Icc a b

Mollifying a locally integrable function with values in [a, b] by a normalized bump keeps its values in [a, b].

theorem ContDiffBump.tendstoUniformlyOn_convolution_indicator_ball {G : Type u_1} {F : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [NormedAddCommGroup F] [NormedSpace ℝ F] [μ.IsAddHaarMeasure] [CompleteSpace F] {ι : Type u_3} {l : Filter ι} {x : G} {r : ℝ} (hr : 0 < r) {V : G → F} (hVc : ContinuousOn V (Metric.ball x r)) {phi : ι → ContDiffBump 0} (hphi : Filter.Tendsto (fun (n : ι) => (phi n).rOut) l (nhds 0)) : TendstoUniformlyOn (fun (n : ι) => MeasureTheory.convolution ((Metric.ball x r).indicator V) ((phi n).normed μ) (ContinuousLinearMap.lsmul ℝ ℝ).flip μ) ((Metric.ball x r).indicator V) l (Metric.ball x (r / 2))

Mollifying a function that is continuous on a ball by bumps with radii tending to 0 converges uniformly on the half-radius ball, along any filter of parameters.

theorem HasCompactSupport.iteratedFDeriv_normed_convolution {E : Type u_1} {F : Type u_2} [NormedAddCommGroup E] [NormedSpace ℝ E] [FiniteDimensional ℝ E] [MeasurableSpace E] [BorelSpace E] [NormedAddCommGroup F] [NormedSpace ℝ F] {μ : MeasureTheory.Measure E} [μ.IsAddHaarMeasure] {f : E → F} {N : ℕ∞} {k : ℕ} (hfc : HasCompactSupport f) (hf : ContDiff ℝ (↑N) f) (ρ : ContDiffBump 0) (hk : ↑k ≤ N) : iteratedFDeriv ℝ k (MeasureTheory.convolution (ρ.normed μ) f (ContinuousLinearMap.lsmul ℝ ℝ) μ) = MeasureTheory.convolution (ρ.normed μ) (iteratedFDeriv ℝ k f) (ContinuousLinearMap.lsmul ℝ ℝ) μ

Every available Fréchet derivative of compactly supported finite-regularity data commutes with normalized-bump convolution.

theorem ContDiffBump.dist_normed_convolution_le_of_dist_sub_le {G : Type u_1} {F : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] {g : G → F} (hg : Continuous g) (ρ : ContDiffBump 0) {x y : G} {B : ℝ} (hB : ∀ (t : G), dist (g (x - t)) (g (y - t)) ≤ B) : dist (MeasureTheory.convolution (ρ.normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x) (MeasureTheory.convolution (ρ.normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ y) ≤ B

Convolution with a nonnegative normalized bump averages the differences of translates: if dist (g (x - t)) (g (y - t)) ≤ B for every t, then the convolutions at x and y are within B of each other.

theorem ContDiffBump.norm_normed_convolution_le {G : Type u_1} {F : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] {g : G → F} (ρ : ContDiffBump 0) {M : ℝ} (hM : ∀ (x : G), ‖g x‖ ≤ M) (x : G) : ‖MeasureTheory.convolution (ρ.normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ x‖ ≤ M

Convolution with a nonnegative normalized bump preserves a uniform bound on the norm.

theorem LipschitzWith.normed_convolution {G : Type u_1} {F : Type u_2} [NormedAddCommGroup G] [NormedSpace ℝ G] [FiniteDimensional ℝ G] [MeasurableSpace G] [BorelSpace G] {μ : MeasureTheory.Measure G} [μ.IsAddHaarMeasure] [NormedAddCommGroup F] [NormedSpace ℝ F] {g : G → F} {K : NNReal} (hg : LipschitzWith K g) (ρ : ContDiffBump 0) : LipschitzWith K (MeasureTheory.convolution (ρ.normed μ) g (ContinuousLinearMap.lsmul ℝ ℝ) μ)

Convolution with a nonnegative normalized bump preserves the Lipschitz constant, including for Banach-valued functions.