BddHoloOn: bounded-holomorphic Banach spaces, and the germ bridges (finiteness-and-chi)

Unit: finiteness-and-chi (docs/design/finiteness-and-chi.md D1, D5, §4.1).

The norm-layer carrier: BddHoloOn S, bounded-continuous functions on the open subtype ↥S that agree on S with some ContMDiffOn ω (holomorphic) function. Sup-norm, chart-free (deviation (D-a) from Forster's L² norms — see the design doc §0). This file provides:

• BddHoloOn S : Submodule ℂ (↥S →ᵇ ℂ), isClosed_bddHoloOn (uniform limits of holomorphic functions are holomorphic, proved chart-locally via Surface.Bridges + TendstoLocallyUniformlyOn.differentiableOn), hence CompleteSpace (BddHoloOn S).
• restrictCLM: restriction between nested BddHoloOns, norm ≤ 1.
• toGerm/evalAt_toGerm/toGerm_restrict_comm: germification into LinSysOn 0 (D5).
• restrictGerm/toGerm_restrictGerm/restrictGerm_toGerm: de-germification onto a compactly-contained smaller open via holoRepr ([T2Space X] [CompactSpace X]).

D5 (Čech/Banach interface localized here): all germ-vs-function traffic goes through these three named maps; the Banach files (Chain.lean, CompactRestrict.lean) never touch MeroGermOn internals directly, and the germ files never touch →ᵇ internals.

BddHoloOn

theorem RS.Finiteness.contMDiffOn_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {U : Set X} (hU : IsOpen U) {g₁ g₂ : X → ℂ} (h1 : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g₁ U) (h2 : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g₂ U) : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (g₁ + g₂) U

Compat: sum of ContMDiffOn ω functions X → ℂ on an open set (chart-local via the Surface bridge + AnalyticAt.add).

theorem RS.Finiteness.contMDiffOn_const_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {U : Set X} (hU : IsOpen U) (c : ℂ) {g : X → ℂ} (hg : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g U) : ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ (c • g) U

Compat: scalar multiple of a ContMDiffOn ω function X → ℂ on an open set.

noncomputable def RS.Finiteness.BddHoloOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (S : TopologicalSpace.Opens X) : Submodule ℂ (BoundedContinuousFunction ↑↑S ℂ)

Bounded-holomorphic elements: BCF on the open subtype agreeing with a holomorphic function on S.

Equations

• One or more equations did not get rendered due to their size.

theorem RS.Finiteness.mem_bddHoloOn_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S : TopologicalSpace.Opens X} {f : BoundedContinuousFunction ↑↑S ℂ} : f ∈ BddHoloOn S ↔ ∃ (g : X → ℂ), ContMDiffOn (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ g ↑S ∧ ∀ (z : ↑↑S), f z = g ↑z

theorem RS.Finiteness.isClosed_bddHoloOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (S : TopologicalSpace.Opens X) : IsClosed ↑(BddHoloOn S)

Uniform limits of holomorphic functions are holomorphic (chart-local, via Surface.Bridges

• TendstoLocallyUniformlyOn.differentiableOn): BddHoloOn S is closed.

instance RS.Finiteness.instCompleteSpaceBddHoloOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (S : TopologicalSpace.Opens X) : CompleteSpace ↥(BddHoloOn S)

restrictCLM

noncomputable def RS.Finiteness.restrictFun {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S' S : TopologicalSpace.Opens X} (h : S' ≤ S) (f : ↥(BddHoloOn S)) : BoundedContinuousFunction ↑↑S' ℂ

The underlying restricted bounded continuous function.

Equations

• RS.Finiteness.restrictFun h f = BoundedContinuousFunction.ofNormedAddCommGroup (fun (z : ↑↑S') => ↑f (Set.inclusion h z)) ⋯ ‖↑f‖ ⋯

theorem RS.Finiteness.restrictFun_mem {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S' S : TopologicalSpace.Opens X} (h : S' ≤ S) (f : ↥(BddHoloOn S)) : restrictFun h f ∈ BddHoloOn S'

theorem RS.Finiteness.restrictFun_add {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S' S : TopologicalSpace.Opens X} (h : S' ≤ S) (f₁ f₂ : ↥(BddHoloOn S)) : restrictFun h (f₁ + f₂) = restrictFun h f₁ + restrictFun h f₂

theorem RS.Finiteness.restrictFun_smul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S' S : TopologicalSpace.Opens X} (h : S' ≤ S) (c : ℂ) (f : ↥(BddHoloOn S)) : restrictFun h (c • f) = c • restrictFun h f

noncomputable def RS.Finiteness.restrictCLM {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S' S : TopologicalSpace.Opens X} (h : S' ≤ S) : ↥(BddHoloOn S) →L[ℂ] ↥(BddHoloOn S')

Restriction, norm ≤ 1.

Equations

• RS.Finiteness.restrictCLM h = { toFun := fun (f : ↥(RS.Finiteness.BddHoloOn S)) => ⟨RS.Finiteness.restrictFun h f, ⋯⟩, map_add' := ⋯, map_smul' := ⋯ }.mkContinuous 1 ⋯

theorem RS.Finiteness.restrictCLM_apply_coe {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S' S : TopologicalSpace.Opens X} (h : S' ≤ S) (f : ↥(BddHoloOn S)) (z : ↑↑S') : ↑((restrictCLM h) f) z = ↑f (Set.inclusion h z)

theorem RS.Finiteness.restrictCLM_restrictCLM {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S'' S' S : TopologicalSpace.Opens X} (h1 : S' ≤ S) (h2 : S'' ≤ S') (h3 : S'' ≤ S) (f : ↥(BddHoloOn S)) : (restrictCLM h2) ((restrictCLM h1) f) = (restrictCLM h3) f

Presheaf law: restrictions compose (the analogue of MeroGermOn.restrict_restrict / LinSysOn.restrictL_restrictL, needed for the cochain-level naturality of resNC1).

theorem RS.Finiteness.norm_restrictCLM_apply_le {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S' S : TopologicalSpace.Opens X} (h : S' ≤ S) (f : ↥(BddHoloOn S)) : ‖(restrictCLM h) f‖ ≤ ‖f‖

toGerm: germification (D5)

theorem RS.Finiteness.mk_eq_mk_of_eqOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {U : Set X} (hU : IsOpen U) {f g : X → ℂ} (hf : MeromorphicOnX f U) (hg : MeromorphicOnX g U) (h : Set.EqOn f g U) : MeroGermOn.mk f hf = MeroGermOn.mk g hg

If two meromorphic functions agree pointwise on an open set U, their germ classes on U agree (Compat: the everywhere-on-U case of mk_eq_mk, used throughout this file's well-definedness proofs since Exists.choose is otherwise opaque).

noncomputable def RS.Finiteness.toGerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (S : TopologicalSpace.Opens X) : ↥(BddHoloOn S) →ₗ[ℂ] MeroGermOn X ↑S

Germification (lands in LinSysOn 0).

Equations

• RS.Finiteness.toGerm S = { toFun := fun (f : ↥(RS.Finiteness.BddHoloOn S)) => RS.MeroGermOn.mk (Exists.choose ⋯) ⋯, map_add' := ⋯, map_smul' := ⋯ }

theorem RS.Finiteness.toGerm_eq_mk {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S : TopologicalSpace.Opens X} (f : ↥(BddHoloOn S)) : (toGerm S) f = MeroGermOn.mk (Exists.choose ⋯) ⋯

Unfolding lemma for toGerm (forces the mk-shape syntactically, since neither metavariable unification nor rw reliably unfolds the LinearMap/FunLike layers of the named toGerm application on their own).

theorem RS.Finiteness.toGerm_mem_linSysOn {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S : TopologicalSpace.Opens X} (f : ↥(BddHoloOn S)) : (toGerm S) f ∈ LinSysOn 0 ↑S

theorem RS.Finiteness.evalAt_toGerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S : TopologicalSpace.Opens X} (f : ↥(BddHoloOn S)) {x : X} (hx : x ∈ S) : ((toGerm S) f).evalAt x = ↑f ⟨x, hx⟩

theorem RS.Finiteness.toGerm_restrict_comm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {S' S : TopologicalSpace.Opens X} (h : S' ≤ S) (f : ↥(BddHoloOn S)) : (toGerm S') ((restrictCLM h) f) = (MeroGermOn.restrict h) ((toGerm S) f)

restrictGerm: de-germification (D5)

theorem RS.Finiteness.le_of_closure {X : Type u_1} [TopologicalSpace X] {S' S : TopologicalSpace.Opens X} (hc : closure ↑S' ⊆ ↑S) : S' ≤ S

A closure-nested open pair S' ⋐ S gives S' ≤ S.

noncomputable def RS.Finiteness.restrictGerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] {S' S : TopologicalSpace.Opens X} (hc : closure ↑S' ⊆ ↑S) (φ : ↥(LinSysOn 0 ↑S)) : ↥(BddHoloOn S')

De-germification onto a compactly-contained smaller open (uses holoRepr).

Equations

• RS.Finiteness.restrictGerm hc φ = ⟨BoundedContinuousFunction.ofNormedAddCommGroup (fun (z : ↑↑S') => (↑φ).holoRepr ↑z) ⋯ ⋯.choose ⋯, ⋯⟩

theorem RS.Finiteness.restrictGerm_apply {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] {S' S : TopologicalSpace.Opens X} (hc : closure ↑S' ⊆ ↑S) (φ : ↥(LinSysOn 0 ↑S)) (z : ↑↑S') : ↑(restrictGerm hc φ) z = (↑φ).holoRepr ↑z

theorem RS.Finiteness.toGerm_restrictGerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] {S' S : TopologicalSpace.Opens X} (hc : closure ↑S' ⊆ ↑S) (φ : ↥(LinSysOn 0 ↑S)) : (toGerm S') (restrictGerm hc φ) = (MeroGermOn.restrict ⋯) ↑φ

theorem RS.Finiteness.restrictGerm_toGerm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [CompactSpace X] {S' S : TopologicalSpace.Opens X} (hc : closure ↑S' ⊆ ↑S) (f : ↥(BddHoloOn S)) : restrictGerm hc ⟨(toGerm S) f, ⋯⟩ = (restrictCLM ⋯) f