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 μ)
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
refine :
  ∀ (x : α)
    (hx :
      Eq (α := ℝ≥0∞)
        ((fun (x : α) ↦
            (↑(nnnorm (E := ℝ)
                  ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) :
                      α → ℝ)
                    x)) :
              ℝ≥0∞))
          x)
        (0 x)),
    Eq (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x)
      (0 x)
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) 0

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

Premises used: 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 :
  (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞)
    (fun (x : α) ↦
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞))
    0
x : α
hx :
  (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞) =
    0 x
⊢ (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞) =
    0

Tactic:
rw [Pi.zero_apply] at hx ⊢

Premises used: Pi.zero_apply
-- 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
x : α
hx :
  (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞) =
    0
rwa :
  ∀
    (hx :
      nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x) =
        0),
    Eq (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x) 0
rwa₁ rwa₂ rwa₃ rwa₄ :
  ∀
    (hx :
      Eq (α := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x)
        0),
    Eq (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x) 0
⊢ Eq (α := ℝ)
    ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ) x) 0

Tactic:
rwa [ENNReal.coe_eq_zero, nnnorm_eq_zero] at hx

Premises used: ENNReal.coe_eq_zero, nnnorm_eq_zero
-- 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
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)

Tactic:
Measurable.coe_nnreal_ennreal (Measurable.nnnorm ?_)

Premises used: Measurable.coe_nnreal_ennreal, Measurable.nnnorm
-- 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
refine :
  Measurable.{u_1, 0} (α := α) (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦
    (↑(nnnorm (E := ℝ)
          ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
            x)) :
      ℝ≥0∞)

Tactic:
refine Measurable.coe_nnreal_ennreal (Measurable.nnnorm ?_)

Premises used: Measurable.coe_nnreal_ennreal, Measurable.nnnorm
-- 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
⊢ Measurable.{u_1, 0} (α := α) (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)

Tactic:
(Lp.stronglyMeasurable _).measurable

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.measurable
-- 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
⊢ Measurable.{u_1, 0} (α := α) (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)

Tactic:
exact (Lp.stronglyMeasurable _).measurable

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.measurable
-- 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
suffices :
  ∫⁻ (x : α) in s,
      (↑(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:
suffices h_nnnorm_eq_zero : ∫⁻ x in s, ‖(condExpL2 ℝ ℝ hm f : α → ℝ) x‖₊ ∂μ = 0 by
    rw [lintegral_eq_zero_iff] at h_nnnorm_eq_zero
    · refine h_nnnorm_eq_zero.mono fun x hx => ?_
      dsimp only at hx
      rw [Pi.zero_apply] at hx ⊢
      · rwa [ENNReal.coe_eq_zero, nnnorm_eq_zero] at hx
    · refine Measurable.coe_nnreal_ennreal (Measurable.nnnorm ?_)
      exact (Lp.stronglyMeasurable _).measurable
-- 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
rw :
  ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ ≤
    0
⊢ ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ =
    0

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- 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
⊢ ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ ≤
    0

Tactic:
(lintegral_nnnorm_condExpL2_le hs hμs f).trans (le_of_eq ?_)

Premises used: MeasureTheory.lintegral_nnnorm_condExpL2_le, LE.le.trans, le_of_eq
-- 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
refine : ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ = 0
⊢ ∫⁻ (x : α) in s,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) f) : ↥(Lp ℝ 2 μ)) : α →ₘ[μ] ℝ) : α → ℝ)
              x)) :
        ℝ≥0∞) ∂μ ≤
    0

Tactic:
refine (lintegral_nnnorm_condExpL2_le hs hμs f).trans (le_of_eq ?_)

Premises used: MeasureTheory.lintegral_nnnorm_condExpL2_le, LE.le.trans, le_of_eq
-- 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
rw : (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞)) 0
rw₁ : Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in s, (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) ∂μ = 0

Tactic:
rw [lintegral_eq_zero_iff]

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
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞)) 0

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

Premises used: Filter.EventuallyEq, 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
refine :
  ∀ (x : α) (hx : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x = 0 x),
    Eq (α := ℝ≥0∞) ((fun (x : α) ↦ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞)) x) (0 x)
⊢ (ae (μ.restrict s)).EventuallyEq (β := ℝ≥0∞) (fun (x : α) ↦ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞)) 0

Tactic:
refine hf.mono fun x hx => ?_

Premises used: 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
x : α
hx : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x = 0 x
rw : (↑(nnnorm (E := ℝ) (0 x)) : ℝ≥0∞) = 0 x
⊢ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞) = 0 x

Tactic:
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 μ)
hf : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) =ᶠ[ae (μ.restrict s)] 0
x : α
hx : (↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x = 0 x
⊢ (↑(nnnorm (E := ℝ) (0 x)) : ℝ≥0∞) = 0 x

Tactic:
simp
-- 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
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞)

Tactic:
(Lp.stronglyMeasurable _).enorm (ε := ℝ)

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.enorm
-- 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
⊢ Measurable (β := ℝ≥0∞) fun (x : α) ↦ (↑‖(↑(↑f : α →ₘ[μ] ℝ) : α → ℝ) x‖₊ : ℝ≥0∞)

Tactic:
exact (Lp.stronglyMeasurable _).enorm (ε := ℝ)

Premises used: MeasureTheory.Lp.stronglyMeasurable, MeasureTheory.StronglyMeasurable.enorm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (a : α) in t,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                            (indicatorConstLp (s := s) 2 hs hμs 1)) :
                        ↥(Lp ℝ 2 μ)) :
                    α →ₘ[μ] ℝ) :
                α → ℝ)
              a)) :
        ℝ≥0∞) ∂μ ≤
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ t)

Tactic:
(lintegral_nnnorm_condExpL2_le ht hμt _).trans (le_of_eq ?_)

Premises used: MeasureTheory.lintegral_nnnorm_condExpL2_le, LE.le.trans, le_of_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine :
  ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ t)
⊢ ∫⁻ (a : α) in t,
      (↑(nnnorm (E := ℝ)
            ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ))
                            (indicatorConstLp (s := s) 2 hs hμs 1)) :
                        ↥(Lp ℝ 2 μ)) :
                    α →ₘ[μ] ℝ) :
                α → ℝ)
              a)) :
        ℝ≥0∞) ∂μ ≤
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ t)

Tactic:
refine (lintegral_nnnorm_condExpL2_le ht hμt _).trans (le_of_eq ?_)

Premises used: MeasureTheory.lintegral_nnnorm_condExpL2_le, LE.le.trans, le_of_eq
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
    ∫⁻ (x : α) in t, s.indicator (fun (x : α) ↦ 1) x ∂μ

Tactic:
lintegral_congr_ae (ae_restrict_of_ae ?_)

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine :
  ∀ᵐ (x : α) ∂μ,
    Eq (α := ℝ≥0∞)
      ((fun (x : α) ↦ (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞))
        x)
      (s.indicator (fun (x : α) ↦ 1) x)
⊢ ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
    ∫⁻ (x : α) in t, s.indicator (fun (x : α) ↦ 1) x ∂μ

Tactic:
refine lintegral_congr_ae (ae_restrict_of_ae ?_)

Premises used: MeasureTheory.lintegral_congr_ae, MeasureTheory.ae_restrict_of_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ,
    Eq (α := ℝ≥0∞)
      ((fun (x : α) ↦ (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞))
        x)
      (s.indicator (fun (x : α) ↦ 1) x)

Tactic:
(@indicatorConstLp_coeFn _ _ _ 2 _ _ _ hs hμs (1 : ℝ)).mono fun x hx => ?_

Premises used: Filter.Eventually.mono, MeasureTheory.indicatorConstLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine :
  ∀ (x : α)
    (hx :
      Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)
        (s.indicator (fun (x : α) ↦ 1) x)),
    Eq (α := ℝ≥0∞)
      ((fun (x : α) ↦ (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞))
        x)
      (s.indicator (fun (x : α) ↦ 1) x)
⊢ ∀ᵐ (x : α) ∂μ,
    Eq (α := ℝ≥0∞)
      ((fun (x : α) ↦ (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞))
        x)
      (s.indicator (fun (x : α) ↦ 1) x)

Tactic:
refine (@indicatorConstLp_coeFn _ _ _ 2 _ _ _ hs hμs (1 : ℝ)).mono fun x hx => ?_

Premises used: Filter.Eventually.mono, MeasureTheory.indicatorConstLp_coeFn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) (s.indicator (fun (x : α) ↦ 1) x)
rw : (↑(nnnorm (E := ℝ) (s.indicator (fun (x : α) ↦ 1) x)) : ℝ≥0∞) = s.indicator (fun (x : α) ↦ 1) x
⊢ (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) =
    s.indicator (fun (x : α) ↦ 1) x

Tactic:
rw [hx]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) (s.indicator (fun (x : α) ↦ 1) x)
pos : x ∈ s → (↑(nnnorm (E := ℝ) 1) : ℝ≥0∞) = 1
neg : x ∉ s → (↑(nnnorm (E := ℝ) 0) : ℝ≥0∞) = 0
⊢ (↑(nnnorm (E := ℝ) (if x ∈ s then 1 else 0)) : ℝ≥0∞) = if x ∈ s then 1 else 0

Tactic:
split_ifs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) (s.indicator (fun (x : α) ↦ 1) x)
h : x ∈ s
⊢ (↑(nnnorm (E := ℝ) 1) : ℝ≥0∞) = 1

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx : Eq (α := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x) (s.indicator (fun (x : α) ↦ 1) x)
h : x ∉ s
⊢ (↑(nnnorm (E := ℝ) 0) : ℝ≥0∞) = 0

Tactic:
simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
    ∫⁻ (x : α) in t, s.indicator (fun (x : α) ↦ 1) x ∂μ

Tactic:
have h_eq :
    ∫⁻ x in t, ‖(indicatorConstLp 2 hs hμs (1 : ℝ)) x‖₊ ∂μ =
      ∫⁻ x in t, s.indicator (fun _ => (1 : ℝ≥0∞)) x ∂μ := by
    refine lintegral_congr_ae (ae_restrict_of_ae ?_)
    refine (@indicatorConstLp_coeFn _ _ _ 2 _ _ _ hs hμs (1 : ℝ)).mono fun x hx => ?_
    dsimp only
    rw [hx]
    classical
    simp_rw [Set.indicator_apply]
    split_ifs <;> simp
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hm : m ≤ m0
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
ht : MeasurableSet t
hμt : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_eq :
  ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
    ∫⁻ (x : α) in t, s.indicator (fun (x : α) ↦ 1) x ∂μ
rw :
  HMul.hMul (α := ℝ≥0∞) (β := ℝ≥0∞) (1 : ℝ≥0∞) ((μ.restrict (s ∩ t) : (a : Set α) → ℝ≥0∞) Set.univ : ℝ≥0∞) =
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ t)
⊢ ∫⁻ (x : α) in t, (↑(nnnorm (E := ℝ) ((↑(↑(indicatorConstLp (s := s) 2 hs hμs 1) : α →ₘ[μ] ℝ) : α → ℝ) x)) : ℝ≥0∞) ∂μ =
    (μ : (a : Set α) → ℝ≥0∞) (s ∩ t)

Tactic:
rw [h_eq, lintegral_indicator hs, lintegral_const, Measure.restrict_restrict hs]

Premises used: MeasureTheory.lintegral_const, MeasureTheory.Measure.restrict_restrict, MeasureTheory.lintegral_indicator