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 : ι), 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
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
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 : ι → α → β
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
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 : ι → α → β
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
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 : ι → α → β
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
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
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 : ι → α → β
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
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 : ι → α → β
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
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 (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)
hfu : UniformIntegrable f p μ
ε : ℝ
hε : 0 < ε
⊢ ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (hfu : UnifIntegrable f p μ) (M : ℝ≥0) (hM : ∀ (i : ι), eLpNorm (f i) p μ ≤ (↑M : ℝ≥0∞)),
  ∃ (C : ℝ≥0), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨-, hfu, M, hM⟩ := hfu
Cleared hypotheses: hfu
-- 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), ∀ (i : ι), eLpNorm (indicator {x : α | C ≤ ‖f i x‖₊} (f i)) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (δ : ℝ) (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 ε
Tactic: obtain ⟨δ, hδpos, hδ⟩ := hfu 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 ≠ ∞
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 : ι), (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f i x‖₊} ≤ ENNReal.ofReal δ
have by_contra! : ∀ (hcon : ∀ (C : ℝ≥0), ∃ (i : ι), ENNReal.ofReal δ < (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f i x‖₊}), False
Tactic: by_contra! hcon
-- 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 ε
hcon : ∀ (C : ℝ≥0), ∃ (i : ι), ENNReal.ofReal δ < (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f i x‖₊}
⊢ False
have choose : ∀ (ℐ : (C : ℝ≥0) → ι) (hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal δ < (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f (ℐ C) x‖₊}), False
Tactic: choose ℐ hℐ using hcon
Cleared hypotheses: hcon
-- 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) → ι
hℐ : ∀ (C : ℝ≥0), ENNReal.ofReal δ < (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f (ℐ C) x‖₊}
⊢ False
have lift : ∀ (δ : ℝ≥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‖₊}), False
Tactic: lift δ to ℝ≥0 using hδpos.le
Cleared hypotheses: δ, hδpos, hδ, hℐ
-- 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 ≠ ∞
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‖₊}
C : ℝ≥0
⊢ (↑C : ℝ≥0∞) * (↑δ : ℝ≥0∞) ^ (1 / p.toReal) ≤
    (↑C : ℝ≥0∞) * HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f (ℐ C) x‖₊} : ℝ≥0∞) (1 / p.toReal)
have hℐ₁ : ∀ (C : ℝ≥0), (↑δ : ℝ≥0∞) < (μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f (ℐ C) x‖₊}
Tactic: simp_rw [ENNReal.ofReal_coe_nnreal] at 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∞
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‖₊}
C : ℝ≥0
⊢ C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f (ℐ C) x‖₊} : ℝ≥0∞) (1 / p.toReal) ≤
    eLpNorm (indicator {x : α | C ≤ ‖f (ℐ C) x‖₊} (f (ℐ C))) p μ
have refine : ∀ (x : α) (hx : Membership.mem (γ := Set α) {x : α | C ≤ ‖f (ℐ C) x‖₊} x),
  C ≤ ‖indicator {x : α | C ≤ ‖f (ℐ C) x‖₊} (f (ℐ C)) x‖₊
Tactic: refine le_eLpNorm_of_bddBelow hp hp' _
            (measurableSet_le measurable_const (hf _).nnnorm.measurable)
            (Eventually.of_forall fun 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 ≠ ∞
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‖₊}
C : ℝ≥0
x : α
hx : Membership.mem (γ := Set α) {x : α | C ≤ ‖f (ℐ C) x‖₊} x
⊢ C ≤ ‖indicator {x : α | C ≤ ‖f (ℐ C) x‖₊} (f (ℐ C)) x‖₊
have rwa : C ≤ indicator {x : α | C ≤ ‖f (ℐ C) x‖₊} (fun (a : α) ↦ ‖f (ℐ C) a‖₊) x
Tactic: rwa [nnnorm_indicator_eq_indicator_nnnorm, 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 ≠ ∞
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‖₊}
C : ℝ≥0
x : α
hx : Membership.mem (γ := Set α) {x : α | C ≤ ‖f (ℐ C) x‖₊} x
rwa : C ≤ indicator {x : α | C ≤ ‖f (ℐ C) x‖₊} (fun (a : α) ↦ ‖f (ℐ C) a‖₊) x
⊢ C ≤ ‖indicator {x : α | C ≤ ‖f (ℐ C) x‖₊} (f (ℐ C)) x‖₊
have rwa₁ : C ≤ ‖f (ℐ C) x‖₊
Tactic: rwa [nnnorm_indicator_eq_indicator_nnnorm, 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 ≠ ∞
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‖₊}
C : ℝ≥0
⊢ C • (↑δ : ℝ≥0∞) ^ (1 / p.toReal) ≤ eLpNorm (f (ℐ C)) p μ
have C₁ : C • (↑δ : ℝ≥0∞) ^ (1 / p.toReal) ≤
  C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f (ℐ C) x‖₊} : ℝ≥0∞) (1 / p.toReal)
Tactic: 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 _
-- 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‖₊}
C : ℝ≥0
C₁ :
  C • (↑δ : ℝ≥0∞) ^ (1 / p.toReal) ≤
    C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f (ℐ C) x‖₊} : ℝ≥0∞) (1 / p.toReal)
⊢ C • (↑δ : ℝ≥0∞) ^ (1 / p.toReal) ≤ eLpNorm (f (ℐ C)) p μ
have C₂ : C • HPow.hPow (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | C ≤ ‖f (ℐ C) x‖₊} : ℝ≥0∞) (1 / p.toReal) ≤
  eLpNorm (indicator {x : α | C ≤ ‖f (ℐ C) x‖₊} (f (ℐ C))) p μ
Tactic: 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 _
-- 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 ≠ ∞
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‖₊}
⊢ False
have this : ∀ (C : ℝ≥0), C • (↑δ : ℝ≥0∞) ^ (1 / p.toReal) ≤ eLpNorm (f (ℐ C)) p μ
Tactic: 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 _
-- 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 ≠ ∞
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 : ∀ (C : ℝ≥0), C • (↑δ : ℝ≥0∞) ^ (1 / p.toReal) ≤ eLpNorm (f (ℐ C)) p μ
⊢ False
have this₁ : (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)) • (↑δ : ℝ≥0∞) ^ (1 / p.toReal) ≤
  eLpNorm (f (ℐ (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)))) p μ
Tactic: specialize this (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal))
Cleared hypotheses: this
-- 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 ≠ ∞
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 * max M 1 * δ⁻¹ ^ (1 / p.toReal)) • (↑δ : ℝ≥0∞) ^ (1 / p.toReal) ≤
    eLpNorm (f (ℐ (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)))) p μ
⊢ False
have this₁ : (↑2 : ℝ≥0∞) * (↑(max M 1) : ℝ≥0∞) ≤ eLpNorm (f (ℐ (2 * max M 1 * δ⁻¹ ^ (1 / p.toReal)))) p μ
Tactic: 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
Cleared hypotheses: this
-- 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 μ
⊢ False
have refine : max (↑M : ℝ≥0∞) 1 < (↑2 : ℝ≥0∞) * (↑(max M 1) : ℝ≥0∞)
Tactic: 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