-- Mathlib/MeasureTheory/Function/ConditionalExpectation/Real.lean
theorem rnDeriv_ae_eq_condExp {hm : m ≤ m0} [hμm : SigmaFinite (μ.trim hm)] {f : α → ℝ}
    (hf : Integrable f μ) :
    SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) =ᵐ[μ] μ[f|m]

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
a✝ : μ s < ⊤
⊢ StronglyMeasurable (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm))

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

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
a✝ : μ s < ⊤
⊢ ∫ (x : α) in s, SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) x ∂μ =
    ↑((μ.trim hm).withDensityᵥ (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm))) s

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

Result:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
a✝ : μ s < ⊤
⊢ StronglyMeasurable (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm))

Proof state:
case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ AEStronglyMeasurable (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm)) μ

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

Result:
no goals

Proof state:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
a✝ : μ s < ⊤
⊢ ∫ (x : α) in s, SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim 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)]

Result:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
a✝ : μ s < ⊤
⊢ ∫ (x : α) in s, SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) x ∂μ =
    ↑((μ.trim hm).withDensityᵥ (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm))) s

Proof state:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ ∀ (s : Set α),
    MeasurableSet s →
      μ s < ⊤ →
        ∫ (x : α) in s, SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) x ∂μ = ∫ (x : α) in s, f x ∂μ

Tactic:
intro s hs _

Result:
case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
s : Set α
hs : MeasurableSet s
a✝ : μ s < ⊤
⊢ ∫ (x : α) in s, SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) x ∂μ = ∫ (x : α) in s, f x ∂μ

Proof state:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) =ᶠ[ae μ] μ[f|m]

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

Result:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ ∀ (s : Set α),
    MeasurableSet s → μ s < ⊤ → IntegrableOn (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm)) s μ

case refine_2
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ ∀ (s : Set α),
    MeasurableSet s →
      μ s < ⊤ →
        ∫ (x : α) in s, SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm) x ∂μ = ∫ (x : α) in s, f x ∂μ

case refine_3
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ AEStronglyMeasurable (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm)) μ

Proof state:
case refine_1
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
f : α → ℝ
hf : Integrable f μ
⊢ ∀ (s : Set α),
    MeasurableSet s → μ s < ⊤ → IntegrableOn (SignedMeasure.rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm)) s μ

Tactic:
exact fun _ _ _ => (integrable_of_integrable_trim hm
  (SignedMeasure.integrable_rnDeriv ((μ.withDensityᵥ f).trim hm) (μ.trim hm))).integrableOn

Result:
no goals