convolution_integrand' — Mathlib

English

If a bound holds for the norm of the integrand, and certain subset conditions, then the convolution exists.

Русский

Если выполнено ограничение нормы интегранда и заданы условия подмножества, то существование свёртки следует.

LaTeX

$$ConvolutionExistsAt f g x₀ L μ$$

Lean4

theorem convolution_integrand' [MeasurableAdd₂ G] [MeasurableNeg G] (hf : AEStronglyMeasurable f ν)
    (hg : AEStronglyMeasurable g <| map (fun p : G × G => p.1 - p.2) (μ.prod ν)) :
    AEStronglyMeasurable (fun p : G × G => L (f p.2) (g (p.1 - p.2))) (μ.prod ν) :=
  L.aestronglyMeasurable_comp₂ hf.comp_snd <| hg.comp_measurable measurable_sub

Похожие утверждения