English
Under positivity and unit-integral-normalization, the distance between the convolution and the target is bounded by ε.
Русский
При неотрицательности и нормировке интеграла равной единице расстояние между сверткой и целью ограничено ε.
LaTeX
$$dist((f ⋆[lsmul ℝ ℝ, μ] g : G → E') x0) z0 ≤ ε$$
Lean4
/-- Approximate `(f ⋆ g) x₀` if the support of the `f` is bounded within a ball, and `g` is near
`g x₀` on a ball with the same radius around `x₀`. See `dist_convolution_le` for a special case.
We can simplify the second argument of `dist` further if we add some extra type-classes on `E`
and `𝕜` or if `L` is scalar multiplication. -/
theorem dist_convolution_le' {x₀ : G} {R ε : ℝ} {z₀ : E'} (hε : 0 ≤ ε) (hif : Integrable f μ)
(hf : support f ⊆ ball (0 : G) R) (hmg : AEStronglyMeasurable g μ) (hg : ∀ x ∈ ball x₀ R, dist (g x) z₀ ≤ ε) :
dist ((f ⋆[L, μ] g : G → F) x₀) (∫ t, L (f t) z₀ ∂μ) ≤ (‖L‖ * ∫ x, ‖f x‖ ∂μ) * ε :=
by
have hfg : ConvolutionExistsAt f g x₀ L μ :=
by
refine BddAbove.convolutionExistsAt L ?_ Metric.isOpen_ball.measurableSet (Subset.trans ?_ hf) hif.integrableOn hmg
swap; · refine fun t => mt fun ht : f t = 0 => ?_; simp_rw [ht, L.map_zero₂]
rw [bddAbove_def]
refine ⟨‖z₀‖ + ε, ?_⟩
rintro _ ⟨x, hx, rfl⟩
refine norm_le_norm_add_const_of_dist_le (hg x ?_)
rwa [mem_ball_iff_norm, norm_sub_rev, ← mem_ball_zero_iff]
have h2 : ∀ t, dist (L (f t) (g (x₀ - t))) (L (f t) z₀) ≤ ‖L (f t)‖ * ε :=
by
intro t; by_cases ht : t ∈ support f
· have h2t := hf ht
rw [mem_ball_zero_iff] at h2t
specialize hg (x₀ - t)
rw [sub_eq_add_neg, add_mem_ball_iff_norm, norm_neg, ← sub_eq_add_neg] at hg
refine ((L (f t)).dist_le_opNorm _ _).trans ?_
exact mul_le_mul_of_nonneg_left (hg h2t) (norm_nonneg _)
· rw [notMem_support] at ht
simp_rw [ht, L.map_zero₂, L.map_zero, norm_zero, zero_mul, dist_self]
rfl
simp_rw [convolution_def]
simp_rw [dist_eq_norm] at h2 ⊢
rw [← integral_sub hfg.integrable]; swap; · exact (L.flip z₀).integrable_comp hif
refine (norm_integral_le_of_norm_le ((L.integrable_comp hif).norm.mul_const ε) (Eventually.of_forall h2)).trans ?_
rw [integral_mul_const]
refine mul_le_mul_of_nonneg_right ?_ hε
have h3 : ∀ t, ‖L (f t)‖ ≤ ‖L‖ * ‖f t‖ := by
intro t
exact L.le_opNorm (f t)
refine (integral_mono (L.integrable_comp hif).norm (hif.norm.const_mul _) h3).trans_eq ?_
rw [integral_const_mul]
