18.6. PlanarStokes.PlanarCompactSupportStokes🔗

Jacobians.PlanarStokes.PlanarCompactSupportStokes — source

integrable_fderiv_apply_of_compactSupport

The directional derivative of a C¹ compactly-supported φ : ℂ → ℂ is integrable.

theorem integrable_fderiv_apply_of_compactSupport (φ : ℂ → ℂ) (hφ : ContDiff ℝ 1 φ)
    (hsupp : HasCompactSupport φ) (v : ℂ) :
    Integrable (fun z : ℂ => fderiv ℝ φ z v) volume

integral_fderiv_apply_eq_zero

Forster (10.20) on the plane, directional form: every directional derivative of a C¹ compactly-supported φ : ℂ → ℂ has vanishing area integral, ∫_ℂ ∂_v φ = 0 (in particular the two partials v = 1, v = I). Mathlib Haar integration by parts against the constant 1.

theorem integral_fderiv_apply_eq_zero (φ : ℂ → ℂ) (hφ : ContDiff ℝ 1 φ)
    (hsupp : HasCompactSupport φ) (v : ℂ) :
    ∫ z : ℂ, fderiv ℝ φ z v = 0

integral_dbar_eq_zero

∫_ℂ ∂̄φ = 0 for C¹ compactly-supported φ (DbarDisk.dbar = the repo's Wirtinger ∂̄ = ½(∂ₓ + i∂_y)). The well-definedness engine for the residue functional (Forster 17.1).

theorem integral_dbar_eq_zero (φ : ℂ → ℂ) (hφ : ContDiff ℝ 1 φ)
    (hsupp : HasCompactSupport φ) :
    ∫ z : ℂ, DbarDisk.dbar φ z = 0

integral_del_eq_zero

∫_ℂ ∂φ = 0 for C¹ compactly-supported φ (Wirtinger ∂ = ½(∂ₓ − i∂_y), stated inline — the repo has no named ∂).

theorem integral_del_eq_zero (φ : ℂ → ℂ) (hφ : ContDiff ℝ 1 φ)
    (hsupp : HasCompactSupport φ) :
    ∫ z : ℂ, (2 : ℂ)⁻¹ * (fderiv ℝ φ z 1 - Complex.I * fderiv ℝ φ z Complex.I) = 0