[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
[PROOFSTEP]
by_cases A : ∃ i ∈ s, z i = 0 ∧ w i ≠ 0
[GOAL]
case pos
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∃ i, i ∈ s ∧ z i = 0 ∧ w i ≠ 0
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
[PROOFSTEP]
rcases A with ⟨i, his, hzi, hwi⟩
[GOAL]
case pos.intro.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
[PROOFSTEP]
rw [prod_eq_zero his]
[GOAL]
case pos.intro.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ 0 ≤ ∑ i in s, w i * z i
[PROOFSTEP]
exact sum_nonneg fun j hj => mul_nonneg (hw j hj) (hz j hj)
[GOAL]
case pos.intro.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ z i ^ w i = 0
[PROOFSTEP]
rw [hzi]
[GOAL]
case pos.intro.intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
i : ι
his : i ∈ s
hzi : z i = 0
hwi : w i ≠ 0
⊢ 0 ^ w i = 0
[PROOFSTEP]
exact zero_rpow hwi
[GOAL]
case neg
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ¬∃ i, i ∈ s ∧ z i = 0 ∧ w i ≠ 0
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
[PROOFSTEP]
simp only [not_exists, not_and, Ne.def, Classical.not_not] at A 
[GOAL]
case neg
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
[PROOFSTEP]
have := convexOn_exp.map_sum_le hw hw' fun i _ => Set.mem_univ <| log (z i)
[GOAL]
case neg
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : exp (∑ i in s, w i • log (z i)) ≤ ∑ i in s, w i • exp (log (z i))
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
[PROOFSTEP]
simp only [exp_sum, (· ∘ ·), smul_eq_mul, mul_comm (w _) (log _)] at this 
[GOAL]
case neg
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
[PROOFSTEP]
convert this using 1 <;> [apply prod_congr rfl; apply sum_congr rfl]
[GOAL]
case neg
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
⊢ ∏ i in s, z i ^ w i ≤ ∑ i in s, w i * z i
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_3
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
⊢ ∏ i in s, z i ^ w i = ∏ x in s, exp (log (z x) * w x)
[PROOFSTEP]
apply prod_congr rfl
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
⊢ ∑ i in s, w i * z i = ∑ x in s, w x * exp (log (z x))
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case h.e'_3
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
⊢ ∀ (x : ι), x ∈ s → z x ^ w x = exp (log (z x) * w x)
[PROOFSTEP]
intro i hi
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
⊢ ∀ (x : ι), x ∈ s → w x * z x = w x * exp (log (z x))
[PROOFSTEP]
intro i hi
[GOAL]
case h.e'_3
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
⊢ z i ^ w i = exp (log (z i) * w i)
[PROOFSTEP]
cases' eq_or_lt_of_le (hz i hi) with hz hz
[GOAL]
case h.e'_3.inl
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz✝ : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
hz : 0 = z i
⊢ z i ^ w i = exp (log (z i) * w i)
[PROOFSTEP]
simp [A i hi hz.symm]
[GOAL]
case h.e'_3.inr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz✝ : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ z i ^ w i = exp (log (z i) * w i)
[PROOFSTEP]
exact rpow_def_of_pos hz _
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
⊢ w i * z i = w i * exp (log (z i))
[PROOFSTEP]
cases' eq_or_lt_of_le (hz i hi) with hz hz
[GOAL]
case h.e'_4.inl
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz✝ : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
hz : 0 = z i
⊢ w i * z i = w i * exp (log (z i))
[PROOFSTEP]
simp [A i hi hz.symm]
[GOAL]
case h.e'_4.inr
ι : Type u
s : Finset ι
w z : ι → ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz✝ : ∀ (i : ι), i ∈ s → 0 ≤ z i
A : ∀ (x : ι), x ∈ s → z x = 0 → w x = 0
this : ∏ x in s, exp (log (z x) * w x) ≤ ∑ x in s, w x * exp (log (z x))
i : ι
hi : i ∈ s
hz : 0 < z i
⊢ w i * z i = w i * exp (log (z i))
[PROOFSTEP]
rw [exp_log hz]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∏ i in s, z i ^ w i = ∏ i in s, x ^ w i
[PROOFSTEP]
refine' prod_congr rfl fun i hi => _
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
⊢ z i ^ w i = x ^ w i
[PROOFSTEP]
cases' eq_or_ne (w i) 0 with h₀ h₀
[GOAL]
case inl
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
h₀ : w i = 0
⊢ z i ^ w i = x ^ w i
[PROOFSTEP]
rw [h₀, rpow_zero, rpow_zero]
[GOAL]
case inr
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
h₀ : w i ≠ 0
⊢ z i ^ w i = x ^ w i
[PROOFSTEP]
rw [hx i hi h₀]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∏ i in s, x ^ w i = x
[PROOFSTEP]
rw [← rpow_sum_of_nonneg _ hw, hw', rpow_one]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ 0 ≤ x
[PROOFSTEP]
have : (∑ i in s, w i) ≠ 0 := by
  rw [hw']
  exact one_ne_zero
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∑ i in s, w i ≠ 0
[PROOFSTEP]
rw [hw']
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ 1 ≠ 0
[PROOFSTEP]
exact one_ne_zero
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
this : ∑ i in s, w i ≠ 0
⊢ 0 ≤ x
[PROOFSTEP]
obtain ⟨i, his, hi⟩ := exists_ne_zero_of_sum_ne_zero this
[GOAL]
case intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
this : ∑ i in s, w i ≠ 0
i : ι
his : i ∈ s
hi : w i ≠ 0
⊢ 0 ≤ x
[PROOFSTEP]
rw [← hx i his hi]
[GOAL]
case intro.intro
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
this : ∑ i in s, w i ≠ 0
i : ι
his : i ∈ s
hi : w i ≠ 0
⊢ 0 ≤ z i
[PROOFSTEP]
exact hz i his
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∑ i in s, w i * z i = ∑ i in s, w i * x
[PROOFSTEP]
refine' sum_congr rfl fun i hi => _
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
⊢ w i * z i = w i * x
[PROOFSTEP]
cases' eq_or_ne (w i) 0 with hwi hwi
[GOAL]
case inl
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i = 0
⊢ w i * z i = w i * x
[PROOFSTEP]
rw [hwi, zero_mul, zero_mul]
[GOAL]
case inr
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
i : ι
hi : i ∈ s
hwi : w i ≠ 0
⊢ w i * z i = w i * x
[PROOFSTEP]
rw [hx i hi hwi]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw' : ∑ i in s, w i = 1
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∑ i in s, w i * x = x
[PROOFSTEP]
rw [← sum_mul, hw', one_mul]
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∏ i in s, z i ^ w i = ∑ i in s, w i * z i
[PROOFSTEP]
rw [geom_mean_weighted_of_constant, arith_mean_weighted_of_constant]
[GOAL]
case x
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ℝ
[PROOFSTEP]
assumption
[GOAL]
case hw'
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∑ i in s, w i = 1
[PROOFSTEP]
assumption
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
[PROOFSTEP]
assumption
[GOAL]
case hw
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∀ (i : ι), i ∈ s → 0 ≤ w i
[PROOFSTEP]
assumption
[GOAL]
case hw'
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∑ i in s, w i = 1
[PROOFSTEP]
assumption
[GOAL]
case hz
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∀ (i : ι), i ∈ s → 0 ≤ z i
[PROOFSTEP]
assumption
[GOAL]
case hx
ι : Type u
s : Finset ι
w z : ι → ℝ
x : ℝ
hw : ∀ (i : ι), i ∈ s → 0 ≤ w i
hw' : ∑ i in s, w i = 1
hz : ∀ (i : ι), i ∈ s → 0 ≤ z i
hx : ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
⊢ ∀ (i : ι), i ∈ s → w i ≠ 0 → z i = x
[PROOFSTEP]
assumption
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
⊢ ∏ i in s, z i ^ ↑(w i) ≤ ∑ i in s, w i * z i
[PROOFSTEP]
exact_mod_cast
  Real.geom_mean_le_arith_mean_weighted _ _ _ (fun i _ => (w i).coe_nonneg) (by assumption_mod_cast) fun i _ =>
    (z i).coe_nonneg
[GOAL]
ι : Type u
s : Finset ι
w z : ι → ℝ≥0
hw' : ∑ i in s, w i = 1
⊢ ∑ i in s, ↑(w i) = 1
[PROOFSTEP]
assumption_mod_cast
[GOAL]
ι : Type u
s : Finset ι
w₁ w₂ p₁ p₂ : ℝ≥0
⊢ w₁ + w₂ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ ≤ w₁ * p₁ + w₂ * p₂
[PROOFSTEP]
simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty, Fintype.univ_of_isEmpty,
  Fin.cons_succ, Fin.cons_zero, add_zero, mul_one] using geom_mean_le_arith_mean_weighted univ ![w₁, w₂] ![p₁, p₂]
[GOAL]
ι : Type u
s : Finset ι
w₁ w₂ w₃ p₁ p₂ p₃ : ℝ≥0
⊢ w₁ + w₂ + w₃ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃
[PROOFSTEP]
simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty, Fintype.univ_of_isEmpty,
  Fin.cons_succ, Fin.cons_zero, add_zero, mul_one, ← add_assoc, mul_assoc] using
  geom_mean_le_arith_mean_weighted univ ![w₁, w₂, w₃] ![p₁, p₂, p₃]
[GOAL]
ι : Type u
s : Finset ι
w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ≥0
⊢ w₁ + w₂ + w₃ + w₄ = 1 → p₁ ^ ↑w₁ * p₂ ^ ↑w₂ * p₃ ^ ↑w₃ * p₄ ^ ↑w₄ ≤ w₁ * p₁ + w₂ * p₂ + w₃ * p₃ + w₄ * p₄
[PROOFSTEP]
simpa only [Fin.prod_univ_succ, Fin.sum_univ_succ, Finset.prod_empty, Finset.sum_empty, Fintype.univ_of_isEmpty,
  Fin.cons_succ, Fin.cons_zero, add_zero, mul_one, ← add_assoc, mul_assoc] using
  geom_mean_le_arith_mean_weighted univ ![w₁, w₂, w₃, w₄] ![p₁, p₂, p₃, p₄]
[GOAL]
ι : Type u
s : Finset ι
w₁ w₂ p₁ p₂ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hw : w₁ + w₂ = 1
⊢ ↑({ val := w₁, property := hw₁ } + { val := w₂, property := hw₂ }) = ↑1
[PROOFSTEP]
assumption
[GOAL]
ι : Type u
s : Finset ι
w₁ w₂ w₃ w₄ p₁ p₂ p₃ p₄ : ℝ
hw₁ : 0 ≤ w₁
hw₂ : 0 ≤ w₂
hw₃ : 0 ≤ w₃
hw₄ : 0 ≤ w₄
hp₁ : 0 ≤ p₁
hp₂ : 0 ≤ p₂
hp₃ : 0 ≤ p₃
hp₄ : 0 ≤ p₄
hw : w₁ + w₂ + w₃ + w₄ = 1
⊢ ↑({ val := w₁, property := hw₁ } + { val := w₂, property := hw₂ } + { val := w₃, property := hw₃ } +
        { val := w₄, property := hw₄ }) =
    ↑1
[PROOFSTEP]
assumption
[GOAL]
ι : Type u
s : Finset ι
a b p q : ℝ
ha : 0 ≤ a
hb : 0 ≤ b
hpq : IsConjugateExponent p q
⊢ a * b ≤ a ^ p / p + b ^ q / q
[PROOFSTEP]
simpa [← rpow_mul, ha, hb, hpq.ne_zero, hpq.symm.ne_zero, _root_.div_eq_inv_mul] using
  geom_mean_le_arith_mean2_weighted hpq.one_div_nonneg hpq.symm.one_div_nonneg (rpow_nonneg_of_nonneg ha p)
    (rpow_nonneg_of_nonneg hb q) hpq.inv_add_inv_conj
[GOAL]
ι : Type u
s : Finset ι
a b : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ a * b ≤ a ^ p / Real.toNNReal p + b ^ q / Real.toNNReal q
[PROOFSTEP]
nth_rw 1 [← Real.coe_toNNReal p hpq.nonneg]
[GOAL]
ι : Type u
s : Finset ι
a b : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ a * b ≤ a ^ ↑(Real.toNNReal p) / Real.toNNReal p + b ^ q / Real.toNNReal q
[PROOFSTEP]
nth_rw 1 [← Real.coe_toNNReal q hpq.symm.nonneg]
[GOAL]
ι : Type u
s : Finset ι
a b : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ a * b ≤ a ^ ↑(Real.toNNReal p) / Real.toNNReal p + b ^ ↑(Real.toNNReal q) / Real.toNNReal q
[PROOFSTEP]
exact young_inequality a b hpq.one_lt_nnreal hpq.inv_add_inv_conj_nnreal
[GOAL]
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
[PROOFSTEP]
by_cases h : a = ⊤ ∨ b = ⊤
[GOAL]
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
[PROOFSTEP]
refine' le_trans le_top (le_of_eq _)
[GOAL]
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
[PROOFSTEP]
repeat rw [div_eq_mul_inv]
[GOAL]
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q / ENNReal.ofReal q
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
[PROOFSTEP]
rw [div_eq_mul_inv]
[GOAL]
case pos
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤ ∨ b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
[PROOFSTEP]
cases' h with h h
[GOAL]
case pos.inl
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
[PROOFSTEP]
rw [h]
[GOAL]
case pos.inr
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
[PROOFSTEP]
rw [h]
[GOAL]
case pos.inl
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a = ⊤
⊢ ⊤ = ⊤ ^ p * (ENNReal.ofReal p)⁻¹ + b ^ q * (ENNReal.ofReal q)⁻¹
[PROOFSTEP]
simp [h, hpq.pos, hpq.symm.pos]
[GOAL]
case pos.inr
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : b = ⊤
⊢ ⊤ = a ^ p * (ENNReal.ofReal p)⁻¹ + ⊤ ^ q * (ENNReal.ofReal q)⁻¹
[PROOFSTEP]
simp [h, hpq.pos, hpq.symm.pos]
[GOAL]
case neg
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : ¬(a = ⊤ ∨ b = ⊤)
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
[PROOFSTEP]
push_neg at h 
[GOAL]
case neg
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ a * b ≤ a ^ p / ENNReal.ofReal p + b ^ q / ENNReal.ofReal q
[PROOFSTEP]
rw [← coe_toNNReal h.left, ← coe_toNNReal h.right, ← coe_mul, coe_rpow_of_nonneg _ hpq.nonneg,
  coe_rpow_of_nonneg _ hpq.symm.nonneg, ENNReal.ofReal, ENNReal.ofReal, ←
  @coe_div (Real.toNNReal p) _ (by simp [hpq.pos]), ← @coe_div (Real.toNNReal q) _ (by simp [hpq.symm.pos]), ← coe_add,
  coe_le_coe]
[GOAL]
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ Real.toNNReal p ≠ 0
[PROOFSTEP]
simp [hpq.pos]
[GOAL]
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ Real.toNNReal q ≠ 0
[PROOFSTEP]
simp [hpq.symm.pos]
[GOAL]
case neg
ι : Type u
s : Finset ι
a b : ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
h : a ≠ ⊤ ∧ b ≠ ⊤
⊢ ENNReal.toNNReal a * ENNReal.toNNReal b ≤
    ENNReal.toNNReal a ^ p / Real.toNNReal p + ENNReal.toNNReal b ^ q / Real.toNNReal q
[PROOFSTEP]
exact NNReal.young_inequality_real a.toNNReal b.toNNReal hpq
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
⊢ ∑ i in s, f i * g i ≤ 1
[PROOFSTEP]
have hp_ne_zero : Real.toNNReal p ≠ 0 := (zero_lt_one.trans hpq.one_lt_nnreal).ne.symm
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
⊢ ∑ i in s, f i * g i ≤ 1
[PROOFSTEP]
have hq_ne_zero : Real.toNNReal q ≠ 0 := (zero_lt_one.trans hpq.symm.one_lt_nnreal).ne.symm
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
hq_ne_zero : Real.toNNReal q ≠ 0
⊢ ∑ i in s, f i * g i ≤ 1
[PROOFSTEP]
calc
  ∑ i in s, f i * g i ≤ ∑ i in s, (f i ^ p / Real.toNNReal p + g i ^ q / Real.toNNReal q) :=
    Finset.sum_le_sum fun i _ => young_inequality_real (f i) (g i) hpq
  _ = (∑ i in s, f i ^ p) / Real.toNNReal p + (∑ i in s, g i ^ q) / Real.toNNReal q := by
    rw [sum_add_distrib, sum_div, sum_div]
  _ ≤ 1 / Real.toNNReal p + 1 / Real.toNNReal q :=
    by
    refine' add_le_add _ _
    · rwa [div_le_iff hp_ne_zero, div_mul_cancel _ hp_ne_zero]
    · rwa [div_le_iff hq_ne_zero, div_mul_cancel _ hq_ne_zero]
  _ = 1 := hpq.inv_add_inv_conj_nnreal
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
hq_ne_zero : Real.toNNReal q ≠ 0
⊢ ∑ i in s, (f i ^ p / Real.toNNReal p + g i ^ q / Real.toNNReal q) =
    (∑ i in s, f i ^ p) / Real.toNNReal p + (∑ i in s, g i ^ q) / Real.toNNReal q
[PROOFSTEP]
rw [sum_add_distrib, sum_div, sum_div]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
hq_ne_zero : Real.toNNReal q ≠ 0
⊢ (∑ i in s, f i ^ p) / Real.toNNReal p + (∑ i in s, g i ^ q) / Real.toNNReal q ≤
    1 / Real.toNNReal p + 1 / Real.toNNReal q
[PROOFSTEP]
refine' add_le_add _ _
[GOAL]
case refine'_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
hq_ne_zero : Real.toNNReal q ≠ 0
⊢ (∑ i in s, f i ^ p) / Real.toNNReal p ≤ 1 / Real.toNNReal p
[PROOFSTEP]
rwa [div_le_iff hp_ne_zero, div_mul_cancel _ hp_ne_zero]
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p ≤ 1
hg : ∑ i in s, g i ^ q ≤ 1
hp_ne_zero : Real.toNNReal p ≠ 0
hq_ne_zero : Real.toNNReal q ≠ 0
⊢ (∑ i in s, g i ^ q) / Real.toNNReal q ≤ 1 / Real.toNNReal q
[PROOFSTEP]
rwa [div_le_iff hq_ne_zero, div_mul_cancel _ hq_ne_zero]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p = 0
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
simp only [hf, hpq.ne_zero, one_div, sum_eq_zero_iff, zero_rpow, zero_mul, inv_eq_zero, Ne.def, not_false_iff,
  le_zero_iff, mul_eq_zero]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p = 0
⊢ ∀ (x : ι), x ∈ s → f x = 0 ∨ g x = 0
[PROOFSTEP]
intro i his
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p = 0
i : ι
his : i ∈ s
⊢ f i = 0 ∨ g i = 0
[PROOFSTEP]
left
[GOAL]
case h
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p = 0
i : ι
his : i ∈ s
⊢ f i = 0
[PROOFSTEP]
rw [sum_eq_zero_iff] at hf 
[GOAL]
case h
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∀ (x : ι), x ∈ s → f x ^ p = 0
i : ι
his : i ∈ s
⊢ f i = 0
[PROOFSTEP]
exact (rpow_eq_zero_iff.mp (hf i his)).left
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
by_cases hF_zero : ∑ i in s, f i ^ p = 0
[GOAL]
case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ∑ i in s, f i ^ p = 0
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
exact inner_le_Lp_mul_Lp_of_norm_eq_zero s f g hpq hF_zero
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
by_cases hG_zero : ∑ i in s, g i ^ q = 0
[GOAL]
case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ∑ i in s, g i ^ q = 0
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
calc
  ∑ i in s, f i * g i = ∑ i in s, g i * f i := by
    congr with i
    rw [mul_comm]
  _ ≤ (∑ i in s, g i ^ q) ^ (1 / q) * (∑ i in s, f i ^ p) ^ (1 / p) :=
    (inner_le_Lp_mul_Lp_of_norm_eq_zero s g f hpq.symm hG_zero)
  _ = (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q) := mul_comm _ _
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ∑ i in s, g i ^ q = 0
⊢ ∑ i in s, f i * g i = ∑ i in s, g i * f i
[PROOFSTEP]
congr with i
[GOAL]
case e_f.h.a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ∑ i in s, g i ^ q = 0
i : ι
⊢ ↑(f i * g i) = ↑(g i * f i)
[PROOFSTEP]
rw [mul_comm]
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
let f' i := f i / (∑ i in s, f i ^ p) ^ (1 / p)
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
f' : ι → ℝ≥0 := fun i => f i / (∑ i in s, f i ^ p) ^ (1 / p)
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
let g' i := g i / (∑ i in s, g i ^ q) ^ (1 / q)
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
f' : ι → ℝ≥0 := fun i => f i / (∑ i in s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i in s, g i ^ q) ^ (1 / q)
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
suffices (∑ i in s, f' i * g' i) ≤ 1
  by
  simp_rw [div_mul_div_comm, ← sum_div] at this 
  rwa [div_le_iff, one_mul] at this 
  refine' mul_ne_zero _ _
  · rw [Ne.def, rpow_eq_zero_iff, not_and_or]
    exact Or.inl hF_zero
  · rw [Ne.def, rpow_eq_zero_iff, not_and_or]
    exact Or.inl hG_zero
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
f' : ι → ℝ≥0 := fun i => f i / (∑ i in s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i in s, g i ^ q) ^ (1 / q)
this : ∑ i in s, f' i * g' i ≤ 1
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
simp_rw [div_mul_div_comm, ← sum_div] at this 
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
f' : ι → ℝ≥0 := fun i => f i / (∑ i in s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i in s, g i ^ q) ^ (1 / q)
this : (∑ i in s, f i * g i) / ((∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)) ≤ 1
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
rwa [div_le_iff, one_mul] at this 
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
f' : ι → ℝ≥0 := fun i => f i / (∑ i in s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i in s, g i ^ q) ^ (1 / q)
this : (∑ i in s, f i * g i) / ((∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)) ≤ 1
⊢ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
[PROOFSTEP]
refine' mul_ne_zero _ _
[GOAL]
case refine'_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
f' : ι → ℝ≥0 := fun i => f i / (∑ i in s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i in s, g i ^ q) ^ (1 / q)
this : (∑ i in s, f i * g i) / ((∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)) ≤ 1
⊢ (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0
[PROOFSTEP]
rw [Ne.def, rpow_eq_zero_iff, not_and_or]
[GOAL]
case refine'_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
f' : ι → ℝ≥0 := fun i => f i / (∑ i in s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i in s, g i ^ q) ^ (1 / q)
this : (∑ i in s, f i * g i) / ((∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)) ≤ 1
⊢ ¬∑ i in s, f i ^ p = 0 ∨ ¬1 / p ≠ 0
[PROOFSTEP]
exact Or.inl hF_zero
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
f' : ι → ℝ≥0 := fun i => f i / (∑ i in s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i in s, g i ^ q) ^ (1 / q)
this : (∑ i in s, f i * g i) / ((∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)) ≤ 1
⊢ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
[PROOFSTEP]
rw [Ne.def, rpow_eq_zero_iff, not_and_or]
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
f' : ι → ℝ≥0 := fun i => f i / (∑ i in s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i in s, g i ^ q) ^ (1 / q)
this : (∑ i in s, f i * g i) / ((∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)) ≤ 1
⊢ ¬∑ i in s, g i ^ q = 0 ∨ ¬1 / q ≠ 0
[PROOFSTEP]
exact Or.inl hG_zero
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
f' : ι → ℝ≥0 := fun i => f i / (∑ i in s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i in s, g i ^ q) ^ (1 / q)
⊢ ∑ i in s, f' i * g' i ≤ 1
[PROOFSTEP]
refine' inner_le_Lp_mul_Lp_of_norm_le_one s f' g' hpq (le_of_eq _) (le_of_eq _)
[GOAL]
case neg.refine'_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
f' : ι → ℝ≥0 := fun i => f i / (∑ i in s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i in s, g i ^ q) ^ (1 / q)
⊢ ∑ i in s, f' i ^ p = 1
[PROOFSTEP]
simp_rw [div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel hpq.ne_zero, rpow_one, div_self hF_zero]
[GOAL]
case neg.refine'_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hF_zero : ¬∑ i in s, f i ^ p = 0
hG_zero : ¬∑ i in s, g i ^ q = 0
f' : ι → ℝ≥0 := fun i => f i / (∑ i in s, f i ^ p) ^ (1 / p)
g' : ι → ℝ≥0 := fun i => g i / (∑ i in s, g i ^ q) ^ (1 / q)
⊢ ∑ i in s, g' i ^ q = 1
[PROOFSTEP]
simp_rw [div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel hpq.symm.ne_zero, rpow_one, div_self hG_zero]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
⊢ (Summable fun i => f i * g i) ∧
    ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
[PROOFSTEP]
have H₁ : ∀ s : Finset ι, ∑ i in s, f i * g i ≤ (∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q) :=
  by
  intro s
  refine' le_trans (inner_le_Lp_mul_Lq s f g hpq) (mul_le_mul _ _ bot_le bot_le)
  · rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr hpq.pos)]
    exact sum_le_tsum _ (fun _ _ => zero_le _) hf
  · rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr hpq.symm.pos)]
    exact sum_le_tsum _ (fun _ _ => zero_le _) hg
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
⊢ ∀ (s : Finset ι), ∑ i in s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
[PROOFSTEP]
intro s
[GOAL]
ι : Type u
s✝ : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ ∑ i in s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
[PROOFSTEP]
refine' le_trans (inner_le_Lp_mul_Lq s f g hpq) (mul_le_mul _ _ bot_le bot_le)
[GOAL]
case refine'_1
ι : Type u
s✝ : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ (∑ i in s, f i ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p)
[PROOFSTEP]
rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr hpq.pos)]
[GOAL]
case refine'_1
ι : Type u
s✝ : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ ∑ i in s, f i ^ p ≤ ∑' (i : ι), f i ^ p
[PROOFSTEP]
exact sum_le_tsum _ (fun _ _ => zero_le _) hf
[GOAL]
case refine'_2
ι : Type u
s✝ : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ (∑ i in s, g i ^ q) ^ (1 / q) ≤ (∑' (i : ι), g i ^ q) ^ (1 / q)
[PROOFSTEP]
rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr hpq.symm.pos)]
[GOAL]
case refine'_2
ι : Type u
s✝ : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
s : Finset ι
⊢ ∑ i in s, g i ^ q ≤ ∑' (i : ι), g i ^ q
[PROOFSTEP]
exact sum_le_tsum _ (fun _ _ => zero_le _) hg
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i in s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ (Summable fun i => f i * g i) ∧
    ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
[PROOFSTEP]
have bdd : BddAbove (Set.range fun s => ∑ i in s, f i * g i) :=
  by
  refine' ⟨(∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q), _⟩
  rintro a ⟨s, rfl⟩
  exact H₁ s
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i in s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ BddAbove (Set.range fun s => ∑ i in s, f i * g i)
[PROOFSTEP]
refine' ⟨(∑' i, f i ^ p) ^ (1 / p) * (∑' i, g i ^ q) ^ (1 / q), _⟩
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i in s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q) ∈
    upperBounds (Set.range fun s => ∑ i in s, f i * g i)
[PROOFSTEP]
rintro a ⟨s, rfl⟩
[GOAL]
case intro
ι : Type u
s✝ : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i in s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
s : Finset ι
⊢ (fun s => ∑ i in s, f i * g i) s ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
[PROOFSTEP]
exact H₁ s
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i in s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
bdd : BddAbove (Set.range fun s => ∑ i in s, f i * g i)
⊢ (Summable fun i => f i * g i) ∧
    ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
[PROOFSTEP]
have H₂ : Summable _ := (hasSum_of_isLUB _ (isLUB_ciSup bdd)).summable
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : Summable fun i => f i ^ p
hg : Summable fun i => g i ^ q
H₁ : ∀ (s : Finset ι), ∑ i in s, f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
bdd : BddAbove (Set.range fun s => ∑ i in s, f i * g i)
H₂ : Summable fun i => f i * g i
⊢ (Summable fun i => f i * g i) ∧
    ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
[PROOFSTEP]
exact ⟨H₂, tsum_le_of_sum_le H₂ H₁⟩
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
⊢ ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C
[PROOFSTEP]
obtain ⟨H₁, H₂⟩ := inner_le_Lp_mul_Lq_tsum hpq hf.summable hg.summable
[GOAL]
case intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C
[PROOFSTEP]
have hA : A = (∑' i : ι, f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hpq.ne_zero]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ A = (∑' (i : ι), f i ^ p) ^ (1 / p)
[PROOFSTEP]
rw [hf.tsum_eq, rpow_inv_rpow_self hpq.ne_zero]
[GOAL]
case intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C
[PROOFSTEP]
have hB : B = (∑' i : ι, g i ^ q) ^ (1 / q) := by rw [hg.tsum_eq, rpow_inv_rpow_self hpq.symm.ne_zero]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ B = (∑' (i : ι), g i ^ q) ^ (1 / q)
[PROOFSTEP]
rw [hg.tsum_eq, rpow_inv_rpow_self hpq.symm.ne_zero]
[GOAL]
case intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ ∃ C, C ≤ A * B ∧ HasSum (fun i => f i * g i) C
[PROOFSTEP]
refine' ⟨∑' i, f i * g i, _, _⟩
[GOAL]
case intro.refine'_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ ∑' (i : ι), f i * g i ≤ A * B
[PROOFSTEP]
simpa [hA, hB] using H₂
[GOAL]
case intro.refine'_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ q) (B ^ q)
H₁ : Summable fun i => f i * g i
H₂ : ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ q) ^ (1 / q)
⊢ HasSum (fun i => f i * g i) (∑' (i : ι), f i * g i)
[PROOFSTEP]
simpa only [rpow_self_rpow_inv hpq.ne_zero] using H₁.hasSum
[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
cases' eq_or_lt_of_le hp with hp hp
[GOAL]
case inl
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 = p
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
simp [← hp]
[GOAL]
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
let q : ℝ := p / (p - 1)
[GOAL]
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
have hpq : p.IsConjugateExponent q := by rw [Real.isConjugateExponent_iff hp]
[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
⊢ Real.IsConjugateExponent p q
[PROOFSTEP]
rw [Real.isConjugateExponent_iff hp]
[GOAL]
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
have hp₁ : 1 / p * p = 1 := one_div_mul_cancel hpq.ne_zero
[GOAL]
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
have hq : 1 / q * p = p - 1 := by
  rw [← hpq.div_conj_eq_sub_one]
  ring
[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
⊢ 1 / q * p = p - 1
[PROOFSTEP]
rw [← hpq.div_conj_eq_sub_one]
[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
⊢ 1 / q * p = p / q
[PROOFSTEP]
ring
[GOAL]
case inr
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
hq : 1 / q * p = p - 1
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
simpa only [NNReal.mul_rpow, ← NNReal.rpow_mul, hp₁, hq, one_mul, one_rpow, rpow_one, Pi.one_apply, sum_const,
  Nat.smul_one_eq_coe] using NNReal.rpow_le_rpow (inner_le_Lp_mul_Lq s 1 f hpq.symm) hpq.nonneg
[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ IsGreatest ((fun g => ∑ i in s, f i * g i) '' {g | ∑ i in s, g i ^ q ≤ 1}) ((∑ i in s, f i ^ p) ^ (1 / p))
[PROOFSTEP]
constructor
[GOAL]
case left
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ (∑ i in s, f i ^ p) ^ (1 / p) ∈ (fun g => ∑ i in s, f i * g i) '' {g | ∑ i in s, g i ^ q ≤ 1}
[PROOFSTEP]
use fun i => f i ^ p / f i / (∑ i in s, f i ^ p) ^ (1 / q)
[GOAL]
case h
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ (fun i => f i ^ p / f i / (∑ i in s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i in s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i in s, f i * g i) fun i => f i ^ p / f i / (∑ i in s, f i ^ p) ^ (1 / q)) =
      (∑ i in s, f i ^ p) ^ (1 / p)
[PROOFSTEP]
by_cases hf : ∑ i in s, f i ^ p = 0
[GOAL]
case pos
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ∑ i in s, f i ^ p = 0
⊢ (fun i => f i ^ p / f i / (∑ i in s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i in s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i in s, f i * g i) fun i => f i ^ p / f i / (∑ i in s, f i ^ p) ^ (1 / q)) =
      (∑ i in s, f i ^ p) ^ (1 / p)
[PROOFSTEP]
simp [hf, hpq.ne_zero, hpq.symm.ne_zero]
[GOAL]
case neg
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ¬∑ i in s, f i ^ p = 0
⊢ (fun i => f i ^ p / f i / (∑ i in s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i in s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i in s, f i * g i) fun i => f i ^ p / f i / (∑ i in s, f i ^ p) ^ (1 / q)) =
      (∑ i in s, f i ^ p) ^ (1 / p)
[PROOFSTEP]
have A : p + q - q ≠ 0 := by simp [hpq.ne_zero]
[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ¬∑ i in s, f i ^ p = 0
⊢ p + q - q ≠ 0
[PROOFSTEP]
simp [hpq.ne_zero]
[GOAL]
case neg
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ¬∑ i in s, f i ^ p = 0
A : p + q - q ≠ 0
⊢ (fun i => f i ^ p / f i / (∑ i in s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i in s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i in s, f i * g i) fun i => f i ^ p / f i / (∑ i in s, f i ^ p) ^ (1 / q)) =
      (∑ i in s, f i ^ p) ^ (1 / p)
[PROOFSTEP]
have B : ∀ y : ℝ≥0, y * y ^ p / y = y ^ p :=
  by
  refine' fun y => mul_div_cancel_left_of_imp fun h => _
  simp [h, hpq.ne_zero]
[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ¬∑ i in s, f i ^ p = 0
A : p + q - q ≠ 0
⊢ ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
[PROOFSTEP]
refine' fun y => mul_div_cancel_left_of_imp fun h => _
[GOAL]
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ¬∑ i in s, f i ^ p = 0
A : p + q - q ≠ 0
y : ℝ≥0
h : y = 0
⊢ y ^ p = 0
[PROOFSTEP]
simp [h, hpq.ne_zero]
[GOAL]
case neg
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ¬∑ i in s, f i ^ p = 0
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (fun i => f i ^ p / f i / (∑ i in s, f i ^ p) ^ (1 / q)) ∈ {g | ∑ i in s, g i ^ q ≤ 1} ∧
    ((fun g => ∑ i in s, f i * g i) fun i => f i ^ p / f i / (∑ i in s, f i ^ p) ^ (1 / q)) =
      (∑ i in s, f i ^ p) ^ (1 / p)
[PROOFSTEP]
simp only [Set.mem_setOf_eq, div_rpow, ← sum_div, ← rpow_mul, div_mul_cancel _ hpq.symm.ne_zero, rpow_one,
  div_le_iff hf, one_mul, hpq.mul_eq_add, ← rpow_sub' _ A, _root_.add_sub_cancel, le_refl, true_and_iff, ←
  mul_div_assoc, B]
[GOAL]
case neg
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ¬∑ i in s, f i ^ p = 0
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i in s, f i ^ p) / (∑ i in s, f i ^ p) ^ (1 / q) = (∑ i in s, f i ^ p) ^ (1 / p)
[PROOFSTEP]
rw [div_eq_iff, ← rpow_add hf, hpq.inv_add_inv_conj, rpow_one]
[GOAL]
case neg
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
hf : ¬∑ i in s, f i ^ p = 0
A : p + q - q ≠ 0
B : ∀ (y : ℝ≥0), y * y ^ p / y = y ^ p
⊢ (∑ i in s, f i ^ p) ^ (1 / q) ≠ 0
[PROOFSTEP]
simpa [hpq.symm.ne_zero] using hf
[GOAL]
case right
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ (∑ i in s, f i ^ p) ^ (1 / p) ∈ upperBounds ((fun g => ∑ i in s, f i * g i) '' {g | ∑ i in s, g i ^ q ≤ 1})
[PROOFSTEP]
rintro _ ⟨g, hg, rfl⟩
[GOAL]
case right.intro.intro
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
g : ι → ℝ≥0
hg : g ∈ {g | ∑ i in s, g i ^ q ≤ 1}
⊢ (fun g => ∑ i in s, f i * g i) g ≤ (∑ i in s, f i ^ p) ^ (1 / p)
[PROOFSTEP]
apply le_trans (inner_le_Lp_mul_Lq s f g hpq)
[GOAL]
case right.intro.intro
ι : Type u
s : Finset ι
f : ι → ℝ≥0
p q : ℝ
hpq : Real.IsConjugateExponent p q
g : ι → ℝ≥0
hg : g ∈ {g | ∑ i in s, g i ^ q ≤ 1}
⊢ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q) ≤ (∑ i in s, f i ^ p) ^ (1 / p)
[PROOFSTEP]
simpa only [mul_one] using mul_le_mul_left' (NNReal.rpow_le_one hg (le_of_lt hpq.symm.one_div_pos)) _
[GOAL]
ι : 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)
[PROOFSTEP]
rcases eq_or_lt_of_le hp with (rfl | hp)
[GOAL]
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)
[PROOFSTEP]
simp [Finset.sum_add_distrib]
[GOAL]
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)
[PROOFSTEP]
have hpq := Real.isConjugateExponent_conjugateExponent hp
[GOAL]
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)
[PROOFSTEP]
have := isGreatest_Lp s (f + g) hpq
[GOAL]
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)
[PROOFSTEP]
simp only [Pi.add_apply, add_mul, sum_add_distrib] at this 
[GOAL]
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)
[PROOFSTEP]
rcases this.1 with ⟨φ, hφ, H⟩
[GOAL]
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)
[PROOFSTEP]
rw [← H]
[GOAL]
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)
[PROOFSTEP]
exact add_le_add ((isGreatest_Lp s f hpq).2 ⟨φ, hφ, rfl⟩) ((isGreatest_Lp s g hpq).2 ⟨φ, hφ, rfl⟩)
[GOAL]
ι : Type u
s : Finset ι
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)
[PROOFSTEP]
have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp
[GOAL]
ι : Type u
s : Finset ι
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)
[PROOFSTEP]
have H₁ : ∀ s : Finset ι, (∑ i in s, (f i + g i) ^ p) ≤ ((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p :=
  by
  intro s
  rw [← NNReal.rpow_one_div_le_iff pos]
  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 _) _
  exacts [hf, hg]
[GOAL]
ι : Type u
s : Finset ι
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 in s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
[PROOFSTEP]
intro s
[GOAL]
ι : Type u
s✝ : Finset ι
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 in s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
[PROOFSTEP]
rw [← NNReal.rpow_one_div_le_iff pos]
[GOAL]
ι : Type u
s✝ : Finset ι
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 in s, (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
[PROOFSTEP]
refine' le_trans (Lp_add_le s f g hp) (add_le_add _ _)
[GOAL]
case refine'_1
ι : Type u
s✝ : Finset ι
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 in s, f i ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p)
[PROOFSTEP]
rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr pos)]
[GOAL]
case refine'_2
ι : Type u
s✝ : Finset ι
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 in s, g i ^ p) ^ (1 / p) ≤ (∑' (i : ι), g i ^ p) ^ (1 / p)
[PROOFSTEP]
rw [NNReal.rpow_le_rpow_iff (one_div_pos.mpr pos)]
[GOAL]
case refine'_1
ι : Type u
s✝ : Finset ι
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 in s, f i ^ p ≤ ∑' (i : ι), f i ^ p
[PROOFSTEP]
refine' sum_le_tsum _ (fun _ _ => zero_le _) _
[GOAL]
case refine'_2
ι : Type u
s✝ : Finset ι
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 in s, g i ^ p ≤ ∑' (i : ι), g i ^ p
[PROOFSTEP]
refine' sum_le_tsum _ (fun _ _ => zero_le _) _
[GOAL]
case refine'_1
ι : Type u
s✝ : Finset ι
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
s✝ : Finset ι
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
[PROOFSTEP]
exacts [hf, hg]
[GOAL]
ι : Type u
s : Finset ι
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 in 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)
[PROOFSTEP]
have bdd : BddAbove (Set.range fun s => ∑ i in 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
[GOAL]
ι : Type u
s : Finset ι
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 in 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 in s, (f i + g i) ^ p)
[PROOFSTEP]
refine' ⟨((∑' i, f i ^ p) ^ (1 / p) + (∑' i, g i ^ p) ^ (1 / p)) ^ p, _⟩
[GOAL]
ι : Type u
s : Finset ι
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 in 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 in s, (f i + g i) ^ p)
[PROOFSTEP]
rintro a ⟨s, rfl⟩
[GOAL]
case intro
ι : Type u
s✝ : Finset ι
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 in s, (f i + g i) ^ p ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
s : Finset ι
⊢ (fun s => ∑ i in s, (f i + g i) ^ p) s ≤ ((∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)) ^ p
[PROOFSTEP]
exact H₁ s
[GOAL]
ι : Type u
s : Finset ι
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 in 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 in 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)
[PROOFSTEP]
have H₂ : Summable _ := (hasSum_of_isLUB _ (isLUB_ciSup bdd)).summable
[GOAL]
ι : Type u
s : Finset ι
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 in 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 in 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)
[PROOFSTEP]
refine' ⟨H₂, _⟩
[GOAL]
ι : Type u
s : Finset ι
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 in 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 in 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)
[PROOFSTEP]
rw [NNReal.rpow_one_div_le_iff pos]
[GOAL]
ι : Type u
s : Finset ι
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 in 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 in 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
[PROOFSTEP]
refine' tsum_le_of_sum_le H₂ H₁
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
⊢ ∃ C, C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p)
[PROOFSTEP]
have hp' : p ≠ 0 := (lt_of_lt_of_le zero_lt_one hp).ne'
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
⊢ ∃ C, C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p)
[PROOFSTEP]
obtain ⟨H₁, H₂⟩ := Lp_add_le_tsum hp hf.summable hg.summable
[GOAL]
case intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ ∃ C, C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p)
[PROOFSTEP]
have hA : A = (∑' i : ι, f i ^ p) ^ (1 / p) := by rw [hf.tsum_eq, rpow_inv_rpow_self hp']
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ A = (∑' (i : ι), f i ^ p) ^ (1 / p)
[PROOFSTEP]
rw [hf.tsum_eq, rpow_inv_rpow_self hp']
[GOAL]
case intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ ∃ C, C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p)
[PROOFSTEP]
have hB : B = (∑' i : ι, g i ^ p) ^ (1 / p) := by rw [hg.tsum_eq, rpow_inv_rpow_self hp']
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
⊢ B = (∑' (i : ι), g i ^ p) ^ (1 / p)
[PROOFSTEP]
rw [hg.tsum_eq, rpow_inv_rpow_self hp']
[GOAL]
case intro
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ ∃ C, C ≤ A + B ∧ HasSum (fun i => (f i + g i) ^ p) (C ^ p)
[PROOFSTEP]
refine' ⟨(∑' i, (f i + g i) ^ p) ^ (1 / p), _, _⟩
[GOAL]
case intro.refine'_1
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ A + B
[PROOFSTEP]
simpa [hA, hB] using H₂
[GOAL]
case intro.refine'_2
ι : Type u
s : Finset ι
f g : ι → ℝ≥0
A B : ℝ≥0
p : ℝ
hp : 1 ≤ p
hf : HasSum (fun i => f i ^ p) (A ^ p)
hg : HasSum (fun i => g i ^ p) (B ^ p)
hp' : p ≠ 0
H₁ : Summable fun i => (f i + g i) ^ p
H₂ : (∑' (i : ι), (f i + g i) ^ p) ^ (1 / p) ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
hA : A = (∑' (i : ι), f i ^ p) ^ (1 / p)
hB : B = (∑' (i : ι), g i ^ p) ^ (1 / p)
⊢ HasSum (fun i => (f i + g i) ^ p) (((∑' (i : ι), (f i + g i) ^ p) ^ (1 / p)) ^ p)
[PROOFSTEP]
simpa only [rpow_self_rpow_inv hp'] using H₁.hasSum
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, |f i| ^ p) ^ (1 / p) * (∑ i in s, |g i| ^ q) ^ (1 / q)
[PROOFSTEP]
have :=
  NNReal.coe_le_coe.2
    (NNReal.inner_le_Lp_mul_Lq s (fun i => ⟨_, abs_nonneg (f i)⟩) (fun i => ⟨_, abs_nonneg (g i)⟩) hpq)
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
this :
  ↑(∑ i in s,
        (fun i => { val := |f i|, property := (_ : 0 ≤ |f i|) }) i *
          (fun i => { val := |g i|, property := (_ : 0 ≤ |g i|) }) i) ≤
    ↑((∑ i in s, (fun i => { val := |f i|, property := (_ : 0 ≤ |f i|) }) i ^ p) ^ (1 / p) *
        (∑ i in s, (fun i => { val := |g i|, property := (_ : 0 ≤ |g i|) }) i ^ q) ^ (1 / q))
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, |f i| ^ p) ^ (1 / p) * (∑ i in s, |g i| ^ q) ^ (1 / q)
[PROOFSTEP]
push_cast at this 
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
this : ∑ x in s, |f x| * |g x| ≤ (∑ x in s, |f x| ^ p) ^ (1 / p) * (∑ x in s, |g x| ^ q) ^ (1 / q)
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, |f i| ^ p) ^ (1 / p) * (∑ i in s, |g i| ^ q) ^ (1 / q)
[PROOFSTEP]
refine' le_trans (sum_le_sum fun i _ => _) this
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
this : ∑ x in s, |f x| * |g x| ≤ (∑ x in s, |f x| ^ p) ^ (1 / p) * (∑ x in s, |g x| ^ q) ^ (1 / q)
i : ι
x✝ : i ∈ s
⊢ f i * g i ≤ |f i| * |g i|
[PROOFSTEP]
simp only [← abs_mul, le_abs_self]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, |f i|) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, |f i| ^ p
[PROOFSTEP]
have := NNReal.coe_le_coe.2 (NNReal.rpow_sum_le_const_mul_sum_rpow s (fun i => ⟨_, abs_nonneg (f i)⟩) hp)
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
this :
  ↑((∑ i in s, (fun i => { val := |f i|, property := (_ : 0 ≤ |f i|) }) i) ^ p) ≤
    ↑(↑(card s) ^ (p - 1) * ∑ i in s, (fun i => { val := |f i|, property := (_ : 0 ≤ |f i|) }) i ^ p)
⊢ (∑ i in s, |f i|) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, |f i| ^ p
[PROOFSTEP]
push_cast at this 
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
this : (∑ x in s, |f x|) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ x in s, |f x| ^ p
⊢ (∑ i in s, |f i|) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, |f i| ^ p
[PROOFSTEP]
exact this
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
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)
[PROOFSTEP]
have := NNReal.coe_le_coe.2 (NNReal.Lp_add_le s (fun i => ⟨_, abs_nonneg (f i)⟩) (fun i => ⟨_, abs_nonneg (g i)⟩) hp)
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
this :
  ↑((∑ i in s,
          ((fun i => { val := |f i|, property := (_ : 0 ≤ |f i|) }) i +
              (fun i => { val := |g i|, property := (_ : 0 ≤ |g i|) }) i) ^
            p) ^
        (1 / p)) ≤
    ↑((∑ i in s, (fun i => { val := |f i|, property := (_ : 0 ≤ |f i|) }) i ^ p) ^ (1 / p) +
        (∑ i in s, (fun i => { val := |g i|, property := (_ : 0 ≤ |g i|) }) 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)
[PROOFSTEP]
push_cast at this 
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
this : (∑ x in s, (|f x| + |g x|) ^ p) ^ (1 / p) ≤ (∑ x in s, |f x| ^ p) ^ (1 / p) + (∑ x in s, |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)
[PROOFSTEP]
refine' le_trans (rpow_le_rpow _ (sum_le_sum fun i _ => _) _) this
[GOAL]
case refine'_1
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
this : (∑ x in s, (|f x| + |g x|) ^ p) ^ (1 / p) ≤ (∑ x in s, |f x| ^ p) ^ (1 / p) + (∑ x in s, |g x| ^ p) ^ (1 / p)
⊢ 0 ≤ ∑ i in s, |f i + g i| ^ p
[PROOFSTEP]
simp [sum_nonneg, rpow_nonneg_of_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add, rpow_le_rpow]
[GOAL]
case refine'_2
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
this : (∑ x in s, (|f x| + |g x|) ^ p) ^ (1 / p) ≤ (∑ x in s, |f x| ^ p) ^ (1 / p) + (∑ x in s, |g x| ^ p) ^ (1 / p)
i : ι
x✝ : i ∈ s
⊢ |f i + g i| ^ p ≤ (|f i| + |g i|) ^ p
[PROOFSTEP]
simp [sum_nonneg, rpow_nonneg_of_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add, rpow_le_rpow]
[GOAL]
case refine'_3
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
this : (∑ x in s, (|f x| + |g x|) ^ p) ^ (1 / p) ≤ (∑ x in s, |f x| ^ p) ^ (1 / p) + (∑ x in s, |g x| ^ p) ^ (1 / p)
⊢ 0 ≤ 1 / p
[PROOFSTEP]
simp [sum_nonneg, rpow_nonneg_of_nonneg, abs_nonneg, le_trans zero_le_one hp, abs_add, rpow_le_rpow]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
convert inner_le_Lp_mul_Lq s f g hpq using 3
[GOAL]
case h.e'_4.h.e'_5.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∑ i in s, f i ^ p = ∑ i in s, |f i| ^ p
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case h.e'_4.h.e'_6.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∑ i in s, g i ^ q = ∑ i in s, |g i| ^ q
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case h.e'_4.h.e'_5.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∀ (x : ι), x ∈ s → f x ^ p = |f x| ^ p
[PROOFSTEP]
intro i hi
[GOAL]
case h.e'_4.h.e'_6.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∀ (x : ι), x ∈ s → g x ^ q = |g x| ^ q
[PROOFSTEP]
intro i hi
[GOAL]
case h.e'_4.h.e'_5.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i ^ p = |f i| ^ p
[PROOFSTEP]
simp only [abs_of_nonneg, hf i hi, hg i hi]
[GOAL]
case h.e'_4.h.e'_6.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
i : ι
hi : i ∈ s
⊢ g i ^ q = |g i| ^ q
[PROOFSTEP]
simp only [abs_of_nonneg, hf i hi, hg i hi]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable fun i => f i ^ p
hg_sum : Summable fun i => g i ^ q
⊢ (Summable fun i => f i * g i) ∧
    ∑' (i : ι), f i * g i ≤ (∑' (i : ι), f i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
[PROOFSTEP]
lift f to ι → ℝ≥0 using hf
[GOAL]
case intro
ι : Type u
s : Finset ι
g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : Summable fun i => g i ^ q
f : ι → ℝ≥0
hf_sum : Summable fun i => (fun i => ↑(f i)) i ^ p
⊢ (Summable fun i => (fun i => ↑(f i)) i * g i) ∧
    ∑' (i : ι), (fun i => ↑(f i)) i * g i ≤
      (∑' (i : ι), (fun i => ↑(f i)) i ^ p) ^ (1 / p) * (∑' (i : ι), g i ^ q) ^ (1 / q)
[PROOFSTEP]
lift g to ι → ℝ≥0 using hg
[GOAL]
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f : ι → ℝ≥0
hf_sum : Summable fun i => (fun i => ↑(f i)) i ^ p
g : ι → ℝ≥0
hg_sum : Summable fun i => (fun i => ↑(g i)) i ^ q
⊢ (Summable fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) ∧
    ∑' (i : ι), (fun i => ↑(f i)) i * (fun i => ↑(g i)) i ≤
      (∑' (i : ι), (fun i => ↑(f i)) i ^ p) ^ (1 / p) * (∑' (i : ι), (fun i => ↑(g i)) i ^ q) ^ (1 / q)
[PROOFSTEP]
norm_cast at *
[GOAL]
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
hf_sum : Summable fun a => f a ^ p
hg_sum : Summable fun a => g a ^ q
⊢ (Summable fun a => f a * g a) ∧
    ∑' (a : ι), f a * g a ≤ (∑' (a : ι), f a ^ p) ^ (1 / p) * (∑' (a : ι), g a ^ q) ^ (1 / q)
[PROOFSTEP]
exact NNReal.inner_le_Lp_mul_Lq_tsum hpq hf_sum hg_sum
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : HasSum (fun i => f i ^ p) (A ^ p)
hg_sum : HasSum (fun i => g i ^ q) (B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i => f i * g i) C
[PROOFSTEP]
lift f to ι → ℝ≥0 using hf
[GOAL]
case intro
ι : Type u
s : Finset ι
g : ι → ℝ
p q : ℝ
hpq : IsConjugateExponent p q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : HasSum (fun i => g i ^ q) (B ^ q)
f : ι → ℝ≥0
hf_sum : 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) C
[PROOFSTEP]
lift g to ι → ℝ≥0 using hg
[GOAL]
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
A B : ℝ
hA : 0 ≤ A
hB : 0 ≤ B
f : ι → ℝ≥0
hf_sum : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (A ^ p)
g : ι → ℝ≥0
hg_sum : HasSum (fun i => (fun i => ↑(g i)) i ^ q) (B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ A * B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
[PROOFSTEP]
lift A to ℝ≥0 using hA
[GOAL]
case intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
B : ℝ
hB : 0 ≤ B
f g : ι → ℝ≥0
hg_sum : HasSum (fun i => (fun i => ↑(g i)) i ^ q) (B ^ q)
A : ℝ≥0
hf_sum : 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) C
[PROOFSTEP]
lift B to ℝ≥0 using hB
[GOAL]
case intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
A : ℝ≥0
hf_sum : HasSum (fun i => (fun i => ↑(f i)) i ^ p) (↑A ^ p)
B : ℝ≥0
hg_sum : HasSum (fun i => (fun i => ↑(g i)) i ^ q) (↑B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
[PROOFSTEP]
norm_cast at hf_sum hg_sum 
[GOAL]
case intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun a => f a ^ p) (A ^ p)
hg_sum : HasSum (fun a => g a ^ q) (B ^ q)
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
[PROOFSTEP]
obtain ⟨C, hC, H⟩ := NNReal.inner_le_Lp_mul_Lq_hasSum hpq hf_sum hg_sum
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun a => f a ^ p) (A ^ p)
hg_sum : HasSum (fun a => g a ^ q) (B ^ q)
C : ℝ≥0
hC : C ≤ A * B
H : HasSum (fun i => f i * g i) C
⊢ ∃ C, 0 ≤ C ∧ C ≤ ↑A * ↑B ∧ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) C
[PROOFSTEP]
refine' ⟨C, C.prop, hC, _⟩
[GOAL]
case intro.intro.intro.intro.intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hpq : IsConjugateExponent p q
f g : ι → ℝ≥0
A B : ℝ≥0
hf_sum : HasSum (fun a => f a ^ p) (A ^ p)
hg_sum : HasSum (fun a => g a ^ q) (B ^ q)
C : ℝ≥0
hC : C ≤ A * B
H : HasSum (fun i => f i * g i) C
⊢ HasSum (fun i => (fun i => ↑(f i)) i * (fun i => ↑(g i)) i) ↑C
[PROOFSTEP]
norm_cast
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
convert rpow_sum_le_const_mul_sum_rpow s f hp using 2
[GOAL]
case h.e'_3.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
⊢ ∑ i in s, f i = ∑ i in s, |f i|
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case h.e'_4.h.e'_6
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
⊢ ∑ i in s, f i ^ p = ∑ i in s, |f i| ^ p
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case h.e'_3.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
⊢ ∀ (x : ι), x ∈ s → f x = |f x|
[PROOFSTEP]
intro i hi
[GOAL]
case h.e'_4.h.e'_6
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
⊢ ∀ (x : ι), x ∈ s → f x ^ p = |f x| ^ p
[PROOFSTEP]
intro i hi
[GOAL]
case h.e'_3.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i = |f i|
[PROOFSTEP]
simp only [abs_of_nonneg, hf i hi]
[GOAL]
case h.e'_4.h.e'_6
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
i : ι
hi : i ∈ s
⊢ f i ^ p = |f i| ^ p
[PROOFSTEP]
simp only [abs_of_nonneg, hf i hi]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ (∑ 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)
[PROOFSTEP]
convert Lp_add_le s f g hp using 2 <;> [skip; congr 1; congr 1]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ (∑ 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)
[PROOFSTEP]
convert Lp_add_le s f g hp using 2
[GOAL]
case h.e'_3.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∑ i in s, (f i + g i) ^ p = ∑ i in s, |f i + g i| ^ p
[PROOFSTEP]
skip
[GOAL]
case h.e'_4.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ (∑ i in s, f i ^ p) ^ (1 / p) = (∑ i in s, |f i| ^ p) ^ (1 / p)
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_4.h.e'_6
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ (∑ i in s, g i ^ p) ^ (1 / p) = (∑ i in s, |g i| ^ p) ^ (1 / p)
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_3.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∑ i in s, (f i + g i) ^ p = ∑ i in s, |f i + g i| ^ p
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case h.e'_4.h.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∑ i in s, f i ^ p = ∑ i in s, |f i| ^ p
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case h.e'_4.h.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∑ i in s, g i ^ p = ∑ i in s, |g i| ^ p
[PROOFSTEP]
apply sum_congr rfl
[GOAL]
case h.e'_3.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∀ (x : ι), x ∈ s → (f x + g x) ^ p = |f x + g x| ^ p
[PROOFSTEP]
intro i hi
[GOAL]
case h.e'_4.h.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∀ (x : ι), x ∈ s → f x ^ p = |f x| ^ p
[PROOFSTEP]
intro i hi
[GOAL]
case h.e'_4.h.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
⊢ ∀ (x : ι), x ∈ s → g x ^ p = |g x| ^ p
[PROOFSTEP]
intro i hi
[GOAL]
case h.e'_3.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
i : ι
hi : i ∈ s
⊢ (f i + g i) ^ p = |f i + g i| ^ p
[PROOFSTEP]
simp only [abs_of_nonneg, hf i hi, hg i hi, add_nonneg]
[GOAL]
case h.e'_4.h.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
i : ι
hi : i ∈ s
⊢ f i ^ p = |f i| ^ p
[PROOFSTEP]
simp only [abs_of_nonneg, hf i hi, hg i hi, add_nonneg]
[GOAL]
case h.e'_4.h.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), i ∈ s → 0 ≤ f i
hg : ∀ (i : ι), i ∈ s → 0 ≤ g i
i : ι
hi : i ∈ s
⊢ g i ^ p = |g i| ^ p
[PROOFSTEP]
simp only [abs_of_nonneg, hf i hi, hg i hi, add_nonneg]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hf : ∀ (i : ι), 0 ≤ f i
hg : ∀ (i : ι), 0 ≤ g i
hf_sum : Summable fun i => f i ^ p
hg_sum : 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)
[PROOFSTEP]
lift f to ι → ℝ≥0 using hf
[GOAL]
case intro
ι : Type u
s : Finset ι
g : ι → ℝ
p q : ℝ
hp : 1 ≤ p
hg : ∀ (i : ι), 0 ≤ g i
hg_sum : Summable fun i => g i ^ p
f : ι → ℝ≥0
hf_sum : Summable fun i => (fun i => ↑(f i)) i ^ p
⊢ (Summable fun i => ((fun i => ↑(f i)) i + g i) ^ p) ∧
    (∑' (i : ι), ((fun i => ↑(f i)) i + g i) ^ p) ^ (1 / p) ≤
      (∑' (i : ι), (fun i => ↑(f i)) i ^ p) ^ (1 / p) + (∑' (i : ι), g i ^ p) ^ (1 / p)
[PROOFSTEP]
lift g to ι → ℝ≥0 using hg
[GOAL]
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
hp : 1 ≤ p
f : ι → ℝ≥0
hf_sum : Summable fun i => (fun i => ↑(f i)) i ^ p
g : ι → ℝ≥0
hg_sum : Summable fun i => (fun i => ↑(g i)) i ^ p
⊢ (Summable fun i => ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) ∧
    (∑' (i : ι), ((fun i => ↑(f i)) i + (fun i => ↑(g i)) i) ^ p) ^ (1 / p) ≤
      (∑' (i : ι), (fun i => ↑(f i)) i ^ p) ^ (1 / p) + (∑' (i : ι), (fun i => ↑(g i)) i ^ p) ^ (1 / p)
[PROOFSTEP]
norm_cast0 at *
[GOAL]
case intro.intro
ι : Type u
s : Finset ι
p q : ℝ
f g : ι → ℝ≥0
hp : 1 ≤ p
hf_sum : Summable fun a => f a ^ p
hg_sum : Summable fun a => g a ^ p
⊢ (Summable fun a => (f a + g a) ^ p) ∧
    (∑' (a : ι), (f a + g a) ^ p) ^ (1 / p) ≤ (∑' (a : ι), f a ^ p) ^ (1 / p) + (∑' (a : ι), g a ^ p) ^ (1 / p)
[PROOFSTEP]
exact NNReal.Lp_add_le_tsum hp hf_sum hg_sum
[GOAL]
ι : 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)
[PROOFSTEP]
lift f to ι → ℝ≥0 using hf
[GOAL]
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)
[PROOFSTEP]
lift g to ι → ℝ≥0 using hg
[GOAL]
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)
[PROOFSTEP]
lift A to ℝ≥0 using hA
[GOAL]
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)
[PROOFSTEP]
lift B to ℝ≥0 using hB
[GOAL]
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)
[PROOFSTEP]
norm_cast at hfA hgB 
[GOAL]
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)
[PROOFSTEP]
obtain ⟨C, hC₁, hC₂⟩ := NNReal.Lp_add_le_hasSum hp hfA hgB
[GOAL]
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)
[PROOFSTEP]
use C
[GOAL]
case h
ι : 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)
[PROOFSTEP]
norm_cast
[GOAL]
case h
ι : 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)
[PROOFSTEP]
exact ⟨zero_le _, hC₁, hC₂⟩
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
by_cases H : (∑ i in s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i in s, g i ^ q) ^ (1 / q) = 0
[GOAL]
case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i in s, g i ^ q) ^ (1 / q) = 0
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
replace H : (∀ i ∈ s, f i = 0) ∨ ∀ i ∈ s, g i = 0
[GOAL]
case H
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i in s, g i ^ q) ^ (1 / q) = 0
⊢ (∀ (i : ι), i ∈ s → f i = 0) ∨ ∀ (i : ι), i ∈ s → g i = 0
[PROOFSTEP]
simpa [ENNReal.rpow_eq_zero_iff, hpq.pos, hpq.symm.pos, asymm hpq.pos, asymm hpq.symm.pos,
  sum_eq_zero_iff_of_nonneg] using H
[GOAL]
case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∀ (i : ι), i ∈ s → f i = 0) ∨ ∀ (i : ι), i ∈ s → g i = 0
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
have : ∀ i ∈ s, f i * g i = 0 := fun i hi => by cases' H with H H <;> simp [H i hi]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∀ (i : ι), i ∈ s → f i = 0) ∨ ∀ (i : ι), i ∈ s → g i = 0
i : ι
hi : i ∈ s
⊢ f i * g i = 0
[PROOFSTEP]
cases' H with H H
[GOAL]
case inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
i : ι
hi : i ∈ s
H : ∀ (i : ι), i ∈ s → f i = 0
⊢ f i * g i = 0
[PROOFSTEP]
simp [H i hi]
[GOAL]
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
i : ι
hi : i ∈ s
H : ∀ (i : ι), i ∈ s → g i = 0
⊢ f i * g i = 0
[PROOFSTEP]
simp [H i hi]
[GOAL]
case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∀ (i : ι), i ∈ s → f i = 0) ∨ ∀ (i : ι), i ∈ s → g i = 0
this : ∀ (i : ι), i ∈ s → f i * g i = 0
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
have : ∑ i in s, f i * g i = ∑ i in s, 0 := sum_congr rfl this
[GOAL]
case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∀ (i : ι), i ∈ s → f i = 0) ∨ ∀ (i : ι), i ∈ s → g i = 0
this✝ : ∀ (i : ι), i ∈ s → f i * g i = 0
this : ∑ i in s, f i * g i = ∑ i in s, 0
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
simp [this]
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : ¬((∑ i in s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i in s, g i ^ q) ^ (1 / q) = 0)
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
push_neg at H 
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
by_cases H' : (∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ q) ^ (1 / q) = ⊤
[GOAL]
case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ q) ^ (1 / q) = ⊤
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
cases' H' with H' H'
[GOAL]
case pos.inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∑ i in s, f i ^ p) ^ (1 / p) = ⊤
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
simp [H', -one_div, -sum_eq_zero_iff, -rpow_eq_zero_iff, H]
[GOAL]
case pos.inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∑ i in s, g i ^ q) ^ (1 / q) = ⊤
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
simp [H', -one_div, -sum_eq_zero_iff, -rpow_eq_zero_iff, H]
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : ¬((∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ q) ^ (1 / q) = ⊤)
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤
[GOAL]
case H'
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : ¬((∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ q) ^ (1 / q) = ⊤)
⊢ (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
[PROOFSTEP]
simpa [ENNReal.rpow_eq_top_iff, asymm hpq.pos, asymm hpq.symm.pos, hpq.pos, hpq.symm.pos, ENNReal.sum_eq_top_iff,
  not_or] using H'
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
have :=
  ENNReal.coe_le_coe.2
    (@NNReal.inner_le_Lp_mul_Lq _ s (fun i => ENNReal.toNNReal (f i)) (fun i => ENNReal.toNNReal (g i)) _ _ hpq)
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ↑(∑ i in s, (fun i => ENNReal.toNNReal (f i)) i * (fun i => ENNReal.toNNReal (g i)) i) ≤
    ↑((∑ i in s, (fun i => ENNReal.toNNReal (f i)) i ^ p) ^ (1 / p) *
        (∑ i in s, (fun i => ENNReal.toNNReal (g i)) i ^ q) ^ (1 / q))
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
simp [← ENNReal.coe_rpow_of_nonneg, le_of_lt hpq.pos, le_of_lt hpq.one_div_pos, le_of_lt hpq.symm.pos,
  le_of_lt hpq.symm.one_div_pos] at this 
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
convert this using 1 <;> [skip; congr 2] <;> [skip; skip; simp; skip; simp]
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
convert this using 1 <;> [skip; congr 2]
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ ∑ i in s, f i * g i ≤ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q)
[PROOFSTEP]
convert this using 1
[GOAL]
case h.e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ ∑ i in s, f i * g i = ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x))
[PROOFSTEP]
skip
[GOAL]
case h.e'_4
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ (∑ i in s, f i ^ p) ^ (1 / p) * (∑ i in s, g i ^ q) ^ (1 / q) =
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
[PROOFSTEP]
congr 2
[GOAL]
case h.e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ ∑ i in s, f i * g i = ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x))
[PROOFSTEP]
skip
[GOAL]
case h.e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ ∑ i in s, f i ^ p = ∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p
[PROOFSTEP]
skip
[GOAL]
case h.e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ 1 / p = p⁻¹
[PROOFSTEP]
simp
[GOAL]
case h.e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ ∑ i in s, g i ^ q = ∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q
[PROOFSTEP]
skip
[GOAL]
case h.e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ 1 / q = q⁻¹
[PROOFSTEP]
simp
[GOAL]
case h.e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ ∑ i in s, f i * g i = ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x))
[PROOFSTEP]
refine Finset.sum_congr rfl fun i hi => ?_
[GOAL]
case h.e'_3
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
i : ι
hi : i ∈ s
⊢ f i * g i = ↑(ENNReal.toNNReal (f i)) * ↑(ENNReal.toNNReal (g i))
[PROOFSTEP]
simp [H'.1 i hi, H'.2 i hi, -WithZero.coe_mul, WithTop.coe_mul.symm]
[GOAL]
case h.e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ ∑ i in s, f i ^ p = ∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p
[PROOFSTEP]
refine Finset.sum_congr rfl fun i hi => ?_
[GOAL]
case h.e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
i : ι
hi : i ∈ s
⊢ f i ^ p = ↑(ENNReal.toNNReal (f i)) ^ p
[PROOFSTEP]
simp [H'.1 i hi, H'.2 i hi, -WithZero.coe_mul, WithTop.coe_mul.symm]
[GOAL]
case h.e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
⊢ ∑ i in s, g i ^ q = ∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q
[PROOFSTEP]
refine Finset.sum_congr rfl fun i hi => ?_
[GOAL]
case h.e'_4.e_a.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hpq : Real.IsConjugateExponent p q
H : (∑ i in s, f i ^ p) ^ (1 / p) ≠ 0 ∧ (∑ i in s, g i ^ q) ^ (1 / q) ≠ 0
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ∑ x in s, ↑(ENNReal.toNNReal (f x)) * ↑(ENNReal.toNNReal (g x)) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ p⁻¹ * (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ q) ^ q⁻¹
i : ι
hi : i ∈ s
⊢ g i ^ q = ↑(ENNReal.toNNReal (g i)) ^ q
[PROOFSTEP]
simp [H'.1 i hi, H'.2 i hi, -WithZero.coe_mul, WithTop.coe_mul.symm]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
cases' eq_or_lt_of_le hp with hp hp
[GOAL]
case inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp✝ : 1 ≤ p
hp : 1 = p
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
simp [← hp]
[GOAL]
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
let q : ℝ := p / (p - 1)
[GOAL]
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q✝ : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
have hpq : p.IsConjugateExponent q := by rw [Real.isConjugateExponent_iff hp]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q✝ : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
⊢ Real.IsConjugateExponent p q
[PROOFSTEP]
rw [Real.isConjugateExponent_iff hp]
[GOAL]
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q✝ : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
have hp₁ : 1 / p * p = 1 := one_div_mul_cancel hpq.ne_zero
[GOAL]
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q✝ : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
have hq : 1 / q * p = p - 1 := by
  rw [← hpq.div_conj_eq_sub_one]
  ring
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q✝ : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
⊢ 1 / q * p = p - 1
[PROOFSTEP]
rw [← hpq.div_conj_eq_sub_one]
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q✝ : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
⊢ 1 / q * p = p / q
[PROOFSTEP]
ring
[GOAL]
case inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q✝ : ℝ
hp✝ : 1 ≤ p
hp : 1 < p
q : ℝ := p / (p - 1)
hpq : Real.IsConjugateExponent p q
hp₁ : 1 / p * p = 1
hq : 1 / q * p = p - 1
⊢ (∑ i in s, f i) ^ p ≤ ↑(card s) ^ (p - 1) * ∑ i in s, f i ^ p
[PROOFSTEP]
simpa only [ENNReal.mul_rpow_of_nonneg _ _ hpq.nonneg, ← ENNReal.rpow_mul, hp₁, hq, coe_one, one_mul, one_rpow,
  rpow_one, Pi.one_apply, sum_const, Nat.smul_one_eq_coe] using
  ENNReal.rpow_le_rpow (inner_le_Lp_mul_Lq s 1 f hpq.symm) hpq.nonneg
[GOAL]
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
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)
[PROOFSTEP]
by_cases H' : (∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ p) ^ (1 / p) = ⊤
[GOAL]
case pos
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : (∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, 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)
[PROOFSTEP]
cases' H' with H' H'
[GOAL]
case pos.inl
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : (∑ i in s, f 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)
[PROOFSTEP]
simp [H', -one_div]
[GOAL]
case pos.inr
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : (∑ i in s, 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)
[PROOFSTEP]
simp [H', -one_div]
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : ¬((∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, 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)
[PROOFSTEP]
have pos : 0 < p := lt_of_lt_of_le zero_lt_one hp
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : ¬((∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ p) ^ (1 / p) = ⊤)
pos : 0 < 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)
[PROOFSTEP]
replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤
[GOAL]
case H'
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
H' : ¬((∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ p) ^ (1 / p) = ⊤)
pos : 0 < p
⊢ (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
[PROOFSTEP]
simpa [ENNReal.rpow_eq_top_iff, asymm pos, pos, ENNReal.sum_eq_top_iff, not_or] using H'
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
⊢ (∑ 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)
[PROOFSTEP]
have :=
  ENNReal.coe_le_coe.2 (@NNReal.Lp_add_le _ s (fun i => ENNReal.toNNReal (f i)) (fun i => ENNReal.toNNReal (g i)) _ hp)
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  ↑((∑ i in s, ((fun i => ENNReal.toNNReal (f i)) i + (fun i => ENNReal.toNNReal (g i)) i) ^ p) ^ (1 / p)) ≤
    ↑((∑ i in s, (fun i => ENNReal.toNNReal (f i)) i ^ p) ^ (1 / p) +
        (∑ i in s, (fun i => ENNReal.toNNReal (g i)) 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)
[PROOFSTEP]
push_cast [← ENNReal.coe_rpow_of_nonneg, le_of_lt pos, le_of_lt (one_div_pos.2 pos)] at this 
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (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)
[PROOFSTEP]
convert this using 2 <;> [skip; congr 1; congr 1]
[GOAL]
case neg
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (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)
[PROOFSTEP]
convert this using 2
[GOAL]
case h.e'_3.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
⊢ ∑ i in s, (f i + g i) ^ p = ∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p
[PROOFSTEP]
skip
[GOAL]
case h.e'_4.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
⊢ (∑ i in s, f i ^ p) ^ (1 / p) = (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p)
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_4.h.e'_6
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
⊢ (∑ i in s, g i ^ p) ^ (1 / p) = (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
[PROOFSTEP]
congr 1
[GOAL]
case h.e'_3.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
⊢ ∑ i in s, (f i + g i) ^ p = ∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p
[PROOFSTEP]
refine Finset.sum_congr rfl fun i hi => ?_
[GOAL]
case h.e'_3.h.e'_5
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
i : ι
hi : i ∈ s
⊢ (f i + g i) ^ p = (↑(ENNReal.toNNReal (f i)) + ↑(ENNReal.toNNReal (g i))) ^ p
[PROOFSTEP]
simp [H'.1 i hi, H'.2 i hi]
[GOAL]
case h.e'_4.h.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
⊢ ∑ i in s, f i ^ p = ∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p
[PROOFSTEP]
refine Finset.sum_congr rfl fun i hi => ?_
[GOAL]
case h.e'_4.h.e'_5.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
i : ι
hi : i ∈ s
⊢ f i ^ p = ↑(ENNReal.toNNReal (f i)) ^ p
[PROOFSTEP]
simp [H'.1 i hi, H'.2 i hi]
[GOAL]
case h.e'_4.h.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
⊢ ∑ i in s, g i ^ p = ∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p
[PROOFSTEP]
refine Finset.sum_congr rfl fun i hi => ?_
[GOAL]
case h.e'_4.h.e'_6.e_a
ι : Type u
s : Finset ι
f g : ι → ℝ≥0∞
p q : ℝ
hp : 1 ≤ p
pos : 0 < p
H' : (∀ (i : ι), i ∈ s → f i ≠ ⊤) ∧ ∀ (i : ι), i ∈ s → g i ≠ ⊤
this :
  (∑ x in s, (↑(ENNReal.toNNReal (f x)) + ↑(ENNReal.toNNReal (g x))) ^ p) ^ (1 / p) ≤
    (∑ x in s, ↑(ENNReal.toNNReal (f x)) ^ p) ^ (1 / p) + (∑ x in s, ↑(ENNReal.toNNReal (g x)) ^ p) ^ (1 / p)
i : ι
hi : i ∈ s
⊢ g i ^ p = ↑(ENNReal.toNNReal (g i)) ^ p
[PROOFSTEP]
simp [H'.1 i hi, H'.2 i hi]
