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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
rw : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
rw₁ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖‖f x‖ ^ p.toReal‖
rw₂ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖‖f x‖‖ ^ p.toReal
⊢ M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
have rw₃ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖f x‖ ^ p.toReal
Tactic: rw [coe_nnnorm, coe_nnnorm, Real.norm_rpow_of_nonneg (norm_nonneg _), norm_norm,
      ← Real.rpow_le_rpow_iff hM' (by positivity)
        (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top), ← Real.rpow_mul (norm_nonneg _),
      mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm, Real.rpow_one]
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
rw : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
rw₁ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖‖f x‖ ^ p.toReal‖
rw₂ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖‖f x‖‖ ^ p.toReal
rw₃ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖f x‖ ^ p.toReal
⊢ M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
have rw₄ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ (‖f x‖ ^ p.toReal) ^ (1 / p.toReal)
Tactic: rw [coe_nnnorm, coe_nnnorm, Real.norm_rpow_of_nonneg (norm_nonneg _), norm_norm,
      ← Real.rpow_le_rpow_iff hM' (by positivity)
        (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top), ← Real.rpow_mul (norm_nonneg _),
      mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm, Real.rpow_one]
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
rw : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
rw₁ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖‖f x‖ ^ p.toReal‖
rw₂ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖‖f x‖‖ ^ p.toReal
rw₃ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖f x‖ ^ p.toReal
rw₄ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ (‖f x‖ ^ p.toReal) ^ (1 / p.toReal)
⊢ M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
have rw₅ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ ‖f x‖ ^ (p.toReal * (1 / p.toReal))
Tactic: rw [coe_nnnorm, coe_nnnorm, Real.norm_rpow_of_nonneg (norm_nonneg _), norm_norm,
      ← Real.rpow_le_rpow_iff hM' (by positivity)
        (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top), ← Real.rpow_mul (norm_nonneg _),
      mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm, Real.rpow_one]
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
rw : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
rw₁ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖‖f x‖ ^ p.toReal‖
rw₂ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖‖f x‖‖ ^ p.toReal
rw₃ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖f x‖ ^ p.toReal
rw₄ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ (‖f x‖ ^ p.toReal) ^ (1 / p.toReal)
rw₅ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ ‖f x‖ ^ (p.toReal * (1 / p.toReal))
⊢ M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
have rw₆ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ HPow.hPow (β := ℝ) ‖f x‖ 1
Tactic: rw [coe_nnnorm, coe_nnnorm, Real.norm_rpow_of_nonneg (norm_nonneg _), norm_norm,
      ← Real.rpow_le_rpow_iff hM' (by positivity)
        (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top), ← Real.rpow_mul (norm_nonneg _),
      mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm, Real.rpow_one]
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
rw : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
rw₁ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖‖f x‖ ^ p.toReal‖
rw₂ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖‖f x‖‖ ^ p.toReal
rw₃ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ≤ ‖f x‖ ^ p.toReal
rw₄ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ (‖f x‖ ^ p.toReal) ^ (1 / p.toReal)
rw₅ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ ‖f x‖ ^ (p.toReal * (1 / p.toReal))
rw₆ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ HPow.hPow (β := ℝ) ‖f x‖ 1
⊢ M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
have rw₇ : M ^ (1 / p.toReal) ≤ ‖f x‖ ↔ M ^ (1 / p.toReal) ≤ ‖f x‖
Tactic: rw [coe_nnnorm, coe_nnnorm, Real.norm_rpow_of_nonneg (norm_nonneg _), norm_norm,
      ← Real.rpow_le_rpow_iff hM' (by positivity)
        (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top), ← Real.rpow_mul (norm_nonneg _),
      mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm, Real.rpow_one]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
p : ℝ≥0∞
f : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
⊢ HPow.hPow (α := ℝ≥0∞) (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖ₑ) x) p.toReal =
    Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (a : α) ↦ ‖‖f a‖ ^ p.toReal‖ₑ) x
have hiff : M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
Tactic: have hiff : M ^ (1 / p.toReal) ≤ ‖f x‖₊ ↔ M ≤ ‖‖f x‖ ^ p.toReal‖₊ := by
    rw [coe_nnnorm, coe_nnnorm, Real.norm_rpow_of_nonneg (norm_nonneg _), norm_norm,
      ← Real.rpow_le_rpow_iff hM' (by positivity)
        (one_div_pos.2 <| ENNReal.toReal_pos hp_ne_zero hp_ne_top), ← Real.rpow_mul (norm_nonneg _),
      mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm, Real.rpow_one]
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
⊢ HPow.hPow (α := ℝ≥0∞) (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖ₑ) x) p.toReal =
    Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (a : α) ↦ ‖‖f a‖ ^ p.toReal‖ₑ) x
have pos : ∀ (hx : Membership.mem (γ := Set α) {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} x),
  HPow.hPow (α := ℝ≥0∞) (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖ₑ) x) p.toReal =
    Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (a : α) ↦ ‖‖f a‖ ^ p.toReal‖ₑ) x
Tactic: by_cases hx : x ∈ { x : α | M ^ (1 / p.toReal) ≤ ‖f x‖₊ }
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
pos :
  ∀ (hx : Membership.mem (γ := Set α) {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} x),
    HPow.hPow (α := ℝ≥0∞) (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖ₑ) x)
        p.toReal =
      Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (a : α) ↦ ‖‖f a‖ ^ p.toReal‖ₑ) x
⊢ HPow.hPow (α := ℝ≥0∞) (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖ₑ) x) p.toReal =
    Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (a : α) ↦ ‖‖f a‖ ^ p.toReal‖ₑ) x
have neg : ∀ (hx : x ∉ {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)}),
  HPow.hPow (α := ℝ≥0∞) (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖ₑ) x) p.toReal =
    Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (a : α) ↦ ‖‖f a‖ ^ p.toReal‖ₑ) x
Tactic: by_cases hx : x ∈ { x : α | M ^ (1 / p.toReal) ≤ ‖f x‖₊ }
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
hx : Membership.mem (γ := Set α) {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} x
⊢ HPow.hPow (α := ℝ≥0∞) (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖ₑ) x) p.toReal =
    Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (a : α) ↦ ‖‖f a‖ ^ p.toReal‖ₑ) x
have pos : Membership.mem (γ := Set α) {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} x
Tactic: rw [Set.indicator_of_mem hx, Set.indicator_of_mem, Real.enorm_of_nonneg (by positivity),
      ← ENNReal.ofReal_rpow_of_nonneg (norm_nonneg _) ENNReal.toReal_nonneg, ofReal_norm]
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
hx : Membership.mem (γ := Set α) {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} x
⊢ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
have pos : M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)
Tactic: rwa [← hiff]
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
hx : x ∉ {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)}
⊢ HPow.hPow (α := ℝ≥0∞) (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖ₑ) x) p.toReal =
    Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (a : α) ↦ ‖‖f a‖ ^ p.toReal‖ₑ) x
have neg : HPow.hPow (α := ℝ≥0∞) 0 p.toReal = 0
Tactic: rw [Set.indicator_of_notMem hx, Set.indicator_of_notMem]
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
hx : x ∉ {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)}
neg : HPow.hPow (α := ℝ≥0∞) 0 p.toReal = 0
⊢ HPow.hPow (α := ℝ≥0∞) (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖ₑ) x) p.toReal =
    Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (a : α) ↦ ‖‖f a‖ ^ p.toReal‖ₑ) x
have neg₁ : x ∉ {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)}
Tactic: rw [Set.indicator_of_notMem hx, Set.indicator_of_notMem]
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
hp_ne_top : ¬p = ∞
M : ℝ
hM' : 0 ≤ M
hM :
  ∫⁻ (x : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
x : α
hiff : M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ) ↔ M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
hx : x ∉ {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)}
⊢ ¬M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)
have neg : ¬M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)
Tactic: rwa [← hiff]
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∃ (M : ℝ), 0 < M ∧ eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
have obtain : ∀ (M : ℝ) (hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε),
  ∃ (M : ℝ), 0 < M ∧ eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨M, hM⟩ := hf.eLpNorm_indicator_norm_ge_le hmeas 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), 0 < M ∧ eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
have M₁ : ∀ (x : α), ‖Set.indicator {x : α | max M 1 ≤ (↑‖f x‖₊ : ℝ)} f x‖ ≤ ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖
Tactic: refine
    ⟨max M 1, lt_of_lt_of_le zero_lt_one (le_max_right _ _), le_trans (eLpNorm_mono fun x => ?_) hM⟩
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ ‖Set.indicator {x : α | max M 1 ≤ (↑‖f x‖₊ : ℝ)} f x‖ ≤ ‖Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f x‖
have simp : LE.le (α := ℝ) (Set.indicator {x : α | max M 1 ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖) x)
  (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖) x)
Tactic: simp only [norm_indicator_eq_indicator_norm]
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
x : α
⊢ LE.le (α := ℝ) (Set.indicator {x : α | max M 1 ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖) x)
    (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖) x)
have h₁ : 0 ≤ ‖f x‖
Tactic: grw [← le_max_left]
-- 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
M : ℝ
hM : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
x : α
h₁ : 0 ≤ ‖f x‖
⊢ LE.le (α := ℝ) (Set.indicator {x : α | max M 1 ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖) x)
    (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖) x)
have grw : LE.le (α := ℝ) (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖) x)
  (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} (fun (a : α) ↦ ‖f a‖) x)
Tactic: grw [← le_max_left]
-- 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_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (hM : M ≤ 0),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases! hM : M ≤ 0
-- 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_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
pos :
  ∀ (hM : M ≤ 0),
    ∃ (δ : ℝ) (_ : 0 < δ),
      ∀ (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 neg : ∀ (hM : 0 < M),
  ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases! hM : M ≤ 0
-- 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_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (s : Set α),
  MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal 1 → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Tactic: refine ⟨1, zero_lt_one, fun 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_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
h : MeasurableSet s
h_1 : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal 1
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have pos : eLpNorm.{u_1, u_2} (ε := β) (s.indicator 0) p μ ≤ ENNReal.ofReal ε
Tactic: rw [(_ : f = 0)]
-- 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_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
h : MeasurableSet s
h_1 : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal 1
pos : eLpNorm.{u_1, u_2} (ε := β) (s.indicator 0) p μ ≤ ENNReal.ofReal ε
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have rw : f = 0
Tactic: rw [(_ : f = 0)]
-- 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_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
h : MeasurableSet s
h_1 : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal 1
⊢ f = 0
have h : ∀ (x : α), f x = 0 x
Tactic: ext x
-- 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_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : M ≤ 0
s : Set α
h : MeasurableSet s
h_1 : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal 1
x : α
⊢ f x = 0 x
have h : ‖f x‖ ≤ 0
Tactic: rw [Pi.zero_apply, ← norm_le_zero_iff]
-- 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_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
⊢ ∃ (δ : ℝ) (_ : 0 < δ),
    ∀ (s : Set α),
      MeasurableSet s → (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal δ → eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have neg : ∀ (s : Set α) (hs : MeasurableSet s) (hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)),
  eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Tactic: refine ⟨(ε / M) ^ p.toReal, Real.rpow_pos_of_pos (div_pos hε hM) _, fun s hs 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_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (hp : p = 0), eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hp : p = 0
-- 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_top : p ≠ ∞
ε : ℝ
hε : 0 < ε
M : ℝ
hf : ∀ (x : α), ‖f x‖ < M
hM : 0 < M
s : Set α
hs : MeasurableSet s
hμ : (μ : (a : Set α) → ℝ≥0∞) s ≤ ENNReal.ofReal ((ε / M) ^ p.toReal)
pos : ∀ (hp : p = 0), eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
⊢ eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
have neg : ∀ (hp : ¬p = 0), eLpNorm (s.indicator f) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hp : p = 0