α : Type ?u.560431
E : α → Type ?u.560436
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
B : I → Type u_2
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
⊢ BddAbove (Set.range fun i => ‖(f * g) i‖)
α : Type ?u.560431
E : α → Type ?u.560436
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
B : I → Type u_2
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
⊢ Memℓp (f * g) ⊤
rw [memℓp_infty_iff]
case intro.intro
α : Type ?u.560431
E : α → Type ?u.560436
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
B : I → Type u_2
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ BddAbove (Set.range fun i => ‖(f * g) i‖)
α : Type ?u.560431
E : α → Type ?u.560436
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
B : I → Type u_2
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
⊢ BddAbove (Set.range fun i => ‖(f * g) i‖)
obtain ⟨⟨Cf, hCf⟩, ⟨Cg, hCg⟩⟩ := hf.bddAbove, hg.bddAbove
case intro.intro
α : Type ?u.560431
E : α → Type ?u.560436
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
B : I → Type u_2
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ Cf * Cg ∈ upperBounds (Set.range fun i => ‖(f * g) i‖)
case intro.intro
α : Type ?u.560431
E : α → Type ?u.560436
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
B : I → Type u_2
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ BddAbove (Set.range fun i => ‖(f * g) i‖)
refine' ⟨Cf * Cg, _⟩
case intro.intro.intro
α : Type ?u.560431
E : α → Type ?u.560436
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
B : I → Type u_2
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)
i : I
⊢ (fun i => ‖(f * g) i‖) i ≤ Cf * Cg
case intro.intro
α : Type ?u.560431
E : α → Type ?u.560436
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
B : I → Type u_2
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ Cf * Cg ∈ upperBounds (Set.range fun i => ‖(f * g) i‖)
rintro _ ⟨i, rfl⟩
no goals
case intro.intro.intro
α : Type ?u.560431
E : α → Type ?u.560436
p q : ℝ≥0∞
inst✝¹ : (i : α) → NormedAddCommGroup (E i)
I : Type u_1
B : I → Type u_2
inst✝ : (i : I) → NonUnitalNormedRing (B i)
f g : (i : I) → B i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
Cf : ℝ
hCf : Cf ∈ upperBounds (Set.range fun i => ‖f i‖)
Cg : ℝ
hCg : Cg ∈ upperBounds (Set.range fun i => ‖g i‖)
i : I
⊢ (fun i => ‖(f * g) i‖) i ≤ Cf * Cg
calc
  ‖(f * g) i‖ ≤ ‖f i‖ * ‖g i‖ := norm_mul_le (f i) (g i)
  _ ≤ Cf * Cg :=
    mul_le_mul (hCf ⟨i, rfl⟩) (hCg ⟨i, rfl⟩) (norm_nonneg _)
      ((norm_nonneg _).trans (hCf ⟨i, rfl⟩))