Schwarz reflection with a totally real linear boundary condition

A holomorphic map into a finite-dimensional complex normed space, continuous up to the real axis and taking its boundary values in an affine maximal totally real subspace, extends holomorphically across the axis. In particular it is smooth up to the boundary, without any boundary differentiability assumption. This is the constant-coefficient local model for Cauchy--Riemann boundary regularity.

The extension domain can be any conjugation-invariant open subset of ℂ; smoothness up to the boundary holds on any open domain. The target boundary condition is f z - q ∈ L, where L is complementary to i L; neither a symplectic form nor a choice of inner product is needed. A real basis of L gives complex coordinates on the target via TauCeti.IsMaximalTotallyReal.complexBasis. Coordinatewise application of TauCeti.differentiableOn_schwarzReflection_of_symmetric gives the extension.

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Appendix B (reflection for totally real boundary conditions).

theorem TauCeti.IsMaximalTotallyReal.exists_analyticOnNhd_eqOn_of_boundary_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E] [IsScalarTower ℝ ℂ E] [FiniteDimensional ℂ E] {L : Submodule ℝ E} {Ω : Set ℂ} {f : ℂ → E} {q : E} (hL : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) (hΩopen : IsOpen Ω) (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hboundary : ∀ z ∈ Ω, z.im = 0 → f z - q ∈ L) : ∃ (F : ℂ → E), AnalyticOnNhd ℂ F Ω ∧ Set.EqOn F f (Ω ∩ {z : ℂ | 0 ≤ z.im})

Schwarz reflection for an affine maximal totally real subspace. A map holomorphic on the open upper part of a conjugation-invariant open domain, continuous on its closed upper part, and with boundary values in q + L, has an analytic extension to the whole domain.

theorem TauCeti.IsMaximalTotallyReal.contDiffOn_of_boundary_mem {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℝ E] [NormedSpace ℂ E] [IsScalarTower ℝ ℂ E] [FiniteDimensional ℂ E] {L : Submodule ℝ E} {Ω : Set ℂ} {f : ℂ → E} {q : E} (hL : IsMaximalTotallyReal (↑ℝ ((LinearMap.lsmul ℂ E) Complex.I)) L) (hΩopen : IsOpen Ω) (hcont : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hholo : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) (hboundary : ∀ z ∈ Ω, z.im = 0 → f z - q ∈ L) : ContDiffOn ℝ (↑⊤) f (Ω ∩ {z : ℂ | 0 ≤ z.im})

A holomorphic map with a constant affine maximal totally real boundary condition is C^∞ on the closed upper part of its domain, including the real axis.