p-Banach spaces

Stream: condensed mathematics

[Johan Commelin]

https://github.com/leanprover-community/lean-liquid/blob/master/src/banach.lean contains

instance (p' p : ℝ) [fact (0 < p')] [fact (p' ≤ p)] [normed_space' 𝕜 p V] :
  normed_space' 𝕜 p' (as_normed_space' p' V) :=
{ norm_smul := λ c v,
  begin
    have hp' : 0 < p'   := fact.out _,
    have hp  : 0 < p    := lt_of_lt_of_le hp' (fact.out _),
    rw [norm_def, norm_def, down_smul, normed_space'.norm_smul, real.mul_rpow, ← real.rpow_mul,
      mul_div_cancel' _ hp.ne'],
    { exact norm_nonneg _ },
    { exact real.rpow_nonneg_of_nonneg (norm_nonneg _) _ },
    { exact norm_nonneg _ },
  end }

In other words: for $p' \le p$, every $p$-Banach space is also $p'$-Banach.

[Kevin Buzzard]

Nice! What needs to be done in order to state the challenge in its Ext form?

[Johan Commelin]

We need the functor TopAbGrp => Cond(Ab), and a definition of $\mathcal M_{<p}(S)$ as condensed abelian group.

[Johan Commelin]

Ooh, and we need to fill in the sorry that Cond(Ab) has enough projectives.

[Johan Commelin]

I think @Adam Topaz and @Filippo A. E. Nuccio were working on the $\mathcal M$ spaces, but maybe on the $\Z((T))$-versions, not on the $\R$-versions.

[Filippo A. E. Nuccio]

Indeed, the fact that it is a pfng-valued functor is almost done, but mainly working with the $\mathbb{Z}((T))$-version.

[Johan Commelin]

Great!

[Johan Commelin]

We'll need that version as an intermediate step in the proof.

[Johan Commelin]

@Peter Scholze Do we even need $\mathcal M(S, \Z((T))_{>r})$ and/or $\mathcal M_{< p}(S)$ for Thm 1.1 of the challenge? I think we only need the "convergent" versions right? The overconvergent versions only matter if we want to go all the way to analytic rings.

[Peter Scholze]

Johan Commelin said:

Peter Scholze Do we even need $\mathcal M(S, \Z((T))_{>r})$ and/or $\mathcal M_{< p}(S)$ for Thm 1.1 of the challenge? I think we only need the "convergent" versions right? The overconvergent versions only matter if we want to go all the way to analytic rings.

You don't need the "overconvergent" versions for the challenge (but of course you do for the analytic ring structures later).

[Johan Commelin]

@Filippo A. E. Nuccio pointed out that our definition of p-Banach spaces isn't really correct. We bundle a p-norm. But there shouldn't be a norm, just the assertion that the topology is induced by a p-norm.

Recording this here, so that we fix it at some point.

[Sebastien Gouezel]

I had to do something like that for Polish spaces. You can have a look at https://github.com/leanprover-community/mathlib/blob/759be3a933834b3822992b15d7ec112105d8b6db/src/topology/metric_space/polish.lean#L58 , the design seems to work pretty well.

[Johan Commelin]

• More seriously, we might also be missing completeness :see_no_evil:

[Filippo A. E. Nuccio]

I had proposed something along the lines of https://github.com/leanprover-community/lean-liquid/blob/master/src/banach.lean#L141 but the definition does not currently make sense: it does not connect to the topology, it was just meant to be a first trial, by defining what a p-norm was and how to state that a p-Banach is a space admitting one.

[Filippo A. E. Nuccio]

As this does not seem to be needed soon, I was planning to come back and improve this later on, and thanks @Sebastien Gouezel for the pointer at your solution for Polish spaces.

[David Michael Roberts]

I'm curious to know how Lean records things like a "p-normable" tvs. In HoTT, for instance, one would have a type whereby the p-norm giving rise to the topology "merely" exists as part of the data. One could of course use some theorem characterising the topology, but then this might make a bad API.

[Adam Topaz]

I'm not sure what you mean by ""merely" exists as part of the data", but if I were to make a guess, that would be similar to how we define docs#metric_space . We could of course do something similar in this case.

[Adam Topaz]

The point is that both the metric and topology are part of the data, along with props ensuring their compatibility.

[Adam Topaz]

(in this case the topology is a couple of layers down, under the pseudo metric space, then under the uniform space structure, so you will have some links to click if you look through the docs)

[David Michael Roberts]

I mean in the technical sense: a piece of data of type T "merely" exists, if the proposition ||T|| is true, where ||-|| is the (-1)-truncation construction.

[Adam Topaz]

Ah ok. So in that case we could say "there exists a metric (or p-norm) which induces the given topology". I suppose that's how we might formalize this in lean.

[Johan Commelin]

"merely" existing could be done using docs#trunc

[Johan Commelin]

But since we are fully using classical logic anyways, we might just as well use ∃.

[David Michael Roberts]

Oh, that would do it. I guess my brain is automatically set to constructive mode when dealing with type theory :upside_down:

[Johan Commelin]

I pushed a fix. So p-Banach spaces are now complete TVS's whose topology is induced by a p-norm.
(As opposed to coming equipped with a distinguished p-norm.)