sup norm on continuous functions?

Stream: Is there code for X?

[Scott Morrison]

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

[Heather Macbeth]

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

[Scott Morrison]

Thanks.

[Scott Morrison]

Do we have something that provides

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

[Heather Macbeth]

Are you assuming compactness of X?

[Scott Morrison]

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

[Heather Macbeth]

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

[Heather Macbeth]

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]

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

[Kevin Buzzard]

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

[Heather Macbeth]

Yup, that also exists! docs#bounded_continuous_function.normed_group

[Scott Morrison]

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]

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

[Heather Macbeth]

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]

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]

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]

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]

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

[Scott Morrison]

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?

[Scott Morrison]

Ah! docs#metric.uniform_continuous_iff

[Heather Macbeth]

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

[Scott Morrison]

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

[Heather Macbeth]

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

[Scott Morrison]

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]

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

[Scott Morrison]

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.

[Heather Macbeth]

Very exciting!

[Scott Morrison]

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]

(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]

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

[Scott Morrison]

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