awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ |μ[s.indicator f | m] x|) fun (x : α) ↦ |s.indicator μ[f | m] x|
⊢ (ae μ).EventuallyEq (β := ℝ) (s.indicator fun (x : α) ↦ |μ[f | m] x|) fun (x : α) ↦ |μ[s.indicator f | m] x|

Tactic:
EventuallyEq.trans (Eventually.of_forall fun x => ?_) this.symm

Premises used: Filter.EventuallyEq.trans, Filter.Eventually.of_forall, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ |μ[s.indicator f | m] x|) fun (x : α) ↦ |s.indicator μ[f | m] x|
refine : ∀ (x : α), s.indicator (fun (x : α) ↦ |μ[f | m] x|) x = |s.indicator μ[f | m] x|
⊢ (ae μ).EventuallyEq (β := ℝ) (s.indicator fun (x : α) ↦ |μ[f | m] x|) fun (x : α) ↦ |μ[s.indicator f | m] x|

Tactic:
refine EventuallyEq.trans (Eventually.of_forall fun x => ?_) this.symm

Premises used: Filter.EventuallyEq.trans, Filter.Eventually.of_forall, Filter.EventuallyEq.symm
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ |μ[s.indicator f | m] x|) fun (x : α) ↦ |s.indicator μ[f | m] x|
x : α
rw : Eq (α := ℝ) (s.indicator (fun (x : α) ↦ |μ[f | m] x|) x) (s.indicator (fun (a : α) ↦ ‖μ[f | m] a‖) x)
⊢ s.indicator (fun (x : α) ↦ |μ[f | m] x|) x = |s.indicator μ[f | m] x|

Tactic:
rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]

Premises used: norm_indicator_eq_indicator_norm, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ |μ[s.indicator f | m] x|) fun (x : α) ↦ |s.indicator μ[f | m] x|
x : α
⊢ Eq (α := ℝ) (s.indicator (fun (x : α) ↦ |μ[f | m] x|) x) (s.indicator (fun (a : α) ↦ ‖μ[f | m] a‖) x)

Tactic:
simp only [Real.norm_eq_abs]

Premises used: Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
⊢ Eq (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ)

Tactic:
have : ∫ x in s, |(μ[f | m]) x| ∂μ = ∫ x, |(μ[s.indicator f | m]) x| ∂μ := by
    rw [← integral_indicator (hnm _ hs)]
    refine integral_congr_ae ?_
    have : (fun x => |(μ[s.indicator f | m]) x|) =ᵐ[μ] fun x => |s.indicator (μ[f | m]) x| :=
      (condExp_indicator hfint hs).fun_comp abs
    refine EventuallyEq.trans (Eventually.of_forall fun x => ?_) this.symm
    rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]
    simp only [Real.norm_eq_abs]
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : Eq (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ)
pos : LE.le (α := ℝ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ) (∫ (x : α), s.indicator (fun (x : α) ↦ |f x|) x ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)

Tactic:
rw [this, ← integral_indicator (hnm _ hs)]

Premises used: MeasureTheory.integral_indicator
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : Eq (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ)
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ) (∫ (x : α), s.indicator (fun (x : α) ↦ |f x|) x ∂μ)

Tactic:
(integral_abs_condExp_le _).trans
    (le_of_eq <| integral_congr_ae <| Eventually.of_forall fun x => ?_)

Premises used: MeasureTheory.integral_congr_ae, Filter.Eventually.of_forall, LE.le.trans, le_of_eq, MeasureTheory.integral_abs_condExp_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : Eq (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ)
pos : ∀ (x : α), Eq (α := ℝ) ((fun (x : α) ↦ |s.indicator f x|) x) (s.indicator (fun (x : α) ↦ |f x|) x)
⊢ LE.le (α := ℝ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ) (∫ (x : α), s.indicator (fun (x : α) ↦ |f x|) x ∂μ)

Tactic:
refine (integral_abs_condExp_le _).trans
    (le_of_eq <| integral_congr_ae <| Eventually.of_forall fun x => ?_)

Premises used: MeasureTheory.integral_congr_ae, Filter.Eventually.of_forall, LE.le.trans, le_of_eq, MeasureTheory.integral_abs_condExp_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
this : Eq (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ)
x : α
pos pos₁ : |s.indicator f x| = s.indicator (fun (x : α) ↦ |f x|) x
pos₂ : ‖s.indicator f x‖ = s.indicator (fun (x : α) ↦ ‖f x‖) x
⊢ Eq (α := ℝ) ((fun (x : α) ↦ |s.indicator f x|) x) (s.indicator (fun (x : α) ↦ |f x|) x)

Tactic:
simp_rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]

Premises used: norm_indicator_eq_indicator_norm, Real.norm_eq_abs
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
pos : ∀ (hnm : m ≤ m0), ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
neg : ∀ (hnm : ¬m ≤ m0), ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)

Tactic:
by_cases hnm : m ≤ m0
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : ¬m ≤ m0
neg : ∀ᵐ (x : α) ∂μ, 0 ≤ (↑R : ℝ)
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)

Tactic:
simp_rw [condExp_of_not_le hnm, Pi.zero_apply, abs_zero]

Premises used: Pi.zero_apply, MeasureTheory.condExp_of_not_le, abs_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : ¬m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, 0 ≤ (↑R : ℝ)

Tactic:
Eventually.of_forall fun _ => R.coe_nonneg

Premises used: Filter.Eventually.of_forall, NNReal.coe_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : ¬m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, 0 ≤ (↑R : ℝ)

Tactic:
exact Eventually.of_forall fun _ => R.coe_nonneg

Premises used: Filter.Eventually.of_forall, NNReal.coe_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
pos : ∀ (hfint : Integrable f μ), ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
neg : ∀ (hfint : ¬Integrable f μ), ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)

Tactic:
by_cases hfint : Integrable f μ

Premises used: MeasureTheory.Integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : ¬Integrable f μ
neg : ∀ᵐ (x : α) ∂μ, |0 x| ≤ (↑R : ℝ)
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)

Tactic:
simp_rw [condExp_of_not_integrable hfint]

Premises used: MeasureTheory.condExp_of_not_integrable
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : ¬Integrable f μ
h : ∀ (x : α) (hx : |f x| ≤ (↑R : ℝ)), |0 x| ≤ (↑R : ℝ)
⊢ ∀ᵐ (x : α) ∂μ, |0 x| ≤ (↑R : ℝ)

Tactic:
filter_upwards [hbdd] with x hx
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : ¬Integrable f μ
x : α
hx : |f x| ≤ (↑R : ℝ)
h : 0 ≤ (↑R : ℝ)
⊢ |0 x| ≤ (↑R : ℝ)

Tactic:
rw [Pi.zero_apply, abs_zero]

Premises used: Pi.zero_apply, abs_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : ¬Integrable f μ
x : α
hx : |f x| ≤ (↑R : ℝ)
⊢ 0 ≤ (↑R : ℝ)

Tactic:
(abs_nonneg _).trans hx

Premises used: LE.le.trans, abs_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : ¬Integrable f μ
x : α
hx : |f x| ≤ (↑R : ℝ)
⊢ 0 ≤ (↑R : ℝ)

Tactic:
exact (abs_nonneg _).trans hx

Premises used: LE.le.trans, abs_nonneg
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
pos : ∀ (h : ¬∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)), False
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)

Tactic:
by_contra h
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : ¬∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
⊢ Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ |μ[f | m] x| ≤ (↑R : ℝ)) x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
change μ _ ≠ 0 at h

Premises used: DFunLike.coe
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ |μ[f | m] x| ≤ (↑R : ℝ)) x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)

Tactic:
simp only [← pos_iff_ne_zero, Set.compl_def, Set.mem_setOf_eq, not_le] at h

Premises used: not_le, Set.compl_def, Set.mem_setOf_eq, pos_iff_ne_zero
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
this : μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ) < μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)
⊢ False

Tactic:
this.ne rfl

Premises used: rfl, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
this : μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ) < μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)
⊢ False

Tactic:
exact this.ne rfl

Premises used: rfl, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
pos : μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ) < μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)
⊢ False

Tactic:
suffices μ.real {x | ↑R < |(μ[f|m]) x|} * ↑R < μ.real {x | ↑R < |(μ[f|m]) x|} * ↑R by
    exact this.ne rfl
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
⊢ μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ) < μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)

Tactic:
lt_of_lt_of_le (setIntegral_gt_gt R.coe_nonneg ?_ h.ne') ?_

Premises used: LT.lt.ne', MeasureTheory.setIntegral_gt_gt, NNReal.coe_nonneg, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
pos : IntegrableOn (ε := ℝ) (fun (x : α) ↦ |μ[f | m] x|) {x : α | (↑R : ℝ) < |μ[f | m] x|} μ
pos₁ :
  ∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, |μ[f | m] x| ∂μ ≤ μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)
⊢ μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ) < μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)

Tactic:
refine lt_of_lt_of_le (setIntegral_gt_gt R.coe_nonneg ?_ h.ne') ?_

Premises used: LT.lt.ne', MeasureTheory.setIntegral_gt_gt, NNReal.coe_nonneg, lt_of_lt_of_le
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ |μ[f | m] x|) {x : α | (↑R : ℝ) < |μ[f | m] x|} μ

Tactic:
integrable_condExp.abs.integrableOn

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.Integrable.abs, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ |μ[f | m] x|) {x : α | (↑R : ℝ) < |μ[f | m] x|} μ

Tactic:
exact integrable_condExp.abs.integrableOn

Premises used: MeasureTheory.integrable_condExp, MeasureTheory.Integrable.abs, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
⊢ ∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, |μ[f | m] x| ∂μ ≤ μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)

Tactic:
(setIntegral_abs_condExp_le ?_ _).trans ?_

Premises used: MeasureTheory.setIntegral_abs_condExp_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
pos : MeasurableSet.{u_1} (α := α) {x : α | (↑R : ℝ) < |μ[f | m] x|}
pos₁ : ∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, |f x| ∂μ ≤ μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)
⊢ ∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, |μ[f | m] x| ∂μ ≤ μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)

Tactic:
refine (setIntegral_abs_condExp_le ?_ _).trans ?_

Premises used: MeasureTheory.setIntegral_abs_condExp_le, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
⊢ MeasurableSet.{u_1} (α := α) {x : α | (↑R : ℝ) < ‖μ[f | m] x‖}

Tactic:
@measurableSet_lt _ _ _ _ _ m _ _ _ _ _ measurable_const
      stronglyMeasurable_condExp.norm.measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, setOf, MeasureTheory.stronglyMeasurable_condExp, measurableSet_lt, MeasureTheory.StronglyMeasurable.norm, measurable_const
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
⊢ MeasurableSet.{u_1} (α := α) {x : α | (↑R : ℝ) < ‖μ[f | m] x‖}

Tactic:
exact @measurableSet_lt _ _ _ _ _ m _ _ _ _ _ measurable_const
      stronglyMeasurable_condExp.norm.measurable

Premises used: MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.stronglyMeasurable_condExp, measurableSet_lt, MeasureTheory.StronglyMeasurable.norm, measurable_const
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
pos :
  LE.le (α := ℝ) (∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, |f x| ∂μ)
    (∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, (↑R : ℝ) ∂μ)
⊢ ∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, |f x| ∂μ ≤ μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)

Tactic:
simp only [← smul_eq_mul, ← setIntegral_const]

Premises used: smul_eq_mul, MeasureTheory.setIntegral_const
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
⊢ LE.le (α := ℝ) (∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, |f x| ∂μ)
    (∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, (↑R : ℝ) ∂μ)

Tactic:
setIntegral_mono_ae hfint.abs.integrableOn ?_ hbdd

Premises used: MeasureTheory.Integrable.abs, MeasureTheory.Integrable.integrableOn, MeasureTheory.setIntegral_mono_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
pos : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (↑R : ℝ)) {x : α | (↑R : ℝ) < |μ[f | m] x|} μ
⊢ LE.le (α := ℝ) (∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, |f x| ∂μ)
    (∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, (↑R : ℝ) ∂μ)

Tactic:
refine setIntegral_mono_ae hfint.abs.integrableOn ?_ hbdd

Premises used: MeasureTheory.Integrable.abs, MeasureTheory.Integrable.integrableOn, MeasureTheory.setIntegral_mono_ae
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ (↑R : ℝ)) {x : α | (↑R : ℝ) < |μ[f | m] x|} μ

Tactic:
⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_
    (integrable_condExp.integrableOn : IntegrableOn (μ[f|m]) {x | ↑R < |(μ[f|m]) x|} μ).2⟩

Premises used: lt_of_le_of_lt, MeasureTheory.aestronglyMeasurable_const, MeasureTheory.integrable_condExp, MeasureTheory.Integrable, MeasureTheory.IntegrableOn, And.right, And.intro, MeasureTheory.Integrable.integrableOn
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
pos :
  ∫⁻ (a : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, enorm (E := ℝ) ((fun (x : α) ↦ (↑R : ℝ)) a) ∂μ ≤
    ∫⁻ (a : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, ‖μ[f | m] a‖ₑ ∂μ
⊢ IntegrableOn (ε := ℝ) (fun (x : α) ↦ (↑R : ℝ)) {x : α | (↑R : ℝ) < |μ[f | m] x|} μ

Tactic:
refine ⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_
    (integrable_condExp.integrableOn : IntegrableOn (μ[f|m]) {x | ↑R < |(μ[f|m]) x|} μ).2⟩
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
⊢ ∫⁻ (a : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, enorm (E := ℝ) ((fun (x : α) ↦ (↑R : ℝ)) a) ∂μ ≤
    ∫⁻ (a : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, ‖μ[f | m] a‖ₑ ∂μ

Tactic:
setLIntegral_mono
    (stronglyMeasurable_condExp.mono hnm).measurable.nnnorm.coe_nnreal_ennreal fun x hx => ?_

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.setLIntegral_mono, Measurable.nnnorm, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
pos :
  ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | (↑R : ℝ) < |μ[f | m] x|} x),
    enorm (E := ℝ) ((fun (x : α) ↦ (↑R : ℝ)) x) ≤ ‖μ[f | m] x‖ₑ
⊢ ∫⁻ (a : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, enorm (E := ℝ) ((fun (x : α) ↦ (↑R : ℝ)) a) ∂μ ≤
    ∫⁻ (a : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, ‖μ[f | m] a‖ₑ ∂μ

Tactic:
refine setLIntegral_mono
    (stronglyMeasurable_condExp.mono hnm).measurable.nnnorm.coe_nnreal_ennreal fun x hx => ?_

Premises used: Measurable.coe_nnreal_ennreal, MeasureTheory.StronglyMeasurable.measurable, MeasureTheory.setLIntegral_mono, Measurable.nnnorm, MeasureTheory.stronglyMeasurable_condExp, MeasureTheory.StronglyMeasurable.mono
-- Module: Mathlib.MeasureTheory.Function.ConditionalExpectation.Real
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
h : LT.lt (α := ℝ≥0∞) (0 : ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (↑R : ℝ) < |μ[f | m] x|} : ℝ≥0∞)
x : α
hx : Membership.mem (γ := Set α) {x : α | (↑R : ℝ) < |μ[f | m] x|} x
pos : NNReal.mk (↑R : ℝ) ⋯ ≤ ‖μ[f | m] x‖₊
⊢ enorm (E := ℝ) ((fun (x : α) ↦ (↑R : ℝ)) x) ≤ ‖μ[f | m] x‖ₑ

Tactic:
rw [enorm_eq_nnnorm, enorm_eq_nnnorm, ENNReal.coe_le_coe, Real.nnnorm_of_nonneg R.coe_nonneg]

Premises used: ENNReal.coe_le_coe, enorm_eq_nnnorm, Real.nnnorm_of_nonneg, NNReal.coe_nonneg