ι : 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
ι : 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)
simp only [hf, hpq.ne_zero, one_div, sum_eq_zero_iff, zero_rpow, MulZeroClass.zero_mul,
  inv_eq_zero, Ne.def, not_false_iff, le_zero_iff, mul_eq_zero]
ι : 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
ι : 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
intro i his
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
ι : 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
left
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
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
rw [sum_eq_zero_iff] at hf
no goals
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
exact (rpow_eq_zero_iff.mp (hf i his)).left