diff --git a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
index b51accd2d82ad..1c522e8948d04 100644
--- a/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
+++ b/Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
@@ -14,9 +14,12 @@ import Mathlib.Tactic.Ring
 
 This file contains the results concerning the interaction of finset big operators with ordered
 rings.
+
+In particular, this file contains the standard form of the Cauchy-Schwarz inequality, as well as
+some of its immediate consequences.
 -/
 
-variable {ι R : Type*}
+variable {ι R S : Type*}
 
 namespace Finset
 
@@ -120,41 +123,10 @@ lemma prod_add_prod_le {i : ι} {f g h : ι → R} (hi : i ∈ s) (h2i : g i + h
 
 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])]
-    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
-
-theorem sum_mul_self_eq_zero_iff (s : Finset ι) (f : ι → R) :
-    ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0 := by
-  induction s using Finset.cons_induction with
-  | empty => simp
-  | cons i s his ih =>
-    simp only [Finset.sum_cons, Finset.mem_cons, forall_eq_or_imp]
-    refine ⟨fun hc => ?_, fun h => by simpa [h.1] using ih.mpr h.2⟩
-    have hi : f i * f i ≤ 0 := by
-      rw [← hc, le_add_iff_nonneg_right]
-      exact Finset.sum_nonneg fun i _ ↦ mul_self_nonneg (f i)
-    have h : f i * f i = 0 := (eq_of_le_of_le (mul_self_nonneg (f i)) hi).symm
-    exact ⟨zero_eq_mul_self.mp h.symm, ih.mp (by rw [← hc, h, zero_add])⟩
-
-end LinearOrderedCommSemiring
+theorem sum_mul_self_eq_zero_iff [LinearOrderedSemiring R] [ExistsAddOfLE R] (s : Finset ι)
+    (f : ι → R) : ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0 := by
+  rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ mul_self_nonneg _]
+  simp
 
 lemma abs_prod [LinearOrderedCommRing R] (s : Finset ι) (f : ι → R) :
     |∏ x ∈ s, f x| = ∏ x ∈ s, |f x| :=
@@ -184,11 +156,63 @@ lemma prod_add_prod_le' (hi : i ∈ s) (h2i : g i + h i ≤ f i) (hgf : ∀ j 
       assumption
 
 end CanonicallyOrderedCommSemiring
+
+/-! ### Named inequalities -/
+
+/-- **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 := by
+  obtain h | h := (sum_nonneg hg).eq_or_gt
+  · 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
+    rw [h, ht']
+    simp
+  · 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
+    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
+
+/-- **Cauchy-Schwarz inequality** for finsets, squared version. -/
+lemma sum_mul_sq_le_sq_mul_sq [LinearOrderedCommSemiring R] [ExistsAddOfLE R] (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 ..)
+
+/-- **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'
+
 end Finset
 
-section AbsoluteValue
+/-! ### Absolute values -/
 
-variable {S : Type*}
+section AbsoluteValue
 
 lemma AbsoluteValue.sum_le [Semiring R] [OrderedSemiring S] (abv : AbsoluteValue R S)
     (s : Finset ι) (f : ι → R) : abv (∑ i ∈ s, f i) ≤ ∑ i ∈ s, abv (f i) :=
@@ -212,6 +236,8 @@ lemma IsAbsoluteValue.map_prod [CommSemiring R] [Nontrivial R] [LinearOrderedCom
 
 end AbsoluteValue
 
+/-! ### Positivity extension -/
+
 namespace Mathlib.Meta.Positivity
 open Qq Lean Meta Finset
 
diff --git a/Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean b/Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
index 06cc0315f08b0..99bd1f2cfd31c 100644
--- a/Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
+++ b/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 r : α}
+    (ha : 0 ≤ a) (hb : 0 ≤ b) (ht : r ^ 2 = a * b) : 2 * r ≤ 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