Skip to content
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.

Sign up for GitHub

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

Jump to bottom

Wip euclidean spaces #26

Draft
wants to merge 4 commits into
base: master
Choose a base branch
from
Draft

Wip euclidean spaces #26

wants to merge 4 commits into from

Conversation

Columbus240
Copy link
Collaborator

@Columbus240 Columbus240 commented Jan 10, 2021 •
edited
Loading

Creating a PR so GitHub doesn’t yell at me that I should make one. Also it can "focus" discussion about this branch.

TODO (incomplete):

  • What was the goal of this file/branch again? Structure/split the file accordingly.
  • Move things out of EuclideanSpaces.v that don't belong there. Among them: DiscreteTopology, seqr, seqr_spec, some facts about lists

@Columbus240 Columbus240 force-pushed the WIP_EuclideanSpaces branch 2 times, most recently from 3508fc3 to 6b24418 Compare February 7, 2021 14:02
@siraben
Copy link
Member

siraben commented May 24, 2021

Maybe this would be good for #29 as well

@Columbus240
Copy link
Collaborator Author

Columbus240 commented Jun 1, 2021 •
edited
Loading

Maybe we should first "stabilize" this branch on euclidean spaces, before doing a lot of work on manifolds #29. I consider my work here very ad-hoc and not very well structured. Names and formatting could be improved, I think. Maybe the definitions could be improved as well.
The changes you (@siraben) added to EuclideanSpaces.v could be moved from branch #30 to here.

Unrelated to manifolds: The theorem that all norms on ℝ^n generate the same topology would be nice to have. By using the basis of open-balls, it suffices to show that there exist C, c ∈ ℝ such that C ||x|| ≥ |x| ≥ c ||x||, if || . || is the euclidean norm and | . | is some other norm (or reversed). From this the general statement follows quickly.

@Columbus240
[v8.16] Declare SubspaceTopology as coercion
eb12085 
This depends on coq v8.16 and is not usable on lower versions.

Relevant issues and PRs from the coq repo:
coq/coq#15789, coq/coq#15853, coq/coq#4593, coq/coq#3115
@Columbus240
WIP: Sketch some theory about euclidean spaces
718d8cf 
Formalize Eucl.Spaces using `R∞`
This way, we have the following benefits:
* All vectors of euclidean spaces use the same operations and live in
the same type. They are inter-compatible.
* We don't have to deal with the difficult induction schemes of
`Vector.t` or have to prove preservation of length for list operations.
* We also get a canonical (with respect to this library) instance of the
`ℝ^ℕ` topology.

Further stuff:
* Prove continuity of `Rinfty_add`, `Rinfty_scale`, `Rn_projection`,
`Rinfty_scalarproduct`.
* Linear subspaces have to be nonempty, thus include zero.
* Some proofs. Including: a linear combination stays inside the
subspace its vectors come from. A linear combination can be reduced to a
list without repetitions of vectors. The unit vectors are linearly
independent.
@Columbus240
Fill in
46a6790
@Columbus240
More misc EuclideanSpaces work
49507b3
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@siraben siraben siraben left review comments

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.
2 participants
@Columbus240 @siraben