Rechart: IsWeakSolutionAt is chart-independent, and general order-additive multiplication

Unit: abel-weak-solutions, closing the gap recorded in this unit's own root docstring and in docs/design/abel-theorem.md §1.4/§4.1 (task: authorized edit inside Jacobian/AbelWeak/). The missing piece for the general multi-chart exists_weakSolutionOfPair was a "rechart" lemma: IsWeakSolutionAt's local model, witnessed in one maximalAtlas chart, can be re-witnessed in ANY OTHER maximalAtlas chart at the same point, via mathlib's removable-singularity theorem applied to the transition map's divided difference (dslope). This file builds that lemma (exists_localModel_of_isWeakSolutionAt) and its main consumer, a fully general order-additive multiplication (IsWeakSolutionAt.mul): combining IsWeakSolutionAt f a k1 and IsWeakSolutionAt g a k2 (witnessed in POSSIBLY DIFFERENT charts) gives a function h, equal to f * g everywhere except possibly at a itself, with IsWeakSolutionAt h a (k1 + k2).

The junk-value subtlety (why h cannot always literally be f * g): IsWeakSolutionAt's local model is a FULL-neighbourhood equality f =ᶠ[𝓝 a] fun x => ψ (e x) * (e x - e a) ^ k, which pins down the actual value of f at a itself via the zpow-at-zero junk convention (0 ^ k = 0 for k ≠ 0, 0 ^ 0 = 1). For k1, k2 both nonzero with k1 + k2 = 0 (the "cancellation" case genuinely needed by the chain induction: a +1-order zero of one piece meeting a -1-order pole of the next), (f * g) a = f a * g a = 0 * 0 = 0 (both individual junk values), but the model at order 0 demands the value at a be ψ (e a) * φ (e a) ≠ 0 (the correct removable-singularity limit). So f * g and the desired weak solution of order k1 + k2 genuinely disagree AT a in this case; Function.update at the single point a repairs this, uniformly for every k1, k2 (no case split needed: Function.update's value ψ (e a) * φ (e a) * (0 : ℂ) ^ (k1 + k2) matches BOTH the cancelling case, = ψ (e a) * φ (e a) when k1 + k2 = 0, AND the generic case, = 0, matching what the naive product already gives).

A planar helper: ContDiffAt of a fixed integer power of a nonvanishing function

The rechart lemma

theorem RS.AbelWeak.exists_localModel_of_isWeakSolutionAt {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f : X → ℂ} {a : X} {k : ℤ} (hf : IsWeakSolutionAt f a k) {e' : OpenPartialHomeomorph X ℂ} (he' : e' ∈ IsManifold.maximalAtlas (modelWithCornersSelf ℂ ℂ) ⊤ X) (ha' : a ∈ e'.source) : ∃ (ψ' : ℂ → ℂ), (∀ᶠ (z : ℂ) in nhds (↑e' a), ψ' z ≠ 0) ∧ ContDiffAt ℝ (↑⊤) ψ' (↑e' a) ∧ f =ᶠ[nhds a] fun (x : X) => ψ' (↑e' x) * (↑e' x - ↑e' a) ^ k

The rechart lemma: IsWeakSolutionAt f a k's local model, witnessed by SOME chart e, is also witnessed by ANY OTHER maximalAtlas chart e' at a. Proof: the transition map S := e ∘ e'.symm is holomorphic (chart compatibility) hence AnalyticAt; its "divided difference" H := dslope S (e' a) is AnalyticAt too (HasFPowerSeriesAt. has_fpower_series_dslope_fslope), agrees with S's derivative at e' a (dslope_same), and that derivative is NONZERO because S has a two-sided holomorphic inverse (the reverse transition T), so T ∘ S = id near e' a forces (deriv T (S (e' a))) * (deriv S (e' a)) = 1 by the chain rule. The unconditional identity sub_smul_dslope ((b - a) • dslope f a b = f b - f a, no case split on b = a) then gives the exact factorisation e x - e a = (e' x - e' a) * H (e' x) needed to rewrite the local model.

General order-additive multiplication

theorem RS.AbelWeak.IsWeakSolutionAt.mul {X : Type u_1} [TopologicalSpace X] [ChartedSpace ℂ X] {f g : X → ℂ} {a : X} {k1 k2 : ℤ} (hf : IsWeakSolutionAt f a k1) (hg : IsWeakSolutionAt g a k2) : ∃ (h : X → ℂ), IsWeakSolutionAt h a (k1 + k2) ∧ ∀ (x : X), x ≠ a → h x = f x * g x

General order-additive multiplication (subsumes IsWeakSolutionAt.mul_of_contMDiffAt's k2 = 0 case, and the "opposite order cancellation" the general chain induction needs at every interior breakpoint): given IsWeakSolutionAt f a k1 and IsWeakSolutionAt g a k2 (witnessed by POSSIBLY DIFFERENT charts, aligned here via exists_localModel_of_isWeakSolutionAt), there is a function h, equal to f * g everywhere EXCEPT possibly at a (see the file docstring for why a needs a genuine Function.update, not the naive product), with IsWeakSolutionAt h a (k1 + k2).