New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
[Merged by Bors] - feat(analysis/normed_space/inner_product): existence of orthonormal basis #5734
Conversation
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: sgouezel <sebastien.gouezel@univ-rennes1.fr>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
Co-authored-by: Eric Wieser <wieser.eric@gmail.com>
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Thanks, I'm very happy this is happening! And I also encourage you to do the infinite-dimensional case, it's definitely worth it.
🎉 Great news! Looks like all the dependencies have been resolved: 💡 To add or remove a dependency please update this issue/PR description. Brought to you by Dependent Issues (:robot: ). Happy coding! |
@@ -595,12 +595,20 @@ lemma prod_ite_eq (f : α →₀ M) (a : α) (b : α → M → N) : | |||
f.prod (λ x v, ite (a = x) (b x v) 1) = ite (a ∈ f.support) (b a (f a)) 1 := | |||
by { dsimp [finsupp.prod], rw f.support.prod_ite_eq, } | |||
|
|||
@[simp] lemma sum_ite_self_eq {N : Type*} [add_comm_monoid N] (f : α →₀ N) (a : α) : | |||
f.sum (λ x v, ite (a = x) v 0) = f a := |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
ite (a = x) v 0
is basically finsupp.single x v a
, for which there are plenty of lemmas about. Does the ite appear in your proof in a place where finsupp.single could be used instead?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Although this lemma is probably good to have anyway
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
I didn't succeed in massaging the use (it's in orthonormal.inner_right_finsupp
) to this form.
bors r+ |
…asis (#5734) Define `orthonormal` sets (indexed) of vectors in an inner product space `E`. Show that a finite-dimensional inner product space has an orthonormal basis. Co-authored by: Busiso Chisala
Pull request successfully merged into master. Build succeeded: |
…asis (#5734) Define `orthonormal` sets (indexed) of vectors in an inner product space `E`. Show that a finite-dimensional inner product space has an orthonormal basis. Co-authored by: Busiso Chisala
Define
orthonormal
sets (indexed) of vectors in an inner product spaceE
. Show that a finite-dimensional inner product space has an orthonormal basis.Co-authored by: Busiso Chisala