-- Mathlib/Analysis/MeanInequalities.lean
theorem Lp_add_le_tsum {f g : ι → ℝ≥0} {p : ℝ} (hp : 1 ≤ p) (hf : Summable fun i => f i ^ p)
    (hg : Summable fun i => g i ^ p) :
    (Summable fun i => (f i + g i) ^ p) ∧
      (∑' i, (f i + g i) ^ p) ^ (1 / p) ≤
        (∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)

Proof state:
case refine_1
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
s : Finset ι
⊢ Summable fun i => f i ^ p

case refine_2
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
s : Finset ι
⊢ Summable fun i => g i ^ p

Tactic:
exacts [hf, hg]

Result:
no goals

Proof state:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p)
⊢ (Summable fun i => (f i + g i) ^ p) ∧
    (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Tactic:
have H₂ : Summable _ := (hasSum_of_isLUB _ (isLUB_ciSup bdd)).summable

Result:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p)
H₂ : Summable fun i => (f i + g i) ^ p
⊢ (Summable fun i => (f i + g i) ^ p) ∧
    (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Proof state:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
⊢ ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p

Tactic:
intro s

Result:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
s : Finset ι
⊢ ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p

Proof state:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p)
H₂ : Summable fun i => (f i + g i) ^ p
⊢ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Tactic:
rw [one_div, NNReal.rpow_inv_le_iff pos, ← one_div]

Result:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p)
H₂ : Summable fun i => (f i + g i) ^ p
⊢ ∑' (i : ι), (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p

Proof state:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
s : Finset ι
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Tactic:
refine le_trans (Lp_add_le s f g hp) (add_le_add ?_ ?_) <;>
    rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr pos)] <;>
  refine sum_le_tsum _ (fun _ _ => zero_le _) ?_

Result:
case refine_1
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
s : Finset ι
⊢ Summable fun i => f i ^ p

case refine_2
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
s : Finset ι
⊢ Summable fun i => g i ^ p

Proof state:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
s : Finset ι
⊢ ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p

Tactic:
rw [one_div, ← NNReal.rpow_inv_le_iff pos, ← one_div]

Result:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
s : Finset ι
⊢ (∑ i ∈ s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Proof state:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
⊢ BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p)

Tactic:
refine ⟨((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p, ?_⟩

Result:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
⊢ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p ∈
    upperBounds (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p)

Proof state:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p)
H₂ : Summable fun i => (f i + g i) ^ p
⊢ ∑' (i : ι), (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p

Tactic:
exact tsum_le_of_sum_le H₂ H₁

Result:
no goals

Proof state:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
⊢ (Summable fun i => (f i + g i) ^ p) ∧
    (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Tactic:
have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp

Result:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
⊢ (Summable fun i => (f i + g i) ^ p) ∧
    (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Proof state:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
⊢ (Summable fun i => (f i + g i) ^ p) ∧
    (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)

Tactic:
have bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p) := by
  refine ⟨((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p, ?_⟩
  rintro a ⟨s, rfl⟩
  exact H₁ s

Result:
ι : Type u
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ p
pos : 0 < p
H₁ :
  ∀ (s : Finset ι), ∑ i ∈ s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
bdd : BddAbove (Set.range fun s => ∑ i ∈ s, (f i + g i) ^ p)
⊢ (Summable fun i => (f i + g i) ^ p) ∧
    (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)