case intro.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)
F : ι → { x // x ∈ lp E p }
hF : Metric.Bounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
left✝ : C > 0
hCF' : ∀ (x : { x // x ∈ lp E p }), x ∈ Set.range F → ‖x‖ ≤ C
⊢ Memℓp f p
α : 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)
F : ι → { x // x ∈ lp E p }
hF : Metric.Bounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
⊢ Memℓp f p
obtain ⟨C, _, hCF'⟩ := hF.exists_pos_norm_le
case intro.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)
F : ι → { x // x ∈ lp E p }
hF : Metric.Bounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
left✝ : C > 0
hCF' : ∀ (x : { x // x ∈ lp E p }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ Memℓp f p
case intro.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)
F : ι → { x // x ∈ lp E p }
hF : Metric.Bounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
left✝ : C > 0
hCF' : ∀ (x : { x // x ∈ lp E p }), x ∈ Set.range F → ‖x‖ ≤ C
⊢ Memℓp f p
have hCF : ∀ k, ‖F k‖ ≤ C := fun k => hCF' _ ⟨k, rfl⟩
case intro.intro.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
f : (a : α) → E a
C : ℝ
left✝ : C > 0
_i : Fact (1 ≤ ⊤)
F : ι → { x // x ∈ lp E ⊤ }
hF : Metric.Bounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF' : ∀ (x : { x // x ∈ lp E ⊤ }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ Memℓp f ⊤

case intro.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)
F : ι → { x // x ∈ lp E p }
hF : Metric.Bounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
left✝ : C > 0
hCF' : ∀ (x : { x // x ∈ lp E p }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ⊤
⊢ Memℓp f p
case intro.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)
F : ι → { x // x ∈ lp E p }
hF : Metric.Bounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
left✝ : C > 0
hCF' : ∀ (x : { x // x ∈ lp E p }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ Memℓp f p
rcases eq_top_or_lt_top p with (rfl | hp)
case intro.intro.inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
f : (a : α) → E a
C : ℝ
left✝ : C > 0
_i : Fact (1 ≤ ⊤)
F : ι → { x // x ∈ lp E ⊤ }
hF : Metric.Bounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF' : ∀ (x : { x // x ∈ lp E ⊤ }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ BddAbove (Set.range fun i => ‖f i‖)
case intro.intro.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
f : (a : α) → E a
C : ℝ
left✝ : C > 0
_i : Fact (1 ≤ ⊤)
F : ι → { x // x ∈ lp E ⊤ }
hF : Metric.Bounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF' : ∀ (x : { x // x ∈ lp E ⊤ }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ Memℓp f ⊤
apply memℓp_infty
case intro.intro.inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
f : (a : α) → E a
C : ℝ
left✝ : C > 0
_i : Fact (1 ≤ ⊤)
F : ι → { x // x ∈ lp E ⊤ }
hF : Metric.Bounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF' : ∀ (x : { x // x ∈ lp E ⊤ }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ C ∈ upperBounds (Set.range fun i => ‖f i‖)
case intro.intro.inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
f : (a : α) → E a
C : ℝ
left✝ : C > 0
_i : Fact (1 ≤ ⊤)
F : ι → { x // x ∈ lp E ⊤ }
hF : Metric.Bounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF' : ∀ (x : { x // x ∈ lp E ⊤ }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ BddAbove (Set.range fun i => ‖f i‖)
use C
case intro.intro.inl.hf.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
f : (a : α) → E a
C : ℝ
left✝ : C > 0
_i : Fact (1 ≤ ⊤)
F : ι → { x // x ∈ lp E ⊤ }
hF : Metric.Bounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF' : ∀ (x : { x // x ∈ lp E ⊤ }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
a : α
⊢ (fun i => ‖f i‖) a ≤ C
case intro.intro.inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
f : (a : α) → E a
C : ℝ
left✝ : C > 0
_i : Fact (1 ≤ ⊤)
F : ι → { x // x ∈ lp E ⊤ }
hF : Metric.Bounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF' : ∀ (x : { x // x ∈ lp E ⊤ }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
⊢ C ∈ upperBounds (Set.range fun i => ‖f i‖)
rintro _ ⟨a, rfl⟩
no goals
case intro.intro.inl.hf.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
ι : Type u_3
l : Filter ι
inst✝ : NeBot l
f : (a : α) → E a
C : ℝ
left✝ : C > 0
_i : Fact (1 ≤ ⊤)
F : ι → { x // x ∈ lp E ⊤ }
hF : Metric.Bounded (Set.range F)
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
hCF' : ∀ (x : { x // x ∈ lp E ⊤ }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
a : α
⊢ (fun i => ‖f i‖) a ≤ C
refine' norm_apply_le_of_tendsto (eventually_of_forall hCF) hf a
case intro.intro.inr.hf
α : 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)
F : ι → { x // x ∈ lp E p }
hF : Metric.Bounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
left✝ : C > 0
hCF' : ∀ (x : { x // x ∈ lp E p }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ⊤
⊢ ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ ?intro.intro.inr.C

case intro.intro.inr.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)
F : ι → { x // x ∈ lp E p }
hF : Metric.Bounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
left✝ : C > 0
hCF' : ∀ (x : { x // x ∈ lp E p }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ⊤
⊢ ℝ
case intro.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)
F : ι → { x // x ∈ lp E p }
hF : Metric.Bounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
left✝ : C > 0
hCF' : ∀ (x : { x // x ∈ lp E p }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ⊤
⊢ Memℓp f p
apply memℓp_gen'
no goals
case intro.intro.inr.hf
α : 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)
F : ι → { x // x ∈ lp E p }
hF : Metric.Bounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
left✝ : C > 0
hCF' : ∀ (x : { x // x ∈ lp E p }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ⊤
⊢ ∀ (s : Finset α), ∑ i in s, ‖f i‖ ^ ENNReal.toReal p ≤ ?intro.intro.inr.C

case intro.intro.inr.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)
F : ι → { x // x ∈ lp E p }
hF : Metric.Bounded (Set.range F)
f : (a : α) → E a
hf : Tendsto (id fun i => ↑(F i)) l (𝓝 f)
C : ℝ
left✝ : C > 0
hCF' : ∀ (x : { x // x ∈ lp E p }), x ∈ Set.range F → ‖x‖ ≤ C
hCF : ∀ (k : ι), ‖F k‖ ≤ C
hp : p < ⊤
⊢ ℝ
exact sum_rpow_le_of_tendsto hp.ne (eventually_of_forall hCF) hf