Bounded holomorphic maps on an open set

For an open subset U of a complex normed space V and a complex normed space E, boundedHolomorphicFunctions E U is the space H^∞(U, E) of bounded holomorphic maps U → E, as a complex subspace of the bounded continuous maps U →ᵇ E with the supremum norm. Holomorphy can be checked on any ambient representative V → E. An ambient map that is holomorphic and bounded on U gives an element (TauCeti.BoundedHolomorphicFunctions.of), and every element has the zero extension TauCeti.BoundedHolomorphicFunctions.extend as a canonical ambient representative.

When E is complete, H^∞(U, E) is closed in U →ᵇ E (TauCeti.isClosed_boundedHolomorphicFunctions), hence a Banach space. Restriction to a smaller open set U' ⊆ U is a continuous linear map of norm at most one (TauCeti.BoundedHolomorphicFunctions.restrict), and these maps are functorial. Holomorphic germs along a compact set form the inductive limit of these Banach spaces over shrinking neighbourhoods; the two further properties below say that its bonding maps are compact and injective:

• Compactness (Montel). If U' lies in a compact subset of U and E is proper (for a complex normed space, finite-dimensional), restriction is a compact operator (TauCeti.BoundedHolomorphicFunctions.isCompactOperator_restrict).
• Injectivity (identity theorem). If V is finite-dimensional, E is complete, and every connected component of U meets U', restriction is injective (TauCeti.BoundedHolomorphicFunctions.restrict_injective).

References

• J. Mujica, Complex Analysis in Banach Spaces, North-Holland Mathematics Studies 120, North-Holland, 1986.
• G. Köthe, Dualität in der Funktionentheorie, J. Reine Angew. Math. 191 (1953), 30–49.

def TauCeti.boundedHolomorphicFunctions {V : Type u_1} (E : Type u_2) [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] (U : TopologicalSpace.Opens V) : Submodule ℂ (BoundedContinuousFunction (↥U) E)

The space H^∞(U, E) of bounded holomorphic maps on an open set U of a complex normed space, as a subspace of the bounded continuous maps U →ᵇ E with the supremum norm. A bounded continuous map belongs to it when some ambient map V → E agreeing with it on U is holomorphic on U.

theorem TauCeti.mem_boundedHolomorphicFunctions_iff {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} {f : BoundedContinuousFunction (↥U) E} : f ∈ boundedHolomorphicFunctions E U ↔ ∃ (g : V → E), DifferentiableOn ℂ g ↑U ∧ ∀ (z : ↥U), g ↑z = f z

Membership means having an ambient holomorphic representative.

theorem TauCeti.mem_boundedHolomorphicFunctions_iff_of_eqOn {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} {f : BoundedContinuousFunction (↥U) E} {g : V → E} (hgf : ∀ (z : ↥U), g ↑z = f z) : f ∈ boundedHolomorphicFunctions E U ↔ DifferentiableOn ℂ g ↑U

Holomorphy can be tested on any ambient map agreeing with f on U.

theorem TauCeti.mem_boundedHolomorphicFunctions_iff_extend {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} {f : BoundedContinuousFunction (↥U) E} : f ∈ boundedHolomorphicFunctions E U ↔ DifferentiableOn ℂ (Function.extend Subtype.val ⇑f fun (x : V) => 0) ↑U

Equivalently, the extension by zero is holomorphic on U.

theorem TauCeti.isClosed_boundedHolomorphicFunctions {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (U : TopologicalSpace.Opens V) : IsClosed ↑(boundedHolomorphicFunctions E U)

For complete E, the bounded holomorphic maps form a closed subspace of the bounded continuous maps: a uniform limit of holomorphic maps is holomorphic.

instance TauCeti.instCompleteSpaceSubtypeBoundedContinuousFunctionMemOpensSubmoduleComplexBoundedHolomorphicFunctions {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] [CompleteSpace E] (U : TopologicalSpace.Opens V) : CompleteSpace ↥(boundedHolomorphicFunctions E U)

For complete E, H^∞(U, E) is a Banach space.

def TauCeti.BoundedHolomorphicFunctions.of {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] (U : TopologicalSpace.Opens V) (g : V → E) (hg : DifferentiableOn ℂ g ↑U) (C : ℝ) (hC : ∀ z ∈ U, ‖g z‖ ≤ C) : ↥(boundedHolomorphicFunctions E U)

Restrict an ambient map, holomorphic on U and bounded there by C, to an element of H^∞(U, E).

@[simp]

theorem TauCeti.BoundedHolomorphicFunctions.of_apply {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} (g : V → E) (hg : DifferentiableOn ℂ g ↑U) (C : ℝ) (hC : ∀ z ∈ U, ‖g z‖ ≤ C) (z : ↥U) : ↑(of U g hg C hC) z = g ↑z

noncomputable def TauCeti.BoundedHolomorphicFunctions.extend {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} (f : ↥(boundedHolomorphicFunctions E U)) : V → E

The ambient representative obtained by extending by zero.

@[simp]

theorem TauCeti.BoundedHolomorphicFunctions.extend_apply {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} (f : ↥(boundedHolomorphicFunctions E U)) (z : ↥U) : extend f ↑z = ↑f z

@[simp]

theorem TauCeti.BoundedHolomorphicFunctions.extend_apply_of_notMem {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} (f : ↥(boundedHolomorphicFunctions E U)) {z : V} (hz : z ∉ U) : extend f z = 0

The zero extension vanishes outside U.

theorem TauCeti.BoundedHolomorphicFunctions.differentiableOn_extend {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} (f : ↥(boundedHolomorphicFunctions E U)) : DifferentiableOn ℂ (extend f) ↑U

The zero extension is holomorphic on U.

theorem TauCeti.BoundedHolomorphicFunctions.norm_extend_apply_le {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} (f : ↥(boundedHolomorphicFunctions E U)) (z : V) : ‖extend f z‖ ≤ ‖f‖

The zero extension is bounded everywhere by the supremum norm.

theorem TauCeti.BoundedHolomorphicFunctions.memLp_extend {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} [MeasurableSpace V] [OpensMeasurableSpace V] [SecondCountableTopologyEither V E] {μ : MeasureTheory.Measure V} [MeasureTheory.IsFiniteMeasure (μ.restrict ↑U)] (p : ENNReal) (f : ↥(boundedHolomorphicFunctions E U)) : MeasureTheory.MemLp (extend f) p (μ.restrict ↑U)

Bounded holomorphic functions on a finite-measure open set have an Lᵖ zero extension for every exponent, including infinity. The range need not be complete or finite-dimensional.

@[simp]

theorem TauCeti.BoundedHolomorphicFunctions.of_extend {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} (f : ↥(boundedHolomorphicFunctions E U)) : of U (extend f) ⋯ ‖↑f‖ ⋯ = f

Recovering a bounded holomorphic map from its zero extension does not change it.

theorem TauCeti.BoundedHolomorphicFunctions.dist_apply_le_of_ball_subset {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} (f : ↥(boundedHolomorphicFunctions E U)) {x z : ↥U} {R : ℝ} (hR : Metric.ball (↑x) R ⊆ ↑U) (hz : dist z x < R) : dist (↑f z) (↑f x) ≤ 2 * ‖f‖ / R * dist z x

Cauchy estimate. On a ball of radius R inside U, a bounded holomorphic map f is Lipschitz at the centre with constant 2 * ‖f‖ / R.

noncomputable def TauCeti.BoundedHolomorphicFunctions.restrict {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U U' : TopologicalSpace.Opens V} (h : U' ≤ U) : ↥(boundedHolomorphicFunctions E U) →L[ℂ] ↥(boundedHolomorphicFunctions E U')

Restriction of bounded holomorphic maps to a smaller open set.

@[simp]

theorem TauCeti.BoundedHolomorphicFunctions.restrict_apply {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U U' : TopologicalSpace.Opens V} (h : U' ≤ U) (f : ↥(boundedHolomorphicFunctions E U)) (z : ↥U') : ↑((restrict h) f) z = ↑f ⟨↑z, ⋯⟩

@[simp]

theorem TauCeti.BoundedHolomorphicFunctions.restrict_of {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U U' : TopologicalSpace.Opens V} (h : U' ≤ U) (g : V → E) (hg : DifferentiableOn ℂ g ↑U) (C : ℝ) (hC : ∀ z ∈ U, ‖g z‖ ≤ C) : (restrict h) (of U g hg C hC) = of U' g ⋯ C ⋯

Restriction agrees with restricting the same ambient representative.

theorem TauCeti.BoundedHolomorphicFunctions.norm_restrict_apply_le {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U U' : TopologicalSpace.Opens V} (h : U' ≤ U) (f : ↥(boundedHolomorphicFunctions E U)) : ‖(restrict h) f‖ ≤ ‖f‖

Restriction does not increase the supremum norm.

theorem TauCeti.BoundedHolomorphicFunctions.norm_restrict_le {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U U' : TopologicalSpace.Opens V} (h : U' ≤ U) : ‖restrict h‖ ≤ 1

Restriction has operator norm at most one.

@[simp]

theorem TauCeti.BoundedHolomorphicFunctions.restrict_refl {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U : TopologicalSpace.Opens V} : restrict ⋯ = ContinuousLinearMap.id ℂ ↥(boundedHolomorphicFunctions E U)

Restriction to the same open set is the identity.

@[simp]

theorem TauCeti.BoundedHolomorphicFunctions.restrict_comp_restrict {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U U' U'' : TopologicalSpace.Opens V} (h : U' ≤ U) (h' : U'' ≤ U') : restrict h' ∘SL restrict h = restrict ⋯

Restrictions compose.

theorem TauCeti.BoundedHolomorphicFunctions.isCompactOperator_restrict {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U U' : TopologicalSpace.Opens V} [ProperSpace E] {K : Set V} (hK : IsCompact K) (hU'K : ↑U' ⊆ K) (hKU : K ⊆ ↑U) : IsCompactOperator ⇑(restrict ⋯)

Montel's theorem for bounded holomorphic maps. If U' lies in a compact subset K of U and E is proper, restriction H^∞(U, E) → H^∞(U', E) is a compact operator.

theorem TauCeti.BoundedHolomorphicFunctions.isCompactOperator_restrict_of_isCompact_closure {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U U' : TopologicalSpace.Opens V} [ProperSpace E] (hU' : IsCompact (closure ↑U')) (hU'U : closure ↑U' ⊆ ↑U) : IsCompactOperator ⇑(restrict ⋯)

If E is proper, restriction to an open set with compact closure inside U is a compact operator.

theorem TauCeti.BoundedHolomorphicFunctions.restrict_injective {V : Type u_1} {E : Type u_2} [NormedAddCommGroup V] [NormedSpace ℂ V] [NormedAddCommGroup E] [NormedSpace ℂ E] {U U' : TopologicalSpace.Opens V} [FiniteDimensional ℂ V] [CompleteSpace E] (h : U' ≤ U) (hU' : ∀ x ∈ U, (connectedComponentIn (↑U) x ∩ ↑U').Nonempty) : Function.Injective ⇑(restrict h)

Identity theorem. If V is finite-dimensional, E is complete, and every connected component of U meets U', then restriction H^∞(U, E) → H^∞(U', E) is injective.