LeanMachineLearning exposition

ProbabilityTheory.ae_eq_of_map_prodMk_eq🔗

Minimal Lean file

ae_eq_of_map_prodMk_eq🔗

LemmaProbabilityTheory.ae_eq_of_map_prodMk_eq
Details

No docstring.

🔗theorem
ProbabilityTheory.ae_eq_of_map_prodMk_eq.{u_1, u_7, u_8} {α : Type u_1}
  {mα : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_7}
  {Ω : Type u_8} {x✝ : MeasurableSpace β} {x✝¹ : MeasurableSpace Ω}
  [MeasurableEq Ω] {X : α → β} {Y : α → Ω} {f : β → Ω}
  (hf : Measurable f) (hX : AEMeasurable X μ) (hY : AEMeasurable Y μ)
  (h :
    MeasureTheory.Measure.map (fun ω => (X ω, Y ω)) μ =
      MeasureTheory.Measure.map (fun ω => (X ω, f (X ω))) μ) :
  Y =ᵐ[μ] f ∘ X
ProbabilityTheory.ae_eq_of_map_prodMk_eq.{u_1,
    u_7, u_8}
  {α : Type u_1} {mα : MeasurableSpace α}
  {μ : MeasureTheory.Measure α}
  {β : Type u_7} {Ω : Type u_8}
  {x✝ : MeasurableSpace β}
  {x✝¹ : MeasurableSpace Ω}
  [MeasurableEq Ω] {X : α → β} {Y : α → Ω}
  {f : β → Ω} (hf : Measurable f)
  (hX : AEMeasurable X μ)
  (hY : AEMeasurable Y μ)
  (h :
    MeasureTheory.Measure.map
        (fun ω => (X ω, Y ω)) μ =
      MeasureTheory.Measure.map
        (fun ω => (X ω, f (X ω))) μ) :
  Y =ᵐ[μ] f ∘ X

Code

lemma ae_eq_of_map_prodMk_eq {β Ω : Type*} {_ : MeasurableSpace β} {_ : MeasurableSpace Ω}
    [MeasurableEq Ω] {X : α → β} {Y : α → Ω} {f : β → Ω} (hf : Measurable f) (hX : AEMeasurable X μ)
    (hY : AEMeasurable Y μ) (h : μ.map (fun ω ↦ (X ω, Y ω)) = μ.map (fun ω ↦ (X ω, f (X ω)))) :
    Y =ᵐ[μ] f ∘ X
Body uses (1)
Used by (2)

Actions: Source · Open Issue

Proof
by
  have hp : ∀ᵐ p ∂μ.map (fun ω ↦ (X ω, f (X ω))), p.2 = f p.1 :=
    (ae_map_iff (by fun_prop) (measurableSet_graph' hf)).2 (by simp)
  exact ae_of_ae_map (by fun_prop) (h ▸ hp)