vonNeumann bounded in product/pi type

Stream: mathlib4

[Yury G. Kudryashov]

Hi, what should we do about von Neumann boundedness in product/pi type?

• prove that the corresponding Bornology agrees with prod/pi bornologies?
• or introduce a typeclass [Bornology X] [IsVonNBornology R X] and migrate all lemmas from IsVonNBounded to this assumption?

How often do we have a Bornology instance but it is not propositionally equal to the von Neumann bornology?

[Anatole Dedecker]

Well, any time we will work in a metrizable TVS which is not normed I think (or rather, any time we would like to endow such a space with a MetricSpace instance inside a proof)

[Yury G. Kudryashov]

Then I'll go with option 1.

[Anatole Dedecker]

I think that the second approach you give is the best and, as a matter of fact, I think we should even do this for the case of metric spaces instead of forgetful inheritance.

[Anatole Dedecker]

(Essentially, I’m unhappy with having MetricSpace -> Bornology as an instance, because MetricSpace clashes with so much things that it essentially forbids making anything else an instance ever)

[Yury G. Kudryashov]

What other instances for Bornology do you have in mind?

[Yaël Dillies]

Surely you want MetricSpace -> Bornology to be an instance, else you can't talk about bounded sets?

[Anatole Dedecker]

I think one could expect to at least capture order-boundedness (above, below, and on both sides) as well as Von-Neumann.

My main complaint about the current setup is that in practice the only thing that has changed is that we now write Bornology.IsBounded instead of Metric.Bounded, and that's about it. As an example, you can check that basically none of the theorems about docs#Bornology.IsVonNBounded are not spelled in terms of docs#Bornology.vonNBornology, exactly because we have no hope of ever making it an instance without causing some diamonds in the case of metrizable TVSs.

The solution I would imagine is to have Metric.IsBounded as a notation/abbrev for PseudoMetricSpace.toBornology.IsBounded, and then have all theorems about boundedness in metric spaces assume [MetricSpace X] {b : Bornology X} [MetricBornology (b := b) X], so that they apply both to Metric.IsBounded as well as the general IsBounded for types which have canonical bornologies agreeing with the metric one. Does that make sense?

[Yaël Dillies]

Certainly, although my fingers currently hurt too much from climbing to expand on why I agree

[Anatole Dedecker]

An example I've had in mind for some time is docs#Real.isBounded_iff_bddBelow_bddAbove. The fact that we only have this for reals is completely stupid, and having a OrderBornology typeclass would make it instantly better.

[Yury G. Kudryashov]

How Lean will deduce b if you rewrite a generalize isBounded_iff_bddBelow_bddAbove from right to left?

[Yury G. Kudryashov]

Also, if Metric.IsBounded fixed defeq for b, then we can no longer use docs#IsBounded.prod with it.

[Yury G. Kudryashov]

It will produce Bornology.IsBounded (b := Bornology.prod) _

[Anatole Dedecker]

On the other hand all theorems should still apply to it because we would have an instance of MetricBornology on the product, but indeed that's a bit annoying

[Yury G. Kudryashov]

No, if you're trying to apply a theorem that assumes Metric.IsBounded s.

[Anatole Dedecker]

Yury G. Kudryashov said:

No, if you're trying to apply a theorem that assumes Metric.IsBounded s.

No theorems should assume it, they should assume [MetricBornology] instead

[Yury G. Kudryashov]

And s is in fact u × v

[Yury G. Kudryashov]

Then apply will produce a Bonology goal.

[Yury G. Kudryashov]

Also, if we never assume Metric.IsBounded, then why should we have it at all?

[Anatole Dedecker]

In order not to have to declare local instances and/or use implicit arguments in the middle of proofs

[Yury G. Kudryashov]

Looks like a footgun to me.

[Yury G. Kudryashov]

Another suggestion:

1. We make the Bornology argument explicit.
2. Metric.IsBounded is a notation for Metric.bornology.IsBounded
3. We have typeclasses like MetricBornology (b : Bornology X) : Prop where eq_metric : _ and rewrite on b.eq_metric as needed.

[Anatole Dedecker]

I'm not saying my suggestion is perfect, what I wanted to point out is that I think the canonicity-level of bornologies is more around that of measures than that of topologies.

[Anatole Dedecker]

Yury G. Kudryashov said:

Another suggestion:

1. We make the Bornology argument explicit.
2. Metric.IsBounded is a notation for Metric.bornology.IsBounded
3. We have typeclasses like MetricBornology (b : Bornology X) : Prop where eq_metric : _ and rewrite on b.eq_metric as needed.

That would work as well, but then that means not "canonical bornologies" on anything (e.g reals, where everything agrees)

[Anatole Dedecker]

Except if we do a volume-kind of trick

[Anatole Dedecker]

In fact if we have the freedom of a tactic, we could also make it so that it tries some common ones, even if they are potentially conflicting ? So that IsBounded in a space which is "only" a metric space defaults to order-boundedness ? Or would it make the statements have an ugly by block instead of Metric.bornology ?

[Yury G. Kudryashov]

Anyway, all these solutions look like medium-to-large refactors, so I'll just add a lemma about isVonNBounded_pi for now.

[Anatole Dedecker]

Sure :+1: