case intro
ι : Type u
s : Finset ι
g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hg : ∀ (i : ι), 0 ≤ g i
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hgB : HasSum (fun i => g i ^ p) (B ^ p)
f : ι → ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + g i) ^ p) (C ^ p)
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hfA : HasSum (fun i => f i ^ p) (A ^ p)
hgB : HasSum (fun i => g i ^ p) (B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p)
lift f to ι → ℝ≥0 using hf
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : ι → ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
g : ι → ℝ≥0
hgB : HasSum (fun i => (fun i => ↑(g i)) i ^ p) (B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)
case intro
ι : Type u
s : Finset ι
g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hg : ∀ (i : ι), 0 ≤ g i
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hgB : HasSum (fun i => g i ^ p) (B ^ p)
f : ι → ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + g i) ^ p) (C ^ p)
lift g to ι → ℝ≥0 using hg
case intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
B : ℝ
hB : 0 ≤ B
f g : ι → ℝ≥0
hgB : HasSum (fun i => (fun i => ↑(g i)) i ^ p) (B ^ p)
A : ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : ι → ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
g : ι → ℝ≥0
hgB : HasSum (fun i => (fun i => ↑(g i)) i ^ p) (B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)
lift A to ℝ≥0 using hA
case intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A : ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
B : ℝ≥0
hgB : HasSum (fun i => (fun i => ↑(g i)) i ^ p) (↑B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)
case intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
B : ℝ
hB : 0 ≤ B
f g : ι → ℝ≥0
hgB : HasSum (fun i => (fun i => ↑(g i)) i ^ p) (B ^ p)
A : ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)
lift B to ℝ≥0 using hB
case intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)
case intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A : ℝ≥0
hfA : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
B : ℝ≥0
hgB : HasSum (fun i => (fun i => ↑(g i)) i ^ p) (↑B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)
norm_cast  at hfA hgB
case intro.intro.intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)
case intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)
obtain ⟨C, hC₁, hC₂⟩ := NNReal.Lp_add_le_hasSum hp hfA hgB
case intro.intro.intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ 0 ≤ ↑C ∧ ↑C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (↑C ^ p)
case intro.intro.intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (C ^ p)
use C
case intro.intro.intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun a => (f a + g a) ^ p) (C ^ p)
case intro.intro.intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ 0 ≤ ↑C ∧ ↑C ≤ ↑A + ↑B ∧ HasSum (fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) (↑C ^ p)
norm_cast
no goals
case intro.intro.intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f g : ι → ℝ≥0
A B : ℝ≥0
hfA : HasSum (fun a => f a ^ p) (A ^ p)
hgB : HasSum (fun a => g a ^ p) (B ^ p)
C : ℝ≥0
hC₁ : C ≤ A + B
hC₂ : HasSum (fun i => (f i + g i) ^ p) (C ^ p)
⊢ 0 ≤ C ∧ C ≤ A + B ∧ HasSum (fun a => (f a + g a) ^ p) (C ^ p)
exact ⟨zero_le _, hC₁, hC₂⟩