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∞)
inst : SigmaFinite (μ.trim hm)
h :
  AEStronglyMeasurable (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              ↥(Lp ℝ 2 μ)) :
          α →ₘ[μ] ℝ) :
      α → ℝ)
    μ
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
refine_2 :
  LE.le (α := ℝ) 0
    (∫ (x : α) in t,
      AEStronglyMeasurable.mk
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        h x ∂μ)
⊢ LE.le (α := ℝ) 0
    (∫ (x : α) in t,
      AEStronglyMeasurable.mk
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        h x ∂μ.trim hm)

Tactic:
rw [← setIntegral_trim hm h.stronglyMeasurable_mk ht]

Premises used: MeasureTheory.setIntegral_trim, MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
-- 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∞)
inst : SigmaFinite (μ.trim hm)
h :
  AEStronglyMeasurable (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              ↥(Lp ℝ 2 μ)) :
          α →ₘ[μ] ℝ) :
      α → ℝ)
    μ
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
x : α
hx :
  (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ)) :
            α →ₘ[μ] ℝ) :
        α → ℝ)
      x =
    AEStronglyMeasurable.mk
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ)) :
            α →ₘ[μ] ℝ) :
        α → ℝ)
      h x
⊢ x ∈ t →
    AEStronglyMeasurable.mk
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        h x =
      (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        x

Tactic:
fun _ => hx.symm

Premises used: Eq.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∞)
inst : SigmaFinite (μ.trim hm)
h :
  AEStronglyMeasurable (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              ↥(Lp ℝ 2 μ)) :
          α →ₘ[μ] ℝ) :
      α → ℝ)
    μ
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
⊢ ∀ᵐ (x : α) ∂μ,
    x ∈ t →
      AEStronglyMeasurable.mk
          (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          h x =
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          x

Tactic:
have h_ae :
        ∀ᵐ x ∂μ, x ∈ t → h.mk _ x = (condExpL2 ℝ ℝ hm (indicatorConstLp 2 hs hμs 1) : α → ℝ) x := by
      filter_upwards [h.ae_eq_mk] with x hx using fun _ => hx.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∞)
inst : SigmaFinite (μ.trim hm)
h :
  AEStronglyMeasurable (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              ↥(Lp ℝ 2 μ)) :
          α →ₘ[μ] ℝ) :
      α → ℝ)
    μ
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_ae :
  ∀ᵐ (x : α) ∂μ,
    x ∈ t →
      AEStronglyMeasurable.mk
          (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          h x =
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          x
refine_2 : 0 ≤ μ.real (s ∩ t)
⊢ LE.le (α := ℝ) 0
    (∫ (x : α) in t,
      AEStronglyMeasurable.mk
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        h x ∂μ)

Tactic:
rw [setIntegral_congr_ae (hm t ht) h_ae,
      setIntegral_condExpL2_indicator ht hs ((le_trim hm).trans_lt hμt).ne hμs]

Premises used: MeasureTheory.setIntegral_congr_ae, MeasureTheory.setIntegral_condExpL2_indicator, MeasureTheory.le_trim, LE.le.trans_lt, 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∞)
inst : SigmaFinite (μ.trim hm)
h :
  AEStronglyMeasurable (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              ↥(Lp ℝ 2 μ)) :
          α →ₘ[μ] ℝ) :
      α → ℝ)
    μ
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_ae :
  ∀ᵐ (x : α) ∂μ,
    x ∈ t →
      AEStronglyMeasurable.mk
          (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          h x =
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          x
⊢ 0 ≤ μ.real (s ∩ t)

Tactic:
ENNReal.toReal_nonneg

Premises used: MeasureTheory.Measure.real, ENNReal.toReal_nonneg
-- 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∞)
inst : SigmaFinite (μ.trim hm)
h :
  AEStronglyMeasurable (β := ℝ)
    (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
              ↥(Lp ℝ 2 μ)) :
          α →ₘ[μ] ℝ) :
      α → ℝ)
    μ
t : Set α
ht : MeasurableSet t
hμt : LT.lt (α := ℝ≥0∞) ((μ.trim hm : (a : Set α) → ℝ≥0∞) t : ℝ≥0∞) (∞ : ℝ≥0∞)
h_ae :
  ∀ᵐ (x : α) ∂μ,
    x ∈ t →
      AEStronglyMeasurable.mk
          (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          h x =
        (↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          x
⊢ 0 ≤ μ.real (s ∩ t)

Tactic:
exact ENNReal.toReal_nonneg

Premises used: ENNReal.toReal_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : NormedSpace ℝ E
inst_3 : IsOrderedModule ℝ E
inst_4 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx : 0 ≤ x
⊢ 0 ≤ᶠ[ae μ] (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] E) : α → E)

Tactic:
EventuallyLE.trans_eq ?_ (condExpIndSMul_ae_eq_smul hm hs hμs x).symm

Premises used: Filter.EventuallyLE.trans_eq, MeasureTheory.condExpIndSMul_ae_eq_smul, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : NormedSpace ℝ E
inst_3 : IsOrderedModule ℝ E
inst_4 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx : 0 ≤ x
refine :
  EventuallyLE.{u_1, u_10} (β := E) (ae μ) 0 fun (a : α) ↦
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x
⊢ 0 ≤ᶠ[ae μ] (↑(↑(condExpIndSMul (s := s) hm hs hμs x) : α →ₘ[μ] E) : α → E)

Tactic:
refine EventuallyLE.trans_eq ?_ (condExpIndSMul_ae_eq_smul hm hs hμs x).symm

Premises used: Filter.EventuallyLE.trans_eq, MeasureTheory.condExpIndSMul_ae_eq_smul, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : NormedSpace ℝ E
inst_3 : IsOrderedModule ℝ E
inst_4 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx : 0 ≤ x
h :
  ∀ (a : α)
    (ha :
      LE.le (α := ℝ) (0 a)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          a)),
    0 a ≤
      HSMul.hSMul (α := ℝ)
        ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                    ↥(Lp ℝ 2 μ)) :
                α →ₘ[μ] ℝ) :
            α → ℝ)
          a)
        x
⊢ EventuallyLE.{u_1, u_10} (β := E) (ae μ) 0 fun (a : α) ↦
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x

Tactic:
filter_upwards [condExpL2_indicator_nonneg hm hs hμs] with a ha

Premises used: MeasureTheory.condExpL2_indicator_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : NormedSpace ℝ E
inst_3 : IsOrderedModule ℝ E
inst_4 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx : 0 ≤ x
a : α
ha :
  LE.le (α := ℝ) (0 a)
    ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ)) :
            α →ₘ[μ] ℝ) :
        α → ℝ)
      a)
⊢ 0 a ≤
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x

Tactic:
smul_nonneg ha hx

Premises used: smul_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.CondexpL2
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hm : m ≤ m0
E : Type u_10
inst : NormedAddCommGroup E
inst_1 : PartialOrder E
inst_2 : NormedSpace ℝ E
inst_3 : IsOrderedModule ℝ E
inst_4 : SigmaFinite (μ.trim hm)
hs : MeasurableSet s
hμs : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) s : ℝ≥0∞) (∞ : ℝ≥0∞)
x : E
hx : 0 ≤ x
a : α
ha :
  LE.le (α := ℝ) (0 a)
    ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                ↥(Lp ℝ 2 μ)) :
            α →ₘ[μ] ℝ) :
        α → ℝ)
      a)
⊢ 0 a ≤
    HSMul.hSMul (α := ℝ)
      ((↑(↑(↑((condExpL2 ℝ ℝ hm : (a : ↥(Lp ℝ 2 μ)) → ↥(lpMeas ℝ ℝ m 2 μ)) (indicatorConstLp (s := s) 2 hs hμs 1)) :
                  ↥(Lp ℝ 2 μ)) :
              α →ₘ[μ] ℝ) :
          α → ℝ)
        a)
      x

Tactic:
exact smul_nonneg ha hx

Premises used: smul_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
pos : ∀ (hm : m ≤ m0), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
neg : ∀ (hm : ¬m ≤ m0), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0

Tactic:
by_cases hm : m ≤ m0
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : ¬m ≤ m0
neg : EventuallyEq.{u_1, u_2} (β := E) (ae (μ.restrict s)) 0 0
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0

Tactic:
simp_rw [condExp_of_not_le hm]

Premises used: MeasureTheory.condExp_of_not_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : ¬m ≤ m0
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae (μ.restrict s)) 0 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
pos : ∀ (hμm : SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
neg : ∀ (hμm : ¬SigmaFinite (μ.trim hm)), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0

Tactic:
by_cases hμm : SigmaFinite (μ.trim hm)

Premises used: MeasureTheory.SigmaFinite, MeasureTheory.Measure.trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
neg : EventuallyEq.{u_1, u_2} (β := E) (ae (μ.restrict s)) 0 0
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0

Tactic:
simp_rw [condExp_of_not_sigmaFinite hm hμm]

Premises used: MeasureTheory.condExp_of_not_sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm : ¬SigmaFinite (μ.trim hm)
⊢ EventuallyEq.{u_1, u_2} (β := E) (ae (μ.restrict s)) 0 0

Tactic:
rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm : SigmaFinite (μ.trim hm)
⊢ SigmaFinite (μ.trim hm)

Tactic:
haveI : SigmaFinite (μ.trim hm) := hμm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
rw : SigmaFinite ((μ.trim hm).restrict s)
⊢ SigmaFinite ((μ.restrict s).trim hm)

Tactic:
rw [← restrict_trim hm _ hs]

Premises used: MeasureTheory.restrict_trim
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
⊢ SigmaFinite ((μ.trim hm).restrict s)

Tactic:
Restrict.sigmaFinite _ s

Premises used: MeasureTheory.Restrict.sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
⊢ SigmaFinite ((μ.trim hm).restrict s)

Tactic:
exact Restrict.sigmaFinite _ s

Premises used: MeasureTheory.Restrict.sigmaFinite
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this : SigmaFinite (μ.trim hm)
⊢ SigmaFinite ((μ.restrict s).trim hm)

Tactic:
have : SigmaFinite ((μ.restrict s).trim hm) := by
    rw [← restrict_trim hm _ hs]
    exact Restrict.sigmaFinite _ s
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
pos : ∀ (hf_int : Integrable f μ), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
neg : ∀ (hf_int : ¬Integrable f μ), μ[f | m] =ᶠ[ae (μ.restrict s)] 0
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0

Tactic:
by_cases hf_int : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : ¬Integrable f μ
neg neg₁ : EventuallyEq.{u_1, u_2} (β := E) (ae (μ.restrict s)) 0 0
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0

Tactic:
rw [condExp_of_not_integrable hf_int]

Premises used: MeasureTheory.condExp_of_not_integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0

Tactic:
ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm ?_ ?_ ?_ ?_ ?_

Premises used: MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
pos :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn μ[f | m] s_1 (μ.restrict s)
pos₁ :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn.{u_1, u_2} (ε := E) 0 s_1 (μ.restrict s)
pos₂ :
  ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        Eq.{u_2 + 1} (α := E) (∫ (x : α) in s_1, μ[f | m] x ∂μ.restrict s) (∫ (x : α) in s_1, 0 x ∂μ.restrict s)
pos₃ : AEStronglyMeasurable μ[f | m] (μ.restrict s)
pos₄ : AEStronglyMeasurable.{u_1, u_2} (β := E) 0 (μ.restrict s)
⊢ μ[f | m] =ᶠ[ae (μ.restrict s)] 0

Tactic:
refine ae_eq_of_forall_setIntegral_eq_of_sigmaFinite' hm ?_ ?_ ?_ ?_ ?_

Premises used: MeasureTheory.ae_eq_of_forall_setIntegral_eq_of_sigmaFinite'
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn μ[f | m] s_1 (μ.restrict s)

Tactic:
fun t _ _ => integrable_condExp.integrableOn.integrableOn

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn μ[f | m] s_1 (μ.restrict s)

Tactic:
exact fun t _ _ => integrable_condExp.integrableOn.integrableOn

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Indicator
Goal:
α : Type u_1
E : Type u_2
m m0 : MeasurableSpace α
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
inst_2 : CompleteSpace E
μ : Measure α
f : α → E
s : Set α
hs : MeasurableSet s
hf : f =ᶠ[ae (μ.restrict s)] 0
hm : m ≤ m0
hμm this_1 : SigmaFinite (μ.trim hm)
this : SigmaFinite ((μ.restrict s).trim hm)
hf_int : Integrable f μ
⊢ ∀ (s_1 : Set α),
    MeasurableSet s_1 →
      LT.lt (α := ℝ≥0∞) ((μ.restrict s : (a : Set α) → ℝ≥0∞) s_1 : ℝ≥0∞) (∞ : ℝ≥0∞) →
        IntegrableOn.{u_1, u_2} (ε := E) 0 s_1 (μ.restrict s)

Tactic:
fun t _ _ => (integrable_zero _ _ _).integrableOn

Premises used: MeasureTheory.Measure.restrict, MeasureTheory.integrable_zero, MeasureTheory.Integrable.integrableOn