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.

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

Draft: Cantor #627

Closed
wants to merge 9 commits into from
Closed

Draft: Cantor #627

wants to merge 9 commits into from

Conversation

zstone1
Copy link
Contributor

@zstone1 zstone1 commented Apr 4, 2022

Motivation for this change

The cantor set is generally useful construction, but not particularly general or easy to formalize. Instead we do most the theory using the "cantor space", that is, functions nat -> bool with the product topology. This is an early draft, but the approach already yields some promise

In terms of formalizability, this has the advantages that

  • It's definable without putting a realType in scope
  • The proofs generally induct over "prefixes" instead of dealing with nested intersections, or ternary representations.

In terms of theory, this is great because

  • Hausdorff-Alexandroff theorem tells us that a metric space is compact iff there's a continuous surjection from the cantor space.
  • uncountability, compactness, hausdorff, are all trivially true.
  • Things need to go into files that make sense. The stuff about discrete topologies obviously belongs in topology. But the definition of the cantor_set belongs after sequences. Not clear where it the cantor_space itself goes.
Things done/to do
  • added corresponding entries in CHANGELOG_UNRELEASED.md
    (do not edit former entries, only append new ones, be careful:
    merge and rebase have a tendency to mess up CHANGELOG_UNRELEASED.md)
  • added corresponding documentation in the headers
  • prove this topology comes from a metric
  • prove this set is complete in that metric
  • prove the continuity of the cantor_map
  • I don't know the measure-theoretic implications of this approach. I wonder if this makes things better or worse?
Automatic note to reviewers

Read this Checklist and put a milestone if possible.

@affeldt-aist
Copy link
Member

Not a deep comment but you may want to consider the if/is/then/else syntax to write functions, e.g.:

Fixpoint false_extend (s : seq bool) : cantor_space :=
  if s is b :: s then
    (fun n => if n is m.+1 then false_extend s m else b)
  else
    (fun=> false).

Fixpoint prefix_of (x : cantor_space) (n : nat) : seq bool :=
  if n is m.+1 then x 0 :: prefix_of (pull x) m else nil.

Local Fixpoint prefix_helper (i : nat) (s : seq bool) :=
  if s is b :: l then
    prod_topo_apply i @^-1` [set b] `&` prefix_helper (S i) l
  else
    [set: cantor_space].

@CohenCyril CohenCyril marked this pull request as draft April 12, 2022 13:12
Adding main lemmas for arzela ascoli, some lemmas for dealing with compactness, and a technique for getting "sufficiently small" sets from a filter.
@zstone1
Copy link
Contributor Author

zstone1 commented Oct 10, 2022

Bigger and better cantor stuff coming. With #763, the bulk of this work becomes redundant anyway.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

2 participants