Theorems · Theorem · probability

ProbabilityTheory.Kernel.IsProper.lintegral_mul

∀ {X : Type u_1} {𝓑 𝓧 : MeasurableSpace X} {π : ProbabilityTheory.Kernel X X} {f g : X → ENNReal},
  π.IsProper →
    𝓑 ≤ 𝓧 → Measurable f → Measurable g → ∀ (x₀ : X), ∫⁻ (x : X), g x * f x ∂π x₀ = g x₀ * ∫⁻ (x : X), f x ∂π x₀

Defined in

Mathlib.Probability.Kernel.Proper

Cited by

0 results in Mathlib

Foundations

Depth 208 from the axioms · uses propext, Classical.choice, Quot.sound