Weak solutions (abel-weak-solutions, D1 / Forster §20.1, §20.1's Lemma-20.1 multiplicativity)

Unit: abel-weak-solutions (docs/design/abel-weak-solutions.md §5). IsWeakSolutionAt/ IsWeakSolutionOfPair: bare X → ℂ functions, no ℳ X, no Divisor X (the pair-based formulation is exactly what abel-theorem consumes).

Deviation from the design's literal D1: IsWeakSolutionAt is stated with the chart taken existentially from IsManifold.maximalAtlas 𝓘(ℂ) ω X (matching the design closely) but the local-model equation is a plain f =ᶠ[𝓝 a] (...) eventual equality (junk-free, no filter-sup formula needed).

SCOPE ADDITION (per docs/design/abel-theorem.md §1.4/§4.1, its finding that Thm 21.4(b) needs the k-point case, not just k = 1): IsWeakSolutionOfFinset and isWeakSolutionOfFinset_prod package Forster's Lemma 20.1 ("weak solutions of D₁, D₂ multiply to a weak solution of D₁ + D₂") as a Finset-indexed product over ι pairwise-disjoint two-point pairs — the degenerate, already-disjoint case abel-theorem's own 21.4(a) construction sets up (no general chain/homology bookkeeping needed).

def RS.AbelWeak.IsWeakSolutionAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : X → ℂ) (a : X) (k : ℤ) : Prop

Forster 20.1's local model at a single point a: f agrees, in some maximal-atlas chart e at a, with ψ (e ·) * (e · - e a) ^ k near a, for ψ smooth and non-vanishing near e a. k : ℤ ranges over all integers (a genuine zpow, allowing a pole k < 0).

Equations

• One or more equations did not get rendered due to their size.

structure RS.AbelWeak.IsWeakSolutionOfPair {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] (f : X → ℂ) (P Q : X) : Prop

The weak-solution predicate for the two-point pair (P, Q) this unit builds: ℝ-smooth away from Q, weak-solution local model +1 at P (a genuine C^∞ zero), -1 at Q (a simple pole, excluded from the smoothness domain), non-vanishing everywhere else.

• contMDiffOn : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) f {Q}ᶜ
• ne_zero_off (x : X) : x ≠ P → x ≠ Q → f x ≠ 0
• weakAt_P : IsWeakSolutionAt f P 1
• weakAt_Q : IsWeakSolutionAt f Q (-1)

structure RS.AbelWeak.IsWeakSolutionOfFinset {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {ι : Type u_2} (f : X → ℂ) (a x : ι → X) : Prop

SCOPE ADDITION (abel-theorem's Thm 21.4(b) finding): the Finset-indexed generalization — a weak solution of k pairwise-disjoint two-point pairs (x i, a i), i : ι, order +1 at each x i, -1 at each a i, matching the conclusion shape RS.Abel.exists_mero_of_periodVector_mem needs.

• contMDiffOn : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) f (Set.range a)ᶜ
• ne_zero_off (z : X) : (∀ (i : ι), z ≠ a i) → (∀ (i : ι), z ≠ x i) → f z ≠ 0
• weakAt_x (i : ι) : IsWeakSolutionAt f (x i) 1
• weakAt_a (i : ι) : IsWeakSolutionAt f (a i) (-1)

Chart bridges: ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) ↔ planar ContDiffAt/ContDiffOn

ℂ's model 𝓘(ℝ, ℂ) has no registered ContMDiffMul instance (mathlib only registers ContMDiffRing 𝓘(𝕜) n 𝕜, i.e. the model over ITSELF, not 𝓘(ℝ, ℂ) for the field ℂ viewed as a real algebra) — so finite products of ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) functions are built by routing through ContDiffAt ℝ in a fixed chart (RS.contMDiffAt_real_iff_contDiffAt) and mathlib's generic contDiffAt_prod (valid for any normed ring), then bridging back.

theorem RS.AbelWeak.contMDiffAt_finsetProd_real {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} {t : Finset ι} {f : ι → X → ℂ} {x : X} (h : ∀ i ∈ t, ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) (f i) x) : ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) (fun (z : X) => ∏ i ∈ t, f i z) x

Finite pointwise products of ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) ∞ functions are again ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) ∞ (Compat: no ContMDiffMul 𝓘(ℝ, ℂ) ∞ ℂ instance is registered, so this routes through ContDiffAt ℝ in the chart extChartAt 𝓘(ℂ) x).

theorem RS.AbelWeak.contMDiffOn_finsetProd_real {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} {t : Finset ι} {f : ι → X → ℂ} {s : Set X} (hs : IsOpen s) (h : ∀ i ∈ t, ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) (f i) s) : ContMDiffOn (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) (fun (z : X) => ∏ i ∈ t, f i z) s

ContMDiffOn companion of contMDiffAt_finsetProd_real, for an OPEN set s (the only case needed here: s is always a finite-set complement, open since X is T2Space).

theorem RS.AbelWeak.contDiffAt_comp_symm_of_contMDiffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {h : X → ℂ} {a : X} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (ha : a ∈ e.source) (hh : ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) h a) : ContDiffAt ℝ (↑⊤) (h ∘ ↑e.symm) (↑e a)

Compat bridge: composing a ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) ∞ function h with the inverse of ANY maximal-atlas chart e at a gives a ContDiffAt ℝ ∞ planar function at e a (needed for IsWeakSolutionAt.mul_of_contMDiffAt, which must reuse the existing witness chart of its IsWeakSolutionAt argument rather than switch to extChartAt).

theorem RS.AbelWeak.contMDiffAt_comp_of_contDiffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {g : ℂ → ℂ} {x : X} {e : OpenPartialHomeomorph X ℂ} (he : e ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (hx : x ∈ e.source) (hg : ContDiffAt ℝ (↑⊤) g (↑e x)) : ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) (g ∘ ↑e) x

Compat bridge, the converse direction: a planar ContDiffAt ℝ ∞ function g composed with ANY maximal-atlas chart e (at a point x ∈ e.source) is ContMDiffAt 𝓘(ℝ, ℂ) 𝓘(ℝ, ℂ) ∞ as a function on X (needed by SingleChart.lean's construction, which builds its weak solution's local formula directly in a ChartChain-supplied chart e, not extChartAt).

Multiplicativity (Forster's Lemma 20.1)

theorem RS.AbelWeak.IsWeakSolutionAt.mul_of_contMDiffAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f h : X → ℂ} {a : X} {k : ℤ} (hf : IsWeakSolutionAt f a k) (hh : ContMDiffAt (modelWithCornersSelf ℝ ℂ) (modelWithCornersSelf ℝ ℂ) (↑⊤) h a) (hha : h a ≠ 0) : IsWeakSolutionAt (fun (x : X) => f x * h x) a k

The core multiplicativity step: multiplying a weak solution at a by a smooth, non-vanishing (at a) cofactor h preserves the local model (same order k, same witness chart).

theorem RS.AbelWeak.isWeakSolutionOfFinset_prod {X : Type u_1} [TopologicalSpace X] [T2Space X] [ChartedSpace ℂ X] [IsManifold (modelWithCornersSelf ℂ ℂ) ⊤ X] {ι : Type u_2} [Fintype ι] {f : ι → X → ℂ} {a x : ι → X} (ha : Function.Injective a) (hx : Function.Injective x) (hax : ∀ (i j : ι), a i ≠ x j) (hf : ∀ (i : ι), IsWeakSolutionOfPair (f i) (x i) (a i)) : IsWeakSolutionOfFinset (fun (z : X) => ∏ i : ι, f i z) a x

Forster's Lemma 20.1, k-point/Finset-indexed form (the abel-theorem scope addition): the pointwise product of k pairwise-disjoint two-point weak solutions is a weak solution of the whole k-point configuration.