convolutionExistsAt_flip — Mathlib

English

The existence of the convolution is preserved when swapping the two input functions and applying the flip to L: ConvolutionExistsAt g f x L.flip μ is equivalent to ConvolutionExistsAt f g x L μ.

Русский

Существование свёртки сохраняется при обмене аргументов: ConvolutionExistsAt(g,f,x,L.flip,μ) эквивалентно ConvolutionExistsAt(f,g,x,L,μ).

LaTeX

$$$\\mathrm{ConvolutionExistsAt}(g,f,x,L^{\\mathrm{flip}},\\mu) \\iff \\mathrm{ConvolutionExistsAt}(f,g,x,L,\\mu)$$$

Lean4

theorem convolutionExistsAt_flip : ConvolutionExistsAt g f x L.flip μ ↔ ConvolutionExistsAt f g x L μ := by
  simp_rw [ConvolutionExistsAt, ← integrable_comp_sub_left (fun t => L (f t) (g (x - t))) x, sub_sub_cancel, flip_apply]

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