Exact order in the distinguished variable

This file connects the public derivative-based order condition to elementary properties of the distinguished-variable slice. The deeper comparison with analytic order is developed separately from these edge-case lemmas.

theorem ClassicalComplexWPT.analyticAt_lastSlice {n : ℕ} {f : Ambient n → ℂ} (hf : AnalyticAt ℂ f 0) : AnalyticAt ℂ (lastSlice f) 0

Restricting an analytic germ to the distinguished-variable axis preserves analyticity.

theorem ClassicalComplexWPT.exactOrderInLastVariable_zero_iff {n : ℕ} {f : Ambient n → ℂ} : ExactOrderInLastVariable f 0 ↔ f 0 ≠ 0

Exact order zero is exactly nonvanishing at the origin.

theorem ClassicalComplexWPT.exactOrderInLastVariable_iff_analyticOrderAt {n d : ℕ} {f : Ambient n → ℂ} (hf : AnalyticAt ℂ f 0) : ExactOrderInLastVariable f d ↔ analyticOrderAt (lastSlice f) 0 = ↑d

For an analytic germ, the public derivative condition agrees with Mathlib's analytic order.

theorem ClassicalComplexWPT.exists_lastSlice_eq_pow_mul {n d : ℕ} {f : Ambient n → ℂ} (hf : AnalyticAt ℂ f 0) (horder : ExactOrderInLastVariable f d) : ∃ (g : ℂ → ℂ), AnalyticAt ℂ g 0 ∧ g 0 ≠ 0 ∧ lastSlice f =ᶠ[nhds 0] fun (w : ℂ) => w ^ d * g w

The exact-order hypothesis supplies the normalized one-variable axis factorization.