tendsto_cobounded_of_meromorphicOrderAt_neg

English

meromorphicAt f x and negative order is equivalent to a cobounded tendsto to infinity; and conversely.

Русский

Смысл: отрицательный порядок эквивалентен совпадению с бесконечностью в cobounded-границах; и наоборот.

LaTeX

$$$ meromorphicOrderAt\ f\ x < 0 \iff Tendsto\ f\ (\mathcal{N}_{\neq} x)\ (\text{cobounded } E) $$$

Lean4

/-- If the order of a meromorphic function is negative, then this function converges to infinity
at this point. See also the iff version `tendsto_cobounded_iff_meromorphicOrderAt_neg`. -/
theorem tendsto_cobounded_of_meromorphicOrderAt_neg (ho : meromorphicOrderAt f x < 0) :
    Tendsto f (𝓝[≠] x) (Bornology.cobounded E) :=
  by
  have hf : MeromorphicAt f x := meromorphicAt_of_meromorphicOrderAt_ne_zero ho.ne
  simp only [← tendsto_norm_atTop_iff_cobounded]
  obtain ⟨m, hm⟩ := WithTop.ne_top_iff_exists.mp ho.ne_top
  have m_neg : m < 0 := by simpa [← hm] using ho
  rcases (meromorphicOrderAt_eq_int_iff hf).1 hm.symm with ⟨g, g_an, gx, hg⟩
  have A : Tendsto (fun z ↦ ‖(z - x) ^ m • g z‖) (𝓝[≠] x) atTop :=
    by
    simp only [norm_smul]
    apply Filter.Tendsto.atTop_mul_pos (C := ‖g x‖) (by simp [gx]) _ g_an.continuousAt.continuousWithinAt.tendsto.norm
    have : Tendsto (fun z ↦ z - x) (𝓝[≠] x) (𝓝[≠] 0) :=
      by
      refine tendsto_nhdsWithin_iff.2 ⟨?_, ?_⟩
      · have : ContinuousWithinAt (fun z ↦ z - x) ({ x }ᶜ) x := ContinuousAt.continuousWithinAt (by fun_prop)
        simpa using this.tendsto
      · filter_upwards [self_mem_nhdsWithin] with y hy
        simpa [sub_eq_zero] using hy
    apply Tendsto.comp (NormedField.tendsto_norm_zpow_nhdsNE_zero_atTop m_neg) this
  apply A.congr'
  filter_upwards [hg] with z hz using by simp [hz]

Похожие утверждения