ae_convolution_exists — Mathlib

English

If f and g are integrable with respect to ν and μ, then almost every x (with respect to μ) has a convolution exists at x with respect to ν and L.

Русский

Если f и g интегрируемы по ν и μ, то почти наверняка по μ существует конволюция на x относительно ν и L.

LaTeX

$$∀ᵐ x ∂μ, ConvolutionExistsAt f g x L ν$$

Lean4

theorem ae_convolution_exists (hf : Integrable f ν) (hg : Integrable g μ) : ∀ᵐ x ∂μ, ConvolutionExistsAt f g x L ν :=
  ((integrable_prod_iff <| hf.aestronglyMeasurable.convolution_integrand L hg.aestronglyMeasurable).mp <|
      hf.convolution_integrand L hg).1

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