awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
x : α
hx : M ≤ ‖f x‖
⊢ f x = (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) x
have pos : x ∉ {x : α | ‖f x‖ < M}
Tactic: rw [Pi.add_apply, Set.indicator_of_mem, Set.indicator_of_notMem, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
x : α
hx : M ≤ ‖f x‖
pos : x ∉ {x : α | ‖f x‖ < M}
⊢ f x = (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) x
have pos₁ : Membership.mem (γ := Set α) {x : α | M ≤ (↑‖f x‖₊ : ℝ)} x
Tactic: rw [Pi.add_apply, Set.indicator_of_mem, Set.indicator_of_notMem, add_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
x : α
hx : ¬M ≤ ‖f x‖
⊢ f x = (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) x
have neg : Membership.mem (γ := Set α) {x : α | ‖f x‖ < M} x
Tactic: rw [Pi.add_apply, Set.indicator_of_notMem, Set.indicator_of_mem, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hMpos : 0 < M
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
        eLpNorm (s.indicator (Set.indicator {x : α | ‖f x‖ < M} f)) p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
x : α
hx : ¬M ≤ ‖f x‖
neg : Membership.mem (γ := Set α) {x : α | ‖f x‖ < M} x
⊢ f x = (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f + Set.indicator {x : α | ‖f x‖ < M} f) x
have neg₁ : x ∉ {x : α | M ≤ (↑‖f x‖₊ : ℝ)}
Tactic: rw [Pi.add_apply, Set.indicator_of_notMem, Set.indicator_of_mem, zero_add]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (δ : ℝ) (hδpos : 0 < δ)
  (hδ :
    ∀ (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨δ, hδpos, hδ⟩ := hf.eLpNorm_indicator_le' hp_one hp_top hmeas (half_pos hε)
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have refine : ∀ (s : Set α) (hs : MeasurableSet s) (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ),
  2 * ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal ε
Tactic: refine ⟨δ, hδpos, fun s hs hμs => le_trans (hδ s hs hμs) ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ 2 * ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal ε
have ha₀ : Ne (α := ℝ≥0∞) 2 0
Tactic: rw [ENNReal.ofReal_div_of_pos zero_lt_two, (by simp : ENNReal.ofReal 2 = 2),
      ENNReal.mul_div_cancel]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ 2 * ENNReal.ofReal (ε / 2)
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
ha₀ : Ne (α := ℝ≥0∞) 2 0
⊢ 2 * ENNReal.ofReal (ε / 2) ≤ ENNReal.ofReal ε
have ha : Ne (α := ℝ≥0∞) 2 ∞
Tactic: rw [ENNReal.ofReal_div_of_pos zero_lt_two, (by simp : ENNReal.ofReal 2 = 2),
      ENNReal.mul_div_cancel]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
hf : MemLp f p μ
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have obtain : eLpNorm f p μ < ∞ →
  ∀ (f' : α → β) (hf' : StronglyMeasurable f') (heq : f =ᶠ[ae μ] f'),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (s : Set α),
        MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨⟨f', hf', heq⟩, _⟩ := hf
Cleared hypotheses: hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right : eLpNorm f p μ < ∞
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (δ : ℝ) (hδpos : 0 < δ)
  (hδ :
    ∀ (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨δ, hδpos, hδ⟩ := (hℒp.ae_eq heq).eLpNorm_indicator_le_of_meas hp_one hp_top hf' hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right : eLpNorm f p μ < ∞
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have refine : ∀ (s : Set α) (hs : MeasurableSet s) (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ),
  eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Tactic: refine ⟨δ, hδpos, fun s hs hμs => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right : eLpNorm f p μ < ∞
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have h : eLpNorm (s.indicator f) p μ = eLpNorm (s.indicator f') p μ
Tactic: convert! hδ s hs hμs using 1
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hp_one : 1 ≤ p
hp_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
hℒp : MemLp f p μ
right : eLpNorm f p μ < ∞
f' : α → β
hf' : StronglyMeasurable f'
heq : f =ᶠ[ae μ] f'
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (s : Set α),
    MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f') p μ ≤ ENNReal.ofReal ε
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ
⊢ eLpNorm (s.indicator f) p μ = eLpNorm (s.indicator f') p μ
have h : eLpNorm f p (μ.restrict s) = eLpNorm f' p (μ.restrict s)
Tactic: rw [eLpNorm_indicator_eq_eLpNorm_restrict hs, eLpNorm_indicator_eq_eLpNorm_restrict hs]
-- 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∞
g : α → β
hp : 1 ≤ p
hp_ne_top : p ≠ ∞
hg : MemLp g p μ
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β) (s.indicator ((fun (x : ι) ↦ g) i)) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (δ : ℝ) (hδ_pos : 0 < δ)
  (hgδ :
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator g) p μ ≤ ENNReal.ofReal ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ →
          eLpNorm.{u_1, u_2} (ε := β) (s.indicator ((fun (x : ι) ↦ g) i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨δ, hδ_pos, hgδ⟩ := hg.eLpNorm_indicator_le hp hp_ne_top 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∞
inst_1 : Subsingleton ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (hι : Nonempty ι),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hι : Nonempty ι
-- 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∞
inst_1 : Subsingleton ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
pos :
  ∀ (hι : Nonempty ι),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (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 (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have neg : ∀ (hι : ¬Nonempty ι),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hι : Nonempty ι
-- 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∞
inst_1 : Subsingleton ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
hι : Nonempty ι
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (i : ι),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨i⟩ := hι
Cleared hypotheses: 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∞
inst_1 : Subsingleton ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
i : ι
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : ι) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (δ : ℝ) (hδpos : 0 < δ)
  (hδ :
    ∀ (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 (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨δ, hδpos, hδ⟩ := (hf i).eLpNorm_indicator_le hp_one hp_top 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∞
inst_1 : Subsingleton ι
hp_one : 1 ≤ p
hp_top : p ≠ ∞
f : ι → α → β
hf : ∀ (i : ι), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
i : ι
δ : ℝ
hδpos : 0 < δ
hδ :
  ∀ (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 (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (j : ι) (s : Set α) (hs : MeasurableSet s) (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ),
  eLpNorm (s.indicator (f j)) p μ ≤ ENNReal.ofReal ε
Tactic: refine ⟨δ, hδpos, fun j s hs hμs => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
f : Fin n → α → β
hf : ∀ (i : Fin n), MemLp (f i) p μ
⊢ UnifIntegrable f p μ
have revert : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifIntegrable f p μ
Tactic: revert f
Cleared hypotheses: f, hf
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun (k : Fin n) ↦ f k.castSucc
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : Fin (n + 1)) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have hgLp : ∀ (i : Fin n), MemLp (g i) p μ
Tactic: have hgLp : ∀ i, MemLp (g i) p μ := fun i => hfLp i.castSucc
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun (k : Fin n) ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : Fin (n + 1)) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have succ : ∀ (δ₁ : ℝ) (hδ₁pos : 0 < δ₁)
  (hδ₁ :
    ∀ (i : Fin n) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : Fin (n + 1)) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨δ₁, hδ₁pos, hδ₁⟩ := h hgLp hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun (k : Fin n) ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : Fin (n + 1)) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have succ : ∀ (δ₂ : ℝ) (hδ₂pos : 0 < δ₂)
  (hδ₂ :
    ∀ (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : Fin (n + 1)) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨δ₂, hδ₂pos, hδ₂⟩ := (hfLp (Fin.last n)).eLpNorm_indicator_le hp_one hp_top hε
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun (k : Fin n) ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (i : Fin (n + 1)) (s : Set α),
      MeasurableSet s →
        (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have succ : ∀ (i : Fin (n + 1)) (s : Set α) (hs : MeasurableSet s) (hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal (min δ₁ δ₂)),
  eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: refine ⟨min δ₁ δ₂, lt_min hδ₁pos hδ₂pos, fun i s hs hμs => ?_⟩
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun (k : Fin n) ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
i : Fin (n + 1)
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal (min δ₁ δ₂)
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (hi : (↑i : ℕ) < n), eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases! hi : i.val < n
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
hp_one : 1 ≤ p
hp_top : p ≠ ∞
n : ℕ
h : ∀ {f : Fin n → α → β} (hf : ∀ (i : Fin n), MemLp (f i) p μ), UnifIntegrable f p μ
f : Fin (n + 1) → α → β
hfLp : ∀ (i : Fin (n + 1)), MemLp (f i) p μ
ε : ℝ
hε : 0 < ε
g : Fin n → α → β := fun (k : Fin n) ↦ f k.castSucc
hgLp : ∀ (i : Fin n), MemLp (g i) p μ
δ₁ : ℝ
hδ₁pos : 0 < δ₁
hδ₁ :
  ∀ (i : Fin n) (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₁ → eLpNorm (s.indicator (g i)) p μ ≤ ENNReal.ofReal ε
δ₂ : ℝ
hδ₂pos : 0 < δ₂
hδ₂ :
  ∀ (s : Set α),
    MeasurableSet s →
      (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ₂ → eLpNorm (s.indicator (f (Fin.last n))) p μ ≤ ENNReal.ofReal ε
i : Fin (n + 1)
s : Set α
hs : MeasurableSet s
hμs : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal (min δ₁ δ₂)
pos : ∀ (hi : (↑i : ℕ) < n), eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
⊢ eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
have neg : ∀ (hi : n ≤ (↑i : ℕ)), eLpNorm (s.indicator (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases! hi : i.val < n