Local equations of an affine hyperplane along an analytic curve

Let ℓ be a continuous linear functional on a normed space E, and γ an analytic curve passing at w through a point p of the affine hyperplane ℓ = b. Any function H analytic at p with nonzero differential at p, vanishing on the hyperplane near p, is a local equation of the hyperplane in the same sense as ℓ - b, and the two equations meet γ to the same order: H ∘ γ and ℓ ∘ γ - b have the same order of vanishing at w (AnalyticAt.analyticOrderAt_comp_eq_analyticOrderAt_sub).

The first step is that a function vanishing on the hyperplane near p has differential at p vanishing on its direction ker ℓ (DifferentiableAt.fderiv_apply_eq_zero_of_eventually_eq_zero).

This is what makes the intersection order of a holomorphic curve with a smooth complex hypersurface independent of the coordinates in which it is computed: after a change of analytic coordinates an affine equation of the hypersurface becomes a nonlinear one, still with nonzero differential.

Implementation notes

The proof compares the two functions directly. Writing γ t = q t + g t • v, where g = ℓ ∘ γ - b, ℓ v = 1 and q t lies on the hyperplane, strict differentiability of H at p gives H (γ t) = H (γ t) - H (q t) = c * g t + o (g t) with c = DH(p) v. Since DH(p) vanishes on the kernel of ℓ but not identically, c ≠ 0, so H ∘ γ and g are equivalent up to constant factors and have the same order (AnalyticAt.analyticOrderAt_eq_of_isTheta).

theorem DifferentiableAt.fderiv_apply_eq_zero_of_eventually_eq_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_3} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {H : E → F} {ℓ : E →L[𝕜] 𝕜} {b : 𝕜} {p : E} (hH : DifferentiableAt 𝕜 H p) (hp : ℓ p = b) (hzero : ∀ᶠ (x : E) in nhds p, ℓ x = b → H x = 0) {u : E} (hu : ℓ u = 0) : (fderiv 𝕜 H p) u = 0

A function differentiable at a point p of an affine hyperplane ℓ = b and vanishing on the hyperplane near p has differential at p vanishing on the kernel of ℓ, the direction of the hyperplane.

theorem AnalyticAt.analyticOrderAt_comp_eq_analyticOrderAt_sub {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {H : E → 𝕜} {γ : 𝕜 → E} {ℓ : E →L[𝕜] 𝕜} {b w : 𝕜} (hH : AnalyticAt 𝕜 H (γ w)) (hH' : fderiv 𝕜 H (γ w) ≠ 0) (hγ : AnalyticAt 𝕜 γ w) (hw : ℓ (γ w) = b) (hzero : ∀ᶠ (x : E) in nhds (γ w), ℓ x = b → H x = 0) : analyticOrderAt (fun (t : 𝕜) => H (γ t)) w = analyticOrderAt (fun (t : 𝕜) => ℓ (γ t) - b) w

Two local equations of an affine hyperplane meet an analytic curve to the same order. Let γ be analytic at w with γ w on the hyperplane ℓ = b, and let H be analytic at γ w with nonzero differential there and vanishing on the hyperplane near γ w. Then H ∘ γ and ℓ ∘ γ - b have the same order of vanishing at w.