Continuity from filters

Stream: Is there code for X?

[Vincent Beffara]

Are these in mathlib?

import topology.continuous_on
open set filter
open_locale topological_space filter

universe u
variables {α : Type u} {β : Type*} [topological_space α] [topological_space β] {f : α → β} {a : α}

lemma L1 : continuous_at f a ↔ ∀ l : filter α, l ≤ 𝓝 a → filter.map f l ≤ 𝓝 (f a) :=
⟨λ h l hl, (map_mono hl).trans h, λ h, h (𝓝 a) le_rfl⟩

lemma L2 : continuous_at f a ↔
  ∀ {γ : Type u} (φ : γ → α) (l : filter γ), tendsto φ l (𝓝 a) → tendsto (f ∘ φ) l (𝓝 (f a)) :=
⟨λ h γ φ l hl, (map_mono hl).trans h, λ h, h id (𝓝 a) tendsto_id⟩

lemma L3 {s : set α} :
  continuous_within_at f s a ↔ ∀ l : filter α, l ≤ 𝓝[s] a → filter.map f l ≤ 𝓝 (f a) :=
⟨λ h l hl, (map_mono hl).trans h, λ h, h (𝓝[s] a) le_rfl⟩

lemma L4 {s : set α} :
  continuous_within_at f s a ↔
  ∀ {γ : Type u} (φ : γ → α) (l : filter γ), tendsto φ l (𝓝[s] a) → tendsto (f ∘ φ) l (𝓝 (f a)) :=
⟨λ h γ φ l hl, (map_mono hl).trans h, λ h, h id (𝓝[s] a) tendsto_id⟩

(I'm not happy about the way universes look in L2 and L4.)

[Kevin Buzzard]

I would try to make a helpful comment about universes but your code doesn't compile for me as it stands and I don't know enough about topology to fix it up (I might be missing an open or an open_locale or something)

[Kevin Buzzard]

I was going to first figure out what you were unhappy about and then suggest that you don't use variables but instead put all the types in your statement -- this sometimes makes a difference.

[Vincent Beffara]

(Added missing import.) The same issue came up with explicit parameters, having all of α, β and γ be Type* fails with a universe error. Which I guess I don't really have to care about, I just want to exploit a proof of convergence that I have to show that a function is continuous without resorting to sequential continuity.

[Vincent Beffara]

The only lemma lokking like this that I found in mathlib is docs#filter.tendsto_iff_ultrafilter

[Sebastien Gouezel]

For L2 and L4, you should probably first prove the direct implication where gamma can be in any universe.

[Kevin Buzzard]

Oh the issue is that gamma and alpha need to be in the same universe?

[Sebastien Gouezel]

(Well, they are so trivial that maybe then don't need a separate lemma).

[Vincent Beffara]

Sebastien Gouezel said:

For L2 and L4, you should probably first prove the direct implication where gamma can be in any universe.

Yes, the direct implication works generally. What puzzles me is that additional restrictions on universes should make the reverse implication more difficult.

[Vincent Beffara]

Sebastien Gouezel said:

(Well, they are so trivial that maybe then don't need a separate lemma).

(Agreed, all 4 equivalences are basically true by definition anyway, they are just useful to me as rw lemmas.)

[Kevin Buzzard]

This came up in the perfectoid project and probably in other places too. If φ : γ → α with gamma and alpha in different universes, then phi factors as a surjection to delta followed by an injection delta->alpha and you can assume that delta is in the same universe as alpha. You can then apply L2 for delta. Is this enough to deduce it for gamma in a different universe? That was the kind of trick we played in the perfectoid repo. You need to be careful though -- if you want the if and only if then you might need that the universe of gamma is >= the universe of alpha. For example the lemma is probably not true if you allow gamma : Sort u as then gamma can be a proposition, which will presumably not be good enough to prove continuous_at (remember that Lean is implicitly claiming that infinitely many lemmas are true, with u and v being any choice of universe variable).

[Vincent Beffara]

Ah! I think I'm slowly getting it, writing ∀ {γ : Type*} does not quantify over the universe, and I was reading this in my head as ∀ {u} {γ : Type u} which makes no sense.

[Kevin Buzzard]

Right! If you can prove a theorem involving two universes u and v then you're actually proving infinitely many theorems, or one theorem with "for all u, v" at the very beginning (and as you point out, you're not allowed to quantify over universes in the middle of a statement)

[Adam Topaz]

One general approach to such things is to use max u v as the universe level of gamma, although (at least in lean3) you may need to tell lean explicitly what the universes are when you use the lemma. (Is this better in lean4?)

[Adam Topaz]

For L2 and L4, you want gamma to be at a universe level at least as large as that of alpha, and the only way to say this is using max.

[Adam Topaz]

The reverse implication would then involve a ulift, not just an id.

[Anatole Dedecker]

Putting universes aside, I'm surprised you need these at all, do you have an example use? Anyways, it looks like you would be interested by docs#filter.tendsto_iff_ultrafilter

[Vincent Beffara]

My example is that I had a proof of tendsto_locally_uniformly_on (deriv ∘ F) (deriv f) φ U from tendsto_locally_uniformly_on F f φ U and ∀ᶠ n in φ, differentiable_on ℂ (F n) U, from before I learned about the type aliases for uniform convergence, and I figured that it would make sense to state that deriv is continuous from {f : ℂ →ᵤ[compacts U] ℂ | differentiable_on ℂ f U} to itself. And being lazy I tried to deduce the continuity from the convergence.

[Anatole Dedecker]

But I don't see how considering all finer filters matter here? Can't you just apply your previous lemma to the identity (from {f : ℂ →ᵤ[compacts U] ℂ | differentiable_on ℂ f U} to itself)?

[Anatole Dedecker]

And use docs#filter.tendsto_id

[Vincent Beffara]

Yes sure, the proof of my stupid lemma is λ h, h id (𝓝[s] a) tendsto_id but figuring this out took me a while (I am still mostly flying blind whenever there are filters involved).

[Anatole Dedecker]

Sorry, I didn't mean to make it sound like a triviality, and I should have read your message better (I even missed that you had seen docs#filter.tendsto_iff_ultrafilter!). I was just curious as to wether it was really more convenient or "only" more familiar looking because of the similarity with docs#seq_continuous

[Anatole Dedecker]

My instinct says that we don't need these in mathlib, but on the other hand filters do take a while to get used to and these lemmas may be good to have exactly because they may seem more instinctive to quite a lot of people.

[Vincent Beffara]

Well for people used to working with sequential characterizations, but who feel guilty about it because not all spaces have first countable topology, there is a temptation to see filters together with indexed families like "sequences but without such pathologies" and those lemmas then feel useful. My first instinct when not finding them in mathlib was to think that maybe they were not true and that I was missing something essential, rather than to figure that they were too close to the definitions to be useful.

[Anatole Dedecker]

Yeah I can get why these statements seem more natural than thinking of the identity as an family in X indexed by X, which always feels like you're cheating somehow. So maybe let's wait one or two days after Christmas to gather more opinions about this.
My concern isn't at all that they are too close to the definitions (this isn't a problem at all in mathlib), it is that while it may look like a sensible thing to apply it can really only make a proof harder. It's like saying that a sequence converges if and only if all subsequences do: it's true, but can't really help since among all of these subsequences you still have your first sequence, so you could have gone straight to it.
But again, the mere fact that people may look for these statement could be a sufficient argument to put them in mathlib, maybe with a docstring explaining how you can skip them.