convolution_congr — Mathlib

English

If hf and hg hold (f,f' equal outside 0), then f ⍟ g = f' ⍟ g'.

Русский

Если hf и hg выполняются, то свёртки совпадают: f ⍟ g = f' ⍟ g'.

LaTeX

$$$\\bigl(\\forall {f,g},{s}, LSeriesSummable f s \\Rightarrow LSeriesSummable g s \\Rightarrow LSeriesSummable (F f g) s\\bigr) \\Rightarrow$ ... (разделено) $$

Lean4

theorem convolution_congr {R : Type*} [Semiring R] {f f' g g' : ℕ → R} (hf : ∀ {n}, n ≠ 0 → f n = f' n)
    (hg : ∀ {n}, n ≠ 0 → g n = g' n) : f ⍟ g = f' ⍟ g' := by
  simp [convolution, toArithmeticFunction_congr hf, toArithmeticFunction_congr hg]

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