Analytic Weierstrass division

This file reconstructs function-level analytic quotients and polynomial remainders from the sequence-level division operators.

noncomputable def LocalComplexGeometry.WPTBridge.analyticDivisionQuotient {n d : ℕ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (r : NNReal) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (x : ClassicalComplexWPT.Ambient n) : ℂ

The analytic quotient reconstructed in the original distinguished variable.

Equations

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

noncomputable def LocalComplexGeometry.WPTBridge.analyticDivisionRemainderCoefficient {n d : ℕ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (r : NNReal) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (i : Fin d) (z : ClassicalComplexWPT.Base n) : ℂ

The i-th remainder coefficient, rescaled back to the original variable.

Equations

• LocalComplexGeometry.WPTBridge.analyticDivisionRemainderCoefficient p r a i z = ↑(LocalComplexGeometry.WPTBridge.DivisionCore.remainderSeq p r a z) ↑i * (↑↑r)⁻¹ ^ ↑i

theorem LocalComplexGeometry.WPTBridge.analyticAt_analyticDivisionQuotient {n d : ℕ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (r : NNReal) (hrp : ↑r < p.radius) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : AnalyticAt ℂ (analyticDivisionQuotient p r a) 0

theorem LocalComplexGeometry.WPTBridge.analyticAt_analyticDivisionRemainderCoefficient {n d : ℕ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (r : NNReal) (hrp : ↑r < p.radius) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) (i : Fin d) : AnalyticAt ℂ (analyticDivisionRemainderCoefficient p r a i) 0

theorem LocalComplexGeometry.WPTBridge.analyticDivision_pointwise {n d : ℕ} {h : ClassicalComplexWPT.Ambient n → ℂ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (r : NNReal) (hr0 : 0 < r) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (z : ClassicalComplexWPT.Base n) (w : ℂ) (hsmall : ‖ClassicalComplexWPT.preparedTailSeq r d a z‖ < 1) (hw : ‖(↑↑r)⁻¹ * w‖ < 1) (hreconstruct : ClassicalComplexWPT.evalL1PowerSeries ((ClassicalComplexWPT.weightedCoefficientSeries p r).sum z) ((↑↑r)⁻¹ * w) = h (z, w)) : h (z, w) = analyticDivisionQuotient p r a (z, w) * ClassicalComplexWPT.preparedPolynomial d a (z, w) + ∑ i : Fin d, analyticDivisionRemainderCoefficient p r a i z * w ^ ↑i

theorem LocalComplexGeometry.WPTBridge.analyticWeierstrassDivision_fixedRadius {n d : ℕ} {h : ClassicalComplexWPT.Ambient n → ℂ} (p : FormalMultilinearSeries ℂ (ClassicalComplexWPT.Ambient n) ℂ) (hp : HasFPowerSeriesAt h p 0) (r : NNReal) (hr0 : 0 < r) (hrp : ↑r < p.radius) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : AnalyticAt ℂ (analyticDivisionQuotient p r a) 0 ∧ (∀ (i : Fin d), AnalyticAt ℂ (analyticDivisionRemainderCoefficient p r a i) 0) ∧ h =ᶠ[nhds 0] fun (x : ClassicalComplexWPT.Ambient n) => analyticDivisionQuotient p r a x * ClassicalComplexWPT.preparedPolynomial d a x + ∑ i : Fin d, analyticDivisionRemainderCoefficient p r a i x.1 * x.2 ^ ↑i

Fixed-radius analytic Weierstrass division by a prepared polynomial. The radius and ambient power-series witness remain explicit so downstream germ bridges can reuse the constructed quotient and remainder functions.

theorem LocalComplexGeometry.WPTBridge.exists_analyticWeierstrassDivision {n d : ℕ} (h : ClassicalComplexWPT.Ambient n → ℂ) (hh : AnalyticAt ℂ h 0) (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) (ha0 : ∀ (i : Fin d), a i 0 = 0) : ∃ (q : ClassicalComplexWPT.Ambient n → ℂ) (remainder : Fin d → ClassicalComplexWPT.Base n → ℂ), AnalyticAt ℂ q 0 ∧ (∀ (i : Fin d), AnalyticAt ℂ (remainder i) 0) ∧ 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

Arbitrary-dividend analytic Weierstrass division. This is the function-level adapter missing from the pinned WPT public surface: it returns an analytic quotient and analytic coefficients of a remainder of distinguished degree strictly below d.