epsilon-delta and such like in filter form

Stream: Is there code for X?

[Eric Rodriguez]

I'm looking to see if something like Metric.tendsto_nhds' below exists in Mathlib already:

import Mathlib
open Filter Metric Topology

variable {α β : Type*} [PseudoMetricSpace α] {x : α} {s : Set α}

theorem Metric.tendsto_nhds' {f : Filter β} {u : β → α} {a : α} :
    Tendsto u f (𝓝 a) ↔ ∀ᶠ ε in 𝓝[>] 0, ∀ᶠ x in f, dist (u x) a < ε := by

This is basically a restatement of usual eps convergence but in terms of Eventually instead, letting us use all the nice filter stuff such as filter_upwards to avoid the awkward max 1 d^2/4 ... stuff that happens in usual epsilon proofs. I'd be really shocked if this didn't exist in some form, because I honestly thought this was part of the sales points of filters.

I asked @Bhavik Mehta last night, and he sent this proof that he suggested I post here for further advice:

A proof that Bhavik sent

import Mathlib
open Filter Metric Topology

variable {α β : Type*} [PseudoMetricSpace α] {x : α} {s : Set α}

theorem nhdsWithin_basis_closedBall {s : Set α} :
    (𝓝[s] x).HasBasis (fun ε : ℝ => 0 < ε) fun ε => closedBall x ε ∩ s :=
  nhdsWithin_hasBasis nhds_basis_closedBall s

-- Bhavik's original proof
theorem Metric.mem_nhds_iff_mem_nhdsWithin' : s ∈ 𝓝 x ↔ {ε | ball x ε ⊆ s} ∈ 𝓝[>] 0 := by
  rw [nhdsWithin_basis_closedBall.mem_iff, Metric.nhds_basis_ball.mem_iff]
  constructor
  · rintro ⟨ε, hε, hs⟩
    refine ⟨ε, hε, fun y hy => (ball_subset_ball ?_).trans hs⟩
    simp only [Set.mem_inter_iff, mem_closedBall_zero_iff] at hy
    exact le_of_abs_le hy.1
  · rintro ⟨ε, hε, hs⟩
    exact ⟨ε, hε, hs <| by simp [hε, abs_of_pos]⟩

-- Mine, golfed inspired on `eventually_closedBall_subset` which is just a little wrong for this application
theorem Metric.mem_nhds_iff_mem_nhdsWithin : s ∈ 𝓝 x ↔ {ε | ball x ε ⊆ s} ∈ 𝓝[>] 0 := by
  rw [Metric.nhds_basis_ball.mem_iff]
  constructor
  · rintro ⟨ε, εpos, hε⟩
    have : Set.Ioc 0 ε ∈ 𝓝[>] (0 : ℝ) := Ioc_mem_nhdsWithin_Ioi' εpos
    filter_upwards [this] with r hr using (ball_subset_ball hr.2).trans hε
  · rw [nhdsWithin_basis_closedBall.mem_iff]
    exact .imp (fun a ha ↦ ha.imp_right fun hs ↦ hs <| by simp [ha.1, abs_of_pos])

theorem Metric.mem_nhds_iff_eventually : s ∈ 𝓝 x ↔ ∀ᶠ ε in 𝓝[>] 0, ball x ε ⊆ s :=
  Metric.mem_nhds_iff_mem_nhdsWithin

theorem eventually_nhds_iff_eventually {p : α → Prop} :
    (∀ᶠ y in 𝓝 x, p y) ↔ ∀ᶠ ε in 𝓝[>] 0, ∀ ⦃y⦄, dist y x < ε → p y :=
  Metric.mem_nhds_iff_eventually

theorem Metric.tendsto_nhds' {f : Filter β} {u : β → α} {a : α} :
    Tendsto u f (𝓝 a) ↔ ∀ᶠ ε in 𝓝[>] 0, ∀ᶠ x in f, dist (u x) a < ε := by
  rw [tendsto_iff_eventually]
  constructor
  · intro h
    rw [eventually_nhdsWithin_iff]
    exact eventually_of_forall fun ε hε => h <| ball_mem_nhds _ hε
  · intro h p hp
    rw [eventually_nhds_iff_eventually] at hp
    obtain ⟨ε, hε, hε'⟩ := (h.and hp).exists
    filter_upwards [hε] with x hx
    exact hε' hx

[Yury G. Kudryashov]

import Mathlib.Topology.MetricSpace.Basic
open Filter Metric Topology

variable {α β : Type*} [PseudoMetricSpace α] {x : α} {s : Set α}

open Filter

theorem Metric.tendsto_nhds' {f : Filter β} {u : β → α} {a : α} :
    Tendsto u f (𝓝 a) ↔ ∀ᶠ ε in 𝓝[>] 0, ∀ᶠ x in f, dist (u x) a < ε := by
  rw [tendsto_nhds]
  refine ⟨eventually_mem_nhdsWithin.mono, fun h ε ε₀ ↦ ?_⟩
  rcases (h.and (Ioo_mem_nhdsWithin_Ioi' ε₀)).exists with ⟨ε', hε', -, hε'ε⟩
  exact hε'.mono fun x hx ↦ hx.trans hε'ε

[Eric Rodriguez]

Amazing! Do you think this should be standard? And replace all similar statements?

[Eric Rodriguez]

(I envisioned a world where even intro on an Eventually works like a blank FilterUpwards...)

[Anatole Dedecker]

I found myself wanting this kind of statements from time to time, and indeed sometimes I'm wondering wether we're missing something. I think the main reason we don't have a lot of these is that the right hand side does not correspond to any nice filter because of the two ∀ᶠ. We do have docs#Filter.curry which seems very related, but I wouldn't say I understand what it means informally. There's also probably a connection to docs#FIlter.smallSets

[Eric Rodriguez]

from a glance, docs#Filter.curry seems to be exactly right; however, I wouldn't understand the aversion to just a double Eventually; in Mathlib I've always preferred \forall a, \forall b instead of \forall (a, b) for many reasons; this seems like exactly the same situation. docs#hasFDerivAt_of_tendstoUniformlyOnFilter uses it quite a lot and it does seem sensible to do so in such circumstances, but to me (a new filter-cult inductee) it seems unnecessary to turn everything into a single filter

[Anatole Dedecker]

I didn't mean that it's a bad statement, rather that there's not a systematic way to prove it because of this. For example docs#Metric.tendsto_nhds is essentially free from docs#nhds_comap_dist

[Anatole Dedecker]

I'm just sharing random thoughts here, but it seems to me that the potential way to make it more systematic would be to have a version of docs#Filter.HasBasis where the basis stes are "indexed by a filter", if that makes any sense.

[Eric Rodriguez]

Ahh, that makes sense. Filter bases are currently out of my depth so I'll have a read and understand them sometime soon :)

[Yury G. Kudryashov]

Anatole Dedecker said:

I'm just sharing random thoughts here, but it seems to me that the potential way to make it more systematic would be to have a version of docs#Filter.HasBasis where the basis stes are "indexed by a filter", if that makes any sense.

This is an interesting idea. Could you please open a github issue for that?

[Yury G. Kudryashov]

Eric Rodriguez said:

Ahh, that makes sense. Filter bases are currently out of my depth so I'll have a read and understand them sometime soon :)

When you read code about filter bases, keep 3 examples in mind: open balls form a basis of nhds of a point, same for closed balls, and intervals $[a, +\infty)$ form a basis of Filter.atTop.

[Junyan Xu]

restatement of usual eps convergence but in terms of Eventually instead, letting us use all the nice filter stuff such as filter_upwards to avoid the awkward max 1 d^2/4 ... stuff that happens in usual epsilon proofs

Some recent discussions (and indeed the solution is to use 𝓝[>] 0)

[Anatole Dedecker]

#9258, feel free to edit