Zulip Chat Archive

Stream: maths

Topic: Bounded continuous functions


view this post on Zulip Heather Macbeth (May 10 2020 at 02:55):

Could someone tell me about the plans for bounded_continuous_function ? The current file, written by @Sebastien Gouezel, proves the Arzela-Ascoli theorem (!) and puts a normed group structure on C(α,β)C(\alpha, \beta), the set of bounded continuous functions from a space α\alpha into a normed group β\beta. But it stops short of constructing the Banach space C(α,E)C(\alpha, E), i.e. putting a normed k\mathbb{k}-space structure on the set of bounded continuous functions into a normed k\mathbb{k}-space EE.
Is this just an oversight? Or is it because there are subtle architecture issues that have not yet been sorted out? (i.e., it would be more efficient to do several more similar things at the same time -- put a normed algebra structure on the set of bounded continuous functions into a normed algebra; put a C(α,k)C(\alpha, \mathbb{k})-module structure on C(α,E)C(\alpha, E), ....)
I actually implemented

instance : normed_space 𝕜 (bounded_continuous_function α E)

as an exercise this afternoon, so I know it is not too hard :)

view this post on Zulip Johan Commelin (May 10 2020 at 03:52):

@Heather Macbeth I have no idea... why don't you PR your "exercise" :wink: :grinning_face_with_smiling_eyes:

view this post on Zulip Yury G. Kudryashov (May 10 2020 at 04:04):

My guess: @Sebastien Gouezel formalized what he needed for some other reason.

view this post on Zulip Sebastien Gouezel (May 10 2020 at 07:33):

Yury is right. I formalized this because I needed Arzela-Ascoli for a proof in the definition of the Gromov-Hausdorff distance. At that time (a long time ago), maybe there wasn't even the notion of a normed k\mathbb{k}-space structure in mathlib!

view this post on Zulip Patrick Massot (May 10 2020 at 08:14):

Normed spaces were there long before you Sébastien.

view this post on Zulip Sebastien Gouezel (May 10 2020 at 08:42):

You're right. Operator norm was not there yet, I think.

view this post on Zulip Patrick Massot (May 10 2020 at 08:43):

It doesn't change anything to this conversation anyway. We try to be systematic, but we also need to go forward, so there tons of loose threads everywhere in mathlib.

view this post on Zulip Kevin Buzzard (May 10 2020 at 13:52):

In short @Heather Macbeth it would be a welcome PR if you wanted to add it. Ask if you need any help. Do you have an account at github?

view this post on Zulip Heather Macbeth (May 10 2020 at 15:12):

OK great, I'll do it! I'll make a github account today.

view this post on Zulip Patrick Massot (May 10 2020 at 15:14):

It would be very convenient if you could also use your real name there.

view this post on Zulip Patrick Massot (May 10 2020 at 15:14):

It's very inconvenient to struggle to map Zulip names to GitHub names

view this post on Zulip Kevin Buzzard (May 10 2020 at 15:16):

The workflow is to clone mathlib from the leanprover-community GitHub with eg leanproject, create a new branch off master, make your changes and then push directly to the leanprover-community GitHub

view this post on Zulip Ryan Lahfa (May 10 2020 at 15:19):

https://help.github.com/en/github/getting-started-with-github/fork-a-repo is quite helpful

view this post on Zulip Johan Commelin (May 10 2020 at 15:21):

Kevin Buzzard said:

The workflow is to clone mathlib from the leanprover-community GitHub with eg leanproject, create a new branch off master, make your changes and then push directly to the leanprover-community GitHub

This only works when one of the maintainers has given you the permission to push to the leanprover-community repo.
But to do that, they need to know a github username.

view this post on Zulip Heather Macbeth (May 11 2020 at 16:27):

Here is the new branch:
https://github.com/leanprover-community/mathlib/tree/bounded-continuous-functions
Comments on the code would be welcome, I know it is a real mess.

view this post on Zulip Johan Commelin (May 11 2020 at 16:56):

@Heather Macbeth At first glance this is already looking very good! Some minor stylistic issues, but nothing big, I think.

view this post on Zulip Johan Commelin (May 11 2020 at 16:57):

I suggest that you open a PR, and then we can give line by line comments.

view this post on Zulip Johan Commelin (May 11 2020 at 16:58):

Here is a small start:

  • I think in mathlib we don't put spaces in the norm operator. So x\|x\| and not  x \|\ x\ \|.

view this post on Zulip Johan Commelin (May 11 2020 at 16:59):

  • Idem dito for: ⟨ ... ⟩

view this post on Zulip Johan Commelin (May 11 2020 at 17:01):

And then, when you build an instance, and it's not a one-liner, the preferred style is

instance foobar : some_class X :=
{ field_name := value,
  other_field := quux }

instead of the anonymous ⟨ ... ⟩

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 17:43):

Lint complains about in norm_eq. We try to use everywhere because it makes the life of rw and simp easier.

view this post on Zulip Heather Macbeth (May 11 2020 at 17:45):

Interesting, thank you! I will make these changes. Let me know if you think of others.

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 17:46):

It will be easier to comment once you'll make PR.

view this post on Zulip Heather Macbeth (May 11 2020 at 17:48):

FWIW, the comes as an adaptation of Sebastien's

/-- The uniform distance between two bounded continuous functions -/
instance : has_dist (α  β) :=
⟨λf g, Inf {C | C  0   x : α, dist (f x) (g x)  C}

Is this also non-standard style, or is there a difference between the two usages?

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 17:49):

I think that we should change this too. @Sebastien Gouezel ?

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 17:49):

The main exception for this rule is ∀ ε > 0 because ∀ ε, 0 < ε → looks worse.

view this post on Zulip Sebastien Gouezel (May 11 2020 at 17:54):

Yes, that's clearly a newcomer's mistake, that should be fixed :)

view this post on Zulip Heather Macbeth (May 11 2020 at 18:24):

PR title conventions: should this be "feat(topology/bounded_continuous_functions): * * * * *" ?

view this post on Zulip Kevin Buzzard (May 11 2020 at 18:25):

and then VS Code will complain that you've gone over your 50 characters before you've even begun to summarise what you did in about 5 words :-/

view this post on Zulip Heather Macbeth (May 11 2020 at 18:31):

OK, done.
https://github.com/leanprover-community/mathlib/pull/2660

view this post on Zulip Heather Macbeth (May 11 2020 at 18:39):

Johan Commelin said:

And then, when you build an instance, and it's not a one-liner, the preferred style is

instance foobar : some_class X :=
{ field_name := value,
  other_field := quux }

instead of the anonymous ⟨ ... ⟩

I ran into difficulties fixing this at line 457 and following, where I have a multi-line ⟨ ... ⟩ constructor for a bounded continuous function:

⟨λx, c  f.1 x,
    continuous.smul continuous_const f.2.left,
    begin
      cases f.2.right with C hbound,
      use c * C,
      intros,
      have hnneg : 0  c,
      { exact norm_nonneg c },
...

I could not discover what the field names were for bounded continuous functions -- here is their definition:

/-- The type of bounded continuous functions from a topological space to a metric space -/
def bounded_continuous_function (α : Type u) (β : Type v) [topological_space α] [metric_space β] :
  Type (max u v) :=
{f : α  β // continuous f  C, x y:α, dist (f x) (f y)  C}

view this post on Zulip Sebastien Gouezel (May 11 2020 at 18:41):

Yes, I did everything wrong at the time. This should be a structure instead of a subtype.

view this post on Zulip Yury G. Kudryashov (May 11 2020 at 18:46):

But probably this refactor could wait till another PR.


Last updated: May 11 2021 at 16:22 UTC