Even reflection across the real axis

The even reflection TauCeti.evenReflection w of a function w : ℂ → F agrees with w on the closed upper half-plane 0 ≤ im z and with w ∘ conj on the lower one. It is the standard way to turn a boundary problem on a half-disc centred on the real axis into an interior problem on the whole disc.

The even reflection of a C² function is in general only Lipschitz across the real axis. It is C² exactly when the odd-order normal derivatives match, and for a function that is C² up to the axis this is the Neumann condition ∂ₜ w = 0 on the axis: the first normal derivative changes sign under reflection, the second does not, and the mixed derivative ∂ₛ ∂ₜ w vanishes on the axis because ∂ₜ w does. So if w is C² on {0 ≤ im z} ∩ U, for an open set U invariant under conjugation, and ∂ₜ w = 0 on U ∩ ℝ, then evenReflection w is C² on U (TauCeti.contDiffOn_evenReflection). Its Laplacian is that of w above the axis and that of w at the mirror point below it, because conjugation is an isometry.

This is the reflection step in the boundary regularity theory of J-holomorphic curves with totally real boundary conditions. For a suitable metric the energy density of such a curve satisfies the Neumann condition on the boundary, and its even reflection reduces the boundary mean-value inequality to the interior one (TauCeti.Analysis.InnerProductSpace.Laplacian.BoundaryMeanValueInequality).

Main definitions

• TauCeti.evenReflection w: the function z ↦ w (re z + i |im z|).

Main results

• TauCeti.evenReflection_of_nonneg, TauCeti.evenReflection_of_nonpos: the reflection is w on the closed upper half-plane and w ∘ conj on the closed lower half-plane.
• TauCeti.continuousOn_evenReflection: the reflection of a function continuous up to the axis is continuous.
• TauCeti.isSymmSndFDerivWithinAt_setOfPred_le_im_inter: the second derivative within {0 ≤ im z} ∩ U of a function that is C² there is symmetric, also on the real axis.
• TauCeti.contDiffOn_evenReflection: the reflection of a function that is C² up to the axis and satisfies the Neumann condition there is C².
• TauCeti.laplacian_evenReflection_of_pos, TauCeti.laplacian_evenReflection_of_neg: the Laplacian of the reflection off the axis.

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, 2nd ed., AMS Colloquium Publications 52, 2012, Section 4.3 (the boundary version of the mean-value inequality, proved by reflecting the energy density).

def TauCeti.evenReflection {F : Type u_1} (w : ℂ → F) (z : ℂ) : F

The even reflection of w : ℂ → F across the real axis: w on the closed upper half-plane and w ∘ conj on the lower half-plane, written as the single formula w (re z + i |im z|).

@[simp]

theorem TauCeti.evenReflection_of_nonneg {F : Type u_1} {w : ℂ → F} {z : ℂ} (hz : 0 ≤ z.im) : evenReflection w z = w z

On the closed upper half-plane the even reflection of w is w.

@[simp]

theorem TauCeti.evenReflection_of_nonpos {F : Type u_1} {w : ℂ → F} {z : ℂ} (hz : z.im ≤ 0) : evenReflection w z = w ((starRingEnd ℂ) z)

On the closed lower half-plane the even reflection of w is w ∘ conj.

@[simp]

theorem TauCeti.evenReflection_conj {F : Type u_1} {w : ℂ → F} {z : ℂ} : evenReflection w ((starRingEnd ℂ) z) = evenReflection w z

The even reflection is invariant under conjugation.

theorem TauCeti.continuousOn_evenReflection {F : Type u_1} {w : ℂ → F} [TopologicalSpace F] {s : Set ℂ} (hs : ∀ z ∈ s, (starRingEnd ℂ) z ∈ s) (hw : ContinuousOn w ({z : ℂ | 0 ≤ z.im} ∩ s)) : ContinuousOn (evenReflection w) s

The even reflection of a function continuous up to the real axis is continuous, on any set invariant under conjugation.

The closed upper half-plane near an open set

theorem TauCeti.eventually_add_smul_one_mem_setOfPred_le_im_inter {U : Set ℂ} (hU : IsOpen U) {x : ℂ} (hx : x ∈ {z : ℂ | 0 ≤ z.im} ∩ U) : ∀ᶠ (t : ℝ) in nhds 0, x + t • 1 ∈ {z : ℂ | 0 ≤ z.im} ∩ U

Horizontal lines stay in {0 ≤ im z} ∩ U near any of its points, for U open.

theorem TauCeti.subset_closure_interior_setOfPred_le_im_inter {U : Set ℂ} (hU : IsOpen U) : {z : ℂ | 0 ≤ z.im} ∩ U ⊆ closure (interior ({z : ℂ | 0 ≤ z.im} ∩ U))

For U open, every point of {0 ≤ im z} ∩ U, including the points on the real axis, lies in the closure of its interior.

C² regularity of the even reflection

theorem TauCeti.isSymmSndFDerivWithinAt_setOfPred_le_im_inter {F : Type u_1} {w : ℂ → F} [NormedAddCommGroup F] [NormedSpace ℝ F] {U : Set ℂ} (hU : IsOpen U) (hw : ContDiffOn ℝ 2 w ({z : ℂ | 0 ≤ z.im} ∩ U)) {x : ℂ} (hx : x ∈ {z : ℂ | 0 ≤ z.im} ∩ U) : IsSymmSndFDerivWithinAt ℝ w ({z : ℂ | 0 ≤ z.im} ∩ U) x

The second derivative within {0 ≤ im z} ∩ U of a function that is C² there is symmetric, also at the points on the real axis.

theorem TauCeti.contDiffOn_evenReflection {F : Type u_1} {w : ℂ → F} [NormedAddCommGroup F] [NormedSpace ℝ F] {U : Set ℂ} (hU : IsOpen U) (hUc : ∀ z ∈ U, (starRingEnd ℂ) z ∈ U) (hw : ContDiffOn ℝ 2 w ({z : ℂ | 0 ≤ z.im} ∩ U)) (hN : ∀ x ∈ U, x.im = 0 → (fderivWithin ℝ w ({z : ℂ | 0 ≤ z.im} ∩ U) x) Complex.I = 0) : ContDiffOn ℝ 2 (evenReflection w) U

C² regularity of the even reflection. Let U be an open set invariant under conjugation, and let w be C² on {0 ≤ im z} ∩ U, up to the real axis, with vanishing normal derivative ∂ₜ w = 0 at the points of U on the axis. Then the even reflection of w is C² on U.

The Laplacian of the even reflection

theorem TauCeti.laplacian_evenReflection_of_pos {F : Type u_1} {w : ℂ → F} {z : ℂ} [NormedAddCommGroup F] [NormedSpace ℝ F] (hz : 0 < z.im) : Laplacian.laplacian (evenReflection w) z = Laplacian.laplacian w z

Above the real axis the even reflection has the Laplacian of w.

theorem TauCeti.laplacian_evenReflection_of_neg {F : Type u_1} {w : ℂ → F} {z : ℂ} [NormedAddCommGroup F] [NormedSpace ℝ F] (hz : z.im < 0) : Laplacian.laplacian (evenReflection w) z = Laplacian.laplacian w ((starRingEnd ℂ) z)

Below the real axis the even reflection has the Laplacian of w at the mirror point.