withDensity_sub_add_cancel — Mathlib

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]

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