Shifted limits

Stream: Is there code for X?

[Michael Stoll]

I'm looking for something like

import Mathlib

example (f : ℂ → ℂ) : Tendsto f (𝓝[≠] 1) (𝓝 1) ↔ Tendsto (fun z ↦ f (1 + z)) (𝓝[≠] 0) (𝓝 1) := by
  sorry

but have difficulties finding it.

[Jireh Loreaux]

Isn't this just an application of docs#Filter.Tendsto.comp ?

[Michael Stoll]

I guess so. I think I was looking for something involving comp, but may have mistyped (it is getting late ...).

[Michael Stoll]

Is there a tactic that clears Tendsto (fun x ↦ 1 - x) (𝓝[≠] 1) (𝓝[≠] 0)?

[Jireh Loreaux]

Hmm... perhaps I led you astray. This works though:

import Mathlib

open Topology Filter

example (f : ℂ → ℂ) : Tendsto f (𝓝[≠] 1) (𝓝 1) ↔ Tendsto (fun z ↦ f (1 + z)) (𝓝[≠] 0) (𝓝 1) := by
  rw [← Function.comp, ← tendsto_map'_iff]
  congr!
  simpa using (Homeomorph.addLeft (1 : ℂ)).toPartialHomeomorph.map_nhdsWithin_eq
    (Set.mem_univ 0) ({0}ᶜ) |>.symm

The first two lines get it down to the essence of the argument.

[Patrick Massot]

That toPartialHomeomorph.map_nhdsWithin_eq is really ugly. If the lemma is missing for homeomorphisms then it should be added.

[Jireh Loreaux]

Indeed, I think it's missing. If I can get to it, I'll PR, but i'm quite busy at the moment.

[Jireh Loreaux]

I guess we have docs#Set.LeftInvOn.map_nhdsWithin_eq, but that's not really better.

[Jireh Loreaux]

Oh, I guess we have docs#Embedding.map_nhdsWithin_eq. So the above can be written:

import Mathlib

open Topology Filter

example (f : ℂ → ℂ) : Tendsto f (𝓝[≠] 1) (𝓝 1) ↔ Tendsto (fun z ↦ f (1 + z)) (𝓝[≠] 0) (𝓝 1) := by
  rw [← Function.comp, ← tendsto_map'_iff]
  congr!
  simpa using (Homeomorph.addLeft (1 : ℂ)).embedding.map_nhdsWithin_eq ({0}ᶜ) 0 |>.symm

which I think is fine.