awhecmu/canonical-drafter-extract-mathlib huggingface dataset:
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : p.toReal = 0
pos : ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ 1) atTop) ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞

Tactic:
simp only [hp0, ENNReal.rpow_zero]

Premises used: ENNReal.rpow_zero
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : p.toReal = 0
pos : ∀ (a : α), LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ 1) atTop) ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ 1) atTop) ∞

Tactic:
filter_upwards with _
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : p.toReal = 0
a : α
pos : LT.lt (α := ℝ≥0∞) 1 ∞
⊢ LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ 1) atTop) ∞

Tactic:
rw [liminf_const (1 : ℝ≥0∞)]

Premises used: Filter.liminf_const, OfNat.ofNat
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : p.toReal = 0
a : α
⊢ LT.lt (α := ℝ≥0∞) 1 ∞

Tactic:
ENNReal.one_lt_top

Premises used: ENNReal.one_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : p.toReal = 0
a : α
⊢ LT.lt (α := ℝ≥0∞) 1 ∞

Tactic:
exact ENNReal.one_lt_top

Premises used: ENNReal.one_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : ¬p.toReal = 0
h : p = 0
⊢ False

Tactic:
simp [h] at hp0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : ¬p.toReal = 0
⊢ p ≠ 0

Tactic:
have hp : p ≠ 0 := fun h => by simp [h] at hp0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
h : p = ∞
⊢ False

Tactic:
simp [h] at hp0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
⊢ p ≠ ∞

Tactic:
have hp' : p ≠ ∞ := fun h => by simp [h] at hp0
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
⊢ (↑R : ℝ≥0∞) ^ p.toReal < ∞

Tactic:
finiteness
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
neg : liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), (↑‖f i a‖₊ : ℝ≥0∞) ^ p.toReal ∂μ) atTop ≤ (↑R : ℝ≥0∞) ^ p.toReal
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞

Tactic:
refine
    ae_lt_top (.liminf fun n => (hfmeas n).nnnorm.coe_nnreal_ennreal.pow_const p.toReal)
      (lt_of_le_of_lt
          (lintegral_liminf_le fun n => (hfmeas n).nnnorm.coe_nnreal_ennreal.pow_const p.toReal)
          (lt_of_le_of_lt ?_ (by finiteness : (R : ℝ≥0∞) ^ p.toReal < ∞))).ne

Premises used: lt_of_le_of_lt, Measurable.coe_nnreal_ennreal, MeasureTheory.lintegral_liminf_le, Measurable.nnnorm, ENNReal.toReal, Measurable.liminf, Measurable.pow_const, LT.lt.ne, MeasureTheory.ae_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
⊢ ∀ (n : ℕ), (∫⁻ (x : α), ‖f n x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤ (↑R : ℝ≥0∞)

Tactic:
simp_rw [eLpNorm_eq_lintegral_rpow_enorm_toReal hp hp', one_div] at hbdd

Premises used: one_div, MeasureTheory.eLpNorm_eq_lintegral_rpow_enorm_toReal
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
hbdd : ∀ (n : ℕ), (∫⁻ (x : α), ‖f n x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤ (↑R : ℝ≥0∞)
neg :
  sSup {a : ℝ≥0∞ | ∃ (a_1 : ℕ), ∀ b ≥ a_1, a ≤ ∫⁻ (a : α), (↑‖f b a‖₊ : ℝ≥0∞) ^ p.toReal ∂μ} ≤ (↑R : ℝ≥0∞) ^ p.toReal
⊢ liminf (fun (i : ℕ) ↦ ∫⁻ (a : α), (↑‖f i a‖₊ : ℝ≥0∞) ^ p.toReal ∂μ) atTop ≤ (↑R : ℝ≥0∞) ^ p.toReal

Tactic:
simp_rw [liminf_eq, eventually_atTop]

Premises used: Filter.liminf_eq, Filter.eventually_atTop
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
hbdd : ∀ (n : ℕ), (∫⁻ (x : α), ‖f n x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤ (↑R : ℝ≥0∞)
⊢ sSup {a : ℝ≥0∞ | ∃ (a_1 : ℕ), ∀ b ≥ a_1, a ≤ ∫⁻ (a : α), (↑‖f b a‖₊ : ℝ≥0∞) ^ p.toReal ∂μ} ≤ (↑R : ℝ≥0∞) ^ p.toReal

Tactic:
sSup_le fun b ⟨a, ha⟩ =>
      (ha a le_rfl).trans ((ENNReal.rpow_inv_le_iff (ENNReal.toReal_pos hp hp')).1 (hbdd _))

Premises used: ENNReal.ofNNReal, le_rfl, _private.0.MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd.match_2, ENNReal.rpow_inv_le_iff, LE.le, ENNReal.toReal_pos, ENNReal.toReal, HPow.hPow, Iff.mp, LE.le.trans, sSup_le
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ∞
hbdd : ∀ (n : ℕ), (∫⁻ (x : α), ‖f n x‖ₑ ^ p.toReal ∂μ) ^ p.toReal⁻¹ ≤ (↑R : ℝ≥0∞)
⊢ sSup {a : ℝ≥0∞ | ∃ (a_1 : ℕ), ∀ b ≥ a_1, a ≤ ∫⁻ (a : α), (↑‖f b a‖₊ : ℝ≥0∞) ^ p.toReal ∂μ} ≤ (↑R : ℝ≥0∞) ^ p.toReal

Tactic:
exact
    sSup_le fun b ⟨a, ha⟩ =>
      (ha a le_rfl).trans ((ENNReal.rpow_inv_le_iff (ENNReal.toReal_pos hp hp')).1 (hbdd _))
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
pos : ∀ (hp' : p = ∞), ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
neg : ∀ (hp' : ¬p = ∞), ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞

Tactic:
by_cases hp' : p = ∞
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : p = ∞
⊢ Ne (α := ℝ≥0∞) ∞ 0

Tactic:
subst hp'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : p = ∞
hp₁ : Ne (α := ℝ≥0∞) ∞ 0
⊢ ∀ (n : ℕ), eLpNorm (f n) ∞ μ ≤ (↑R : ℝ≥0∞)

Tactic:
subst hp'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : Ne (α := ℝ≥0∞) ∞ 0
hbdd : ∀ (n : ℕ), eLpNorm (f n) ∞ μ ≤ (↑R : ℝ≥0∞)
⊢ ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ (↑R : ℝ≥0∞)

Tactic:
simp_rw [eLpNorm_exponent_top] at hbdd

Premises used: MeasureTheory.eLpNorm_exponent_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : Ne (α := ℝ≥0∞) ∞ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ (↑R : ℝ≥0∞)
⊢ ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖f n x‖ₑ < (↑R : ℝ≥0∞) + 1

Tactic:
have : ∀ n, ∀ᵐ x ∂μ, (‖f n x‖ₑ) < R + 1 := fun n =>
      ae_lt_of_essSup_lt
        (lt_of_le_of_lt (hbdd n) <| ENNReal.lt_add_right ENNReal.coe_ne_top one_ne_zero)
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : Ne (α := ℝ≥0∞) ∞ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ (↑R : ℝ≥0∞)
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖f n x‖ₑ < (↑R : ℝ≥0∞) + 1
⊢ ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖f i a‖ₑ < (↑R : ℝ≥0∞) + 1

Tactic:
rw [← ae_all_iff] at this

Premises used: MeasureTheory.ae_all_iff
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : Ne (α := ℝ≥0∞) ∞ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ (↑R : ℝ≥0∞)
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖f i a‖ₑ < (↑R : ℝ≥0∞) + 1
x : α
hx : ∀ (i : ℕ), ‖f i x‖ₑ < (↑R : ℝ≥0∞) + 1
⊢ LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞

Tactic:
lt_of_le_of_lt
        (liminf_le_of_frequently_le' <| Frequently.of_forall fun n => (hx n).le)
        (ENNReal.add_lt_top.2 ⟨ENNReal.coe_lt_top, ENNReal.one_lt_top⟩)

Premises used: Iff.mpr, lt_of_le_of_lt, Filter.Frequently.of_forall, ENNReal.one_lt_top, Filter.liminf_le_of_frequently_le', LT.lt.le, And.intro, ENNReal.add_lt_top, ENNReal.coe_lt_top
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : Ne (α := ℝ≥0∞) ∞ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ (↑R : ℝ≥0∞)
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖f i a‖ₑ < (↑R : ℝ≥0∞) + 1
h :
  ∀ (a : α),
    Membership.mem (γ := Set α)
      {x : α |
        Membership.mem (γ := Set α) {x : α | (fun (a : α) ↦ ∀ (i : ℕ), ‖f i a‖ₑ < (↑R : ℝ≥0∞) + 1) x} x →
          Membership.mem (γ := Set α)
            {x : α | (fun (x : α) ↦ LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞) x} x}
      a
h₁ h₂ :
  ∀ (x : α) (hx : ∀ (i : ℕ), ‖f i x‖ₑ < (↑R : ℝ≥0∞) + 1), LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞

Tactic:
filter_upwards [this] with x hx using lt_of_le_of_lt
        (liminf_le_of_frequently_le' <| Frequently.of_forall fun n => (hx n).le)
        (ENNReal.add_lt_top.2 ⟨ENNReal.coe_lt_top, ENNReal.one_lt_top⟩)
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
h :
  ∀ (x : α) (hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞),
    LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞
⊢ ∀ᵐ (x : α) ∂μ, LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞

Tactic:
filter_upwards [ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd hfmeas hbdd] with x hx

Premises used: MeasureTheory.ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
⊢ 0 < p.toReal

Tactic:
have hppos : 0 < p.toReal := ENNReal.toReal_pos hp hp'
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
⊢ Eq (α := ℝ≥0∞)
    (liminf (fun (n : ℕ) ↦ (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f n x‖ₑ) atTop : ℝ≥0∞)
    ((ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) : ℝ≥0∞)

Tactic:
(OrderIso.liminf_apply (ENNReal.orderIsoRpow p.toReal _) ?_ ?_ ?_ ?_).symm

Premises used: OrderIso.liminf_apply, ENNReal.toReal, ENNReal.orderIsoRpow, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
refine_1 : IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ‖f n x‖ₑ
refine_2 : IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ‖f n x‖ₑ
refine_3 :
  IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
    (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f x_1 x‖ₑ
refine_4 :
  IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
    (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f x_1 x‖ₑ
⊢ Eq (α := ℝ≥0∞)
    (liminf (fun (n : ℕ) ↦ (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f n x‖ₑ) atTop : ℝ≥0∞)
    ((ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) : ℝ≥0∞)

Tactic:
refine (OrderIso.liminf_apply (ENNReal.orderIsoRpow p.toReal _) ?_ ?_ ?_ ?_).symm

Premises used: OrderIso.liminf_apply, ENNReal.toReal, ENNReal.orderIsoRpow, Eq.symm
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ‖f n x‖ₑ

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (n : ℕ) ↦ ‖f n x‖ₑ

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
⊢ IsBoundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
    (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f x_1 x‖ₑ

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
⊢ IsCoboundedUnder (fun (x1 x2 : ℝ≥0∞) ↦ x1 ≥ x2) atTop fun (x_1 : ℕ) ↦
    (ENNReal.orderIsoRpow p.toReal hppos : (a : ℝ≥0∞) → ℝ≥0∞) ‖f x_1 x‖ₑ

Tactic:
isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
⊢ liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal

Tactic:
have :
    liminf (fun n => (‖f n x‖ₑ) ^ p.toReal) atTop =
      liminf (fun n => (‖f n x‖ₑ)) atTop ^ p.toReal := by
    change
      liminf (fun n => ENNReal.orderIsoRpow p.toReal hppos (‖f n x‖ₑ)) atTop =
        ENNReal.orderIsoRpow p.toReal hppos (liminf (fun n => (‖f n x‖ₑ)) atTop)
    refine (OrderIso.liminf_apply (ENNReal.orderIsoRpow p.toReal _) ?_ ?_ ?_ ?_).symm <;>
      isBoundedDefault
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
this :
  liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal
⊢ HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal < ∞

Tactic:
rw [this] at hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
this :
  liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal
hx₁ : HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal < ∞
⊢ 0 < p.toReal

Tactic:
rw [this] at hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop) ∞
hppos : 0 < p.toReal
this :
  liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal
hx₁ : HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal < ∞
hppos₁ : 0 < p.toReal
⊢ liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal

Tactic:
rw [this] at hx
-- Module: Mathlib.MeasureTheory.Function.LpSeminorm.Basic
Goal:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
μ : Measure α
inst : NormedAddCommGroup E
inst_1 : MeasurableSpace E
inst_2 : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ (↑R : ℝ≥0∞)
hp' : ¬p = ∞
x : α
hx : HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal < ∞
hppos : 0 < p.toReal
this :
  liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ ^ p.toReal) atTop =
    HPow.hPow (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) p.toReal
h : HPow.hPow (α := ℝ≥0∞) (liminf (fun (x_1 : ℕ) ↦ ‖f x_1 x‖ₑ) atTop) p.toReal ^ p.toReal⁻¹ < ∞
⊢ LT.lt (α := ℝ≥0∞) (liminf (fun (n : ℕ) ↦ ‖f n x‖ₑ) atTop) ∞

Tactic:
rw [← ENNReal.rpow_one (liminf (‖f · x‖ₑ) atTop), ← mul_inv_cancel₀ hppos.ne.symm,
    ENNReal.rpow_mul]

Premises used: ENNReal.rpow_mul, Filter.liminf, mul_inv_cancel₀, ENNReal.rpow_one, Ne.symm, Filter.atTop, ENorm.enorm, LT.lt.ne