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
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
hg₁ : StronglyMeasurable (β := ℝ) ν[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𝓨]

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 ν)
⊢ (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:
toReal_rnDeriv_map hμν hg

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
inst_1 : 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𝓨]

Tactic:
exact toReal_rnDeriv_map hμν hg

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
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
⊢ StronglyMeasurable (β := ℝ) fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal

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 ℝ) (hs : MeasurableSet s),
    MeasurableSet.{u_1} (α := 𝓧)
      ((fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal) ⁻¹' s)
⊢ StronglyMeasurable (β := ℝ) fun (a : 𝓧) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) (g a)).toReal

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 ℝ
hs : MeasurableSet s
⊢ Measurable (β := ℝ) fun (a : 𝓨) ↦ (Measure.rnDeriv (m := m𝓨) (Measure.map g μ) (Measure.map g ν) a).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
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
s : Set ℝ
hs : MeasurableSet s
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
⊢ MeasurableSet.{u_1} (α := 𝓧)
    ((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), ?_⟩
-- 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 ℝ
hs : MeasurableSet s
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
⊢ 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:
rw [← Set.preimage_comp]

Premises used: Set.preimage_comp
-- 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 ℝ
hs : MeasurableSet s
⊢ (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:
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
inst_1 : SigmaFinite (m0 := m𝓨) (Measure.map g ν)
⊢ StronglyMeasurable (β := ℝ) ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | MeasurableSpace.comap g m𝓨]

Tactic:
fun_prop
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
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]
⊢ (ae (ν.trim hm)).EventuallyEq (β := ℝ) (fun (x : 𝓧) ↦ ((μ.trim hm).rnDeriv (ν.trim hm) x).toReal)
    ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m]

Tactic:
simp_rw [trim_eq_map hm]

Premises used: MeasureTheory.trim_eq_map
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
rwa rwa₁ rwa₂ rwa₃ : SigmaFinite (ν.trim hm)
⊢ SigmaFinite (m0 := m) (Measure.map id ν)

Tactic:
rwa [← trim_eq_map hm]

Premises used: MeasureTheory.trim_eq_map
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
hsf : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
⊢ SigmaFinite (m0 := m) (Measure.map id ν)

Tactic:
have : SigmaFinite (@Measure.map _ _ m𝓧 m id ν) := by rwa [← trim_eq_map hm]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 (ν.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]

Tactic:
have h := toReal_rnDeriv_map_ae_eq_trim hμν (measurable_id'' hm)
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 (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

Premises used: MeasureTheory.trim_eq_map, id_def, MeasurableSpace.comap_id
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 (a : 𝓧) ↦ (Measure.rnDeriv (m := m) (Measure.map id μ) (Measure.map id ν) a).toReal)
    ν[fun (a : 𝓧) ↦ (μ.rnDeriv ν a).toReal | m]

Tactic:
h
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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
h₂ h₃ : Measure 𝓧 = Measure 𝓧 → 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]

Tactic:
convert! h
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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₁ h₂ : m = m
⊢ m = MeasurableSpace.comap id m

Tactic:
rw [MeasurableSpace.comap_id]

Premises used: MeasurableSpace.comap_id
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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 𝓧
h₁ h₂ : m = m
⊢ m = MeasurableSpace.comap id m

Tactic:
rw [MeasurableSpace.comap_id]

Premises used: MeasurableSpace.comap_id
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
Goal:
𝓧 : Type u_1
m m𝓧 : MeasurableSpace 𝓧
μ ν : Measure 𝓧
hm : m ≤ m𝓧
inst : IsFiniteMeasure μ
inst_1 : SigmaFinite (ν.trim hm)
hμν : μ ≪ ν
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)
⊢ (μ.trim hm).rnDeriv (ν.trim hm) =ᶠ[ae (ν.trim hm)] fun (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

Premises used: MeasureTheory.toReal_rnDeriv_trim, MeasureTheory.Measure.trim, MeasureTheory.Measure.rnDeriv_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.RadonNikodym
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
h₁ h₂ : (μ.trim hm).rnDeriv (ν.trim hm) x = (μ.trim hm).rnDeriv (ν.trim hm) x
⊢ (μ.trim hm).rnDeriv (ν.trim hm) x = ENNReal.ofReal (ν[fun (x : 𝓧) ↦ (μ.rnDeriv ν x).toReal | m] x)

Tactic:
rw [← hx, ENNReal.ofReal_toReal hx_ne_top]

Premises used: ENNReal.ofReal_toReal
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
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 ∂μ)
refine_3 : AEStronglyMeasurable (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm)) μ
⊢ SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm) =ᶠ[ae μ] μ[f | m]

Tactic:
refine ae_eq_condExp_of_forall_setIntegral_eq hm hf ?_ ?_ ?_

Premises used: MeasureTheory.ae_eq_condExp_of_forall_setIntegral_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ ∀ (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:
fun _ _ _ => (integrable_of_integrable_trim hm
      (SignedMeasure.integrable_rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm))).integrableOn

Premises used: MeasureTheory.VectorMeasure.trim, MeasureTheory.Measure.withDensityᵥ, MeasureTheory.integrable_of_integrable_trim, MeasureTheory.Measure.trim, MeasureTheory.Integrable.integrableOn, MeasureTheory.SignedMeasure.integrable_rnDeriv
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ ∀ (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:
exact fun _ _ _ => (integrable_of_integrable_trim hm
      (SignedMeasure.integrable_rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm))).integrableOn

Premises used: MeasureTheory.VectorMeasure.trim, MeasureTheory.Measure.withDensityᵥ, MeasureTheory.integrable_of_integrable_trim, MeasureTheory.Measure.trim, MeasureTheory.Integrable.integrableOn, MeasureTheory.SignedMeasure.integrable_rnDeriv
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
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
refine_2 :
  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 ∂μ)
⊢ 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:
_
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
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∞)
rw :
  (↑((μ.trim hm).withDensityᵥ (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm))) :
      Set α → ℝ)
    s
| ∫ (x : α) in s, f x ∂μ

Tactic:
rw [← hf.withDensityᵥ_trim_eq_integral hm hs,
      ← SignedMeasure.withDensityᵥ_rnDeriv_eq ((μ.withDensityᵥ f).trim hm) (μ.trim hm)
        (hf.withDensityᵥ_trim_absolutelyContinuous hm)]

Premises used: MeasureTheory.VectorMeasure.trim, MeasureTheory.Measure.withDensityᵥ, MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq, MeasureTheory.Measure.trim, MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous, MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
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∞)
refine_2 :
  ∫ (x : α) in s, SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm) x ∂μ =
    (↑((μ.trim hm).withDensityᵥ (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm))) :
        Set α → ℝ)
      s
⊢ Eq (α := ℝ) (∫ (x : α) in s, SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm) x ∂μ)
    (∫ (x : α) in s, f x ∂μ)

Tactic:
conv_rhs => rw [← hf.withDensityᵥ_trim_eq_integral hm hs,
      ← SignedMeasure.withDensityᵥ_rnDeriv_eq ((μ.withDensityᵥ f).trim hm) (μ.trim hm)
        (hf.withDensityᵥ_trim_absolutelyContinuous hm)]

Premises used: MeasureTheory.VectorMeasure.trim, MeasureTheory.Measure.withDensityᵥ, MeasureTheory.SignedMeasure.withDensityᵥ_rnDeriv_eq, MeasureTheory.Measure.trim, MeasureTheory.Integrable.withDensityᵥ_trim_absolutelyContinuous, MeasureTheory.Integrable.withDensityᵥ_trim_eq_integral
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
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∞)
rw : StronglyMeasurable (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm))
⊢ ∫ (x : α) in s, SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm) x ∂μ =
    (↑((μ.trim hm).withDensityᵥ (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm))) :
        Set α → ℝ)
      s

Tactic:
rw [withDensityᵥ_apply
      (SignedMeasure.integrable_rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm)) hs,
      ← setIntegral_trim hm _ hs]

Premises used: MeasureTheory.VectorMeasure.trim, MeasureTheory.Measure.withDensityᵥ, MeasureTheory.setIntegral_trim, MeasureTheory.Measure.trim, MeasureTheory.withDensityᵥ_apply, MeasureTheory.SignedMeasure.integrable_rnDeriv
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
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∞)
⊢ StronglyMeasurable (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm))

Tactic:
(SignedMeasure.measurable_rnDeriv _ _).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, MeasureTheory.SignedMeasure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
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∞)
⊢ StronglyMeasurable (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm))

Tactic:
exact (SignedMeasure.measurable_rnDeriv _ _).stronglyMeasurable

Premises used: Measurable.stronglyMeasurable, MeasureTheory.SignedMeasure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ AEStronglyMeasurable (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm)) μ

Tactic:
(SignedMeasure.measurable_rnDeriv _ _).stronglyMeasurable.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, Measurable.stronglyMeasurable, MeasureTheory.SignedMeasure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ AEStronglyMeasurable (SignedMeasure.rnDeriv (VectorMeasure.trim (μ.withDensityᵥ f) hm) (μ.trim hm)) μ

Tactic:
exact (SignedMeasure.measurable_rnDeriv _ _).stronglyMeasurable.aestronglyMeasurable

Premises used: MeasureTheory.StronglyMeasurable.aestronglyMeasurable, Measurable.stronglyMeasurable, MeasureTheory.SignedMeasure.measurable_rnDeriv
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
pos : ∀ (hf : Integrable f μ), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
neg : ∀ (hf : ¬Integrable f μ), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ

Tactic:
by_cases hf : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
neg : 0 ≤ eLpNorm f 1 μ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ

Tactic:
rw [condExp_of_not_integrable hf, eLpNorm_zero]

Premises used: MeasureTheory.eLpNorm_zero, MeasureTheory.condExp_of_not_integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ 0 ≤ eLpNorm f 1 μ

Tactic:
zero_le

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : ¬Integrable f μ
⊢ 0 ≤ eLpNorm f 1 μ

Tactic:
exact zero_le

Premises used: zero_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
pos : ∀ (hm : m ≤ m0), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
neg : ∀ (hm : ¬m ≤ m0), eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ

Tactic:
by_cases hm : m ≤ m0
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : ¬m ≤ m0
neg : 0 ≤ eLpNorm f 1 μ
⊢ eLpNorm μ[f | m] 1 μ ≤ eLpNorm f 1 μ

Tactic:
rw [condExp_of_not_le hm, eLpNorm_zero]

Premises used: MeasureTheory.eLpNorm_zero, MeasureTheory.condExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
f : α → ℝ
hf : Integrable f μ
hm : ¬m ≤ m0
⊢ 0 ≤ eLpNorm f 1 μ

Tactic:
zero_le

Premises used: zero_le