inner product on R^n

Stream: new members

[Jean-Philippe Burelle]

Shouldn't lean be able to infer that inner x y is a real number in this context?
Untitled.png

[Mario Carneiro]

We recommend pasting code blocks instead of images

[Mario Carneiro]

A vector space can exist over multiple scalar fields, so the result type is not determined

[Mario Carneiro]

I see these in the normed_space.inner_product file:

notation `⟪`x`, `y`⟫_ℝ` := @inner ℝ _ _ x y
notation `⟪`x`, `y`⟫_ℂ` := @inner ℂ _ _ x y

so you should probably use these to force the result type

[Mario Carneiro]

from these:

localized "notation `⟪`x`, `y`⟫` := @inner ℝ _ _ x y" in real_inner_product_space
localized "notation `⟪`x`, `y`⟫` := @inner ℂ _ _ x y" in complex_inner_product_space

it follows that you can open_locale real_inner_product_space to say you want the unadorned notation to refer to the real inner product

[Floris van Doorn]

If I look at the instances for inner_product_space, I think there is no inner-product space structure (yet) on euclidean_space. There should be one on pi_Lp 2 one_le_two (λ _ : fin n, ℝ) (which is the same space), however, it doesn't work for me:

import analysis.normed_space.inner_product

constant n : ℕ
constants x y : pi_Lp 2 one_le_two (λ _ : fin n, ℝ)

set_option trace.class_instances true
example : ⟪x, y⟫_ℝ = 0 :=
_

This is worrying. The problem from the trace seems to be:

[class_instances] (2) ?x_12 i : @inner_product_space ℝ ℝ ?x_8 := @is_R_or_C.inner_product_space (?x_13 i) (?x_14 i)
failed is_def_eq

[Frédéric Dupuis]

This is really weird. If I replace the line

example : ⟪x, y⟫_ℝ = 0 := sorry

by

#check (show inner_product_space ℝ (pi_Lp 2 one_le_two (λ (_x : fin n), ℝ)), by apply_instance)

everything seems to work fine. In the example the typeclass search seems to fail to find the instance real.is_R_or_C, but in the #check line it finds it immediately.

[Frédéric Dupuis]

This is really ridiculous -- this fails:

import analysis.normed_space.inner_product

constant n : ℕ
constants x y : pi_Lp 2 one_le_two (λ _ : fin n, ℝ)
local notation `⟪`x`, `y`⟫` := @inner ℝ (pi_Lp 2 one_le_two (λ _ : fin n, ℝ)) _ x y

set_option trace.class_instances true

example : ⟪x, x⟫ = (0 : ℝ) := sorry

whereas this works:

import analysis.normed_space.inner_product

constant n : ℕ
constants x y : pi_Lp 2 one_le_two (λ _ : fin n, ℝ)
local notation `⟪`x`, `y`⟫` := @inner ℝ (pi_Lp 2 one_le_two (λ _ : fin n, ℝ))
  (@inner_product_space.to_has_inner _ _ _ _) x y

set_option trace.class_instances true

example : ⟪x, x⟫ = (0 : ℝ) := sorry

[Frédéric Dupuis]

Even though the first and only thing it tries for that _ is inner_product_space.to_has_inner.

[Frédéric Dupuis]

So even this works:

import analysis.normed_space.inner_product

constant n : ℕ
constants x y : pi_Lp 2 one_le_two (λ _ : fin n, ℝ)
local notation `⟪`x`, `y`⟫` := @inner _ _ inner_product_space.to_has_inner x y

example : ⟪x, x⟫ = (0 : ℝ) := sorry

I have no idea what's going on.

[Johan Commelin]

Hmmm, can we have a type class expert look at this?

[Johan Commelin]

@Mario Carneiro @Gabriel Ebner

[Gabriel Ebner]

I would add these instances.

noncomputable instance inner_product_space.to_has_inner_real {E} :=
@inner_product_space.to_has_inner ℝ E _
noncomputable instance inner_product_space.to_has_inner_complex {E} :=
@inner_product_space.to_has_inner ℂ E _

[Frédéric Dupuis]

That seems to fix it for ℝ and ℂ, but if we do the same example for some [is_R_or_C 𝕜] we get the same problem...

[Jean-Philippe Burelle]

The original problem came up when I was trying to use the Cauchy-Schwarz inequality (as implemented) real_inner_mul_inner_self_le in a concrete setting. I still don't know how to prove, say, (x1*y1 + x2*y2)^2 <= (x1*x1 + x2*x2)*(y1*y1 + y2*y2) from that theorem without running into problems. Even when inner returns a real number, I couldn't get it to unfold into a sum of products in the case of euclidean_space ℝ (fin 2). So far I have :

lemma cauchyschwarz {x y : euclidean_space ℝ (fin 2)} : (x 1*y 1 + x 2*y 2)*(x 1*y 1 + x 2*y 2) ≤ (x 1*x 1 + x 2*x 2)*(y 1*y 1 + y 2*y 2) :=
begin
   have h:inner x y * inner x y ≤ inner x x * inner y y := real_inner_mul_inner_self_le x y,
   unfold inner at h,
   simp at h,
end

which gets me a bunch of terms like finset.univ.sum (λ (x_1 : fin 2), x x_1 * y x_1). Where do I go from here?

[Frédéric Dupuis]

The whole issue is that the inner product is defined in terms of sums over the underlying type (here fin 2), and it turns out that showing that the sum is equal to a sequence of additions is not so easy (or at least I don't know how to do it cleanly). Otherwise it works:

lemma cauchyschwarz {x y : euclidean_space ℝ (fin 2)} :
(x 1*y 1 + x 2*y 2)*(x 1*y 1 + x 2*y 2) ≤ (x 1*x 1 + x 2*x 2)*(y 1*y 1 + y 2*y 2) :=
begin
  have h₁ : x 1 * y 1 + x 2 * y 2 = ∑ i, x i * y i := sorry,
  have h₂ : x 1 * x 1 + x 2 * x 2 = ∑ i, x i * x i := sorry,
  have h₃ : y 1 * y 1 + y 2 * y 2 = ∑ i, y i * y i := sorry,
  rw [h₁, h₂, h₃],
  exact real_inner_mul_inner_self_le x y,
end

[Joseph Myers]

Using 0 and 1 instead of 1 and 2 as indices would be a good idea (though 2 = 0 in fin 2), then by { simp [fin.sum_univ_succ, add_assoc], refl } works for those sums.

[Johan Commelin]

If you follow that suggestion, those sorrys should be rfl.

[Heather Macbeth]

So, to summarize the suggestions above,

import analysis.normed_space.inner_product

lemma cauchyschwarz {x y : euclidean_space ℝ (fin 2)} :
  (x 0 * y 0 + x 1 * y 1) * (x 0 * y 0 + x 1 * y 1)
  ≤ (x 0 * x 0 + x 1 * x 1) * (y 0 * y 0 + y 1 * y 1) :=
by convert real_inner_mul_inner_self_le x y using 2; simpa [fin.sum_univ_succ, inner]

[Yakov Pechersky]

Also this:

import analysis.normed_space.inner_product

lemma cauchyschwarz {x y : euclidean_space ℝ (fin 2)} :
(x 0 * y 0 + x 1 * y 1) * (x 0 * y 0 + x 1 * y 1) ≤ (x 0 * x 0 + x 1 * x 1) * (y 0 * y 0 + y 1 * y 1) :=
begin
  convert real_inner_mul_inner_self_le x y;
  simp only [inner, list.pmap, is_R_or_C.conj_to_real, add_zero, nat.add_def,
             fin.mk_eq_subtype_mk, list.foldr, fin.mk_one, list.map]
end

[Yakov Pechersky]

which just uses the output of squeeze_simp [inner]

[Yakov Pechersky]

But wouldn't a more basic proof of this be on expanding polynomials?