English
If g has compact support, f is Locally Integrable, and g is continuous, then the convolution of f and g with respect to L and μ exists (globally in the sense of ConvolutionExists).
Русский
Если функция g имеет компактную опору, f локально интегрируема по μ, и g непрерывна, тогда свёртка f⋆g по L и μ существует во всей области определения.
LaTeX
$$$\\mathrm{ConvolutionExists}(f,g,L,μ)$$$
Lean4
theorem _root_.HasCompactSupport.convolutionExists_right (hcg : HasCompactSupport g) (hf : LocallyIntegrable f μ)
(hg : Continuous g) : ConvolutionExists f g L μ := by
intro x₀
refine HasCompactSupport.convolutionExistsAt L ?_ hf hg
refine (hcg.comp_homeomorph (Homeomorph.subLeft x₀)).mono ?_
refine fun t => mt fun ht : g (x₀ - t) = 0 => ?_
simp_rw [ht, (L _).map_zero]
