Shift pointed neighborhoods?

Stream: Is there code for X?

[Michael Stoll]

I'm looking for the following:

import Mathlib

open Topology

example : Filter.Tendsto (fun w : ℂ ↦ 1 + w) (𝓝[≠] 0) (𝓝[≠] 1) := by
  sorry

There are lemmas like docs#Filter.Tendsto.const_add, but they seem to always need a non-pointed neighborhood in the target. I tried to fiddle around a bit with apply?, but it did not seem to produce anything helpful.

@loogle Filter.Tendsto, "const", "add"

[loogle]

:search: Filter.tendsto_atBot_add_const_left, Filter.tendsto_atBot_add_const_right, and 11 more

[Michael Stoll]

example : Filter.Tendsto (fun w : ℂ ↦ 1 + w) (𝓝[≠] 0) (𝓝[≠] 1) := by
  refine Filter.tendsto_iff_comap.mpr <| Eq.le ?_

leaves me at ⊢ 𝓝[≠] 0 = Filter.comap (fun w ↦ 1 + w) (𝓝[≠] 1), which looks like simp or so should be able to solve it, but no luck...

[Anatole Dedecker]

I would try to use docs#tendsto_nhdsWithin_iff together with docs#eventually_nhdsWithin_of_forall

[Anatole Dedecker]

Or use the fact that your map is an homeomorphism and docs#Embedding.map_nhdsWithin_eq

[Anatole Dedecker]

But I guess some more specialized API for the case of homeomorphisms wouldn’t hurt

[Michael Stoll]

This comes up when you want to change the base-point of a limit, as in

open Topology Filter

example (f : ℂ → ℂ) (a b c : ℂ) :
    Tendsto (fun z ↦ f (a + z)) (𝓝[≠] b) (𝓝 c) ↔ Tendsto f (𝓝[≠] (a + b)) (𝓝 c) := sorry

It would be nice to have lemmas in Mathlib that make that easy.

[Michael Stoll]

To un-#xy, this is what I'm really after here:

import Mathlib

open Topology Filter

example {f : ℂ → ℂ} (h : Tendsto (fun z ↦ (z - 1) * f z) (𝓝[≠] 1) (𝓝 1)) :
    (fun w ↦ f (1 + w)) =O[𝓝[≠] 1] (‖.‖⁻¹) := by
  sorry

Maybe the approach I was taking is not the best one?

[Patrick Massot]

Didn't we have the exact same conversation a couple of weeks ago?

[Patrick Massot]

In https://leanprover.zulipchat.com/#narrow/stream/217875-Is-there-code-for-X.3F/topic/Shifted.20limits/near/409025823?

[Michael Stoll]

Right (I had forgotten about that conversation). I guess the lemmas you were suggesting there are still missing. So I'll try to open a PR adding them. Re-reading, I see that you did open #9166, but it has not been merged so far.

[Michael Stoll]

It is labeled "awaiting-author" since three weeks or so...

[Patrick Massot]

Ok, I commited the suggested change, let's see if it builds.

[Michael Stoll]

Is there an easy way of constructing the homeomorphism given by translation (on a topological (additive) group)?

[Yaël Dillies]

docs#Homeomorph.addRight

[Michael Stoll]

(I needed docs#Homeomorph.addLeft instead.)