Zulip Chat Archive

Stream: condensed mathematics

Topic: analytic theorem 9.4


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

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

view this post on Zulip Johan Commelin (Dec 08 2020 at 18:13):

that's a very brief summary

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:13):

Does ```math work?

view this post on Zulip Johan Commelin (Dec 08 2020 at 18:13):

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

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:14):

A+B=CA + B = C

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:14):

I guess not.

view this post on Zulip Reid Barton (Dec 08 2020 at 18:14):

A+B=CA + B = C? wrong theorem

view this post on Zulip Reid Barton (Dec 08 2020 at 18:15):

```math is like \[ \]

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

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

Which feeds into:

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

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

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:23):

I guess we have docs#normed_space and docs#complete_space

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:23):

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

view this post on Zulip Kevin Buzzard (Dec 08 2020 at 18:26):

you might only need a uniform space structure

view this post on Zulip Riccardo Brasca (Dec 08 2020 at 18:28):

There is to_metric_space for any normed_group docs#normed_group

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:30):

(deleted)

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:42):

I think we can get p-banach spaces

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

view this post on Zulip Johan Commelin (Dec 08 2020 at 18:48):

Is that what we want?

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

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:52):

This doesn't work does it...

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:55):

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

view this post on Zulip Adam Topaz (Dec 08 2020 at 18:56):

I think this is incompatible with [normed_space ℝ V]

view this post on Zulip Johan Commelin (Dec 08 2020 at 19:00):

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

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

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

view this post on Zulip Adam Topaz (Dec 08 2020 at 19:08):

I didn't check if that typechecks

view this post on Zulip Johan Commelin (Dec 08 2020 at 19:10):

It does

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

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

view this post on Zulip Johan Commelin (Dec 08 2020 at 19:24):

Hmm, thanks for that remark!

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

view this post on Zulip Adam Topaz (Dec 08 2020 at 19:41):

Functional analysis stream?

view this post on Zulip Frédéric Dupuis (Dec 08 2020 at 19:41):

Or just maths

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

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

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

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

view this post on Zulip Reid Barton (Dec 08 2020 at 21:05):

triangle equality

view this post on Zulip Frédéric Dupuis (Dec 08 2020 at 21:05):

Oops! Let me correct that.

view this post on Zulip Patrick Massot (Dec 08 2020 at 21:06):

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

view this post on Zulip Frédéric Dupuis (Dec 08 2020 at 21:07):

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


Last updated: May 09 2021 at 16:20 UTC