awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 𝓨
left : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn (ε := ℝ) (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal)
    (g ⁻¹' t) ν

Tactic:
Integrable.integrableOn (Measure.integrable_toReal_rnDeriv.comp_measurable hg)

Premises used: MeasureTheory.Integrable.comp_measurable, MeasureTheory.Integrable.integrableOn, MeasureTheory.Measure.integrable_toReal_rnDeriv
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 𝓨
left : MeasurableSet t
h : LT.lt (α := ℝ≥0∞) ((ν : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t) : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ IntegrableOn (ε := ℝ) (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal)
    (g ⁻¹' t) ν

Tactic:
exact Integrable.integrableOn (Measure.integrable_toReal_rnDeriv.comp_measurable hg)

Premises used: MeasureTheory.Integrable.comp_measurable, MeasureTheory.Integrable.integrableOn, MeasureTheory.Measure.integrable_toReal_rnDeriv
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 :
  AEStronglyMeasurable (β := ℝ) (m₀ := m𝓨)
    (fun (y : 𝓨) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal) (Measure.map g ν)
⊢ 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:
rw [setIntegral_map ht _ hg.aemeasurable]

Premises used: Measurable.aemeasurable, MeasureTheory.setIntegral_map
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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∞)
⊢ Measurable (β := ℝ) fun (y : 𝓨) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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∞)
⊢ AEStronglyMeasurable (β := ℝ) (m₀ := m𝓨)
    (fun (y : 𝓨) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) y).toReal) (Measure.map g ν)

Tactic:
exact Measurable.aestronglyMeasurable (by fun_prop)

Premises used: Measurable.aestronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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)
rw₄ rw₅ : ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) (g ⁻¹' t)) = ENNReal.toReal ((μ : (a : Set 𝓧) → ℝ≥0∞) (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 ∂ν)

Tactic:
rw [Measure.setIntegral_toReal_rnDeriv (hμν.map hg),
        Measure.setIntegral_toReal_rnDeriv hμν, measureReal_def, Measure.map_apply hg ht,
        measureReal_def]

Premises used: MeasureTheory.Measure.map_apply, MeasureTheory.measureReal_def, MeasureTheory.Measure.AbsolutelyContinuous.map, MeasureTheory.Measure.setIntegral_toReal_rnDeriv
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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)
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 ∂ν)
⊢ 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 ∂ν)

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]

Premises used: MeasureTheory.Measure.map
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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) ν

Tactic:
(Measurable.ennreal_toReal fun s hs ↦ ?_).aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, Measurable.ennreal_toReal
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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_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)
⊢ AEStronglyMeasurable (β := ℝ)
    (fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) ν

Tactic:
refine (Measurable.ennreal_toReal fun s hs ↦ ?_).aestronglyMeasurable

Premises used: Measurable.aestronglyMeasurable, Measurable.ennreal_toReal
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ν
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:
⟨_, Measure.measurable_rnDeriv _ _ hs, rfl⟩

Premises used: MeasurableSet, And.intro, Exists.intro, MeasureTheory.Measure.measurable_rnDeriv, rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ν
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:
exact ⟨_, Measure.measurable_rnDeriv _ _ hs, rfl⟩
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ν)
⊢ SigmaFinite ν

Tactic:
have : SigmaFinite ν := SigmaFinite.of_map _ hg.aemeasurable hσ
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ν
⊢ ∀ᵐ (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))
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ≠ ∞

Tactic:
condLExp_ne_top ?_

Premises used: MeasureTheory.condLExp_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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) ≠ ∞
refine : ∫⁻ (x : 𝓧), μ.rnDeriv ν x ∂ν ≠ ∞
⊢ ∀ᵐ (x : 𝓧) ∂ν, ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞

Tactic:
refine condLExp_ne_top ?_

Premises used: MeasureTheory.condLExp_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ν x ∂ν ≠ ∞

Tactic:
simp [Measure.lintegral_rnDeriv hμν]

Premises used: MeasureTheory.Measure.lintegral_rnDeriv
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ≠ ∞

Tactic:
have h_ne_top2 : ∀ᵐ x ∂ν, ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨] x ≠ ∞ := by
    refine condLExp_ne_top ?_
    simp [Measure.lintegral_rnDeriv hμν]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ≠ ∞
⊢ AEMeasurable (μ.rnDeriv ν) ν

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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𝓨]
refine_1 : ∫⁻ (x : 𝓧), μ.rnDeriv ν x ∂ν ≠ ∞
⊢ (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) ?_
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ≠ ∞
⊢ ∫⁻ (x : 𝓧), μ.rnDeriv ν x ∂ν ≠ ∞

Tactic:
simp [Measure.lintegral_rnDeriv hμν]

Premises used: MeasureTheory.Measure.lintegral_rnDeriv
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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𝓨]
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
⊢ (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) =ᶠ[ae ν]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]

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

Premises used: MeasureTheory.toReal_rnDeriv_map
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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
h₁ h₂ h₃ 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
⊢ 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

Premises used: ENNReal.toReal_eq_toReal_iff'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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)
hg₁ : StronglyMeasurable ν⁻[μ.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𝓨]

Tactic:
rw [StronglyMeasurable.ae_eq_trim_iff]

Premises used: MeasureTheory.StronglyMeasurable.ae_eq_trim_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ν]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]

Tactic:
rnDeriv_map hμν hg

Premises used: MeasureTheory.rnDeriv_map
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ν]
    ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]

Tactic:
exact rnDeriv_map hμν hg

Premises used: MeasureTheory.rnDeriv_map
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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)

Tactic:
Measurable.stronglyMeasurable fun s hs ↦ ?_

Premises used: Measurable.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ν)
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)
⊢ StronglyMeasurable (β := ℝ≥0∞) fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)

Tactic:
refine Measurable.stronglyMeasurable fun s hs ↦ ?_

Premises used: Measurable.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ℝ≥0∞
hs : MeasurableSet s
⊢ Measurable (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν))

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ℝ≥0∞
hs : MeasurableSet s
⊢ g ⁻¹' Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) ⁻¹' s =
    (fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) ⁻¹' s

Tactic:
grind
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ℝ≥0∞
hs : MeasurableSet s
⊢ MeasurableSet.{u_1} (α := 𝓧)
    ((fun (a : 𝓧) ↦ Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)) ⁻¹' s)

Tactic:
exact ⟨((μ.map g).rnDeriv (ν.map g)) ⁻¹' s, hs.preimage (by fun_prop), by grind⟩
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 ν⁻[μ.rnDeriv ν|MeasurableSpace.comap g m𝓨]

Tactic:
fun_prop