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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑M : ℝ≥0∞)
ℐ : (C : ℝ≥0) → ι
δ : ℝ≥0
hδpos : 0 < (↑δ : ℝ)
hδ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal (↑δ : ℝ) → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal (↑δ : ℝ) < (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f (ℐ C) x‖₊}
this : (↑2 : ℝ≥0∞) * (↑(max M 1) : ℝ≥0∞) ≤ eLpNorm (f (ℐ (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)))) p μ
⊢ max (↑M : ℝ≥0∞) 1 < (↑2 : ℝ≥0∞) * (↑(max M 1) : ℝ≥0∞)
have rw : max M 1 < 2 * max M 1
Tactic: rw [← ENNReal.coe_one, ← ENNReal.coe_max, ← ENNReal.coe_mul, ENNReal.coe_lt_coe]
-- 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hf : ∀ (i : ι), StronglyMeasurable (f i)
ε : ℝ
hε : 0 < ε
hfu : UnifIntegrable f p μ
M : ℝ≥0
hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑M : ℝ≥0∞)
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (i : ι) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (C : ℝ≥0) (hC : ∀ (i : ι), (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f i x‖₊} ≤ ENNReal.ofReal δ),
  ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨C, hC⟩ : ∃ C : ℝ≥0, ∀ i, μ { x | C ≤ ‖f i x‖₊ } ≤ ENNReal.ofReal δ := by
    by_contra! hcon
    choose ℐ hℐ using hcon
    lift δ to ℝ≥0 using hδpos.le
    have : ∀ C : ℝ≥0, C • (δ : ℝ≥0∞) ^ (1 / p.toReal) ≤ eLpNorm (f (ℐ C)) p μ := by
      intro C
      calc
        C • (δ : ℝ≥0∞) ^ (1 / p.toReal) ≤ C • μ { x | C ≤ ‖f (ℐ C) x‖₊ } ^ (1 / p.toReal) := by
          rw [ENNReal.smul_def, ENNReal.smul_def, smul_eq_mul, smul_eq_mul]
          simp_rw [ENNReal.ofReal_coe_nnreal] at hℐ
          refine mul_le_mul' le_rfl
            (ENNReal.rpow_le_rpow (hℐ C).le (one_div_nonneg.2 ENNReal.toReal_nonneg))
        _ ≤ eLpNorm ({ x | C ≤ ‖f (ℐ C) x‖₊ }.indicator (f (ℐ C))) p μ := by
          refine le_eLpNorm_of_bddBelow hp hp' _
            (measurableSet_le measurable_const (hf _).nnnorm.measurable)
            (Eventually.of_forall fun x hx => ?_)
          rwa [nnnorm_indicator_eq_indicator_nnnorm, Set.indicator_of_mem hx]
        _ ≤ eLpNorm (f (ℐ C)) p μ := eLpNorm_indicator_le _
    specialize this (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal))
    rw [← ENNReal.coe_rpow_of_nonneg _ (one_div_nonneg.2 ENNReal.toReal_nonneg), ← ENNReal.coe_smul,
      smul_eq_mul, mul_assoc, NNReal.inv_rpow,
      inv_mul_cancel₀ (NNReal.rpow_pos (NNReal.coe_pos.1 hδpos)).ne.symm, mul_one, ENNReal.coe_mul,
      ← NNReal.inv_rpow] at this
    refine (lt_of_le_of_lt (le_trans
      (hM <| ℐ <| 2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)) (le_max_left (M : ℝ≥0∞) 1))
        (lt_of_lt_of_le ?_ this)).ne rfl
    rw [← ENNReal.coe_one, ← ENNReal.coe_max, ← ENNReal.coe_mul, ENNReal.coe_lt_coe]
    exact lt_two_mul_self (lt_max_of_lt_right one_pos)
-- 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
have hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
Tactic: have hgmeas : ∀ i, StronglyMeasurable (g i) := fun i => (Exists.choose_spec <| hfu.1 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
have hgunif : UniformIntegrable g p μ
Tactic: have hgunif : UniformIntegrable g p μ := hfu.ae_eq fun i => (Exists.choose_spec <| hfu.1 i).2
-- 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (C : ℝ≥0) (hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε),
  ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨C, hC⟩ := hgunif.spec' hp hp' hgmeas hε
-- 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
have refine : ∀ (i : ι), indicator {x : α | C ≤ ‖f i x‖₊} (f i) =ᶠ[ae μ] indicator {x : α | C ≤ ‖g i x‖₊} (g 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
⊢ indicator {x : α | C ≤ ‖f i x‖₊} (f i) =ᶠ[ae μ] indicator {x : α | C ≤ ‖g i x‖₊} (g i)
have h : ∀ (x : α) (hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x),
  indicator {x : α | C ≤ ‖f i x‖₊} (f i) x = indicator {x : α | C ≤ ‖g i x‖₊} (g i) x
Tactic: filter_upwards [(Exists.choose_spec <| hfu.1 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g 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 ≤ ‖f i x‖₊} (f i) x = indicator {x : α | C ≤ ‖g i x‖₊} (g i) x
have pos : ∀ (hfx : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x),
  indicator {x : α | C ≤ ‖f i x‖₊} (f i) x = indicator {x : α | C ≤ ‖g i x‖₊} (g 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g 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 ≤ ‖f i x‖₊} (f i) 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
have neg : ∀ (hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}),
  indicator {x : α | C ≤ ‖f i x‖₊} (f i) x = indicator {x : α | C ≤ ‖g i x‖₊} (g 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x
⊢ indicator {x : α | C ≤ ‖f i x‖₊} (f i) x = indicator {x : α | C ≤ ‖g i x‖₊} (g i) x
have pos : Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
Tactic: rw [Set.indicator_of_mem hfx, Set.indicator_of_mem, 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x
⊢ Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
have pos : ∀ (hfx : C ≤ ‖f i x‖₊), Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
Tactic: rwa [Set.mem_setOf, hx] at hfx
Cleared hypotheses: hfx
-- 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : Membership.mem (γ := Set α) {x : α | C ≤ ‖f i x‖₊} x
pos : ∀ (hfx : C ≤ ‖f i x‖₊), Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
⊢ Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
have pos₁ : ∀ (hfx : C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x‖₊),
  Membership.mem (γ := Set α) {x : α | C ≤ ‖g i x‖₊} x
Tactic: rwa [Set.mem_setOf, hx] at hfx
Cleared hypotheses: hfx
-- 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}
⊢ indicator {x : α | C ≤ ‖f i x‖₊} (f i) x = indicator {x : α | C ≤ ‖g i x‖₊} (g i) x
have neg : x ∉ {x : α | C ≤ ‖g i x‖₊}
Tactic: rw [Set.indicator_of_notMem hfx, Set.indicator_of_notMem]
-- 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}
⊢ x ∉ {x : α | C ≤ ‖g i x‖₊}
have neg : ∀ (hfx : ¬C ≤ ‖f i x‖₊), x ∉ {x : α | C ≤ ‖g i x‖₊}
Tactic: rwa [Set.mem_setOf, hx] at hfx
Cleared hypotheses: hfx
-- 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 : ι → α → β
hp : p ≠ 0
hp' : p ≠ ∞
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
g : ι → α → β := fun (i : ι) ↦ Exists.choose (p := fun (g : α → β) ↦ StronglyMeasurable g ∧ f i =ᶠ[ae μ] g) ⋯
hgmeas : ∀ (i : ι), StronglyMeasurable (g i)
hgunif : UniformIntegrable g p μ
C : ℝ≥0
hC : ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖g i x‖₊} (g i)) p μ ≤ ENNReal.ofReal ε
i : ι
x : α
hx : f i x = Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) ⋯ x
hfx : x ∉ {x : α | C ≤ ‖f i x‖₊}
neg : ∀ (hfx : ¬C ≤ ‖f i x‖₊), x ∉ {x : α | C ≤ ‖g i x‖₊}
⊢ x ∉ {x : α | C ≤ ‖g i x‖₊}
have neg₁ : ∀ (hfx : ¬C ≤ ‖Exists.choose (p := fun (a : α → β) ↦ StronglyMeasurable a ∧ f i =ᶠ[ae μ] a) sorry x‖₊),
  x ∉ {x : α | C ≤ ‖g i x‖₊}
Tactic: rwa [Set.mem_setOf, hx] at hfx
Cleared hypotheses: hfx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf : UniformIntegrable f p μ
⊢ UniformIntegrable.{u_1, u_4, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) p μ
have hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
Tactic: obtain ⟨hf₁, hf₂, hf₃⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf : UniformIntegrable f p μ
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
⊢ UniformIntegrable.{u_1, u_4, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) p μ
have hf₂ : UnifIntegrable f p μ
Tactic: obtain ⟨hf₁, hf₂, hf₃⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf : UniformIntegrable f p μ
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
⊢ UniformIntegrable.{u_1, u_4, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) p μ
have hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
Tactic: obtain ⟨hf₁, hf₂, hf₃⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
⊢ UniformIntegrable.{u_1, u_4, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) p μ
have refine_1 : ∀ (n : ℕ),
  AEStronglyMeasurable.{u_1, u_4} (β := E)
    ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) n) μ
Tactic: refine ⟨fun n => ?_, fun ε hε => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
refine_1 :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_4} (β := E)
      ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) n) μ
⊢ UniformIntegrable.{u_1, u_4, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) p μ
have refine_2 : ∀ (ε : ℝ) (hε : 0 < ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_4} (ε := E)
              (s.indicator ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i))
              p μ ≤
            ENNReal.ofReal ε
Tactic: refine ⟨fun n => ?_, fun ε hε => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
refine_1 :
  ∀ (n : ℕ),
    AEStronglyMeasurable.{u_1, u_4} (β := E)
      ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) n) μ
refine_2 :
  ∀ (ε : ℝ) (hε : 0 < ε),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (i : ℕ) (s : Set α),
        MeasurableSet s →
          (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
            eLpNorm.{u_1, u_4} (ε := E)
                (s.indicator
                  ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i))
                p μ ≤
              ENNReal.ofReal ε
⊢ UniformIntegrable.{u_1, u_4, 0} (β := E)
    (fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) p μ
have refine_3 : ∃ (C : ℝ≥0),
  ∀ (i : ℕ),
    eLpNorm.{u_1, u_4} (ε := E)
        ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i) p μ ≤
      (↑C : ℝ≥0∞)
Tactic: refine ⟨fun n => ?_, fun ε hε => ?_, ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_4} (ε := E)
              (s.indicator ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i))
              p μ ≤
            ENNReal.ofReal ε
have refine_2 : ∀ (δ : ℝ) (hδ₁ : 0 < δ)
  (hδ₂ :
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_4} (ε := E)
              (s.indicator ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i))
              p μ ≤
            ENNReal.ofReal ε
Tactic: obtain ⟨δ, hδ₁, hδ₂⟩ := hf₂ hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ℕ) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_4} (ε := E)
              (s.indicator ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) i))
              p μ ≤
            ENNReal.ofReal ε
have refine_2 : ∀ (n : ℕ) (s : Set α) (hs : MeasurableSet s) (hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ),
  eLpNorm.{u_1, u_4} (ε := E)
      (s.indicator ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) n)) p μ ≤
    ENNReal.ofReal ε
Tactic: refine ⟨δ, hδ₁, fun n s hs hle => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
p : ℝ≥0∞
E : Type u_4
inst : NormedAddCommGroup E
inst_1 : NormedSpace ℝ E
hp : 1 ≤ p
f : ℕ → α → E
hf₁ : ∀ (i : ℕ), AEStronglyMeasurable (f i) μ
hf₂ : UnifIntegrable f p μ
hf₃ : ∃ (C : ℝ≥0), ∀ (i : ℕ), eLpNorm (f i) p μ ≤ (↑C : ℝ≥0∞)
ε : ℝ
hε : 0 < ε
δ : ℝ
hδ₁ : 0 < δ
hδ₂ :
  ∀ (i : ℕ) (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
n : ℕ
s : Set α
hs : MeasurableSet s
hle : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm.{u_1, u_4} (ε := E)
      (s.indicator ((fun (n : ℕ) ↦ HSMul.hSMul (α := ℝ) (β := α → E) (↑n : ℝ)⁻¹ (∑ i ∈ Finset.range n, f i)) n)) p μ ≤
    ENNReal.ofReal ε
have refine_2 : eLpNorm.{u_1, u_4} (ε := E) (∑ i ∈ Finset.range n, s.indicator (HSMul.hSMul (α := ℝ) (↑n : ℝ)⁻¹ (f i))) p μ ≤
  ENNReal.ofReal ε
Tactic: simp_rw [Finset.smul_sum, Finset.indicator_sum]