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)

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)
ι : 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)
by_cases hF_zero : (∑ i in s, f i ^ p) = 0
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)

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)
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)
by_cases hG_zero : (∑ i in s, g i ^ q) = 0
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)
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)
let f' i := f i / (∑ i in s, f i ^ p) ^ (1 / p)
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)
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)
let g' i := g i / (∑ i in s, g i ^ q) ^ (1 / q)
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

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
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
refine' inner_le_Lp_mul_Lp_of_norm_le_one s f' g' hpq (le_of_eq _) (le_of_eq _)
no goals
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)
exact inner_le_Lp_mul_Lp_of_norm_eq_zero s f g hpq hF_zero
no goals
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)
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 _ _
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)
ι : 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
congr with i
no goals
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)
rw [mul_comm]
ι : 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)
ι : 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)
simp_rw [div_mul_div_comm, ← sum_div] at this
ι : 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
ι : 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)
rwa [div_le_iff, one_mul] at this
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

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
ι : 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
refine' mul_ne_zero _ _
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
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
rw [Ne.def, rpow_eq_zero_iff, not_and_or]
no goals
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
exact Or.inl hF_zero
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
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
rw [Ne.def, rpow_eq_zero_iff, not_and_or]
no goals
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
exact Or.inl hG_zero
no goals
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
simp_rw [div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel hpq.ne_zero, rpow_one,
  div_self hF_zero]
no goals
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
simp_rw [div_rpow, ← sum_div, ← rpow_mul, one_div, inv_mul_cancel hpq.symm.ne_zero,
  rpow_one, div_self hG_zero]