convolutionExists_right_of_continuous_left

English

If two input pairs (f,g) and (f',g') are equal almost everywhere, then their convolutions agree: convolution f g = convolution f' g'.

Русский

Если пары функций совпадают почти наверняка, то их свёртки совпадают: свёртка f,g равна свёртке f',g'.

LaTeX

$$$\\mathrm{ConvolutionExists}(f,g,L,μ)\\iff \\mathrm{ConvolutionExists}(f',g',L,μ)$ при равенстве почти наверняка.$$

Lean4

theorem _root_.HasCompactSupport.convolutionExists_right_of_continuous_left (hcg : HasCompactSupport g)
    (hf : Continuous f) (hg : LocallyIntegrable g μ) : ConvolutionExists f g L μ := fun x₀ =>
  convolutionExistsAt_flip.mp <| hcg.convolutionExists_left_of_continuous_right L.flip hg hf x₀

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