abel-theorem: the planar log piece and its residue identity (design §4.1 step 5, planar core)

Unit: abel-theorem. Namespace RS.Abel. Pure ℂ → ℂ, no manifold imports.

LogPieceData packages one planar weak-solution piece exactly as AbelWeak/SingleChart.lean builds it: inside ball c ρ the rational function (z - β)/(z - α) (simple zero at β, simple pole at α), interpolated to 1 across the bump annulus ρ < rIn ≤ ‖z - c‖ ≤ rOut through exp (χ · L) with L the exterior log branch (exists_exteriorLogBranch). Exports:

• g — the piece itself, with the SingleChart-style facts (g_eqOn_inner, g_one, g_contDiffAt, g_ne_zero) plus the punctured-limit factorizations tendsto_zero_factor / tendsto_pole_factor (feeding the order bookkeeping of UpgradeDischarge.lean);
• dlog — the (0,1) logarithmic-derivative coefficient h = dbar(χL), globally smooth, compactly supported in the closed bump annulus, with dbarg = h · g off {α, β} (wirtingerDbar_g);
• integral_dlog_mul — Forster's Lemma 20.3/20.5 in planar form: for any holomorphic primitive pair Gp' = w on a ball containing the piece, ∫ h·w dA = π (Gp β - Gp α) — the annulus-Stokes atom (circleIntegral_sub_circleIntegral_eq_two_mul_I_mul_integral_wirtingerDbar) reduces the area integral to -∮ L·w over the inner circle, integration by parts along the circle (circleIntegral.integral_eq_zero_of_hasDerivWithinAt) trades L·w for the two-pole kernel ((z-β)⁻¹ - (z-α)⁻¹)·Gp, and the Cauchy integral formula (DiffContOnCl.circleIntegral_sub_inv_smul) evaluates it.

structure RS.Abel.LogPieceData : Type

One planar log piece: zero at β, pole at α, both inside ball c ρ, with a fixed exterior log branch L and bump χ.

• c : ℂ

  The chart-ball center.

• ρ : ℝ

  The inner radius enclosing the two divisor points.

• hρ : 0 < self.ρ
• α : ℂ

  The pole.

• β : ℂ

  The zero.

• hne : self.α ≠ self.β
• hα : self.α - self.c ∈ Metric.ball 0 self.ρ
• hβ : self.β - self.c ∈ Metric.ball 0 self.ρ
• χ : ContDiffBump 0

  The interpolation bump (recentred at 0).

• hρχ : self.ρ < self.χ.rIn
• L : ℂ → ℂ

  The exterior log branch of (z - (β - c))/(z - (α - c)) on {ρ < ‖z‖}.

• hL (z : ℂ) : self.ρ < ‖z‖ → HasDerivAt self.L (1 / (z - (self.β - self.c)) - 1 / (z - (self.α - self.c))) z
• hLexp (z : ℂ) : self.ρ < ‖z‖ → Complex.exp (self.L z) = (z - (self.β - self.c)) / (z - (self.α - self.c))

theorem RS.Abel.LogPieceData.hρOut (P : LogPieceData) : P.ρ < P.χ.rOut

noncomputable def RS.Abel.LogPieceData.g (P : LogPieceData) : ℂ → ℂ

The piece.

Equations

• P.g z = if ‖z - P.c‖ ≤ P.ρ then (z - P.β) / (z - P.α) else Complex.exp (↑(↑P.χ (z - P.c)) * P.L (z - P.c))

theorem RS.Abel.LogPieceData.hasDerivAt_L_sub (P : LogPieceData) {z : ℂ} (hz : P.ρ < ‖z - P.c‖) : HasDerivAt (fun (w : ℂ) => P.L (w - P.c)) (1 / (z - P.β) - 1 / (z - P.α)) z

The recentred branch composite and its derivative.

theorem RS.Abel.LogPieceData.exp_L_sub (P : LogPieceData) {z : ℂ} (hz : P.ρ < ‖z - P.c‖) : Complex.exp (P.L (z - P.c)) = (z - P.β) / (z - P.α)

theorem RS.Abel.LogPieceData.g_consistent (P : LogPieceData) {z : ℂ} (hz1 : P.ρ < ‖z - P.c‖) (hz2 : ‖z - P.c‖ ≤ P.χ.rIn) : P.g z = (z - P.β) / (z - P.α)

Consistency on the transition annulus.

theorem RS.Abel.LogPieceData.g_one (P : LogPieceData) {z : ℂ} (hz : P.χ.rOut ≤ ‖z - P.c‖) : P.g z = 1

The piece is 1 far from the center.

theorem RS.Abel.LogPieceData.g_eqOn_inner (P : LogPieceData) : Set.EqOn P.g (fun (z : ℂ) => (z - P.β) / (z - P.α)) (Metric.ball P.c P.χ.rIn)

The piece is the rational function on the whole inner ball.

theorem RS.Abel.LogPieceData.g_exp (P : LogPieceData) {z : ℂ} (hz : P.ρ < ‖z - P.c‖) : P.g z = Complex.exp (↑(↑P.χ (z - P.c)) * P.L (z - P.c))

The piece agrees with exp (χ L) on the exterior region.

theorem RS.Abel.LogPieceData.isOpen_exterior (P : LogPieceData) : IsOpen {w : ℂ | P.ρ < ‖w - P.c‖}

theorem RS.Abel.LogPieceData.mem_exterior (P : LogPieceData) {z : ℂ} (hz : P.ρ < ‖z - P.c‖) : z ∈ {w : ℂ | P.ρ < ‖w - P.c‖}

theorem RS.Abel.LogPieceData.notMem_exterior (P : LogPieceData) {z : ℂ} (hz : ¬P.ρ < ‖z - P.c‖) : z ∉ {w : ℂ | P.ρ < ‖w - P.c‖}

theorem RS.Abel.LogPieceData.contDiffAt_chiL (P : LogPieceData) {z : ℂ} (hz : P.ρ < ‖z - P.c‖) : ContDiffAt ℝ (↑⊤) (fun (w : ℂ) => ↑(↑P.χ (w - P.c)) * P.L (w - P.c)) z

The bump-log product is real-smooth on the exterior region.

theorem RS.Abel.LogPieceData.g_contDiffAt (P : LogPieceData) {z : ℂ} (hz : z ≠ P.α) : ContDiffAt ℝ (↑⊤) P.g z

Real-smoothness of the piece off the pole.

theorem RS.Abel.LogPieceData.g_ne_zero (P : LogPieceData) {z : ℂ} (hzα : z ≠ P.α) (hzβ : z ≠ P.β) : P.g z ≠ 0

Non-vanishing off the divisor.

theorem RS.Abel.LogPieceData.g_zero_at_zero (P : LogPieceData) : P.g P.β = 0

The (0,1) logarithmic-derivative coefficient

noncomputable def RS.Abel.LogPieceData.dlog (P : LogPieceData) : ℂ → ℂ

The dbar log g coefficient: dbar(χ L) on the exterior region, 0 inside.

Equations

• P.dlog = {w : ℂ | P.ρ < ‖w - P.c‖}.indicator (RS.wirtingerDbar fun (w : ℂ) => ↑(↑P.χ (w - P.c)) * P.L (w - P.c))

theorem RS.Abel.LogPieceData.dlog_eq_zero_inner (P : LogPieceData) {z : ℂ} (hz : ‖z - P.c‖ < P.χ.rIn) : P.dlog z = 0

The coefficient vanishes on the inner ball (where χ ≡ 1 and L is holomorphic).

theorem RS.Abel.LogPieceData.dlog_eq_zero_outer (P : LogPieceData) {z : ℂ} (hz : P.χ.rOut < ‖z - P.c‖) : P.dlog z = 0

The coefficient vanishes outside the closed bump ball.

theorem RS.Abel.LogPieceData.support_dlog_subset (P : LogPieceData) : Function.support P.dlog ⊆ Metric.closedBall P.c P.χ.rOut \ Metric.ball P.c P.χ.rIn

The support of the coefficient sits in the closed bump annulus.

theorem RS.Abel.LogPieceData.contDiff_dlog (P : LogPieceData) : ContDiff ℝ (↑⊤) P.dlog

Global smoothness of the coefficient.

The exponential chain rule and the logarithmic-derivative identity

theorem RS.Abel.LogPieceData.wirtingerDbar_cexp (v : ℂ → ℂ) (z : ℂ) (hv : DifferentiableAt ℝ v z) : wirtingerDbar (fun (w : ℂ) => Complex.exp (v w)) z = Complex.exp (v z) * wirtingerDbar v z

dbar(exp v) = exp v · dbarv for real-differentiable v.

theorem RS.Abel.LogPieceData.wirtingerDbar_g (P : LogPieceData) {z : ℂ} (hzα : z ≠ P.α) (_hzβ : z ≠ P.β) : wirtingerDbar P.g z = P.dlog z * P.g z

The logarithmic-derivative identity: dbarg = dlog · g off the divisor.

Punctured-limit factorizations (order bookkeeping inputs)

theorem RS.Abel.LogPieceData.tendsto_zero_factor (P : LogPieceData) : Filter.Tendsto (fun (z : ℂ) => P.g z * (z - P.β)⁻¹) (nhdsWithin P.β {P.β}ᶜ) (nhds (P.β - P.α)⁻¹)

At the zero β: g(z)/(z - β) → (β - α)⁻¹ ≠ 0.

theorem RS.Abel.LogPieceData.tendsto_pole_factor (P : LogPieceData) : Filter.Tendsto (fun (z : ℂ) => P.g z * (z - P.α)) (nhdsWithin P.α {P.α}ᶜ) (nhds (P.α - P.β))

At the pole α: g(z)·(z - α) → α - β ≠ 0.

The residue identity (Forster 20.3/20.5, planar)

theorem RS.Abel.LogPieceData.integral_dlog_mul (P : LogPieceData) {r : ℝ} (hr : P.χ.rOut < r) {w Gp : ℂ → ℂ} (hprim : ∀ z ∈ Metric.ball P.c r, HasDerivAt Gp (w z) z) : ∫ (z : ℂ), P.dlog z * w z = ↑Real.pi * (Gp P.β - Gp P.α)

The residue identity: for a holomorphic primitive Gp of w on a ball containing the whole piece, ∫ dlog · w dA = π (Gp β - Gp α).