awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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| ∂μ)
have rw : Eq (α := ℝ) (∫ (x : α), s.indicator (fun (x : α) ↦ |μ[f | m] x|) x ∂μ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ)
Tactic: rw [← integral_indicator (hnm _ hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
⊢ Eq (α := ℝ) (∫ (x : α), s.indicator (fun (x : α) ↦ |μ[f | m] x|) x ∂μ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ)
have refine : (ae μ).EventuallyEq (β := ℝ) (s.indicator fun (x : α) ↦ |μ[f | m] x|) fun (x : α) ↦ |μ[s.indicator f | m] x|
Tactic: refine integral_congr_ae ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
⊢ (ae μ).EventuallyEq (β := ℝ) (s.indicator fun (x : α) ↦ |μ[f | m] x|) fun (x : α) ↦ |μ[s.indicator f | m] x|
have this : (ae μ).EventuallyEq (β := ℝ) (fun (x : α) ↦ |μ[s.indicator f | m] x|) fun (x : α) ↦ |s.indicator μ[f | m] x|
Tactic: have : (fun x => |(μ[s.indicator f | m]) x|) =ᵐ[μ] fun x => |s.indicator (μ[f | m]) x| :=
      (condExp_indicator hfint hs).fun_comp abs
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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|
have refine : ∀ (x : α), s.indicator (fun (x : α) ↦ |μ[f | m] x|) x = |s.indicator μ[f | m] x|
Tactic: refine EventuallyEq.trans (Eventually.of_forall fun x => ?_) this.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : α
⊢ s.indicator (fun (x : α) ↦ |μ[f | m] x|) x = |s.indicator μ[f | m] x|
have rw : Eq (α := ℝ) (s.indicator (fun (x : α) ↦ |μ[f | m] x|) x) (s.indicator (fun (a : α) ↦ ‖μ[f | m] a‖) x)
Tactic: rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
s : Set α
hs : MeasurableSet s
f : α → ℝ
hnm : m ≤ m0
hfint : Integrable f μ
⊢ LE.le (α := ℝ) (∫ (x : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
have this : 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]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : α) in s, |μ[f | m] x| ∂μ) (∫ (x : α) in s, |f x| ∂μ)
have pos : LE.le (α := ℝ) (∫ (x : α), |μ[s.indicator f | m] x| ∂μ) (∫ (x : α), s.indicator (fun (x : α) ↦ |f x|) x ∂μ)
Tactic: rw [this, ← integral_indicator (hnm _ hs)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 ∂μ)
have pos : ∀ (x : α), Eq (α := ℝ) ((fun (x : α) ↦ |s.indicator f 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 => ?_)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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
⊢ Eq (α := ℝ) ((fun (x : α) ↦ |s.indicator f x|) x) (s.indicator (fun (x : α) ↦ |f x|) x)
have pos₂ : ‖s.indicator f x‖ = s.indicator (fun (x : α) ↦ ‖f x‖) x
Tactic: simp_rw [← Real.norm_eq_abs, norm_indicator_eq_indicator_norm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
have pos : ∀ (hnm : m ≤ m0), ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
Tactic: by_cases hnm : m ≤ m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : ℝ)
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
have neg : ∀ (hnm : ¬m ≤ m0), ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
Tactic: by_cases hnm : m ≤ m0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : ¬m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
have neg : ∀ᵐ (x : α) ∂μ, 0 ≤ (↑R : ℝ)
Tactic: simp_rw [condExp_of_not_le hnm, Pi.zero_apply, abs_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
have pos : ∀ (hfint : Integrable f μ), ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
Tactic: by_cases hfint : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : ℝ)
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
have neg : ∀ (hfint : ¬Integrable f μ), ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
Tactic: by_cases hfint : Integrable f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
have neg : ∀ᵐ (x : α) ∂μ, |0 x| ≤ (↑R : ℝ)
Tactic: simp_rw [condExp_of_not_integrable hfint]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : ¬Integrable f μ
⊢ ∀ᵐ (x : α) ∂μ, |0 x| ≤ (↑R : ℝ)
have h : ∀ (x : α) (hx : |f x| ≤ (↑R : ℝ)), |0 x| ≤ (↑R : ℝ)
Tactic: filter_upwards [hbdd] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 x| ≤ (↑R : ℝ)
have h : 0 ≤ (↑R : ℝ)
Tactic: rw [Pi.zero_apply, abs_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m m0 : MeasurableSpace α
μ : Measure α
R : ℝ≥0
f : α → ℝ
hbdd : ∀ᵐ (x : α) ∂μ, |f x| ≤ (↑R : ℝ)
hnm : m ≤ m0
hfint : Integrable f μ
⊢ ∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)
have pos : ∀ (h : ¬∀ᵐ (x : α) ∂μ, |μ[f | m] x| ≤ (↑R : ℝ)), False
Tactic: by_contra h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
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 : ℝ)
⊢ False
have h₁ : Ne (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (fun (x : α) ↦ |μ[f | m] x| ≤ (↑R : ℝ)) x}ᶜ : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: change μ _ ≠ 0 at h
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
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∞)
⊢ False
have h₁ : 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
Cleared hypotheses: h
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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∞)
⊢ False
have pos : μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ) < μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)
Tactic: suffices μ.real {x | ↑R < |(μ[f|m]) x|} * ↑R < μ.real {x | ↑R < |(μ[f|m]) x|} * ↑R by
    exact this.ne rfl
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : ℝ)
have pos : IntegrableOn (ε := ℝ) (fun (x : α) ↦ |μ[f | m] x|) {x : α | (↑R : ℝ) < |μ[f | m] x|} μ
Tactic: refine lt_of_lt_of_le (setIntegral_gt_gt R.coe_nonneg ?_ h.ne') ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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|} μ
⊢ μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ) < μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)
have pos₁ : ∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, |μ[f | m] x| ∂μ ≤ μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)
Tactic: refine lt_of_lt_of_le (setIntegral_gt_gt R.coe_nonneg ?_ h.ne') ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : ℝ)
have pos : MeasurableSet.{u_1} (α := α) {x : α | (↑R : ℝ) < |μ[f | m] x|}
Tactic: refine (setIntegral_abs_condExp_le ?_ _).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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|}
⊢ ∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, |μ[f | m] x| ∂μ ≤ μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)
have pos₁ : ∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, |f x| ∂μ ≤ μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)
Tactic: refine (setIntegral_abs_condExp_le ?_ _).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 x| ∂μ ≤ μ.real {x : α | (↑R : ℝ) < |μ[f | m] x|} * (↑R : ℝ)
have pos : LE.le (α := ℝ) (∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, |f x| ∂μ)
  (∫ (x : α) in {x : α | (↑R : ℝ) < |μ[f | m] x|}, (↑R : ℝ) ∂μ)
Tactic: simp only [← smul_eq_mul, ← setIntegral_const]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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 : ℝ) ∂μ)
have pos : IntegrableOn (ε := ℝ) (fun (x : α) ↦ (↑R : ℝ)) {x : α | (↑R : ℝ) < |μ[f | m] x|} μ
Tactic: refine setIntegral_mono_ae hfint.abs.integrableOn ?_ hbdd
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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|} μ
have pos : ∫⁻ (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 ⟨aestronglyMeasurable_const, lt_of_le_of_lt ?_
    (integrable_condExp.integrableOn : IntegrableOn (μ[f|m]) {x | ↑R < |(μ[f|m]) x|} μ).2⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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‖ₑ ∂μ
have pos : ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | (↑R : ℝ) < |μ[f | m] x|} x),
  enorm (E := ℝ) ((fun (x : α) ↦ (↑R : ℝ)) x) ≤ ‖μ[f | m] x‖ₑ
Tactic: refine setLIntegral_mono
    (stronglyMeasurable_condExp.mono hnm).measurable.nnnorm.coe_nnreal_ennreal fun x hx => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
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
⊢ enorm (E := ℝ) ((fun (x : α) ↦ (↑R : ℝ)) x) ≤ ‖μ[f | m] x‖ₑ
have pos : NNReal.mk (↑R : ℝ) sorry ≤ ‖μ[f | m] x‖₊
Tactic: rw [enorm_eq_nnnorm, enorm_eq_nnnorm, ENNReal.coe_le_coe, Real.nnnorm_of_nonneg R.coe_nonneg]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
⊢ UniformIntegrable (β := ℝ) (fun (i : ι) ↦ μ[g | ℱ i]) 1 μ
have hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
Tactic: have hmeas : ∀ n, ∀ C, MeasurableSet {x | C ≤ ‖(μ[g|ℱ n]) x‖₊} := fun n C =>
    measurableSet_le measurable_const (stronglyMeasurable_condExp.mono (hℱ n)).measurable.nnnorm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
⊢ UniformIntegrable (β := ℝ) (fun (i : ι) ↦ μ[g | ℱ i]) 1 μ
have hg : MemLp g 1 μ
Tactic: have hg : MemLp g 1 μ := memLp_one_iff_integrable.2 hint
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
⊢ UniformIntegrable (β := ℝ) (fun (i : ι) ↦ μ[g | ℱ i]) 1 μ
have refine : ∀ (ε : ℝ) (hε : 0 < ε),
  ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
Tactic: refine uniformIntegrable_of le_rfl ENNReal.one_ne_top
    (fun n => (stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable) fun ε hε => ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
have pos : ∀ (hne : eLpNorm g 1 μ = 0),
  ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
Tactic: by_cases hne : eLpNorm g 1 μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
pos :
  ∀ (hne : eLpNorm g 1 μ = 0),
    ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
have neg : ∀ (hne : ¬eLpNorm g 1 μ = 0),
  ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
Tactic: by_cases hne : eLpNorm g 1 μ = 0
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : eLpNorm g 1 μ = 0
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
have hne₁ : g =ᶠ[ae μ] 0
Tactic: rw [eLpNorm_eq_zero_iff hg.1 one_ne_zero] at hne
Cleared hypotheses: hne
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : g =ᶠ[ae μ] 0
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
have pos : ∀ (n : ι), Set.indicator {x : α | 0 ≤ ‖μ[g | ℱ n] x‖₊} μ[g | ℱ n] =ᶠ[ae μ] 0
Tactic: refine ⟨0, fun n => (le_of_eq <|
      (eLpNorm_eq_zero_iff ((stronglyMeasurable_condExp.mono (hℱ n)).aestronglyMeasurable.indicator
        (hmeas n 0)) one_ne_zero).2 ?_).trans zero_le⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (goal)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : g =ᶠ[ae μ] 0
n : ι
⊢ Set.indicator {x : α | 0 ≤ ‖μ[g | ℱ n] x‖₊} μ[g | ℱ n] =ᶠ[ae μ] 0
have h : ∀ (x : α) (hx : μ[g | ℱ n] x = μ[0 | ℱ n] x), Set.indicator {x : α | 0 ≤ ‖μ[g | ℱ n] x‖₊} μ[g | ℱ n] x = 0 x
Tactic: filter_upwards [condExp_congr_ae (m := ℱ n) hne] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
have hC : let C := (NNReal.mk δ sorry)⁻¹ * (eLpNorm g 1 μ).toNNReal;
C = (NNReal.mk δ sorry)⁻¹ * (eLpNorm g 1 μ).toNNReal
Tactic: set C : ℝ≥0 := (.mk δ hδ.le)⁻¹ * (eLpNorm g 1 μ).toNNReal with hC
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.ConditionalExpectation.Real (hypothesis)
Goal:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
ι : Type u_2
inst : IsFiniteMeasure μ
g : α → ℝ
hint : Integrable g μ
ℱ : ι → MeasurableSpace α
hℱ : ∀ (i : ι), ℱ i ≤ m0
A : MeasurableSpace α := m0
hmeas : ∀ (n : ι) (C : ℝ≥0), MeasurableSet.{u_1} (α := α) {x : α | C ≤ ‖μ[g | ℱ n] x‖₊}
hg : MemLp g 1 μ
ε : ℝ
hε : 0 < ε
hne : ¬eLpNorm g 1 μ = 0
δ : ℝ
hδ : 0 < δ
h :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) 1 μ ≤ ENNReal.ofReal ε
C : ℝ≥0 := (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
hC : C = (NNReal.mk δ ⋯)⁻¹ * (eLpNorm g 1 μ).toNNReal
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (Set.indicator {x : α | C ≤ ‖μ[g | ℱ i] x‖₊} μ[g | ℱ i]) 1 μ ≤ ENNReal.ofReal ε
have hCpos : 0 < C
Tactic: have hCpos : 0 < C := mul_pos (inv_pos.2 hδ) (ENNReal.toNNReal_pos hne hg.eLpNorm_lt_top.ne)