Theorems · Theorem · measure theory

MeasureTheory.llr_smul_right

∀ {α : Type u_1} {mα : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [MeasureTheory.IsFiniteMeasure μ]
  [μ.HaveLebesgueDecomposition ν],
  μ.AbsolutelyContinuous ν →
    ∀ (c : ENNReal),
      c ≠ 0 → c ≠ ⊤ → MeasureTheory.llr μ (c • ν) =ᵐ[μ] fun x => MeasureTheory.llr μ ν x - Real.log c.toReal

Defined in

Mathlib.MeasureTheory.Measure.LogLikelihoodRatio

Cited by

3 results in Mathlib

Foundations

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

Assumes

MeasureTheory.IsFiniteMeasureMeasureTheory.Measure.HaveLebesgueDecomposition