convolution_integrand_snd' — Mathlib

English

If f and g are AEStronglyMeasurable, then the convolution integrand (the function on G×G given by L(f p.2, g (p.1−p.2))) is AEStronglyMeasurable with respect to μ×ν.

Русский

Если f и g — AEStronglyMeasurable, то интегрант свёртки (на G×G) заданный L(f p.2, g(p.1−p.2)) измерим по мере μ×ν.

LaTeX

$$AEStronglyMeasurable (λ p : G×G, L (f p.2) (g (p.1 - p.2))) (μ.prod ν)$$

Lean4

theorem convolution_integrand_snd' (hf : AEStronglyMeasurable f μ) {x : G}
    (hg : AEStronglyMeasurable g <| map (fun t => x - t) μ) : AEStronglyMeasurable (fun t => L (f t) (g (x - t))) μ :=
  L.aestronglyMeasurable_comp₂ hf <| hg.comp_measurable <| measurable_id.const_sub x

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