more inner product spaces

Stream: new members

[Busiso Chisala]

I was obliged to abandon the real.inner_product_space when I was finally able to upgrade mathlib. A few hoops later, I am struggling to show what was straightforward before.

First question: what is missing here so that the #check inner x y returns ?M_1 instead of 𝕜 ? Is this nothing to worry about?

import algebra.module
import linear_algebra.basic
import analysis.normed_space.inner_product
import data.complex.is_R_or_C
import tactic

noncomputable theory
open_locale big_operators classical


variables {𝕜 E : Type*} [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E]
variables {ι : Type*}
variables {v : ι → E}

notation `⟪`e₁`, `e₂`⟫`:= inner e₁ e₂

variable {e₁ : E}
#check ⟪ e₁, e₁ ⟫   -- returns ⟪e₁, e₁⟫ : ?M_1 ??

variable c: 𝕜
#check c    --  c : 𝕜  , as expected
#check c • ⟪ e₁, e₁ ⟫

[Sebastien Gouezel]

What happens if you either include 𝕜, or redefine your notation with @inner specifying the field 𝕜?

[Busiso Chisala]

Sebastien Gouezel said:

What happens if you either include 𝕜, or redefine your notation with @inner specifying the field 𝕜?

Not sure how either of those work. I put an include just before that check. No avail ...

Is this the expected behaviour?

[Frédéric Dupuis]

As Sébastien said, the problem probably stems from the line that defines the notation, because it doesn't specify over which field the inner product is taken, and very often Lean can't figure it out. I would try replacing it with:

local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y

[Busiso Chisala]

Frédéric Dupuis said:

As Sébastien said, the problem probably stems from the line that defines the notation, because it doesn't specify over which field the inner product is taken, and very often Lean can't figure it out. I would try replacing it with:

local notation `⟪`x`, `y`⟫` := @inner 𝕜 _ _ x y

Thanks. I have a couple more confusions ... unless that change has disappeared them :^)

[Busiso Chisala]

How do I unravel the definition of inner product that I have managed to 'induce' on submodules? I include the code for this, and cannot move the demonstration that the inner product is 'what it is':

variable {W : submodule 𝕜 E}
instance submodule_inner_product_space  : inner_product_space 𝕜 W :=
inner_product_space.of_core {
  inner :=  λ v w, ⟪v.1 ,w.1⟫, -- ⟪(v:E) ,(w:E)⟫,
  conj_sym := by { intros v w, apply inner_conj_sym, }, --λ _ _ , inner_conj_sym _ _ ,
  nonneg_im := by { intro v, apply inner_self_nonneg_im, }, -- λ _, inner_self_nonneg_im _ ,
  nonneg_re := by { intro v, apply inner_self_nonneg, }, -- λ _, inner_self_nonneg ,
  definite := by { intros v hv, have := inner_self_eq_zero.mp hv,
    apply subtype.eq,
    rw this,
    simp,},
  add_left := by { intros , exact inner_add_left,},
  smul_left  := by { intros , exact inner_smul_left,}
}

this makes Lean happy enough, but now this:

example (W : submodule 𝕜 E) (x y:W) : ⟪x, y⟫ = ⟪x.val,y.val⟫ := by {
    sorry
}

Indeed, how can I distinguish the one inner from the other, even?

[Yury G. Kudryashov]

Does rfl work as a proof?

[Busiso Chisala]

Yury G. Kudryashov said:

Does rfl work as a proof?

I tried, it seemed not to. Then read about simpa just now. That does it instantly. I would still like to know how to unfold (if that's the word) the inner

.. := rfl works. Not in tactic mode ?

[Reid Barton]

The tactic would be refl

[Busiso Chisala]

Reid Barton said:

The tactic would be refl

Thanks ! How to trace how Lean is using the instance?

[Patrick Massot]

I'm not sure what the question means, but you should try to click on stuff in the info view.

[Patrick Massot]

inner_product.gif

[Busiso Chisala]

Patrick Massot said:

inner_product.gif

brilliant!

[Frédéric Dupuis]

I would just like to point out a pitfall before you go too far down this route: the analogue of what you're doing for inner product spaces has already been done for normed spaces (see submodule.normed_space in analysis/normed_space/basic). This means that you shouldn't be using of_core but rather the main definition, where you'll have to prove that the norm that is already there is compatible with the inner product. Using of_core you'll end up with two norm instances on the space, and that just leads to trouble.

[Busiso Chisala]

Frédéric Dupuis said:

I would just like to point out a pitfall before you go too far down this route: the analogue of what you're doing for inner product spaces has already been done for normed spaces (see submodule.normed_space in analysis/normed_space/basic). This means that you shouldn't be using of_core but rather the main definition, where you'll have to prove that the norm that is already there is compatible with the inner product. Using of_core you'll end up with two norm instances on the space, and that just leads to trouble.

I am particularly interested in the inner product. Normed space need not come with ...

[Yury G. Kudryashov]

You should not use of_core constructur.

[Yury G. Kudryashov]

Because this constructor will define norm for you, and this norm will not be defeq to the restriction of the norm on the ambient space.

[Yury G. Kudryashov]

Instead you should use the standard constructor and prove norm_sq_eq_inner reusing the same equality in the ambient space.

[Yury G. Kudryashov]

Probably we should add this warning to the docstring of the of_core constructor.

[Frédéric Dupuis]

I just opened #4571 a few hours ago with several small updates to the inner product code, I'll throw in the warning as well.

[Busiso Chisala]

Yury G. Kudryashov said:

Instead you should use the standard constructor and prove norm_sq_eq_inner reusing the same equality in the ambient space.

I will look this up: but for the record, which is the standard constructor?

[Frédéric Dupuis]

This just means directly defining an inner_product_space structure, as in

instance submodule_inner_product_space  : inner_product_space 𝕜 W :=
{
 norm_sq_eq_inner := sorry,
conj_sym := sorry,
nonneg_im := sorry,
add_left := sorry,
smul_left := sorry
}