add_mconv — Mathlib

English

Convolution distributes over addition in the left argument: (μ + ν) ∗ ρ = μ ∗ ρ + ν ∗ ρ.

Русский

Свёртка распределена по сложению в первом аргументе: (μ + ν) ∗ ρ = μ ∗ ρ + ν ∗ ρ.

LaTeX

$$$ (\mu + \nu) \ast_m \rho = \mu \ast_m \rho + \nu \ast_m \rho $$$

Lean4

@[to_additive]
theorem add_mconv [MeasurableMul₂ M] (μ : Measure M) (ν : Measure M) (ρ : Measure M) [SFinite μ] [SFinite ν]
    [SFinite ρ] : (μ + ν) ∗ₘ ρ = μ ∗ₘ ρ + ν ∗ₘ ρ := by
  unfold mconv
  rw [add_prod, Measure.map_add]
  fun_prop

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