Nets instead of sequences

Stream: Is there code for X?

[Josha Dekker]

Hi, in my efforts to define various concepts of tightness, I just defined asymptotically tight sequences, but I'd like to extend this to asymptotically tight nets. What is the proper/preferred way of setting this up? My current definition is the following, where I'd like to replace ℕ by a directed set.

def IsAsymptoticallyTight [TopologicalSpace α] (μs : ℕ → Measure α) : Prop :=
  ∀ ε : ℝ≥0∞, 0 < ε → ∃ K : Set α, IsCompact K ∧ Filter.limsup (fun i ↦ (μs i) Kᶜ) Filter.atTop ≤ ε

[Vincent Beffara]

Can you rewrite your definition in terms of filters instead? That would likely be easier to generalize. Like, a single measure being tight means Tendsto μ something (𝓝 0) where something : Filter (Set α) is appropriately chosen.

[Vincent Beffara]

I want to say something := (cocompact α).smallSets but I'm really not sure

[Vincent Beffara]

See docs#Filter.eventually_smallSets

[Josha Dekker]

I think I see your point, so you would be able to unify Uniformly Tight and Asymptotically Tight (on sequences/nets) by properly picking a filter, and Tight (for one measure) would then be given by restricting Uniformly Tight to one element? I'd need to think about how to implement this and correctly set this up, but it would certainly be the Mathlib way...

[Vincent Beffara]

I believe tight for one measure would be simpler as a single Tendsto but otherwise yes that would be my point. And then you get the whole Filter API so you never have to slice epsilons into 3 parts ever again.

[Josha Dekker]

Vincent Beffara said:

I believe tight for one measure would be simpler as a single Tendsto but otherwise yes that would be my point. And then you get the whole Filter API so you never have to slice epsilons into 3 parts ever again.

That is a big advantage of course! I'll try to play around with that a bit when I have the time. If you like puzzling with this, feel free to write up the definitions and I'll modify my existing API to work for these! Otherwise, I'll give it a shot sometime soon!

[Vincent Beffara]

import Mathlib

open Topology Filter Uniformity Uniform MeasureTheory Set

variable {α ι : Type*} [MeasurableSpace α] [TopologicalSpace α]

def isTight (μ : Measure α) : Prop := Tendsto μ (cocompact α).smallSets (𝓝 0)

example (μ : Measure α) :
    isTight μ ↔ ∀ ε > 0, ∃ K : Set α, IsCompact K ∧ μ (Kᶜ) ≤ ε := by

  simp [isTight, ENNReal.tendsto_nhds, Filter.eventually_smallSets, Filter.mem_cocompact]
  apply forall₂_congr ; rintro ε - ; constructor
  · rintro ⟨A, ⟨K, h1, h2⟩, hA⟩
    exact ⟨K, h1, hA Kᶜ h2⟩
  · rintro ⟨K, h1, h2⟩
    refine ⟨Kᶜ, ⟨K, h1, subset_rfl⟩, fun A hA => μ.mono hA |>.trans h2⟩

[Josha Dekker]

Amazing, thank you for your effort! I will refactor using this, and I'll think a bit about how to write the analogous definition of this for a set of measures/sequence of measures/net of measures!

[Vincent Beffara]

def IsTightAtFilter_v1 (μ : ι → Measure α) (F : Filter ι) : Prop :=
    ∀ ε > 0, ∃ K : Set α, IsCompact K ∧ ∀ᶠ i in F, (μ i) Kᶜ ≤ ε

but that is not really satisfactory. I would really like to write this in terms of docs#TendstoUniformlyOnFilter but that requires a UniformSpace which ENNReal is not (but only small values matter, so it should be workable ...)

[Vincent Beffara]

Alternatively, we could put a uniform structure on ENNReal that matches its topology, as in docs#compactSpace_uniformity and be done with it.

[Josha Dekker]

If I'm interpreting this correctly, we would than have, in the notation of docs#TendstoUniformlyOnFilter, F = ι → Measure α and f = 0 : Measure α? Or am I misinterpreting this?

[Vincent Beffara]

There are indices going along one filter and sets going along the cocompact based other filters, I always forget which is which in tendstouniformlyonfilter but in any case uniform tightness would be easier to start with.

[Antoine Chambert-Loir]

Why isn't docs#ENNReal a uniform space?

[Yaël Dillies]

Is it not the same issue as why it's not a metric space? namely that it would induce a topology where Nat.cast : ℕ → ℝ≥0∞ does not tend to ∞?

[Sébastien Gouëzel]

There is no natural metric space structure on ENNReal, indeed, but there is a canonical uniform structure, as it's a compact space. It would make sense to have it in mathlib, I guess nobody has needed it yet.

[Vincent Beffara]

Do we have a homeomorphism between ENNReal and unitInterval somewhere available?

[Yaël Dillies]

Sébastien Gouëzel said:

There is no natural metric space structure on ENNReal, indeed, but there is a canonical uniform structure

Interesting. That's what I wanted to be true, but I didn't actually know whether it was

[Yaël Dillies]

@Vincent Beffara said:

Do we have a homeomorphism between ENNReal and unitInterval somewhere available?

docs#ENNReal.orderIsoUnitIntervalBirational

[Vincent Beffara]

So we can just say this?

noncomputable instance : UniformSpace ENNReal :=
  UniformSpace.comap ENNReal.orderIsoUnitIntervalBirational inferInstance

[Yaël Dillies]

No because most likely that doesn't give the correct topology on ENNReal up to defeq

[Yaël Dillies]

Indeed, it won't, but it should be easy to prove it's propeq

[Vincent Beffara]

It's propeq because it is canonical, if everything is set up right.

[Yaël Dillies]

Yes, exactly. The way I would go about it is by observing that both ENNReal and unitInterval are both endowed with the order topology and then I would use the fact that ENNReal.orderIsoUnitIntervalBirational is an OrderIso.

[Vincent Beffara]

IIUC, if we really need the TopologicalSpace to be defeq to the one obtained from the UniformSpace we can always remove the current instance and prove [OrderTopology ENNReal] using the fact that we have an OrderIso?

[Yaël Dillies]

That too would work, although I'm afraid there's a bootstrapping issue: the topology on unitInterval comes much later

[Vincent Beffara]

This works:

attribute [-instance] ENNReal.instTopologicalSpaceENNReal

noncomputable instance : UniformSpace ENNReal :=
  UniformSpace.comap ENNReal.orderIsoUnitIntervalBirational inferInstance

noncomputable instance : TopologicalSpace ENNReal := UniformSpace.toTopologicalSpace

instance : OrderTopology ENNReal := by
  apply induced_orderTopology ENNReal.orderIsoUnitIntervalBirational (by simp)
  intro x y hxy
  obtain ⟨z, hxz, hzy⟩ : ∃ z, x < z ∧ z < y := exists_between hxy
  use ENNReal.orderIsoUnitIntervalBirational.invFun z
  simp [*]

[Antoine Chambert-Loir]

Is it clear, on this definition, that the inclusion of Real into ENNReal induces it's topology?

[Yaël Dillies]

Antoine, please reconsider your previous message :wink:

[Yaël Dillies]

The inclusion from NNReal to ENNReal however should indeed be easily shown to induce the topology because it is an order embedding and both NNReal and ENNRealare equipped with their order topology

[Sébastien Gouëzel]

Instead of changing the definition of the topology on ENNReal, you could probably keep the original one, but adjust the definition of the uniform space to make sure that the topology is definitionally the original one, with docs#UniformSpace.replaceTopology.

[Vincent Beffara]

Like this,

noncomputable instance : UniformSpace ENNReal := by
  apply (UniformSpace.comap ENNReal.orderIsoUnitIntervalBirational inferInstance).replaceTopology
  simp [ENNReal.instTopologicalSpaceENNReal, UniformSpace.toTopologicalSpace]
  rw [StrictMono.induced_topology_eq_preorder (OrderIso.strictMono _)]
  sorry

Remains to show OrdConnected (univ : Set (Icc 0 1)) which is suspiciously close to docs#Set.ordConnected_Icc so I'm guessing a proper incantation around Subtype.val would close it, but I have to go now. Will try a bit later.

[Notification Bot]

A message was moved here from #Is there code for X? > Tight measures by Vincent Beffara.

[Vincent Beffara]

noncomputable instance toto : UniformSpace ENNReal :=
  (UniformSpace.comap ENNReal.orderIsoUnitIntervalBirational inferInstance).replaceTopology
    (StrictMono.induced_topology_eq_preorder (OrderIso.strictMono _)
      (by simp [RelIso.range_eq, ordConnected_univ])).symm

example : toto.toTopologicalSpace = ENNReal.instTopologicalSpaceENNReal := rfl

[Kevin Buzzard]

I want to react with some kind of triumphant rfl emoji :-)

[Richard Copley]

example : :rolling_on_the_floor_laughing: := rofl

[Kevin Buzzard]

well rfl used to be called refl so maybe we need to start a campaign to rename it rofl

[Johan Commelin]

Proof by rofloxovity

[Antoine Chambert-Loir]

Yaël Dillies said:

Antoine, please reconsider your previous message :wink:

By “was it clear”, I meant “was it clear to Lean”, aka “defeq”, that...

[Patrick Massot]

Antoine, Yaël points out a typo in your message.

[Patrick Massot]

You wrote that reals are contained in extended non-negative reals.

[Antoine Chambert-Loir]

Oh, sorry. (That must be the autocorrect.)