withDensity_congr_ae — Mathlib

English

If κ is a kernel and f,g are jointly measurable and f a =ᵐ[κ a] g a for all a, then κ.withDensity f = κ.withDensity g.

Русский

Если κ — ядро и f, g измеримы совместно, и для каждого a имеет место a.e. согласование f a =ᵐ[κ a] g a, то κ.withDensity f = κ.withDensity g.

LaTeX

$$$ (\forall a, f a =^{\text{a.e.}}_{κ a} g a) \Rightarrow κ.withDensity f = κ.withDensity g $$$

Lean4

nonrec theorem withDensity_congr_ae (κ : Kernel α β) [IsSFiniteKernel κ] {f g : α → β → ℝ≥0∞}
    (hf : Measurable (Function.uncurry f)) (hg : Measurable (Function.uncurry g)) (hfg : ∀ a, f a =ᵐ[κ a] g a) :
    withDensity κ f = withDensity κ g := by
  ext a
  rw [Kernel.withDensity_apply _ hf, Kernel.withDensity_apply _ hg, withDensity_congr_ae (hfg a)]

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