LeanMachineLearning exposition

MeasureTheory.map_swap_withDensity_comp_snd🔗

Minimal Lean file

map_swap_withDensity_comp_snd🔗

LemmaMeasureTheory.map_swap_withDensity_comp_snd
Details

No docstring.

🔗theorem
MeasureTheory.map_swap_withDensity_comp_snd.{u_1, u_2} {α : Type u_1}
  {β : Type u_2} {mα : MeasurableSpace α} {mβ : MeasurableSpace β}
  {μ : Measure (α × β)} {f : β → ENNReal} (hf : Measurable f) :
  Measure.map Prod.swap
      (Measure.withDensity μ fun ab => f (Prod.snd ab)) =
    Measure.withDensity (Measure.map Prod.swap μ) fun ba =>
      f (Prod.fst ba)
MeasureTheory.map_swap_withDensity_comp_snd.{u_1,
    u_2}
  {α : Type u_1} {β : Type u_2}
  {mα : MeasurableSpace α}
  {mβ : MeasurableSpace β}
  {μ : Measure (α × β)} {f : β → ENNReal}
  (hf : Measurable f) :
  Measure.map Prod.swap
      (Measure.withDensity μ fun ab =>
        f (Prod.snd ab)) =
    Measure.withDensity
      (Measure.map Prod.swap μ) fun ba =>
      f (Prod.fst ba)

Code

lemma map_swap_withDensity_comp_snd {μ : Measure (α × β)} {f : β → ℝ≥0∞} (hf : Measurable f) :
    (μ.withDensity (fun ab ↦ f ab.2)).map Prod.swap =
      (μ.map Prod.swap).withDensity (fun ba ↦ f ba.1)
Body uses (1)
Used by (1)

Actions: Source · Open Issue

Proof
by
  rw [← map_withDensity_comp measurable_swap (by fun_prop)]
  rfl