Completeness of padics

Stream: Is there code for X?

[Sebastien Gouezel]

I can't find the instance that ℚ_[p] is a complete metric space -- there are many related things, but I can't find this precise one. Is it really missing?

[Johan Commelin]

It is defined as a completion, right? So that would be very surprising

[Johan Commelin]

Aah, we have

instance complete : cau_seq.is_complete ℚ_[p] norm :=

[Patrick Massot]

This is not what Sébastien is looking for

[Patrick Massot]

The issue is that this completion is defined by hand using Cauchy sequences of rationals, not through the general machinery of uniform spaces (or even metric spaces).

[Patrick Massot]

You need some glue like in docs#real.complete_space

[Sebastien Gouezel]

Hopefully there is the correspondance between the two notions somewhere in mathlib. I'm just surprised that the instance does not seem to be here.

[Patrick Massot]

Maybe it hasn't been written for p-adics

[Johan Commelin]

Yes, we clearly need to show that $\mathbb Q_p$ admits an "abstract completion package"

[Patrick Massot]

That instance for real makes me pessimistic that the p-adic version exists. Otherwise we would have a generalization covering both.

[Patrick Massot]

And as Johan wrote, you can also go through the route in topology.uniform_space.compare_real

[Sebastien Gouezel]

It's not that I'm interested in padics :-), but this would have been a nice example for my talk of today in Lorentz center. I'll pick another one, then.

[Patrick Massot]

When is that talk?

[Patrick Massot]

And I must admit I was curious to read how you realized that you need completeness of p-adics to prove a proper version of the change of variable formula.

[Sebastien Gouezel]

2:30
:-)

[Patrick Massot]

Without bors taking ages this would be fine.

[Patrick Massot]

I'll try something anyway, but I can't do it right now.

[Sebastien Gouezel]

I'll be in a particular branch anyway. And I really don't need this, it's just that I wanted to share my surprise it's not there.

[Sebastien Gouezel]

Patrick Massot said:

And I must admit I was curious to read how you realized that you need completeness of p-adics to prove a proper version of the change of variable formula.

The proper version of the change of variable formula is ready (https://github.com/leanprover-community/mathlib/blob/b472a7d1eb4134b907c913b67a889bcefc131da5/src/measure_theory/function/jacobian.lean#L1255), and does not use padics. Not clear how long it takes to get in mathlib, though, because #12220 is already hard to get in...

[Patrick Massot]

The issue is deeper than completion. Even the metric space structure is done in an ad-hoc way for reals and padics

[Patrick Massot]

And I need to go so I probably won't have time to fix this before your talk

[Patrick Massot]

I had a bit more time in the end so I gave up and duplicated the ad hoc code we have for real. See #12424

[Patrick Massot]

@Sebastien Gouezel

[Patrick Massot]

Bors failed with

 Error: /home/lean/actions-runner/_work/mathlib/mathlib/src/algebraic_topology/simplex_category.lean:1:0:
file 'category_theory/reflects_isomorphisms' not found in the search path

I claim this has nothing to do with my change...

[Sebastien Gouezel]

Next PR on the road to the change of variables formula is ready, in #12437. Unfortunately again a little bit longish, and mathematically a little bit exotic, unless you're into Polish spaces and tweaking topologies on a given type.