bound_by

Stream: condensed mathematics

[Riccardo Brasca]

I started the work to refactor LTE to get rid of bound_by, in branch byebye-bound_by. I started working on a random place where it was used, just to have an idea about what I have to do, and I chose double_complex.d_one_norm_noninc in src/thm95/double_complex.lean.

Can someone have a look of what I've done, just to check that is reasonable? This is the relevant commit. To start with, I decided to keep norm_noninc, adding norm_noninc_iff_norm_le_one. Of course sooner or later we should also get rid of norm_noninc.

[Johan Commelin]

Nice branch name :rofl:
Maybe norm_noninc can stay? I don't know. @Sebastien Gouezel @Patrick Massot what do you think? With norm_noninc you don't have the 1 * _ appearing that you would otherwise.

[Riccardo Brasca]

Ah yes, that's why we introduce it!

[Patrick Massot]

I understand the 1 * _ can be annoying if it comes up a lot. I also understand this special case has nicer composition behavior so maybe we need some category using this as morphisms.

[Patrick Massot]

I think having bound_by duplicating the operator norm stuff is ridiculous, but the norm_noninc special case may be worth the trouble.

[Adam Topaz]

We have the category with non increasing morphisms in mathlib

[Adam Topaz]

docs#SemiNormedGroup₁

[Adam Topaz]

My inclination is still that SemiNormedGroup should be considered as something like a seminormed category a la

https://github.com/leanprover-community/lean-liquid/blob/semi-normed-category/src/for_mathlib/seminormed_category/basic.lean

along with the notion of bounded (co)limits, or something similar. But this is probably too experimental even for the LTexperiment…

[Riccardo Brasca]

OK, I will keep norm_noninc

[Riccardo Brasca]

I will start merging my branch to master if the build succeed. bound_by is used a lot, but replacing it with the norm condition it's not difficult.

[Riccardo Brasca]

LTE is normed_group_hom.bound_by free. (Note that if you search bound_by you still get a lot of results, some of them are in the for_mathlib folder and are useless, and the others refer to different notion of bound_by).

[Riccardo Brasca]

If someone has some time I noticed two simple cleanups:

• all the stuff about completion of normed_group in src/locally_constant/Vhat.lean are already in the for_mathlib folder.
• src/prop_92/concrete.lean contains some lemmas about geometric series that I think are in mathlib, or at least should go to to mathlib.

I can do them tomorrow if nobody wants to do them.

[Johan Commelin]

@Riccardo Brasca Great! Thanks a lot for doing this

[Johan Commelin]

fyi: I bumped mathlib

[Riccardo Brasca]

I am taking care of src/locally_constant/Vhat.lean.

[Patrick Massot]

I'll work on geometric series now

[Patrick Massot]

See #7858. This takes care of specific_limits, pseudo_metric and part of normed_group

[Johan Commelin]

@Riccardo Brasca So what is the status with bound_by? I guess we can now rip the defn out of mathlib?

[Riccardo Brasca]

Yes, it is in my todo list

[Riccardo Brasca]

bound_by has been removed from mathlib. This shouldn't cause any problem in the next mathlib bump :)

[Kevin Buzzard]

Bye bye bound_by!

[Johan Commelin]

I'll try bumping mathlib now

[Johan Commelin]

Done. Thanks @Riccardo Brasca, that went really smooth!

[Riccardo Brasca]

I will see next week what can I do about has_nnnorm.

[Riccardo Brasca]

Creating the class is of course very easy, but I guess that using it everywhere in LTE requires a little work

[Johan Commelin]

Mathlib might be even easier. Not sure how much nnnorm is used there :wink:

[Riccardo Brasca]

What is a reasonale notation for nnnorm? Lean doesn't like

class has_nnnorm (α : Type*) := (nnnorm : α → ℝ≥0)

export has_nnnorm (nnnorm)

notation `∥`:1024 e:1 `∥₊`:1 := nnnorm e

I got tons of errors in analys/normed_space/basic if I add these lines... I think this is because with this notation when Lean sees ∥x∥ it gets confused.

notation `∥₊`:1024 e:1 `∥`:1 := nnnorm e

works, but it seems quite unnatural...

[Riccardo Brasca]

#7986