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.

[Michael Stoll]

Michael Stoll said:

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

I'm still stuck at this. To un-#xy:

import Mathlib

local notation "Γ" => Complex.Gamma

open Complex Topology Filter Metric in
lemma tendsto_sub_one_mul_Gamma_one_sub_nhds_one :
    Tendsto (fun x ↦ (x - 1) * Γ (1 - x)) (𝓝[≠] 1) (𝓝 (-1)) := by
  conv =>
    enter [1, x]
    rw [show (x - 1) * Γ (1 - x) = - ((1 - x) * Γ (1 - x)) by ring]
  refine (tendsto_self_mul_Gamma_nhds_zero.comp ?_).neg
  convert tendsto_map
  sorry -- goal is `𝓝[≠] 0 = map (fun x ↦ 1 - x) (𝓝[≠] 1)`

[Michael Stoll]

This should be easy, but trying to use docs#Embedding.map_nhdsWithin_eq together with some docs#Homeomorph gave me trouble, because I could not identify the homeomorphism with the function...

[Michael Stoll]

Here is another one that should be easy, but which I found tricky:

lemma dist_one (m : ℕ) : dist (m : ℂ) 1 < 1 ↔ m = 1 := by
  refine ⟨fun H ↦ ?_, fun H ↦ by simp [H]⟩
  rwa [dist_eq, ← Int.cast_one, ← Int.cast_Nat_cast, ← Int.cast_sub, ← int_cast_abs, ← Int.cast_abs,
      ← Int.cast_one (R := ℝ), Int.cast_lt, Int.abs_lt_one_iff, sub_eq_zero, ← Nat.cast_one,
      Int.ofNat_inj] at H

[Ruben Van de Velde]

Needs more lemmas!

import Mathlib

open Complex

lemma Nat.dist_eq_dist (m n : ℕ) : Dist.dist m n = Nat.dist m n := by
  rw [Nat.dist_eq, Nat.dist_eq_max_sub_min, ← max_sub_min_eq_abs']
  simp

lemma dist_nat_cast' (m n : ℕ) : dist (m : ℂ) n = dist m n := by
  rw [dist_eq, Nat.dist_eq]
  norm_cast -- not sure why this still introduces `Int.subNatNat`
  rw [Int.cast_abs, ← int_cast_abs]

lemma dist_nat_cast (m n : ℕ) : dist (m : ℂ) n = Nat.dist m n := by
  rw [dist_nat_cast', Nat.dist_eq_dist]

lemma Nat.dist_eq_zero_iff (m n : ℕ) : dist m n = 0 ↔ m = n :=
  ⟨Nat.eq_of_dist_eq_zero, Nat.dist_eq_zero⟩

lemma dist_const (m n : ℕ) : dist (m : ℂ) n < 1 ↔ m = n := by
  rw [dist_nat_cast, Nat.cast_lt_one, Nat.dist_eq_zero_iff]

lemma dist_one (m : ℕ) : dist (m : ℂ) 1 < 1 ↔ m = 1 := by
  exact_mod_cast dist_const m 1

[Patrick Massot]

Regarding the previous question: struggling with such trivialities always means missing stupid lemmas, often simp lemmas. You simply need to have the patience to write those lemmas and put them into Mathlib.

import Mathlib

open Topology Filter

@[to_additive (attr := simp)] lemma Homeomorph.mulLeft_apply {G : Type*} [TopologicalSpace G] [Group G] [ContinuousMul G]
  (a b : G) : Homeomorph.mulLeft a b = a * b := rfl

@[to_additive (attr := simp)] lemma Homeomorph.mulRight_apply {G : Type*} [TopologicalSpace G] [Group G] [ContinuousMul G]
  (a b : G) : Homeomorph.mulRight a b = b * a := rfl

@[to_additive (attr := simp)] lemma Homeomorph.inv_apply {G : Type*} [TopologicalSpace G] [InvolutiveInv G] [ContinuousInv G] (a : G) :
  Homeomorph.inv G a = a⁻¹ := rfl

lemma Homeomorph.image_compl {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y] (f : X ≃ₜ Y)
    (s : Set X) : f '' (sᶜ) = (f '' s)ᶜ := f.toEquiv.image_compl s

lemma Homeomorph.map_punctured_nhds_eq {X Y : Type*} [TopologicalSpace X] [TopologicalSpace Y]
    (f : X ≃ₜ Y) (x : X) : map f (𝓝[≠] x) = 𝓝[≠] (f x) := by
  convert f.embedding.map_nhdsWithin_eq ({x}ᶜ) x
  rw [f.image_compl, Set.image_singleton]

local notation "Γ" => Complex.Gamma

open Complex Topology Filter Metric in
lemma tendsto_sub_one_mul_Gamma_one_sub_nhds_one :
    Tendsto (fun x ↦ (x - 1) * Γ (1 - x)) (𝓝[≠] 1) (𝓝 (-1)) := by
  conv =>
    enter [1, x]
    rw [show (x - 1) * Γ (1 - x) = - ((1 - x) * Γ (1 - x)) by ring]
  refine (tendsto_self_mul_Gamma_nhds_zero.comp ?_).neg
  convert tendsto_map
  symm
  simpa using ((Homeomorph.neg ℂ).trans (Homeomorph.addLeft (1 : ℂ))).map_punctured_nhds_eq 1

[Patrick Massot]

The fact the first three lemmas are missing is very weird. They should be the first lemmas after the definition of these homeomorphisms.

[Patrick Massot]

Maybe they should even be auto-generated by @[simps] or something.

[Michael Stoll]

I am not really feeling at home in this part of Mathlib, so I would appreciate it if someone more knowledgeable would PR these missing lemmas. (Alternatively, I'd need some help with finding the right places to put them.)

[Ruben Van de Velde]

Fwiw:

@[to_additive (attr := simp)] lemma Homeomorph.mulLeft_apply {G : Type*} [TopologicalSpace G] [Group G] [ContinuousMul G]
  (a b : G) : Homeomorph.mulLeft a b = a * b := by simp? says simp only [coe_mulLeft]

[Ruben Van de Velde]

But there's zero lemmas about Homeomorph.inv

[Patrick Massot]

Ok, so the first two are there already, but didn't trigger because the third one was missing

[Patrick Massot]

I opened #9166