Pair-form residues (`form-trace-tower`, file 1/6) #

Unit: form-trace-tower (docs/design/form-trace-tower.md §2 D2, §4.1, §5 P1). Fully independent of meromorphic-trace's build state.

For F : X → Y and h : X → ℂ, the pair-form h · F^*(dz) has coefficient h against the pullback of the target's own coordinate differential — no new Form1-meromorphic type is introduced (D1). Its residue at x, read in the PREFERRED chart pair (chartAt), is resAtX.

Deviation from the design (found during construction, recorded honestly): §4.1's resAtX_eq_of_mem_source claims resAtX may be recomputed in ANY pair of maximal-atlas charts (e, e') with NO correction factor. This is FALSE in general: e.g. X = Y = ℂ (standard self-charts), F = id, h = fun z => 1/z, x = 0. Using (e, e') = (id, id) gives resAtX F h 0 = resAt (1/z) 0 = 1. Using the (equally valid, maximal-atlas) target chart e' := (fun y => 2*y) (an entire, invertible-derivative self-map of ℂ, hence in the maximal atlas) gives resAt (fun z => (1/z) * 2) 0 = 2 ≠ 1. The root cause: changing the TARGET chart changes WHICH 1-form F^*(dz) means (d(e'_new) = deriv(e'_new ∘ e'_old.symm)(·) · d(e'_old), a coefficient that VARIES over X, not a constant), so reusing the SAME bare h against a different target chart computes the residue of a genuinely DIFFERENT 1-form. By contrast, changing only the SOURCE chart (e) is a bona fide 1-form reparametrization and IS invariant (exactly RS.resAt_comp_mul_deriv's content) — this is resAtX_eq_of_mem_source_left below, the one general, exported "chart invariance" fact. The target side is genuinely NOT free; where a target-chart change is needed (§5 P-main, comparing to AdaptedChartsAt's adapted target chart), the correction is tracked explicitly via an additional calibration hypothesis rather than assumed away (see ResidueTraceCompat.lean).

resAtX F h x — the residue of h · F^*(dz) at x (D2).
resAtX_eq_of_mem_source_left — SOURCE-chart invariance (task item 1, the TRUE half): may be computed in ANY maximal-atlas chart at x, target chart held fixed at chartAt ℂ (F x).
Basic algebra: resAtX_congr, resAtX_add, resAtX_const_mul.

source

noncomputable def RS.FormTrace.resAtX {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (h : X → ℂ) (x : X) :

ℂ

The residue at x of the pair-form h · F^*(dz), read in the PREFERRED chart at x (and the preferred chart at F x for the target coordinate). Source-side chart-independence: resAtX_eq_of_mem_source_left below.

Equations

RS.FormTrace.resAtX F h x = RS.resAt (fun (z : ℂ) => h (↑(chartAt ℂ x).symm z) * deriv (↑(chartAt ℂ (F x)) ∘ F ∘ ↑(chartAt ℂ x).symm) z) (↑(chartAt ℂ x) x)

Instances For

source

theorem RS.FormTrace.resAtX_def {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] (F : X → Y) (h : X → ℂ) (x : X) :

resAtX F h x = resAt (fun (z : ℂ) => h (↑(chartAt ℂ x).symm z) * deriv (↑(chartAt ℂ (F x)) ∘ F ∘ ↑(chartAt ℂ x).symm) z) (↑(chartAt ℂ x) x)

Compat: the two-chart `ContMDiffAt ↔ AnalyticAt` bridge #

Not currently exported by surfaces-and-charts/Meromorphic.Predicates for a general chart PAIR (e, e') on X/Y (only for f : X → ℂ against the trivial target chart, via RS.contMDiffAt_iff_analyticAt_of_mem_source). Derived here (one direction only — the direction actually needed, ContMDiffAt → AnalyticAt) directly from mathlib's contMDiffWithinAt_iff_of_mem_maximalAtlas, mirroring that existing proof's simp pattern.

source

theorem RS.FormTrace.analyticAt_comp_chart_pair {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {x : X} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hx : x ∈ e.source) {e' : OpenPartialHomeomorph Y ℂ} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y) (hFx : F x ∈ e'.source) (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) :

AnalyticAt ℂ (↑e' ∘ F ∘ ↑e.symm) (↑e x)

ContMDiffAt for a map F : X → Y gives analyticity of the chart composite in ANY pair of maximal-atlas charts (e at x, e' at F x). (Only the forward direction is proved/needed; the converse would need an extra continuity argument not required here.)

Source-chart invariance (task item 1) #

source

theorem RS.FormTrace.resAt_pairForm_source_change {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] {F : X → Y} {h : X → ℂ} {x : X} {e1 e2 : OpenPartialHomeomorph X ℂ} (he1 : e1 ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hx1 : x ∈ e1.source) (he2 : e2 ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hx2 : x ∈ e2.source) {e' : OpenPartialHomeomorph Y ℂ} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ Y) (hFx : F x ∈ e'.source) (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hh : MeromorphicAtX h x) :

resAt (fun (z : ℂ) => h (↑e1.symm z) * deriv (↑e' ∘ F ∘ ↑e1.symm) z) (↑e1 x) = resAt (fun (z : ℂ) => h (↑e2.symm z) * deriv (↑e' ∘ F ∘ ↑e2.symm) z) (↑e2 x)

Source-chart invariance of the pair-form integrand's residue: the target chart e' is held FIXED (arbitrary), only the source chart varies. The TRUE, general half of chart-invariance — directly analogous to RS.ordAtX_eq_of_mem_source, via ONE application of RS.resAt_comp_mul_deriv.

source

theorem RS.FormTrace.resAtX_eq_of_mem_source_left {X : Type u_1} {Y : Type u_2} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] [TopologicalSpace Y] [ChartedSpace ℂ Y] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ Y] {F : X → Y} {h : X → ℂ} {x : X} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hx : x ∈ e.source) (hF : ContMDiffAt (modelWithCornersSelf ℂ ℂ) (modelWithCornersSelf ℂ ℂ) ⊤ F x) (hh : MeromorphicAtX h x) :

resAtX F h x = resAt (fun (z : ℂ) => h (↑e.symm z) * deriv (↑(chartAt ℂ (F x)) ∘ F ∘ ↑e.symm) z) (↑e x)

Source-chart invariance (task item 1): resAtX may be computed in ANY maximal-atlas chart at x, provided the TARGET chart is held at the preferred chartAt ℂ (F x).