One-dimensional hyperfunctions as boundary values of holomorphic functions

In one variable, Sato's hyperfunctions on an open set U ⊆ ℝ can be written as differences of boundary values of holomorphic functions. Put W(U) = ℂ ∖ (ℝ ∖ U), the largest open subset of ℂ whose intersection with ℝ is U. A hyperfunction on U is represented by a holomorphic function f on ℂ ∖ ℝ, that is, by a pair of holomorphic functions on the upper and the lower half-plane, and two representatives give the same hyperfunction when their difference extends holomorphically across U, i.e. to all of W(U). The space of hyperfunctions on U is the quotient O(ℂ ∖ ℝ) / O(W(U)). Restriction to a smaller open V ⊆ U keeps the representative: a function extending across U also extends across V.

Encoding

Holomorphic functions on an open U ⊆ ℂ are encoded as genuine functions ℂ → ℂ that are complex differentiable on U and vanish outside U (TauCeti.Hyperfunction.holomorphicSections). The extension by zero is only a device for using one ambient module of functions; no continuity across the boundary of U is imposed or used. Restriction to a smaller open multiplies by the indicator function (TauCeti.Hyperfunction.holomorphicRestrict).

Main declarations

• TauCeti.Hyperfunction.nonRealOpen: the open set ℂ ∖ ℝ, which is dense (TauCeti.Hyperfunction.dense_nonRealOpen);
• TauCeti.Hyperfunction.complexNeighborhood U: the open set W(U) = ℂ ∖ (ℝ ∖ U);
• TauCeti.Hyperfunction.throughReal U: the holomorphic functions on ℂ ∖ ℝ that extend holomorphically to W(U);
• TauCeti.Hyperfunction.OneDimBoundaryQuotient U: the quotient O(ℂ ∖ ℝ) / O(W(U)), and TauCeti.Hyperfunction.oneDimBoundaryPresheaf the presheaf of complex vector spaces U ↦ O(ℂ ∖ ℝ) / O(W(U)) on ℝ. All its restriction maps are surjective (TauCeti.Hyperfunction.oneDimBoundaryRestrict_surjective).

Main results

• TauCeti.Hyperfunction.throughReal_iSup: a holomorphic function on ℂ ∖ ℝ extends across ⋃ i, U i exactly when it extends across every U i. The local extensions agree on the real points of the overlaps, because they are continuous there and agree on the dense set ℂ ∖ ℝ, so they glue.
• TauCeti.Hyperfunction.oneDimBoundaryPresheaf_isSeparated: consequently the presheaf U ↦ O(ℂ ∖ ℝ) / O(W(U)) is separated: a section that vanishes locally vanishes. This is the uniqueness half of the sheaf property. The existence half needs the vanishing of the first cohomology of the sheaf of holomorphic functions on open subsets of ℂ (a Cousin problem) and is not proved here.

References

• M. Sato, Theory of hyperfunctions I, J. Fac. Sci. Univ. Tokyo Sect. I 8 (1959), 139–193.
• H. Komatsu, An introduction to the theory of hyperfunctions, in Hyperfunctions and pseudo-differential equations, Lecture Notes in Mathematics 287 (1973), 3–40.
• L. Hörmander, The analysis of linear partial differential operators I, §9.1.

Holomorphic sections

def TauCeti.Hyperfunction.holomorphicSections (U : TopologicalSpace.Opens ℂ) : Submodule ℂ (ℂ → ℂ)

The holomorphic functions on an open set U ⊆ ℂ, encoded as the functions ℂ → ℂ that are complex differentiable on U and vanish outside U.

theorem TauCeti.Hyperfunction.mem_holomorphicSections_iff {U : TopologicalSpace.Opens ℂ} {f : ℂ → ℂ} : f ∈ holomorphicSections U ↔ DifferentiableOn ℂ f ↑U ∧ ∀ z ∉ U, f z = 0

theorem TauCeti.Hyperfunction.indicator_mem_holomorphicSections {U V : TopologicalSpace.Opens ℂ} (h : U ≤ V) {f : ℂ → ℂ} (hf : f ∈ holomorphicSections V) : (↑U).indicator f ∈ holomorphicSections U

The indicator function of a smaller open set restricts holomorphic sections.

noncomputable def TauCeti.Hyperfunction.holomorphicRestrict {U V : TopologicalSpace.Opens ℂ} (h : U ≤ V) : ↥(holomorphicSections V) →ₗ[ℂ] ↥(holomorphicSections U)

Restriction of holomorphic sections to a smaller open set.

@[simp]

theorem TauCeti.Hyperfunction.coe_holomorphicRestrict {U V : TopologicalSpace.Opens ℂ} (h : U ≤ V) (f : ↥(holomorphicSections V)) : ↑((holomorphicRestrict h) f) = (↑U).indicator ↑f

@[simp]

theorem TauCeti.Hyperfunction.holomorphicRestrict_self (U : TopologicalSpace.Opens ℂ) (f : ↥(holomorphicSections U)) : (holomorphicRestrict ⋯) f = f

@[simp]

theorem TauCeti.Hyperfunction.holomorphicRestrict_holomorphicRestrict {U V W : TopologicalSpace.Opens ℂ} (h₁ : U ≤ V) (h₂ : V ≤ W) (f : ↥(holomorphicSections W)) : (holomorphicRestrict h₁) ((holomorphicRestrict h₂) f) = (holomorphicRestrict ⋯) f

The open sets ℂ ∖ ℝ and W(U)

def TauCeti.Hyperfunction.nonRealOpen : TopologicalSpace.Opens ℂ

The open set ℂ ∖ ℝ, the union of the upper and the lower half-plane.

@[simp]

theorem TauCeti.Hyperfunction.mem_nonRealOpen_iff {z : ℂ} : z ∈ nonRealOpen ↔ z.im ≠ 0

theorem TauCeti.Hyperfunction.dense_nonRealOpen : Dense ↑nonRealOpen

The non-real complex numbers are dense in ℂ.

noncomputable def TauCeti.Hyperfunction.complexNeighborhood (U : TopologicalSpace.Opens ℝ) : TopologicalSpace.Opens ℂ

The open set W(U) = ℂ ∖ (ℝ ∖ U) attached to an open set U ⊆ ℝ: the non-real complex numbers together with the points of U.

@[simp]

theorem TauCeti.Hyperfunction.mem_complexNeighborhood_iff {U : TopologicalSpace.Opens ℝ} {z : ℂ} : z ∈ complexNeighborhood U ↔ z.im ≠ 0 ∨ z.re ∈ U

theorem TauCeti.Hyperfunction.nonRealOpen_le_complexNeighborhood (U : TopologicalSpace.Opens ℝ) : nonRealOpen ≤ complexNeighborhood U

The set W(U) contains ℂ ∖ ℝ.

theorem TauCeti.Hyperfunction.complexNeighborhood_mono : Monotone complexNeighborhood

The set W(U) grows with U.

Functions extending across a real open set

noncomputable def TauCeti.Hyperfunction.throughReal (U : TopologicalSpace.Opens ℝ) : Submodule ℂ ↥(holomorphicSections nonRealOpen)

The holomorphic functions on ℂ ∖ ℝ that extend holomorphically across the open set U ⊆ ℝ, that is, that are restrictions of holomorphic functions on W(U).

theorem TauCeti.Hyperfunction.mem_throughReal_iff {U : TopologicalSpace.Opens ℝ} {f : ↥(holomorphicSections nonRealOpen)} : f ∈ throughReal U ↔ ∃ g ∈ holomorphicSections (complexNeighborhood U), Set.EqOn g ↑f ↑nonRealOpen

A holomorphic function on ℂ ∖ ℝ extends across U exactly when it agrees on ℂ ∖ ℝ with a holomorphic function on W(U).

theorem TauCeti.Hyperfunction.throughReal_antitone : Antitone throughReal

A function extending across V extends across every smaller U.

theorem TauCeti.Hyperfunction.throughReal_iSup {ι : Sort u_1} (U : ι → TopologicalSpace.Opens ℝ) : throughReal (⨆ (i : ι), U i) = ⨅ (i : ι), throughReal (U i)

Extension across a union. A holomorphic function on ℂ ∖ ℝ extends holomorphically across ⋃ i, U i exactly when it extends holomorphically across every U i.

theorem TauCeti.Hyperfunction.mem_throughReal_of_le_iSup {ι : Sort u_1} {U : ι → TopologicalSpace.Opens ℝ} {V : TopologicalSpace.Opens ℝ} (hV : V ≤ ⨆ (i : ι), U i) {f : ↥(holomorphicSections nonRealOpen)} (hf : ∀ (i : ι), f ∈ throughReal (U i)) : f ∈ throughReal V

A holomorphic function on ℂ ∖ ℝ that extends across every member of a cover of V extends across V.

The presheaf U ↦ O(ℂ ∖ ℝ) / O(W(U))

@[reducible, inline]

abbrev TauCeti.Hyperfunction.OneDimBoundaryQuotient (U : TopologicalSpace.Opens ℝ) : Type

The space O(ℂ ∖ ℝ) / O(W(U)) of one-dimensional hyperfunctions on an open set U ⊆ ℝ, represented by holomorphic functions on ℂ ∖ ℝ modulo those extending holomorphically across U.

noncomputable def TauCeti.Hyperfunction.oneDimBoundaryRestrict {U V : TopologicalSpace.Opens ℝ} (h : U ≤ V) : OneDimBoundaryQuotient V →ₗ[ℂ] OneDimBoundaryQuotient U

Restriction of one-dimensional hyperfunctions to a smaller open set, keeping the holomorphic representative on ℂ ∖ ℝ.

@[simp]

theorem TauCeti.Hyperfunction.oneDimBoundaryRestrict_mk {U V : TopologicalSpace.Opens ℝ} (h : U ≤ V) (f : ↥(holomorphicSections nonRealOpen)) : (oneDimBoundaryRestrict h) (Submodule.Quotient.mk f) = Submodule.Quotient.mk f

@[simp]

theorem TauCeti.Hyperfunction.oneDimBoundaryRestrict_self (U : TopologicalSpace.Opens ℝ) (q : OneDimBoundaryQuotient U) : (oneDimBoundaryRestrict ⋯) q = q

@[simp]

theorem TauCeti.Hyperfunction.oneDimBoundaryRestrict_oneDimBoundaryRestrict {U V W : TopologicalSpace.Opens ℝ} (h₁ : U ≤ V) (h₂ : V ≤ W) (q : OneDimBoundaryQuotient W) : (oneDimBoundaryRestrict h₁) ((oneDimBoundaryRestrict h₂) q) = (oneDimBoundaryRestrict ⋯) q

theorem TauCeti.Hyperfunction.oneDimBoundaryRestrict_surjective {U V : TopologicalSpace.Opens ℝ} (h : U ≤ V) : Function.Surjective ⇑(oneDimBoundaryRestrict h)

Every one-dimensional hyperfunction on a smaller open set is the restriction of one on a larger open set.

theorem TauCeti.Hyperfunction.eq_zero_of_oneDimBoundaryRestrict_eq_zero {ι : Sort u_1} {U : ι → TopologicalSpace.Opens ℝ} {V : TopologicalSpace.Opens ℝ} (hUV : ∀ (i : ι), U i ≤ V) (hV : V ≤ ⨆ (i : ι), U i) {q : OneDimBoundaryQuotient V} (hq : ∀ (i : ι), (oneDimBoundaryRestrict ⋯) q = 0) : q = 0

Locality. A one-dimensional hyperfunction on V whose restrictions to the members of a cover of V all vanish is zero.

theorem TauCeti.Hyperfunction.eq_of_oneDimBoundaryRestrict_eq {ι : Sort u_1} {U : ι → TopologicalSpace.Opens ℝ} {V : TopologicalSpace.Opens ℝ} (hUV : ∀ (i : ι), U i ≤ V) (hV : V ≤ ⨆ (i : ι), U i) {q₁ q₂ : OneDimBoundaryQuotient V} (hq : ∀ (i : ι), (oneDimBoundaryRestrict ⋯) q₁ = (oneDimBoundaryRestrict ⋯) q₂) : q₁ = q₂

Locality. Two one-dimensional hyperfunctions on V with the same restrictions to the members of a cover of V are equal.

noncomputable def TauCeti.Hyperfunction.oneDimBoundaryPresheaf : TopCat.Presheaf (ModuleCat ℂ) ↧ℝ

The presheaf of complex vector spaces U ↦ O(ℂ ∖ ℝ) / O(W(U)) on ℝ, whose sections are the one-dimensional hyperfunctions.

@[simp]

theorem TauCeti.Hyperfunction.oneDimBoundaryPresheaf_map_apply {U V : (TopologicalSpace.Opens ↑↧ℝ)ᵒᵖ} (f : U ⟶ V) (q : OneDimBoundaryQuotient (Opposite.unop U)) : (CategoryTheory.ConcreteCategory.hom (oneDimBoundaryPresheaf.map f)) q = (oneDimBoundaryRestrict ⋯) q

theorem TauCeti.Hyperfunction.oneDimBoundaryPresheaf_isSeparated : CategoryTheory.Presheaf.IsSeparated (Opens.grothendieckTopology ↑↧ℝ) oneDimBoundaryPresheaf

The presheaf of one-dimensional hyperfunctions is separated: a section that vanishes on the members of an open cover vanishes.