!3#18887 feat(analysis/specific_limits/complex)

Stream: PR reviews

[Scott Morrison]

@Xavier Généreux, are you still interested in having your PR !3#18887 merged to mathlib3, so that it can be forward ported to Mathlib4? (I'm sorry it wasn't reviewed and merged earlier, I'm not sure what happened; everyone's attention has been on the port for a while.)

You mentioned some planned follow up work, which hopefully it is still possible to do in Mathlib4.

[Alex J. Best]

Iirc @Xavier Généreux was at the Leiden workshop last month and was porting some of his work to lean 4 there before we started on the group projects

[Xavier Généreux]

Hello @Scott Morrison! Yes I am still interested since I would still like to push my follow up work. That being said, because of the freeze, I will need some time to translate it to lean4.

[Xavier Généreux]

Do you think it would just be better to ditch !3#18887 and just do a new PR in mathlib4?

[Jireh Loreaux]

@Xavier Généreux, I have just oneshotted this for you. You can PR the following directly to mathlib4 (with the appropriate moving of the first lemma to the other file). When you open that PR, just link to the first one saying it was already approved in mathlib3 (or ping me for review).

/-
Copyright (c) 2023 Xavier Généreux. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Xavier Généreux, Patrick Massot

! This file was ported from Lean 3 source module main
-/
import Mathlib.Analysis.SpecificLimits.Basic
import Mathlib.Analysis.Complex.ReImTopology

/-!
# A collection of specific limit computations for is_R_or_C
-/


open Set Algebra Filter

theorem tendsto_algebraMap_inverse_atTop_nhds_0_nat (𝕜 : Type _) [Semiring 𝕜] [Algebra ℝ 𝕜]
    [TopologicalSpace 𝕜] [TopologicalSemiring 𝕜] [ContinuousSMul ℝ 𝕜] :
    Tendsto (algebraMap ℝ 𝕜 ∘ fun n : ℕ => (n : ℝ)⁻¹) atTop (nhds 0) :=
  by
  rw [← map_zero (algebraMap ℝ 𝕜)]
  exact Tendsto.comp (continuous_algebraMap ℝ 𝕜).continuousAt tendsto_inverse_atTop_nhds_0_nat

variable (𝕜 : Type _) [IsROrC 𝕜]

theorem IsROrC.tendsto_inverse_atTop_nhds_0_nat : Tendsto (fun n : ℕ => (n : 𝕜)⁻¹) atTop (nhds 0) :=
  by
  rw [show (fun n : ℕ => (n : 𝕜)⁻¹) = (↑) ∘ fun n : ℕ => (n : ℝ)⁻¹ by ext1 n; simp]
  exact tendsto_algebraMap_inverse_atTop_nhds_0_nat 𝕜

[Jireh Loreaux]

As a result, I'll just close the mathlib3 PR.

[Xavier Généreux]

Oh thank you @Jireh Loreaux !

[Xavier Généreux]

I have it done on my computer. I just need to be added as a collaborator on Github to create a branch!

[Scott Morrison]

@Xavier Généreux, please check on github for your invitation.

[Xavier Généreux]

@Jireh Loreaux Done!

[Jireh Loreaux]

@Xavier Généreux I've left a review.