support_convolution_subset_swap — Mathlib

English

If (f,g) and (f',g) are both valid for convolution, then the convolution with f+f' against g equals the sum of the two convolutions.

Русский

Если обе пары (f,g) и (f',g) корректны, то конволюция (f+f',g) равна конволюции f,g плюс конволюции f',g.

LaTeX

$$$\\mathrm{convolution}(f+f',g)=\\mathrm{convolution}(f,g)+\\mathrm{convolution}(f',g)$$$

Lean4

theorem support_convolution_subset_swap : support (f ⋆[L, μ] g) ⊆ support g + support f :=
  by
  intro x h2x
  by_contra hx
  apply h2x
  simp_rw [Set.mem_add, ← exists_and_left, not_exists, not_and_or, notMem_support] at hx
  rw [convolution_def]
  convert integral_zero G F using 2
  ext t
  rcases hx (x - t) t with (h | h | h)
  · rw [h, (L _).map_zero]
  · rw [h, L.map_zero₂]
  · exact (h <| sub_add_cancel x t).elim

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