English
If the norm of f and g is bounded and the corresponding convolution exists, then there is a convolution with L.
Русский
Если норма функций f и g ограничена и соответствующая свёртка существует, значит существует свёртка с L.
LaTeX
$$ConvolutionExistsAt f g x₀ L μ$$
Lean4
/-- A sufficient condition to prove that `f ⋆[L, μ] g` exists.
We assume that `f` is integrable on a set `s` and `g` is bounded and ae strongly measurable
on `x₀ - s` (note that both properties hold if `g` is continuous with compact support). -/
theorem _root_.BddAbove.convolutionExistsAt' {x₀ : G} {s : Set G}
(hbg : BddAbove ((fun i => ‖g i‖) '' ((fun t => -t + x₀) ⁻¹' s))) (hs : MeasurableSet s)
(h2s : (support fun t => L (f t) (g (x₀ - t))) ⊆ s) (hf : IntegrableOn f s μ)
(hmg : AEStronglyMeasurable g <| map (fun t => x₀ - t) (μ.restrict s)) : ConvolutionExistsAt f g x₀ L μ :=
by
rw [ConvolutionExistsAt]
rw [← integrableOn_iff_integrable_of_support_subset h2s]
set s' := (fun t => -t + x₀) ⁻¹' s
have : ∀ᵐ t : G ∂μ.restrict s, ‖L (f t) (g (x₀ - t))‖ ≤ s.indicator (fun t => ‖L‖ * ‖f t‖ * ⨆ i : s', ‖g i‖) t :=
by
filter_upwards
refine le_indicator (fun t ht => ?_) fun t ht => ?_
· apply_rules [L.le_of_opNorm₂_le_of_le, le_rfl]
refine (le_ciSup_set hbg <| mem_preimage.mpr ?_)
rwa [neg_sub, sub_add_cancel]
· have : t ∉ support fun t => L (f t) (g (x₀ - t)) := mt (fun h => h2s h) ht
rw [notMem_support.mp this, norm_zero]
refine Integrable.mono' ?_ ?_ this
· rw [integrable_indicator_iff hs]; exact ((hf.norm.const_mul _).mul_const _).integrableOn
· exact hf.aestronglyMeasurable.convolution_integrand_snd' L hmg
