19.4. Finiteness.BddHol🔗

Jacobians.Finiteness.BddHol — source

BddHolCarrier

The ℂ-submodule of ℂ → ℂ consisting of functions analytic on U, vanishing off U, and bounded on U. The "vanishing off U" clause is a canonical normal form: it does not affect the analytic/bounded content (which only sees U) but makes the sup-U seminorm definite and the embedding into ↥U →ᵇ ℂ injective.

def BddHolCarrier (U : Set ℂ) : Submodule ℂ (ℂ → ℂ) where

BddHol

The Banach space of bounded holomorphic functions on the open set U ⊆ ℂ.

Implemented as the subtype ↥(BddHolCarrier U), but kept *opaque* (non-reducible) so that the ambient subtype UniformSpace/TopologicalSpace instances do not leak and clash with the sup-U-norm NormedAddCommGroup we install below.

def BddHol (U : Set ℂ) : Type

toCarrier

Reinterpret f : BddHol U as the underlying subtype element. Definitional identity.

def toCarrier (f : BddHol U) : ↥(BddHolCarrier U)

toFun

The underlying ℂ → ℂ function of an element of BddHol U.

def toFun (f : BddHol U) : ℂ → ℂ

analyticOn

theorem analyticOn (f : BddHol U) : AnalyticOn ℂ f.toFun U

zero_off

theorem zero_off (f : BddHol U) : ∀ z ∉ U, f.toFun z = 0

bddOn

theorem bddOn (f : BddHol U) : ∃ C, ∀ z ∈ U, ‖f.toFun z‖ ≤ C

toFun_add

@[simp] theorem toFun_add (f g : BddHol U) : (f + g).toFun = f.toFun + g.toFun

toFun_smul

@[simp] theorem toFun_smul (c : ℂ) (f : BddHol U) : (c • f).toFun = c • f.toFun

toFun_injective

theorem toFun_injective : Function.Injective (toFun : BddHol U → (ℂ → ℂ))

toBcf

The restriction of f : BddHol U to ↥U, as a bounded continuous function.

noncomputable def toBcf (f : BddHol U) : ↥U →ᵇ ℂ

toBcf_apply

@[simp] theorem toBcf_apply (f : BddHol U) (z : ↥U) : f.toBcf z = f.toFun z.1

toBcfₗ

The bcf embedding as a ℂ-linear map.

noncomputable def toBcfₗ : BddHol U →ₗ[ℂ] (↥U →ᵇ ℂ) where

toBcf_injective

theorem toBcf_injective : Function.Injective (toBcf : BddHol U → (↥U →ᵇ ℂ))

norm_def

theorem norm_def (f : BddHol U) : ‖f‖ = ‖f.toBcf‖

toBcf_sub

theorem toBcf_sub (f g : BddHol U) : (f - g).toBcf = f.toBcf - g.toBcf

isometry_toBcf

theorem isometry_toBcf : Isometry (toBcf : BddHol U → (↥U →ᵇ ℂ))

isUniformInducing_toBcf

theorem isUniformInducing_toBcf : IsUniformInducing (toBcf : BddHol U → (↥U →ᵇ ℂ))

extend

Extend a bounded continuous function φ : ↥U →ᵇ ℂ to all of ℂ by zero off U. This is the canonical-normal-form preimage candidate for φ under toBcf.

noncomputable def extend (φ : ↥U →ᵇ ℂ) : ℂ → ℂ

extend_mem

theorem extend_mem (φ : ↥U →ᵇ ℂ) {z : ℂ} (hz : z ∈ U) : extend φ z = φ ⟨z, hz⟩

extend_notMem

theorem extend_notMem (φ : ↥U →ᵇ ℂ) {z : ℂ} (hz : z ∉ U) : extend φ z = 0

extend_comp_coe

theorem extend_comp_coe (φ : ↥U →ᵇ ℂ) : extend φ ∘ (Subtype.val : ↥U → ℂ) = ⇑φ

analyticOn_extend_of_tendsto

The limit (in ↥U →ᵇ ℂ) of toBcf-images of BddHol U elements is analytic on U, after extending by zero. The uniform-on-↥U convergence transfers to uniform-on-U (functions on ℂ), hence locally uniform, so the uniform-limit lemma applies.

theorem analyticOn_extend_of_tendsto (hU : IsOpen U) {ι : Type*} {p : Filter ι} [p.NeBot]
    (g : ι → BddHol U) (φ : ↥U →ᵇ ℂ) (hφ : Filter.Tendsto (fun n => (g n).toBcf) p (nhds φ)) :
    AnalyticOn ℂ (extend φ) U

norm_extend_le

extend φ is bounded on U by ‖φ‖.

theorem norm_extend_le (φ : ↥U →ᵇ ℂ) {z : ℂ} (hz : z ∈ U) : ‖extend φ z‖ ≤ ‖φ‖

mem_range_toBcf_of_tendsto

The membership criterion for the image of toBcf: if φ is the p-limit of toBcf-images of BddHol U elements (for U open), then φ lies in the range — its extension by zero is a genuine element of BddHol U.

theorem mem_range_toBcf_of_tendsto (hU : IsOpen U) {ι : Type*} {p : Filter ι} [p.NeBot]
    (g : ι → BddHol U) (φ : ↥U →ᵇ ℂ) (hφ : Filter.Tendsto (fun n => (g n).toBcf) p (nhds φ)) :
    φ ∈ Set.range (toBcf : BddHol U → (↥U →ᵇ ℂ))

isClosed_range_toBcf

The image of toBcf is closed in ↥U →ᵇ ℂ (uniform limits of bounded-holomorphic restrictions are bounded-holomorphic restrictions).

theorem isClosed_range_toBcf (hU : IsOpen U) :
    IsClosed (Set.range (toBcf : BddHol U → (↥U →ᵇ ℂ)))

isComplete_range_toBcf

The image of toBcf is complete (closed in the Banach space ↥U →ᵇ ℂ).

theorem isComplete_range_toBcf (hU : IsOpen U) :
    IsComplete (Set.range (toBcf : BddHol U → (↥U →ᵇ ℂ)))

completeSpace

BddHol U is a Banach space. Completeness follows from the isometric embedding into the complete ↥U →ᵇ ℂ whose image is closed.

theorem completeSpace (hU : IsOpen U) : CompleteSpace (BddHol U)

norm_toFun_le

Pointwise bound: the sup-U norm dominates |f| at every point of U.

theorem norm_toFun_le (f : BddHol U) {z : ℂ} (hz : z ∈ U) : ‖f.toFun z‖ ≤ ‖f‖

restrict

Restriction of f : BddHol U to a compact K ⊆ U, as a bounded continuous function on K. This is the exact element form consumed by the Montel lemma CechFiniteness.isCompact_closure_restrict_bddHolo.

noncomputable def restrict (hKU : K ⊆ U) (f : BddHol U) : K →ᵇ ℂ

restrict_apply

@[simp] theorem restrict_apply (hKU : K ⊆ U) (f : BddHol U) (z : K) :
    restrict hKU f z = f.toFun z.1

restrictₗ

Restriction to K ⊆ U as a ℂ-linear map.

noncomputable def restrictₗ (hKU : K ⊆ U) : BddHol U →ₗ[ℂ] (K →ᵇ ℂ) where

restrictCLM

Restriction continuous-linear map BddHol U →L[ℂ] (K →ᵇ ℂ) for K ⊆ U compact, with operator norm ≤ 1.

noncomputable def restrictCLM (hKU : K ⊆ U) : BddHol U →L[ℂ] (K →ᵇ ℂ)

restrictCLM_apply

@[simp] theorem restrictCLM_apply (hKU : K ⊆ U) (f : BddHol U) :
    restrictCLM hKU f = restrict hKU f

precompBcf

Bounded-continuous precomposition g ↦ (z ↦ g(τ z)) on the compact K, for τ continuous on K mapping into the open U where g lives. Continuity of the composite is g.toFun continuous on U composed with τ : K → U.

noncomputable def precompBcf {τ : ℂ → ℂ} (hτcont : ContinuousOn τ K) (hτmaps : Set.MapsTo τ K U)
    (g : BddHol U) : K →ᵇ ℂ

precompBcf_apply

@[simp] theorem precompBcf_apply {τ : ℂ → ℂ} (hτcont : ContinuousOn τ K) (hτmaps : Set.MapsTo τ K U)
    (g : BddHol U) (z : K) : precompBcf hτcont hτmaps g z = g.toFun (τ z.1)

precompₗ

Precomposition as a ℂ-linear map BddHol U →ₗ[ℂ] (K →ᵇ ℂ).

noncomputable def precompₗ {τ : ℂ → ℂ} (hτcont : ContinuousOn τ K) (hτmaps : Set.MapsTo τ K U) :
    BddHol U →ₗ[ℂ] (K →ᵇ ℂ) where

precompCLM

Precomposition continuous-linear map BddHol U →L[ℂ] (K →ᵇ ℂ) for τ continuous K → U, operator norm ≤ 1. The cross-chart transport of a sup-norm cochain component: a function bounded-holomorphic on chart-b's image, read on the compact K (a chart-a overlap shrinking) through the transition τ = φ_b ∘ φ_a⁻¹.

noncomputable def precompCLM {τ : ℂ → ℂ} (hτcont : ContinuousOn τ K) (hτmaps : Set.MapsTo τ K U) :
    BddHol U →L[ℂ] (K →ᵇ ℂ)

precompCLM_apply

@[simp] theorem precompCLM_apply {τ : ℂ → ℂ} (hτcont : ContinuousOn τ K) (hτmaps : Set.MapsTo τ K U)
    (g : BddHol U) : precompCLM hτcont hτmaps g = precompBcf hτcont hτmaps g