-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem ae_bdd_liminf_atTop_rpow_of_eLpNorm_bdd {p : ℝ≥0∞} {f : ℕ → α → E}
    (hfmeas : ∀ n, Measurable (f n)) (hbdd : ∀ n, eLpNorm (f n) p μ ≤ R) :
    ∀ᵐ x ∂μ, liminf (fun n => ((‖f n x‖ₑ) ^ p.toReal : ℝ≥0∞)) 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
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤

Tactic:
simp only [hp0, ENNReal.rpow_zero]

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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => 1) 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
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => 1) atTop < ⊤

Tactic:
filter_upwards with _

Result:
case pos.h
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝² : NormedAddCommGroup E
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
a✝ : α
⊢ liminf (fun n => 1) 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
hp : p ≠ 0
h : p = ⊤
⊢ False

Tactic:
simp [h] at hp0

Result:
no goals

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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤

Tactic:
by_cases hp0 : p.toReal = 0

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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ ^ p.toReal) 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤

Proof state:
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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, 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 ?_
          (ENNReal.rpow_lt_top_of_nonneg ENNReal.toReal_nonneg ENNReal.coe_ne_top :
            (R : ℝ≥0∞) ^ p.toReal < ∞))).ne

Result:
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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ⊤
⊢ liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ p.toReal ∂μ) atTop ≤ ↑R ^ p.toReal

Proof state:
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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
hp : p ≠ 0
hp' : p ≠ ⊤
⊢ liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ p.toReal ∂μ) atTop ≤ ↑R ^ p.toReal

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

Result:
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∞
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
⊢ liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ p.toReal ∂μ) atTop ≤ ↑R ^ p.toReal

Proof state:
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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ ^ p.toReal) atTop < ⊤

Tactic:
have hp : p ≠ 0 := fun h => by simp [h] at hp0

Result:
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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
hp : p ≠ 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ‖f n x‖ₑ ^ p.toReal) 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∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), eLpNorm (f n) p μ ≤ ↑R
hp0 : ¬p.toReal = 0
h : p = 0
⊢ False

Tactic:
simp [h] at hp0

Result:
no goals

Proof state:
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∞
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
⊢ sSup {a | ∃ a_1, ∀ b ≥ a_1, a ≤ ∫⁻ (a : α), ↑‖f b a‖₊ ^ p.toReal ∂μ} ≤ ↑R ^ 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 _))

Result:
no goals

Proof state:
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∞
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
⊢ liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ p.toReal ∂μ) atTop ≤ ↑R ^ p.toReal

Tactic:
simp_rw [liminf_eq, eventually_atTop]

Result:
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∞
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
⊢ sSup {a | ∃ a_1, ∀ b ≥ a_1, a ≤ ∫⁻ (a : α), ↑‖f b a‖₊ ^ p.toReal ∂μ} ≤ ↑R ^ p.toReal