completion of a normed space

Stream: Is there code for X?

[Yury G. Kudryashov]

I want to have an instance for normed_space 𝕜 (completion E). Am I right that the mathlib way is to define a typeclass for ∀ c, uniform_continuous ((•) c) and use it to define the whole hierarchy of actions?

[Yury G. Kudryashov]

My goal is to drop [complete_space E] assumptions in some theorems from complex analysis that use integrals in their proofs by applying the original theorem to (coe : E → completion E) ∘ f.

[Johan Commelin]

Note that normed_group (completion E) should already exist. But you are probably aware of that already.

[Riccardo Brasca]

It's docs#uniform_space.completion.normed_group

[Yury G. Kudryashov]

I see that the multiplication docs#uniform_space.completion.has_mul and addition docs#uniform_space.completion.has_add are defined in a completely different way. The reason is that the multiplication in a uniform ring is not uniformly continuous.
@Patrick Massot what is the right way to define multiplication on completion M so that it works in all reasonable cases? Do we need a new typeclass (something weaker than not-yet-existing has_uniform_continuous_mul)?

[Kevin Buzzard]

Multiplication is almost never uniformly continuous -- this is one of Patrick's favourite facts! For example it's not uniformly continuous on the rationals so Bourbaki have to deal with this when defining the reals. I'm confused about whether you think this example is "reasonable". IIRC there's something about this in the perfectoid paper.

[Patrick Massot]

The key point is https://github.com/leanprover-community/mathlib/blob/213e2ed70129fb145dadb94b130f144d8a3355a4/src/topology/algebra/uniform_group.lean#L465-L468

[Yury G. Kudryashov]

I understand that (*) is not uniform continuous, e.g., in a normed ring. Should we introduce something like docs#completable_top_field but for multiplication?

[Yury G. Kudryashov]

Another question. Once we have normed_space K (completion E), we can also introduce normed_space (completion K) (completion E) but in the case K = E this will create a diamond. What should we do?

[Yury G. Kudryashov]

But we can postpone these questions for another few years if @Sebastien Gouezel 's planned refactor of Bochner integral will work for non-complete codomains too.

[Yury G. Kudryashov]

I only want normed_space K (completion E) because I don't like the way some of the theorems in complex analysis are currently formulated.

[Yury G. Kudryashov]

Actually, if we only need normed_space K (completion E), then we can do this: #12148

[Sebastien Gouezel]

Yury G. Kudryashov said:

But we can postpone these questions for another few years if Sebastien Gouezel 's planned refactor of Bochner integral will work for non-complete codomains too.

No, completeness of the codomain is non-negotiable here, sorry :-)

[Yury G. Kudryashov]

Then I'll use embedding to completion E to get rid of this assumption.