Zulip Chat Archive

What do you have in mind? Do you want to show is_bounded_map f for all bounded linear maps f? because that's not how it works since the hom refactor.

Adam Topaz (Feb 15 2022 at 00:36):

Why isn't the predicate on sets called is_bounded btw to be consistent with is_open?

Yaël Dillies (Feb 15 2022 at 00:37):

Well, actually, it is called like that.

Yury G. Kudryashov (Feb 15 2022 at 00:37):

BTW we have docs#bounded and docs#metroc.bounded

Yaël Dillies (Feb 15 2022 at 00:37):

No, it's docs#set.bounded since @Violeta Hernández came along.

Yury G. Kudryashov (Feb 15 2022 at 00:37):

Ah, the former is now called docs#set.bounded

Adam Topaz (Feb 15 2022 at 00:38):

Oh I thought you were complaining at my suggestion for the name bounded for the predicate on maps because it conflicts with the name for sets.

Adam Topaz (Feb 15 2022 at 00:39):

I honestly don't really care about names. But I do think we should try to be consistent.

Yaël Dillies (Feb 15 2022 at 00:39):

Ah no, I complained because it was not obviously about functions and could easily be confused with several predicates about sets.

Adam Topaz (Feb 15 2022 at 00:40):

Now what's the issue with bounded linear maps? I haven't been following the morphism refactor.

Yaël Dillies (Feb 15 2022 at 00:42):

I'm asking you what you expect from the unbundled predicate. If there is some type such that all its terms are (mathematically, not in Lean) bounded_maps, then this type will get a bounded_map_class instance rather than a lemma saying all its terms respect is_bounded_map.

Adam Topaz (Feb 15 2022 at 00:44):

How would you define a bounded linear map?

Yaël Dillies (Feb 15 2022 at 00:46):

What do you mean? docs#is_bounded_linear_map is already a thing, but I don't know if that's what you're referring to. You're the one who brought them up.

Adam Topaz (Feb 15 2022 at 00:49):

Yury asked whether we should have an unbundled version. What I was suggesting is that it would be worthwhile to have because we have definitions, like bounded linear maps, which impose boundedness as a predicate in addition to some other property, like linearity. Similarly to how continuity can be dropped in to define continuous multiplication, etc. If we only had a bundled version, defining such things would get annoying.

Yaël Dillies (Feb 15 2022 at 00:51):

Sorry, my brain is bundled. I cannot comprehend such thoughts :grinning:

Yaël Dillies (Feb 15 2022 at 00:51):

#12046 for bounded_map
#12045 for Born

Yaël Dillies (Feb 15 2022 at 00:54):

Honestly, I'm not qualified to know whether we need the unbundled predicate. My job is the bundled type. Feel free to add the unbundled version if you feel like it's needed. Just be aware of what the bundled type can do.

Yury G. Kudryashov (Feb 15 2022 at 01:23):

Sorry if my question was written in a way that suggested negative answer. I just thought that this is a question that should be asked. If the unbundled version is useful, then we should have it.

Jireh Loreaux (Feb 15 2022 at 01:54):

If you want the unbundled version I wrote, it's sitting in a commit on the branch for #12036, but it should be moved and renamed according to the above.

Yaël Dillies (Feb 15 2022 at 10:22):

Could you also add a class bounded_space that says bounded univ?

Yaël Dillies (Feb 15 2022 at 10:28):

It seems there are two (incompatible?) ways to get a bornology from a metric space. One is to declare bounded all sets which are contained in some ball, the other is to get the topology induced by the metric and declare bounded the sets whose closure is compact.

Yaël Dillies (Feb 15 2022 at 10:28):

This also suggests topological_space should extend bornological_space. Do not do this in #12036 though.

Yaël Dillies (Feb 15 2022 at 10:29):

Can you also a reducible non-instance bornological_space.cofinite (not sure about the name) where cobounded := cofinite?

Yaël Dillies (Feb 15 2022 at 10:30):

Then we'll get the nice instance compact_space -> bounded_space.

Yaël Dillies (Feb 15 2022 at 10:32):

Once we have bornological_space in, I'll define bornological_module and convex_bornological_module.

Yaël Dillies (Feb 15 2022 at 10:37):

Oh actually I think we have a naming problem. On Wikipedia, a bornological space is not a space with a bornology, but rather a space where we can recover the topology from the bornology.

Jireh Loreaux (Feb 15 2022 at 13:49):

Right, the metric and topological versions are incompatible in general because any metric space is homeomorphic to the same space with a bounded metric.

Jireh Loreaux (Feb 15 2022 at 13:54):

So for metric spaces the bornology should be the metric (co)bounded sets, not the ones from the topology.

Yaël Dillies (Feb 15 2022 at 13:55):

That means you can't consider topological spaces as bornological spaces however.

Jireh Loreaux (Feb 15 2022 at 13:56):

Oh sorry, we do have a naming problem. I didn't catch that distinction on my read through. I guess we just use bornology?

Yaël Dillies (Feb 15 2022 at 13:56):

I'm happy with bornology_space, if that makes for a more coherent naming scheme.

Jireh Loreaux (Feb 15 2022 at 13:58):

Then we would end up having both bornology_space and bornological_space, which I think could get confusing.

Yaël Dillies (Feb 15 2022 at 13:59):

Eh, not our fault. You got confused too :stuck_out_tongue:

Jireh Loreaux (Feb 15 2022 at 13:59):

Right, topological spaces shouldn't get a bornology instance automatically.

Jireh Loreaux (Feb 15 2022 at 14:00):

But I don't think we should contribute to the confusion. My preference I think it's for bornology.

Yaël Dillies (Feb 15 2022 at 14:00):

Do you know anything about bornology or are you just reading the Wikipedia like I am? Would be nice if someone had working experience with them to guide us.

Jireh Loreaux (Feb 15 2022 at 14:01):

No, I don't have experience.

Adam Topaz (Feb 15 2022 at 14:01):

I'm sure Patrick would suggest to follow Bourbaki in this case...

Jireh Loreaux (Feb 15 2022 at 16:10):

So, Bourbaki distinguishes a bornology from a covering bornology, where the latter includes the condition that the union of the bounded sets is the entire space, but it seems that this has since just been included in the definition. Moreover, notice there are two wikipediea pages bornology and bornological space. In the former, it looks like they call the cobounded sets the filter at infinity (although I personally prefer cobounded, especially because of the comap definition of bounded maps). A quick text search of Bourbaki seems to suggest they don't refer to this filter at all, but it's possible I missed it.

Rémi Bottinelli (Feb 15 2022 at 16:49):

@Daniel Roca González would probably be interested in this, since he's working on coarse structures (which seems to be a bit of a stronger concept).

Jireh Loreaux (Feb 15 2022 at 16:53):

@Yaël Dillies I have pushed the changes suggested above and used the bornology terminology to be consistent with Bourbaki and Wikipedia.

Yury G. Kudryashov (Feb 15 2022 at 18:24):

We can have a type synonym for the "closure is compact" bornology

Kyle Miller (Feb 15 2022 at 18:24):

Jireh Loreaux said:

In the former, it looks like they call the cobounded sets the filter at infinity (although I personally prefer cobounded, especially because of the comap definition of bounded maps).

That was why I'd named it infty earlier, but cobounded makes more sense to me. Wikipedia cites https://www.worldcat.org/title/topological-vector-spaces/oclc/144216834 which seems like it would be good to take a look at.

Daniel Roca González (Feb 15 2022 at 18:26):

Rémi Bottinelli said:

Daniel Roca González would probably be interested in this, since he's working on coarse structures (which seems to be a bit of a stronger concept).

I haven't had time to work on it for some weeks, but yes it's definitely related.

Kyle Miller (Feb 15 2022 at 18:42):

Terminology from Chapter 6 of Narici and Beckenstein, "Topological Vector Spaces":

a bornology or boundedness for the structure. Elements of the set of subsets are bounded sets. The definition consists of the covering condition and closure under subsets and finite unions.
T along with bornology T is a bounded structure
the bornology of bounded sets of a topological vector space is usual bornology or natural boundedness
the bornology of relatively compact sets of a topological space is the compact bornology
the cobounded sets according to a bornology form the filter at infinity
mentions definitions for the base and subbase of a bornology, generating bornologies, weaker/stronger bornologies, etc.
if f : A -> B is a function and (A, S) and (B, T) are bounded structures, and if f carries bounded sets to bounded sets, then f is locally bounded. If f is invertible and both f and the inverse of f are locally bounded, then f is a bornomorphism
a bornology on a vector space is a vector bornology if scalar multiplication and addition are locally bounded (using the natural bornologies on product spaces)
exercise 6.111 defines bornivorous subsets of a topological vector space (synonym: the set is a bornivore)
exercise 6.203 describes two constructions to create new bornologies from a bornology on a topological space: taking closures and taking interiors of the bounded sets.

Kyle Miller (Feb 15 2022 at 18:52):

It seems to me that [bornology T] and locally_bounded f could be the names, with locally_bounded_map for the homs.

Yaël Dillies (Feb 15 2022 at 18:53):

I don't quite understand the "local" part of the names. Is there another notion of bounded map?

Yaël Dillies (Feb 15 2022 at 18:53):

Aaah, maps with a uniform bound?

Kyle Miller (Feb 15 2022 at 18:54):

Yeah

Kyle Miller (Feb 15 2022 at 18:54):

The identity map reals -> reals with the usual bornology on reals is locally bounded (and a bornomorphism).

Yaël Dillies (Feb 15 2022 at 18:55):

I will change the name in #12046 then.

Yaël Dillies (Feb 15 2022 at 18:56):

I'm not defining bornomorphisms yet because I'm waiting for @Anne Baanen's equiv refactor (or is it usable already?)

Jireh Loreaux (Feb 15 2022 at 19:55):

We don't have a definition for maps with a uniform bound do we? Isn't is just bounded (range f)

Yaël Dillies (Feb 15 2022 at 19:56):

Yes to both.

Jireh Loreaux (Feb 15 2022 at 19:59):

Personally, I would prefer to see just bounded_map as opposed to locally_bounded_map, but I understand if the majority is not with me on this. In many cases where bornology is useful (functional analysis) the maps are just called bounded anyway.

Yaël Dillies (Feb 15 2022 at 20:00):

What about borned_map? This is apparently nonstandard, but follows quite the "born..." terminology.

Kyle Miller (Feb 15 2022 at 20:04):

Another terminology note that I forgot to mention: a reason I proposed bornology a few messages back versus bornological_space is that a bornological space is a locally convex vector space X such that every locally bounded linear map X -> Y with Y a locally convex vector space is continuous. (Section 13.2 of the book.)

Jireh Loreaux (Feb 15 2022 at 20:04):

Yes, thanks Kyle, we realized that just a bit earlier in the thread. I didn't read carefully enough the first time.

Jireh Loreaux (Feb 15 2022 at 20:06):

I mean, if we go with the french, then why not bornee_map? I like it.

Yaël Dillies (Feb 15 2022 at 20:07):

Half correct French is a bit painful for me to read.

Jireh Loreaux (Feb 15 2022 at 20:07):

Or is it just borne? I don't know the gender of "map" in french.

Yaël Dillies (Feb 15 2022 at 20:07):

«map_bornée» :upside_down:

Jireh Loreaux (Feb 15 2022 at 20:09):

I originally suggested it with the accent before I realized it wasn't an allowable character in declarations and had to be quoted.

Yaël Dillies (Feb 15 2022 at 20:12):

Yeah...

Patrick Massot (Feb 15 2022 at 20:13):

And that's why we don't have the étale topology in mathlib

Kyle Miller (Feb 15 2022 at 20:16):

I don't really have a hat in the ring here, but locally_bounded seems to be the most self-explanatory name (bounded feels like "uniformly bounded," and, apologies to the francophones, all the words associated to bornology seem more like made-up words to me than usual...)

Kyle Miller (Feb 15 2022 at 20:16):

Ignoring bornologies, I think the usual notion of "locally bounded" is that each point in the domain has a neighborhood whose image is bounded. This seems to carry over to maps between topological vector spaces with their usual bornologies.

Patrick Massot (Feb 15 2022 at 20:21):

I think all those words were invented by Bourbaki at the same time they invented the espaces tonnelés. They clearly liked this kind of jokes

Anne Baanen (Feb 15 2022 at 20:21):

Yaël Dillies said:

I'm not defining bornomorphisms yet because I'm waiting for Anne Baanen's equiv refactor (or is it usable already?)

Equiv classes up to mul_equiv/add_equiv are already in, ring_equiv was straightforward (up to some simp/coercion details). So I'd say you can go ahead and use equiv_like.

Jireh Loreaux (Feb 15 2022 at 20:31):

@Kyle Miller you convinced me, locally_bounded_map is preferable to bounded_map.

Jireh Loreaux (Feb 15 2022 at 20:46):

Can someone explain to me the plan for making a bornology from a metric space? If I understand correctly, we don't want to make it an instance because of non-defeq diamonds and so we want to implement it in the metric space structure itself (as with uniform spaces), right? But then don't we run into a bootstrapping problem, that is, we will have to define the cobounded filter on the metric space before we define bounded sets in a metric space? I would like to give this a shot, but I'm not sure how to proceed.

Yaël Dillies (Feb 15 2022 at 20:48):

There's no bootstrapping problem if you define cobounded before metric_space.

Kyle Miller (Feb 15 2022 at 20:50):

Could someone explain what the diamond problem here is?

Kyle Miller (Feb 15 2022 at 20:53):

Oh, is one that if a metric_space gives a bornology, then since product spaces have bornology and metric space instances, then they might defeq disagree on the bornology instance?

Jireh Loreaux (Feb 15 2022 at 20:53):

Yes, that's the point.

Yaël Dillies (Feb 15 2022 at 20:54):

Yeah, exactly the same story as with the product topology.

Yaël Dillies (Feb 15 2022 at 20:54):

Good thing is: same problem, same solution.

Jireh Loreaux (Feb 15 2022 at 20:55):

Okay, I guess I understand what to do. I'm going to give it a try.

Jireh Loreaux (Feb 16 2022 at 01:51):

How does this look?

bornology from a pseudo metric

import data.real.basic
import topology.bornology.basic

/- bornology from a pseudo metric -/

open set filter

lemma bounded_iff_aux {α : Type*} (dist : α → α → ℝ)
  (dist_comm : ∀ x y : α, dist x y = dist y x)
  (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z)
  (s : set α) (a : α) :
  (∃ c, ∀ x y ∈ s, dist x y ≤ c) ↔ (∃ r, ∀ x ∈ s, dist x a ≤ r) :=
begin
  split; rintro ⟨C, hC⟩,
  { cases s.eq_empty_or_nonempty with h h,
    { subst s, exact ⟨0, by simp⟩ },
    { rcases h with ⟨x, hx⟩,
      exact ⟨C + dist x a, λ y hy, calc
        dist y a ≤ dist y x + dist x a : dist_triangle _ _ _
        ...      ≤ _                   : add_le_add_right (hC y hy x hx) _⟩ } },
  { exact ⟨C + C, λ x hx y hy, calc
      dist x y ≤ dist x a + dist y a : dist_comm a y ▸ dist_triangle x a y
      ...      ≤ _                   : add_le_add (hC x hx) (hC y hy)⟩, }
end

def bornology.of_dist {α : Type*} (dist : α → α → ℝ)
  (dist_comm : ∀ x y : α, dist x y = dist y x)
  (dist_triangle : ∀ x y z : α, dist x z ≤ dist x y + dist y z) :
  bornology α :=
{ cobounded :=
  { sets := { s : set α | ∃ C, ∀ x y ∈ sᶜ, dist x y ≤ C },
    univ_sets := ⟨0, λ x hx, false.elim (compl_univ.subst hx)⟩,
    sets_of_superset := by
    { rintros s t ⟨c, hc⟩ h,
      exact ⟨c, (λ x hx y hy, hc x (compl_subset_compl.mpr h hx) y (compl_subset_compl.mpr h hy))⟩ },
    inter_sets := λ s t hs ht,
    begin
      by_cases hs' : s = univ,
      { simpa [hs'] using ht, },
      { obtain ⟨z, hz⟩ := (ne_univ_iff_exists_not_mem s).mp hs',
        simp only [λ u, bounded_iff_aux dist dist_comm dist_triangle u z] at hs ht ⊢,
        rcases ⟨hs, ht⟩ with ⟨⟨r₁, hr₁⟩, ⟨r₂, hr₂⟩⟩,
        exact ⟨max r₁ r₂, λ x hx, or.elim ((compl_inter _ _).subst hx)
          (λ hx', (hr₁ x hx').trans (le_max_left _ _))
          (λ hx', (hr₂ x hx').trans (le_max_right _ _))⟩, }
    end },
  le_cofinite :=
  begin
    refine le_def.mpr (λ s hs, _),
    simp only [filter.mem_mk, mem_set_of_eq],
    rw mem_cofinite at hs,
    revert hs,
    generalize : sᶜ = t,
    refine λ h, h.dinduction_on _ (λ x s hx hs h, _),
    { exact ⟨0, λ x hx, false.elim hx⟩ },
    { simp only [λ u, bounded_iff_aux dist dist_comm dist_triangle u x] at h ⊢,
      rcases h with ⟨r, hr⟩,
      rw insert_eq,
      exact ⟨max r (dist x x), λ y hy, or.elim hy
        (λ hy', mem_singleton_iff.mp hy' ▸ le_max_right _ _)
        (λ hy', (hr y hy').trans (le_max_left _ _))⟩ }
  end }

/-
Add this to the structure of a pseudo metric :

`(to_bornology : bornology α := bornology.of_dist dist dist_comm dist_triangle)`
-/

Yaël Dillies (Feb 16 2022 at 01:55):

Looks good!

Yaël Dillies (Feb 16 2022 at 01:55):

(except that I know feel a :golf: urge)

Jireh Loreaux (Feb 16 2022 at 18:41):

#12078: bornology for pseudo metric structure

Anatole Dedecker (Feb 17 2022 at 16:28):

I'm late to the party, but it's really nice to see that you are taking care of that, it'll be useful for my work on distributions !

Anatole Dedecker (Apr 03 2022 at 14:44):

I've been working with bornologies recently, mostly proving that the topology of $\mathfrak{S}$ -convergence (see #13073) is the same as the topology of $\mathfrak{S}'$ -convergence, where $\mathfrak{S}'$ is the bornology generated by $\mathfrak{S}$ (which is actually not true, see below), and I have a few questions about the intended way of using this definition and its API in mathlib :

Are there any good reasons to make it a class ? I may be biased because I've been working quite low level in the API, especially in #12964, but I'm starting to think it would just be easier to make bornologies explicit everywhere, because I can't think of any bornology we could declare as an instance that would not conflict (at least definitionally) with the metric one in at least one case. Like, we can't make the Von Neumann bornology an instance because we can have TVSs with a metric structure, we can't make the compact bornology an instance because it would conflict in a case of a metric space, ...
Would it be easier to remove the covering condition from the definition and just have it as a separate def/typeclass, mimicking how we chose to separate docs#filter.ne_bot from the definition of filters ? I'm asking this because it turns out the result I was trying to prove is false with this definition of bornology. Of course that's not a good reason for changing the definition, but I think what is a good reason is that I can't find an easy way to express it without having a notion of "noncovering bornology", whereas adding some covering assumption when needed. So, yes, it would go against the current usage in the litterature, but it would definitely make formalization easier imo

Yaël Dillies (Apr 03 2022 at 15:28):

The idea at some point was to make docs#bornology.is_bounded subsume docs#metric.bounded, in which case having it a class makes sense.

Patrick Massot (Apr 03 2022 at 16:43):

Is the theorem true if you assume a covering condition on $\mathfrak{S}$ ? Isn't it enough for your purposes?

Kyle Miller (Apr 03 2022 at 17:08):

Anatole Dedecker said:

Would it be easier to remove the covering condition from the definition and just have it as a separate def/typeclass, mimicking how we chose to separate docs#filter.ne_bot from the definition of filters ? I'm asking this because it turns out the result I was trying to prove is false with this definition of bornology.

Once you remove the covering condition, you're left with just a filter -- maybe you can prove what you need about filters then wrap it up in bornologies in the cases where the bornology theorem is true? (Not sure if this is actually a good idea, but it might be one way to go about implementing Patrick's suggestion.)

Anatole Dedecker (Apr 03 2022 at 18:09):

Kyle Miller said:

maybe you can prove what you need about filters then wrap it up in bornologies in the cases where the bornology theorem is true? (Not sure if this is actually a good idea, but it might be one way to go about implementing Patrick's suggestion.)

Indeed that's what I ended up doing, but it's a bit more painful because there are docs#compl popping everywhere

Anatole Dedecker (Apr 03 2022 at 18:15):

Patrick Massot said:

Is the theorem true if you assume a covering condition on $\mathfrak{S}$ ?

Indeed, I proved it too.

Isn't it enough for your purposes?

Ahem, I may have been a bit distracted from distributions indeed :sweat_smile: More seriously, this was mostly a way to test the uniform convergence API, so indeed I don't need it, but I thought it was a shame not to have the general theorem.

Jireh Loreaux (Apr 05 2022 at 16:30):

@Anatole Dedecker So, I will provide my input on your original two points, but perhaps I will just show my own ignorance (likely the latter).

It seems to me that the situation is very much like the situation with topologies. Most of the time, you have one you want to work with, but every so often you need others. When this happens it is kind of a pain unless you have a few common topologies that repeatedly show up, in which case you create type synonyms. As for the conflicting instances problem, isn't this just a matter of baking the bornology into the definitions themselves? For example, now a TVS would get the von Neumann bornology in the definition, and then so would normed vector spaces? Perhaps I'm missing something here.
I really don't think we should exclude the cofinite/covering condition, because then it's just a filter.

Jireh Loreaux (Apr 05 2022 at 19:17):

Sorry, I realized I may not have been entirely clear. The point would be that a normed_space would come with a defined bornology. Then in the derived instances metric_spaceand topological_vector_space (I just noticed the latter doesn't exist, what do we do here, just [module 𝕜 E] [has_continuous_add E] [has_continuous_smul 𝕜 E]? If so, we might need to actually make a TVS class for my suggestion to work) you would replace the default generated bornology with the one coming from the normed space and then prove that it has the specified form. I think this would avoid the defeq problem.

Moritz Doll (Apr 05 2022 at 20:11):

I have the bad feeling that this is more difficult to do. For something like Fréchet space you have that 'metrically bounded = bounded' (Fréchet implies that the space is metrizable), but it is not true for all topologically vector spaces. I guess that we will need a class of metrizable tvs for which 'metrically bounded = bounded' and normed spaces just extend that. Unfortunately, we cannot do everything on the level of groups, since the von Neumann bornology needs has_continuous_smul.

Jireh Loreaux (Apr 05 2022 at 20:55):

Isn't a bornological space exactly an LCS where the von Neumann bounded sets are metrically bounded, or did I internalize that definition incorrectly? If that's correct, then maybe we want this type class, and it's exactly the one that generalizes TVS with a bornology and metric space with a bornology in the defeq way. Then normed spaces and Frechet spaces would be instances of this. Then a TVS which is metrizable and has a bornology which doesn't coincide would rightly be considered an outlier. Does all this make sense?

Jireh Loreaux (Apr 05 2022 at 20:58):

(sorry, my characterization of bornological spaces applies when the space is metrizable, otherwise the condition involves a neighborhood of zero)

Yury G. Kudryashov (Apr 11 2022 at 18:31):

Hi, what's the status here? I want to add lemmas like antilipschitz_with.tendsto_cobounded and corollaries for left/right scalar multiplication. Which filter should I use for cobounded?

Yury G. Kudryashov (Apr 11 2022 at 18:32):

I mean cobounded instance that comes from pseudo_metric_space.

Yaël Dillies (Apr 11 2022 at 18:32):

docs#bornology.cobounded I believe

Yury G. Kudryashov (Apr 11 2022 at 18:34):

BTW, what are your plans about diamonds? E.g., cobounded coming from metric space structure and the one coming from a TVS structure are not defeq.

Yury G. Kudryashov (Apr 11 2022 at 18:34):

I'm sorry for asking questions that probably were answered before. I haven't read backlog for a while.

Yury G. Kudryashov (Apr 11 2022 at 18:35):

BTW, why docs#bounded_space extends bornology? How do I say "consider a bounded metric space"?

Yaël Dillies (Apr 11 2022 at 18:35):

We plan on incorporating bornology into metric_space in the same as uniform_space has been done before. Does that fix your diamond?

Yaël Dillies (Apr 11 2022 at 18:37):

Yury G. Kudryashov said:

BTW, why docs#bounded_space extends bornology? How do I say "consider a bounded metric space"?

I believe this is a mistake, given the mixin approach of the topology library.

Yury G. Kudryashov (Apr 11 2022 at 18:40):

It looks like there is no instance metric_space.to_bornology yet (at least, not in the list of instances here), so I can't use it for antilipschitz_with.tendsto_cobounded.

Yaël Dillies (Apr 11 2022 at 18:41):

@Jireh Loreaux already has all the code for it. It just needs a PR I believe.

Anatole Dedecker (Apr 11 2022 at 18:42):

It has been PR-ed

Anatole Dedecker (Apr 11 2022 at 18:43):

It’s in the definition of docs#pseudo_metric_space, but maybe it is not registered as an instance

Moritz Doll (Apr 11 2022 at 18:47):

Yury G. Kudryashov said:

BTW, what are your plans about diamonds? E.g., cobounded coming from metric space structure and the one coming from a TVS structure are not defeq.

There are cases where they are not equal at all. This has caused me a bit of headache and I haven't had a good idea what to do about it.

Yury G. Kudryashov (Apr 11 2022 at 19:29):

What are these cases? A completely different approach is to use bornology as a bundled structure, not a class.

Jireh Loreaux (Apr 11 2022 at 19:44):

@Moritz Doll at the risk of beating a dead horse, can't this be addressed with a bornological_space class for TVS? Do you really have a lot of cases where the TVS bornology and the metric bornology aren't propositionally equal?

Moritz Doll (Apr 11 2022 at 20:25):

I know only one example and it is somewhat artificial: you take the seminorms $|a_n - b_n|$ on the space of all sequences and then take the usual metric generated by those seminorms. Every sequence is metrically bounded by 1, but not von Neumann bounded (it is in Narici-Beckenstein).

Moritz Doll (Apr 11 2022 at 20:33):

Yes, for bornological spaces we should be fine, but not having typeclasses for general topological vector spaces feels wrong.

Moritz Doll (Apr 11 2022 at 20:35):

isn't the way the bornology is defined for metric spaces essentially a bundled approach?

Jireh Loreaux (Apr 11 2022 at 20:36):

Right, I think we might want a generic TVS type class also. My thought is that the bornological_space type class would fix defeq issues, and that places where they aren't propositionally equal are sufficiently rare to not be a huge problem.

Yaël Dillies (Apr 11 2022 at 20:37):

Do you mean an actual bornological space by bornological_space or did terminology lead you astray again?

Jireh Loreaux (Apr 11 2022 at 20:38):

I mean actual bornological spaces. These are the ones for which the metric bornology and the von Neumann bornology coincide (at least, I think).

Yury G. Kudryashov (Apr 11 2022 at 21:03):

What is the definition of the bornology for a TVS? Does it work for any (normed) base field or only for reals? In the former case, you can't have an instance [add_comm_group] [module k V] [has_continuous_smul k V] : bornology V because it leads to an instance search has_continuous_smul ?_m V. In any case, you can't resolve defeq for normed spaces because a general normed space works with any underlying metric_space structure, hence with any underlying bornology.

Yury G. Kudryashov (Apr 11 2022 at 21:05):

So, I guess that the way to go with the bornology for a TVS is to have a mixin typeclass that says "bornology on V agrees with the TVS structure".

Yury G. Kudryashov (Apr 11 2022 at 21:15):

Is there a branch that replaces docs#metric.bounded with docs#bornology.is_bounded?

Jireh Loreaux (Apr 11 2022 at 21:16):

Not that I've created. Been busy with other things

Jireh Loreaux (Apr 11 2022 at 21:19):

see docs#bornology.vonN_bornology for the bornology arising naturally from a TVS.

Yury G. Kudryashov (Apr 11 2022 at 21:21):

Are there any (not yet formalized) theorems that link this bornology to the one arising from metric space structure?

Jireh Loreaux (Apr 11 2022 at 23:05):

I'm no longer convinced that my previous claim about bornological spaces holds. This is because such spaces have a topology which agrees with the one induced by the bornology, but that doesn't have anything to do with the metric structure. So, consider ℝ with the usual metric and then the metric bounded sets are exactly the von Neumann bounded sets (considering ℝ as a TVS). However, we may replace the metric with a bounded metric without changing the topology. Then every set is metric bounded, but since the topology didn't change the von Neumann bounded sets are the usual bounded sets. Now the two bornologies don't agree, but nevertheless ℝ is still a bornological space.

Jireh Loreaux (Apr 11 2022 at 23:09):

Point being, I think Moritz is right, the metric bornology and the von Neumann bornology can easily fail to be propositionally equal, even if the TVS is bornological. Perhaps letting metric spaces have a bornology instance is not the right way to go, even if we keep the metric bornology structure.

Yury G. Kudryashov (Apr 12 2022 at 03:53):

What do we need to assume to say that the bornology is the same as the one from the metric_space structure?

Yury G. Kudryashov (Apr 12 2022 at 03:53):

E.g., is it true for a normed space? Or only for a finite dimensional normed space?

Yury G. Kudryashov (Apr 12 2022 at 04:21):

I'm going to add a complete_lattice structure on bornology α. Which order should I choose: t ≤ t' if @is_bounded α t s → @is_bounded α t' s or if @is_bounded α t' s → @is_bounded α t s?

Yury G. Kudryashov (Apr 12 2022 at 04:21):

One makes is_bounded monotone, another makes cobounded monotone.

Yury G. Kudryashov (Apr 12 2022 at 04:54):

Started review of bornology API in #13374

Moritz Doll (Apr 12 2022 at 05:21):

For normed spaces is it correct since a set is von Neumann bounded iff all seminorms are bounded.

Moritz Doll (Apr 12 2022 at 05:27):

But if you are only normable, then I think (haven't checked the details) you could replace the metric $d(x,y) = \|x - y\|$ by the metric $d(x,y) = \frac{\|x - y\|}{1 + \|x - y\|}$ and then every set is metrically bounded, but not von Neumann bounded (this is the normed version of the example I mentioned above, which isn't so artificial after all and the same thing Jireh was saying).

Moritz Doll (Apr 12 2022 at 05:51):

Yury G. Kudryashov said:

I'm going to add a complete_lattice structure on bornology α. Which order should I choose: t ≤ t' if @is_bounded α t s → @is_bounded α t' s or if @is_bounded α t' s → @is_bounded α t s?

@Anatole Dedecker has a PR for that already: #12964

Yury G. Kudryashov (May 15 2022 at 20:45):

I'm going to merge docs#bornology.is_bounded with docs#metric.bounded. The next PR in line is #13927. It would be nice if someone who uses bornology outside of mathlib will review it.

Yury G. Kudryashov (May 15 2022 at 20:46):

My main goal is to be able to use docs#bornology.cobounded on metric spaces (and reformulate various lemmas in terms of this filter).

Anatole Dedecker (May 15 2022 at 21:27):

Will you need the complete lattice structure on bornologies ? I didn't really get back to it because I didn't need it immediately (and also because, in the case I had in mind, I really wanted the generated "noncovering bornology", not the generated bornology), but I can revivre #12964 if you need it.

Yury G. Kudryashov (May 15 2022 at 22:26):

I won't need it.

Yury G. Kudryashov (May 15 2022 at 22:26):

I just want to have cobounded : filter complex

Yury G. Kudryashov (May 15 2022 at 22:27):

And restate lemmas that use comap norm at_top in terms of cobounded.

Yury G. Kudryashov (May 15 2022 at 22:28):

BTW, I see that we have some non-instance bornologies. What's the plan: restate lemmas about is_bounded etc so that they take {_ : bornology α} instead of [bornology α], introduce type tags, or something else?

Yury G. Kudryashov (May 22 2022 at 19:58):

Let me ping here again about #13927. I have a few other changes that depend on it.

Yury G. Kudryashov (May 22 2022 at 20:06):

E.g., I want to

start using docs#bornology.is_bounded instead of docs#metric.bounded
move definitions of docs#pseudo_emetric_space, docs#pseudo_metric_space, docs#emetric_space, docs#metric_space, docs#pseudo_metrizable_space, and docs#metrizable_space to a new file; then we can use [metrizable_space X] instead of [metric_space X] much earlier.

Eric Wieser (May 22 2022 at 22:28):

Yury G. Kudryashov said:

Let me ping here again about #13927. I have a few other changes that depend on it.

How reasonable would it be to change docs#pseudo_emetric_space.to_pseudo_metric_space_of_dist to require the bornology to already exist? In that PR, you change two uses of it to subsequently replace the bornology; are there any other uses of it?

Yury G. Kudryashov (May 22 2022 at 22:56):

It is used 5 times in mathlib. I'll check all of them tonight.

Yury G. Kudryashov (May 22 2022 at 23:06):

See docs#pseudo_emetric_space.to_pseudo_metric_space

Yury G. Kudryashov (May 22 2022 at 23:07):

We have no bornology in this case.

Eric Wieser (May 22 2022 at 23:15):

RIght, I guess what I was suggesting is

def pseudo_emetric_space.to_pseudo_metric_space_of_dist {α : Type u} [bornology α]
  [e : pseudo_emetric_space α]
  (dist : α → α → ℝ)
  (edist_ne_top : ∀x y: α, edist x y ≠ ⊤)
  (h : ∀x y, dist x y = ennreal.to_real (edist x y))
  (h' : ∀ s : set α,
    is_bounded s ↔ ∀ᶠ (C : ℝ) in at_top, ∀ ⦃x : α⦄, x ∈ s → ∀ ⦃y : α⦄, y ∈ s → dist x y ≤ C) :

I have no idea if that's actually helpful

Last updated: Dec 20 2023 at 11:08 UTC