Locally uniform convergence

Stream: Is there code for X?

[Vincent Beffara]

Is any of these already in mathlib?

variables {α β ι : Type*} [topological_space α] [uniform_space β] {s t : set α} {a : α}
  {φ : filter ι} {G : ι → α → β} {g : α → β}

lemma mem_nhds_within_of_subset (hs : s ∈ 𝓝 a) (hsU : s ⊆ t) : s ∈ 𝓝[t] a :=
by simpa [inter_eq_right_iff_subset.mpr hsU] using inter_mem_nhds_within t hs

lemma tendsto_locally_uniformly_on_iff [locally_compact_space α] (ht : is_open t) :
  (tendsto_locally_uniformly_on G g φ t) ↔
  (∀ K ⊆ t, is_compact K → tendsto_uniformly_on G g φ K) :=
begin
  split,
  { rintro h K hK1 hK2,
    exact (tendsto_locally_uniformly_on_iff_tendsto_uniformly_on_of_compact hK2).mp (h.mono hK1) },
  { rintro h ε hε z hz,
    obtain ⟨K, ⟨hK1, hK2⟩, hK3⟩ := (compact_basis_nhds z).mem_iff.mp (ht.mem_nhds hz),
    exact ⟨K, mem_nhds_within_of_subset hK1 hK3, h K hK3 hK2 ε hε⟩ }
end

lemma tendsto_locally_uniformly_on_iff_filter :
  tendsto_locally_uniformly_on G g φ t ↔
  ∀ x ∈ t, tendsto_uniformly_on_filter G g φ (𝓝[t] x) :=
begin
  simp only [tendsto_uniformly_on_filter, eventually_prod_iff],
  split,
  { rintro h x hx u hu,
    obtain ⟨s, hs1, hs2⟩ := h u hu x hx,
    exact ⟨_, hs2, _, eventually_of_mem hs1 (λ x, id), λ i hi y hy, hi y hy⟩ },
  { rintro h u hu x hx,
    obtain ⟨pa, hpa, pb, hpb, h⟩ := h x hx u hu,
    refine ⟨pb, hpb, eventually_of_mem hpa (λ i hi y hy, h hi hy)⟩ }
end

lemma tendsto_locally_uniformly_iff_filter :
  tendsto_locally_uniformly G g φ ↔
  ∀ x, tendsto_uniformly_on_filter G g φ (𝓝 x) :=
by simpa [← tendsto_locally_uniformly_on_univ, ← nhds_within_univ] using
  @tendsto_locally_uniformly_on_iff_filter _ _ _ _ _ univ _ _ _

In particular, tendsto_locally_uniformly and tendsto_uniformly_on_filter (with nhds) are essentially the same things with the quantifiers reversed, and they both get some use in mathlib in different places but I couldn't find the equivalence.

[Anatole Dedecker]

Not answering the main question, but just FYI the docs#tendsto_uniformly_on_filter stuff is quite recent, so it’s not surprising if we are lacking API here

[Floris van Doorn]

The first is
docs#nhds_within_le_nhds and doesn't need the second argument

[Floris van Doorn]

As Anatole said, @Kevin Wilson added the definition docs#tendsto_uniformly_on_filter only recently in #15871.
I think it might be good to simplify the definitions of tendsto_locally_uniformly_... so that these properties are true by definition. Hopefully that will simplify proving the API for these lemmas (assuming the API for tendsto_uniformly_on_filter is good enough).
In any case, I don't think the other lemmas exist yet.

[Kevin Wilson]

Yes, this was a bit of laziness on my part. The motivation for the `uniformly_on_filter definitions was two-fold:

• It provided a nice way to unify basically all the proofs in that file up to tendsto_locally_uniformly...
• The uniformly_on_filter notion makes it easier to see that uniform convergence is just convergence on the product filter, which is what I needed for the proof I was working on at the time.

100% certain that there's API improvements to be had. :-)

[Vincent Beffara]

That makes sense - the risk would be to duplicate API between the two even though they are equivalent. Probably redefining tendsto_locally_uniformly(_on) in terms of tendsto_uniformly_on_filter would be relatively painless, and would prevent duplication.

[Oliver Nash]

I added docs#tendsto_locally_uniformly_iff_forall_tendsto some time ago (and ended up not using it). If we are considering changing the definition I would suggest we make this true by definition.

[Anatole Dedecker]

Let me just say that this innocent lemma inspired me quite a lot when working on docs#uniform_convergence.uniform_space (and related things), and I think it also what inspired Kevin for docs#tendsto_uniformly_on_filter. I love how one single lemma in 100k can still give ideas to people who are not searching for it

[Kevin Wilson]

Indeed! Many thanks :-)