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