mconv_add — Mathlib

English

Convolution distributes over addition: μ ∗ (ν + ρ) = μ ∗ ν + μ ∗ ρ.

Русский

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

LaTeX

$$$ μ ∗ (ν + ρ) = μ ∗ ν + μ ∗ ρ $$$

Lean4

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

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