Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

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

Closed
wants to merge 16 commits into from
100 changes: 63 additions & 37 deletions Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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

Expand Down Expand Up @@ -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) :
theorem sum_mul_self_eq_zero_iff [LinearOrderedRing R] (s : Finset ι) (f : ι → R) :
eric-wieser marked this conversation as resolved.
Show resolved Hide resolved
∑ 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
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| :=
Expand Down Expand Up @@ -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 -/

Comment on lines +160 to +161
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I suspect this grouping isn't particularly helpful in the long term, because inevitably it ends up being desirable to extract a helper lemma that sits between these. I'll let @YaelDillies decide though.

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Fair, this wasn't meant so much as a "inequalities with names go here" but rather as a "the more difficult and mathematically interesting results go here".

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I suspect it will change again once we add the inequalities you both mentioned, but until then this looks like a mostly okay sectioning.

bors merge

/-- **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 ι)
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Can you move this out of the LinearOrderedCommSemiring section?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This theorem is right after the end of that section. I didn't think it'd make sense to make a new section for just this one theorem.

Copy link
Collaborator Author

@vihdzp vihdzp Nov 22, 2024

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Actually, I think it makes more sense to just have a "named inequalities" section in the file. (I also want to add Nesbitt in a subsequent PR, which can be proven as a consequence of Sedrakyan).

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I've reordered the file slightly, does this change make sense?

(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) :=
Expand All @@ -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

Expand Down
12 changes: 11 additions & 1 deletion Mathlib/Algebra/Order/Ring/Unbundled/Basic.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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]
Expand All @@ -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
Expand Down