English
If the convolution exists at f and g with given x and L, then the integrand t ↦ L(f(x − t), g(t)) is integrable with respect to μ.
Русский
Если свёртка существует в точке x для функций f и g с данным L, то интегрант t ↦ L(f(x − t), g(t)) по μ интегрируем.
LaTeX
$$$\\mathrm{Integrable}\\left(t\\mapsto L\\bigl(f(x-t)\\bigr)\n (g(t)),\\mu\\right)$$$
Lean4
/-- A sufficient condition to prove that `f ⋆[L, μ] g` exists.
We assume that the integrand has compact support and `g` is bounded on this support (note that
both properties hold if `g` is continuous with compact support). We also require that `f` is
integrable on the support of the integrand, and that both functions are strongly measurable.
This is a variant of `BddAbove.convolutionExistsAt'` in an abelian group with a left-invariant
measure. This allows us to state the boundedness and measurability of `g` in a more natural way. -/
theorem _root_.BddAbove.convolutionExistsAt [MeasurableAdd₂ G] [SFinite μ] {x₀ : G} {s : Set G}
(hbg : BddAbove ((fun i => ‖g i‖) '' ((fun t => x₀ - t) ⁻¹' s))) (hs : MeasurableSet s)
(h2s : (support fun t => L (f t) (g (x₀ - t))) ⊆ s) (hf : IntegrableOn f s μ) (hmg : AEStronglyMeasurable g μ) :
ConvolutionExistsAt f g x₀ L μ :=
by
refine BddAbove.convolutionExistsAt' L ?_ hs h2s hf ?_
· simp_rw [← sub_eq_neg_add, hbg]
· have : AEStronglyMeasurable g (map (fun t : G => x₀ - t) μ) :=
hmg.mono_ac (quasiMeasurePreserving_sub_left_of_right_invariant μ x₀).absolutelyContinuous
apply this.mono_measure
exact map_mono restrict_le_self (measurable_const.sub measurable_id')
