awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)

Tactic:
have hg_nnnorm_eq : (fun x => (‖g x‖₊ : ℝ≥0∞)) =ᵐ[μ.restrict s] fun x =>
      (‖(condExpL2 ℝ ℝ hm f : α → ℝ) x‖₊ : ℝ≥0∞) := by
    refine hg_eq_restrict.mono fun x hx => ?_
    dsimp only
    simp_rw [hx]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
rw : ∫⁻ (a : α) in s, (↑‖g a‖₊ : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ
⊢ ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ ≤
    ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ

Tactic:
rw [lintegral_congr_ae hg_nnnorm_eq.symm]

Premises used: MeasureTheory.lintegral_congr_ae, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
⊢ ∫⁻ (a : α) in s, (↑‖g a‖₊ : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ

Tactic:
lintegral_enorm_le_of_forall_fin_meas_integral_eq
    hm (Lp.stronglyMeasurable f) ?_ ?_ ?_ ?_ hs hμs

Premises used: MeasureTheory.lintegral_enorm_le_of_forall_fin_meas_integral_eq, MeasureTheory.Lp.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
refine_1 : IntegrableOn (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) s μ
refine_2 : StronglyMeasurable g
refine_3 : IntegrableOn g s μ
refine_4 :
  ∀ (t : Set α),
    MeasurableSet t →
      LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x ∂μ)
⊢ ∫⁻ (a : α) in s, (↑‖g a‖₊ : ℝ≥0∞) ∂μ ≤ ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ

Tactic:
refine lintegral_enorm_le_of_forall_fin_meas_integral_eq
    hm (Lp.stronglyMeasurable f) ?_ ?_ ?_ ?_ hs hμs

Premises used: MeasureTheory.lintegral_enorm_le_of_forall_fin_meas_integral_eq, MeasureTheory.Lp.stronglyMeasurable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
⊢ IntegrableOn (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) s μ

Tactic:
integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs

Premises used: fact_one_le_two_ennreal, MeasureTheory.integrableOn_Lp_of_measure_ne_top, Fact.elim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
⊢ IntegrableOn (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) s μ

Tactic:
exact integrableOn_Lp_of_measure_ne_top f fact_one_le_two_ennreal.elim hμs

Premises used: fact_one_le_two_ennreal, MeasureTheory.integrableOn_Lp_of_measure_ne_top, Fact.elim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
⊢ StronglyMeasurable g

Tactic:
hg_meas
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
⊢ StronglyMeasurable g

Tactic:
exact hg_meas
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
refine_3 :
  Integrable (ε := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
    (μ.restrict s)
⊢ IntegrableOn g s μ

Tactic:
rw [IntegrableOn, integrable_congr hg_eq_restrict]

Premises used: MeasureTheory.integrable_congr, MeasureTheory.IntegrableOn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
⊢ Integrable (ε := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
    (μ.restrict s)

Tactic:
integrableOn_condExpL2_of_measure_ne_top hm hμs f

Premises used: MeasureTheory.IntegrableOn, MeasureTheory.integrableOn_condExpL2_of_measure_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
⊢ Integrable (ε := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
    (μ.restrict s)

Tactic:
exact integrableOn_condExpL2_of_measure_ne_top hm hμs f

Premises used: MeasureTheory.integrableOn_condExpL2_of_measure_ne_top
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_4 :
  Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ)
    (∫ (x : α) in t,
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x ∂μ)
⊢ Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ) (∫ (x : α) in t, (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x ∂μ)

Tactic:
rw [← integral_condExpL2_eq_of_fin_meas_real (hm := hm) f ht hμt.ne]

Premises used: MeasureTheory.integral_condExpL2_eq_of_fin_meas_real, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ)
    (∫ (x : α) in t,
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x ∂μ)

Tactic:
setIntegral_congr_ae (hm t ht) (hg_eq.mono fun x hx _ => hx)

Premises used: MeasureTheory.setIntegral_congr_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
h_meas : AEStronglyMeasurable (β := ℝ)
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) μ :=
  ⋯
g : α → ℝ :=
  Exists.choose (p := fun (g : α → ℝ) ↦
    StronglyMeasurable g ∧
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
          α → ℝ) =ᶠ[ae μ]
        g)
    h_meas
hg_meas : StronglyMeasurable g
hg_eq :
  g =ᶠ[ae μ] (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_eq_restrict :
  g =ᶠ[ae (μ.restrict s)]
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
hg_nnnorm_eq :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖g x‖₊ : ℝ≥0∞)) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ Eq (α := ℝ) (∫ (x : α) in t, g x ∂μ)
    (∫ (x : α) in t,
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x ∂μ)

Tactic:
exact setIntegral_congr_ae (hm t ht) (hg_eq.mono fun x hx _ => hx)

Premises used: MeasureTheory.setIntegral_congr_ae, Filter.Eventually.mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero :
  ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ =
    0
rw :
  ∀
    (h_nnnorm_eq_zero :
      (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
        (fun (x : α) ↦
          (↑(nnnorm (E := ℝ)
                ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
                    α → ℝ)
                  x)) :
            ℝ≥0∞))
        0),
    (ae (μ.restrict s)).EventuallyEq (β := ℝ)
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) 0
rw₁ :
  Measurable (β := ℝ≥0∞) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) 0

Tactic:
rw [lintegral_eq_zero_iff] at h_nnnorm_eq_zero

Premises used: MeasureTheory.lintegral_eq_zero_iff
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
f : ↥(Lp ℝ 2 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
h_nnnorm_eq_zero :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞))
    0
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) 0

Tactic:
h_nnnorm_eq_zero.mono fun x hx => ?_

Premises used: Filter.EventuallyEq, Filter.Eventually.mono