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