Zulip Chat Archive

Stream: Is there code for X?

Topic: sup norm on continuous functions?


view this post on Zulip Scott Morrison (Feb 28 2021 at 08:12):

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

view this post on Zulip Heather Macbeth (Feb 28 2021 at 08:13):

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

view this post on Zulip Scott Morrison (Feb 28 2021 at 08:13):

Thanks.

view this post on Zulip 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

view this post on Zulip Heather Macbeth (Feb 28 2021 at 08:14):

Are you assuming compactness of X?

view this post on Zulip Scott Morrison (Feb 28 2021 at 08:14):

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

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Feb 28 2021 at 08:18):

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

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Feb 28 2021 at 09:00):

Yup, that also exists! docs#bounded_continuous_function.normed_group

view this post on Zulip 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?

view this post on Zulip 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 →ᵇ?

view this post on Zulip 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.

view this post on Zulip 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.

view this post on Zulip 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?

view this post on Zulip 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?

view this post on Zulip 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 →ᵇ!

view this post on Zulip 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?

view this post on Zulip Scott Morrison (Feb 28 2021 at 09:54):

Ah! docs#metric.uniform_continuous_iff

view this post on Zulip Heather Macbeth (Feb 28 2021 at 09:56):

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

view this post on Zulip 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?

view this post on Zulip Heather Macbeth (Feb 28 2021 at 10:25):

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

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Feb 28 2021 at 16:38):

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

view this post on Zulip 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.

view this post on Zulip Heather Macbeth (Mar 01 2021 at 23:13):

Very exciting!

view this post on Zulip 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.

view this post on Zulip 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.)

view this post on Zulip 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.

view this post on Zulip 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