case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : 0 ≠ 0
f : { x // x ∈ lp E 0 }
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

case inr.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
rcases p.trichotomy with (rfl | rfl | hp)
no goals
case inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : 0 ≠ 0
f : { x // x ∈ lp E 0 }
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
exact absurd rfl hp
case inr.inl.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : IsEmpty α
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖

case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
case inr.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
cases isEmpty_or_nonempty α
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have hcf := lp.isLUB_norm (c • f)
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB ((fun b => ‖c‖ * b) '' Set.range fun i => ‖↑f i‖) (‖c‖ * ‖f‖)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have hfc := (lp.isLUB_norm f).mul_left (norm_nonneg c)
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB (Set.range fun x => ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB ((fun b => ‖c‖ * b) '' Set.range fun i => ‖↑f i‖) (‖c‖ * ‖f‖)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
simp_rw [← Set.range_comp, Function.comp] at hfc
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB (Set.range fun x => ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
⊢ ‖c‖ * ‖f‖ ∈ upperBounds (Set.range fun i => ‖↑(c • f) i‖)
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB (Set.range fun x => ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
refine' hcf.right _
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB (Set.range fun x => ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
this : ‖c‖ * ‖f‖ ∈ upperBounds (Set.range fun x => ‖c‖ * ‖↑f x‖)
⊢ ‖c‖ * ‖f‖ ∈ upperBounds (Set.range fun i => ‖↑(c • f) i‖)
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB (Set.range fun x => ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
⊢ ‖c‖ * ‖f‖ ∈ upperBounds (Set.range fun i => ‖↑(c • f) i‖)
have := hfc.left
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB (Set.range fun x => ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
this : ∀ (a : α), ‖c‖ * ‖↑f a‖ ≤ ‖c‖ * ‖f‖
⊢ ∀ (a : α), ‖↑(c • f) a‖ ≤ ‖c‖ * ‖f‖
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB (Set.range fun x => ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
this : ‖c‖ * ‖f‖ ∈ upperBounds (Set.range fun x => ‖c‖ * ‖↑f x‖)
⊢ ‖c‖ * ‖f‖ ∈ upperBounds (Set.range fun i => ‖↑(c • f) i‖)
simp_rw [mem_upperBounds, Set.mem_range, forall_exists_index, forall_apply_eq_imp_iff'] at this⊢
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB (Set.range fun x => ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
this : ∀ (a : α), ‖c‖ * ‖↑f a‖ ≤ ‖c‖ * ‖f‖
a : α
⊢ ‖↑(c • f) a‖ ≤ ‖c‖ * ‖f‖
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB (Set.range fun x => ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
this : ∀ (a : α), ‖c‖ * ‖↑f a‖ ≤ ‖c‖ * ‖f‖
⊢ ∀ (a : α), ‖↑(c • f) a‖ ≤ ‖c‖ * ‖f‖
intro a
no goals
case inr.inl.inr
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : Nonempty α
hcf : IsLUB (Set.range fun i => ‖↑(c • f) i‖) ‖c • f‖
hfc : IsLUB (Set.range fun x => ‖c‖ * ‖↑f x‖) (‖c‖ * ‖f‖)
this : ∀ (a : α), ‖c‖ * ‖↑f a‖ ≤ ‖c‖ * ‖f‖
a : α
⊢ ‖↑(c • f) a‖ ≤ ‖c‖ * ‖f‖
exact (norm_smul_le _ _).trans (this a)
no goals
case inr.inl.inl
α : Type u_1
E : α → Type u_2
q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
c : 𝕜
hp : ⊤ ≠ 0
f : { x // x ∈ lp E ⊤ }
h✝ : IsEmpty α
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
simp [lp.eq_zero' f]
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p } := { nnnorm := fun f => { val := ‖f‖, property := (_ : 0 ≤ ‖f‖) } }
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
letI inst : NNNorm (lp E p) := ⟨fun f => ⟨‖f‖, norm_nonneg' _⟩⟩
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p } := { nnnorm := fun f => { val := ‖f‖, property := (_ : 0 ≤ ‖f‖) } }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p } := { nnnorm := fun f => { val := ‖f‖, property := (_ : 0 ≤ ‖f‖) } }
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
have coe_nnnorm : ∀ f : lp E p, ↑‖f‖₊ = ‖f‖ := fun _ => rfl
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p } := { nnnorm := fun f => { val := ‖f‖, property := (_ : 0 ≤ ‖f‖) } }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖₊ ^ ENNReal.toReal p ≤ (‖c‖₊ * ‖f‖₊) ^ ENNReal.toReal p
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p } := { nnnorm := fun f => { val := ‖f‖, property := (_ : 0 ≤ ‖f‖) } }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
suffices ‖c • f‖₊ ^ p.toReal ≤ (‖c‖₊ * ‖f‖₊) ^ p.toReal by
  rwa [NNReal.rpow_le_rpow_iff hp] at this
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖₊ ^ ENNReal.toReal p ≤ (‖c‖₊ * ‖f‖₊) ^ ENNReal.toReal p
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p } := { nnnorm := fun f => { val := ‖f‖, property := (_ : 0 ≤ ‖f‖) } }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖₊ ^ ENNReal.toReal p ≤ (‖c‖₊ * ‖f‖₊) ^ ENNReal.toReal p
clear_value inst
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖₊ ^ ENNReal.toReal p ≤ ‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖₊ ^ ENNReal.toReal p ≤ (‖c‖₊ * ‖f‖₊) ^ ENNReal.toReal p
rw [NNReal.mul_rpow]
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hLHS : HasSum (fun i => ‖↑(c • f) i‖ ^ ENNReal.toReal p) (‖c • f‖ ^ ENNReal.toReal p)
⊢ ‖c • f‖₊ ^ ENNReal.toReal p ≤ ‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
⊢ ‖c • f‖₊ ^ ENNReal.toReal p ≤ ‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p
have hLHS := lp.hasSum_norm hp (c • f)
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hLHS : HasSum (fun i => ‖↑(c • f) i‖ ^ ENNReal.toReal p) (‖c • f‖ ^ ENNReal.toReal p)
hRHS :
  HasSum (fun i => ‖c‖ ^ ENNReal.toReal p * ‖↑f i‖ ^ ENNReal.toReal p) (‖c‖ ^ ENNReal.toReal p * ‖f‖ ^ ENNReal.toReal p)
⊢ ‖c • f‖₊ ^ ENNReal.toReal p ≤ ‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hLHS : HasSum (fun i => ‖↑(c • f) i‖ ^ ENNReal.toReal p) (‖c • f‖ ^ ENNReal.toReal p)
⊢ ‖c • f‖₊ ^ ENNReal.toReal p ≤ ‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p
have hRHS := (lp.hasSum_norm hp f).mul_left (‖c‖ ^ p.toReal)
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hRHS :
  HasSum (fun a => ‖c‖₊ ^ ENNReal.toReal p * ‖↑f a‖₊ ^ ENNReal.toReal p)
    (‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p)
hLHS : HasSum (fun a => ‖↑(c • f) a‖₊ ^ ENNReal.toReal p) (‖c • f‖₊ ^ ENNReal.toReal p)
⊢ ‖c • f‖₊ ^ ENNReal.toReal p ≤ ‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hLHS : HasSum (fun i => ‖↑(c • f) i‖ ^ ENNReal.toReal p) (‖c • f‖ ^ ENNReal.toReal p)
hRHS :
  HasSum (fun i => ‖c‖ ^ ENNReal.toReal p * ‖↑f i‖ ^ ENNReal.toReal p) (‖c‖ ^ ENNReal.toReal p * ‖f‖ ^ ENNReal.toReal p)
⊢ ‖c • f‖₊ ^ ENNReal.toReal p ≤ ‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p
simp_rw [← coe_nnnorm, ← _root_.coe_nnnorm, ← NNReal.coe_rpow, ← NNReal.coe_mul,
  NNReal.hasSum_coe] at hRHS hLHS
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hRHS :
  HasSum (fun a => ‖c‖₊ ^ ENNReal.toReal p * ‖↑f a‖₊ ^ ENNReal.toReal p)
    (‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p)
hLHS : HasSum (fun a => ‖↑(c • f) a‖₊ ^ ENNReal.toReal p) (‖c • f‖₊ ^ ENNReal.toReal p)
i : α
⊢ ‖↑(c • f) i‖₊ ^ ENNReal.toReal p ≤ ‖c‖₊ ^ ENNReal.toReal p * ‖↑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
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hRHS :
  HasSum (fun a => ‖c‖₊ ^ ENNReal.toReal p * ‖↑f a‖₊ ^ ENNReal.toReal p)
    (‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p)
hLHS : HasSum (fun a => ‖↑(c • f) a‖₊ ^ ENNReal.toReal p) (‖c • f‖₊ ^ ENNReal.toReal p)
⊢ ‖c • f‖₊ ^ ENNReal.toReal p ≤ ‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p
refine' hasSum_mono hLHS hRHS fun i => _
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hRHS :
  HasSum (fun a => ‖c‖₊ ^ ENNReal.toReal p * ‖↑f a‖₊ ^ ENNReal.toReal p)
    (‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p)
hLHS : HasSum (fun a => ‖↑(c • f) a‖₊ ^ ENNReal.toReal p) (‖c • f‖₊ ^ ENNReal.toReal p)
i : α
⊢ ‖↑(c • f) i‖₊ ^ ENNReal.toReal p ≤ ‖c‖₊ ^ ENNReal.toReal p * ‖↑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
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hRHS :
  HasSum (fun a => ‖c‖₊ ^ ENNReal.toReal p * ‖↑f a‖₊ ^ ENNReal.toReal p)
    (‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p)
hLHS : HasSum (fun a => ‖↑(c • f) a‖₊ ^ ENNReal.toReal p) (‖c • f‖₊ ^ ENNReal.toReal p)
i : α
⊢ ‖↑(c • f) i‖₊ ^ ENNReal.toReal p ≤ ‖c‖₊ ^ ENNReal.toReal p * ‖↑f i‖₊ ^ ENNReal.toReal p
dsimp only
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hRHS :
  HasSum (fun a => ‖c‖₊ ^ ENNReal.toReal p * ‖↑f a‖₊ ^ ENNReal.toReal p)
    (‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p)
hLHS : HasSum (fun a => ‖↑(c • f) a‖₊ ^ ENNReal.toReal p) (‖c • f‖₊ ^ ENNReal.toReal p)
i : α
⊢ ‖↑(c • f) i‖₊ ^ ENNReal.toReal p ≤ (‖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
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hRHS :
  HasSum (fun a => ‖c‖₊ ^ ENNReal.toReal p * ‖↑f a‖₊ ^ ENNReal.toReal p)
    (‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p)
hLHS : HasSum (fun a => ‖↑(c • f) a‖₊ ^ ENNReal.toReal p) (‖c • f‖₊ ^ ENNReal.toReal p)
i : α
⊢ ‖↑(c • f) i‖₊ ^ ENNReal.toReal p ≤ ‖c‖₊ ^ ENNReal.toReal p * ‖↑f i‖₊ ^ ENNReal.toReal p
rw [← NNReal.mul_rpow]
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hRHS :
  HasSum (fun a => ‖c‖₊ ^ ENNReal.toReal p * ‖↑f a‖₊ ^ ENNReal.toReal p)
    (‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p)
hLHS : HasSum (fun a => ‖↑(c • f) a‖₊ ^ ENNReal.toReal p) (‖c • f‖₊ ^ ENNReal.toReal p)
i : α
⊢ ‖c • ↑f i‖₊ ^ ENNReal.toReal p ≤ (‖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
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hRHS :
  HasSum (fun a => ‖c‖₊ ^ ENNReal.toReal p * ‖↑f a‖₊ ^ ENNReal.toReal p)
    (‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p)
hLHS : HasSum (fun a => ‖↑(c • f) a‖₊ ^ ENNReal.toReal p) (‖c • f‖₊ ^ ENNReal.toReal p)
i : α
⊢ ‖↑(c • f) i‖₊ ^ ENNReal.toReal p ≤ (‖c‖₊ * ‖↑f i‖₊) ^ ENNReal.toReal p
rw [lp.coeFn_smul, Pi.smul_apply]
no goals
case inr.inr
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
hRHS :
  HasSum (fun a => ‖c‖₊ ^ ENNReal.toReal p * ‖↑f a‖₊ ^ ENNReal.toReal p)
    (‖c‖₊ ^ ENNReal.toReal p * ‖f‖₊ ^ ENNReal.toReal p)
hLHS : HasSum (fun a => ‖↑(c • f) a‖₊ ^ ENNReal.toReal p) (‖c • f‖₊ ^ 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
no goals
α : Type u_1
E : α → Type u_2
p q : ℝ≥0∞
inst✝⁶ : (i : α) → NormedAddCommGroup (E i)
𝕜 : Type u_3
𝕜' : Type ?u.424487
inst✝⁵ : NormedRing 𝕜
inst✝⁴ : NormedRing 𝕜'
inst✝³ : (i : α) → Module 𝕜 (E i)
inst✝² : (i : α) → Module 𝕜' (E i)
inst✝¹ : ∀ (i : α), BoundedSMul 𝕜 (E i)
inst✝ : ∀ (i : α), BoundedSMul 𝕜' (E i)
hp✝ : p ≠ 0
c : 𝕜
f : { x // x ∈ lp E p }
hp : 0 < ENNReal.toReal p
inst : NNNorm { x // x ∈ lp E p } := { nnnorm := fun f => { val := ‖f‖, property := (_ : 0 ≤ ‖f‖) } }
coe_nnnorm : ∀ (f : { x // x ∈ lp E p }), ↑‖f‖₊ = ‖f‖
this : ‖c • f‖₊ ^ ENNReal.toReal p ≤ (‖c‖₊ * ‖f‖₊) ^ ENNReal.toReal p
⊢ ‖c • f‖ ≤ ‖c‖ * ‖f‖
rwa [NNReal.rpow_le_rpow_iff hp] at this