Sequential convergence and countably generated filters

Stream: maths

[Manuel Eberl]

I was playing around with filters a bit (in Isabelle) and eventually realised that the answer to some of my questions was already in Mathlib. So I was wondering if the people on here could clarify one thing that I don't quite understand and couldn't find much about on the internet. I only have vague understanding of filters to be honest.

The question is about the theorem filter.tendsto_iff_seq_tendsto in Mathlib, which states:

 theorem filter.tendsto_of_seq_tendsto
   {α : Type u_3} {β : Type u_4} {f : α → β} {k : filter α} {l : filter β} [k.is_countably_generated] :
    (∀ (x : ℕ → α), filter.tendsto x filter.at_top k → filter.tendsto (f ∘ x) filter.at_top l) → filter.tendsto f k l

So basically, if you have a countably generated filter then its behaviour is completely characterised by convergence of sequences.

What I'm wondering is: Does the converse also hold? I.e. is any filter that satisfies this countably generated? If not, is there a standard name for filters that have this property and what is an example of one that isn't countably generated?

[Ruben Van de Velde]

Fwiw, you're pointing at lean3 code that's years out of date by now

[Christian Merten]

docs#Filter.tendsto_iff_seq_tendsto is the Lean4 version.

[Patrick Massot]

I would guess the converse doesn’t hold, and search internet for examples of sequential spaces that are not first countable, hoping to find inspiration for counter-examples.

[Patrick Massot]

Do you have any reason to ask or are you simply hoping to use more sequences and less filters? We can probably help if you want to become friends with filters.

[Patrick Massot]

I have lectures notes about filters but they are in French.

[Manuel Eberl]

The original motivation was this: suppose I have a family of sets $A(x)$ that "converges" to $B$ as $x\to F$ (for some filter $F$). I also have a function that is Lebesgue-integrable on $B$.

I wanted to show that $\lim_{x\to F} \int_{A(x)} f(t)\,\text{d}t = \int_B f(t)\,\text{d}t$.
We have some versions of this for various filters $F$ and various families of intervals $A$, but it's a mess. So I wanted to prove it once and for all for all sensible values of $F$ and $A$.

Capturing the notion that $A(x) \to B$ for $x\to F$ is a bit strange as well. I don't think "convergence of a family of sets to a set" can be expressed as a filter (if it can, I'd be interested to hear how). I ended up doing it like this:

definition tendsto_set :: "('a ⇒ 'b set) ⇒ 'b set ⇒ 'a filter ⇒ bool" where
  "tendsto_set A B F ⟷ eventually (λy. A y ⊆ B) F ∧ (∀x. eventually (λy. x ∈ A y ⟷ x ∈ B) F)"

That works. But I don't think it can be expressed as a filter.

Anyway, the fact I wanted to prove follows easily from dominated convergence, but we only have dominated convergence for $F = \text{sequentially}$. So I investigated to see how to make this work for more general filters. I was able to show that it works for all countably generated filters.

I did wonder, however, whether it makes sense to introduce a more general class of "sequentially determined filters" (or whatever you want to call them). In Isabelle it would be something like this:

locale sequential_filter =
  fixes F :: "'a filter"
  assumes approachable:
    "(⋀f. filterlim f F sequentially ⟹ eventually (λn. P (f n)) sequentially) ⟹ eventually P F"

Clearly, every countably generated filter is "sequentially determined". Not sure if the converse holds, or if there are interesting filters that satisfy one but not the other.

[Anatole Dedecker]

The way we deal with this in Mathlib is docs#MeasureTheory.AECover, and indeed most of the theory is done for countably generated filters.

[Anatole Dedecker]

I'm not claiming this is the most natural notion, I wrote it a while ago and with not a ton of mathematical background. Note that the way we get rid of the extra set B is that we put it in the measure (see e.g docs#MeasureTheory.aecover_Icc_of_Icc)

[Moritz Doll]

Patrick Massot said:

I would guess the converse doesn’t hold, and search internet for examples of sequential spaces that are not first countable, hoping to find inspiration for counter-examples.

There are lots of examples of spaces that are sequential, but not Frechet-Urysohn (and therefore not first countable). In particular, duals of infinite dimensional Montel Frechet spaces.

[Anatole Dedecker]

About convergence with sets,

Patrick Massot said:

I would guess the converse doesn’t hold, and search internet for examples of sequential spaces that are not first countable, hoping to find inspiration for counter-examples.

I also expect the converse to be false, but I'm not sure this is enough. I claim that if all neighborhoods filter of a space satisfy Manuel's condition then the space is Fréchet-Urysohn.

Let me denote by $\mathrm{Seq}(\mathcal{F})$ the sequentialization of a filter, namely the supremum over all sequences $u$ converging to $\mathcal{F}$ of $u_*\mathrm{atTop}_{\mathbb{N}}$. Manuel's condition is then precisely $\mathrm{Seq}(\mathcal{F}) = \mathcal{F}$.

But, in a topological space, one has $A\in\mathrm{Seq}(\mathcal{N}_x) \iff x\in\mathrm{SeqInterior}(A)$. Hence if $\forall x, \mathrm{Seq}(\mathcal{N}_x) = \mathcal{N}_x$ we get that interior and sequential interior always coincide.

[Anatole Dedecker]

I think there is more hope to be found by looking for Fréchet-Urysohn spaces which are not first countable.

[Manuel Eberl]

Okay, thanks for all the replies! The AE cover looks like a good idea. I'll probably steal that.

[Manuel Eberl]

On a related note, there are two other things that are giving me some trouble:

First, is a supremum of countably many countably generated filters again countably generated? I tried to prove it and I now suspect the answer is no.

Second, can someone explain to me how the proof works that in a second countable linear order topology, at_top is countably generated?

[Patrick Massot]

Anatole Dedecker said:

About convergence with sets,

Patrick Massot said:

I would guess the converse doesn’t hold, and search internet for examples of sequential spaces that are not first countable, hoping to find inspiration for counter-examples.

I also expect the converse to be false, but I'm not sure this is enough.

Yes, I’m sure it’s not enough, that’s why I wrote “hoping to find inspiration”.

[Patrick Massot]

Manuel Eberl said:

On a related note, there are two other things that are giving me some trouble:

First, is a supremum of countably many countably generated filters again countably generated? I tried to prove it and I now suspect the answer is no.

Which order relation do you put on filters? Is it the Mathlib one or the wrong one?

[Manuel Eberl]

I think it's the same one that Mathlib uses. Because the proof for countable infimum was trivial, and Mathlib has that one.

[Patrick Massot]

Ok, then my guess is the result is wrong.

[Aaron Liu]

Anatole Dedecker said:

I think there is more hope to be found by looking for Fréchet-Urysohn spaces which are not first countable.

here's some spaces

• OnePoint ℚ
• OnePoint (Σ _ : ℝ, Unit)
• @Quot ℝ fun a b => a ∈ Set.range Int.cast ∧ b ∈ Set.range Int.cast
• @Quot (ℕ × OnePoint ℕ) fun a b => a.2 = OnePoint.infty ∧ b.2 = OnePoint.infty
• CofiniteTopology ℝ

[Patrick Massot]

It looks like it would require a countable product of countable sets to be countable.

[Manuel Eberl]

Okay that's what I thought. Thanks!

[Aaron Liu]

I'm having trouble coming up with a counterexample

[Aaron Liu]

ok, looks like ⨆ i : ℕ, Filter.map (Prod.mk i) (Filter.atTop : Filter ℕ) isn't countably generated