## Stream: Is there code for X?

### Topic: sup norm on continuous functions?

#### Scott Morrison (Feb 28 2021 at 08:12):

What do I need to import to get the sup norm on continuous functions?

#### Heather Macbeth (Feb 28 2021 at 08:13):

It's in topology.bounded_continuous_function -- docs#bounded_continuous_function.normed_space !

Thanks.

#### Scott Morrison (Feb 28 2021 at 08:13):

Do we have something that provides

instance {X : Type*} [topological_space X] : has_norm C(X, ℝ) := by apply_instance


#### Heather Macbeth (Feb 28 2021 at 08:14):

Are you assuming compactness of X?

#### Scott Morrison (Feb 28 2021 at 08:14):

I guess yes. I really just want X = [0,1].

#### Heather Macbeth (Feb 28 2021 at 08:15):

There is docs#bounded_continuous_function.mk_of_compact, which turns a continuous function on compact X into a bounded_continuous_function.

#### Heather Macbeth (Feb 28 2021 at 08:16):

It would be nice to have this operation as a linear equivalence from C(X, ℝ) to bounded_continuous_function X ℝ, but I think currently it exists just as a raw function.

#### Heather Macbeth (Feb 28 2021 at 08:18):

Can you perhaps just work in bounded_continuous_function X ℝ, and forget about C(X, ℝ)?

#### Kevin Buzzard (Feb 28 2021 at 08:55):

I'm going to need this sup norm on the continuous functions from a compact space to a normed group soon.

#### Heather Macbeth (Feb 28 2021 at 09:00):

Yup, that also exists! docs#bounded_continuous_function.normed_group

#### Scott Morrison (Feb 28 2021 at 09:27):

Heather Macbeth said:

Can you perhaps just work in bounded_continuous_function X ℝ, and forget about C(X, ℝ)?

I'm not so excited about doing this, just because it will sound awkward. No one talks about the bounded continuous functions on [0,1].

Would it be a bad idea if I invested some effort into upgrading mk_of_compact into a linear equivalence, and provide that has_norm instance?

#### Scott Morrison (Feb 28 2021 at 09:28):

Or will this just result in too many ways to talk about the same thing, and I should get over using →ᵇ?

#### Heather Macbeth (Feb 28 2021 at 09:43):

Hmm, it might become awkward, you'll have to prove a bunch of lemmas about properties (eg, completeness) of a norm being preserved when you pull it back by a linear equivalence.

#### Heather Macbeth (Feb 28 2021 at 09:45):

On the other hand, I think nobody much likes bounded_continuous_function in its current form. I think @Sebastien Gouezel said he thinks it ought to be made as a structure rather than a subtype, for example.

#### Scott Morrison (Feb 28 2021 at 09:47):

Can it extend continuous_map? Or would the topological_space on the target there get in the way of the metric space on the target in bounded_continuous_function?

#### Heather Macbeth (Feb 28 2021 at 09:50):

I think that would be nice! I would hope that if the topological_space on the target is induced by the metric_space, there isn't a problem?

#### Scott Morrison (Feb 28 2021 at 09:52):

Okay, maybe I will try it someday. :-) In the meantime I think I will try to get used to →ᵇ!

#### Scott Morrison (Feb 28 2021 at 09:53):

Another question while you're here --- if I have a continuous function [0,1] →ᵇ ℝ, and I just want the epsilon delta formulation of it being uniformly continuous, where do I go?

#### Heather Macbeth (Feb 28 2021 at 09:56):

Yup, plus docs#compact_space.uniform_continuous_of_continuous to get the uniform continuity.

#### Scott Morrison (Feb 28 2021 at 10:21):

Do we have that, on a compact space, || f || < M iff for all x, |f(x)| < M?

#### Heather Macbeth (Feb 28 2021 at 10:25):

I think not directly, but you can deduce it from docs#is_compact.exists_forall_ge

#### Scott Morrison (Feb 28 2021 at 13:48):

Do these look okay:

lemma norm_le_of_bound {X Y : Type*} [topological_space X] [nonempty X] [normed_group Y]
{f : X →ᵇ Y} {M : ℝ} (w : ∀ x, ∥f x∥ ≤ M) : ∥f∥ ≤ M :=
begin
have z : 0 ≤ M := le_trans (norm_nonneg _) (w (nonempty.some ‹_›)),
apply real.Inf_le _,
exact ⟨0, λ y p, p.1⟩,
exact ⟨z, λ x, by { convert w x, exact dist_zero_right _, }⟩,
end

lemma norm_lt_of_bound
{X Y : Type*} [topological_space X] [compact_space X] [nonempty X] [normed_group Y]
{f : X →ᵇ Y} {M : ℝ} (h : ∀ x, ∥f x∥ < M) : ∥f∥ < M :=
begin
have c : continuous (λ x, ∥f x∥), { have := f.2.1, continuity, },
obtain ⟨x, -, le⟩ :=
is_compact.exists_forall_ge compact_univ set.univ_nonempty (continuous.continuous_on c),
exact lt_of_le_of_lt (norm_le_of_bound (λ y, le y trivial)) (h x),
end


I'm hoping the first one already exists in some easier form.

#### Heather Macbeth (Feb 28 2021 at 16:38):

Looks good! The first one does indeed exist, docs#bounded_continuous_function.norm_le.

#### Scott Morrison (Mar 01 2021 at 23:08):

Thanks Heather, for your help on these questions. I've just pushed my proof of Weierstrass' theorem, and as punishment for helping me I've requested a review from you. :-) The PR is #6497 and the diff relative to earlier PRs still in the queue is https://github.com/leanprover-community/mathlib/compare/bernstein_identities...bernstein_approximation.

Very exciting!

#### Scott Morrison (Mar 01 2021 at 23:18):

In this PR is a very "concrete" statement --- the approximations by Bernstein polynomials converge uniformly. In a later PR I'll set up the abstract statement about density.

#### Heather Macbeth (Mar 01 2021 at 23:19):

(Do you want me to review it now or wait for some of the prerequisites to be merged? I see silly things, like finset lemmas in the wrong file src/analysis/special_functions/bernstein.lean, that you are probably planning to fix later.)

#### Scott Morrison (Mar 01 2021 at 23:27):

Hmm, okay, maybe I was too eager to ask for a review. :-) I'll ask again once I've finished cleaning up.

#### Scott Morrison (Mar 16 2021 at 01:03):

@Heather Macbeth, @Sebastien Gouezel I've just put up #6701, which transfers the various normed_X structures from α →ᵇ β to C(α, β) when α is compact, and proves the various equivalences/isometries.

I'm uncertain how far to go, however. Should I restate the lemmas characterising the norm/distance on α →ᵇ β? Should I e.g. transfer completeness?

I want to do this because it feels cumbersome to have to talk about α →ᵇ β (and keep providing proofs of boundedness) when you know α is compact and would naturally just talk about continuous functions. But I don't want to duplicate too much API... :-(

The same issue is going to come up for talking about functions vanishing at infinity.

Last updated: May 19 2021 at 03:22 UTC