Cauchy-Schwarz

Stream: Is there code for X?

[Kyle Miller]

Do we have Cauchy-Schwarz for docs#finset.sum? I was wanting this specialization:

lemma cauchy {α : Type*} [fintype α] (f : α → ℕ) :
  (∑ x, f x) ^ 2 ≤ fintype.card α * ∑ x, f x ^ 2 :=
begin
  sorry
end

[Yakov Pechersky]

(deleted)

[Junyan Xu]

docs#abs_real_inner_le_norm and docs#pi_Lp.inner_product_space

[Sebastien Gouezel]

You also have docs#pow_arith_mean_le_arith_mean_pow, from which your inequality follows by taking w i = 1/n.

[Junyan Xu]

Here's a proof with ℕ replaced by ℝ:

import analysis.inner_product_space.pi_L2
open_locale big_operators

example {α : Type*} [fintype α] (f : α → ℝ) :
  (∑ x, f x) ^ 2 ≤ fintype.card α * ∑ x, f x ^ 2 :=
begin
  let c : euclidean_space ℝ α := λ _, 1,
  change euclidean_space ℝ α at f,
  have := @abs_inner_le_norm ℝ _ _ _ c f,
  rw [← abs_norm_eq_norm c, ← abs_norm_eq_norm f, ← abs_mul] at this,
  rw [pi_Lp.inner_apply, is_R_or_C.abs_to_real] at this,
  convert sq_le_sq this using 1, { simp },
  rw mul_pow, iterate 2 { rw [euclidean_space.norm_eq, real.sq_sqrt] },
  { congr, simpa, simp [is_R_or_C.norm_eq_abs] },
  iterate 2 { rw ← finsum_eq_sum_of_fintype, apply finsum_nonneg, simp },
end

[Yaël Dillies]

This is lemma chebyshev'here.

[Yaël Dillies]

Note that this is not called Cauchy-Schwarz, but Chebyshev's inequality (even thought it indeed is a special case).

[Eric Wieser]

Looks like https://github.com/leanprover-community/mathlib/blob/01df77b33954aed5999e78837627e241523ebb49/src/combinatorics/szemeredi/mathlib.lean#L120 is another good match

[Bhavik Mehta]

Note that I proved the chebyshev' that Yaël links by reproving Cauchy-Schwarz on finsets rather than using the general version in Euclidean spaces (because I couldn't figure out how to link them cleanly enough), I think the general case (∑ i in s, f i * g i)^2 ≤ (∑ i in s, (f i)^2) * ∑ i in s, (g i)^2 is worth having in mathlib somewhere (with any proof)

[Eric Wieser]

I ended up fighting pi_Lp for a similar lemma here:
https://github.com/leanprover-community/mathlib/blob/e72114ea93abdf1d5adb4dc0bb37d5e82723bb8d/src/analysis/matrix.lean#L231-L233

[Vincent Beffara]

Do we have that ∑ is integral against counting measure somewhere? (asking for a friend)

[Yaël Dillies]

@Jason KY. is the one to ask.

[Vincent Beffara]

We do have docs#measure_theory.lintegral_count

[Junyan Xu]

Combining docs#convex_on.map_average_le (which is Jensen) with that could presumably yield another proof ... why is that called chebyshev'?

[Kyle Miller]

Thanks everyone. I've taken @Junyan Xu's proof and generalized it:

lemma cauchy_schwarz {α : Type*} [fintype α] (f g : α → ℝ) :
  (∑ x, f x * g x) ^ 2 ≤ (∑ x, f x ^ 2) * (∑ x, g x ^ 2) :=
begin
  change euclidean_space ℝ α at f,
  change euclidean_space ℝ α at g,
  have := @abs_inner_le_norm ℝ _ _ _ f g,
  rw [← abs_norm_eq_norm f, ← abs_norm_eq_norm g, ← abs_mul,
    pi_Lp.inner_apply, is_R_or_C.abs_to_real] at this,
  convert sq_le_sq this using 1,
  rw mul_pow,
  iterate 2 { rw [euclidean_space.norm_eq, real.sq_sqrt] },
  { congr; simp only [is_R_or_C.norm_eq_abs, is_R_or_C.abs_to_real, pow_bit0_abs], },
  iterate 2 { exact finset.sum_nonneg' (λ _, sq_nonneg _) },
end

then created a natural number version and the specialization I needed:

lemma cauchy_schwarz_nat {α : Type*} [fintype α] (f g : α → ℕ) :
  (∑ x, f x * g x) ^ 2 ≤ (∑ x, f x ^ 2) * (∑ x, g x ^ 2) :=
by exact_mod_cast cauchy_schwarz (λ x, f x) (λ x, g x)

lemma cauchy {α : Type*} [fintype α] (f : α → ℕ) :
  (∑ x, f x) ^ 2 ≤ fintype.card α * ∑ x, f x ^ 2 :=
by simpa using cauchy_schwarz_nat (λ _, 1) f

[Kyle Miller]

That's not the general version, though, since it's still using fintype rather than a summation over a finset, but at least the sorry is filled in in the meantime.

[Yaël Dillies]

The general version is something like

lemma chebyshev {ι α β : Type*} [has_scalar α β] [linear_ordered_add_comm_monoid α]
  [linear_ordered_ring β] [module α β] [ordered_smul α β]
  (s : finset ι) (f : ι → α) (g : ι → β) (hfg : monovary_on s f g) :
  (∑ i in s, f i) • ∑ i in s, g i ≤ s.card • ∑ i in s, f i • g i := sorry

[Mauricio Collares]

Junyan Xu said:

Combining docs#convex_on.map_average_le (which is Jensen) with that could presumably yield another proof ... why is chebyshev' called so?

Presumably because it is a special case of https://en.wikipedia.org/wiki/Chebyshev%27s_sum_inequality

[Junyan Xu]

golf: the last three lines in cauchy_schwarz can be replaced by iterate 2 { rw ← real_inner_self_eq_norm_sq }, simp [sq],

[Kyle Miller]

Thanks. With a simp_rw, it can handle the rw on the fourth-to-last line, too. (I squeezed the last simp since it was a little slow.)

lemma cauchy_schwarz {α : Type*} [fintype α] (f g : α → ℝ) :
  (∑ x, f x * g x) ^ 2 ≤ (∑ x, f x ^ 2) * (∑ x, g x ^ 2) :=
begin
  change euclidean_space ℝ α at f,
  change euclidean_space ℝ α at g,
  have := @abs_inner_le_norm ℝ _ _ _ f g,
  rw [← abs_norm_eq_norm f, ← abs_norm_eq_norm g, ← abs_mul,
    pi_Lp.inner_apply, is_R_or_C.abs_to_real] at this,
  convert sq_le_sq this using 1,
  simp_rw [mul_pow, ← real_inner_self_eq_norm_sq],
  simp only [sq, pi_Lp.inner_apply, is_R_or_C.inner_apply, is_R_or_C.conj_to_real],
end

[Junyan Xu]

I split the proof into two parts, since the first lemma is perhaps worth having:

lemma sq_abs_inner_le_norm {𝕜 E : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] (x y : E) :
  (is_R_or_C.abs (@inner 𝕜 _ _ x y)) ^ 2 ≤ ∥x∥ ^ 2 * ∥y∥ ^ 2 :=
/- in the file LHS can be written as `(abs ⟪x, y⟫)^2` as in`abs_inner_le_norm` -/
by { rw ← mul_pow, apply sq_le_sq, rw abs_mul, convert abs_inner_le_norm x y; simp }

lemma cauchy_schwarz {α : Type*} [fintype α] (f g : α → ℝ) :
  (∑ x, f x * g x) ^ 2 ≤ (∑ x, f x ^ 2) * (∑ x, g x ^ 2) :=
begin
  change euclidean_space ℝ α at f,
  change euclidean_space ℝ α at g,
  rw ← sq_abs,
  convert ← sq_abs_inner_le_norm f g,
  { exact is_R_or_C.abs_to_real },
  iterate 2 { rw ← real_inner_self_eq_norm_sq, simp [sq] },
end

[Eric Wieser]

With #13569 it's possible to avoid the changes