Uniqueness in analytic Weierstrass division

This file proves germ-level uniqueness of the analytic quotient and the finite-degree remainder coefficients.

theorem LocalComplexGeometry.WPTBridge.eval_preparedTailSeq_physical {n d : ℕ} (r : NNReal) (b : Fin d → ClassicalComplexWPT.Base n → ℂ) (z : ClassicalComplexWPT.Base n) {w : ℂ} (hw : ‖w‖ < 1) : ClassicalComplexWPT.evalL1PowerSeries (ClassicalComplexWPT.preparedTailSeq r d b z) w = (↑↑r ^ d)⁻¹ * ∑ i : Fin d, b i z * (↑↑r * w) ^ ↑i

Evaluation of a normalized finite prepared tail in physical coordinates.

theorem LocalComplexGeometry.WPTBridge.eval_sequenceProduct_preparedPolynomial {n d : ℕ} (r : NNReal) (hr0 : 0 < r) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (z : ClassicalComplexWPT.Base n) (q : ↥ClassicalComplexWPT.L1Sequence) {w : ℂ} (hw : ‖w‖ < 1) : ClassicalComplexWPT.evalL1PowerSeries (ClassicalComplexWPT.seqLowShift d q + ClassicalComplexWPT.convolution q (ClassicalComplexWPT.preparedTailSeq r d a z)) w = ClassicalComplexWPT.evalL1PowerSeries q w * (↑↑r ^ d)⁻¹ * ClassicalComplexWPT.preparedPolynomial d a (z, ↑↑r * w)

Evaluation of a quotient sequence times the normalized prepared divisor.

theorem LocalComplexGeometry.WPTBridge.analyticWeierstrassDivision_unique {n d : ℕ} (h q q' : ClassicalComplexWPT.Ambient n → ℂ) (remainder remainder' a : Fin d → ClassicalComplexWPT.Base n → ℂ) (hq : AnalyticAt ℂ q 0) (hq' : AnalyticAt ℂ q' 0) (hremainder : ∀ (i : Fin d), AnalyticAt ℂ (remainder i) 0) (hremainder' : ∀ (i : Fin d), AnalyticAt ℂ (remainder' i) 0) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (hfactor : h =ᶠ[nhds 0] fun (x : ClassicalComplexWPT.Ambient n) => q x * ClassicalComplexWPT.preparedPolynomial d a x + ∑ i : Fin d, remainder i x.1 * x.2 ^ ↑i) (hfactor' : h =ᶠ[nhds 0] fun (x : ClassicalComplexWPT.Ambient n) => q' x * ClassicalComplexWPT.preparedPolynomial d a x + ∑ i : Fin d, remainder' i x.1 * x.2 ^ ↑i) : q =ᶠ[nhds 0] q' ∧ ∀ (i : Fin d), remainder i =ᶠ[nhds 0] remainder' i

Function-germ uniqueness in analytic Weierstrass division: two analytic quotients and analytic degree-< d remainders representing the same germ have the same quotient germ and the same coefficient germs.