The real analytic Weierstrass preparation and division theorems

Let f : (ι → ℝ) × ℝ → ℝ be real analytic at (x₀, t₀), with ι finite, and suppose that the vertical slice t ↦ f (x₀, t) vanishes to finite order d at t₀. Then near (x₀, t₀), f (x, t) = P_x (t - t₀) * u (x, t), where P_x is the monic polynomial of degree d whose lower coefficients are real analytic functions of x vanishing at x₀, and u is real analytic and nonvanishing at (x₀, t₀) (AnalyticAt.exists_weierstrassPreparation_real). Any real analytic g can be divided by such a real Weierstrass polynomial P_x, with a real analytic quotient and a remainder of degree less than d in t - t₀ whose coefficients are real analytic in x (AnalyticAt.exists_weierstrassDivision_monicOfCoeff_real). The polynomials are written with TauCeti.Polynomial.monicOfCoeff, exactly as in the complex theorems AnalyticAt.exists_weierstrassPreparation and AnalyticAt.exists_weierstrassDivision_monicOfCoeff.

The real theorems are deduced from the complex ones. A holomorphic extension of f commuting with complex conjugation has a complex Weierstrass preparation. Conjugating that factorization gives a second one, so by uniqueness of the preparation (TauCeti.eventuallyEq_of_weierstrassPreparation) the coefficients and the unit commute with conjugation near the real point (TauCeti.eventually_apply_star_of_weierstrassPreparation). In particular they are real at real points, and their restrictions to the real points form the real preparation. The complex slice has order d because the order of a holomorphic function at a real point can be computed on the real line (AnalyticAt.analyticOrderAt_comp_ofReal). Division is handled in the same way, using uniqueness of the Weierstrass division (TauCeti.eventuallyEq_of_weierstrassDivision, TauCeti.eventually_apply_star_of_weierstrassDivision).

Real Weierstrass polynomials are the starting point of the local analysis of real analytic functions: their discriminants and subresultants control the real roots, as in Łojasiewicz's proof of the local structure of semianalytic sets.

Main results

• TauCeti.eventually_apply_star_of_weierstrassPreparation, TauCeti.eventually_apply_star_of_weierstrassDivision: the coefficients, unit, quotient and remainder of a Weierstrass preparation or division of holomorphic functions commuting with conjugation themselves commute with conjugation near a real point.
• AnalyticAt.exists_weierstrassPreparation_real: real analytic Weierstrass preparation.
• AnalyticAt.exists_weierstrassDivision_monicOfCoeff_real: real analytic Weierstrass division by a real Weierstrass polynomial.

References

• S. Łojasiewicz, Introduction to Complex Analytic Geometry, Birkhäuser, 1991.
• S. G. Krantz, H. R. Parks, A Primer of Real Analytic Functions, second edition, Birkhäuser, 2002, Section 6.1.

theorem TauCeti.eventually_apply_star_of_weierstrassPreparation {E : Type} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [StarAddMonoid E] [StarModule ℂ E] [ContinuousStar E] {f : E × ℂ → ℂ} {x₀ : E} {w₀ : ℂ} {d : ℕ} {c : Fin d → E → ℂ} {u : E × ℂ → ℂ} (hx₀ : star x₀ = x₀) (hw₀ : star w₀ = w₀) (hf : ∀ᶠ (p : E × ℂ) in nhds (x₀, w₀), f (star p) = star (f p)) (hc : ∀ (i : Fin d), AnalyticAt ℂ (c i) x₀) (hc0 : ∀ (i : Fin d), c i x₀ = 0) (hu : AnalyticAt ℂ u (x₀, w₀)) (hu0 : u (x₀, w₀) ≠ 0) (hfac : f =ᶠ[nhds (x₀, w₀)] fun (p : E × ℂ) => Polynomial.eval (p.2 - w₀) (Polynomial.monicOfCoeff fun (i : Fin d) => c i p.1) * u p) : (∀ (i : Fin d), ∀ᶠ (x : E) in nhds x₀, c i (star x) = star (c i x)) ∧ ∀ᶠ (p : E × ℂ) in nhds (x₀, w₀), u (star p) = star (u p)

Conjugation symmetry of the Weierstrass preparation. Let f commute with conjugation near a point (x₀, w₀) fixed by conjugation, and let f (x, w) = P_x (w - w₀) * u (x, w) be a Weierstrass preparation of f there. Then the coefficients of P_x and the unit u commute with conjugation near x₀ and (x₀, w₀); in particular they are real at real points near x₀ and (x₀, w₀).

theorem TauCeti.eventually_apply_star_of_weierstrassDivision {E : Type} [NormedAddCommGroup E] [NormedSpace ℂ E] [FiniteDimensional ℂ E] [StarAddMonoid E] [StarModule ℂ E] [ContinuousStar E] {g : E × ℂ → ℂ} {x₀ : E} {w₀ : ℂ} {d : ℕ} {c : Fin d → E → ℂ} {q : E × ℂ → ℂ} {r : Fin d → E → ℂ} (hx₀ : star x₀ = x₀) (hw₀ : star w₀ = w₀) (hc : ∀ (i : Fin d), AnalyticAt ℂ (c i) x₀) (hc0 : ∀ (i : Fin d), c i x₀ = 0) (hcstar : ∀ (i : Fin d), ∀ᶠ (x : E) in nhds x₀, c i (star x) = star (c i x)) (hg : ∀ᶠ (p : E × ℂ) in nhds (x₀, w₀), g (star p) = star (g p)) (hq : AnalyticAt ℂ q (x₀, w₀)) (hr : ∀ (i : Fin d), AnalyticAt ℂ (r i) x₀) (hdiv : g =ᶠ[nhds (x₀, w₀)] fun (p : E × ℂ) => Polynomial.eval (p.2 - w₀) (Polynomial.monicOfCoeff fun (i : Fin d) => c i p.1) * q p + ∑ i : Fin d, r i p.1 * (p.2 - w₀) ^ ↑i) : (∀ᶠ (p : E × ℂ) in nhds (x₀, w₀), q (star p) = star (q p)) ∧ ∀ (i : Fin d), ∀ᶠ (x : E) in nhds x₀, r i (star x) = star (r i x)

Conjugation symmetry of the Weierstrass division. Let g and the coefficients c i commute with conjugation near a point (x₀, w₀) fixed by conjugation, and let g (x, w) = P_x (w - w₀) * q (x, w) + ∑ i, r i x * (w - w₀) ^ i be a Weierstrass division of g by the Weierstrass polynomial P_x with coefficients c i x. Then the quotient q and the remainder coefficients r i commute with conjugation near (x₀, w₀) and x₀.

theorem AnalyticAt.exists_weierstrassPreparation_real {ι : Type} [Fintype ι] {f : (ι → ℝ) × ℝ → ℝ} {x₀ : ι → ℝ} {t₀ : ℝ} {d : ℕ} (hf : AnalyticAt ℝ f (x₀, t₀)) (hd : analyticOrderAt (fun (t : ℝ) => f (x₀, t)) t₀ = ↑d) : ∃ (c : Fin d → (ι → ℝ) → ℝ) (u : (ι → ℝ) × ℝ → ℝ), (∀ (i : Fin d), AnalyticAt ℝ (c i) x₀) ∧ (∀ (i : Fin d), c i x₀ = 0) ∧ AnalyticAt ℝ u (x₀, t₀) ∧ u (x₀, t₀) ≠ 0 ∧ f =ᶠ[nhds (x₀, t₀)] fun (p : (ι → ℝ) × ℝ) => Polynomial.eval (p.2 - t₀) (TauCeti.Polynomial.monicOfCoeff fun (i : Fin d) => c i p.1) * u p

Real analytic Weierstrass preparation theorem. Let f : (ι → ℝ) × ℝ → ℝ be real analytic at (x₀, t₀), with ι finite, and suppose the vertical slice t ↦ f (x₀, t) has finite order of vanishing d at t₀. Then there exist real analytic coefficient functions c : Fin d → (ι → ℝ) → ℝ vanishing at x₀ and a real analytic function u nonvanishing at (x₀, t₀) such that near (x₀, t₀), f (x, t) = (TauCeti.Polynomial.monicOfCoeff (fun i ↦ c i x)).eval (t - t₀) * u (x, t).

theorem AnalyticAt.exists_weierstrassDivision_monicOfCoeff_real {ι : Type} [Fintype ι] {d : ℕ} {c : Fin d → (ι → ℝ) → ℝ} {g : (ι → ℝ) × ℝ → ℝ} {x₀ : ι → ℝ} {t₀ : ℝ} (hg : AnalyticAt ℝ g (x₀, t₀)) (hc : ∀ (i : Fin d), AnalyticAt ℝ (c i) x₀) (hc0 : ∀ (i : Fin d), c i x₀ = 0) : ∃ (q : (ι → ℝ) × ℝ → ℝ) (r : Fin d → (ι → ℝ) → ℝ), AnalyticAt ℝ q (x₀, t₀) ∧ (∀ (i : Fin d), AnalyticAt ℝ (r i) x₀) ∧ g =ᶠ[nhds (x₀, t₀)] fun (p : (ι → ℝ) × ℝ) => Polynomial.eval (p.2 - t₀) (TauCeti.Polynomial.monicOfCoeff fun (i : Fin d) => c i p.1) * q p + ∑ i : Fin d, r i p.1 * (p.2 - t₀) ^ ↑i

Real analytic Weierstrass division by a Weierstrass polynomial. Let c : Fin d → (ι → ℝ) → ℝ be real analytic at x₀ with c i x₀ = 0, with ι finite, and let g : (ι → ℝ) × ℝ → ℝ be real analytic at (x₀, t₀). Then there exist q real analytic at (x₀, t₀) and r : Fin d → (ι → ℝ) → ℝ real analytic at x₀ such that near (x₀, t₀), g (x, t) = (TauCeti.Polynomial.monicOfCoeff (fun i ↦ c i x)).eval (t - t₀) * q (x, t) + ∑ i : Fin d, r i x * (t - t₀) ^ (i : ℕ).