-- Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
/-- **Cauchy-Schwarz inequality** for finsets.

This is written in terms of sequences `f`, `g`, and `r`, where `r` is a stand-in for
`√(f i * g i)`. See `sum_mul_sq_le_sq_mul_sq` for the more usual form in terms of squared
sequences. -/
lemma sum_sq_le_sum_mul_sum_of_sq_eq_mul [LinearOrderedCommSemiring R] [ExistsAddOfLE R]
    (s : Finset ι) {r f g : ι → R} (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 ≤ g i)
    (ht : ∀ i ∈ s, r i ^ 2 = f i * g i) : (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Proof state:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
obtain h | h := (sum_nonneg hg).eq_or_gt

Result:
case inl
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : ∑ i ∈ s, g i = 0
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

case inr
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Proof state:
case inl
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : ∑ i ∈ s, g i = 0
ht' : ∑ i ∈ s, r i = 0
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
rw [h, ht']

Result:
case inl
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : ∑ i ∈ s, g i = 0
ht' : ∑ i ∈ s, r i = 0
⊢ 0 ^ 2 ≤ (∑ i ∈ s, f i) * 0

Proof state:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 =
    2 * ((∑ i ∈ s, r i) * ((∑ i ∈ s, g i) * ∑ i ∈ s, r i))

Tactic:
ring

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 =
    ∑ i ∈ s, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j

Tactic:
simp_rw [mul_assoc, ← mul_sum, ← sum_mul]

Result:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 =
    2 * ((∑ i ∈ s, r i) * ((∑ i ∈ s, g i) * ∑ i ∈ s, r i))

Proof state:
case inl
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : ∑ i ∈ s, g i = 0
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
have ht' : ∑ i ∈ s, r i = 0 := sum_eq_zero fun i hi ↦ by
  simpa [(sum_eq_zero_iff_of_nonneg hg).1 h i hi] using ht i hi

Result:
case inl
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : ∑ i ∈ s, g i = 0
ht' : ∑ i ∈ s, r i = 0
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Proof state:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
⊢ ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 = r i ^ 2 * ((∑ j ∈ s, g j) ^ 2 * (∑ j ∈ s, r j) ^ 2)

Tactic:
ring

Result:
no goals

Proof state:
case inr
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, r i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i

Tactic:
refine le_of_mul_le_mul_of_pos_left
  (le_of_add_le_add_left (a := (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2) ?_) h

Result:
case inr
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : 0 < ∑ i ∈ s, g i
⊢ (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 ≤
    (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * ((∑ i ∈ s, f i) * ∑ i ∈ s, g i)

Proof state:
case inl
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht : ∀ i ∈ s, r i ^ 2 = f i * g i
h : ∑ i ∈ s, g i = 0
ht' : ∑ i ∈ s, r i = 0
⊢ 0 ^ 2 ≤ (∑ i ∈ s, f i) * 0

Tactic:
simp

Result:
no goals

Proof state:
case h
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedCommSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
r f g : ι → R
hf : ∀ i ∈ s, 0 ≤ f i
hg : ∀ i ∈ s, 0 ≤ g i
ht✝ : ∀ i ∈ s, r i ^ 2 = f i * g i
h : 0 < ∑ i ∈ s, g i
i : ι
hi : i ∈ s
ht : ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j) ^ 2 = f i * (∑ j ∈ s, g j) ^ 2 * (g i * (∑ j ∈ s, r j) ^ 2)
⊢ (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j = 2 * ((r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j)

Tactic:
repeat rw [mul_assoc]

Result:
no goals