abel-theorem: chart-supported (0,1)-forms and pairing localization (design §4.1 step 5)

Unit: abel-theorem. Namespace RS.Abel.

The packaging device for design step 5: a planar function h smooth on ℂ, supported in a compact K inside the target of one maximal-atlas chart e, spreads to a global (0,1)-form ChartSupportedData.form whose coefficient in any preferred chart is the conj (deriv τ)-transported copy of h (exactly Form01.compat's law) — the concrete global object that a weak solution's chart-local dbarf/f-data assembles into.

Two consumption lemmas:

• ChartSupportedData.coeffAt_center / coeffAt_center_of_notMem: the coefficient at a chart center, active and inactive cases (feeding the dbar-matching of UpgradeDischarge.lean).
• pairing_form (the localization): pairing PU D.form θ = ∫ z, h z · coeffIn e θ z — the global PoU pairing of a chart-supported form collapses to ONE planar integral in the supporting chart. Proof: per PoU index, transport by the (1,1)-density change of variables (integral_eq_integral_transition), where the conj (deriv)-factor of the form's transported coefficient cancels against the transition's normSq (deriv) and coeffIn_trans (deriv_trans_mul_deriv_trans_symm), then sum ∑ᵢ ψᵢ = 1.

Also here: the inverse-derivative units deriv_trans_mul_deriv_trans_symm / deriv_trans_ne_zero (consumed again by the order bookkeeping in UpgradeDischarge.lean), and Form01.coeffAt_finsetSum.

Inverse-derivative units

theorem RS.Abel.deriv_trans_mul_deriv_trans_symm {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {w : ℂ} (hw : w ∈ ↑e' '' (e.source ∩ e'.source)) : deriv (↑e ∘ ↑e'.symm) w * deriv (↑e' ∘ ↑e.symm) (↑e (↑e'.symm w)) = 1

The two transition derivatives at matched points multiply to 1.

theorem RS.Abel.deriv_trans_ne_zero {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {e e' : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) {w : ℂ} (hw : w ∈ ↑e' '' (e.source ∩ e'.source)) : deriv (↑e ∘ ↑e'.symm) w ≠ 0

Transition derivatives never vanish.

Finset sums of (0,1)-form coefficients

theorem RS.Abel.Form01.coeffAt_finsetSum {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} (s : Finset ι) (F : ι → Form01 X) (x : X) (z : ℂ) : (∑ k ∈ s, F k).coeffAt x z = ∑ k ∈ s, (F k).coeffAt x z

Chart-supported (0,1)-data

structure RS.Abel.ChartSupportedData (X : Type u_1) [TopologicalSpace X] [ChartedSpace ℂ X] : Type u_1

A planar (0,1)-coefficient supported compactly inside one maximal-atlas chart.

• e : OpenPartialHomeomorph X ℂ

  The supporting chart.

• he : self.e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X
• h : ℂ → ℂ

  The planar coefficient in the supporting chart.

• smooth : ContDiff ℝ (↑⊤) self.h
• K : Set ℂ

  The compact planar carrier.

• hK : IsCompact self.K
• hKsub : self.K ⊆ self.e.target
• hsupp : Function.support self.h ⊆ self.K

def RS.Abel.ChartSupportedData.Ksrc {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : ChartSupportedData X) : Set X

The source-side compact carrier.

Equations

• D.Ksrc = ↑D.e.symm '' D.K

theorem RS.Abel.ChartSupportedData.isCompact_Ksrc {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : ChartSupportedData X) : IsCompact D.Ksrc

theorem RS.Abel.ChartSupportedData.Ksrc_subset_source {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : ChartSupportedData X) : D.Ksrc ⊆ D.e.source

theorem RS.Abel.ChartSupportedData.h_eq_zero_of_notMem_Ksrc {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : ChartSupportedData X) {y : X} (hy : y ∈ D.e.source) (hyK : y ∉ D.Ksrc) : D.h (↑D.e y) = 0

noncomputable def RS.Abel.ChartSupportedData.coeff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : ChartSupportedData X) (x : X) : ℂ → ℂ

The raw coefficient formula in the preferred chart at x.

Equations

• D.coeff x = (↑(chartAt ℂ x) '' ((chartAt ℂ x).source ∩ D.e.source)).indicator fun (z : ℂ) => (starRingEnd ℂ) (deriv (↑D.e ∘ ↑(chartAt ℂ x).symm) z) * D.h (↑D.e (↑(chartAt ℂ x).symm z))

theorem RS.Abel.ChartSupportedData.mem_coeffSet_iff {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : ChartSupportedData X) (x : X) {z : ℂ} (hz : z ∈ (chartAt ℂ x).target) : ↑(chartAt ℂ x).symm z ∈ D.e.source ↔ z ∈ ↑(chartAt ℂ x) '' ((chartAt ℂ x).source ∩ D.e.source)

theorem RS.Abel.ChartSupportedData.coeffSet_subset_target {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (D : ChartSupportedData X) (x : X) : ↑(chartAt ℂ x) '' ((chartAt ℂ x).source ∩ D.e.source) ⊆ (chartAt ℂ x).target

theorem RS.Abel.ChartSupportedData.coeff_eventuallyEq_zero {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] (D : ChartSupportedData X) (x : X) {z : ℂ} (hz : z ∈ (chartAt ℂ x).target) (hy : ↑(chartAt ℂ x).symm z ∉ D.Ksrc) : D.coeff x =ᶠ[nhds z] 0

The coefficient vanishes near any target point whose source point avoids the compact source carrier.

noncomputable def RS.Abel.ChartSupportedData.form {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : ChartSupportedData X) : Form01 X

The chart-supported global (0,1)-form.

Equations

• D.form = { coeffAt := D.coeff, coeffAt_zero_off := ⋯, contDiffOn_coeffAt := ⋯, compat := ⋯ }

theorem RS.Abel.ChartSupportedData.form_coeffAt_center {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : ChartSupportedData X) {x : X} (hx : x ∈ D.e.source) : D.form.coeffAt x (↑(chartAt ℂ x) x) = (starRingEnd ℂ) (deriv (↑D.e ∘ ↑(chartAt ℂ x).symm) (↑(chartAt ℂ x) x)) * D.h (↑D.e x)

The coefficient at an active chart center.

theorem RS.Abel.ChartSupportedData.form_coeffAt_center_of_notMem {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (D : ChartSupportedData X) {x : X} (hx : x ∉ D.e.source) : D.form.coeffAt x (↑(chartAt ℂ x) x) = 0

The coefficient at an inactive chart center.

Pairing localization

theorem RS.Abel.pairing_form {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] (PU : SurfPoU X) (D : ChartSupportedData X) (θ : Form1 X) : pairing PU D.form θ = ∫ (z : ℂ), D.h z * coeffIn D.e θ z

The localization lemma: the global PoU pairing of a chart-supported (0,1)-form collapses to a single planar integral in the supporting chart.