withDensity_add_left — Mathlib

English

If κ and η are finite kernels and f is measurable, then withDensity(κ+η) f = withDensity κ f + withDensity η f.

Русский

Если κ и η — конечные ядра и f измерим, то withDensity(κ+η) f = withDensity κ f + withDensity η f.

LaTeX

$$$ withDensity (κ + η) f = withDensity κ f + withDensity η f $$$

Lean4

theorem withDensity_add_left (κ η : Kernel α β) [IsSFiniteKernel κ] [IsSFiniteKernel η] (f : α → β → ℝ≥0∞) :
    withDensity (κ + η) f = withDensity κ f + withDensity η f :=
  by
  by_cases hf : Measurable (Function.uncurry f)
  · ext a s
    simp only [Kernel.withDensity_apply _ hf, coe_add, Pi.add_apply, withDensity_add_measure, Measure.add_apply]
  · simp_rw [withDensity_of_not_measurable _ hf]
    rw [zero_add]

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