-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem ae_bdd_liminf_atTop_of_eLpNorm_bdd {p : ℝ≥0∞} (hp : p ≠ 0) {f : ℕ → α → E}
    (hfmeas : ∀ n, Measurable (f n)) (hbdd : ∀ n, eLpNorm (f n) p μ ≤ R) :
    ∀ᵐ x ∂μ, liminf (fun n => (‖f n x‖ₑ)) atTop < ∞

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Tactic:
by_cases hp' : p = ∞

Result:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : p = ⊤
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

case neg
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Proof state:
case h
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
x : α
hx : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤
hppos : 0 < p.toReal
this : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop = liminf (fun n => ‖f n x‖ₑ) atTop ^ p.toReal
⊢ liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Tactic:
rw [this] at hx

Result:
case h
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
x : α
hx : liminf (fun n => ‖f n x‖ₑ) atTop ^ p.toReal < ⊤
hppos : 0 < p.toReal
this : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop = liminf (fun n => ‖f n x‖ₑ) atTop ^ p.toReal
⊢ liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Proof state:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : ⊤ ≠ 0
hbdd : ∀ (n : ℕ), eLpNorm (f n) ⊤ μ ≤ ↑R
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Tactic:
simp_rw [eLpNorm_exponent_top] at hbdd

Result:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : ⊤ ≠ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ ↑R
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Proof state:
case h
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
x : α
hx : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤
hppos : 0 < p.toReal
⊢ liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

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

Result:
case h
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
x : α
hx : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤
hppos : 0 < p.toReal
this : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop = liminf (fun n => ‖f n x‖ₑ) atTop ^ p.toReal
⊢ liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
x : α
hx : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤
hppos : 0 < p.toReal
⊢ liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop = liminf (fun n => ‖f n x‖ₑ) atTop ^ p.toReal

Tactic:
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)

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
x : α
hx : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤
hppos : 0 < p.toReal
⊢ liminf (fun n => (ENNReal.orderIsoRpow p.toReal hppos) ‖f n x‖ₑ) atTop =
    (ENNReal.orderIsoRpow p.toReal hppos) (liminf (fun n => ‖f n x‖ₑ) atTop)

Proof state:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : ⊤ ≠ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ ↑R
this : ∀ (n : ℕ), ∀ᵐ (x : α) ∂μ, ‖f n x‖ₑ < ↑R + 1
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Tactic:
rw [← ae_all_iff] at this

Result:
case pos
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp : ⊤ ≠ 0
hbdd : ∀ (n : ℕ), eLpNormEssSup (f n) μ ≤ ↑R
this : ∀ᵐ (a : α) ∂μ, ∀ (i : ℕ), ‖f i a‖ₑ < ↑R + 1
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Proof state:
case h
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
x : α
hx : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤
⊢ liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Tactic:
have hppos : 0 < p.toReal := ENNReal.toReal_pos hp hp'

Result:
case h
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
x : α
hx : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤
hppos : 0 < p.toReal
⊢ liminf (fun n => ‖f n x‖ₑ) atTop < ⊤

Proof state:
case h
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
hp : p ≠ 0
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp' : ¬p = ⊤
x : α
hx : liminf (fun n => ‖f n x‖ₑ) atTop ^ p.toReal < ⊤
hppos : 0 < p.toReal
this : liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop = liminf (fun n => ‖f n x‖ₑ) atTop ^ p.toReal
⊢ (liminf (fun x_1 => ‖f x_1 x‖ₑ) atTop ^ p.toReal) ^ p.toReal⁻¹ < ⊤

Tactic:
exact ENNReal.rpow_lt_top_of_nonneg (inv_nonneg.2 hppos.le) hx.ne

Result:
no goals