Normal families: equicontinuity of a locally bounded family of holomorphic functions

A family of holomorphic functions on an open set U ⊆ ℂ that is locally bounded — uniformly bounded on every compact subset of U — is automatically equicontinuous on U. This is the analytic heart of Montel's normal-families theorem: combined with Arzelà--Ascoli and an exhaustion/diagonal argument, it yields precompactness for local uniform convergence.

The estimates here are stated for maps ℂ → E into a complex normed space, because nothing in a Cauchy estimate uses the multiplicative structure of the target: Mathlib's Complex.norm_deriv_le_of_forall_mem_sphere_norm_le, which is the sole analytic input, is itself E-valued. Only TauCeti.IsLocallyBoundedOn.equicontinuousOn_deriv needs E complete, and that is because it differentiates twice. Taking E = ℂ recovers the scalar statements.

Local boundedness itself is a statement about compact subsets of the domain and about ‖·‖ alone: it mentions neither holomorphy nor the complex structure of either side. So TauCeti.IsLocallyBoundedOn and its elementary API are stated for a family of maps X → E from an arbitrary topological space into a type with a norm. The domain specialises to ℂ, and the target acquires its normed complex vector space structure, exactly where holomorphy is first assumed: at the Cauchy estimates below.

The mechanism is Cauchy's estimate for the first derivative. Mathlib's Complex.norm_deriv_le_of_forall_mem_sphere_norm_le bounds ‖deriv f c‖ at the centre of a disc; halving the radius turns that pointwise bound into one that is uniform over a ball (norm_deriv_le_of_forall_mem_closedBall_two_mul_norm_le), and the mean value inequality on that ball then bounds dist (f z) (f w) by a multiple of dist z w with a constant depending only on the sup bound (dist_le_of_forall_mem_closedBall_two_mul_norm_le). That constant is uniform in the family, which is exactly equicontinuity.

Main definitions

• TauCeti.IsLocallyBoundedOn F s: the family F of maps out of a topological space is uniformly bounded on every compact subset of s.
• TauCeti.IsLocallyBoundedOn.comp: local boundedness passes to any reindexing of the family, in particular to a subsequence.

Main results

• TauCeti.norm_deriv_le_of_forall_mem_closedBall_norm_le and TauCeti.norm_deriv_le_of_forall_mem_closedBall_two_mul_norm_le: Cauchy's estimate from a sup bound on a closed ball, at the centre and then uniformly over the ball of half the radius.
• TauCeti.dist_le_of_forall_mem_closedBall_two_mul_norm_le and TauCeti.lipschitzOnWith_of_forall_mem_closedBall_two_mul_norm_le: a sup bound M on closedBall c (2 * r) makes a holomorphic function M / r-Lipschitz on ball c r.
• TauCeti.IsLocallyBoundedOn.equicontinuousOn: a locally bounded family of holomorphic functions is equicontinuous. With TauCeti.IsLocallyBoundedOn.exists_forall_norm_le, this supplies the local inputs for an Arzelà--Ascoli exhaustion argument.
• TauCeti.IsLocallyBoundedOn.deriv and TauCeti.IsLocallyBoundedOn.equicontinuousOn_deriv: the derivatives of a locally bounded family of holomorphic functions are again locally bounded, hence also equicontinuous.

This advances the L1 (normal families / Montel) layer of the conformal-mapping roadmap, which fixes local boundedness as "bounded on each compact K ⊆ Ω". The roadmap's scalar generality bar governs the conformal statements it adds — Rouché, Hurwitz, the Riemann mapping theorem — whose hypotheses genuinely use ℂ as the target; the Cauchy estimates below are the inputs those statements consume, and are stated at the generality Mathlib already provides for them. As with the rest of the L0--L3 conformal-mapping material it is coordinated with the upstream Mathlib Riemann-mapping effort leanprover-community/mathlib4#33505, which proves a Montel equicontinuity statement internally as a private lemma; these declarations are a temporary shim, to be deleted and refactored to Mathlib's API once that human-curated work lands.

References

Ahlfors, Complex Analysis, Ch. 5; Conway, Functions of One Complex Variable I, VII.

def TauCeti.IsLocallyBoundedOn {ι : Type u_1} {E : Type u_2} {X : Type u_3} [TopologicalSpace X] [Norm E] (F : ι → X → E) (s : Set X) : Prop

A family F : ι → X → E of maps from a topological space into a type with a norm is locally bounded on s if it is uniformly bounded — with a single constant, independent of the index — on every compact subset of s.

This is the hypothesis of Montel's theorem, in the form fixed by the conformal-mapping roadmap; there X = ℂ and E is a complex normed space.

Equations

• TauCeti.IsLocallyBoundedOn F s = ∀ K ⊆ s, IsCompact K → ∃ (C : ℝ), ∀ (i : ι), ∀ z ∈ K, ‖F i z‖ ≤ C

@[simp]

theorem TauCeti.isLocallyBoundedOn_def {ι : Type u_1} {E : Type u_2} {X : Type u_3} [TopologicalSpace X] [Norm E] {s : Set X} {F : ι → X → E} : IsLocallyBoundedOn F s ↔ ∀ K ⊆ s, IsCompact K → ∃ (C : ℝ), ∀ (i : ι), ∀ z ∈ K, ‖F i z‖ ≤ C

The defining compact-set characterization of local boundedness.

theorem TauCeti.IsLocallyBoundedOn.mono {ι : Type u_1} {E : Type u_2} {X : Type u_3} [TopologicalSpace X] [Norm E] {s t : Set X} {F : ι → X → E} (hb : IsLocallyBoundedOn F s) (hts : t ⊆ s) : IsLocallyBoundedOn F t

Local boundedness is inherited by subsets.

theorem TauCeti.IsLocallyBoundedOn.comp {ι : Type u_1} {E : Type u_2} {X : Type u_3} [TopologicalSpace X] [Norm E] {s : Set X} {F : ι → X → E} {κ : Type u_4} (hb : IsLocallyBoundedOn F s) (σ : κ → ι) : IsLocallyBoundedOn (fun (k : κ) => F (σ k)) s

Local boundedness is inherited by any reindexing of the family: the bound on a compact set is uniform in the index, so it survives being restricted to a subfamily.

The case σ : ℕ → ℕ is the one Montel-based arguments use, where passing to a subsequence must not lose the hypothesis.

theorem TauCeti.IsLocallyBoundedOn.exists_forall_norm_le {ι : Type u_1} {E : Type u_2} {X : Type u_3} [TopologicalSpace X] [Norm E] {s : Set X} {F : ι → X → E} (hb : IsLocallyBoundedOn F s) {z : X} (hz : z ∈ s) : ∃ (C : ℝ), ∀ (i : ι), ‖F i z‖ ≤ C

A locally bounded family is bounded at each point of the set, uniformly in the index.

Together with IsLocallyBoundedOn.equicontinuousOn, this supplies the pointwise bounds used in an Arzelà--Ascoli exhaustion argument.

theorem TauCeti.isLocallyBoundedOn_of_forall_norm_le {ι : Type u_1} {E : Type u_2} {X : Type u_3} [TopologicalSpace X] [Norm E] {s : Set X} {F : ι → X → E} {C : ℝ} (h : ∀ (i : ι), ∀ z ∈ s, ‖F i z‖ ≤ C) : IsLocallyBoundedOn F s

A family bounded by a single constant on all of s is locally bounded on s.

theorem TauCeti.norm_deriv_le_of_forall_mem_closedBall_norm_le {E : Type u_2} {U : Set ℂ} {f : ℂ → E} [NormedAddCommGroup E] [NormedSpace ℂ E] (hf : DifferentiableOn ℂ f U) {c : ℂ} {r M : ℝ} (hr : 0 < r) (hsub : Metric.closedBall c r ⊆ U) (hM : ∀ w ∈ Metric.closedBall c r, ‖f w‖ ≤ M) : ‖deriv f c‖ ≤ M / r

Cauchy's estimate on a closed ball. If f is holomorphic on an open set U containing closedBall c r and ‖f‖ ≤ M on that closed ball, then ‖deriv f c‖ ≤ M / r.

This is Mathlib's Complex.norm_deriv_le_of_forall_mem_sphere_norm_le with its DiffContOnCl hypothesis and its bound on the boundary circle both supplied from a sup bound on a closed ball inside the domain of holomorphy, which is the form the family estimates below consume.

theorem TauCeti.norm_deriv_le_of_forall_mem_closedBall_two_mul_norm_le {E : Type u_2} {U : Set ℂ} {f : ℂ → E} [NormedAddCommGroup E] [NormedSpace ℂ E] (hf : DifferentiableOn ℂ f U) {c : ℂ} {r M : ℝ} (hr : 0 < r) (hsub : Metric.closedBall c (2 * r) ⊆ U) (hM : ∀ w ∈ Metric.closedBall c (2 * r), ‖f w‖ ≤ M) {z : ℂ} (hz : z ∈ Metric.ball c r) : ‖deriv f z‖ ≤ M / r

Cauchy's estimate, uniformly on a ball. If f is holomorphic on an open set U containing closedBall c (2 * r) and ‖f‖ ≤ M on that closed ball, then ‖deriv f z‖ ≤ M / r at every point z of ball c r, not just at the centre.

Halving the radius is what leaves room to recentre norm_deriv_le_of_forall_mem_closedBall_norm_le at an arbitrary z ∈ ball c r: the ball closedBall z r is still inside closedBall c (2 * r).

theorem TauCeti.dist_le_of_forall_mem_closedBall_two_mul_norm_le {E : Type u_2} {U : Set ℂ} {f : ℂ → E} [NormedAddCommGroup E] [NormedSpace ℂ E] (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) {c : ℂ} {r M : ℝ} (hr : 0 < r) (hsub : Metric.closedBall c (2 * r) ⊆ U) (hM : ∀ w ∈ Metric.closedBall c (2 * r), ‖f w‖ ≤ M) {z w : ℂ} (hz : z ∈ Metric.ball c r) (hw : w ∈ Metric.ball c r) : dist (f z) (f w) ≤ M / r * dist z w

A sup bound makes a holomorphic function Lipschitz on half the ball. If f is holomorphic on an open U ⊇ closedBall c (2 * r) and ‖f‖ ≤ M there, then f moves points of ball c r by at most M / r times the distance between them.

The constant M / r depends only on the sup bound and the radius, which is what makes this estimate usable uniformly across a family; see IsLocallyBoundedOn.equicontinuousOn.

theorem TauCeti.lipschitzOnWith_of_forall_mem_closedBall_two_mul_norm_le {E : Type u_2} {U : Set ℂ} {f : ℂ → E} [NormedAddCommGroup E] [NormedSpace ℂ E] (hU : IsOpen U) (hf : DifferentiableOn ℂ f U) {c : ℂ} {r M : ℝ} (hr : 0 < r) (hsub : Metric.closedBall c (2 * r) ⊆ U) (hM : ∀ w ∈ Metric.closedBall c (2 * r), ‖f w‖ ≤ M) : LipschitzOnWith (M / r).toNNReal f (Metric.ball c r)

The LipschitzOnWith form of dist_le_of_forall_mem_closedBall_two_mul_norm_le.

theorem TauCeti.IsLocallyBoundedOn.equicontinuousOn {ι : Type u_1} {E : Type u_2} {U : Set ℂ} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : ι → ℂ → E} (hb : IsLocallyBoundedOn F U) (hU : IsOpen U) (hF : ∀ (i : ι), DifferentiableOn ℂ (F i) U) : EquicontinuousOn F U

The equicontinuity half of Montel's theorem. A locally bounded family of holomorphic functions on an open set U ⊆ ℂ is equicontinuous on U.

Around a point z₀ ∈ U pick r > 0 with closedBall z₀ (2 * r) ⊆ U; local boundedness supplies one constant C bounding the whole family on that compact ball, and dist_le_of_forall_mem_closedBall_two_mul_norm_le then makes every member of the family C / r-Lipschitz on ball z₀ r. A single Lipschitz constant is a common continuity modulus.

theorem TauCeti.IsLocallyBoundedOn.deriv {ι : Type u_1} {E : Type u_2} {U : Set ℂ} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : ι → ℂ → E} (hb : IsLocallyBoundedOn F U) (hU : IsOpen U) (hF : ∀ (i : ι), DifferentiableOn ℂ (F i) U) : IsLocallyBoundedOn (fun (i : ι) => _root_.deriv (F i)) U

The derivatives of a locally bounded family of holomorphic functions are locally bounded.

On a compact K ⊆ U choose δ > 0 with cthickening δ K ⊆ U; a bound C for the family on that compact thickening bounds each derivative on K by C / δ, by Cauchy's estimate on closedBall z δ for z ∈ K.

theorem TauCeti.IsLocallyBoundedOn.equicontinuousOn_deriv {ι : Type u_1} {E : Type u_2} {U : Set ℂ} [NormedAddCommGroup E] [NormedSpace ℂ E] {F : ι → ℂ → E} [CompleteSpace E] (hb : IsLocallyBoundedOn F U) (hU : IsOpen U) (hF : ∀ (i : ι), DifferentiableOn ℂ (F i) U) : EquicontinuousOn (fun (i : ι) => _root_.deriv (F i)) U

The derivatives of a locally bounded family of holomorphic functions are equicontinuous.

The result follows by applying the preceding equicontinuity theorem to the locally bounded derivative family. This is the one statement in this file that needs E complete, because that theorem asks the derivatives themselves to be holomorphic, and holomorphy of deriv f (DifferentiableOn.deriv) rests on the Cauchy integral formula.