Ambient polynomial order along analytic curves

An analytic curve through a point cannot lower the ambient order of a polynomial. Together with a line detecting that order, this compares ambient orders under analytic coordinate substitutions and multiplication by an analytic function. These comparisons allow polynomial order to be transported through local coordinate changes, even when the coordinate change itself is not polynomial.

theorem MvPolynomial.orderAt_le_analyticOrderAt_eval {𝕜 : Type u_1} {σ : Type u_2} [NontriviallyNormedField 𝕜] (p : MvPolynomial σ 𝕜) {γ : 𝕜 → σ → 𝕜} {t₀ : 𝕜} (hγ : ∀ (i : σ), AnalyticAt 𝕜 (fun (t : 𝕜) => γ t i) t₀) : p.orderAt (γ t₀) ≤ analyticOrderAt (fun (t : 𝕜) => (eval (γ t)) p) t₀

Evaluation along a coordinatewise analytic curve does not decrease ambient order. The index type need not be finite: each polynomial uses only finitely many coordinates.

theorem MvPolynomial.orderAt_le_of_analyticAt_mul_eq {𝕜 : Type u_1} {σ : Type u_2} {τ : Type u_3} [NontriviallyNormedField 𝕜] [Fintype σ] (p : MvPolynomial τ 𝕜) (q : MvPolynomial σ 𝕜) (a : σ → 𝕜) {g : (σ → 𝕜) → τ → 𝕜} {u : (σ → 𝕜) → 𝕜} (hg : ∀ (i : τ), AnalyticAt 𝕜 (fun (x : σ → 𝕜) => g x i) a) (hu : AnalyticAt 𝕜 u a) (heq : ∀ᶠ (x : σ → 𝕜) in nhds a, (eval (g x)) p * u x = (eval x) q) : p.orderAt (g a) ≤ q.orderAt a

An analytic substitution and multiplication by an analytic function cannot lower ambient polynomial order. The identity is required only near the comparison point.

theorem MvPolynomial.orderAt_le_of_eval_cons_mul_mul_eq {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {n : ℕ} (f g : MvPolynomial (Fin (n + 1)) 𝕜) {l μ : (Fin n → 𝕜) → 𝕜} {a : Fin n → 𝕜} (z : 𝕜) (hl : AnalyticAt 𝕜 l a) (hμ : AnalyticAt 𝕜 μ a) (h : ∀ᶠ (y : Fin n → 𝕜) in nhds a, ∀ (t : 𝕜), (eval (Fin.cons (l y * t) y)) f * μ y = (eval (Fin.cons t y)) g) : f.orderAt (Fin.cons (l a * z) a) ≤ g.orderAt (Fin.cons z a)

Rescaling the distinguished coordinate by an analytic factor, together with multiplication by an analytic function, cannot lower ambient order. The identity is required only for base points near a.