English
If f and g are measurable functions, then withDensity κ (f + g) = withDensity κ f + withDensity κ g.
Русский
Если f и g измеримы, то withDensity κ (f + g) = withDensity κ f + withDensity κ g.
LaTeX
$$$ \text{withDensity } κ (f + g) = \text{withDensity } κ f + \text{withDensity } κ g $$$
Lean4
theorem withDensity_sub_add_cancel [IsSFiniteKernel κ] {f g : α → β → ℝ≥0∞} (hf : Measurable (Function.uncurry f))
(hg : Measurable (Function.uncurry g)) (hfg : ∀ a, g a ≤ᵐ[κ a] f a) :
withDensity κ (fun a x ↦ f a x - g a x) + withDensity κ g = withDensity κ f :=
by
rw [← withDensity_add_right _ hg]
swap; · exact hf.sub hg
refine withDensity_congr_ae κ ((hf.sub hg).add hg) hf (fun a ↦ ?_)
filter_upwards [hfg a] with x hx
rwa [Pi.add_apply, Pi.add_apply, tsub_add_cancel_iff_le]