-- 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:
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 ≤ f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2

Tactic:
refine le_of_eq_of_le ?_ (two_mul_le_add_of_sq_eq_mul
  (mul_nonneg (hf i hi) (sq_nonneg _)) (mul_nonneg (hg i hi) (sq_nonneg _)) ht)

Result:
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)

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, (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j ≤ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2)

Tactic:
gcongr with i hi

Result:
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
⊢ (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j ≤ f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2

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, f i) * (∑ j ∈ s, g j) ^ 2 + (∑ j ∈ s, g j) * (∑ j ∈ s, r j) ^ 2 =
    (∑ j ∈ s, g j) * (∑ j ∈ s, r j) ^ 2 + (∑ j ∈ s, g j) * ((∑ i ∈ s, f i) * ∑ j ∈ s, g j)

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 : ι
hi : i ∈ s
⊢ ((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)

Tactic:
conv_rhs => rw [mul_mul_mul_comm, ← ht i hi]

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 : ι
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)

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
⊢ (2 * r i * ∑ j ∈ s, g j) * ∑ j ∈ s, r j ≤ f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2

Tactic:
have 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) := by
  conv_rhs => rw [mul_mul_mul_comm, ← ht i hi]
  ring

Result:
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 ≤ f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2

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, 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)

Tactic:
calc
  _ = ∑ i ∈ s, 2 * r i * (∑ j ∈ s, g j) * (∑ j ∈ s, r j) := by
      simp_rw [mul_assoc, ← mul_sum, ← sum_mul]; ring
  _ ≤ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) := by
      gcongr with i hi
      have 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) := by
        conv_rhs => rw [mul_mul_mul_comm, ← ht i hi]
        ring
      refine le_of_eq_of_le ?_ (two_mul_le_add_of_sq_eq_mul
        (mul_nonneg (hf i hi) (sq_nonneg _)) (mul_nonneg (hg i hi) (sq_nonneg _)) ht)
      repeat rw [mul_assoc]
  _ = _ := by simp_rw [sum_add_distrib, ← sum_mul]; 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, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, r j) ^ 2) =
    (∑ i ∈ s, g i) * (∑ i ∈ s, r i) ^ 2 + (∑ i ∈ s, g i) * ((∑ i ∈ s, f i) * ∑ i ∈ s, g i)

Tactic:
simp_rw [sum_add_distrib, ← 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, f i) * (∑ j ∈ s, g j) ^ 2 + (∑ j ∈ s, g j) * (∑ j ∈ s, r j) ^ 2 =
    (∑ j ∈ s, g j) * (∑ j ∈ s, r j) ^ 2 + (∑ j ∈ s, g j) * ((∑ i ∈ s, f i) * ∑ j ∈ s, g j)

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 : ∑ i ∈ s, g i = 0
i : ι
hi : i ∈ s
⊢ r i = 0

Tactic:
simpa [(sum_eq_zero_iff_of_nonneg hg).1 h i hi] using ht i hi

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:
rw [mul_assoc]

Result:
no goals