case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f 0
⊢ Memℓp (c • f) 0

case inr.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ⊤
⊢ Memℓp (c • f) ⊤

case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < ENNReal.toReal p
⊢ Memℓp (c • f) p
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
⊢ Memℓp (c • f) p
rcases p.trichotomy with (rfl | rfl | hp)
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f 0
⊢ Set.Finite {i | (c • f) i ≠ 0}
case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f 0
⊢ Memℓp (c • f) 0
apply memℓp_zero
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f 0
i : α
⊢ ¬c • f i = 0 → ¬f i = 0
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f 0
⊢ Set.Finite {i | (c • f) i ≠ 0}
refine' hf.finite_dsupport.subset fun i => (_ : ¬c • f i = 0 → ¬f i = 0)
no goals
case inl.hf
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f 0
i : α
⊢ ¬c • f i = 0 → ¬f i = 0
exact not_imp_not.mpr fun hf' => hf'.symm ▸ smul_zero c
case inr.inl.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
⊢ Memℓp (c • f) ⊤
case inr.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ⊤
⊢ Memℓp (c • f) ⊤
obtain ⟨A, hA⟩ := hf.bddAbove
case inr.inl.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
⊢ ‖c‖ * A ∈ upperBounds (Set.range fun i => ‖(c • f) i‖)
case inr.inl.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
⊢ Memℓp (c • f) ⊤
refine' memℓp_infty ⟨‖c‖ * A, _⟩
case inr.inl.intro.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
i : α
⊢ (fun i => ‖(c • f) i‖) i ≤ ‖c‖ * A
case inr.inl.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
⊢ ‖c‖ * A ∈ upperBounds (Set.range fun i => ‖(c • f) i‖)
rintro a ⟨i, rfl⟩
case inr.inl.intro.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
i : α
⊢ ‖c‖ * ‖f i‖ ≤ ‖c‖ * A
case inr.inl.intro.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
i : α
⊢ (fun i => ‖(c • f) i‖) i ≤ ‖c‖ * A
refine' (norm_smul_le _ _).trans _
no goals
case inr.inl.intro.intro
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
c : 𝕜
hf : Memℓp f ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
i : α
⊢ ‖c‖ * ‖f i‖ ≤ ‖c‖ * A
exact mul_le_mul_of_nonneg_left (hA ⟨i, rfl⟩) (norm_nonneg c)
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < ENNReal.toReal p
⊢ Summable fun i => ‖(c • f) i‖ ^ ENNReal.toReal p
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < ENNReal.toReal p
⊢ Memℓp (c • f) p
apply memℓp_gen
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < ENNReal.toReal p
this : Summable fun i => ↑(‖c‖₊ ^ ENNReal.toReal p) * ‖f i‖ ^ ENNReal.toReal p
⊢ Summable fun i => ‖(c • f) i‖ ^ ENNReal.toReal p
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < ENNReal.toReal p
⊢ Summable fun i => ‖(c • f) i‖ ^ ENNReal.toReal p
have := (hf.summable hp).mul_left (↑(‖c‖₊ ^ p.toReal) : ℝ)
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < ENNReal.toReal p
this : Summable fun a => (‖c‖₊ * ‖f a‖₊) ^ ENNReal.toReal p
⊢ Summable fun a => ‖(c • f) a‖₊ ^ ENNReal.toReal p
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < ENNReal.toReal p
this : Summable fun i => ↑(‖c‖₊ ^ ENNReal.toReal p) * ‖f i‖ ^ ENNReal.toReal p
⊢ Summable fun i => ‖(c • f) i‖ ^ ENNReal.toReal p
simp_rw [← coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul, NNReal.summable_coe,
  ← NNReal.mul_rpow] at this⊢
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < ENNReal.toReal p
this : Summable fun a => (‖c‖₊ * ‖f a‖₊) ^ ENNReal.toReal p
⊢ ∀ (b : α), ‖(c • f) b‖₊ ^ ENNReal.toReal p ≤ (‖c‖₊ * ‖f b‖₊) ^ ENNReal.toReal p
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < ENNReal.toReal p
this : Summable fun a => (‖c‖₊ * ‖f a‖₊) ^ ENNReal.toReal p
⊢ Summable fun a => ‖(c • f) a‖₊ ^ ENNReal.toReal p
refine' NNReal.summable_of_le _ this
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < ENNReal.toReal p
this : Summable fun a => (‖c‖₊ * ‖f a‖₊) ^ ENNReal.toReal p
i : α
⊢ ‖(c • f) i‖₊ ^ ENNReal.toReal p ≤ (‖c‖₊ * ‖f i‖₊) ^ ENNReal.toReal p
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < ENNReal.toReal p
this : Summable fun a => (‖c‖₊ * ‖f a‖₊) ^ ENNReal.toReal p
⊢ ∀ (b : α), ‖(c • f) b‖₊ ^ ENNReal.toReal p ≤ (‖c‖₊ * ‖f b‖₊) ^ ENNReal.toReal p
intro i
no goals
case inr.inr.hf
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝³ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
inst✝² : NormedRing 𝕜
inst✝¹ : (i : α) → Module 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜 (E i)
f : (i : α) → E i
hf : Memℓp f p
c : 𝕜
hp : 0 < ENNReal.toReal p
this : Summable fun a => (‖c‖₊ * ‖f a‖₊) ^ ENNReal.toReal p
i : α
⊢ ‖(c • f) i‖₊ ^ ENNReal.toReal p ≤ (‖c‖₊ * ‖f i‖₊) ^ ENNReal.toReal p
exact NNReal.rpow_le_rpow (nnnorm_smul_le _ _) ENNReal.toReal_nonneg