Weak conjugate Wirtinger derivatives

HasWeakConjWirtingerDerivOn μ Ω u g expresses \bar∂u = g by integration by parts against real smooth compactly supported test functions. The normalization is \bar∂ = (∂₁ + I ∂ᵢ)/2. This does not require either real first derivative of u to be represented by a function.

The codomain is complete and both functions are locally integrable, preventing the totalized Bochner integral from making the defining identity vacuous. With a Haar measure the identity is the distributional equation; for a general measure it is the corresponding adjoint relation.

Main results

The relation is local, complex-linear, invariant under almost-everywhere replacement and compatible with continuous complex-linear maps. Its value is unique almost everywhere. hasWeakConjWirtingerDerivOn_of_hasWeakLineDerivOn and HasWeakFDerivOn.hasWeakConjWirtingerDerivOn compare it with the native real weak derivatives, and HasWeakConjWirtingerDerivOn.weakLineDeriv differentiates the equation in a real direction. hasWeakConjWirtingerDerivOn_of_contDiffOn compares it with the classical normalized operator; for real C¹ maps, its vanishing is equivalent to holomorphy. Every holomorphic map solves the distributional equation. hasWeakConjWirtingerDerivOn_conj computes the weak derivative of conjugation as 1, which rules out an almost-everywhere equal holomorphic representative on nonempty open sets.

References

• D. McDuff and D. Salamon, J-holomorphic Curves and Symplectic Topology, second edition, Appendix B.

def TauCeti.HasWeakConjWirtingerDerivOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] (μ : MeasureTheory.Measure ℂ) (Ω : TopologicalSpace.Opens ℂ) (u g : ℂ → F) : Prop

The normalized distributional equation \bar∂u = g, relative to μ, with locally integrable source and derivative and a complete codomain. Real tests suffice for a complex-linear equation.

theorem TauCeti.hasWeakConjWirtingerDerivOn_iff {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g : ℂ → F} : HasWeakConjWirtingerDerivOn μ Ω u g ↔ CompleteSpace F ∧ MeasureTheory.LocallyIntegrableOn u (↑Ω) μ ∧ MeasureTheory.LocallyIntegrableOn g (↑Ω) μ ∧ ∀ (φ : TestFunction Ω ℝ ⊤), ∫ (z : ℂ), lineDeriv ℝ (⇑φ) z 1 • u z ∂μ + Complex.I • ∫ (z : ℂ), lineDeriv ℝ (⇑φ) z Complex.I • u z ∂μ = -2 • ∫ (z : ℂ), φ z • g z ∂μ

The defining conditions, usable without unfolding the sealed definition.

theorem TauCeti.HasWeakConjWirtingerDerivOn.completeSpace {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g : ℂ → F} (h : HasWeakConjWirtingerDerivOn μ Ω u g) : CompleteSpace F

The codomain of a weak conjugate Wirtinger derivative is complete.

theorem TauCeti.HasWeakConjWirtingerDerivOn.locallyIntegrableOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g : ℂ → F} (h : HasWeakConjWirtingerDerivOn μ Ω u g) : MeasureTheory.LocallyIntegrableOn u (↑Ω) μ

The source is locally integrable.

theorem TauCeti.HasWeakConjWirtingerDerivOn.locallyIntegrableOn_deriv {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g : ℂ → F} (h : HasWeakConjWirtingerDerivOn μ Ω u g) : MeasureTheory.LocallyIntegrableOn g (↑Ω) μ

The weak conjugate Wirtinger derivative is locally integrable.

theorem TauCeti.HasWeakConjWirtingerDerivOn.integral_lineDeriv_smul_add_I_smul_eq_neg_two_smul_integral_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g : ℂ → F} (h : HasWeakConjWirtingerDerivOn μ Ω u g) (φ : TestFunction Ω ℝ ⊤) : ∫ (z : ℂ), lineDeriv ℝ (⇑φ) z 1 • u z ∂μ + Complex.I • ∫ (z : ℂ), lineDeriv ℝ (⇑φ) z Complex.I • u z ∂μ = -2 • ∫ (z : ℂ), φ z • g z ∂μ

Integration by parts for the normalized conjugate Wirtinger derivative.

theorem TauCeti.HasWeakConjWirtingerDerivOn.mono {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g : ℂ → F} {Ω' : TopologicalSpace.Opens ℂ} (h : HasWeakConjWirtingerDerivOn μ Ω u g) (hΩ : Ω' ≤ Ω) : HasWeakConjWirtingerDerivOn μ Ω' u g

Weak conjugate Wirtinger differentiation restricts to smaller open sets.

@[simp]

theorem TauCeti.hasWeakConjWirtingerDerivOn_zero {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} [CompleteSpace F] : HasWeakConjWirtingerDerivOn μ Ω 0 0

The zero function has weak conjugate Wirtinger derivative zero.

theorem TauCeti.HasWeakConjWirtingerDerivOn.neg {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g : ℂ → F} (h : HasWeakConjWirtingerDerivOn μ Ω u g) : HasWeakConjWirtingerDerivOn μ Ω (-u) (-g)

Weak conjugate Wirtinger differentiation commutes with negation.

theorem TauCeti.HasWeakConjWirtingerDerivOn.add {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g v k : ℂ → F} (h : HasWeakConjWirtingerDerivOn μ Ω u g) (hv : HasWeakConjWirtingerDerivOn μ Ω v k) : HasWeakConjWirtingerDerivOn μ Ω (u + v) (g + k)

Weak conjugate Wirtinger differentiation commutes with addition.

theorem TauCeti.HasWeakConjWirtingerDerivOn.sub {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g v k : ℂ → F} (h : HasWeakConjWirtingerDerivOn μ Ω u g) (hv : HasWeakConjWirtingerDerivOn μ Ω v k) : HasWeakConjWirtingerDerivOn μ Ω (u - v) (g - k)

Weak conjugate Wirtinger differentiation commutes with subtraction.

theorem TauCeti.HasWeakConjWirtingerDerivOn.clm_comp {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g : ℂ → F} {G : Type u_2} [NormedAddCommGroup G] [NormedSpace ℂ G] [CompleteSpace G] (h : HasWeakConjWirtingerDerivOn μ Ω u g) (L : F →L[ℂ] G) : HasWeakConjWirtingerDerivOn μ Ω (fun (z : ℂ) => L (u z)) fun (z : ℂ) => L (g z)

A complex continuous linear map commutes with the weak conjugate Wirtinger derivative.

theorem TauCeti.HasWeakConjWirtingerDerivOn.const_smul {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g : ℂ → F} (h : HasWeakConjWirtingerDerivOn μ Ω u g) (c : ℂ) : HasWeakConjWirtingerDerivOn μ Ω (c • u) (c • g)

Weak conjugate Wirtinger differentiation is complex-linear.

theorem TauCeti.HasWeakConjWirtingerDerivOn.congr_ae {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g v : ℂ → F} (h : HasWeakConjWirtingerDerivOn μ Ω u g) (huv : u =ᵐ[μ.restrict ↑Ω] v) : HasWeakConjWirtingerDerivOn μ Ω v g

Almost-everywhere replacement on the open set preserves the source of a weak derivative.

theorem TauCeti.HasWeakConjWirtingerDerivOn.congr_ae_deriv {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g k : ℂ → F} (h : HasWeakConjWirtingerDerivOn μ Ω u g) (hgk : g =ᵐ[μ.restrict ↑Ω] k) : HasWeakConjWirtingerDerivOn μ Ω u k

Almost-everywhere replacement preserves the weak conjugate Wirtinger derivative.

theorem TauCeti.HasWeakConjWirtingerDerivOn.ae_eq {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u g k : ℂ → F} (h : HasWeakConjWirtingerDerivOn μ Ω u g) (hk : HasWeakConjWirtingerDerivOn μ Ω u k) : g =ᵐ[μ.restrict ↑Ω] k

The weak conjugate Wirtinger derivative is unique almost everywhere on the open set.

theorem TauCeti.hasWeakConjWirtingerDerivOn_of_hasWeakLineDerivOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u us ut : ℂ → F} (hs : HasWeakLineDerivOn μ Ω u us 1) (ht : HasWeakLineDerivOn μ Ω u ut Complex.I) : HasWeakConjWirtingerDerivOn μ Ω u fun (z : ℂ) => 2⁻¹ • (us z + Complex.I • ut z)

The two weak real partial derivatives combine to the normalized weak \bar∂ derivative.

theorem TauCeti.HasWeakFDerivOn.hasWeakConjWirtingerDerivOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u : ℂ → F} {D : ℂ → ℂ →L[ℝ] F} (h : HasWeakFDerivOn μ Ω u D) : HasWeakConjWirtingerDerivOn μ Ω u fun (z : ℂ) => 2⁻¹ • ((D z) 1 + Complex.I • (D z) Complex.I)

A weak Fréchet derivative determines the weak conjugate Wirtinger derivative.

theorem TauCeti.hasWeakConjWirtingerDerivOn_of_contDiffOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u : ℂ → F} [CompleteSpace F] [μ.IsAddHaarMeasure] (hu : ContDiffOn ℝ 1 u ↑Ω) : HasWeakConjWirtingerDerivOn μ Ω u fun (z : ℂ) => (conjWirtingerDeriv u z) 1

The classical conjugate Wirtinger derivative of a C¹ function is its weak derivative.

theorem TauCeti.hasWeakConjWirtingerDerivOn_conj {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} [μ.IsAddHaarMeasure] : HasWeakConjWirtingerDerivOn μ Ω ⇑(starRingEnd ℂ) fun (x : ℂ) => 1

Conjugation has normalized weak \bar∂ derivative 1, fixing both its sign and factor.

theorem TauCeti.hasWeakConjWirtingerDerivOn_zero_iff_of_contDiffOn {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u : ℂ → F} [CompleteSpace F] [μ.IsAddHaarMeasure] (hu : ContDiffOn ℝ 1 u ↑Ω) : HasWeakConjWirtingerDerivOn μ Ω u 0 ↔ DifferentiableOn ℂ u ↑Ω

For a function of class C¹ over ℝ, the weak equation \bar∂u=0 is precisely holomorphy.

theorem DifferentiableOn.hasWeakConjWirtingerDerivOn_zero {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u : ℂ → F} [CompleteSpace F] [μ.IsAddHaarMeasure] (h : DifferentiableOn ℂ u ↑Ω) : TauCeti.HasWeakConjWirtingerDerivOn μ Ω u 0

Every holomorphic function with Banach coefficients solves the distributional equation.

theorem TauCeti.not_exists_differentiableOn_ae_eq_conj {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} [μ.IsAddHaarMeasure] (hΩ : (↑Ω).Nonempty) : ¬∃ (v : ℂ → ℂ), DifferentiableOn ℂ v ↑Ω ∧ ⇑(starRingEnd ℂ) =ᵐ[μ.restrict ↑Ω] v

Conjugation cannot agree almost everywhere with a holomorphic function on a nonempty open set: its weak \bar∂ derivative is 1, while a holomorphic representative has derivative 0.

theorem TauCeti.HasWeakConjWirtingerDerivOn.weakLineDeriv {F : Type u_1} [NormedAddCommGroup F] [NormedSpace ℂ F] {μ : MeasureTheory.Measure ℂ} {Ω : TopologicalSpace.Opens ℂ} {u f u' f' : ℂ → F} {v : ℂ} (h : HasWeakConjWirtingerDerivOn μ Ω u f) (hu : HasWeakLineDerivOn μ Ω u u' v) (hf : HasWeakLineDerivOn μ Ω f f' v) : HasWeakConjWirtingerDerivOn μ Ω u' f'

A weak directional derivative of a solution of \bar∂u = f solves the differentiated equation \bar∂(∂ᵥu) = ∂ᵥf. No other derivative of u or f is assumed.