-- Mathlib/Analysis/Normed/Lp/lpSpace.lean
theorem add {f g : ∀ i, E i} (hf : Memℓp f p) (hg : Memℓp g p) : Memℓp (f + g) p

Proof state:
case inr.inl.hf.intro.intro
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
B : ℝ
hB : B ∈ upperBounds (Set.range fun i => ‖g i‖)
⊢ A + B ∈ upperBounds (Set.range fun i => ‖(f + g) i‖)

Tactic:
rintro a ⟨i, rfl⟩

Result:
case inr.inl.hf.intro.intro.intro
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
A : ℝ
hA : A ∈ upperBounds (Set.range fun i => ‖f i‖)
B : ℝ
hB : B ∈ upperBounds (Set.range fun i => ‖g i‖)
i : α
⊢ (fun i => ‖(f + g) i‖) i ≤ A + B

Proof state:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ f i = 0 ∧ g i = 0 → f i + g i = 0

Tactic:
rintro ⟨hf', hg'⟩

Result:
case inl.hf.intro
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
hf' : f i = 0
hg' : g i = 0
⊢ f i + g i = 0

Proof state:
case inr.inr.hf
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
⊢ Summable fun i => ‖(f + g) i‖ ^ p.toReal

Tactic:
refine .of_nonneg_of_le ?_ (fun i => ?_) (((hf.summable hp).add (hg.summable hp)).mul_left C)

Result:
case inr.inr.hf.refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
⊢ ∀ (b : α), 0 ≤ ‖(f + g) b‖ ^ p.toReal

case inr.inr.hf.refine_2
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
i : α
⊢ ‖(f + g) i‖ ^ p.toReal ≤ C * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Proof state:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ ¬f i + g i = 0 → ¬f i = 0 ∨ ¬g i = 0

Tactic:
contrapose!

Result:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ f i = 0 ∧ g i = 0 → f i + g i = 0

Proof state:
case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
⊢ Memℓp (f + g) p

Tactic:
apply memℓp_gen

Result:
case inr.inr.hf
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
⊢ Summable fun i => ‖(f + g) i‖ ^ p.toReal

Proof state:
case inr.inr.hf.refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
⊢ ∀ (b : α), 0 ≤ ‖(f + g) b‖ ^ p.toReal

Tactic:
intro

Result:
case inr.inr.hf.refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
b✝ : α
⊢ 0 ≤ ‖(f + g) b✝‖ ^ p.toReal

Proof state:
case neg
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
i : α
h : ¬p.toReal < 1
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤ 2 ^ (p.toReal - 1) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
let F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]

Result:
case neg
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
i : α
h : ¬p.toReal < 1
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤ 2 ^ (p.toReal - 1) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Proof state:
case inr.inr.hf
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
⊢ Summable fun i => ‖(f + g) i‖ ^ p.toReal

Tactic:
let C : ℝ := if p.toReal < 1 then 1 else (2 : ℝ) ^ (p.toReal - 1)

Result:
case inr.inr.hf
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
⊢ Summable fun i => ‖(f + g) i‖ ^ p.toReal

Proof state:
case inr.inr.hf.refine_1
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
C : ℝ := if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)
b✝ : α
⊢ 0 ≤ ‖(f + g) b✝‖ ^ p.toReal

Tactic:
positivity

Result:
no goals

Proof state:
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
⊢ Memℓp (f + g) p

Tactic:
rcases p.trichotomy with (rfl | rfl | hp)

Result:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
⊢ Memℓp (f + g) 0

case inr.inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f ⊤
hg : Memℓp g ⊤
⊢ Memℓp (f + g) ⊤

case inr.inr
α : Type u_3
E : α → Type u_4
p : ℝ≥0∞
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f p
hg : Memℓp g p
hp : 0 < p.toReal
⊢ Memℓp (f + g) p

Proof state:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
⊢ {i | (f + g) i ≠ 0}.Finite

Tactic:
refine (hf.finite_dsupport.union hg.finite_dsupport).subset fun i => ?_

Result:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
i : α
⊢ i ∈ {i | (f + g) i ≠ 0} → i ∈ {i | f i ≠ 0} ∪ {i | g i ≠ 0}

Proof state:
case inl
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
⊢ Memℓp (f + g) 0

Tactic:
apply memℓp_zero

Result:
case inl.hf
α : Type u_3
E : α → Type u_4
inst✝ : (i : α) → NormedAddCommGroup (E i)
f g : (i : α) → E i
hf : Memℓp f 0
hg : Memℓp g 0
⊢ {i | (f + g) i ≠ 0}.Finite