Documentation

TauCeti.Analysis.Polynomial.Puiseux.Lazard

Puiseux Laurent branches along Lazard monomial deformations #

Let a real polynomial in a distinguished variable have leading coefficient, constant coefficient, and formal discriminant with locally constant finite Lazard valuations along real analytic centers. A common evaluator gives monomial deformations of a complexification of the centers. Along these deformations, construct a complete distinct Puiseux splitting and analytic extensions of the branches after removing their poles. The Laurent exponents and nowhere-zero analytic units are global on the parameter product. Ordinary specialization at the centers may be nullified.

The evaluator can also separate any prescribed finite set of base exponents, so it can be chosen for the removed base exponents of the polynomial being lifted. The complex centers respect conjugation. The conclusion constructs the root labels; neither a splitting nor complex valuation constancy is assumed. Discriminants are compared with the formal coefficient polynomial only away from the exceptional hyperplane, where the leading coefficient guarantees preservation of degree.

The construction uses TauCeti.exists_complexification_isLazardEvaluator_analytic_units and TauCeti.Polynomial.exists_analyticOnNhd_nonmonic_laurent.

References #

source
theorem Polynomial.exists_complexification_isLazardEvaluator_nonmonic_laurent {σ : Type u_1} {ι : Type u_2} [LinearOrder σ] [Fintype σ] [Fintype ι] (p : Polynomial (MvPolynomial σ ℝ)) {φ : (ι → ℝ) → σ → ℝ} {a : ι → ℝ} (hφ : AnalyticAt ℝ φ a) (vLead vConst vDiscr : σ →₀ ℕ) (hlead : ∀ᶠ (x : ι → ℝ) in nhds a, p.leadingCoeff.lazardValuation (φ x) = ↑(toLex vLead)) (hconst : ∀ᶠ (x : ι → ℝ) in nhds a, (p.coeff 0).lazardValuation (φ x) = ↑(toLex vConst)) (hdiscr : ∀ᶠ (x : ι → ℝ) in nhds a, p.discr.lazardValuation (φ x) = ↑(toLex vDiscr)) {V : Set (σ →₀ ℕ)} (hV : V.Finite) :
∃ ρ > 0, ∃ (Φ : (ι → ℂ) → σ → ℂ) (c : σ → ℕ), TauCeti.IsLazardEvaluator ({vLead, vConst, vDiscr} ∪ V) c ∧ AnalyticOnNhd ℂ Φ (Metric.ball (fun (j : ι) => ↑(a j)) ρ) ∧ (∀ x ∈ Metric.ball a ρ, (Φ fun (j : ι) => ↑(x j)) = fun (i : σ) => ↑(φ x i)) ∧ (∀ (z : ι → ℂ), Φ (star z) = star (Φ z)) ∧ ∃ (u : (ι → ℂ) × ℂ → ℂ) (v : (ι → ℂ) × ℂ → ℂ), AnalyticOnNhd ℂ u (Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ Metric.ball 0 ρ) ∧ (∀ b ∈ Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ Metric.ball 0 ρ, u b ≠ 0 ∧ MvPolynomial.eval₂ Complex.ofRealHom (fun (j : σ) => Φ b.1 j + b.2 ^ c j) p.leadingCoeff = b.2 ^ (Finsupp.weight c) vLead * u b) ∧ AnalyticOnNhd ℂ v (Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ Metric.ball 0 ρ) ∧ (∀ b ∈ Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ Metric.ball 0 ρ, v b ≠ 0 ∧ MvPolynomial.eval₂ Complex.ofRealHom (fun (j : σ) => Φ b.1 j + b.2 ^ c j) p.discr = b.2 ^ (Finsupp.weight c) vDiscr * v b) ∧ ∃ R > 0, R ^ p.natDegree.factorial ≤ ρ ∧ ∃ (r : Fin p.natDegree → (ι → ℂ) × ℂ → ℂ) (g : Fin p.natDegree → (ι → ℂ) × ℂ → ℂ), (∀ (i : Fin p.natDegree), AnalyticOnNhd ℂ (r i) (Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ (Metric.ball 0 R \ {0}))) ∧ (∀ (i : Fin p.natDegree), AnalyticOnNhd ℂ (g i) (Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ Metric.ball 0 R) ∧ Set.EqOn (g i) (fun (b : (ι → ℂ) × ℂ) => b.2 ^ (p.natDegree.factorial * (Finsupp.weight c) vLead) * r i b) (Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ (Metric.ball 0 R \ {0}))) ∧ (∀ b ∈ Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ (Metric.ball 0 R \ {0}), (Function.Injective fun (i : Fin p.natDegree) => r i b) ∧ map (MvPolynomial.eval₂Hom Complex.ofRealHom fun (j : σ) => Φ b.1 j + b.2 ^ (p.natDegree.factorial * c j)) p = C (MvPolynomial.eval₂ Complex.ofRealHom (fun (j : σ) => Φ b.1 j + b.2 ^ (p.natDegree.factorial * c j)) p.leadingCoeff) * ∏ i : Fin p.natDegree, (X - C (r i b))) ∧ ∃ (e : Fin p.natDegree → ℤ) (w : Fin p.natDegree → (ι → ℂ) × ℂ → ℂ), (∀ (i : Fin p.natDegree), -(↑p.natDegree.factorial * ↑((Finsupp.weight c) vLead)) ≤ e i) ∧ (∀ (i : Fin p.natDegree), AnalyticOnNhd ℂ (w i) (Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ Metric.ball 0 R)) ∧ (∀ (i : Fin p.natDegree), ∀ b ∈ Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ Metric.ball 0 R, w i b ≠ 0) ∧ ∀ b ∈ Metric.ball (fun (j : ι) => ↑(a j)) ρ ×ˢ (Metric.ball 0 R \ {0}), ∀ (i : Fin p.natDegree), r i b = b.2 ^ e i * w i b

Locally constant finite Lazard valuations of the formal leading coefficient, constant coefficient, and discriminant along real analytic centers construct Puiseux Laurent branches of the monomial deformation. The centers have one conjugation-compatible complex extension, and the evaluator also separates the prescribed finite set V. After the factorial power substitution, the same distinct root labels have analytic pole-removed extensions and Laurent-power forms whose exponents are constant on the parameter ball and bounded below by the negative substituted leading-coefficient weight. Their analytic units are nowhere zero on the whole parameter product, including its distinguished hyperplane. The analytic leading-coefficient and formal-discriminant units are retained for the same deformation, before the factorial substitution. Nullified ordinary fibers are allowed; degree zero is included.