[Merged by Bors] - feat: Sedrakyan's lemma

Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean

@@ -124,26 +124,57 @@ end OrderedCommSemiring
 section LinearOrderedCommSemiring
 variable [LinearOrderedCommSemiring R] [ExistsAddOfLE R]
 
-/-- **Cauchy-Schwarz inequality** for finsets. -/
-lemma sum_mul_sq_le_sq_mul_sq (s : Finset ι) (f g : ι → R) :
-    (∑ i ∈ s, f i * g i) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) * ∑ i ∈ s, g i ^ 2 := by
-  nontriviality R
-  obtain h' | h' := (sum_nonneg fun _ _ ↦ sq_nonneg <| g _).eq_or_lt
-  · have h'' : ∀ i ∈ s, g i = 0 := fun i hi ↦ by
-      simpa using (sum_eq_zero_iff_of_nonneg fun i _ ↦ sq_nonneg (g i)).1 h'.symm i hi
-    rw [← h', sum_congr rfl (show ∀ i ∈ s, f i * g i = 0 from fun i hi ↦ by simp [h'' i hi])]
+/-- **Cauchy-Schwarz inequality** for finsets.
+
+This is written in terms of sequences `f`, `g`, and `t`, where `t` 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 (s : Finset ι) {t f g : ι → R}
+    (hf : ∀ i ∈ s, 0 ≤ f i) (hg : ∀ i ∈ s, 0 ≤ g i) (ht : ∀ i ∈ s, t i ^ 2 = f i * g i) :
+    (∑ i ∈ s, t i) ^ 2 ≤ (∑ i ∈ s, f i) * ∑ i ∈ s, g i := by
+  obtain h | h := (sum_nonneg hg).eq_or_gt
+  · have ht' : ∑ i ∈ s, t 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
+    rw [h, ht']
     simp
-  refine le_of_mul_le_mul_of_pos_left
-    (le_of_add_le_add_left (a := (∑ i ∈ s, g i ^ 2) * (∑ j ∈ s, f j * g j) ^ 2) ?_) h'
-  calc
-    _ = ∑ i ∈ s, 2 * (f i * ∑ j ∈ s, g j ^ 2) * (g i * ∑ j ∈ s, f j * g j) := by
-        simp_rw [mul_assoc (2 : R), mul_mul_mul_comm, ← mul_sum, ← sum_mul]; ring
-    _ ≤ ∑ i ∈ s, ((f i * ∑ j ∈ s, g j ^ 2) ^ 2 + (g i * ∑ j ∈ s, f j * g j) ^ 2) :=
-        sum_le_sum fun i _ ↦ two_mul_le_add_sq (f i * ∑ j ∈ s, g j ^ 2) (g i * ∑ j ∈ s, f j * g j)
-    _ = _ := by simp_rw [sum_add_distrib, mul_pow, ← sum_mul]; ring
+  · refine le_of_mul_le_mul_of_pos_left
+      (le_of_add_le_add_left (a := (∑ i ∈ s, g i) * (∑ i ∈ s, t i) ^ 2) ?_) h
+    calc
+      _ = ∑ i ∈ s, 2 * t i * (∑ j ∈ s, g j) * (∑ j ∈ s, t j) := by
+          simp_rw [mul_assoc, ← mul_sum, ← sum_mul]; ring
+      _ ≤ ∑ i ∈ s, (f i * (∑ j ∈ s, g j) ^ 2 + g i * (∑ j ∈ s, t j) ^ 2) := by
+          gcongr with i hi
+          have ht : (t i * (∑ j ∈ s, g j) * (∑ j ∈ s, t j)) ^ 2 =
+              (f i * (∑ j ∈ s, g j) ^ 2) * (g i * (∑ j ∈ s, t 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
+
+/-- **Cauchy-Schwarz inequality** for finsets, squared version. -/
+lemma sum_mul_sq_le_sq_mul_sq (s : Finset ι) (f g : ι → R) :
+    (∑ i ∈ s, f i * g i) ^ 2 ≤ (∑ i ∈ s, f i ^ 2) * ∑ i ∈ s, g i ^ 2 :=
+  sum_sq_le_sum_mul_sum_of_sq_eq_mul s
+    (fun _ _ ↦ sq_nonneg _) (fun _ _ ↦ sq_nonneg _) (fun _ _ ↦ mul_pow ..)
 
 end LinearOrderedCommSemiring
 
+/-- **Sedrakyan's lemma**, aka **Titu's lemma** or **Engel's form**.
+
+This is a specialization of the Cauchy-Schwarz inequality with the sequences `f n / √(g n)` and
+`√(g n)`, though here it is proven without relying on square roots. -/
+theorem sq_sum_div_le_sum_sq_div [LinearOrderedSemifield R] [ExistsAddOfLE R] (s : Finset ι)
+    (f : ι → R) {g : ι → R} (hg : ∀ i ∈ s, 0 < g i) :
+    (∑ i ∈ s, f i) ^ 2 / ∑ i ∈ s, g i ≤ ∑ i ∈ s, f i ^ 2 / g i := by
+  have hg' : ∀ i ∈ s, 0 ≤ g i := fun i hi ↦ (hg i hi).le
+  have H : ∀ i ∈ s, 0 ≤ f i ^ 2 / g i := fun i hi ↦ div_nonneg (sq_nonneg _) (hg' i hi)
+  refine div_le_of_le_mul₀ (sum_nonneg hg') (sum_nonneg H)
+    (sum_sq_le_sum_mul_sum_of_sq_eq_mul _ H hg' fun i hi ↦ ?_)
+  rw [div_mul_cancel₀]
+  exact (hg i hi).ne'
+
 lemma abs_prod [LinearOrderedCommRing R] (s : Finset ι) (f : ι → R) :
     |∏ x ∈ s, f x| = ∏ x ∈ s, |f x| :=
   map_prod absHom _ _

Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean

@@ -764,7 +764,7 @@ alias two_mul_le_add_pow_two := two_mul_le_add_sq
 /-- Binary, squared, and division-free **arithmetic mean-geometric mean inequality**
 (aka AM-GM inequality) for linearly ordered commutative semirings. -/
 lemma four_mul_le_sq_add [ExistsAddOfLE α] [MulPosStrictMono α]
-    [ContravariantClass α α (· + ·) (· ≤ ·)] [CovariantClass α α (· + ·) (· ≤ ·)]
+    [AddLeftReflectLE α] [AddLeftMono α]
     (a b : α) : 4 * a * b ≤ (a + b) ^ 2 := by
   calc 4 * a * b
     _ = 2 * a * b + 2 * a * b := by rw [mul_assoc, two_add_two_eq_four.symm, add_mul, mul_assoc]
@@ -774,6 +774,16 @@ lemma four_mul_le_sq_add [ExistsAddOfLE α] [MulPosStrictMono α]
 
 alias four_mul_le_pow_two_add := four_mul_le_sq_add
 
+/-- Binary and division-free **arithmetic mean-geometric mean inequality**
+(aka AM-GM inequality) for linearly ordered commutative semirings. -/
+lemma two_mul_le_add_of_sq_eq_mul [ExistsAddOfLE α] [MulPosStrictMono α] [PosMulStrictMono α]
+    [AddLeftReflectLE α] [AddLeftMono α] {a b t : α}
+    (ha : 0 ≤ a) (hb : 0 ≤ b) (ht : t ^ 2 = a * b) : 2 * t ≤ a + b := by
+  apply nonneg_le_nonneg_of_sq_le_sq (Left.add_nonneg ha hb)
+  conv_rhs => rw [← pow_two]
+  convert four_mul_le_sq_add a b using 1
+  rw [mul_mul_mul_comm, two_mul, two_add_two_eq_four, ← pow_two, ht, mul_assoc]
+
 end LinearOrderedCommSemiring
 
 section LinearOrderedRing