Vitali's convergence theorem

Vitali's theorem upgrades pointwise convergence on a set with an accumulation point to locally uniform convergence for a locally bounded sequence of holomorphic functions. This completes the Vitali component of layer L1 (normal families / Montel) of the conformal-mapping roadmap.

The proof applies TauCeti.montel twice. First choose one locally uniform subsequential limit g. For an arbitrary subsequence, Montel supplies a further locally uniform limit q. Both limits agree on the pointwise convergence set, hence on the whole preconnected domain by Mathlib's analytic identity theorem AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq. Thus every subsequence has a further subsequence converging to g; the sequential convergence criterion, applied to continuous maps on each compact subset, gives locally uniform convergence of the original sequence.

When the sequence already converges pointwise on the whole of Ω, none of that machinery is needed. Local boundedness makes the sequence equicontinuous on Ω (TauCeti.IsLocallyBoundedOn.equicontinuousOn, the Cauchy-estimate half of Montel's theorem), and on an equicontinuous family pointwise convergence is uniform convergence on each compact subset, by Mathlib's Arzelà–Ascoli lemma Equicontinuous.tendsto_uniformFun_iff_pi. This is why the whole-domain statements below are not corollaries of TauCeti.vitali: they spend no identity theorem, hence need neither an accumulation point nor connectivity of Ω, and no selection theorem, hence do not run on TauCeti.montel at all.

Main results

• TauCeti.vitali — a locally bounded sequence of holomorphic functions on an open preconnected Ω which converges pointwise on a set with an accumulation point in the domain converges locally uniformly to a holomorphic function.
• TauCeti.vitali_of_tendsto — the same theorem with a prescribed pointwise limit on the convergence set.
• TauCeti.tendstoLocallyUniformlyOn_of_isLocallyBoundedOn_of_forall_tendsto — a locally bounded sequence of holomorphic functions converging pointwise on the whole of Ω converges to that limit locally uniformly: on such a sequence, pointwise convergence and locally uniform convergence are the same thing.
• TauCeti.exists_differentiableOn_tendstoLocallyUniformlyOn_of_isLocallyBoundedOn — its existential companion, for a consumer who knows the sequence converges at each point of Ω without a name for the limit.

Holomorphy of such a pointwise limit, and termwise differentiation along it, are then Mathlib's TendstoLocallyUniformlyOn.differentiableOn and TendstoLocallyUniformlyOn.deriv applied to the third of these.

The scalar target

Unlike the estimates of Conformal/NormalFamilies.lean and the Montel results they feed, which are stated for a target complex normed space E, this file keeps the roadmap's scalar target ℂ. For TauCeti.vitali the reason is the proof: it runs TauCeti.montel, which is genuinely false for a target that is not proper, so an E-valued version of that argument would prove only the finite-dimensional case. Vitali's theorem does hold for an arbitrary Banach target (Arendt and Nikolski, Vector-valued holomorphic functions revisited, Math. Z. 234 (2000), §2), but by a different argument — convergence of the Taylor coefficients at an accumulation point, and a clopen propagation — so that generality is a separate theorem rather than a weakening of this one. The whole-domain statements spend no selection theorem, so their argument is target-agnostic; they too are stated at ℂ, the generality the conformal-mapping roadmap sets for the theorems this entry adds and the one at which its consumers use them.

Coordination with upstream Mathlib

Per the Coordination with upstream Mathlib section of ConformalMapping/README.md, L0–L3 material overlaps mathlib4#33505. This file is therefore a temporary shim: if a human-curated Vitali theorem lands in Mathlib, this statement should be backed by it, or deleted and its consumers refactored to the upstream API. Mathlib's TendstoLocallyUniformlyOn.differentiableOn, its identity theorem and its Arzelà–Ascoli framework are consumed rather than restated.

References

• L. Ahlfors, Complex Analysis, Ch. 5 §5.
• J. B. Conway, Functions of One Complex Variable I (GTM 11), Ch. VII §2.

Vitali's theorem

theorem TauCeti.vitali {Ω A : Set ℂ} {F : ℕ → ℂ → ℂ} (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω) (hF : ∀ (n : ℕ), DifferentiableOn ℂ (F n) Ω) (hb : IsLocallyBoundedOn F Ω) (hAΩ : A ⊆ Ω) {z₀ : ℂ} (hz₀ : z₀ ∈ Ω) (hacc : AccPt z₀ (Filter.principal A)) (hpoint : ∀ z ∈ A, ∃ (w : ℂ), Filter.Tendsto (fun (n : ℕ) => F n z) Filter.atTop (nhds w)) : ∃ (g : ℂ → ℂ), DifferentiableOn ℂ g Ω ∧ TendstoLocallyUniformlyOn F g Filter.atTop Ω

Vitali's convergence theorem. Let Ω be an open preconnected subset of ℂ. A locally bounded sequence of holomorphic functions on Ω which converges pointwise on a subset A ⊆ Ω having an accumulation point in Ω converges locally uniformly on Ω to a holomorphic function.

The pointwise limit on A need not be supplied: its existence is enough to determine the holomorphic limit uniquely.

theorem TauCeti.vitali_of_tendsto {Ω A : Set ℂ} {F : ℕ → ℂ → ℂ} (hΩ : IsOpen Ω) (hconn : IsPreconnected Ω) (hF : ∀ (n : ℕ), DifferentiableOn ℂ (F n) Ω) (hb : IsLocallyBoundedOn F Ω) (hAΩ : A ⊆ Ω) {z₀ : ℂ} (hz₀ : z₀ ∈ Ω) (hacc : AccPt z₀ (Filter.principal A)) {g : ℂ → ℂ} (hpoint : ∀ z ∈ A, Filter.Tendsto (fun (n : ℕ) => F n z) Filter.atTop (nhds (g z))) : ∃ (q : ℂ → ℂ), DifferentiableOn ℂ q Ω ∧ Set.EqOn q g A ∧ TendstoLocallyUniformlyOn F q Filter.atTop Ω

Vitali's theorem with prescribed pointwise values. Under the hypotheses of vitali, if the sequence converges pointwise on A to a specified function g, its locally uniform holomorphic limit agrees with g throughout A.

No regularity of g away from A is assumed or concluded; when A is all of Ω the limit is g itself, which is TauCeti.tendstoLocallyUniformlyOn_of_isLocallyBoundedOn_of_forall_tendsto.

Pointwise convergence on the whole domain

theorem TauCeti.tendstoLocallyUniformlyOn_of_isLocallyBoundedOn_of_forall_tendsto {Ω : Set ℂ} {F : ℕ → ℂ → ℂ} (hΩ : IsOpen Ω) (hF : ∀ (n : ℕ), DifferentiableOn ℂ (F n) Ω) (hb : IsLocallyBoundedOn F Ω) {g : ℂ → ℂ} (hpoint : ∀ z ∈ Ω, Filter.Tendsto (fun (n : ℕ) => F n z) Filter.atTop (nhds (g z))) : TendstoLocallyUniformlyOn F g Filter.atTop Ω

On a locally bounded sequence of holomorphic functions, pointwise convergence is locally uniform convergence. If a locally bounded sequence of holomorphic functions on an open Ω converges pointwise at every point of Ω, it converges locally uniformly to that pointwise limit.

This is not a case of TauCeti.vitali, which asks Ω preconnected in order to propagate an identification made on a small set A to the whole domain: here the identification is available at every point already, so the identity theorem — and with it the connectivity — is not needed. The converse implication is immediate, locally uniform convergence being pointwise convergence at each point of Ω.

Neither is it a case of TauCeti.montel: only the equicontinuity half of Montel's theorem is spent, not the selection theorem. On a compact K ⊆ Ω local boundedness makes the restricted sequence equicontinuous (TauCeti.IsLocallyBoundedOn.equicontinuousOn), and on an equicontinuous family the topology of uniform convergence and the topology of pointwise convergence have the same convergent sequences, which is Mathlib's Arzelà–Ascoli lemma Equicontinuous.tendsto_uniformFun_iff_pi.

theorem TauCeti.exists_differentiableOn_tendstoLocallyUniformlyOn_of_isLocallyBoundedOn {Ω : Set ℂ} {F : ℕ → ℂ → ℂ} (hΩ : IsOpen Ω) (hF : ∀ (n : ℕ), DifferentiableOn ℂ (F n) Ω) (hb : IsLocallyBoundedOn F Ω) (hpoint : ∀ z ∈ Ω, ∃ (w : ℂ), Filter.Tendsto (fun (n : ℕ) => F n z) Filter.atTop (nhds w)) : ∃ (g : ℂ → ℂ), DifferentiableOn ℂ g Ω ∧ TendstoLocallyUniformlyOn F g Filter.atTop Ω

The pointwise limit need not be named. A locally bounded sequence of holomorphic functions on an open Ω which converges at each point of Ω converges locally uniformly on Ω to a holomorphic function — the existential companion of the statement above, in the shape TauCeti.vitali takes on a subset A.

The limit is fun z => limUnder atTop fun n => F n z, which the hypothesis identifies as the pointwise limit on Ω; no connectivity of Ω and no accumulation point is involved, exactly as above, and holomorphy of the limit is TendstoLocallyUniformlyOn.differentiableOn.