30.12. Abel.AbelPairingStokes🔗

Jacobians.Abel.AbelPairingStokes — source

coverRhoCF

The j-th cover PoU component as a complex SmoothCFunctions (ρ̃ⱼ = ofReal ∘ ρⱼ).

def coverRhoCF (j : Fin ((chartCover : Finset X).card)) : SmoothCFunctions X

sum_coverRhoCF

The PoU components sum to the constant 1.

theorem sum_coverRhoCF : ∑ j, coverRhoCF (X := X) j = 1

dbarL_coverRhoCF_eq_zero_of_notMem

∂̄ρ̃ⱼ vanishes off tsupport ρⱼ.

theorem dbarL_coverRhoCF_eq_zero_of_notMem (j : Fin ((chartCover : Finset X).card)) {x : X}
    (hx : x ∉ tsupport (coverPoU (X := X) j)) : (dbarL (coverRhoCF j)) x = 0

glueForm

The j-th gluing form τⱼ := u • ∂̄ρ̃ⱼ (a global smooth (0,1)-valued form).

def glueForm (u : SmoothCFunctions X) (j : Fin ((chartCover : Finset X).card)) :
    SmoothCOneForms X

glueForm_apply

theorem glueForm_apply (u : SmoothCFunctions X) (j : Fin ((chartCover : Finset X).card))
    (x : X) : (glueForm u j) x = u x • (dbarL (coverRhoCF j)) x

glueForm_eq_zero_of_notMem

τⱼ dies off tsupport ρⱼ.

theorem glueForm_eq_zero_of_notMem (u : SmoothCFunctions X)
    (j : Fin ((chartCover : Finset X).card)) {x : X}
    (hx : x ∉ tsupport (coverPoU (X := X) j)) :
    (glueForm u j) x = (0 : ℂ →L[ℝ] ℂ)

sum_glueForm_apply

The gluing forms sum to zero: ∑ⱼ u·∂̄ρⱼ = u·∂̄(∑ρⱼ) = u·∂̄1 = 0 (pointwise).

theorem sum_glueForm_apply (u : SmoothCFunctions X) (x : X) :
    ∑ j, ((glueForm u j) x) = (0 : ℂ →L[ℝ] ℂ)

sum_glueForm

∑ⱼ τⱼ = 0 as forms.

theorem sum_glueForm (u : SmoothCFunctions X) :
    ∑ j, glueForm (X := X) u j = 0

stokesPotential

The per-chart Stokes potential Φⱼ = 𝟙·ρ̂ⱼ·ûⱼ·η̂ⱼ.

def stokesPotential (u : SmoothCFunctions X) (η : HolomorphicOneForms X)
    (j : Fin ((chartCover : Finset X).card)) : ℂ → ℂ

stokesPotential_eventuallyEq

Inside the chart image of the window the potential is the bare product (locally).

theorem stokesPotential_eventuallyEq (u : SmoothCFunctions X) (η : HolomorphicOneForms X)
    (j : Fin ((chartCover : Finset X).card)) {z : ℂ}
    (hz : z ∈ (chartAt (H := ℂ) (coverCenter j)) '' coverWindow (X := X) j) :
    stokesPotential u η j =ᶠ[𝓝 z]
      fun w => coverRhoC (X := X) j ((chartAt (H := ℂ) (coverCenter j)).symm w)
        * u ((chartAt (H := ℂ) (coverCenter j)).symm w)
        * Jacobians.Montel.localRep η (coverCenter j)
            ((chartAt (H := ℂ) (coverCenter j)).symm w)

stokesPotential_eventually_zero

Off the (compact) chart image of tsupport ρⱼ the potential vanishes locally.

theorem stokesPotential_eventually_zero (u : SmoothCFunctions X) (η : HolomorphicOneForms X)
    (j : Fin ((chartCover : Finset X).card)) {z : ℂ}
    (hz : z ∉ (chartAt (H := ℂ) (coverCenter j)) '' tsupport (coverPoU (X := X) j)) :
    stokesPotential u η j =ᶠ[𝓝 z] fun _ => 0

contDiff_stokesPotential

The potential is globally smooth.

theorem contDiff_stokesPotential (u : SmoothCFunctions X) (η : HolomorphicOneForms X)
    (j : Fin ((chartCover : Finset X).card)) :
    ContDiff ℝ (⊤ : ℕ∞) (stokesPotential u η j)

hasCompactSupport_stokesPotential

The potential has compact support.

theorem hasCompactSupport_stokesPotential (u : SmoothCFunctions X)
    (η : HolomorphicOneForms X) (j : Fin ((chartCover : Finset X).card)) :
    HasCompactSupport (stokesPotential u η j)

dbar_stokesPotential

The pointwise Stokes split: ∂̄Φⱼ = (𝟙·(∂̄ρ̂ⱼ)·ûⱼ·η̂ⱼ) + (𝟙·ρ̂ⱼ·∂̄ûⱼ·η̂ⱼ), i.e. ∂̄ of the potential is the glueForm-integrand plus the ∂̄u-integrand (the η̂ⱼ factor is holomorphic so its ∂̄ dies).

theorem dbar_stokesPotential (u : SmoothCFunctions X) (η : HolomorphicOneForms X)
    (j : Fin ((chartCover : Finset X).card)) (z : ℂ) :
    DbarDisk.dbar (stokesPotential u η j) z
      = pairingIntegrand (glueForm u j) η (fun _ => 1) (coverCenter j)
          (coverWindow (X := X) j) z
        + pairingIntegrand (dbarL u) η (coverRhoC (X := X) j) (coverCenter j)
          (coverWindow (X := X) j) z

integrable_glueForm_piece

Integrability of the glueForm piece.

theorem integrable_glueForm_piece (u : SmoothCFunctions X) (η : HolomorphicOneForms X)
    (j : Fin ((chartCover : Finset X).card)) :
    Integrable (pairingIntegrand (glueForm u j) η (fun _ => 1) (coverCenter j)
      (coverWindow (X := X) j)) volume

integral_dbar_piece_eq_neg

The per-chart Stokes identity: the ∂̄u-piece integral is minus the glueForm-piece integral.

theorem integral_dbar_piece_eq_neg (u : SmoothCFunctions X) (η : HolomorphicOneForms X)
    (j : Fin ((chartCover : Finset X).card)) :
    (∫ z, pairingIntegrand (dbarL u) η (coverRhoC (X := X) j) (coverCenter j)
      (coverWindow (X := X) j) z)
    = -∫ z, pairingIntegrand (glueForm u j) η (fun _ => 1) (coverCenter j)
        (coverWindow (X := X) j) z

pairForm_dbarL

Stokes vanishing of the pairing (Forster 19.10, necessity): the pairing of any holomorphic 1-form against a ∂̄-coboundary is zero.

theorem pairForm_dbarL (η : HolomorphicOneForms X) (u : SmoothCFunctions X) :
    pairForm η (dbarL u) = 0