convolutionExists_left_of_continuous_right

English

Let HasCompactSupport f hold. If f is locally integrable and g is continuous, then the convolution f ⋆[L, μ] g exists (globally).

Русский

Пусть соблюдается компактность опоры f. Если f локально интегрируема, а g непрерывна, то свёртка f ⋆ g по L и μ существует во всех точках.

LaTeX

$$$\\mathrm{ConvolutionExists}(f,g,L,μ)$$$

Lean4

theorem _root_.HasCompactSupport.convolutionExists_left_of_continuous_right (hcf : HasCompactSupport f)
    (hf : LocallyIntegrable f μ) (hg : Continuous g) : ConvolutionExists f g L μ :=
  by
  intro x₀
  refine HasCompactSupport.convolutionExistsAt L ?_ hf hg
  refine hcf.mono ?_
  refine fun t => mt fun ht : f t = 0 => ?_
  simp_rw [ht, L.map_zero₂]

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