Theorems · Theorem · probability

MeasureTheory.Measure.comp_smul

∀ {α : Type u_1} {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β} {μ : MeasureTheory.Measure α}
  {κ : ProbabilityTheory.Kernel α β} (a : ENNReal), (a • μ).bind ⇑κ = a • μ.bind ⇑κ

Defined in

Mathlib.Probability.Kernel.Composition.MeasureComp

Cited by

0 results in Mathlib

Foundations

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