18.7. PlanarStokes.PlanarHolomorphicChangeOfVariables🔗

Jacobians.PlanarStokes.PlanarHolomorphicChangeOfVariables — source

det_restrictScalars_smulRight

The ℝ-linear endomorphism of ℂ given by multiplication by d (the restrictScalars of the canonical smulRight form of the complex derivative) has determinant normSq d = |d|².

theorem det_restrictScalars_smulRight (d : ℂ) :
    (((1 : ℂ →L[ℂ] ℂ).smulRight d).restrictScalars ℝ : ℂ →L[ℝ] ℂ).det
      = Complex.normSq d

integral_image_holomorphic

Planar holomorphic change of variables (unconditional — both sides may fail to be integrable, in which case both are 0):

∫_{T''U} F(w) dw = ∫_U normSq(T′(z)) • F(T(z)) dz

for T ℂ-differentiable and injective on the measurable U.

theorem integral_image_holomorphic {U : Set ℂ} (hU : MeasurableSet U) {T : ℂ → ℂ}
    (hT : ∀ z ∈ U, DifferentiableAt ℂ T z) (hinj : Set.InjOn T U) (F : ℂ → ℂ) :
    ∫ w in T '' U, F w = ∫ z in U, Complex.normSq (deriv T z) • F (T z)

dbar_comp_holomorphic

The ∂̄ chain rule for g ∘ T with T holomorphic:

∂̄(g∘T)(z) = ∂̄g(T z) · conj (T′ z).

This is the transformation rule of a (0,1)-form coefficient. Pure linear algebra on the real Fréchet derivatives: fderiv ℝ T z is multiplication by c := T′(z), and for any ℝ-linear M : ℂ → ℂ, M(c) + i·M(i·c) = conj(c)·(M(1) + i·M(i)) (decompose c = c.re + c.im·i).

theorem dbar_comp_holomorphic {g T : ℂ → ℂ} {z : ℂ}
    (hg : DifferentiableAt ℝ g (T z)) (hT : DifferentiableAt ℂ T z) :
    DbarDisk.dbar (g ∘ T) z = DbarDisk.dbar g (T z) * (starRingEnd ℂ) (deriv T z)