case intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
⊢ ‖f‖ ≤ C
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
⊢ ‖f‖ ≤ C
obtain ⟨i, hi⟩ := hCF.exists
case intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
⊢ ‖f‖ ≤ C
case intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
⊢ ‖f‖ ≤ C
have hC : 0 ≤ C := (norm_nonneg _).trans hi
case intro.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (1 ≤ ⊤)
F : ι → { x // x ∈ lp E ⊤ }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E ⊤ }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
hi : ‖F i‖ ≤ C
⊢ ‖f‖ ≤ C

case intro.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
⊢ ‖f‖ ≤ C
case intro
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
⊢ ‖f‖ ≤ C
rcases eq_top_or_lt_top p with (rfl | hp)
case intro.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (1 ≤ ⊤)
F : ι → { x // x ∈ lp E ⊤ }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E ⊤ }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
hi : ‖F i‖ ≤ C
⊢ ∀ (i : α), ‖↑f i‖ ≤ C
case intro.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (1 ≤ ⊤)
F : ι → { x // x ∈ lp E ⊤ }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E ⊤ }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
hi : ‖F i‖ ≤ C
⊢ ‖f‖ ≤ C
apply norm_le_of_forall_le hC
no goals
case intro.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
C : ℝ
i : ι
hC : 0 ≤ C
_i : Fact (1 ≤ ⊤)
F : ι → { x // x ∈ lp E ⊤ }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E ⊤ }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
hi : ‖F i‖ ≤ C
⊢ ∀ (i : α), ‖↑f i‖ ≤ C
exact norm_apply_le_of_tendsto hCF hf
case intro.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
this : 0 < p
⊢ ‖f‖ ≤ C
case intro.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
⊢ ‖f‖ ≤ C
have : 0 < p := zero_lt_one.trans_le _i.elim
case intro.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
this : 0 < p
hp' : 0 < ENNReal.toReal p
⊢ ‖f‖ ≤ C
case intro.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
this : 0 < p
⊢ ‖f‖ ≤ C
have hp' : 0 < p.toReal := ENNReal.toReal_pos this.ne' hp.ne
case intro.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
this : 0 < p
hp' : 0 < ENNReal.toReal p
⊢ ∀ (s : Finset α), ∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p ≤ C ^ ENNReal.toReal p
case intro.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
this : 0 < p
hp' : 0 < ENNReal.toReal p
⊢ ‖f‖ ≤ C
apply norm_le_of_forall_sum_le hp' hC
no goals
case intro.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
_i : Fact (1 ≤ p)
C : ℝ
F : ι → { x // x ∈ lp E p }
hCF : ∀ᶠ (k : ι) in l, ‖F k‖ ≤ C
f : { x // x ∈ lp E p }
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 ↑f)
i : ι
hi : ‖F i‖ ≤ C
hC : 0 ≤ C
hp : p < ⊤
this : 0 < p
hp' : 0 < ENNReal.toReal p
⊢ ∀ (s : Finset α), ∑ i in s, ‖↑f i‖ ^ ENNReal.toReal p ≤ C ^ ENNReal.toReal p
exact sum_rpow_le_of_tendsto hp.ne hCF hf