Hilbert Projection Theorem

Stream: new members

[Chris M]

Based on a discussion in this "starting to contribute to mathlib" thread, I wanna try to prove the Hilbert Projection Theorem in Lean. @Heather Macbeth

however I can't actually find the definition of a hilbert space.
There is a definition of an inner product space in analysis/normed_space/real_inner_product, but I can't find any hilbert_space

What should I do? ( note this is my first attempt at contributing to mathlib)

[Chris M]

What about this:

import analysis.normed_space.real_inner_product
import topology.uniform_space.cauchy

class hilbert_space (T:Type*) extends inner_product_space T:=
compl : sorry

where sorry formalizes that the distance metric w.r.t. the inner product is complete.

[Chris M]

(Btw, what is the difference between Type* and Type u?)

[Mario Carneiro]

I think there are some discussions about how to define hilbert spaces in suitable generality. See https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Complex.20inner.20product

[Mario Carneiro]

Type* is the same as Type _, that is, it infers a suitable universe or universe variable to put there. You should prefer it over Type u if you can use it, since it doesn't require declaring a universe variable u. But they have the same effect in the end

[Chris M]

Does it make sense for me to just work on a real hilbert space, and have it refactor later? Or should I wait with this project entirely until there is actually a general definition of a Hilbert space?

[Mario Carneiro]

If you have theorems you want to prove, then do what you can. It will serve as a guide for the next iteration, so it won't be wasted work even if there is a major refactor later

[Heather Macbeth]

I had in mind just to do it for real Hilbert spaces, yes. Similarly, Hahn-Banach was initially done only for real Banach spaces, although @Ruben Van de Velde has been looking at how to extend it to complex Banach spaces.

[Heather Macbeth]

Actually, I'm really sorry @Chris M , it seems like the Hilbert projection theorem in this setting already exists in mathlib! docs#exists_norm_eq_infi_of_complete_subspace, #1248. The undergrad math list needs to be updated here.

[Heather Macbeth]

As does orthogonal projection. The good news is that that means that everything is in place to do the Riesz representation theorem, the next thing on the list.

[Patrick Massot]

@Heather Macbeth could you please edit https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/overview.yaml and https://github.com/leanprover-community/leanprover-community.github.io/blob/newsite/data/undergrad.yaml You don't even need to use git, you can do it online entirely (there is an edit button in the upper right corner). I don't mind doing it but I would prefer more people realize this is easy and they can do it.

[Chris M]

Heather Macbeth said:

As does orthogonal projection. The good news is that that means that everything is in place to do the Riesz representation theorem, the next thing on the list.

I'm somewhat concerned that the Riesz representation theorem is a bit hard. It's not totally out of reach but it relies on some abstractions that aren't intuitive to me. I could do it, but I predict it'll be a bit inefficient as a first project (I'd have to spend some more time studying Hilbert spaces, as opposed to focusing on the formalization).

I'd still be willing to do it if there aren't better options. (see my Starting to contribute to mathlib thread)

[Heather Macbeth]

OK, a few more ideas: (1) the double dual of a finite-dimensional normed space is itself (should be fairly easy using docs#linear_map.continuous_of_finite_dimensional), (2) Stone-Weierstrass theorem (mathlib has the Banach algebra C(X), you'd need to define "separates points"), (3) Mertens' theorem on the product of two series, (4) Riemann's theorem on rearranging series. If you wanted something more geometric, @Joseph Myers might have some ideas (my first thought would be the theorem that a distance-preserving self-map of the plane is determined by its values at 3 points, but I don't know whether the preliminaries exist yet).

[Scott Morrison]

For Stone-Weierstrass, the proofs I know fall into two camps:

1. prove the Weierstrass theorem first (e.g. develop Bernstein polynomials)
2. avoid it somehow, but not trivially. e.g. there's a direct proof in Pedersen's "Analysis Now", but from memory it requires knowing about uniform convergence of a Taylor series.

[Heather Macbeth]

The proof I was first taught involved an explicit approximation of $|x|$ by a sequence of polynomials.

[Heather Macbeth]

But yes, I think there is some meat hidden behind the bland statement :)

[Heather Macbeth]

(mixed metaphors alert! ...)

[Chris M]

@Heather Macbeth , I'll look into those, (I don't know the theorem statements), but I don't have time right now, so let me just ask this question: Does it make sense for me to go through a couple of textbooks, and list quite a few theorems from them myself, and post them here as suggestions? Is this a reasonable thing to do, or is there already so much formalized regarding Linear algebra, etc, that this wouldn't generate anything useful? (e.g. maybe mathlib is only intersted in "important" theorems, or something)

[Heather Macbeth]

Chris M said:

is there already so much formalized regarding Linear algebra, etc, that this wouldn't generate anything useful?

Yes, this is pretty much my concern. But feel free to try it! I will repeat Scott and Kevin's advice, that the ideal is a theorem for which all the definitions already exist.

(e.g. maybe mathlib is only intersted in "important" theorems, or something)

This, not at all.

[Chris M]

The thing I'm concerned about with some of the more complex theorems is that I'll end up being slowed down a lot by not yet knowing how mathlib structures things. Does it make sense for me to be very hacky about it, even introducing definitions that would not be library-quality definitions, with the expectation of later cleaning it up with help on zulip?

[Heather Macbeth]

Well, this is what I mean about avoiding theorems which involve new definitions. The examples I and others mentioned would (mostly, hopefully) not require them.

[Joseph Myers]

I think "a distance-preserving self-map of the plane is determined by its values at 3 points" (those points need to be affinely independent) splits into a few pieces, some present in mathlib and some not.

1. An isometry of Euclidean spaces is an affine map. If surjective, we have analysis/normed_space/mazur_ulam. So either (a) state in a form requiring surjectivity, (b) prove surjectivity for any isometry from a finite-dimensional Euclidean space to one of the same dimension (or some such statement in a more general context) or (c) prove that isometries of Euclidean spaces are affine maps whether or not surjective. (I have (c), but haven't PRed it because it was pointed out that it should be done in a more general context, for any affine spaces over normed spaces with strictly convex balls, rather than relying on the inner product.)

2. Affine maps interact with affine combinations as expected (not present, but should be easy). Thus given the values of an affine map on some points, its values on all points in their affine span are determined.

3. Any affinely independent spanning set (in an affine space over a vector space) has cardinality one more than the dimension, and in the finite-dimensional case any affinely independent set with cardinality one more than the dimension spans the whole space. (See the recent discussions with Patrick; these results should be derived from the corresponding results for vector spaces.)

[Patrick Massot]

Also note that nothing is specific to dimension 2 here (except that "3 independent points" should be replaced by "dim + 1 independent points".

[Chris M]

My routine was disrupted by travel but I should be back on this now. My current favorite is "the double dual of a finite-dimensional normed space is itself". Though I presume you mean "is isomorphic to itself"?

Also, would the "permutation group" stuff in "undergrad math missing from Lean" be doable? The topics listed there are : decomposition into transpositions, decomposition into cycles with disjoint support, alternating group.

[Chris M]

By the way, I've noticed that it seems the majority of topics listed on that page are definitions not theorems, is that right?

For example, in linear algebra,

• Fundamentals: direct sum
• Duality: transpose of a linear map, orthogonality
• Finite-dimensional vector spaces : rank of a set of vectors, rank of a system of linear equations,

[Kyle Miller]

I can't really comment on this other than to point you toward group_theory.perm.cycles, which contains equiv.perm.cycle_factors, and group_theory.perm.sign, which contains equiv.perm.swap_factors. I don't know what's entailed for doing symmetric groups.

[Alex J. Best]

I think that means the symmetric group stuff is basically done, but the alternating group of permutations of a given set could be defined as the kernel of the sign map, then its cardinality computed (when finite), and results like "the alternating group is generated by 3-cycles" would be great to have.

[Alex J. Best]

The way that missing undergrad math page was made was a translation of a french syllabus if i remember correctly, so while the things listed are definitions they are really topic titles I think, so if one makes these definitions I think its implied that we should eventually have all "undergraduate level" theorems about those definitions.

[Kyle Miller]

Found the group instance: it's equiv.perm.perm_group in data.equiv.basic. I wonder if the permutation representation of a group (Cayley's theorem) is already in mathlib somewhere, or the characterization of conjugacy classes of a symmetric group as partitions of n.

[Bryan Gin-ge Chen]

I don't think we have either (but I could be wrong about the first one). We have partitions of sets and compositions of natural numbers, but not partitions of natural numbers.

[Chris M]

Alex J. Best said:

The way that missing undergrad math page was made was a translation of a french syllabus if i remember correctly, so while the things listed are definitions they are really topic titles I think, so if one makes these definitions I think its implied that we should eventually have all "undergraduate level" theorems about those definitions.

Yes, but I've been advised against starting out with topics that require creating new definitions, hence I stated that.

[Kyle Miller]

I think what @Alex J. Best was addressing was this question of yours:

By the way, I've noticed that it seems the majority of topics listed on that page are definitions not theorems, is that right?

The list might be definitions, but I guess the intent is to fill in all of the associated theorems. For example, the definitions of symmetric groups, cycles, and signs of permutations exist, but mathlib could probably stand to have a lot more textbook theorems about them.

[Chris M]

@Kyle Miller , yes that's how I interpreted it. sorry for being unclear, what I meant to say is: I've been advised against picking topics that require new definitions, and I'm assuming that these topics do require them?
Or are you saying that the fact that the topic says e.g. "transpose of a linear map", doesn't mean that the transpose of a linear map isn't defined? You're saying it could still be the case that these things are defined despite being stated in the list?

[Chris M]

I'd like to do Cayley's theorem or "characterization of conjugacy classes of a symmetric group as partitions of n". I've searched mathlib for "Cayley" and Cayley's theorem doesn't seem to be there. Can I just start doing this?

[Chris M]

If I search "symmetric group" nothing comes up.

[Kyle Miller]

All I know is that perm X has a group instance (I mention where it is a few messages up). The group $S_n$ would be perm (fin n). I'd say just go ahead and try to formalize these things and check in as you go. (You might try things generally for X : Type* with [fintype X] as needed. Cayley's theorem can be stated as there being an injective homomorphism G -> perm G, which is true even if G is infinite. For conjugacy classes, you'll need the fintype.)