Planar Montel theorem (holomorphic-forms unit)

This file proves Montel's theorem in compactness form for the complex plane, together with the Cauchy derivative estimate feeding it. It is deliberately free of any manifold imports so that finiteness-and-chi (compact-operator argument) can import it cheaply.

Main declarations:

• RS.norm_deriv_le_of_bounded — Cauchy estimate: ‖deriv g z‖ ≤ C / r for g holomorphic and bounded by C on an open set containing closedBall z r.
• RS.montelFamily Ω K C — restrictions to a compact K of functions holomorphic on Ω ⊇ K and bounded by C there, as a subset of C(K, ℂ).
• RS.isCompact_closure_montelFamily — the closure of montelFamily Ω K C is compact in C(K, ℂ) (Cauchy estimate ⇒ equicontinuity ⇒ Arzelà–Ascoli).

theorem RS.norm_deriv_le_of_bounded {Ω : Set ℂ} {g : ℂ → ℂ} {C : ℝ} (hΩ : IsOpen Ω) (hg : DifferentiableOn ℂ g Ω) (hC : ∀ w ∈ Ω, ‖g w‖ ≤ C) {z : ℂ} {r : ℝ} (hr : 0 < r) (hball : Metric.closedBall z r ⊆ Ω) : ‖deriv g z‖ ≤ C / r

Cauchy estimate: if g is holomorphic on an open set Ω and bounded by C there, then its derivative at the center of any closed ball of radius r contained in Ω is bounded by C / r.

def RS.montelFamily (Ω K : Set ℂ) (C : ℝ) : Set C(↑K, ℂ)

The set of restrictions to a compact K of functions holomorphic on an open Ω ⊇ K and bounded by C there.

Equations

• RS.montelFamily Ω K C = {f : C(↑K, ℂ) | ∃ (g : ℂ → ℂ), DifferentiableOn ℂ g Ω ∧ (∀ z ∈ Ω, ‖g z‖ ≤ C) ∧ ∀ (z : ↑K), f z = g ↑z}

theorem RS.norm_sub_le_of_bounded_of_cthickening_subset {Ω K : Set ℂ} (hΩ : IsOpen Ω) {δ C : ℝ} (hδ : 0 < δ) (hsub : Metric.cthickening δ K ⊆ Ω) {g : ℂ → ℂ} (hg : DifferentiableOn ℂ g Ω) (hC : ∀ z ∈ Ω, ‖g z‖ ≤ C) {z w : ℂ} (hz : z ∈ K) (hw : dist w z ≤ δ / 2) : ‖g w - g z‖ ≤ 2 * C / δ * ‖w - z‖

Interior Lipschitz estimate for a bounded holomorphic function: on the half-thickening of a set K whose δ-thickening stays in Ω, g is (2C/δ)-Lipschitz.

theorem RS.isCompact_closure_montelFamily {Ω K : Set ℂ} (hΩ : IsOpen Ω) (hK : IsCompact K) (hKΩ : K ⊆ Ω) (C : ℝ) : IsCompact (closure (montelFamily Ω K C))

Montel's theorem, compactness form: a family of holomorphic functions on an open Ω ⊇ K with a common bound, restricted to the compact K, has compact closure in C(K, ℂ).