Slice orders from Laurent unit forms

An analytic function agreeing with a fixed Laurent power times an analytic unit off a coordinate hyperplane has locally constant slice order on that hyperplane. The Laurent representation is allowed to use an integer exponent; analyticity forces that exponent to be nonnegative. This lets finite extensions of meromorphic root branches retain their contact orders after poles have been removed from other branches.

theorem AnalyticAt.eventually_analyticOrderAt_eq_of_zpow_smul_unit {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [NontriviallyNormedField 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {G w : E × 𝕜 → F} {x₀ : E} {y₀ : 𝕜} {b : ℤ} (hG : AnalyticAt 𝕜 G (x₀, y₀)) (hw : AnalyticAt 𝕜 w (x₀, y₀)) (hw0 : w (x₀, y₀) ≠ 0) (heq : ∀ᶠ (p : E × 𝕜) in nhds (x₀, y₀), p.2 ≠ y₀ → G p = (p.2 - y₀) ^ b • w p) : ∀ᶠ (x : E) in nhds x₀, analyticOrderAt (fun (y : 𝕜) => G (x, y)) y₀ = analyticOrderAt (fun (y : 𝕜) => G (x₀, y)) y₀

A fixed Laurent unit form off a coordinate hyperplane makes the slice order of an analytic function with complete codomain locally constant on the hyperplane. The equality need not be supplied on the hyperplane itself.