7. Chapter 7.3 Differentiation rules and differentiation at the point at infinity🔗

import Mathlib.Data.Complex.Basic
import Mathlib.Tactic

In this section we formulate three L'Hospital rules for complex functions

The basic version of L'Hospital rule:

Assumptions: f(z₀)=g(z₀)=0, and g'(z₀) ≠ 0
Then, lim (f(z)/g(z)) = f'(z₀)/g'(z₀)

Alternate form of L'Hospital rule

Assumptions: f(z₀)=0, and g(z) has a simple zero at z₀
Then, lim (f(z)/g(z)) = f'(z₀)/g'(z₀)

L'Hospital rule at the point at infinity

Assumptions: f(∞)=g(∞)=0, and g'(∞) ≠ 0
Then, lim (f(z)/g(z)) = f'(∞)/g'(∞)

Open a noncomputable section Lhospital rule

noncomputable section Lhospital_rule

We will need functions from the namespaces Complex, Filter, and Topology.

open Complex Filter Topology

By deriative, we mean Frechet deriative:

f x' = f x + (x' - x) • f' + o(x' - x) where x' converges to x.

This is implemented in Mathlib API HasDerivAt f f' x

HasDerivAt.{u, v} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F]
  [TopologicalSpace F] [ContinuousSMul 𝕜 F] (f : 𝕜 → F) (f' : F) (x : 𝕜) : Prop#check HasDerivAt

The first LHospital rule is similar as in the real case.

Note: We can comment out the line {f g : ℂ → ℂ} {z₀ f' g' : ℂ} and replace it with {f g : ℝ → ℝ} {z₀ f' g' : ℝ}, and the same proof will work.

/--
  L'Hôpital's Rule for complex differentiable functions at
  a point where both vanish.

  If f(z₀) = 0, g(z₀) = 0, and g'(z₀) ≠ 0,
  then lim (f(z)/g(z)) = f'(z₀)/g'(z₀).
-/
theorem complex_lhopital_zero_zero
--{f g : ℝ → ℝ} {z₀ f' g' : ℝ} We can uncomment this line
  {f g : ℂ → ℂ} {z₀ f' g' : ℂ} -- and comment this line
  (hf : HasDerivAt f f' z₀)
  (hg : HasDerivAt g g' z₀)
  (hf0 : f z₀ = 0)
  (hg0 : g z₀ = 0)
  (hg_ne : g' ≠ 0) :
  Tendsto (fun z ↦ f z / g z) (𝓝[≠] z₀)
    (𝓝 (f' / g')) := byf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0hg_ne:g' ≠ 0⊢ Tendsto (fun z => f z / g z) (𝓝[≠] z₀) (𝓝 (f' / g'))


  /- By definition of the derivative, we know that
  \lim_{z \to z_0} \frac{f(z) - f(z_0)}{z - z_0} = f'(z_0)
  \lim_{z \to z_0} \frac{g(z) - g(z_0)}{z - z_0} = g'(z_0).
  -/
  have h_deriv : Filter.Tendsto (fun z =>
   (f z - f z₀) / (z - z₀)) (nhdsWithin z₀ {z₀}ᶜ) (nhds f')
    ∧ Filter.Tendsto (fun z => (g z - g z₀) / (z - z₀))
      (nhdsWithin z₀ {z₀}ᶜ) (nhds g')
    := byf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0hg_ne:g' ≠ 0⊢ Tendsto (fun z => f z / g z) (𝓝[≠] z₀) (𝓝 (f' / g'))
    -- By definition of HasDerivAt, we know that the limit
    --  of (f(z) - f(z₀)) / (z - z₀) as z approaches z₀
    -- is f', and similarly for g.
    have h_deriv_f : Filter.Tendsto (fun z =>
     (f z - f z₀) / (z - z₀))
     (nhdsWithin z₀ {z₀}ᶜ) (nhds f')
      := byf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0hg_ne:g' ≠ 0⊢ Tendsto (fun z => f z / g z) (𝓝[≠] z₀) (𝓝 (f' / g'))
      rw [ hasDerivAt_iff_tendsto_slope ] at hff:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:Tendsto (slope f z₀) (𝓝[≠] z₀) (𝓝 f')hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0hg_ne:g' ≠ 0⊢ Tendsto (fun z => (f z - f z₀) / (z - z₀)) (𝓝[≠] z₀) (𝓝 f')
      simpa [ div_eq_inv_mul ] using hfAll goals completed! 🐙
    have h_deriv_g : Filter.Tendsto (fun z =>
    (g z - g z₀) / (z - z₀))
      (nhdsWithin z₀ {z₀}ᶜ) (nhds g') := byf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0hg_ne:g' ≠ 0⊢ Tendsto (fun z => f z / g z) (𝓝[≠] z₀) (𝓝 (f' / g'))
      rw [ hasDerivAt_iff_tendsto_slope ] at hgf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:Tendsto (slope g z₀) (𝓝[≠] z₀) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0hg_ne:g' ≠ 0h_deriv_f:Tendsto (fun z => (f z - f z₀) / (z - z₀)) (𝓝[≠] z₀) (𝓝 f')⊢ Tendsto (fun z => (g z - g z₀) / (z - z₀)) (𝓝[≠] z₀) (𝓝 g')
      simpa [ div_eq_inv_mul ] using hgAll goals completed! 🐙
    exact ⟨h_deriv_f, h_deriv_g⟩All goals completed! 🐙
  -- Since the denominator is non-zero, we can apply
  -- the fact that the limit of a quotient is
  -- the quotient of the limits.
  have h_quot : Filter.Tendsto (fun z =>
    ((f z - f z₀) / (z - z₀)) / ((g z - g z₀) / (z - z₀)))
    (nhdsWithin z₀ {z₀}ᶜ) (nhds (f' / g')) := byf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0hg_ne:g' ≠ 0⊢ Tendsto (fun z => f z / g z) (𝓝[≠] z₀) (𝓝 (f' / g'))
    exact h_deriv.1.div h_deriv.2 hg_neAll goals completed! 🐙

  -- Apply the congruence rule.
  -- This allows us to prove the limits are the same
  -- if the functions are equal near z₀.
  apply h_quot.congr'f:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0hg_ne:g' ≠ 0h_deriv:Tendsto (fun z => (f z - f z₀) / (z - z₀)) (𝓝[≠] z₀) (𝓝 f') ∧
  Tendsto (fun z => (g z - g z₀) / (z - z₀)) (𝓝[≠] z₀) (𝓝 g')h_quot:Tendsto (fun z => (f z - f z₀) / (z - z₀) / ((g z - g z₀) / (z - z₀))) (𝓝[≠] z₀) (𝓝 (f' / g'))⊢ (fun z => (f z - f z₀) / (z - z₀) / ((g z - g z₀) / (z - z₀))) =ᶠ[𝓝[≠] z₀] fun z => f z / g z

  -- Filter to the set of points where z ≠ z₀.
  -- The filter 𝓝[≠] z₀ guarantees
  -- we only care about z where z ≠ z₀.
  filter_upwards [self_mem_nhdsWithin] with z hzhf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0hg_ne:g' ≠ 0h_deriv:Tendsto (fun z => (f z - f z₀) / (z - z₀)) (𝓝[≠] z₀) (𝓝 f') ∧
  Tendsto (fun z => (g z - g z₀) / (z - z₀)) (𝓝[≠] z₀) (𝓝 g')h_quot:Tendsto (fun z => (f z - f z₀) / (z - z₀) / ((g z - g z₀) / (z - z₀))) (𝓝[≠] z₀) (𝓝 (f' / g'))z:ℂhz:z ∈ {z₀}ᶜ⊢ (f z - f z₀) / (z - z₀) / ((g z - g z₀) / (z - z₀)) = f z / g z

  -- Substitute f(z₀) = 0 and g(z₀) = 0 and
  -- simplify "something - 0"
  simp only [hf0, hg0, sub_zero]hf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0hg_ne:g' ≠ 0h_deriv:Tendsto (fun z => (f z - f z₀) / (z - z₀)) (𝓝[≠] z₀) (𝓝 f') ∧
  Tendsto (fun z => (g z - g z₀) / (z - z₀)) (𝓝[≠] z₀) (𝓝 g')h_quot:Tendsto (fun z => (f z - f z₀) / (z - z₀) / ((g z - g z₀) / (z - z₀))) (𝓝[≠] z₀) (𝓝 (f' / g'))z:ℂhz:z ∈ {z₀}ᶜ⊢ f z / (z - z₀) / (g z / (z - z₀)) = f z / g z

  -- Perform the algebraic cancellation of (z - z₀).
  -- We need to establish that the denominator
  -- (z - z₀) is not zero.
  have h_ne : z - z₀ ≠ 0 := sub_ne_zero.mpr hzhf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0hg_ne:g' ≠ 0h_deriv:Tendsto (fun z => (f z - f z₀) / (z - z₀)) (𝓝[≠] z₀) (𝓝 f') ∧
  Tendsto (fun z => (g z - g z₀) / (z - z₀)) (𝓝[≠] z₀) (𝓝 g')h_quot:Tendsto (fun z => (f z - f z₀) / (z - z₀) / ((g z - g z₀) / (z - z₀))) (𝓝[≠] z₀) (𝓝 (f' / g'))z:ℂhz:z ∈ {z₀}ᶜh_ne:z - z₀ ≠ 0⊢ f z / (z - z₀) / (g z / (z - z₀)) = f z / g z

  -- Use field_simp to cancel the common factor.
  -- Alternatively, you could use:
  -- rw [div_div_div_cancel_right _ _ h_ne]
  field_simp [h_ne]All goals completed! 🐙

We Will use deriv and iteratedDeriv in the next theorem. The API deriv f x returns the derivative of function f at the point x, iteratedDeriv n f x returns the n-th derivative of function f at the point x.

deriv.{u, v} {𝕜 : Type u} [NontriviallyNormedField 𝕜] {F : Type v} [AddCommGroup F] [Module 𝕜 F] [TopologicalSpace F]
  (f : 𝕜 → F) (x : 𝕜) : F#check deriv
iteratedDeriv.{u_1, u_2} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {F : Type u_2} [NormedAddCommGroup F]
  [NormedSpace 𝕜 F] (n : ℕ) (f : 𝕜 → F) (x : 𝕜) : F#check iteratedDeriv

A function g has zero order m if the m-th deriative is not zero, but for all k<m, the k-th deriative vanishes.

def HasZeroOrder (g : ℂ → ℂ) (z₀ : ℂ) (m : ℕ) : Prop :=
  (∀ k < m, iteratedDeriv k g z₀ = 0)
  ∧ (iteratedDeriv m g z₀ ≠ 0)

/--
  L'Hopital's rule for complex functions at a point where
  the denominator has a simple zero (order 1).
  The formula f'/g' is valid whe g has zero order m=1.
-/
theorem complex_lhopital_zero_zero'
  {f g : ℂ → ℂ} {z₀ f' g' : ℂ}
  (hf : HasDerivAt f f' z₀)
  (hg : HasDerivAt g g' z₀)
  (hf0 : f z₀ = 0)
  (hg0 : g z₀ = 0)
  (m : ℕ) (hm : m = 1)
  (hg_zero_order : HasZeroOrder g z₀ m) :
  Tendsto (fun z ↦ f z / g z) (𝓝[≠] z₀) (𝓝 (f' / g'))
    := byf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ m⊢ Tendsto (fun z => f z / g z) (𝓝[≠] z₀) (𝓝 (f' / g'))

  rw [ hasDerivAt_iff_tendsto_slope_zero ] at hf hgf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ • (g (z₀ + t) - g z₀)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ m⊢ Tendsto (fun z => f z / g z) (𝓝[≠] z₀) (𝓝 (f' / g'));

  -- We'll use the fact that if the denominator is
  -- non-zero and the numerator tends to a limit, then
  -- the quotient tends to the quotient of the limits.
  have h_div : Filter.Tendsto (fun t =>
    (f (z₀ + t) - f z₀) / (g (z₀ + t) - g z₀))
    (nhdsWithin 0 {0}ᶜ) (nhds (f' / g'))
    := byf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ m⊢ Tendsto (fun z => f z / g z) (𝓝[≠] z₀) (𝓝 (f' / g'))
    have h_div : Filter.Tendsto (fun t =>
      (f (z₀ + t) - f z₀)/ t / ((g (z₀+t) - g z₀) / t))
      (nhdsWithin 0 {0}ᶜ) (nhds (f' / g'))
      := byf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:HasDerivAt f f' z₀hg:HasDerivAt g g' z₀hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ m⊢ Tendsto (fun z => f z / g z) (𝓝[≠] z₀) (𝓝 (f' / g'))
      convert hf.div hg _ using 1h.e'_3f:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ • (g (z₀ + t) - g z₀)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ m⊢ (fun t => (f (z₀ + t) - f z₀) / t / ((g (z₀ + t) - g z₀) / t)) =
  (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) / fun t => t⁻¹ • (g (z₀ + t) - g z₀)f:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ • (g (z₀ + t) - g z₀)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ m⊢ g' ≠ 0;
      ·h.e'_3f:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ • (g (z₀ + t) - g z₀)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ m⊢ (fun t => (f (z₀ + t) - f z₀) / t / ((g (z₀ + t) - g z₀) / t)) =
  (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) / fun t => t⁻¹ • (g (z₀ + t) - g z₀) exth.e'_3.hf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ • (g (z₀ + t) - g z₀)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ mx✝:ℂ⊢ (f (z₀ + x✝) - f z₀) / x✝ / ((g (z₀ + x✝) - g z₀) / x✝) =
  ((fun t => t⁻¹ • (f (z₀ + t) - f z₀)) / fun t => t⁻¹ • (g (z₀ + t) - g z₀)) x✝; simp [ div_eq_inv_mul ]All goals completed! 🐙
      ·f:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ • (g (z₀ + t) - g z₀)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ m⊢ g' ≠ 0 simp_all [ HasZeroOrder ]f:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂm:ℕhf:Tendsto (fun t => t⁻¹ * f (z₀ + t)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ * g (z₀ + t)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0hm:m = 1hg_zero_order:¬deriv g z₀ = 0⊢ ¬g' = 0;
        contrapose! hg_zero_orderf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂm:ℕhf:Tendsto (fun t => t⁻¹ * f (z₀ + t)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ * g (z₀ + t)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0hm:m = 1hg_zero_order:g' = 0⊢ deriv g z₀ = 0
        rw [ show deriv g z₀ = g' by
        exact ( HasDerivAt.deriv <|
        by rw [ hasDerivAt_iff_tendsto_slope_zero ] ;
            simpa [ div_eq_inv_mul, hg0 ] using hg ) ]f:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂm:ℕhf:Tendsto (fun t => t⁻¹ * f (z₀ + t)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ * g (z₀ + t)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0hm:m = 1hg_zero_order:g' = 0⊢ g' = 0;
            aesopAll goals completed! 🐙
    refine' h_div.congr'
      ( byf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ • (g (z₀ + t) - g z₀)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ mh_div:Tendsto (fun t => (f (z₀ + t) - f z₀) / t / ((g (z₀ + t) - g z₀) / t)) (𝓝[≠] 0) (𝓝 (f' / g'))⊢ (fun t => (f (z₀ + t) - f z₀) / t / ((g (z₀ + t) - g z₀) / t)) =ᶠ[𝓝[≠] 0] fun t =>
  (f (z₀ + t) - f z₀) / (g (z₀ + t) - g z₀) filter_upwards [ self_mem_nhdsWithin ]
        with t hthf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ • (g (z₀ + t) - g z₀)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ mh_div:Tendsto (fun t => (f (z₀ + t) - f z₀) / t / ((g (z₀ + t) - g z₀) / t)) (𝓝[≠] 0) (𝓝 (f' / g'))t:ℂht:t ∈ {0}ᶜ⊢ (f (z₀ + t) - f z₀) / t / ((g (z₀ + t) - g z₀) / t) = (f (z₀ + t) - f z₀) / (g (z₀ + t) - g z₀) using byf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ • (g (z₀ + t) - g z₀)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ mh_div:Tendsto (fun t => (f (z₀ + t) - f z₀) / t / ((g (z₀ + t) - g z₀) / t)) (𝓝[≠] 0) (𝓝 (f' / g'))t:ℂht:t ∈ {0}ᶜ⊢ (f (z₀ + t) - f z₀) / t / ((g (z₀ + t) - g z₀) / t) = (f (z₀ + t) - f z₀) / (g (z₀ + t) - g z₀)
        {f:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:Tendsto (fun t => t⁻¹ • (f (z₀ + t) - f z₀)) (𝓝[≠] 0) (𝓝 f')hg:Tendsto (fun t => t⁻¹ • (g (z₀ + t) - g z₀)) (𝓝[≠] 0) (𝓝 g')hf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ mh_div:Tendsto (fun t => (f (z₀ + t) - f z₀) / t / ((g (z₀ + t) - g z₀) / t)) (𝓝[≠] 0) (𝓝 (f' / g'))t:ℂht:t ∈ {0}ᶜ⊢ (f (z₀ + t) - f z₀) / t / ((g (z₀ + t) - g z₀) / t) = (f (z₀ + t) - f z₀) / (g (z₀ + t) - g z₀)rw [ div_div_div_cancel_right₀ ht ]All goals completed! 🐙} )
  rw [ Metric.tendsto_nhdsWithin_nhds ] at *f:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist (x⁻¹ • (f (z₀ + x) - f z₀)) f' < εhg:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist (x⁻¹ • (g (z₀ + x) - g z₀)) g' < εhf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ mh_div:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist ((f (z₀ + x) - f z₀) / (g (z₀ + x) - g z₀)) (f' / g') < ε⊢ ∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {z₀}ᶜ → dist x z₀ < δ → dist (f x / g x) (f' / g') < ε
  intro ε hεf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist (x⁻¹ • (f (z₀ + x) - f z₀)) f' < εhg:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist (x⁻¹ • (g (z₀ + x) - g z₀)) g' < εhf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ mh_div:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist ((f (z₀ + x) - f z₀) / (g (z₀ + x) - g z₀)) (f' / g') < εε:ℝhε:ε > 0⊢ ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {z₀}ᶜ → dist x z₀ < δ → dist (f x / g x) (f' / g') < ε
  rcases h_div ε hε with ⟨ δ, hδ, H ⟩f:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist (x⁻¹ • (f (z₀ + x) - f z₀)) f' < εhg:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist (x⁻¹ • (g (z₀ + x) - g z₀)) g' < εhf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ mh_div:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist ((f (z₀ + x) - f z₀) / (g (z₀ + x) - g z₀)) (f' / g') < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0H:∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist ((f (z₀ + x) - f z₀) / (g (z₀ + x) - g z₀)) (f' / g') < ε⊢ ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {z₀}ᶜ → dist x z₀ < δ → dist (f x / g x) (f' / g') < ε
  exact ⟨ δ, hδ, fun { x } hx₁ hx₂ =>
    byf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist (x⁻¹ • (f (z₀ + x) - f z₀)) f' < εhg:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist (x⁻¹ • (g (z₀ + x) - g z₀)) g' < εhf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ mh_div:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist ((f (z₀ + x) - f z₀) / (g (z₀ + x) - g z₀)) (f' / g') < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0H:∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist ((f (z₀ + x) - f z₀) / (g (z₀ + x) - g z₀)) (f' / g') < εx:ℂhx₁:x ∈ {z₀}ᶜhx₂:dist x z₀ < δ⊢ dist (f x / g x) (f' / g') < ε simpa [ * ] using H ( sub_ne_zero_of_ne hx₁ )
      <| byf:ℂ → ℂg:ℂ → ℂz₀:ℂf':ℂg':ℂhf:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist (x⁻¹ • (f (z₀ + x) - f z₀)) f' < εhg:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist (x⁻¹ • (g (z₀ + x) - g z₀)) g' < εhf0:f z₀ = 0hg0:g z₀ = 0m:ℕhm:m = 1hg_zero_order:HasZeroOrder g z₀ mh_div:∀ ε > 0, ∃ δ > 0, ∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist ((f (z₀ + x) - f z₀) / (g (z₀ + x) - g z₀)) (f' / g') < εε:ℝhε:ε > 0δ:ℝhδ:δ > 0H:∀ ⦃x : ℂ⦄, x ∈ {0}ᶜ → dist x 0 < δ → dist ((f (z₀ + x) - f z₀) / (g (z₀ + x) - g z₀)) (f' / g') < εx:ℂhx₁:x ∈ {z₀}ᶜhx₂:dist x z₀ < δ⊢ dist (x - z₀) 0 < δ simpa [ dist_eq_norm ] using hx₂All goals completed! 🐙 ⟩

For the point at infinity, we define HasDerivAtInfinity f f' as

\lim_{z \to \infty} z f(z) = f'.

def HasDerivAtInfinity (f : ℂ → ℂ) (f' : ℂ) :=
  Filter.Tendsto (fun z ↦ z * f z)
  (Filter.cocompact ℂ) (nhds f')

We show that if HasDerivAtInfinity f f' and HasDerivAtInfinity g g' with g' \neq 0, then

\lim_{z \to \infty} f(z)/g(z) = f'/g'.

/--
L'Hopital's rule for the form 0/0 at infinity.
    If f and g behave like f'/z and g'/z at infinity,
    then f/g tends to f'/g'.
-/
theorem complex_lhopital_infinity_infinity
  {f g : ℂ → ℂ} {f' g' : ℂ}
  (hf : HasDerivAtInfinity f f')
  (hg : HasDerivAtInfinity g g')
  (hg_ne : g' ≠ 0) :
  Filter.Tendsto (fun z ↦ f z / g z) (Filter.cocompact ℂ)
      (nhds (f' / g')) := byf:ℂ → ℂg:ℂ → ℂf':ℂg':ℂhf:HasDerivAtInfinity f f'hg:HasDerivAtInfinity g g'hg_ne:g' ≠ 0⊢ Tendsto (fun z => f z / g z) (cocompact ℂ) (𝓝 (f' / g'))
    -- We have f(z)/g(z) = (zf(z)) / (zg(z)) for z ≠ 0.
    suffices h_eq : Filter.Tendsto
      (fun z => (z * f z) / (z * g z))
      (Filter.cocompact ℂ) (nhds (f' / g')) byf:ℂ → ℂg:ℂ → ℂf':ℂg':ℂhf:HasDerivAtInfinity f f'hg:HasDerivAtInfinity g g'hg_ne:g' ≠ 0h_eq:Tendsto (fun z => z * f z / (z * g z)) (cocompact ℂ) (𝓝 (f' / g'))⊢ Tendsto (fun z => f z / g z) (cocompact ℂ) (𝓝 (f' / g'))
      refine' h_eq.congr' _f:ℂ → ℂg:ℂ → ℂf':ℂg':ℂhf:HasDerivAtInfinity f f'hg:HasDerivAtInfinity g g'hg_ne:g' ≠ 0h_eq:Tendsto (fun z => z * f z / (z * g z)) (cocompact ℂ) (𝓝 (f' / g'))⊢ (fun z => z * f z / (z * g z)) =ᶠ[cocompact ℂ] fun z => f z / g z ;
      filter_upwards [ ( Filter.mem_cocompact.mpr
        ⟨ Metric.closedBall 0 1,
        ProperSpace.isCompact_closedBall _ _,
        byf:ℂ → ℂg:ℂ → ℂf':ℂg':ℂhf:HasDerivAtInfinity f f'hg:HasDerivAtInfinity g g'hg_ne:g' ≠ 0h_eq:Tendsto (fun z => z * f z / (z * g z)) (cocompact ℂ) (𝓝 (f' / g'))⊢ (Metric.closedBall 0 1)ᶜ ⊆ ?m.60 aesop_catAll goals completed! 🐙 ⟩ ) ] with x hxhf:ℂ → ℂg:ℂ → ℂf':ℂg':ℂhf:HasDerivAtInfinity f f'hg:HasDerivAtInfinity g g'hg_ne:g' ≠ 0h_eq:Tendsto (fun z => z * f z / (z * g z)) (cocompact ℂ) (𝓝 (f' / g'))x:ℂhx:x ∈ (Metric.closedBall 0 1)ᶜ⊢ x * f x / (x * g x) = f x / g x ;
      by_cases h : x = 0posf:ℂ → ℂg:ℂ → ℂf':ℂg':ℂhf:HasDerivAtInfinity f f'hg:HasDerivAtInfinity g g'hg_ne:g' ≠ 0h_eq:Tendsto (fun z => z * f z / (z * g z)) (cocompact ℂ) (𝓝 (f' / g'))x:ℂhx:x ∈ (Metric.closedBall 0 1)ᶜh:x = 0⊢ x * f x / (x * g x) = f x / g xnegf:ℂ → ℂg:ℂ → ℂf':ℂg':ℂhf:HasDerivAtInfinity f f'hg:HasDerivAtInfinity g g'hg_ne:g' ≠ 0h_eq:Tendsto (fun z => z * f z / (z * g z)) (cocompact ℂ) (𝓝 (f' / g'))x:ℂhx:x ∈ (Metric.closedBall 0 1)ᶜh:¬x = 0⊢ x * f x / (x * g x) = f x / g x <;>posf:ℂ → ℂg:ℂ → ℂf':ℂg':ℂhf:HasDerivAtInfinity f f'hg:HasDerivAtInfinity g g'hg_ne:g' ≠ 0h_eq:Tendsto (fun z => z * f z / (z * g z)) (cocompact ℂ) (𝓝 (f' / g'))x:ℂhx:x ∈ (Metric.closedBall 0 1)ᶜh:x = 0⊢ x * f x / (x * g x) = f x / g xnegf:ℂ → ℂg:ℂ → ℂf':ℂg':ℂhf:HasDerivAtInfinity f f'hg:HasDerivAtInfinity g g'hg_ne:g' ≠ 0h_eq:Tendsto (fun z => z * f z / (z * g z)) (cocompact ℂ) (𝓝 (f' / g'))x:ℂhx:x ∈ (Metric.closedBall 0 1)ᶜh:¬x = 0⊢ x * f x / (x * g x) = f x / g x
      simp_all [ mul_div_mul_left ]All goals completed! 🐙

    /- Since $z * f(z) \to f'$ and $z * g(z) \to g'$
        as $z \to \infty$, we can use the fact that
        the ratio of two functions that tend to their
        respective limits also tends to the ratio
        of the limits. -/
    have h_tendsto : Filter.Tendsto
      (fun z => z * f z) (Filter.cocompact ℂ) (nhds f')
        ∧ Filter.Tendsto (fun z => z * g z)
        (Filter.cocompact ℂ) (nhds g') := byf:ℂ → ℂg:ℂ → ℂf':ℂg':ℂhf:HasDerivAtInfinity f f'hg:HasDerivAtInfinity g g'hg_ne:g' ≠ 0⊢ Tendsto (fun z => f z / g z) (cocompact ℂ) (𝓝 (f' / g'))
      unfold HasDerivAtInfinity at hf hgf:ℂ → ℂg:ℂ → ℂf':ℂg':ℂhf:Tendsto (fun z => z * f z) (cocompact ℂ) (𝓝 f')hg:Tendsto (fun z => z * g z) (cocompact ℂ) (𝓝 g')hg_ne:g' ≠ 0⊢ Tendsto (fun z => z * f z) (cocompact ℂ) (𝓝 f') ∧ Tendsto (fun z => z * g z) (cocompact ℂ) (𝓝 g')
      aesopAll goals completed! 🐙;
    exact h_tendsto.1.div h_tendsto.2 hg_neAll goals completed! 🐙

end Lhospital_rule