LeanMachineLearning exposition

MeasureTheory.map_equiv_withDensity🔗

Minimal Lean file

map_equiv_withDensity🔗

LemmaMeasureTheory.map_equiv_withDensity
Details

No docstring.

🔗theorem
MeasureTheory.map_equiv_withDensity.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {μ : Measure α} {e : α ≃ᵐ β} {f : α → ENNReal} (hf : Measurable f) :
  Measure.map (⇑e) (Measure.withDensity μ f) =
    Measure.withDensity (Measure.map (⇑e) μ)
      (f ∘ ⇑(MeasurableEquiv.symm e))
MeasureTheory.map_equiv_withDensity.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β} {μ : Measure α}
  {e : α ≃ᵐ β} {f : α → ENNReal}
  (hf : Measurable f) :
  Measure.map (⇑e)
      (Measure.withDensity μ f) =
    Measure.withDensity
      (Measure.map (⇑e) μ)
      (f ∘ ⇑(MeasurableEquiv.symm e))

Code

lemma map_equiv_withDensity {e : α ≃ᵐ β} {f : α → ℝ≥0∞} (hf : Measurable f) :
    (μ.withDensity f).map e = (μ.map e).withDensity (f ∘ e.symm)
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  simp_rw [← map_withDensity_comp e.measurable (hf.comp e.symm.measurable),
    Function.comp_assoc, MeasurableEquiv.symm_comp_self]
  rfl