Concrete polynomial representatives

This file relates the generic fixed-degree representative API to the two polynomial shapes occurring in Weierstrass division and records independence of an inessential larger degree bound.

theorem LocalComplexGeometry.eventually_germPolynomialRepresentativeAt_C {n m : ℕ} (f : ↥(HolomorphicGerm n)) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, germPolynomialRepresentativeAt m (Polynomial.C f) z = Polynomial.C (HolomorphicGerm.representative f z)

A constant germ polynomial specializes to the constant polynomial of its chosen representative, independently of the displayed bound.

@[simp]

theorem LocalComplexGeometry.preparedGermPolynomial_natDegree {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) : (preparedGermPolynomial a ha).natDegree = d

The prepared germ polynomial has exact natural degree d.

theorem LocalComplexGeometry.eventually_germPolynomialRepresentativeAt_preparedGermPolynomial {n d : ℕ} (a : Fin d → ClassicalComplexWPT.Base n → ℂ) (ha : ∀ (i : Fin d), AnalyticAt ℂ (a i) 0) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, germPolynomialRepresentativeAt d (preparedGermPolynomial a ha) z = preparedPolynomialAt a z

Chosen coefficient representatives of the prepared germ polynomial specialize to the original prepared polynomial family after shrinking.

theorem LocalComplexGeometry.remainderGermPolynomial_natDegree_le {n d : ℕ} (r : Fin d → ↥(HolomorphicGerm n)) : (remainderGermPolynomial r).natDegree ≤ d

A degree-< d remainder germ polynomial has natural degree at most d.

theorem LocalComplexGeometry.eventually_germPolynomialRepresentativeAt_remainderGermPolynomial {n d : ℕ} (r : Fin d → ↥(HolomorphicGerm n)) : ∀ᶠ (z : ComplexEuclidean n) in nhds 0, germPolynomialRepresentativeAt d (remainderGermPolynomial r) z = remainderPolynomialAt (HolomorphicGerm.coefficientRepresentatives r) z

Chosen representatives of a remainder germ polynomial specialize to the usual displayed coefficient sum.