limits of functions defined on subset of domain

Stream: mathlib4

[Amos Turchet]

In PR #14442 we needed some lemmas about limits of functions f: ℕ → ℝ that coincided with functions g: ℝ → ℝ for which the same limit was already in mathlib.

Example:

lemma tendsto_nat_rpow_div : Filter.Tendsto (fun k : ℕ ↦ (k : ℝ) ^ (k : ℝ)⁻¹)
     Filter.atTop (nhds 1) :=

This existed already for real-valued functions with domain ℝ.

In the original PR we inserted these auxiliary lemmas, proved by hand, but it seems that a more general statement might/should be in Mathlib. Since the PR is still under review we (with @Fabrizio Barroero ) proposed a couple of more general statements like:

theorem aux {l: Filter ℝ} {f : ℝ → ℝ} {g: ℕ → ℝ} (hg: ∀ᶠ n in atTop, g n = f n)
     (hl : Filter.Tendsto f Filter.atTop l) : Filter.Tendsto g Filter.atTop l

or even more generally

theorem aux' {α : Type*} [Nonempty α] [LinearOrder α] {l : Filter ℝ} {f : ℝ → ℝ} {g : α → ℝ}
    {c : α → ℝ} (hc₀ : Monotone c) (hc : ∀ x : ℝ, ∃ a : α, x ≤ c a)
    (hg : ∀ᶠ n in atTop, g n = f (c n)) (hl : Filter.Tendsto f Filter.atTop l) :
    Filter.Tendsto g Filter.atTop l

I guess one could keep generalizing this to arbitrary functions sharing an accumulation point and coinciding eventually at a filter, but we are unsure what is the best way to procede.

Shall we stick with what is needed for our PR (that is about Ostrowski theorem), i.e. the specific lemmas? Or rather try to write some more general statement that works for real-valued functions, like the theorems above? Or even wait for some topology experts to formulate the most general statement?

[Etienne Marion]

I’m definitely not an expert, but isn’t this just a composition of limit, because the coercion from Nat to Real tends to atTop along atTop?

[Etienne Marion]

docs#tendsto_natCast_atTop_atTop