LeanMachineLearning exposition

MeasureTheory.map_withDensity_comp🔗

Minimal Lean file

map_withDensity_comp🔗

LemmaMeasureTheory.map_withDensity_comp
Details

No docstring.

🔗theorem
MeasureTheory.map_withDensity_comp.{u_1, u_3} {α : Type u_1}
  {γ : Type u_3} {mα : MeasurableSpace α} {mγ : MeasurableSpace γ}
  {μ : Measure α} {g : α → γ} {f : γ → ENNReal} (hg : Measurable g)
  (hf : Measurable f) :
  Measure.map g (Measure.withDensity μ (f ∘ g)) =
    Measure.withDensity (Measure.map g μ) f
MeasureTheory.map_withDensity_comp.{u_1,
    u_3}
  {α : Type u_1} {γ : Type u_3}
  {mα : MeasurableSpace α}
  {mγ : MeasurableSpace γ} {μ : Measure α}
  {g : α → γ} {f : γ → ENNReal}
  (hg : Measurable g)
  (hf : Measurable f) :
  Measure.map g
      (Measure.withDensity μ (f ∘ g)) =
    Measure.withDensity (Measure.map g μ)
      f

Code

lemma map_withDensity_comp {g : α → γ} {f : γ → ℝ≥0∞} (hg : Measurable g) (hf : Measurable f) :
    (μ.withDensity (f ∘ g)).map g = (μ.map g).withDensity f
Used by (2)

Actions: Source · Open Issue

Proof
by
  ext s hs
  rw [Measure.map_apply hg hs, withDensity_apply _ (hg hs), withDensity_apply _ hs,
    setLIntegral_map hs hf hg]
  rfl