## Stream: maths

### Topic: Bounded continuous functions

#### 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(\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 (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:

#### Yury G. Kudryashov (May 10 2020 at 04:04):

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

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

#### Patrick Massot (May 10 2020 at 08:14):

Normed spaces were there long before you Sébastien.

#### Sebastien Gouezel (May 10 2020 at 08:42):

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

#### 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.

#### 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?

#### Heather Macbeth (May 10 2020 at 15:12):

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

#### Patrick Massot (May 10 2020 at 15:14):

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

#### Patrick Massot (May 10 2020 at 15:14):

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

#### 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

#### 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.

#### 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.

#### 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.

#### Johan Commelin (May 11 2020 at 16:57):

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

#### 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\|$ and not $\|\ x\ \|$.

#### Johan Commelin (May 11 2020 at 16:59):

• Idem dito for: ⟨ ... ⟩

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

#### 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.

#### Heather Macbeth (May 11 2020 at 17:45):

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

#### Yury G. Kudryashov (May 11 2020 at 17:46):

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

#### 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?

#### Yury G. Kudryashov (May 11 2020 at 17:49):

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

#### Yury G. Kudryashov (May 11 2020 at 17:49):

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

#### Sebastien Gouezel (May 11 2020 at 17:54):

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

#### Heather Macbeth (May 11 2020 at 18:24):

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

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

#### 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}


#### 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.

#### 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