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)

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)
ι : 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 H : (∑ i in s, f i ^ p) ^ (1 / p) = 0 ∨ (∑ i in s, g i ^ q) ^ (1 / q) = 0
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)
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)
push_neg at H
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)

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)
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)
by_cases H' : (∑ i in s, f i ^ p) ^ (1 / p) = ⊤ ∨ (∑ i in s, g i ^ q) ^ (1 / q) = ⊤
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 ≠ ⊤

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)
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)
replace H' : (∀ i ∈ s, f i ≠ ⊤) ∧ ∀ i ∈ s, g i ≠ ⊤
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)
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)
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)
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)
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)
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
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

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)
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)
replace H : (∀ i ∈ s, f i = 0) ∨ ∀ i ∈ s, g i = 0
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)
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)
have : ∀ i ∈ s, f i * g i = 0 := fun i hi => by cases' H with H H <;> simp [H i hi]
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)
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)
have : (∑ i in s, f i * g i) = ∑ i in s, 0 := sum_congr rfl this
no goals
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)
simp [this]
no goals
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
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
no goals
ι : 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
cases' H with H H <;> simp [H i hi]
no goals
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)
cases' H' with H' H' <;> simp [H', -one_div, -sum_eq_zero_iff, -rpow_eq_zero_iff, H]
no goals
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 ≠ ⊤
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'
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
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
refine Finset.sum_congr rfl fun i hi => ?_
no goals
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
simp [H'.1 i hi, H'.2 i hi, -WithZero.coe_mul, WithTop.coe_mul.symm]