awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 μ + 1 ≠ ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
⊢ 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
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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∞)}
rw : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
rw [← nonpos_iff_eq_zero]

Premises used: nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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∞)

Tactic:
(measure_mono this).trans ?_

Premises used: setOf, MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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∞)}
refine : LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | (eLpNormEssSup f μ + 1).toReal ≤ ‖f x‖} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
refine (measure_mono this).trans ?_

Premises used: MeasureTheory.measure_mono, LE.le.trans
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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∞)}
⊢ ∀ᵐ (x : α) ∂μ, ‖f x‖ₑ ≤ eLpNormEssSup f μ

Tactic:
have hle := enorm_ae_le_eLpNormEssSup f μ
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 μ
⊢ Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | eLpNormEssSup f μ < ‖f a‖ₑ} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
simp_rw [ae_iff, not_le] at hle

Premises used: not_le, MeasureTheory.ae_iff
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | eLpNormEssSup f μ < ‖f a‖ₑ} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
nonpos_iff_eq_zero.2 hle

Premises used: Iff.mpr, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 : Eq (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {a : α | eLpNormEssSup f μ < ‖f a‖ₑ} : ℝ≥0∞) (0 : ℝ≥0∞)
⊢ LE.le (α := ℝ≥0∞) ((μ : (a : Set α) → ℝ≥0∞) {x : α | eLpNormEssSup f μ < (↑‖f x‖₊ : ℝ≥0∞)} : ℝ≥0∞) (0 : ℝ≥0∞)

Tactic:
exact nonpos_iff_eq_zero.2 hle

Premises used: Iff.mpr, nonpos_iff_eq_zero
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
⊢ μ.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
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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
rw₁ rw₂ : Eq (α := ℝ≥0∞) 0 0
⊢ eLpNormEssSup f (μ.restrict {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)}) = 0

Tactic:
rw [this, eLpNormEssSup_measure_zero]

Premises used: MeasureTheory.eLpNormEssSup_measure_zero
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
⊢ MeasurableSet.{u_1} (α := α) {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)}

Tactic:
measurableSet_le measurable_const hmeas.nnnorm.measurable.subtype_coe

Premises used: measurableSet_le, MeasureTheory.StronglyMeasurable.measurable, setOf, Measurable.subtype_coe, MeasureTheory.StronglyMeasurable.nnnorm, measurable_const
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
Goal:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup β
f : α → β
hf : MemLp f ∞ μ
hmeas : StronglyMeasurable f
hbdd : eLpNormEssSup f μ < ∞
⊢ MeasurableSet.{u_1} (α := α) {x : α | (eLpNorm f ∞ μ + 1).toReal ≤ (↑‖f x‖₊ : ℝ)}

Tactic:
exact measurableSet_le measurable_const hmeas.nnnorm.measurable.subtype_coe

Premises used: measurableSet_le, MeasureTheory.StronglyMeasurable.measurable, Measurable.subtype_coe, MeasureTheory.StronglyMeasurable.nnnorm, measurable_const
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 ε
neg : ∀ (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 ε

Tactic:
by_cases hp_ne_zero : p = 0
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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
⊢ eLpNorm (Set.indicator {x : α | 1 ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε

Tactic:
simp [hp_ne_zero]
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 ε

Tactic:
exact ⟨1, by simp [hp_ne_zero]⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 ε
neg : ∀ (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 ε

Tactic:
by_cases hp_ne_top : p = ∞
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 = ∞
pos :
  ∀ (hf : MemLp f ∞ μ) (hp_ne_zero : ¬Eq (α := ℝ≥0∞) ∞ 0),
    ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) ∞ μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε

Tactic:
subst hp_ne_top
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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
pos :
  ∀ (M : ℝ) (hM : eLpNormEssSup (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) μ = 0),
    ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) ∞ μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) ∞ μ ≤ ENNReal.ofReal ε

Tactic:
obtain ⟨M, hM⟩ := hf.eLpNormEssSup_indicator_norm_ge_eq_zero hmeas

Premises used: MeasureTheory.MemLp.eLpNormEssSup_indicator_norm_ge_eq_zero
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 ε

Tactic:
⟨M, ?_⟩

Premises used: Exists.intro
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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
pos : eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) ∞ μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) ∞ μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨M, ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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
⊢ eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) ∞ μ ≤ ENNReal.ofReal ε

Tactic:
simp only [eLpNorm_exponent_top, hM, zero_le]

Premises used: zero_le, MeasureTheory.eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 = ∞
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 ε
⊢ ∃ (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)

Premises used: Real.rpow_pos_of_pos, MeasureTheory.MemLp.norm_rpow, MeasureTheory.MemLp.integral_indicator_norm_ge_nonneg_le, ENNReal.toReal
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 ε

Tactic:
⟨M ^ (1 / p.toReal), ?_⟩

Premises used: HDiv.hDiv, ENNReal.toReal, HPow.hPow, Exists.intro, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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)
neg : eLpNorm (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε
⊢ ∃ (M : ℝ), eLpNorm (Set.indicator {x : α | M ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε

Tactic:
refine ⟨M ^ (1 / p.toReal), ?_⟩
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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)
neg :
  (∫⁻ (x : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤
    HPow.hPow (β := ℝ) (ENNReal.ofReal ε) 1
⊢ eLpNorm (Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f) p μ ≤ ENNReal.ofReal ε

Tactic:
rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp_ne_zero hp_ne_top, ← ENNReal.rpow_one (.ofReal ε)]

Premises used: ENNReal.ofReal, ENNReal.rpow_one, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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)
rw : ENNReal.ofReal ε ^ (p.toReal * (1 / p.toReal))
| HPow.hPow (β := ℝ) (ENNReal.ofReal ε) 1

Tactic:
rw [← mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm]

Premises used: Ne.symm, mul_one_div_cancel, ENNReal.toReal_pos, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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)
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))
⊢ (∫⁻ (x : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ) ^ (1 / p.toReal) ≤
    HPow.hPow (β := ℝ) (ENNReal.ofReal ε) 1

Tactic:
conv_rhs => rw [← mul_one_div_cancel (ENNReal.toReal_pos hp_ne_zero hp_ne_top).ne.symm]

Premises used: Ne.symm, mul_one_div_cancel, ENNReal.toReal_pos, LT.lt.ne
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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)
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)
⊢ (∫⁻ (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]

Premises used: ENNReal.rpow_mul
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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)
neg :
  ∫⁻ (x : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ ≤
    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)

Tactic:
gcongr
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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)
neg :
  ∫⁻ (x : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)
⊢ ∫⁻ (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ε]

Premises used: ENNReal.ofReal_rpow_of_pos
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 : α),
      ENorm.enorm (E := ℝ)
        (Set.indicator {x : α | M ≤ (↑‖‖f x‖ ^ p.toReal‖₊ : ℝ)} (fun (x : α) ↦ ‖f x‖ ^ p.toReal) x) ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)

Tactic:
hM
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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)
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)
⊢ ∫⁻ (x : α), ‖Set.indicator {x : α | M ^ (1 / p.toReal) ≤ (↑‖f x‖₊ : ℝ)} f x‖ₑ ^ p.toReal ∂μ ≤
    ENNReal.ofReal (ε ^ p.toReal)

Tactic:
convert! hM using 3 with x
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 : α
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
⊢ ‖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:
rw [enorm_indicator_eq_indicator_enorm, enorm_indicator_eq_indicator_enorm]

Premises used: enorm_indicator_eq_indicator_enorm
-- Module: Mathlib.MeasureTheory.Function.UniformIntegrable
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 : α
⊢ 0 ≤ ‖f x‖ ^ p.toReal

Tactic:
positivity