Planar Wirtinger derivatives on Schwartz space

The planar operators ∂ = (∂ₛ - i ∂ₜ) / 2 and bar∂ = (∂ₛ + i ∂ₜ) / 2 preserve Schwartz space and are continuous and complex linear. On the Fourier side they are multiplication by πi conj ξ and πi ξ, respectively. Evaluation agrees with the existing Wirtinger derivatives applied to the direction 1.

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, second edition, Appendix B.2 (planar Cauchy–Riemann operators).

noncomputable def SchwartzMap.conjWirtingerDerivCLM (F : Type u_1) [NormedAddCommGroup F] [NormedSpace ℂ F] : SchwartzMap ℂ F →L[ℂ] SchwartzMap ℂ F

The planar conjugate Wirtinger derivative (∂ₛ + i ∂ₜ) / 2 on Schwartz space.

theorem SchwartzMap.conjWirtingerDerivCLM_eq {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (u : SchwartzMap ℂ F) : (conjWirtingerDerivCLM F) u = 2⁻¹ • (LineDeriv.lineDerivOp 1 u + Complex.I • LineDeriv.lineDerivOp Complex.I u)

The conjugate Wirtinger derivative as the sum of the two directional derivatives.

@[simp]

theorem SchwartzMap.conjWirtingerDerivCLM_apply {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (u : SchwartzMap ℂ F) (z : ℂ) : ((conjWirtingerDerivCLM F) u) z = (TauCeti.conjWirtingerDeriv (⇑u) z) 1

Evaluation agrees with TauCeti.conjWirtingerDeriv in direction 1.

noncomputable def SchwartzMap.wirtingerDerivCLM (F : Type u_1) [NormedAddCommGroup F] [NormedSpace ℂ F] : SchwartzMap ℂ F →L[ℂ] SchwartzMap ℂ F

The planar Wirtinger derivative (∂ₛ - i ∂ₜ) / 2 on Schwartz space.

theorem SchwartzMap.wirtingerDerivCLM_eq {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (u : SchwartzMap ℂ F) : (wirtingerDerivCLM F) u = 2⁻¹ • (LineDeriv.lineDerivOp 1 u + -Complex.I • LineDeriv.lineDerivOp Complex.I u)

The Wirtinger derivative as the difference of the two directional derivatives.

@[simp]

theorem SchwartzMap.wirtingerDerivCLM_apply {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (u : SchwartzMap ℂ F) (z : ℂ) : ((wirtingerDerivCLM F) u) z = (TauCeti.wirtingerDeriv (⇑u) z) 1

Evaluation agrees with TauCeti.wirtingerDeriv in direction 1.

theorem SchwartzMap.fourier_conjWirtingerDerivCLM_apply {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (u : SchwartzMap ℂ F) (ξ : ℂ) : (FourierTransform.fourier ((conjWirtingerDerivCLM F) u)) ξ = (↑Real.pi * Complex.I * ξ) • (FourierTransform.fourier u) ξ

On the Fourier side bar∂ is multiplication by πi ξ.

theorem SchwartzMap.fourier_wirtingerDerivCLM_apply {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (u : SchwartzMap ℂ F) (ξ : ℂ) : (FourierTransform.fourier ((wirtingerDerivCLM F) u)) ξ = (↑Real.pi * Complex.I * (starRingEnd ℂ) ξ) • (FourierTransform.fourier u) ξ

On the Fourier side ∂ is multiplication by πi conj ξ.