8. Chapter 12.3 Sequence of holomorphic functions🔗

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

Equivalence of Locally Uniform Convergence and Compact Convergence

We prove that for a sequence of complex-valued functions on a nonempty open connected domain D \subseteq \mathbb{C}

Definition of Locally uniform convergence: at every point of D, there is a neighborhood on which the sequence converges uniformly.

Theorem 12.3.1. The following are equivalent:

Locally uniform convergence: For every z_0 \in D, there exists a neighborhood U of z_0 such that f_k \to f uniformly on U.
Compact convergence: For every compact set K \subset D, f_k → f uniformly on K.

We will need some functions from Filter, Topology and Set

open Filter Topology Set

Define locally uniform convergence and compact convergence.

def LocallyUniformConvergence (F : ℕ → ℂ → ℂ) (f : ℂ → ℂ)
   (D : Set ℂ) : Prop :=
  ∀ z₀ ∈ D, ∃ U ∈ 𝓝 z₀, TendstoUniformlyOn F f atTop U

/-- Compact convergence: the sequence converges
   uniformly on every compact subset of D. -/
def CompactConvergence (F : ℕ → ℂ → ℂ)
 (f : ℂ → ℂ) (D : Set ℂ) : Prop :=
  ∀ K ⊆ D, IsCompact K → TendstoUniformlyOn F f atTop K

Locally uniform convergence implies compact convergence.

/--
Locally uniform convergence implies compact convergence
  for sequences of complex functions on a
  nonempty open connected domain.
-/
theorem locallyUniform_implies_compact
    (D : Set ℂ)
    -- (hD_open : IsOpen D) -- the argument does not
    -- (hD_nonempty : D.Nonempty) -- requires these
    -- (hD_conn : IsConnected D) -- assumptions
    (F : ℕ → ℂ → ℂ) (f : ℂ → ℂ)
    (hloc : LocallyUniformConvergence F f D) :
    CompactConvergence F f D := byD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f D⊢ CompactConvergence F f D
  intro K hK_subD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ D⊢ IsCompact K → TendstoUniformlyOn F f atTop K hK_compactD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact K⊢ TendstoUniformlyOn F f atTop K
  have h_neighborhoods : ∀ z ∈ K, ∃ U ∈ 𝓝 z,
     TendstoUniformlyOn F f atTop U := byD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f D⊢ CompactConvergence F f D
    exact fun z hz => hloc z ( hK_sub hz )All goals completed! 🐙
  generalize_proofs at *D:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact Kh_neighborhoods:∀ z ∈ K, ∃ U ∈ 𝓝 z, TendstoUniformlyOn F f atTop U⊢ TendstoUniformlyOn F f atTop K; (
  choose! U hU using h_neighborhoodsD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact KU:ℂ → Set ℂhU:∀ z ∈ K, U z ∈ 𝓝 z ∧ TendstoUniformlyOn F f atTop (U z)⊢ TendstoUniformlyOn F f atTop K;
  -- Since $K$ is compact, we can find a finite subcover
  -- of $K$ by the neighborhoods $U_z$.
  obtain ⟨z_fin, hz_fin⟩ : ∃ z_fin : Finset ℂ,
    (∀ z ∈ z_fin, z ∈ K) ∧ K ⊆ ⋃ z ∈ z_fin, U z := byD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact KU:ℂ → Set ℂhU:∀ z ∈ K, U z ∈ 𝓝 z ∧ TendstoUniformlyOn F f atTop (U z)⊢ ∃ z_fin, (∀ z ∈ z_fin, z ∈ K) ∧ K ⊆ ⋃ z ∈ z_fin, U z
    have := hK_compact.elim_nhds_subcover U
       fun z hz => hU z hz |>.1D:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact KU:ℂ → Set ℂhU:∀ z ∈ K, U z ∈ 𝓝 z ∧ TendstoUniformlyOn F f atTop (U z)this:∃ t, (∀ x ∈ t, x ∈ K) ∧ K ⊆ ⋃ x ∈ t, U x⊢ ∃ z_fin, (∀ z ∈ z_fin, z ∈ K) ∧ K ⊆ ⋃ z ∈ z_fin, U z; aesopAll goals completed! 🐙;
  generalize_proofs at *D:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact KU:ℂ → Set ℂhU:∀ z ∈ K, U z ∈ 𝓝 z ∧ TendstoUniformlyOn F f atTop (U z)z_fin:Finset ℂhz_fin:(∀ z ∈ z_fin, z ∈ K) ∧ K ⊆ ⋃ z ∈ z_fin, U z⊢ TendstoUniformlyOn F f atTop K; (
  simp_all [ Metric.tendstoUniformlyOn_iff ]D:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact KU:ℂ → Set ℂz_fin:Finset ℂhU:∀ z ∈ K, U z ∈ 𝓝 z ∧ ∀ (ε : ℝ), 0 < ε → ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < εhz_fin:(∀ z ∈ z_fin, z ∈ K) ∧ K ⊆ ⋃ z ∈ z_fin, U z⊢ ∀ (ε : ℝ), 0 < ε → ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ K, dist (f x) (F b x) < ε
  intro ε hεD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact KU:ℂ → Set ℂz_fin:Finset ℂhU:∀ z ∈ K, U z ∈ 𝓝 z ∧ ∀ (ε : ℝ), 0 < ε → ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < εhz_fin:(∀ z ∈ z_fin, z ∈ K) ∧ K ⊆ ⋃ z ∈ z_fin, U zε:ℝhε:0 < ε⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ K, dist (f x) (F b x) < ε
  choose! a ha using fun z hz
     => hU z ( hz_fin.1 z hz ) |>.2 ε hεD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact KU:ℂ → Set ℂz_fin:Finset ℂhU:∀ z ∈ K, U z ∈ 𝓝 z ∧ ∀ (ε : ℝ), 0 < ε → ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < εhz_fin:(∀ z ∈ z_fin, z ∈ K) ∧ K ⊆ ⋃ z ∈ z_fin, U zε:ℝhε:0 < εa:ℂ → ℕha:∀ z ∈ z_fin, ∀ (b : ℕ), a z ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < ε⊢ ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ K, dist (f x) (F b x) < ε
  use Finset.sup z_fin ahD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact KU:ℂ → Set ℂz_fin:Finset ℂhU:∀ z ∈ K, U z ∈ 𝓝 z ∧ ∀ (ε : ℝ), 0 < ε → ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < εhz_fin:(∀ z ∈ z_fin, z ∈ K) ∧ K ⊆ ⋃ z ∈ z_fin, U zε:ℝhε:0 < εa:ℂ → ℕha:∀ z ∈ z_fin, ∀ (b : ℕ), a z ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < ε⊢ ∀ (b : ℕ), z_fin.sup a ≤ b → ∀ x ∈ K, dist (f x) (F b x) < ε
  intro n hnhD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact KU:ℂ → Set ℂz_fin:Finset ℂhU:∀ z ∈ K, U z ∈ 𝓝 z ∧ ∀ (ε : ℝ), 0 < ε → ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < εhz_fin:(∀ z ∈ z_fin, z ∈ K) ∧ K ⊆ ⋃ z ∈ z_fin, U zε:ℝhε:0 < εa:ℂ → ℕha:∀ z ∈ z_fin, ∀ (b : ℕ), a z ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < εn:ℕhn:z_fin.sup a ≤ n⊢ ∀ x ∈ K, dist (f x) (F n x) < ε xhD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact KU:ℂ → Set ℂz_fin:Finset ℂhU:∀ z ∈ K, U z ∈ 𝓝 z ∧ ∀ (ε : ℝ), 0 < ε → ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < εhz_fin:(∀ z ∈ z_fin, z ∈ K) ∧ K ⊆ ⋃ z ∈ z_fin, U zε:ℝhε:0 < εa:ℂ → ℕha:∀ z ∈ z_fin, ∀ (b : ℕ), a z ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < εn:ℕhn:z_fin.sup a ≤ nx:ℂ⊢ x ∈ K → dist (f x) (F n x) < ε hxhD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact KU:ℂ → Set ℂz_fin:Finset ℂhU:∀ z ∈ K, U z ∈ 𝓝 z ∧ ∀ (ε : ℝ), 0 < ε → ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < εhz_fin:(∀ z ∈ z_fin, z ∈ K) ∧ K ⊆ ⋃ z ∈ z_fin, U zε:ℝhε:0 < εa:ℂ → ℕha:∀ z ∈ z_fin, ∀ (b : ℕ), a z ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < εn:ℕhn:z_fin.sup a ≤ nx:ℂhx:x ∈ K⊢ dist (f x) (F n x) < ε
  rcases Set.mem_iUnion₂.1 ( hz_fin.2 hx )
    with ⟨ z, hz, hxz ⟩hD:Set ℂF:ℕ → ℂ → ℂf:ℂ → ℂhloc:LocallyUniformConvergence F f DK:Set ℂhK_sub:K ⊆ DhK_compact:IsCompact KU:ℂ → Set ℂz_fin:Finset ℂhU:∀ z ∈ K, U z ∈ 𝓝 z ∧ ∀ (ε : ℝ), 0 < ε → ∃ a, ∀ (b : ℕ), a ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < εhz_fin:(∀ z ∈ z_fin, z ∈ K) ∧ K ⊆ ⋃ z ∈ z_fin, U zε:ℝhε:0 < εa:ℂ → ℕha:∀ z ∈ z_fin, ∀ (b : ℕ), a z ≤ b → ∀ x ∈ U z, dist (f x) (F b x) < εn:ℕhn:z_fin.sup a ≤ nx:ℂhx:x ∈ Kz:ℂhz:z ∈ z_finhxz:x ∈ U z⊢ dist (f x) (F n x) < ε
  exact ha z hz n
    ( le_trans ( Finset.le_sup hz ) hn ) x hxzAll goals completed! 🐙;))

Compact convergence implies locally uniform convergence

/--
  Compact convergence implies locally uniform
  convergence for sequences of complex functions
  on a nonempty open connected domain.
-/
theorem compact_implies_locallyUniform
    (D : Set ℂ) (hD_open : IsOpen D)
    -- (_hD_nonempty : D.Nonempty)
    -- (_hD_conn : IsConnected D)
    (F : ℕ → ℂ → ℂ)
    (f : ℂ → ℂ)
    (hcpt : CompactConvergence F f D) :
    LocallyUniformConvergence F f D := byD:Set ℂhD_open:IsOpen DF:ℕ → ℂ → ℂf:ℂ → ℂhcpt:CompactConvergence F f D⊢ LocallyUniformConvergence F f D
  -- Given that F converges compactly to f on D,
  -- we need to show that F converges locally
  -- uniformly to f on D.
  intro z₀ hz₀D:Set ℂhD_open:IsOpen DF:ℕ → ℂ → ℂf:ℂ → ℂhcpt:CompactConvergence F f Dz₀:ℂhz₀:z₀ ∈ D⊢ ∃ U ∈ 𝓝 z₀, TendstoUniformlyOn F f atTop U
  obtain ⟨r, hr_pos, hr⟩ :
    ∃ r > 0, (Metric.closedBall z₀ r) ⊆ D := byD:Set ℂhD_open:IsOpen DF:ℕ → ℂ → ℂf:ℂ → ℂhcpt:CompactConvergence F f Dz₀:ℂhz₀:z₀ ∈ D⊢ ∃ r > 0, Metric.closedBall z₀ r ⊆ D
    exact Metric.nhds_basis_closedBall.mem_iff.mp
      ( hD_open.mem_nhds hz₀ )All goals completed! 🐙
  exact ⟨ Metric.closedBall z₀ r, Metric.closedBall_mem_nhds
    _ hr_pos, hcpt _ hr
    ( ProperSpace.isCompact_closedBall _ _ ) ⟩All goals completed! 🐙

/-- Locally uniform convergence and
  compact convergence are equivalent for sequences
  of complex functions on a nonempty open connected
  domain D ⊆ ℂ.
-/
theorem locallyUniform_iff_compact
    (D : Set ℂ) (hD_open : IsOpen D)
    -- (hD_nonempty : D.Nonempty)
    -- (hD_conn : IsConnected D)
    (F : ℕ → ℂ → ℂ) (f : ℂ → ℂ) :
    LocallyUniformConvergence F f D
         ↔ CompactConvergence F f D := byD:Set ℂhD_open:IsOpen DF:ℕ → ℂ → ℂf:ℂ → ℂ⊢ LocallyUniformConvergence F f D ↔ CompactConvergence F f D
  constructormpD:Set ℂhD_open:IsOpen DF:ℕ → ℂ → ℂf:ℂ → ℂ⊢ LocallyUniformConvergence F f D → CompactConvergence F f DmprD:Set ℂhD_open:IsOpen DF:ℕ → ℂ → ℂf:ℂ → ℂ⊢ CompactConvergence F f D → LocallyUniformConvergence F f D
  ·mpD:Set ℂhD_open:IsOpen DF:ℕ → ℂ → ℂf:ℂ → ℂ⊢ LocallyUniformConvergence F f D → CompactConvergence F f D exact locallyUniform_implies_compact D F fAll goals completed! 🐙
    -- hD_open hD_nonempty hD_conn F f
  ·mprD:Set ℂhD_open:IsOpen DF:ℕ → ℂ → ℂf:ℂ → ℂ⊢ CompactConvergence F f D → LocallyUniformConvergence F f D exact compact_implies_locallyUniform D hD_open F fAll goals completed! 🐙
    -- hD_nonempty hD_conn F f