-- 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
α : 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 ⊤
⊢ BddAbove (Set.range fun i => ‖(f + g) i‖)

Tactic:
obtain ⟨A, hA⟩ := hf.bddAbove

Result:
case inr.inl.hf.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‖)
⊢ BddAbove (Set.range fun i => ‖(f + g) i‖)

Proof state:
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 i‖ + ‖g i‖) ^ p.toReal ≤ C * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
dsimp only [C]

Result:
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 i‖ + ‖g i‖) ^ p.toReal ≤ (if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ 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 : 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)

Tactic:
simp only [not_lt] at h

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 : α
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
h : 1 ≤ p.toReal
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤ 2 ^ (p.toReal - 1) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Proof state:
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

Tactic:
exact le_trans (norm_add_le _ _) (add_le_add (hA ⟨i, rfl⟩) (hB ⟨i, rfl⟩))

Result:
no goals

Proof state:
case pos
α : 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 ≤ 1 * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
simpa using NNReal.coe_le_coe.2 (NNReal.rpow_add_le_add_rpow ‖f i‖₊ ‖g i‖₊ hp.le h.le)

Result:
no goals

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‖)
⊢ BddAbove (Set.range fun i => ‖(f + g) i‖)

Tactic:
refine ⟨A + B, ?_⟩

Result:
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‖)

Proof state:
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 i‖ + ‖g i‖) ^ p.toReal ≤ (if p.toReal < 1 then 1 else 2 ^ (p.toReal - 1)) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
split_ifs with h

Result:
case pos
α : 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 ≤ 1 * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

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)

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 : α
F : Fin 2 → ℝ≥0 := ![‖f i‖₊, ‖g i‖₊]
h : 1 ≤ p.toReal
⊢ (‖f i‖ + ‖g i‖) ^ p.toReal ≤ 2 ^ (p.toReal - 1) * (‖f i‖ ^ p.toReal + ‖g i‖ ^ p.toReal)

Tactic:
simpa [Fin.sum_univ_succ] using
  Real.rpow_sum_le_const_mul_sum_rpow_of_nonneg Finset.univ h fun i _ => (F i).coe_nonneg

Result:
no goals

Proof state:
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

Tactic:
simp [hf', hg']

Result:
no goals

Proof state:
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) ⊤

Tactic:
apply memℓp_infty

Result:
case inr.inl.hf
α : 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 ⊤
⊢ BddAbove (Set.range fun i => ‖(f + g) i‖)

Proof state:
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)

Tactic:
refine (Real.rpow_le_rpow (norm_nonneg _) (norm_add_le _ _) hp.le).trans ?_

Result:
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 i‖ + ‖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 : α
⊢ i ∈ {i | (f + g) i ≠ 0} → i ∈ {i | f i ≠ 0} ∪ {i | g i ≠ 0}

Tactic:
simp only [Pi.add_apply, Ne, Set.mem_union, Set.mem_setOf_eq]

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 + g i = 0 → ¬f i = 0 ∨ ¬g i = 0

Proof state:
case inr.inl.hf.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‖)
⊢ BddAbove (Set.range fun i => ‖(f + g) i‖)

Tactic:
obtain ⟨B, hB⟩ := hg.bddAbove

Result:
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‖)
⊢ BddAbove (Set.range fun i => ‖(f + g) i‖)