awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
this : SigmaFinite ν
h_ne_top1_1 : ∀ᵐ (x : 𝓧) ∂ν, Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞
h_ne_top2_1 : ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞
h_condExp_1 :
  (ae ν).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x).toReal)
    ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨]
x : 𝓧
hx :
  (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x)).toReal =
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨] x
h_condExp :
  (ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x).toReal =
    ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x
h_ne_top1 : Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞
h_ne_top2 : ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞
⊢ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) = ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x
have h : ∀
  (hx :
    (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x)).toReal =
      (ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x).toReal)
  (h_condExp :
    (ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x).toReal =
      ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x)
  (h_ne_top1 : Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞)
  (h_ne_top2 : ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞),
  Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) = ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x
Tactic: rwa [← h_condExp, ENNReal.toReal_eq_toReal_iff' h_ne_top1 h_ne_top2] at hx
Cleared hypotheses: hx, h_condExp, h_ne_top1, h_ne_top2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
this : SigmaFinite ν
h_ne_top1_1 : ∀ᵐ (x : 𝓧) ∂ν, Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞
h_ne_top2_1 : ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞
h_condExp_1 :
  (ae ν).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x).toReal)
    ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨]
x : 𝓧
hx :
  (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x)).toReal =
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨] x
h_condExp :
  (ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x).toReal =
    ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x
h_ne_top1 : Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞
h_ne_top2 : ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞
h :
  ∀
    (hx :
      (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x)).toReal =
        (ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x).toReal)
    (h_condExp :
      (ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x).toReal =
        ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x)
    (h_ne_top1 : Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞)
    (h_ne_top2 : ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞),
    Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) = ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x
⊢ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) = ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x
have h₁ : ∀
  (hx :
    Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) = ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x)
  (h_condExp :
    (ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x).toReal =
      ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨] x)
  (h_ne_top1 : Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞)
  (h_ne_top2 : ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞),
  Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) = ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x
Tactic: rwa [← h_condExp, ENNReal.toReal_eq_toReal_iff' h_ne_top1 h_ne_top2] at hx
Cleared hypotheses: hx, h_condExp, h_ne_top1, h_ne_top2
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
⊢ (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae (ν.trim ⋯)]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
have rw : (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae ν]
  ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
Tactic: rw [StronglyMeasurable.ae_eq_trim_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
rw :
  (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae ν]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
⊢ (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae (ν.trim ⋯)]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
have hf : StronglyMeasurable (β := ℝ≥0∞) fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)
Tactic: rw [StronglyMeasurable.ae_eq_trim_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
rw :
  (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae ν]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
hf : StronglyMeasurable (β := ℝ≥0∞) fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)
⊢ (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae (ν.trim ⋯)]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
have hg₁ : StronglyMeasurable ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
Tactic: rw [StronglyMeasurable.ae_eq_trim_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
⊢ StronglyMeasurable (β := ℝ≥0∞) fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)
have hf : ∀ (s : Set ℝ≥0∞) (hs : MeasurableSet s),
  MeasurableSet.{u_1} (α := 𝓧)
    ((fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) ⁻¹' s)
Tactic: refine Measurable.stronglyMeasurable fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
⊢ (ae (ν.trim ⋯)).EventuallyEq (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal)
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]
have rw : (ae ν).EventuallyEq (β := ℝ)
  (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal)
  ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]
Tactic: rw [StronglyMeasurable.ae_eq_trim_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
rw :
  (ae ν).EventuallyEq (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal)
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]
⊢ (ae (ν.trim ⋯)).EventuallyEq (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal)
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]
have hf : StronglyMeasurable (β := ℝ) fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal
Tactic: rw [StronglyMeasurable.ae_eq_trim_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
rw :
  (ae ν).EventuallyEq (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal)
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]
hf :
  StronglyMeasurable (β := ℝ) fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal
⊢ (ae (ν.trim ⋯)).EventuallyEq (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal)
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]
have hg₁ : StronglyMeasurable (β := ℝ) ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]
Tactic: rw [StronglyMeasurable.ae_eq_trim_iff]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
⊢ StronglyMeasurable (β := ℝ) fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal
have hf : ∀ (s : Set ℝ) (hs : MeasurableSet s),
  MeasurableSet.{u_1} (α := 𝓧)
    ((fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) ⁻¹' s)
Tactic: refine Measurable.stronglyMeasurable fun s hs ↦ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
s : Set ℝ
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := 𝓧)
    ((fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) ⁻¹' s)
have hf : g ⁻¹' (fun (a : 𝓨) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) a).toReal) ⁻¹' s =
  (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) ⁻¹' s
Tactic: refine ⟨(fun a ↦ ((μ.map g).rnDeriv (ν.map g) a).toReal) ⁻¹' s, hs.preimage (by fun_prop), ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
𝓨 : Type u_2
m𝓧 : MeasurableSpace 𝓧
m𝓨 : MeasurableSpace 𝓨
μ ν : Measure 𝓧
inst : IsFiniteMeasure μ
hμν : μ ≪ ν
g : 𝓧 → 𝓨
hg : Measurable g
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
s : Set ℝ
hs : MeasurableSet s
⊢ g ⁻¹' (fun (a : 𝓨) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) a).toReal) ⁻¹' s =
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) ⁻¹' s
have hf : (fun (a : 𝓨) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) a).toReal) ∘ g ⁻¹' s =
  (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) ⁻¹' s
Tactic: rw [← Set.preimage_comp]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
⊢ (ae (ν.trim hm)).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal)
    ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m]
have simp_rw : (ae (F := Measure 𝓧) (Measure.map id ν)).EventuallyEq (β := ℝ)
  (fun (x : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) x).toReal)
  ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m]
Tactic: simp_rw [trim_eq_map hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (hypothesis)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
⊢ (ae (F := Measure 𝓧) (Measure.map id ν)).EventuallyEq (β := ℝ)
    (fun (x : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) x).toReal)
    ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m]
have this : SigmaFinite (m0 := m) (Measure.map id ν)
Tactic: have : SigmaFinite (@Measure.map _ _ m𝓧 m id ν) := by rwa [← trim_eq_map hm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (hypothesis)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (m0 := m) (Measure.map id ν)
⊢ (ae (F := Measure 𝓧) (Measure.map id ν)).EventuallyEq (β := ℝ)
    (fun (x : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) x).toReal)
    ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m]
have h : (ae (ν.trim sorry)).EventuallyEq (β := ℝ)
  (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) (id a)).toReal)
  ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap id m]
Tactic: have h := toReal_rnDeriv_map_ae_eq_trim hμν (measurable_id'' hm)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (hypothesis)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (m0 := m) (Measure.map id ν)
h :
  (ae (ν.trim ⋯)).EventuallyEq (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) (id a)).toReal)
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap id m]
⊢ (ae (F := Measure 𝓧) (Measure.map id ν)).EventuallyEq (β := ℝ)
    (fun (x : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) x).toReal)
    ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m]
have h₁ : (ae (F := Measure 𝓧) (Measure.map id ν)).EventuallyEq (β := ℝ)
  (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) a).toReal)
  ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | m]
Tactic: simp_rw [MeasurableSpace.comap_id, id_def, trim_eq_map] at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (m0 := m) (Measure.map id ν)
h :
  (ae (F := Measure 𝓧) (Measure.map id ν)).EventuallyEq (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) a).toReal)
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | m]
⊢ (ae (F := Measure 𝓧) (Measure.map id ν)).EventuallyEq (β := ℝ)
    (fun (x : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) x).toReal)
    ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m]
have h₁ : m = MeasurableSpace.comap id m
Tactic: convert! h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (m0 := m) (Measure.map id ν)
h :
  (ae (F := Measure 𝓧) (Measure.map id ν)).EventuallyEq (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) a).toReal)
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | m]
h₁ : m = MeasurableSpace.comap id m
⊢ (ae (F := Measure 𝓧) (Measure.map id ν)).EventuallyEq (β := ℝ)
    (fun (x : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) x).toReal)
    ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m]
have h₂ : Measure 𝓧 = Measure 𝓧 → m = MeasurableSpace.comap id m
Tactic: convert! h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (m0 := m) (Measure.map id ν)
h :
  (ae (F := Measure 𝓧) (Measure.map id ν)).EventuallyEq (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) a).toReal)
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | m]
⊢ m = MeasurableSpace.comap id m
have h₁ : m = m
Tactic: rw [MeasurableSpace.comap_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
this : SigmaFinite (m0 := m) (Measure.map id ν)
h :
  (ae (F := Measure 𝓧) (Measure.map id ν)).EventuallyEq (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) a).toReal)
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | m]
e_2 : Measure 𝓧 = Measure 𝓧
⊢ m = MeasurableSpace.comap id m
have h₁ : m = m
Tactic: rw [MeasurableSpace.comap_id]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
⊢ (μ.trim hm).rnDeriv (ν.trim hm) =ᶠ[ae (ν.trim hm)] fun (x : 𝓧) ↦
    ENNReal.ofReal (ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m] x)
have h : ∀ (x : 𝓧) (hx : ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal = ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m] x)
  (hx_ne_top : (μ.trim hm).rnDeriv (ν.trim hm) x ≠ ∞),
  (μ.trim hm).rnDeriv (ν.trim hm) x = ENNReal.ofReal (ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m] x)
Tactic: filter_upwards [toReal_rnDeriv_trim hm hμν, Measure.rnDeriv_ne_top (μ.trim hm) (ν.trim hm)]
    with x hx hx_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
x : 𝓧
hx : ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal = ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m] x
hx_ne_top : (μ.trim hm).rnDeriv (ν.trim hm) x ≠ ∞
⊢ (μ.trim hm).rnDeriv (ν.trim hm) x = ENNReal.ofReal (ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m] x)
have h : (μ.trim hm).rnDeriv (ν.trim hm) x = ENNReal.ofReal ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal
Tactic: rw [← hx, ENNReal.ofReal_toReal hx_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (goal)
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
x : 𝓧
hx : ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal = ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m] x
hx_ne_top : (μ.trim hm).rnDeriv (ν.trim hm) x ≠ ∞
h : (μ.trim hm).rnDeriv (ν.trim hm) x = ENNReal.ofReal ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal
⊢ (μ.trim hm).rnDeriv (ν.trim hm) x = ENNReal.ofReal (ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m] x)
have h₁ : (μ.trim hm).rnDeriv (ν.trim hm) x = (μ.trim hm).rnDeriv (ν.trim hm) x
Tactic: rw [← hx, ENNReal.ofReal_toReal hx_ne_top]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm) =ᶠ[ae μ] μ[f | m]
have refine_1 : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm)) s μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm hf ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
refine_1 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm)) s μ
⊢ SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm) =ᶠ[ae μ] μ[f | m]
have refine_2 : ∀ (s : Set α),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ) (∫ (x : α) in s, SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm) x ∂μ)
        (∫ (x : α) in s, f x ∂μ)
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm hf ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
refine_1 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm)) s μ
refine_2 :
  ∀ (s : Set α),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in s, SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm) x ∂μ)
          (∫ (x : α) in s, f x ∂μ)
⊢ SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm) =ᶠ[ae μ] μ[f | m]
have refine_3 : AEStronglyMeasurable (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm)) μ
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq hm hf ?_ ?_ ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
h : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
| ∫ (x : α) in s, f x ∂μ
have rw : (↑((μ.trim hm).withDensityᵥ (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm))) : Set α → ℝ)
  s
Tactic: rw [← hf.withDensityᵥ_trim_eq_integral hm hs,
      ← SignedMeasure.withDensityᵥ_rnDeriv_eq ((μ.withDensityᵥ f).trim hm) (μ.trim hm)
        (hf.withDensityᵥ_trim_absolutelyContinuous hm)]