Normal families

DefinitionLocally uniformly bounded sequence of functions#✓fully proved

Let \(U \subseteq \mathbb{C}\) and let \((F_n)_{n \in \mathbb{N}}\) be a sequence of functions \(\mathbb{C} \to \mathbb{C}\). The sequence is locally uniformly bounded on \(U\) when every \(x \in U\) has an open neighbourhood \(V \subseteq U\) and a real \(C \ge 0\) such that \(|F_n(y)| \le C\) for all \(n \in \mathbb{N}\) and all \(y \in V\).

def IsLocallyUniformlyBoundedOn (U : Set ℂ) (F : ℕ → ℂ → ℂ) : Prop :=
  ∀ x ∈ U, ∃ V, IsOpen V ∧ x ∈ V ∧ V ⊆ U ∧ ∃ C : ℝ, 0 ≤ C ∧ ∀ n, ∀ y ∈ V, ‖F n y‖ ≤ C

Used by 6

Used byLocally uniformly bounded sequences are uniformly bounded on compact subsets · A uniformly bounded sequence on an open set is locally uniformly bounded · Montel's theorem · Vitali's convergence theorem · Riemann mapping theorem · Jentzsch's theorem

TheoremA uniformly bounded sequence on an open set is locally uniformly bounded#✓fully proved

Let \(U \subseteq \mathbb{C}\) be open, let \((F_n)_{n \in \mathbb{N}}\) be a sequence of functions \(\mathbb{C} \to \mathbb{C}\) and let \(C \ge 0\) be real. If \(|F_n(y)| \le C\) for all \(n \in \mathbb{N}\) and all \(y \in U\), then \((F_n)\) is locally uniformly bounded on \(U\).

theorem isLocallyUniformlyBoundedOn_of_forall_norm_le {U : Set ℂ} (hU : IsOpen U)
    {F : ℕ → ℂ → ℂ} {C : ℝ} (hC : 0 ≤ C) (hF : ∀ n, ∀ y ∈ U, ‖F n y‖ ≤ C) :
    IsLocallyUniformlyBoundedOn U F

Uses 1 · Used by 2

Statement usesLocally uniformly bounded sequence of functions

Used byRiemann mapping theorem · Jentzsch's theorem

TheoremLocally uniformly bounded sequences are uniformly bounded on compact subsets#✓fully proved

Let \((F_n)_{n \in \mathbb{N}}\) be a sequence of functions \(\mathbb{C} \to \mathbb{C}\) that is locally uniformly bounded on \(U \subseteq \mathbb{C}\). Then for every compact set \(K \subseteq U\) there is a real \(C \ge 0\) with \(|F_n(y)| \le C\) for all \(n \in \mathbb{N}\) and all \(y \in K\).

theorem IsLocallyUniformlyBoundedOn.exists_bound_of_isCompact {U : Set ℂ} {F : ℕ → ℂ → ℂ}
    (hB : IsLocallyUniformlyBoundedOn U F)
    {K : Set ℂ} (hKU : K ⊆ U) (hKc : IsCompact K) :
    ∃ C : ℝ, 0 ≤ C ∧ ∀ n, ∀ y ∈ K, ‖F n y‖ ≤ C

Uses 1 · Used by 1

Statement usesLocally uniformly bounded sequence of functions

Used byMontel's theorem

TheoremMontel's theorem#✓fully proved

Let \(U \subseteq \mathbb{C}\) be open and let \((F_n)_{n \in \mathbb{N}}\) be a sequence of functions \(\mathbb{C} \to \mathbb{C}\), each holomorphic on \(U\), that is locally uniformly bounded on \(U\). Then there are a strictly increasing map \(\varphi : \mathbb{N} \to \mathbb{N}\) and a function \(f : \mathbb{C} \to \mathbb{C}\), holomorphic on \(U\), such that \(F_{\varphi(n)} \to f\) locally uniformly on \(U\) as \(n \to \infty\).

theorem montel
    {U : Set ℂ} (hU : IsOpen U)
    (F : ℕ → ℂ → ℂ) (hF : ∀ n, DifferentiableOn ℂ (F n) U)
    (hB : IsLocallyUniformlyBoundedOn U F) :
    ∃ φ : ℕ → ℕ, StrictMono φ ∧ ∃ f : ℂ → ℂ, DifferentiableOn ℂ f U ∧
      TendstoLocallyUniformlyOn (fun n => F (φ n)) f atTop U

Sources

• Montel's theorem on normal families, P. Montel 1912/1927; see Ahlfors, Functions of One Complex Variable II; Lean is locally uniformly bounded holomorphic family with strictly monotone subsequence locally uniform convergent to holomorphic limit, open U form.

Uses 2 · Used by 3

Statement usesLocally uniformly bounded sequence of functions

Proof usesLocally uniformly bounded sequences are uniformly bounded on compact subsets

Used byVitali's convergence theorem · Riemann mapping theorem · Jentzsch's theorem

TheoremVitali's convergence theorem#✓fully proved

Let \(U \subseteq \mathbb{C}\) be open and preconnected, and let \((F_n)_{n \in \mathbb{N}}\) be a sequence of functions \(\mathbb{C} \to \mathbb{C}\), each holomorphic on \(U\), that is locally uniformly bounded on \(U\). Let \(S \subseteq U\) have an accumulation point \(x_0 \in U\), and let \(g : \mathbb{C} \to \mathbb{C}\) satisfy \(F_n(z) \to g(z)\) as \(n \to \infty\) for every \(z \in S\). Then there is a function \(f : \mathbb{C} \to \mathbb{C}\), holomorphic on \(U\), with \(f(z) = g(z)\) for all \(z \in S\), such that \(F_n \to f\) locally uniformly on \(U\).

theorem vitali
    {U : Set ℂ} (hU : IsOpen U) (hUc : IsPreconnected U)
    (F : ℕ → ℂ → ℂ) (hF : ∀ n, DifferentiableOn ℂ (F n) U)
    (hB : IsLocallyUniformlyBoundedOn U F)
    {S : Set ℂ} (hS : S ⊆ U) (hAcc : ∃ x₀ ∈ U, AccPt x₀ (𝓟 S))
    (g : ℂ → ℂ) (hg : ∀ z ∈ S, Tendsto (fun n => F n z) atTop (𝓝 (g z))) :
    ∃ f : ℂ → ℂ, DifferentiableOn ℂ f U ∧ (∀ z ∈ S, f z = g z) ∧
      TendstoLocallyUniformlyOn F f atTop U

Sources

• Vitali convergence theorem, G. Vitali 1903; see Hille, Analytic Function Theory Vol II and Conway II; Lean is open preconnected U locally uniformly bounded with AccPt accumulation and pointwise limit on S extends to locally uniform holomorphic convergence, Montel-related strengthening.

Uses 2

Statement usesLocally uniformly bounded sequence of functions

Proof usesMontel's theorem

5 fully proved

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.