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 β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : Membership.mem (γ := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} x
⊢ Membership.mem (γ := Set α) {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)} x
have rw : (eLpNormEssSup f μ).toReal < ‖f x‖
Tactic: rw [Set.mem_setOf_eq, ← ENNReal.toReal_lt_toReal hbdd.ne ENNReal.coe_lt_top.ne,
          ENNReal.coe_toReal, coe_nnnorm]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : Membership.mem (γ := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} x
⊢ (eLpNormEssSup f μ).toReal < ‖f x‖
have refine : (eLpNormEssSup f μ).toReal < (eLpNormEssSup f μ + 1).toReal
Tactic: refine lt_of_lt_of_le ?_ hx
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : Membership.mem (γ := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} x
⊢ (eLpNormEssSup f μ).toReal < (eLpNormEssSup f μ + 1).toReal
have rw : eLpNormEssSup f μ < eLpNormEssSup f μ + 1
Tactic: rw [ENNReal.toReal_lt_toReal hbdd.ne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
x : α
hx : Membership.mem (γ := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} x
rw : eLpNormEssSup f μ < eLpNormEssSup f μ + 1
⊢ (eLpNormEssSup f μ).toReal < (eLpNormEssSup f μ + 1).toReal
have rw₁ : eLpNormEssSup f μ + 1 ≠ ∞
Tactic: rw [ENNReal.toReal_lt_toReal hbdd.ne]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} : ℝ≥0∞) (0 : ℝ≥0∞)
have this : Subset.{u_1} (α := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
  {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
Tactic: have : { x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖ } ⊆
          { x : α | eLpNormEssSup f μ < ‖f x‖₊ } := by
        intro x hx
        rw [Set.mem_setOf_eq, ← ENNReal.toReal_lt_toReal hbdd.ne ENNReal.coe_lt_top.ne,
          ENNReal.coe_toReal, coe_nnnorm]
        refine lt_of_lt_of_le ?_ hx
        rw [ENNReal.toReal_lt_toReal hbdd.ne]
        · exact ENNReal.lt_add_right hbdd.ne one_ne_zero
        · finiteness
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
this :
  Subset.{u_1} (α := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
    {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} : ℝ≥0∞) (0 : ℝ≥0∞)
have rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: rw [← nonpos_iff_eq_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
this :
  Subset.{u_1} (α := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
    {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} : ℝ≥0∞) (0 : ℝ≥0∞)
have refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: refine (measure_mono this).trans ?_
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
this :
  Subset.{u_1} (α := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
    {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (0 : ℝ≥0∞)
have hle : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ
Tactic: have hle := enorm_ae_le_eLpNormEssSup f μ
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
this :
  Subset.{u_1} (α := Set α) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖}
    {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)}
hle : ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (0 : ℝ≥0∞)
have hle₁ : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | eLpNormEssSup f μ < ‖f a‖ₑ} : ℝ≥0∞) (0 : ℝ≥0∞)
Tactic: simp_rw [ae_iff, not_le] at hle
Cleared hypotheses: hle
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (hypothesis)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
⊢ eLpNormEssSup f (μ.restrict {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)}) = 0
have this : μ.restrict {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)} = 0
Tactic: have : μ.restrict { x : α | (eLpNorm f ⊤ μ + 1).toReal ≤ ‖f x‖₊ } = 0 := by
      simp only [coe_nnnorm, eLpNorm_exponent_top, Measure.restrict_eq_zero]
      have : { x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖ } ⊆
          { x : α | eLpNormEssSup f μ < ‖f x‖₊ } := by
        intro x hx
        rw [Set.mem_setOf_eq, ← ENNReal.toReal_lt_toReal hbdd.ne ENNReal.coe_lt_top.ne,
          ENNReal.coe_toReal, coe_nnnorm]
        refine lt_of_lt_of_le ?_ hx
        rw [ENNReal.toReal_lt_toReal hbdd.ne]
        · exact ENNReal.lt_add_right hbdd.ne one_ne_zero
        · finiteness
      rw [← nonpos_iff_eq_zero]
      refine (measure_mono this).trans ?_
      have hle := enorm_ae_le_eLpNormEssSup f μ
      simp_rw [ae_iff, not_le] at hle
      exact nonpos_iff_eq_zero.2 hle
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
this : μ.restrict {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)} = 0
⊢ eLpNormEssSup f (μ.restrict {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)}) = 0
have rw : eLpNormEssSup (m0 := m) f 0 = 0
Tactic: rw [this, eLpNormEssSup_measure_zero]
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
this : μ.restrict {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)} = 0
rw : eLpNormEssSup (m0 := m) f 0 = 0
⊢ eLpNormEssSup f (μ.restrict {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)}) = 0
have rw₁ : Eq (α := ℝ≥0∞) 0 0
Tactic: rw [this, eLpNormEssSup_measure_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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
⊢ ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (hp_ne_zero : p = 0), ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hp_ne_zero : 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
pos : ∀ (hp_ne_zero : p = 0), ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
have neg : ∀ (hp_ne_zero : ¬p = 0), ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hp_ne_zero : 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 : α → β
hf : MemLp f p μ
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hp_ne_zero : ¬p = 0
⊢ ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (hp_ne_top : p = ∞), ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hp_ne_top : p = ∞
-- 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
pos : ∀ (hp_ne_top : p = ∞), ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
have neg : ∀ (hp_ne_top : ¬p = ∞), ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
Tactic: by_cases hp_ne_top : p = ∞
-- 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 : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
have pos : ∀ (hf : MemLp f ∞ μ) (hp_ne_zero : ¬Eq (α := ℝ≥0∞) ∞ 0),
  ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) ∞ μ ≤ ENNReal.ofReal ε
Tactic: subst hp_ne_top
Cleared hypotheses: p, hf, hp_ne_zero, hp_ne_top
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : MemLp f ∞ μ
hp_ne_zero : ¬Eq (α := ℝ≥0∞) ∞ 0
⊢ ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) ∞ μ ≤ ENNReal.ofReal ε
have pos : ∀ (M : ℝ) (hM : eLpNormEssSup (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) μ = 0),
  ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) ∞ μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨M, hM⟩ := hf.eLpNormEssSup_indicator_norm_ge_eq_zero hmeas
-- Lean 4 proof step from Mathlib.MeasureTheory.Function.UniformIntegrable (goal)
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hmeas : StronglyMeasurable f
ε : ℝ
hε : 0 < ε
hf : MemLp f ∞ μ
hp_ne_zero : ¬Eq (α := ℝ≥0∞) ∞ 0
M : ℝ
hM : eLpNormEssSup (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) μ = 0
⊢ ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) ∞ μ ≤ ENNReal.ofReal ε
have pos : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) ∞ μ ≤ ENNReal.ofReal ε
Tactic: refine ⟨M, ?_⟩
-- 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 : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
have neg : ∀ (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)),
  ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
Tactic: obtain ⟨M, hM', hM⟩ := MemLp.integral_indicator_norm_ge_nonneg_le
    (μ := μ) (hf.norm_rpow hp_ne_zero hp_ne_top) (Real.rpow_pos_of_pos hε p.toReal)
-- 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)
⊢ ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
have neg : eLpNorm (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
Tactic: refine ⟨M ^ (1 / p.toReal), ?_⟩
-- 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)
⊢ eLpNorm (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
have neg : (∫⁻ (x : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤
  HPow.hPow (β := ℝ) (ENNReal.ofReal ε) 1
Tactic: rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_ne_zero hp_ne_top, ← ENNReal.rpow_one (.ofReal ε)]
-- 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)
| HPow.hPow (β := ℝ) (ENNReal.ofReal ε) 1
have rw : ENNReal.ofReal ε ^ (p.toReal * (1 / p.toReal))
Tactic: rw [← mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm]
-- 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 : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤
    HPow.hPow (β := ℝ) (ENNReal.ofReal ε) 1
have neg : (∫⁻ (x : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤
  ENNReal.ofReal ε ^ (p.toReal * (1 / p.toReal))
Tactic: conv_rhs => rw [← mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm]
-- 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 : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤
    ENNReal.ofReal ε ^ (p.toReal * (1 / p.toReal))
have neg : (∫⁻ (x : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤
  (ENNReal.ofReal ε ^ p.toReal) ^ (1 / p.toReal)
Tactic: rw [ENNReal.rpow_mul]
-- 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 : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤
    (ENNReal.ofReal ε ^ p.toReal) ^ (1 / p.toReal)
have neg : ∫⁻ (x : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ ≤
  ENNReal.ofReal ε ^ p.toReal
Tactic: gcongr
-- 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 : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ ≤
    ENNReal.ofReal ε ^ p.toReal
have neg : ∫⁻ (x : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ ≤
  ENNReal.ofReal (ε ^ p.toReal)
Tactic: rw [ENNReal.ofReal_rpow_of_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 : α → β
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 : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
have h : ∀ (x : α),
  ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal =
    ENorm.enorm (E := ℝ) (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x)
Tactic: convert! hM using 3 with 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 : α
⊢ ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal =
    ENorm.enorm (E := ℝ) (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x)
have h : 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: rw [enorm_indicator_eq_indicator_enorm, enorm_indicator_eq_indicator_enorm]
-- 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 : α
⊢ 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‖₊ : ℝ)
⊢ 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‖
⊢ 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]