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 (ν.trim ⋯))
⊢ SigmaFinite (ν.trim ⋯)
have refine : AEMeasurable g (ν.trim sorry)
Tactic: refine SigmaFinite.of_map (ν.trim hg.comap_le) ?_ hσ
-- 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 (ν.trim ⋯))
⊢ AEMeasurable g (ν.trim ⋯)
have refine : Measurable g
Tactic: refine Measurable.aemeasurable ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (hypothesis)
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 ν)
⊢ (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𝓨]
have this : SigmaFinite (ν.trim sorry)
Tactic: have : SigmaFinite (ν.trim hg.comap_le) := by
    rw [← map_trim_comap hg] at hσ
    refine SigmaFinite.of_map (ν.trim hg.comap_le) ?_ hσ
    refine Measurable.aemeasurable ?_
    exact measurable_iff_comap_le.mpr le_rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (hypothesis)
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 (ν.trim ⋯)
⊢ (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𝓨]
have this₁ : SigmaFinite ν
Tactic: have : SigmaFinite ν := SigmaFinite.of_map _ hg.aemeasurable hσ
-- 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_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
⊢ (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𝓨]
have refine_1 : ∀ (s : Set 𝓧),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      IntegrableOn (ε := ℝ) (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal)
        s ν
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq _ (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
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
this_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
refine_1 :
  ∀ (s : Set 𝓧),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ)
          (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) s ν
⊢ (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𝓨]
have refine_2 : ∀ (s : Set 𝓧),
  MeasurableSet s →
    LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
      Eq (α := ℝ) (∫ (x : 𝓧) in s, (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x)).toReal ∂ν)
        (∫ (x : 𝓧) in s, (μ.rnDeriv ν x).toReal ∂ν)
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq _ (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
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
this_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
refine_1 :
  ∀ (s : Set 𝓧),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn (ε := ℝ)
          (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) s ν
refine_2 :
  ∀ (s : Set 𝓧),
    MeasurableSet s →
      LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : 𝓧) in s, (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x)).toReal ∂ν)
          (∫ (x : 𝓧) in s, (μ.rnDeriv ν x).toReal ∂ν)
⊢ (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𝓨]
have refine_3 : AEStronglyMeasurable (β := ℝ)
  (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) ν
Tactic: refine ae_eq_condExp_of_forall_setIntegral_eq _ (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
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
this_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : 𝓧) in g ⁻¹' t, (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x)).toReal ∂ν)
    (@integral _ _ _ _ m𝓨 (Measure.restrict (Measure.map g ν) t) fun (y : 𝓨) ↦
      (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal)
have rw : AEStronglyMeasurable (β := ℝ) (m₀ := m𝓨)
  (fun (y : 𝓨) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal) (Measure.map g ν)
Tactic: rw [setIntegral_map ht _ hg.aemeasurable]
-- 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_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ m𝓨 (Measure.restrict (Measure.map g ν) t) fun (y : 𝓨) ↦
      (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal)
    (∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν)
have rw : Measure.real (m := m𝓨) (Measure.map g μ) t = ∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν
Tactic: rw [Measure.setIntegral_toReal_rnDeriv (hμν.map hg),
        Measure.setIntegral_toReal_rnDeriv hμν, measureReal_def, Measure.map_apply hg ht,
        measureReal_def]
-- 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_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Measure.real (m := m𝓨) (Measure.map g μ) t = ∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ m𝓨 (Measure.restrict (Measure.map g ν) t) fun (y : 𝓨) ↦
      (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal)
    (∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν)
have rw₁ : Measure.real (m := m𝓨) (Measure.map g μ) t = μ.real (g ⁻¹' t)
Tactic: rw [Measure.setIntegral_toReal_rnDeriv (hμν.map hg),
        Measure.setIntegral_toReal_rnDeriv hμν, measureReal_def, Measure.map_apply hg ht,
        measureReal_def]
-- 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_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Measure.real (m := m𝓨) (Measure.map g μ) t = ∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν
rw₁ : Measure.real (m := m𝓨) (Measure.map g μ) t = μ.real (g ⁻¹' t)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ m𝓨 (Measure.restrict (Measure.map g ν) t) fun (y : 𝓨) ↦
      (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal)
    (∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν)
have rw₂ : ENNReal.toReal (((Measure.map g μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) t) = μ.real (g ⁻¹' t)
Tactic: rw [Measure.setIntegral_toReal_rnDeriv (hμν.map hg),
        Measure.setIntegral_toReal_rnDeriv hμν, measureReal_def, Measure.map_apply hg ht,
        measureReal_def]
-- 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_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Measure.real (m := m𝓨) (Measure.map g μ) t = ∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν
rw₁ : Measure.real (m := m𝓨) (Measure.map g μ) t = μ.real (g ⁻¹' t)
rw₂ : ENNReal.toReal (((Measure.map g μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) t) = μ.real (g ⁻¹' t)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ m𝓨 (Measure.restrict (Measure.map g ν) t) fun (y : 𝓨) ↦
      (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal)
    (∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν)
have rw₃ : ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t)) = μ.real (g ⁻¹' t)
Tactic: rw [Measure.setIntegral_toReal_rnDeriv (hμν.map hg),
        Measure.setIntegral_toReal_rnDeriv hμν, measureReal_def, Measure.map_apply hg ht,
        measureReal_def]
-- 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_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
rw : Measure.real (m := m𝓨) (Measure.map g μ) t = ∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν
rw₁ : Measure.real (m := m𝓨) (Measure.map g μ) t = μ.real (g ⁻¹' t)
rw₂ : ENNReal.toReal (((Measure.map g μ : Measure 𝓨) : (a : Set 𝓨) → ℝ≥0∞) t) = μ.real (g ⁻¹' t)
rw₃ : ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t)) = μ.real (g ⁻¹' t)
⊢ Eq (α := ℝ)
    (@integral _ _ _ _ m𝓨 (Measure.restrict (Measure.map g ν) t) fun (y : 𝓨) ↦
      (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal)
    (∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν)
have rw₄ : ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t)) = ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t))
Tactic: rw [Measure.setIntegral_toReal_rnDeriv (hμν.map hg),
        Measure.setIntegral_toReal_rnDeriv hμν, measureReal_def, Measure.map_apply hg ht,
        measureReal_def]
-- 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_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : 𝓧) in g ⁻¹' t, (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x)).toReal ∂ν)
    (∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν)
have calc : Eq (α := ℝ) (∫ (x : 𝓧) in g ⁻¹' t, (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x)).toReal ∂ν)
  (@integral _ _ _ _ m𝓨 (Measure.restrict (Measure.map g ν) t) fun (y : 𝓨) ↦
    (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal)
Tactic: calc ∫ x in g ⁻¹' t, ((μ.map g).rnDeriv (ν.map g) (g x)).toReal ∂ν
    _ = ∫ y in t, ((μ.map g).rnDeriv (ν.map g) y).toReal ∂(ν.map g) := by
      rw [setIntegral_map ht _ hg.aemeasurable]
      exact Measurable.aestronglyMeasurable (by fun_prop)
    _ = ∫ x in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν := by
      rw [Measure.setIntegral_toReal_rnDeriv (hμν.map hg),
        Measure.setIntegral_toReal_rnDeriv hμν, measureReal_def, Measure.map_apply hg ht,
        measureReal_def]
-- 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_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
t : Set 𝓨
ht : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
calc :
  Eq (α := ℝ) (∫ (x : 𝓧) in g ⁻¹' t, (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x)).toReal ∂ν)
    (@integral _ _ _ _ m𝓨 (Measure.restrict (Measure.map g ν) t) fun (y : 𝓨) ↦
      (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal)
⊢ Eq (α := ℝ) (∫ (x : 𝓧) in g ⁻¹' t, (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x)).toReal ∂ν)
    (∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν)
have calc₁ : Eq (α := ℝ)
  (@integral _ _ _ _ m𝓨 (Measure.restrict (Measure.map g ν) t) fun (y : 𝓨) ↦
    (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal)
  (∫ (x : 𝓧) in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν)
Tactic: calc ∫ x in g ⁻¹' t, ((μ.map g).rnDeriv (ν.map g) (g x)).toReal ∂ν
    _ = ∫ y in t, ((μ.map g).rnDeriv (ν.map g) y).toReal ∂(ν.map g) := by
      rw [setIntegral_map ht _ hg.aemeasurable]
      exact Measurable.aestronglyMeasurable (by fun_prop)
    _ = ∫ x in g ⁻¹' t, (μ.rnDeriv ν x).toReal ∂ν := by
      rw [Measure.setIntegral_toReal_rnDeriv (hμν.map hg),
        Measure.setIntegral_toReal_rnDeriv hμν, measureReal_def, Measure.map_apply hg ht,
        measureReal_def]
-- 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_1 : SigmaFinite (ν.trim ⋯)
this : SigmaFinite ν
⊢ AEStronglyMeasurable (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) ν
have refine_3 : ∀ (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.ennreal_toReal fun s hs ↦ ?_).aestronglyMeasurable
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (hypothesis)
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 ν)
⊢ (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae ν]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
have this : SigmaFinite ν
Tactic: have : SigmaFinite ν := SigmaFinite.of_map _ hg.aemeasurable hσ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (hypothesis)
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 ν
⊢ (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae ν]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
have h_ne_top1 : ∀ᵐ (x : 𝓧) ∂ν, Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞
Tactic: have h_ne_top1 : ∀ᵐ x ∂ν, (μ.map g).rnDeriv (ν.map g) (g x) ≠ ∞ :=
    ae_of_ae_map hg.aemeasurable (Measure.rnDeriv_ne_top (μ.map g) (ν.map g))
-- 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 : ∀ᵐ (x : 𝓧) ∂ν, Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞
⊢ ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞
have refine : ∫⁻ (x : 𝓧), μ.rnDeriv ν x ∂ν ≠ ∞
Tactic: refine condLExp_ne_top ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym (hypothesis)
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 : ∀ᵐ (x : 𝓧) ∂ν, Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞
⊢ (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae ν]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
have h_ne_top2 : ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞
Tactic: have h_ne_top2 : ∀ᵐ x ∂ν, ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞ := by
    refine condLExp_ne_top ?_
    simp [Measure.lintegral_rnDeriv hμν]
-- 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 : ∀ᵐ (x : 𝓧) ∂ν, Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞
h_ne_top2 : ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞
⊢ (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae ν]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
have refine_2 : ∀
  (h_condExp :
    (ae ν).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x).toReal)
      ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨]),
  (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae ν]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
Tactic: have h_condExp := toReal_condLExp (m𝓨.comap g) (f := μ.rnDeriv ν) (μ := ν) (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
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
this : SigmaFinite ν
h_ne_top1 : ∀ᵐ (x : 𝓧) ∂ν, Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞
h_ne_top2 : ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞
refine_2 :
  ∀
    (h_condExp :
      (ae ν).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x).toReal)
        ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨]),
    (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 ν]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
have refine_1 : ∫⁻ (x : 𝓧), μ.rnDeriv ν x ∂ν ≠ ∞
Tactic: have h_condExp := toReal_condLExp (m𝓨.comap g) (f := μ.rnDeriv ν) (μ := ν) (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
hσ : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
this : SigmaFinite ν
h_ne_top1 : ∀ᵐ (x : 𝓧) ∂ν, Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g x) ≠ ∞
h_ne_top2 : ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞
h_condExp :
  (ae ν).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ (ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x).toReal)
    ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | MeasurableSpace.comap g m𝓨]
⊢ (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae ν]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]
have h : ∀ (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
Tactic: filter_upwards [toReal_rnDeriv_map hμν hg, h_condExp, h_ne_top1, h_ne_top2]
    with x hx h_condExp h_ne_top1 h_ne_top2