Completeness and compact convergence

Stream: maths

[Oliver Nash]

I just noticed that the following fails:

import Mathlib.Topology.ContinuousFunction.Compact

example : CompleteSpace C(ℝ, ℝ) := inferInstance -- fails

Can we generalise docs#ContinuousMap.instCompleteSpace to cover this?

[Oliver Nash]

More precisely:

variable {X Y : Type*} [TopologicalSpace X]

-- We have this:
example [CompactSpace X] [MetricSpace Y] [CompleteSpace Y] :
    CompleteSpace C(X, Y) :=
  inferInstance -- `ContinuousMap.instCompleteSpace`

-- But presumably this is also true:
example [CompactSpace X] [UniformSpace Y] [CompleteSpace Y] :
    CompleteSpace C(X, Y) :=
  sorry

-- And even this (with some uncertainty about assumptions on `X`):
example [LocallyCompactSpace X] [UniformSpace Y] [CompleteSpace Y] :
    CompleteSpace C(X, Y) :=
  sorry

[Jireh Loreaux]

I think they're all true. This file might be helpful in establishing them: Mathlib.Topology.UniformSpace.CompactConvergence

[Oliver Nash]

Agreed. Actually what I really wanted to know was whether this is true:

example : BaireSpace C(ℝ, ℝ) := sorry

and I now realise even given the above, it's not clear (to me, though I'd guess "yes").

Sadly I won't have time to do anything there for at least a few weeks but maybe I can nerd snipe someone :)

[Felix Weilacher]

According to this https://en.wikipedia.org/wiki/Hemicompact_space

[Felix Weilacher]

C(R,R) is metrizable, so Baire-ness will follow from completeness

[Felix Weilacher]

I guess it may be helpful to think about C(R,R) as a closed subspace of C([0,1],R)^N

[Oliver Nash]

Ah yes, thanks. Indeed looking more carefully now I see that we have docs#ContinuousMap.instIsCountablyGeneratedProdUniformityOfWeaklyLocallyCompactSpaceOfSigmaCompactSpace and so as you say completeness is sufficient. Even Lean agrees:

import Mathlib.Topology.Baire.CompleteMetrizable
import Mathlib.Topology.UniformSpace.CompactConvergence

open scoped Uniformity

example : (𝓤 C(ℝ, ℝ)).IsCountablyGenerated := inferInstance -- already exists

instance : CompleteSpace C(ℝ, ℝ) := sorry

example : BaireSpace C(ℝ, ℝ) := inferInstance -- works given the sorried completeness

[Yury G. Kudryashov]

To prove this completeness, you can use docs#UniformOnFun.instCompleteSpace with docs#UniformOnFun.isClosed_setOf_continuous

[Yury G. Kudryashov]

The right assumption on X is some kind of "compactly generated" but I didn't follow too closely which definition landed in Mathlib.

[Yury G. Kudryashov]

I was going to generalize this but forgot to do it.

[Yury G. Kudryashov]

If you're going to formalize this, then please make sure that it works both for [WeaklyLocallyCompactSpace X] and for [SequentialSpace X].

[Oliver Nash]

Oh I see you've done so much it's dead easy from here. Great!

I wasn't intending to spend any time on this but you've made it so easy I've made #16224

[Oliver Nash]

Ooooh this is quite nice: the linter complained that the new instances I added made some compactness assumptions in the Continuous Functional Calculus redundant. So I ripped them out and found a bunch more were now redundant and then shake told me an import was now redundant so it got binned too.

Basically as I battled to get CI passing, our tooling kept pointing out how to simplify the mathematics.

[Jireh Loreaux]

That's great! Thanks for simplifying our work!

[Johan Commelin]

Oliver Nash said:

Basically as I battled to get CI passing, our tooling kept pointing out how to simplify the mathematics.

And along the way forced you to spend 10x time on a "dead easy" task. There goes your nice free evening. /s :rofl:

[Johan Commelin]

Mathlib.Analysis.CStarAlgebra.ContinuousFunctionalCalculus.Restrict 1933 1393 -540 (-27.94%)

Quite a substantial import reduction! Congrats!