## Stream: condensed mathematics

### Topic: analytic theorem 9.4

#### Kevin Buzzard (Dec 08 2020 at 18:11):

@Johan Commelin was talking about about formalising the _statement_ of 9.4 of Analytic.pdf as a good short term goal. What needs to be done here Johan?

#### Johan Commelin (Dec 08 2020 at 18:13):

  this theorem statement requires us to formalise the following definitions:
\begin{itemize}
\item $p$-Banach spaces
\item profinite sets
\item the construction $V \mapsto \hat V$
\item the profinite sets $\bar{\mathcal M}_{p'}(S)$
\item the statement of the Breen--Deligne resolution,
which feeds into:
\item the complex $C_c^\bullet$
\item the notion of $\le k$-exactness in degree $\le m$
\end{itemize}


#### Johan Commelin (Dec 08 2020 at 18:13):

that's a very brief summary

#### Adam Topaz (Dec 08 2020 at 18:13):

Does  math  work?

#### Johan Commelin (Dec 08 2020 at 18:13):

doesn't seem to be an option
result isn't very nice

#### Adam Topaz (Dec 08 2020 at 18:14):

$A + B = C$

I guess not.

#### Reid Barton (Dec 08 2020 at 18:14):

$A + B = C$? wrong theorem

#### Reid Barton (Dec 08 2020 at 18:15):

 math  is like 

#### Adam Topaz (Dec 08 2020 at 18:16):

I guess markdown works (just typesetting Johan's message above):

This theorem statement requires us to formalise the following definitions:

• $p$-Banach spaces
• profinite sets
• the construction $V \mapsto \widehat V$
• the profinite sets $\overline{\mathcal M}_{p'}(S)$
• the statement of the Breen--Deligne resolution,

Which feeds into:

• the complex $C_c^\bullet$
• the notion of $\le k$-exactness in degree $\le m$

#### Kevin Buzzard (Dec 08 2020 at 18:20):

Do we have Banach spaces or is it one of those things like number fields when when you come to write down the definition you find that it's just a bunch of typeclasses and you feel a bit silly doing it? ([field K] [algebra rat K] [finite_dimensional rat K])

#### Adam Topaz (Dec 08 2020 at 18:23):

I guess we have docs#normed_space and docs#complete_space

#### Adam Topaz (Dec 08 2020 at 18:23):

I assume there is a metric space instance induced by a normed space somewhere...

#### Kevin Buzzard (Dec 08 2020 at 18:26):

you might only need a uniform space structure

#### Riccardo Brasca (Dec 08 2020 at 18:28):

There is to_metric_space for any normed_group docs#normed_group

(deleted)

#### Adam Topaz (Dec 08 2020 at 18:42):

I think we can get p-banach spaces

#### Johan Commelin (Dec 08 2020 at 18:48):

import analysis.normed_space.basic

/-- Called an r-Banach space in [Analytic].

Officially we need 0 < r < 1, but maybe we only want to assume that in theorems.
Otoh, we might want to use r : nnreal, or maybe even r : preal after introducing preal. -/
class quasibanach (r : ℝ) (V : Type*) :=
[normed_group  : normed_group V]
[normed_space  : normed_space ℝ V]
[compact_space : compact_space V]
(T : V →+ V)
(norm_mul_T : ∀ v, ∥T v∥ = r • ∥v∥)


#### Johan Commelin (Dec 08 2020 at 18:48):

Is that what we want?

#### Adam Topaz (Dec 08 2020 at 18:51):

I'm thinking to define this

import data.set.intervals.basic
import data.real.basic
import analysis.normed_space.basic
import analysis.special_functions.pow

noncomputable theory

open set

@[derive field]
def rr {p : ℝ} (hp : p ∈ Ioo (0 : ℝ) 1) := ℝ

namespace rr
instance {p : ℝ} {hp : p ∈ Ioo (0 : ℝ) 1} : normed_field (rr hp) :=
{ norm := λ (x : ℝ), ∥x∥^p,
dist := λ (x : ℝ) y, ∥x - y∥^p,
dist_self := _,
eq_of_dist_eq_zero := _,
dist_comm := _,
dist_triangle := _,
edist := _,
edist_dist := _,
to_uniform_space := _,
uniformity_dist := _,
dist_eq := _,
norm_mul' := _,
..(infer_instance : field _) }

end rr


#### Adam Topaz (Dec 08 2020 at 18:52):

This doesn't work does it...

#### Adam Topaz (Dec 08 2020 at 18:55):

Take a look at definition 6.1 in analytic.pdf, item 2, for example.

#### Adam Topaz (Dec 08 2020 at 18:56):

I think this is incompatible with [normed_space ℝ V]

#### Johan Commelin (Dec 08 2020 at 19:00):

@Adam Topaz You are right. I should have taken a closer look

#### Johan Commelin (Dec 08 2020 at 19:06):

import analysis.normed_space.basic
import analysis.special_functions.pow

class quasinormed_space (r : ℝ) (V : Type*) [normed_group V]
extends semimodule ℝ V :=
(norm_smul : ∀ (x:ℝ) (v:V), ∥x • v∥ = ∥x∥^r * ∥v∥)


is hopefully a bit better (though this doesn't include the completeness from def 6.1)

#### Adam Topaz (Dec 08 2020 at 19:08):

Maybe with completeness?

import analysis.normed_space.basic
import analysis.special_functions.pow

class quasinormed_space (r : ℝ) (V : Type*) [normed_group V] [complete_space V]
extends semimodule ℝ V :=
(norm_smul : ∀ (x:ℝ) (v:V), ∥x • v∥ = ∥x∥^r * ∥v∥)


#### Adam Topaz (Dec 08 2020 at 19:08):

I didn't check if that typechecks

It does

#### Adam Topaz (Dec 08 2020 at 19:16):

My thought was to define the rr p gadget above, and that a "banach space" over rr p is a p-banach space

#### Frédéric Dupuis (Dec 08 2020 at 19:22):

I'm not sure it's such a good idea to have a definition where V already needs to have a norm, because then you're forced to only pick one r for the type (i.e. the one that agrees with the previously defined norm) and can't move between norms as one usually wants to do here. For example, even stating something like Hölder's inequality would be annoying with this kind of definition.

#### Johan Commelin (Dec 08 2020 at 19:24):

Hmm, thanks for that remark!

#### Frédéric Dupuis (Dec 08 2020 at 19:40):

Also, it might make sense to move this particular discussion to a more general stream, I just had a look at this stream purely out of curiosity and stumbled on a topic I was interested in -- I'm absolutely not qualified to work on condensed mathematics!

#### Adam Topaz (Dec 08 2020 at 19:41):

Functional analysis stream?

Or just maths

#### Johan Commelin (Dec 08 2020 at 20:11):

@Frédéric Dupuis I think we are all just trying to find our way in this new field. I don't have any experience in functional analysis. So it would be great if this becomes a joint effort of the leanprover/mathlib community.

#### Frédéric Dupuis (Dec 08 2020 at 20:41):

Indeed! I just meant that condensed math is pretty intimidating for people like me who aren't pure mathematicians at all and might end up missing, say, a discussion on Banach spaces to which they might actually have something to contribute.

#### Frédéric Dupuis (Dec 08 2020 at 20:58):

I was thinking some more about this p-norm issue, and I was wondering if a definition like this would make sense:

class normed_group_family (ι : Type*) (α : Type*) (p : (ι → α → ℝ) → Prop) [add_comm_group α] :=
(norm : ι → α → ℝ)
(norm_eq_zero_iff : ∀ (r : ι) (x : α), norm r x = 0 ↔ x = 0)
(triangle : ∀ (r : ι) (x y : α), norm r (x + y) ≤ norm r x + norm r y)
(norm_neg : ∀ (r : ι) (x : α), norm r (-x) = norm r x)
(property : p norm)


This would be a general typeclass for families of norms that satisfy some property p. We could then duplicate part of the code for norms and have a function that could turn any of the members of the family into the standard norm instance on the type. For types that already have a norm defined on it, we could have another typeclass that says that the standard norm is equal to one of the members of the family.

#### Johan Commelin (Dec 08 2020 at 21:04):

@Frédéric Dupuis interesting idea. (btw, there's a typo in the triangle field... both sides are the same)

#### Reid Barton (Dec 08 2020 at 21:05):

triangle equality

#### Frédéric Dupuis (Dec 08 2020 at 21:05):

Oops! Let me correct that.

#### Patrick Massot (Dec 08 2020 at 21:06):

That new version doesn't sound like it would type-check

#### Frédéric Dupuis (Dec 08 2020 at 21:07):

Indeed... We'll get there! :-)

Last updated: May 09 2021 at 16:20 UTC