case inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
hp : 1 ≤ 1
⊢ (∑ i in s, (f i + g i) ^ 1) ^ (1 / 1) ≤ (∑ i in s, f i ^ 1) ^ (1 / 1) + (∑ i in s, g i ^ 1) ^ (1 / 1)

case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
rcases eq_or_lt_of_le hp with (rfl | hp)
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
have hpq := Real.isConjugateExponent_conjugateExponent hp
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
this :
  IsGreatest ((fun g_1 => ∑ i in s, (f + g) i * g_1 i) '' {g | ∑ i in s, g i ^ Real.conjugateExponent p ≤ 1})
    ((∑ i in s, (f + g) i ^ p) ^ (1 / p))
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
have := isGreatest_Lp s (f + g) hpq
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
this :
  IsGreatest
    ((fun a => ∑ x in s, f x * a x + ∑ x in s, g x * a x) '' {g | ∑ i in s, g i ^ Real.conjugateExponent p ≤ 1})
    ((∑ x in s, (f x + g x) ^ p) ^ (1 / p))
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
this :
  IsGreatest ((fun g_1 => ∑ i in s, (f + g) i * g_1 i) '' {g | ∑ i in s, g i ^ Real.conjugateExponent p ≤ 1})
    ((∑ i in s, (f + g) i ^ p) ^ (1 / p))
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
simp only [Pi.add_apply, add_mul, sum_add_distrib] at this
case inr.intro.intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
this :
  IsGreatest
    ((fun a => ∑ x in s, f x * a x + ∑ x in s, g x * a x) '' {g | ∑ i in s, g i ^ Real.conjugateExponent p ≤ 1})
    ((∑ x in s, (f x + g x) ^ p) ^ (1 / p))
φ : ι → ℝ≥0
hφ : φ ∈ {g | ∑ i in s, g i ^ Real.conjugateExponent p ≤ 1}
H : (fun a => ∑ x in s, f x * a x + ∑ x in s, g x * a x) φ = (∑ x in s, (f x + g x) ^ p) ^ (1 / p)
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
this :
  IsGreatest
    ((fun a => ∑ x in s, f x * a x + ∑ x in s, g x * a x) '' {g | ∑ i in s, g i ^ Real.conjugateExponent p ≤ 1})
    ((∑ x in s, (f x + g x) ^ p) ^ (1 / p))
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
rcases this.1 with ⟨φ, hφ, H⟩
case inr.intro.intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
this :
  IsGreatest
    ((fun a => ∑ x in s, f x * a x + ∑ x in s, g x * a x) '' {g | ∑ i in s, g i ^ Real.conjugateExponent p ≤ 1})
    ((∑ x in s, (f x + g x) ^ p) ^ (1 / p))
φ : ι → ℝ≥0
hφ : φ ∈ {g | ∑ i in s, g i ^ Real.conjugateExponent p ≤ 1}
H : (fun a => ∑ x in s, f x * a x + ∑ x in s, g x * a x) φ = (∑ x in s, (f x + g x) ^ p) ^ (1 / p)
⊢ (fun a => ∑ x in s, f x * a x + ∑ x in s, g x * a x) φ ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
case inr.intro.intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
this :
  IsGreatest
    ((fun a => ∑ x in s, f x * a x + ∑ x in s, g x * a x) '' {g | ∑ i in s, g i ^ Real.conjugateExponent p ≤ 1})
    ((∑ x in s, (f x + g x) ^ p) ^ (1 / p))
φ : ι → ℝ≥0
hφ : φ ∈ {g | ∑ i in s, g i ^ Real.conjugateExponent p ≤ 1}
H : (fun a => ∑ x in s, f x * a x + ∑ x in s, g x * a x) φ = (∑ x in s, (f x + g x) ^ p) ^ (1 / p)
⊢ (∑ i in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
rw [← H]
no goals
case inr.intro.intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
hpq : Real.IsConjugateExponent p (Real.conjugateExponent p)
this :
  IsGreatest
    ((fun a => ∑ x in s, f x * a x + ∑ x in s, g x * a x) '' {g | ∑ i in s, g i ^ Real.conjugateExponent p ≤ 1})
    ((∑ x in s, (f x + g x) ^ p) ^ (1 / p))
φ : ι → ℝ≥0
hφ : φ ∈ {g | ∑ i in s, g i ^ Real.conjugateExponent p ≤ 1}
H : (fun a => ∑ x in s, f x * a x + ∑ x in s, g x * a x) φ = (∑ x in s, (f x + g x) ^ p) ^ (1 / p)
⊢ (fun a => ∑ x in s, f x * a x + ∑ x in s, g x * a x) φ ≤ (∑ i in s, f i ^ p) ^ (1 / p) + (∑ i in s, g i ^ p) ^ (1 / p)
exact
  add_le_add ((isGreatest_Lp s f hpq).2 ⟨φ, hφ, rfl⟩) ((isGreatest_Lp s g hpq).2 ⟨φ, hφ, rfl⟩)
no goals
case inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
hp : 1 ≤ 1
⊢ (∑ i in s, (f i + g i) ^ 1) ^ (1 / 1) ≤ (∑ i in s, f i ^ 1) ^ (1 / 1) + (∑ i in s, g i ^ 1) ^ (1 / 1)
simp [Finset.sum_add_distrib]