English
Let G be a topological group with a left-invariant μ-measure and suppose f and g are functions such that the map t ↦ L(f(t), g(x0 − t)) has compact support for a given x0, while f is locally integrable and g is continuous. Then the convolution of f and g with respect to L and μ exists at x0.
Русский
Пусть G — топологическая группа с лево-инвариантной мераю μ. Пусть f и g такие, что для данного x0 функция t ↦ L(f(t), g(x0 − t)) имеет компактную опору, при этом f локально интегрируемо по μ, а g непрерывна. Тогда свёртка f и g по L и μ существует в точке x0.
LaTeX
$$$\\mathrm{ConvolutionExistsAt}(f,g,L,μ;x_0)$$$
Lean4
theorem _root_.HasCompactSupport.convolutionExistsAt {x₀ : G} (h : HasCompactSupport fun t => L (f t) (g (x₀ - t)))
(hf : LocallyIntegrable f μ) (hg : Continuous g) : ConvolutionExistsAt f g x₀ L μ :=
by
let u := (Homeomorph.neg G).trans (Homeomorph.addRight x₀)
let v := (Homeomorph.neg G).trans (Homeomorph.addLeft x₀)
apply
((u.isCompact_preimage.mpr h).bddAbove_image hg.norm.continuousOn).convolutionExistsAt' L
isClosed_closure.measurableSet subset_closure (hf.integrableOn_isCompact h)
have A : AEStronglyMeasurable (g ∘ v) (μ.restrict (tsupport fun t : G => L (f t) (g (x₀ - t)))) :=
by
apply (hg.comp v.continuous).continuousOn.aestronglyMeasurable_of_isCompact h
exact (isClosed_tsupport _).measurableSet
convert
((v.continuous.measurable.measurePreserving
(μ.restrict (tsupport fun t => L (f t) (g (x₀ - t))))).aestronglyMeasurable_comp_iff
v.measurableEmbedding).1
A
ext x
simp only [v, Homeomorph.neg, sub_eq_add_neg, val_toAddUnits_apply, Homeomorph.trans_apply, Equiv.neg_apply,
Homeomorph.homeomorph_mk_coe, Homeomorph.coe_addLeft]
