orthonormal basis structure

Stream: maths

[Daniel Packer]

Hi all,

At the suggestion/guidance of @Heather Macbeth, @Hans Parshall, @Dustin Mixon, and I are thinking about introducing an orthonormal_basis structure,

structure orthonormal_basis := of_repr :: (repr : E ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι)

Which will be the finite dimensional version of docs#hilbert_basis.has_coe_to_fun. I think we have a basic sense of lemmas that we want to hit, but if you have any thoughts let us know!

[Daniel Packer]

So, there is already a noncomputable definition of orthonormal_basis at docs#orthonormal_basis. Ultimately it seems like this should get roped into the structure definition above. I'm not quite sure what the standard rules for how to combine these sorts of definitions for compatibility are.
That is, it seems to me that the new output of docs#orthonormal_basis should be:

def orthonormal_basis (𝕜 : Type u_1) (E : Type u_2) [is_R_or_C 𝕜] [inner_product_space 𝕜 E] [finite_dimensional 𝕜 E] :
orthonormal_basis 𝕜 E

But I don't know if it's my role to refactor a thing like this (to be clear, I'm happy to, I just don't want to mess up some one else's code)

[Heather Macbeth]

That definition is the definition of a particular "standard" orthonormal basis of a given inner product space. Your definition is more important, so it should get the name. And we'll rename that definition.

[Daniel Packer]

Ah, I see. So the definition there should be like std_orthonormal_basis?

[Heather Macbeth]

But your formulation of the type signature for the new output is correct!

[Heather Macbeth]

More generally, I've been thinking for a while that this would be a good change, and I'm very pleased that @Daniel Packer and co will take it on. There are several parts of the library that could probably be rewritten more elegantly once we have this new structure. It would supersede docs#basis.isometry_euclidean_of_orthonormal , we'd probably rewrite docs#maximal_orthonormal_iff_basis_of_finite_dimensional using it ...

[Heather Macbeth]

Probably docs#inner_product_space.is_self_adjoint.diagonalization_basis would pass through it

[Heather Macbeth]

And maybe @Joseph Myers will have applications for Euclidean geometry.

[Heather Macbeth]

I'd be happy to help out switching all these parts of the library to the new structure ... Maybe the strategy should be: first make the new definition and the "obvious" new lemmas, then we can slowly switch these other parts of the library over, and discover what the other standard lemmas should be in the process of developing these applications.

[Heather Macbeth]

One thought: When we have theories developed in parallel, it's good to have parallel naming. Here, both docs#hilbert_basis and docs#basis are quite parallel, so when there is a lemma that is parallel to lemmas there, the names should also be the same.

[Heather Macbeth]

By the way, if you are curious about this design choice to make the definition of "basis" the strongest possible thing one gets from a basis -- namely the identification with C^n -- you can read some of the history at the PR #7496 and the Zulip discussions linked there. It was @Anne Baanen's idea.

[Joseph Myers]

I'd expect the orthonormal_basis API to provide definitions converting to and from a basis that is propositionally orthonormal (with proofs that the basis vectors and coordinates are the same etc.) and analogues of basis APIs such as basis.map, basis.reindex, basis.equiv (orthonormal_basis.map and orthonormal_basis.equiv would of course work with linear_isometry_equiv), with lemmas showing those APIs are consistent with the corresponding APIs for basis. Some other APIs may be needed for particular purposes (e.g. adjust_to_orientation, in order to make orientation.fin_orthonormal_basis give a bundled orthonormal_basis; that may be a case where "convert to basis, apply the basis API and then convert back to orthonormal_basis" is an appropriate implementation strategy).

My current work on oriented angles defines things in terms of a basis that's propositionally orthonormal (and then proves that the definition depends only on the orientation associated with the basis, so that the API can then be replicated with definitions and lemmas that only take an orientation and not a basis as an argument and hopefully most users don't need to refer to bases at all). (That work is sorry-free, but there are still more lemmas I'd like to add before PRing it.) It should be straightforward to adapt to take an orthonormal_basis once such a bundled type is available, with API corresponding to that of basis and existing lemmas about a basis that is orthonormal updated accordingly to use the new type.

[Heather Macbeth]

Joseph Myers said:

I'd expect the orthonormal_basis API to provide definitions converting to and from a basis that is propositionally orthonormal (with proofs that the basis vectors and coordinates are the same etc.)

Agreed; I think this should look very similar to docs#hilbert_basis.mk together with the associated lemma docs#hilbert_basis.coe_mk .

[Heather Macbeth]

Or, perhaps we should have both orthonormal_basis.mk, from

(hv : orthonormal 𝕜 v) (hsp : submodule.span 𝕜 (set.range v)= ⊤)

and also basis.to_orthonormal_basis from

(b : basis ι 𝕜 E) (hv : orthonormal 𝕜 b)

[Daniel Packer]

Okay, I've got a basic API set up mirroring some of docs#hilbert_basis. We have both

protected def mk (hon : orthonormal 𝕜 v) (hsp: submodule.span 𝕜 (set.range v) = ⊤):
orthonormal_basis ι 𝕜 E

and

def _root_.basis.to_orthonormal_basis (b : basis ι 𝕜 E) (hb : orthonormal 𝕜 b) :
orthonormal_basis  ι 𝕜 E

There's still more to do, but I wanted to check in that it's generally going in the right direction. Some of the proofs are much longer than they need to be, but I don't think I know the right tricks to get them shorter. I also think I might need permission to the non-master branch--my github is Daniel-Packer.
Currently, the repository is at Daniel-Packer/orthonormal_basis.

[Heather Macbeth]

@Daniel Packer I think you can use docs#set.indicator to define euclidean_space.single, and indeed there are probably some proofs that can be made shorter over the course of the PR process. Also, can you make an analogue of docs#hilbert_basis.has_sum_repr_symm, using the finite sum (docs#finset.sum)? But otherwise this looks good to me! Please go ahead and open a PR (I think the material can be put directly in the file inner_product_space.pi_Lp, and we may find that some of the lemmas there will naturally be deleted.)

[Daniel Packer]

Okay! Both changes done! I think I might need permission for non-master branches on the mathlib repo, my user id is Daniel-Packer

[Kyle Miller]

@Daniel Packer Invite sent!

[Daniel Packer]

Okay, so we now have a branch at :
https://github.com/leanprover-community/mathlib/tree/orthonormal_basis
I think there are some linting issues, and when building, it introduces some error in orientation world, so I haven't opened a pull request yet.
That said, I've opened up a draft pull request here:
https://github.com/leanprover-community/mathlib/pull/12060

[Kevin Buzzard]

I would love to hear more people talking about the various worlds we have in mathlib :-)

[Daniel Packer]

Okeedokes! I think that the orthonormal_basis refactor is ready for review for merging. It has passed the checks, it seems.

[Daniel Packer]

Okay! Now that we have the updated orthonormal_basis structure, I'm going to go through projection.lean and spectrum.lean to refactor appropriately. I'm going to be starting with the section orthonormal_basis in projection.lean (which we might incidentally want to rename?). Let me know if you have strong opinions on how it refactors.
My main goal is get std_orthonormal_basis to be of type orthonormal_basis, and to have self_adjoint.eigenvector_basis to be of type orthonormal_basis as well.

[Heather Macbeth]

@Daniel Packer Oh, snap! I was doing this too. I haven't made too much progress but I'll push what I have.

[Heather Macbeth]

Daniel Packer said:

I'm going to be starting with the section orthonormal_basis in projection.lean (which we might incidentally want to rename?).
My main goal is get std_orthonormal_basis to be of type orthonormal_basis, and to have self_adjoint.eigenvector_basis to be of type orthonormal_basis as well.

Yes, I had the same idea. And that stuff should, therefore, move from projection to pi_L2.

[Heather Macbeth]

branch#std_orthonormal_basis (about half-debugged)

[Daniel Packer]

@Heather Macbeth No worries! Do you plan on working on it today? Because I'm happy to stay away from it for now if so--long term I just want self_adjoint.eigenvector_basis to be an orthonormal_basis for my own selfish purposes.
If you aren't planning on working on it today, I can try to make some progress and you can take over from wherever I leave off.

[Heather Macbeth]

Sounds great, I should really do some other things :). I'll leave the branch for you now, keep me posted!

[Daniel Packer]

Will do!

[Daniel Packer]

The first thing I've been trying to do is build a version of dos#basis.reindex for orthonormal_basis. It seems like the way to do that is to make a version of docs#finsupp.dom_lcongr with linear_isometry_equiv instead. Where should such a definition go?

[Heather Macbeth]

I think in pi_L2, too.

[Heather Macbeth]

Or, no, sorry, in normed_space.pi_Lp.

[Daniel Packer]

Ah, you're totally right! Thanks!

[Daniel Packer]

I think I might be misunderstanding things, but if I want to put finsupp.dom_licongr in normed_space.pi_Lp, then I think I will have to add an import in that file for euclidean_space to work (which feels wrong to me). Should euclidean_space be living in normed_space.pi_Lp?

[Daniel Packer]

Currently, I'm working with:

variables [fintype ι']
def _root_.finsupp.dom_licongr (e : ι ≃ ι') : euclidean_space 𝕜 ι ≃ₗᵢ[𝕜] euclidean_space 𝕜 ι' :=

[Daniel Packer]

Separately, this definition seems silly to have around now that we have the orthonormal_basis structure:

def linear_isometry_equiv.of_inner_product_space
  [finite_dimensional 𝕜 E] {n : ℕ} (hn : finrank 𝕜 E = n) :
  E ≃ₗᵢ[𝕜] (euclidean_space 𝕜 (fin n)) :=
(fin_std_orthonormal_basis hn).repr

[Heather Macbeth]

@Daniel Packer I was thinking more like

variables [fintype ι'] {E : Type*} [normed_group E] [normed_space 𝕜 E]
def pi_Lp.dom_licongr (e : ι ≃ ι') : pi_Lp 𝕜 (λ i : ι, E) p ≃ₗᵢ[𝕜] pi_Lp 𝕜 (λ i : ι, E) p :=

[Heather Macbeth]

Daniel Packer said:

Separately, this definition seems silly to have around now that we have the orthonormal_basis structure:

def linear_isometry_equiv.of_inner_product_space
  [finite_dimensional 𝕜 E] {n : ℕ} (hn : finrank 𝕜 E = n) :
  E ≃ₗᵢ[𝕜] (euclidean_space 𝕜 (fin n)) :=
(fin_std_orthonormal_basis hn).repr

Agreed! Let's delete it.

[Daniel Packer]

@Heather Macbeth I've pushed where I'm at rn. I think my proof of finsupp.dom_licongr is far too long.
I'm also unsure how to mess with

lemma maximal_orthonormal_iff_basis_of_finite_dimensional
(hv : orthonormal 𝕜 (coe : v → E)) :

which you had commented out, as well as how the following discussion ought to go.

[Daniel Packer]

For instance, I had:

@[irreducible] def direct_sum.submodule_is_internal.subordinate_orthonormal_basis :
  orthonormal_basis (fin n) 𝕜 E :=

[Daniel Packer]

Which I tried to combine with the later subordinate_orthonormal_basis_orthonormal, which added this hypothesis:

@[irreducible] def direct_sum.submodule_is_internal.subordinate_orthonormal_basis
  (hV' : @orthogonal_family 𝕜 _ _ _ _ (λ i, V i) _ (λ i, (V i).subtypeₗᵢ)) :
  orthonormal_basis (fin n) 𝕜 E :=

[Daniel Packer]

But this created errors later on, and I suspect it will mess up stuff in other parts of mathlib, so I think I would like to get others' (i.e. your) opinions before I push any changes to this.

[Heather Macbeth]

@Daniel Packer Quick comment -- I think it would be faster to prove finsupp.dom_licongr without passing through finitely-supported functions -- that's a complication you don't need when the index set itself is finite. I think docs#linear_equiv.Pi_congr_right will be a better "basic model" for a linear-equiv-to-upgrade-to-linear-isometry-equiv than docs#finsupp.dom_lcongr

[Heather Macbeth]

maximal_orthonormal_iff_basis_of_finite_dimensional can hopefully be deleted, I just commented it out in case we needed to raid its proof for some argument.

[Heather Macbeth]

And to deal with the awkwardness about subordinate_orthonormal_basis, I think you should define an analogue of the construction docs#direct_sum.submodule_is_internal.collected_basis called something like

direct_sum.submodule_is_internal.collected_orthonormal_basis

[Heather Macbeth]

(refer to docs#direct_sum.submodule_is_internal.collected_basis_orthonormal for some of the work involved in that construction)

[Daniel Packer]

@Heather Macbeth For the finsupp.dom_licongr did you mean docs#linear_equiv.Pi_congr_left ? I'm not sure I understand how docs#linear_equiv.Pi_congr_right will help. (Separately, what does the naming convention refer to?)

[Heather Macbeth]

Yes, sorry! I have no idea what the names refer to :)

[Heather Macbeth]

Git blame says @Eric Wieser baptised them.

[Eric Wieser]

I think I just copied docs#equiv.Pi_congr_left

[Eric Wieser]

The left vs right naming corresponds to the domain vs codomain of the pi type

[Eric Wieser]

dom and cod would probably be more sensible names

[Daniel Packer]

So should I be calling the lemma linear_isometry_equiv.Pi_congr_dom instead?

[Eric Wieser]

No, you should stick to Pi_congr_left and Pi_congr_right, unless you first want to make a PR to rename all the existing _left / _rights to _dom / _cod.

[Daniel Packer]

I'm going to put this question here, but feel free to move it if it deserves its own thread.
I've been trying to port the lemmas about docs#basis.reindex to docs#orthonormal_basis, and one of these is docs#basis.coe_reindex_repr, which looks like: ((b.reindex e).repr x : ι' → R) = b.repr x ∘ e.symm.
I've tried to port this over as:

protected lemma coe_reindex_repr
  (b : orthonormal_basis ι 𝕜 E) (e : ι ≃ ι') (x : E) (i' : ι') :
  ((b.reindex e).repr x) = (id(b.repr x) : ι → 𝕜) ∘ (e.symm) :=

but this requires an id (or perhaps something else) to make it run through, which tells Lean that this can't be a simplification lemma.
I have a few associated questions:

• Should I even be bothering to formalize this lemma?
• Why does this id prevent this from being a simplification lemma?
• Why doesn't euclidean_space ι 𝕜 have an instance of has_coe_to_fun : ι → 𝕜?

[Heather Macbeth]

All very interesting questions! I'd go for avoiding the issue by temporarily answering no to

Daniel Packer said:

• Should I even be bothering to formalize this lemma?

but maybe someone will come along with a more principled answer :)

[Yaël Dillies]

If you gave us a #mwe I could investigate further but I don't see why

• you need the id (maybe you just need a coercion arrow ↑?)
• the id would matter for simp normal form as it's on the RHS

[Heather Macbeth]

@Yaël Dillies the id is because euclidean_space is a type synonym.

[Yaël Dillies]

Ahah, so you're saying you're missing the "identity" equivalence between euclidean_space and ι → 𝕜? Definitely add that, in the spirit of docs#order_dual.to_dual and docs#of_lex.

[Heather Macbeth]

Well, I think that's somewhat of an orthogonal (ha!) project to Daniel's.

[Heather Macbeth]

And also might not be necessarily once we find the Platonic ideal of how to represent Euclidean space ... therefore fine to punt on.

[Yaël Dillies]

Sure, but it seems related to Daniel's current problem and is also very cheap to have.

[Heather Macbeth]

I still advocate for trying other approaches to the issue, so I'd rather not (yet) add a lot of boilerplate to double down on the type synonym method.

[Heather Macbeth]

@Daniel Packer Do you need this lemma?

[Yaël Dillies]

Heather, two definitions is not a lot of boilerplate :stuck_out_tongue_wink:

[Yaël Dillies]

That's all you need to make your translations from and to euclidean_space type-correct.

[Yaël Dillies]

One thing I didn't add in the thread you just linked to is that you don't need to insert those identity equivalences when writing non public-facing API. See for example docs#order_iso.dual_dual, which I literally just defined as docs#order_iso.refl but without the @[simps] so that I get to write docs#order_iso.coe_dual_dual and friends myself in the correct form.

[Daniel Packer]

Heather Macbeth said:

Daniel Packer Do you need this lemma?

I don't need this lemma at all. I just didn't want to build half of an API. I'm also happy to add this change in, but I'm not quite sure what it looks like. Specifically, what sort of equivalence do we think it should be?

[Yaël Dillies]

def to_euclidean_space : (ι → 𝕜) ≃ euclidean_space 𝕜 ι := equiv.refl _
def of_euclidean_space : euclidean_space 𝕜 ι ≃ (ι → 𝕜) := equiv.refl _

Note the absence of the simps attribute.

[Heather Macbeth]

Daniel Packer said:

I don't need this lemma at all. I just didn't want to build half of an API.

I'd suggest adding the following equivalent lemma, which feels more "native" to Euclidean space.

protected lemma reindex_repr_apply
  (b : orthonormal_basis ι 𝕜 E) (e : ι ≃ ι') (x : E) (i' : ι') :
  (b.reindex e).repr x i' = b.repr x (e.symm i') :=

[Daniel Packer]

Heather Macbeth said:

Daniel Packer said:

I don't need this lemma at all. I just didn't want to build half of an API.

I'd suggest adding the following equivalent lemma, which feels more "native" to Euclidean space.

protected lemma reindex_repr_apply
  (b : orthonormal_basis ι 𝕜 E) (e : ι ≃ ι') (x : E) (i' : ι') :
  (b.reindex e).repr x i' = b.repr x (e.symm i') :=

Ah nice! In fact, that is the lemma that I did add after coming across the struggles with the other form. (Although I titled it reindex_repr to follow the convention of docs#basis.reindex_repr).