Zulip Chat Archive
Stream: new members
Topic: Hilbert Projection Theorem
Chris M (Aug 16 2020 at 04:13):
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 (Aug 16 2020 at 04:36):
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 (Aug 16 2020 at 04:37):
(Btw, what is the difference between Type*
and Type u
?)
Mario Carneiro (Aug 16 2020 at 04:39):
I think there are some discussions about how to define hilbert spaces in suitable generality. See https://leanprover.zulipchat.com/#narrow/stream/116395maths/topic/Complex.20inner.20product
Mario Carneiro (Aug 16 2020 at 04:40):
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 (Aug 16 2020 at 05:06):
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 (Aug 16 2020 at 06:25):
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 (Aug 16 2020 at 14:40):
I had in mind just to do it for real Hilbert spaces, yes. Similarly, HahnBanach 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 (Aug 16 2020 at 14:52):
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 (Aug 16 2020 at 14:59):
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 (Aug 16 2020 at 16:02):
@Heather Macbeth could you please edit https://github.com/leanprovercommunity/leanprovercommunity.github.io/blob/newsite/data/overview.yaml and https://github.com/leanprovercommunity/leanprovercommunity.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 (Aug 17 2020 at 03:12):
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 (Aug 17 2020 at 04:27):
OK, a few more ideas: (1) the double dual of a finitedimensional normed space is itself (should be fairly easy using docs#linear_map.continuous_of_finite_dimensional), (2) StoneWeierstrass 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 distancepreserving selfmap of the plane is determined by its values at 3 points, but I don't know whether the preliminaries exist yet).
Scott Morrison (Aug 17 2020 at 04:35):
For StoneWeierstrass, the proofs I know fall into two camps:
 prove the Weierstrass theorem first (e.g. develop Bernstein polynomials)
 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 (Aug 17 2020 at 04:41):
The proof I was first taught involved an explicit approximation of $x$ by a sequence of polynomials.
Heather Macbeth (Aug 17 2020 at 04:42):
But yes, I think there is some meat hidden behind the bland statement :)
Heather Macbeth (Aug 17 2020 at 04:45):
(mixed metaphors alert! ...)
Chris M (Aug 17 2020 at 06:36):
@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 (Aug 17 2020 at 06:41):
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 (Aug 17 2020 at 06:49):
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 libraryquality definitions, with the expectation of later cleaning it up with help on zulip?
Heather Macbeth (Aug 17 2020 at 06:51):
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 (Aug 18 2020 at 20:12):
I think "a distancepreserving selfmap 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.

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 finitedimensional 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.) 
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.

Any affinely independent spanning set (in an affine space over a vector space) has cardinality one more than the dimension, and in the finitedimensional 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 (Aug 18 2020 at 21:25):
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 (Aug 21 2020 at 04:16):
My routine was disrupted by travel but I should be back on this now. My current favorite is "the double dual of a finitedimensional 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 (Aug 21 2020 at 04:17):
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
 Finitedimensional vector spaces : rank of a set of vectors, rank of a system of linear equations,
Kyle Miller (Aug 21 2020 at 04:30):
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 (Aug 21 2020 at 04:35):
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 3cycles" would be great to have.
Alex J. Best (Aug 21 2020 at 04:38):
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 (Aug 21 2020 at 04:41):
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 Ginge Chen (Aug 21 2020 at 04:46):
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 (Aug 21 2020 at 05:05):
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 (Aug 21 2020 at 05:13):
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 (Aug 21 2020 at 08:55):
@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 (Aug 22 2020 at 04:07):
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 (Aug 22 2020 at 04:16):
If I search "symmetric group" nothing comes up.
Kyle Miller (Aug 22 2020 at 05:36):
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
.)
Last updated: May 08 2021 at 09:11 UTC