Conjugation and holomorphic domains

This file records the elementary conjugation API used by the conformal-mapping roadmap's Schwarz-reflection layer. Mathlib already proves the pointwise fact DifferentiableAt.conj_conj: if f is complex differentiable at conj z, then z ↦ conj (f (conj z)) is complex differentiable at z. The lemmas here package the corresponding within-set statement for reflected images, which is the form needed before the real-axis Schwarz reflection principle.

It also names the standard real-axis Schwarz-reflection extension z ↦ if 0 ≤ z.im then f z else conj (f (conj z)), together with the pointwise API for the upper and lower half-planes and the conjugation symmetry forced by real boundary values. The closed upper branch is intentionally exposed through the pointwise simplifier schwarzReflection_of_im_nonneg, with subset-level wrappers for branch agreement and differentiability transfer. The continuity lemmas record the topological gluing input for the later Morera-based reflection theorem: the reflected branch is continuous on reflected sets, and the explicit Schwarz-reflection extension is continuous across the real axis when the boundary values are real.

The last section turns conjugation symmetry into a statement about limits at a real point: a holomorphic function on a punctured disc about a real point which commutes with conjugation has a two-sided limit there as soon as it has one along the upper half-plane. Symmetry transports the bound to the lower half-plane and continuity to the real axis, after which the singularity is removable. This is how a one-sided asymptotic at a boundary point of the upper half-plane becomes a residue of the continued function.

noncomputable def TauCeti.schwarzReflection (f : ℂ → ℂ) (z : ℂ) : ℂ

The explicit real-axis Schwarz-reflection extension of a function from the closed upper half-plane to the plane.

On 0 ≤ z.im this is f z; on the lower half-plane it is conj (f (conj z)).

Equations

• TauCeti.schwarzReflection f z = if 0 ≤ z.im then f z else (starRingEnd ℂ) (f ((starRingEnd ℂ) z))

theorem TauCeti.schwarzReflection_def (f : ℂ → ℂ) (z : ℂ) : schwarzReflection f z = if 0 ≤ z.im then f z else (starRingEnd ℂ) (f ((starRingEnd ℂ) z))

The Schwarz-reflection extension is the explicit upper/lower half-plane witness.

@[simp]

theorem TauCeti.schwarzReflection_of_im_nonneg {f : ℂ → ℂ} {z : ℂ} (hz : 0 ≤ z.im) : schwarzReflection f z = f z

On the closed upper half-plane, Schwarz reflection agrees with the original function.

@[simp]

theorem TauCeti.schwarzReflection_of_im_neg {f : ℂ → ℂ} {z : ℂ} (hz : z.im < 0) : schwarzReflection f z = (starRingEnd ℂ) (f ((starRingEnd ℂ) z))

On the lower half-plane, Schwarz reflection is z ↦ conj (f (conj z)).

theorem TauCeti.schwarzReflection_of_im_zero {f : ℂ → ℂ} {z : ℂ} (hz : z.im = 0) : schwarzReflection f z = f z

On the real axis, Schwarz reflection agrees with the original function.

theorem TauCeti.eqOn_schwarzReflection_of_subset_im_nonneg {f : ℂ → ℂ} {S : Set ℂ} (hS : S ⊆ {z : ℂ | 0 ≤ z.im}) : Set.EqOn (schwarzReflection f) f S

On any subset of the closed upper half-plane, Schwarz reflection agrees with the original function.

theorem TauCeti.eqOn_schwarzReflection_of_subset_im_neg {f : ℂ → ℂ} {S : Set ℂ} (hS : S ⊆ {z : ℂ | z.im < 0}) : Set.EqOn (schwarzReflection f) (fun (z : ℂ) => (starRingEnd ℂ) (f ((starRingEnd ℂ) z))) S

On any subset of the lower half-plane, Schwarz reflection agrees with the reflected branch.

theorem TauCeti.schwarzReflection_conj_of_im_pos {f : ℂ → ℂ} {z : ℂ} (hz : 0 < z.im) : schwarzReflection f ((starRingEnd ℂ) z) = (starRingEnd ℂ) (f z)

Conjugating a point in the upper half-plane evaluates the reflected lower branch.

theorem TauCeti.conj_schwarzReflection_of_im_neg {f : ℂ → ℂ} {z : ℂ} (hz : z.im < 0) : (starRingEnd ℂ) (schwarzReflection f z) = f ((starRingEnd ℂ) z)

Conjugating the lower-half-plane value recovers the original function at conj z.

theorem TauCeti.schwarzReflection_conj {f : ℂ → ℂ} (z : ℂ) (hreal : z.im = 0 → (f z).im = 0) : schwarzReflection f ((starRingEnd ℂ) z) = (starRingEnd ℂ) (schwarzReflection f z)

The Schwarz-reflection extension is conjugation-symmetric when the original function has real value at the real-axis point under consideration.

theorem TauCeti.schwarzReflection_conj_of_real_on_axis {f : ℂ → ℂ} {Ω : Set ℂ} (hreal : ∀ z ∈ Ω, z.im = 0 → (f z).im = 0) {z : ℂ} (hz : z ∈ Ω) : schwarzReflection f ((starRingEnd ℂ) z) = (starRingEnd ℂ) (schwarzReflection f z)

On a domain where the original function is real-valued on the real axis, the Schwarz-reflection extension is conjugation-symmetric at each point of the domain.

theorem TauCeti.eqOn_schwarzReflection_conj_of_real_on_axis {f : ℂ → ℂ} {Ω : Set ℂ} (hreal : ∀ z ∈ Ω, z.im = 0 → (f z).im = 0) : Set.EqOn (fun (z : ℂ) => schwarzReflection f ((starRingEnd ℂ) z)) (fun (z : ℂ) => (starRingEnd ℂ) (schwarzReflection f z)) Ω

On a domain where the original function is real-valued on the real axis, the Schwarz-reflection extension is conjugation-symmetric on that domain.

theorem TauCeti.image_conj_inter_im_pos_of_symmetric {Ω : Set ℂ} (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) : ⇑(starRingEnd ℂ) '' (Ω ∩ {z : ℂ | 0 < z.im}) = Ω ∩ {z : ℂ | z.im < 0}

For a domain closed under conjugation, conjugation carries the upper half-plane part of the domain to its lower half-plane part.

theorem TauCeti.image_conj_inter_im_neg_of_symmetric {Ω : Set ℂ} (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) : ⇑(starRingEnd ℂ) '' (Ω ∩ {z : ℂ | z.im < 0}) = Ω ∩ {z : ℂ | 0 < z.im}

For a domain closed under conjugation, conjugation carries the lower half-plane part of the domain to its upper half-plane part.

theorem TauCeti.continuousOn_conj_conj {f : ℂ → ℂ} {S : Set ℂ} (hf : ContinuousOn f S) : ContinuousOn (fun (z : ℂ) => (starRingEnd ℂ) (f ((starRingEnd ℂ) z))) (⇑(starRingEnd ℂ) '' S)

Conjugating both source and target preserves continuity on reflected sets.

@[simp]

theorem TauCeti.continuousOn_conj_conj_iff {f : ℂ → ℂ} {S : Set ℂ} : ContinuousOn (fun (z : ℂ) => (starRingEnd ℂ) (f ((starRingEnd ℂ) z))) (⇑(starRingEnd ℂ) '' S) ↔ ContinuousOn f S

Conjugating both source and target preserves continuity on reflected sets, in both directions.

theorem TauCeti.continuousOn_schwarzReflection_of_subset_im_nonneg {f : ℂ → ℂ} {S : Set ℂ} (hS : S ⊆ {z : ℂ | 0 ≤ z.im}) (hf : ContinuousOn f S) : ContinuousOn (schwarzReflection f) S

On any subset of the closed upper half-plane, the explicit Schwarz-reflection extension is continuous whenever the original function is.

theorem TauCeti.continuousOn_conj_conj_inter_im_neg_of_symmetric {f : ℂ → ℂ} {Ω : Set ℂ} (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hf : ContinuousOn f (Ω ∩ {z : ℂ | 0 < z.im})) : ContinuousOn (fun (z : ℂ) => (starRingEnd ℂ) (f ((starRingEnd ℂ) z))) (Ω ∩ {z : ℂ | z.im < 0})

If a domain is closed under conjugation and f is continuous on its upper half-plane part, then the reflected branch z ↦ conj (f (conj z)) is continuous on the lower half-plane part.

theorem TauCeti.continuousOn_schwarzReflection_inter_im_neg_of_symmetric {f : ℂ → ℂ} {Ω : Set ℂ} (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hf : ContinuousOn f (Ω ∩ {z : ℂ | 0 < z.im})) : ContinuousOn (schwarzReflection f) (Ω ∩ {z : ℂ | z.im < 0})

On the lower half-plane part of a domain closed under conjugation, the explicit Schwarz reflection extension is continuous whenever the original function is continuous on the upper half-plane part.

theorem TauCeti.image_conj_inter_im_nonneg_of_symmetric {Ω : Set ℂ} (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) : ⇑(starRingEnd ℂ) '' (Ω ∩ {z : ℂ | 0 ≤ z.im}) = Ω ∩ {z : ℂ | z.im ≤ 0}

For a domain closed under conjugation, conjugation carries the closed upper half-plane part of the domain to its closed lower half-plane part.

theorem TauCeti.continuousOn_schwarzReflection_of_symmetric {f : ℂ → ℂ} {Ω : Set ℂ} (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hf : ContinuousOn f (Ω ∩ {z : ℂ | 0 ≤ z.im})) (hreal : ∀ z ∈ Ω, z.im = 0 → (f z).im = 0) : ContinuousOn (schwarzReflection f) Ω

If a domain Ω is closed under conjugation, f is continuous on its closed upper half-plane part, and f takes real values at the real-axis points of Ω, then the explicit Schwarz-reflection extension is continuous on Ω.

theorem TauCeti.continuous_schwarzReflection {f : ℂ → ℂ} (hf : ContinuousOn f {z : ℂ | 0 ≤ z.im}) (hreal : ∀ (z : ℂ), z.im = 0 → (f z).im = 0) : Continuous (schwarzReflection f)

If f is continuous on the closed upper half-plane and takes real values on the real axis, then its explicit Schwarz-reflection extension is continuous on the plane.

theorem TauCeti.differentiableOn_conj_conj {f : ℂ → ℂ} {S : Set ℂ} (hf : DifferentiableOn ℂ f S) : DifferentiableOn ℂ (fun (z : ℂ) => (starRingEnd ℂ) (f ((starRingEnd ℂ) z))) (⇑(starRingEnd ℂ) '' S)

Antiholomorphic-composition prerequisite for Schwarz reflection.

If f is holomorphic on S, then z ↦ conj (f (conj z)) is holomorphic on the reflected set conj '' S.

theorem TauCeti.differentiableOn_schwarzReflection_of_subset_im_nonneg {f : ℂ → ℂ} {S : Set ℂ} (hS : S ⊆ {z : ℂ | 0 ≤ z.im}) (hf : DifferentiableOn ℂ f S) : DifferentiableOn ℂ (schwarzReflection f) S

On any subset of the closed upper half-plane, the explicit Schwarz-reflection extension is holomorphic whenever the original function is.

@[simp]

theorem TauCeti.differentiableOn_conj_conj_iff {f : ℂ → ℂ} {S : Set ℂ} : DifferentiableOn ℂ (fun (z : ℂ) => (starRingEnd ℂ) (f ((starRingEnd ℂ) z))) (⇑(starRingEnd ℂ) '' S) ↔ DifferentiableOn ℂ f S

Conjugating both source and target preserves holomorphicity on domains, in both directions.

theorem TauCeti.differentiableOn_conj_conj_inter_im_neg_of_symmetric {f : ℂ → ℂ} {Ω : Set ℂ} (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hf : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) : DifferentiableOn ℂ (fun (z : ℂ) => (starRingEnd ℂ) (f ((starRingEnd ℂ) z))) (Ω ∩ {z : ℂ | z.im < 0})

If a domain is closed under conjugation and f is holomorphic on its upper half-plane part, then the reflected branch z ↦ conj (f (conj z)) is holomorphic on the lower half-plane part.

theorem TauCeti.differentiableOn_schwarzReflection_inter_im_neg_of_symmetric {f : ℂ → ℂ} {Ω : Set ℂ} (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hf : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) : DifferentiableOn ℂ (schwarzReflection f) (Ω ∩ {z : ℂ | z.im < 0})

On the lower half-plane part of a domain closed under conjugation, the explicit Schwarz reflection extension is holomorphic whenever the original function is holomorphic on the upper half-plane part.

theorem TauCeti.differentiableOn_schwarzReflection_inter_im_ne_zero_of_symmetric {f : ℂ → ℂ} {Ω : Set ℂ} (hΩ : Set.MapsTo (⇑(starRingEnd ℂ)) Ω Ω) (hf : DifferentiableOn ℂ f (Ω ∩ {z : ℂ | 0 < z.im})) : DifferentiableOn ℂ (schwarzReflection f) (Ω ∩ {z : ℂ | z.im ≠ 0})

Away from the real axis, the Schwarz-reflection extension is holomorphic on a conjugation-symmetric domain whenever the original function is holomorphic on its upper half-plane part.

theorem TauCeti.hasDerivAt_schwarzReflection_of_im_pos {f : ℂ → ℂ} {z f' : ℂ} (hz : 0 < z.im) (hf : HasDerivAt f f' z) : HasDerivAt (schwarzReflection f) f' z

At a point in the open upper half-plane, the Schwarz-reflection extension has the same derivative as the original function.

theorem TauCeti.hasDerivAt_schwarzReflection_of_im_neg {f : ℂ → ℂ} {z f' : ℂ} (hz : z.im < 0) (hf : HasDerivAt f f' ((starRingEnd ℂ) z)) : HasDerivAt (schwarzReflection f) ((starRingEnd ℂ) f') z

At a point in the open lower half-plane, the derivative of the Schwarz-reflection extension is the conjugate of the derivative of f at the conjugate point.

@[simp]

theorem TauCeti.deriv_schwarzReflection_of_im_pos {f : ℂ → ℂ} {z : ℂ} (hz : 0 < z.im) : deriv (schwarzReflection f) z = deriv f z

On the open upper half-plane, the derivative of the Schwarz-reflection extension agrees with the derivative of the original function.

@[simp]

theorem TauCeti.deriv_schwarzReflection_of_im_neg {f : ℂ → ℂ} {z : ℂ} (hz : z.im < 0) : deriv (schwarzReflection f) z = (starRingEnd ℂ) (deriv f ((starRingEnd ℂ) z))

On the open lower half-plane, the derivative of the Schwarz-reflection extension is the conjugate of the derivative of the original function at the conjugate point.

theorem TauCeti.tendsto_nhdsNE_of_tendsto_nhdsWithin_im_pos {g : ℂ → ℂ} {x : ℝ} {c : ℂ} {r : ℝ} (hr : 0 < r) (hg : DifferentiableOn ℂ g (Metric.ball (↑x) r \ {↑x})) (hconj : ∀ z ∈ Metric.ball (↑x) r \ {↑x}, g ((starRingEnd ℂ) z) = (starRingEnd ℂ) (g z)) (hlim : Filter.Tendsto g (nhdsWithin ↑x {z : ℂ | 0 < z.im}) (nhds c)) : Filter.Tendsto g (nhdsWithin ↑x {↑x}ᶜ) (nhds c)

A conjugation-symmetric holomorphic function has a two-sided limit at a real point as soon as it has one from above. If g is holomorphic on a punctured disc about a real point x, commutes with conjugation, and tends to c along the open upper half-plane, then it tends to c along the whole punctured neighbourhood of x. In particular c is then real.