withDensity_add_right — Mathlib

English

If a fiberwise almost everywhere inequality g a ≤ᵐ[κ a] f a holds and hf, hg are measurable, then withDensity κ (f − g) + withDensity κ g = withDensity κ f.

Русский

Если почти повсюду выполняется g a ≤ᵐ[κ a] f a и hf, hg измеримы, тогда withDensity κ (f − g) + withDensity κ g = withDensity κ f.

LaTeX

$$$ \text{withDensity } κ (f - g) + \text{withDensity } κ g = \text{withDensity } κ f $$$

Lean4

theorem withDensity_add_right [IsSFiniteKernel κ] {f g : α → β → ℝ≥0∞} (hf : Measurable (Function.uncurry f))
    (hg : Measurable (Function.uncurry g)) : withDensity κ (f + g) = withDensity κ f + withDensity κ g :=
  by
  ext a
  rw [coe_add, Pi.add_apply, Kernel.withDensity_apply _ hf, Kernel.withDensity_apply _ hg, Kernel.withDensity_apply,
    Pi.add_apply, MeasureTheory.withDensity_add_right]
  · fun_prop
  · exact hf.add hg

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