analytic theorem 9.4

Stream: condensed mathematics

[Kevin Buzzard]

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

  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]

that's a very brief summary

[Adam Topaz]

Does ```math work?

[Johan Commelin]

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

[Adam Topaz]

$$A + B = C$$

[Adam Topaz]

I guess not.

[Reid Barton]

$A + B = C$? wrong theorem

[Reid Barton]

```math is like \[ \]

[Adam Topaz]

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]

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]

I guess we have docs#normed_space and docs#complete_space

[Adam Topaz]

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

[Kevin Buzzard]

you might only need a uniform space structure

[Riccardo Brasca]

There is to_metric_space for any normed_group docs#normed_group

[Adam Topaz]

(deleted)

[Adam Topaz]

I think we can get p-banach spaces

[Johan Commelin]

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]

Is that what we want?

[Adam Topaz]

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]

This doesn't work does it...

[Adam Topaz]

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

[Adam Topaz]

I think this is incompatible with [normed_space ℝ V]

[Johan Commelin]

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

[Johan Commelin]

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]

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]

I didn't check if that typechecks

[Johan Commelin]

It does

[Adam Topaz]

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]

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]

Hmm, thanks for that remark!

[Frédéric Dupuis]

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]

Functional analysis stream?

[Frédéric Dupuis]

Or just maths

[Johan Commelin]

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

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]

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]

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

[Reid Barton]

triangle equality

[Frédéric Dupuis]

Oops! Let me correct that.

[Patrick Massot]

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

[Frédéric Dupuis]

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