Bounded continuous functions

Stream: maths

[Heather Macbeth]

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(\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(\alpha, E)$, i.e. putting a normed $\mathbb{k}$-space structure on the set of bounded continuous functions into a normed $\mathbb{k}$-space $E$.
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(\alpha, \mathbb{k})$-module structure on $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 :)

[Johan Commelin]

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

[Yury G. Kudryashov]

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

[Sebastien Gouezel]

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 $\mathbb{k}$-space structure in mathlib!

[Patrick Massot]

Normed spaces were there long before you Sébastien.

[Sebastien Gouezel]

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

[Patrick Massot]

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.

[Kevin Buzzard]

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?

[Heather Macbeth]

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

[Patrick Massot]

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

[Patrick Massot]

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

[Kevin Buzzard]

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

[Ryan Lahfa]

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

[Johan Commelin]

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.

[Heather Macbeth]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Johan Commelin]

Here is a small start:

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

[Johan Commelin]

• Idem dito for: ⟨ ... ⟩

[Johan Commelin]

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 ⟨ ... ⟩

[Yury G. Kudryashov]

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

[Heather Macbeth]

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

[Yury G. Kudryashov]

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

[Heather Macbeth]

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?

[Yury G. Kudryashov]

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

[Yury G. Kudryashov]

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

[Sebastien Gouezel]

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

[Heather Macbeth]

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

[Kevin Buzzard]

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 :-/

[Heather Macbeth]

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

[Heather Macbeth]

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}

[Sebastien Gouezel]

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

[Yury G. Kudryashov]

But probably this refactor could wait till another PR.