case pos
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p = 0
⊢ snorm f_lim p μ ≤ liminf (fun n => snorm (f n) p μ) atTop

case neg
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : ¬p = 0
⊢ snorm f_lim p μ ≤ liminf (fun n => snorm (f n) p μ) atTop
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
⊢ snorm f_lim p μ ≤ liminf (fun n => snorm (f n) p μ) atTop
by_cases hp0 : p = 0
case neg
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
⊢ snorm f_lim p μ ≤ liminf (fun n => snorm (f n) p μ) atTop
case neg
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : ¬p = 0
⊢ snorm f_lim p μ ≤ liminf (fun n => snorm (f n) p μ) atTop
rw [← Ne.def] at hp0
case pos
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : p = ⊤
⊢ snorm f_lim p μ ≤ liminf (fun n => snorm (f n) p μ) atTop

case neg
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : ¬p = ⊤
⊢ snorm f_lim p μ ≤ liminf (fun n => snorm (f n) p μ) atTop
case neg
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
⊢ snorm f_lim p μ ≤ liminf (fun n => snorm (f n) p μ) atTop
by_cases hp_top : p = ∞
case neg
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : ¬p = ⊤
⊢ snorm' f_lim (ENNReal.toReal p) μ ≤ liminf (fun n => snorm' (f n) (ENNReal.toReal p) μ) atTop
case neg
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : ¬p = ⊤
⊢ snorm f_lim p μ ≤ liminf (fun n => snorm (f n) p μ) atTop
simp_rw [snorm_eq_snorm' hp0 hp_top]
case neg
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ snorm' f_lim (ENNReal.toReal p) μ ≤ liminf (fun n => snorm' (f n) (ENNReal.toReal p) μ) atTop
case neg
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : ¬p = ⊤
⊢ snorm' f_lim (ENNReal.toReal p) μ ≤ liminf (fun n => snorm' (f n) (ENNReal.toReal p) μ) atTop
have hp_pos : 0 < p.toReal := ENNReal.toReal_pos hp0 hp_top
no goals
case neg
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : ¬p = ⊤
hp_pos : 0 < ENNReal.toReal p
⊢ snorm' f_lim (ENNReal.toReal p) μ ≤ liminf (fun n => snorm' (f n) (ENNReal.toReal p) μ) atTop
exact snorm'_lim_le_liminf_snorm' hp_pos hf h_lim
no goals
case pos
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p = 0
⊢ snorm f_lim p μ ≤ liminf (fun n => snorm (f n) p μ) atTop
simp [hp0]
case pos
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : p = ⊤
⊢ snorm f_lim ⊤ μ ≤ liminf (fun n => snorm (f n) ⊤ μ) atTop
case pos
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : p = ⊤
⊢ snorm f_lim p μ ≤ liminf (fun n => snorm (f n) p μ) atTop
simp_rw [hp_top]
no goals
case pos
α : Type u_2
E✝ : Type ?u.8118264
F : Type ?u.8118267
G : Type ?u.8118270
m m0 : MeasurableSpace α
p : ℝ≥0∞
q : ℝ
μ ν : Measure α
inst✝³ : NormedAddCommGroup E✝
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedAddCommGroup G
E : Type u_1
inst✝ : NormedAddCommGroup E
f : ℕ → α → E
hf : ∀ (n : ℕ), AEStronglyMeasurable (f n) μ
f_lim : α → E
h_lim : ∀ᵐ (x : α) ∂μ, Tendsto (fun n => f n x) atTop (𝓝 (f_lim x))
hp0 : p ≠ 0
hp_top : p = ⊤
⊢ snorm f_lim ⊤ μ ≤ liminf (fun n => snorm (f n) ⊤ μ) atTop
exact snorm_exponent_top_lim_le_liminf_snorm_exponent_top h_lim