awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
⊢ ‖f i x‖ₑ ≤ ‖(indicator {x : α | ‖f i x‖₊ < C} (f i) + indicator {x : α | C ≤ ‖f i x‖₊} (f i)) x‖ₑ
have rw : ‖f i x‖ₑ ≤
  ‖(if Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x then f i x else 0) +
      indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ
Tactic: rw [Pi.add_apply, Set.indicator_apply]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
⊢ ‖f i x‖ₑ ≤
    ‖(if Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x then f i x else 0) +
        indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ
have pos : ∀ (hx : Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x),
  ‖f i x‖ₑ ≤ ‖f i x + indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
pos :
  ∀ (hx : Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x),
    ‖f i x‖ₑ ≤ ‖f i x + indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ
⊢ ‖f i x‖ₑ ≤
    ‖(if Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x then f i x else 0) +
        indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ
have neg : ∀ (hx : x ∉ {x : α | ‖f i x‖₊ < C}), ‖f i x‖ₑ ≤ ‖0 + indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ
Tactic: split_ifs with hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
hx : Membership.mem (γ := Set α) {x : α | ‖f i x‖₊ < C} x
⊢ ‖f i x‖ₑ ≤ ‖f i x + indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ
have pos : x ∉ {x : α | C ≤ ‖f i x‖₊}
Tactic: rw [Set.indicator_of_notMem, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
x : α
hx : x ∉ {x : α | ‖f i x‖₊ < C}
⊢ ‖f i x‖ₑ ≤ ‖0 + indicator {x : α | C ≤ ‖f i x‖₊} (f i) x‖ₑ
have neg : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x
Tactic: rw [Set.indicator_of_mem, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ ∀ᵐ (x : α) ∂μ, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖₊ ≤ C
have h₁ : ∀ (a : α), ‖indicator {x : α | ‖f i x‖₊ < C} (f i) a‖₊ ≤ C
Tactic: filter_upwards
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ ∀ (a : α), ‖indicator {x : α | ‖f i x‖₊ < C} (f i) a‖₊ ≤ C
have h₁ : ∀ (a : α), indicator {x : α | ‖f i x‖₊ < C} (fun (a : α) ↦ ‖f i a‖₊) a ≤ C
Tactic: simp_rw [nnnorm_indicator_eq_indicator_nnnorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p μ + eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1
have this : ∀ᵐ (x : α) ∂μ, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖₊ ≤ C
Tactic: have : ∀ᵐ x ∂μ, ‖{ x : α | ‖f i x‖₊ < C }.indicator (f i) x‖₊ ≤ C := by
        filter_upwards
        simp_rw [nnnorm_indicator_eq_indicator_nnnorm]
        exact Set.indicator_le fun x (hx : _ < _) => hx.le
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
this : ∀ᵐ (x : α) ∂μ, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖₊ ≤ C
⊢ eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p μ + eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1
have refine : HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ * ENNReal.ofReal (↑C : ℝ) ≤
  (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹
Tactic: refine add_le_add (le_trans (eLpNorm_le_of_ae_bound this) ?_) (ENNReal.ofReal_one ▸ hC i)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
this : ∀ᵐ (x : α) ∂μ, ‖indicator {x : α | ‖f i x‖₊ < C} (f i) x‖₊ ≤ C
⊢ HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ * ENNReal.ofReal (↑C : ℝ) ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹
have simp_rw : (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ ≤
  (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹
Tactic: simp_rw [NNReal.val_eq_coe, ENNReal.ofReal_coe_nnreal, mul_comm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1 =
    (↑((↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1).toNNReal : ℝ≥0∞)
have rw : (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1 =
  (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1
Tactic: rw [ENNReal.coe_toNNReal (by finiteness)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
⊢ eLpNorm (f i) p μ ≤
    (↑((↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1).toNNReal : ℝ≥0∞)
have eLpNorm : eLpNorm (f i) p μ ≤
  eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p μ + eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ
Tactic: calc
    eLpNorm (f i) p μ ≤
        eLpNorm ({ x : α | ‖f i x‖₊ < C }.indicator (f i)) p μ +
          eLpNorm ({ x : α | C ≤ ‖f i x‖₊ }.indicator (f i)) p μ := by
      refine le_trans (eLpNorm_mono_enorm fun x => ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const)))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))) hp)
      rw [Pi.add_apply, Set.indicator_apply]
      split_ifs with hx
      · rw [Set.indicator_of_notMem, add_zero]
        simpa using hx
      · rw [Set.indicator_of_mem, zero_add]
        simpa using hx
    _ ≤ (C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 := by
      have : ∀ᵐ x ∂μ, ‖{ x : α | ‖f i x‖₊ < C }.indicator (f i) x‖₊ ≤ C := by
        filter_upwards
        simp_rw [nnnorm_indicator_eq_indicator_nnnorm]
        exact Set.indicator_le fun x (hx : _ < _) => hx.le
      refine add_le_add (le_trans (eLpNorm_le_of_ae_bound this) ?_) (ENNReal.ofReal_one ▸ hC i)
      simp_rw [NNReal.val_eq_coe, ENNReal.ofReal_coe_nnreal, mul_comm]
      exact le_rfl
    _ = ((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 : ℝ≥0∞).toNNReal := by
      rw [ENNReal.coe_toNNReal (by finiteness)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε →
      ∃ (C : ℝ≥0), ∀ (i : ι), MeasureTheory.eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), MeasureTheory.eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
eLpNorm :
  MeasureTheory.eLpNorm (f i) p μ ≤
    MeasureTheory.eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p μ +
      MeasureTheory.eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ
⊢ MeasureTheory.eLpNorm (f i) p μ ≤
    (↑((↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1).toNNReal : ℝ≥0∞)
have eLpNorm₁ : MeasureTheory.eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p μ +
    MeasureTheory.eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤
  (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1
Tactic: calc
    eLpNorm (f i) p μ ≤
        eLpNorm ({ x : α | ‖f i x‖₊ < C }.indicator (f i)) p μ +
          eLpNorm ({ x : α | C ≤ ‖f i x‖₊ }.indicator (f i)) p μ := by
      refine le_trans (eLpNorm_mono_enorm fun x => ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const)))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))) hp)
      rw [Pi.add_apply, Set.indicator_apply]
      split_ifs with hx
      · rw [Set.indicator_of_notMem, add_zero]
        simpa using hx
      · rw [Set.indicator_of_mem, zero_add]
        simpa using hx
    _ ≤ (C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 := by
      have : ∀ᵐ x ∂μ, ‖{ x : α | ‖f i x‖₊ < C }.indicator (f i) x‖₊ ≤ C := by
        filter_upwards
        simp_rw [nnnorm_indicator_eq_indicator_nnnorm]
        exact Set.indicator_le fun x (hx : _ < _) => hx.le
      refine add_le_add (le_trans (eLpNorm_le_of_ae_bound this) ?_) (ENNReal.ofReal_one ▸ hC i)
      simp_rw [NNReal.val_eq_coe, ENNReal.ofReal_coe_nnreal, mul_comm]
      exact le_rfl
    _ = ((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 : ℝ≥0∞).toNNReal := by
      rw [ENNReal.coe_toNNReal (by finiteness)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
h :
  ∀ (ε : ℝ),
    0 < ε →
      ∃ (C : ℝ≥0), ∀ (i : ι), MeasureTheory.eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
C : ℝ≥0
hC : ∀ (i : ι), MeasureTheory.eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal 1
i : ι
eLpNorm :
  MeasureTheory.eLpNorm (f i) p μ ≤
    MeasureTheory.eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p μ +
      MeasureTheory.eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ
eLpNorm₁ :
  MeasureTheory.eLpNorm (indicator {x : α | ‖f i x‖₊ < C} (f i)) p μ +
      MeasureTheory.eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1
⊢ MeasureTheory.eLpNorm (f i) p μ ≤
    (↑((↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1).toNNReal : ℝ≥0∞)
have eLpNorm₂ : (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1 =
  (↑((↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) univ : ℝ≥0∞) p.toReal⁻¹ + 1).toNNReal : ℝ≥0∞)
Tactic: calc
    eLpNorm (f i) p μ ≤
        eLpNorm ({ x : α | ‖f i x‖₊ < C }.indicator (f i)) p μ +
          eLpNorm ({ x : α | C ≤ ‖f i x‖₊ }.indicator (f i)) p μ := by
      refine le_trans (eLpNorm_mono_enorm fun x => ?_) (eLpNorm_add_le
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator ((hf i).nnnorm.measurableSet_lt stronglyMeasurable_const)))
        (StronglyMeasurable.aestronglyMeasurable
          ((hf i).indicator (stronglyMeasurable_const.measurableSet_le (hf i).nnnorm))) hp)
      rw [Pi.add_apply, Set.indicator_apply]
      split_ifs with hx
      · rw [Set.indicator_of_notMem, add_zero]
        simpa using hx
      · rw [Set.indicator_of_mem, zero_add]
        simpa using hx
    _ ≤ (C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 := by
      have : ∀ᵐ x ∂μ, ‖{ x : α | ‖f i x‖₊ < C }.indicator (f i) x‖₊ ≤ C := by
        filter_upwards
        simp_rw [nnnorm_indicator_eq_indicator_nnnorm]
        exact Set.indicator_le fun x (hx : _ < _) => hx.le
      refine add_le_add (le_trans (eLpNorm_le_of_ae_bound this) ?_) (ENNReal.ofReal_one ▸ hC i)
      simp_rw [NNReal.val_eq_coe, ENNReal.ofReal_coe_nnreal, mul_comm]
      exact le_rfl
    _ = ((C : ℝ≥0∞) * μ Set.univ ^ p.toReal⁻¹ + 1 : ℝ≥0∞).toNNReal := by
      rw [ENNReal.coe_toNNReal (by finiteness)]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
⊢ UniformIntegrable f p μ
have hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
Tactic: have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hf i).1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
⊢ UniformIntegrable f p μ
have hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
Tactic: have hgeq : ∀ i, g i =ᵐ[μ] f i := fun i => (Exists.choose_spec <| hf i).2.symm
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
⊢ UniformIntegrable f p μ
have refine : ∀ (ε : ℝ) (hε : 0 < ε), ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
Tactic: refine (uniformIntegrable_of' hp hp' hgmeas fun ε hε => ?_).ae_eq hgeq
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
have refine : ∀ (i : ι), indicator {x : α | C ≤ ‖g i x‖₊} (g i) =ᶠ[ae μ] indicator {x : α | C ≤ ‖f i x‖₊} (f i)
Tactic: refine ⟨C, fun i => le_trans (le_of_eq <| eLpNorm_congr_ae ?_) (hC i)⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ indicator {x : α | C ≤ ‖g i x‖₊} (g i) =ᶠ[ae μ] indicator {x : α | C ≤ ‖f i x‖₊} (f i)
have h₁ : ∀ (x : α) (hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x),
  indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
Tactic: filter_upwards [(Exists.choose_spec <| hf i).2] with x hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
⊢ indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
have pos : ∀ (hfx : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x),
  indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
Tactic: by_cases hfx : x ∈ { x | C ≤ ‖f i x‖₊ }
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
ι : Type u_3
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : ι → α → β
inst_1 : IsFiniteMeasure μ
hp : 1 ≤ p
hp' : p ≠ ∞
hf : ∀ (i : ι), AEStronglyMeasurable (f i) μ
h : ∀ (ε : ℝ), 0 < ε → ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgeq : ∀ (i : ι), g i =ᶠ[ae μ] f i
ε : ℝ
hε : 0 < ε
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
pos :
  ∀ (hfx : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x),
    indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
⊢ indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
have neg : ∀ (hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}),
  indicator {x : α | C ≤ ‖g i x‖₊} (g i) x = indicator {x : α | C ≤ ‖f i x‖₊} (f i) x
Tactic: by_cases hfx : x ∈ { x | C ≤ ‖f i x‖₊ }