case pos
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ENNReal.toReal p = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ↑‖f n x‖₊ ^ ENNReal.toReal p) atTop < ⊤

case neg
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ¬ENNReal.toReal p = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ↑‖f n x‖₊ ^ ENNReal.toReal p) atTop < ⊤
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ↑‖f n x‖₊ ^ ENNReal.toReal p) atTop < ⊤
by_cases hp0 : p.toReal = 0
case neg
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ¬ENNReal.toReal p = 0
hp : p ≠ 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ↑‖f n x‖₊ ^ ENNReal.toReal p) atTop < ⊤
case neg
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ¬ENNReal.toReal p = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ↑‖f n x‖₊ ^ ENNReal.toReal p) atTop < ⊤
have hp : p ≠ 0 := fun h => by simp [h] at hp0
case neg
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ¬ENNReal.toReal p = 0
hp : p ≠ 0
hp' : p ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ↑‖f n x‖₊ ^ ENNReal.toReal p) atTop < ⊤
case neg
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ¬ENNReal.toReal p = 0
hp : p ≠ 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ↑‖f n x‖₊ ^ ENNReal.toReal p) atTop < ⊤
have hp' : p ≠ ∞ := fun h => by simp [h] at hp0
case neg
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ¬ENNReal.toReal p = 0
hp : p ≠ 0
hp' : p ≠ ⊤
⊢ liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ ENNReal.toReal p ∂μ) atTop ≤ ↑R ^ ENNReal.toReal p
case neg
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ¬ENNReal.toReal p = 0
hp : p ≠ 0
hp' : p ≠ ⊤
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ↑‖f n x‖₊ ^ ENNReal.toReal p) atTop < ⊤
refine'
  ae_lt_top (measurable_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
case neg
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp0 : ¬ENNReal.toReal p = 0
hp : p ≠ 0
hp' : p ≠ ⊤
hbdd : ∀ (n : ℕ), (∫⁻ (x : α), ↑‖f n x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) ≤ ↑R
⊢ liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ ENNReal.toReal p ∂μ) atTop ≤ ↑R ^ ENNReal.toReal p
case neg
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ¬ENNReal.toReal p = 0
hp : p ≠ 0
hp' : p ≠ ⊤
⊢ liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ ENNReal.toReal p ∂μ) atTop ≤ ↑R ^ ENNReal.toReal p
simp_rw [snorm_eq_lintegral_rpow_nnnorm hp hp'] at hbdd
case neg
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp0 : ¬ENNReal.toReal p = 0
hp : p ≠ 0
hp' : p ≠ ⊤
hbdd : ∀ (n : ℕ), (∫⁻ (x : α), ↑‖f n x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) ≤ ↑R
⊢ sSup {a | ∃ a_1, ∀ (b : ℕ), b ≥ a_1 → a ≤ ∫⁻ (a : α), ↑‖f b a‖₊ ^ ENNReal.toReal p ∂μ} ≤ ↑R ^ ENNReal.toReal p
case neg
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp0 : ¬ENNReal.toReal p = 0
hp : p ≠ 0
hp' : p ≠ ⊤
hbdd : ∀ (n : ℕ), (∫⁻ (x : α), ↑‖f n x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) ≤ ↑R
⊢ liminf (fun n => ∫⁻ (a : α), ↑‖f n a‖₊ ^ ENNReal.toReal p ∂μ) atTop ≤ ↑R ^ ENNReal.toReal p
simp_rw [liminf_eq, eventually_atTop]
no goals
case neg
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hp0 : ¬ENNReal.toReal p = 0
hp : p ≠ 0
hp' : p ≠ ⊤
hbdd : ∀ (n : ℕ), (∫⁻ (x : α), ↑‖f n x‖₊ ^ ENNReal.toReal p ∂μ) ^ (1 / ENNReal.toReal p) ≤ ↑R
⊢ sSup {a | ∃ a_1, ∀ (b : ℕ), b ≥ a_1 → a ≤ ∫⁻ (a : α), ↑‖f b a‖₊ ^ ENNReal.toReal p ∂μ} ≤ ↑R ^ ENNReal.toReal p
exact
  sSup_le fun b ⟨a, ha⟩ =>
    (ha a le_rfl).trans ((ENNReal.rpow_one_div_le_iff (ENNReal.toReal_pos hp hp')).1 (hbdd _))
case pos
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ENNReal.toReal p = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => 1) atTop < ⊤
case pos
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ENNReal.toReal p = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => ↑‖f n x‖₊ ^ ENNReal.toReal p) atTop < ⊤
simp only [hp0, ENNReal.rpow_zero]
case pos
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ENNReal.toReal p = 0
x : α
⊢ liminf (fun n => 1) atTop < ⊤
case pos
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ENNReal.toReal p = 0
⊢ ∀ᵐ (x : α) ∂μ, liminf (fun n => 1) atTop < ⊤
refine' eventually_of_forall fun x => _
case pos
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ENNReal.toReal p = 0
x : α
⊢ 1 < ⊤
case pos
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ENNReal.toReal p = 0
x : α
⊢ liminf (fun n => 1) atTop < ⊤
rw [liminf_const (1 : ℝ≥0∞)]
no goals
case pos
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ENNReal.toReal p = 0
x : α
⊢ 1 < ⊤
exact ENNReal.one_lt_top
no goals
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ¬ENNReal.toReal p = 0
h : p = 0
⊢ False
simp [h] at hp0
no goals
α : Type u_1
E : Type u_2
F : Type ?u.6222998
G : Type ?u.6223001
m m0 : MeasurableSpace α
p✝ : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedAddCommGroup G
inst✝¹ : MeasurableSpace E
inst✝ : OpensMeasurableSpace E
R : ℝ≥0
p : ℝ≥0∞
f : ℕ → α → E
hfmeas : ∀ (n : ℕ), Measurable (f n)
hbdd : ∀ (n : ℕ), snorm (f n) p μ ≤ ↑R
hp0 : ¬ENNReal.toReal p = 0
hp : p ≠ 0
h : p = ⊤
⊢ False
simp [h] at hp0