Linear changes of variables on Conv K n

Rückert's induction makes a series regular in a distinguished variable by a linear change of coordinates [GR65, Chapter II, §B]; the printed condition is "there are local coordinates … such that f_a(0, …, 0, x_m) ∼ x_m^e" [BM88, proof of Theorem 4.4, p. 24]. The generic linear change of Hironaka/Analytic/Germ/Axis.lean is a function-level statement (evalSeries f (L (Pi.single 0 t)) = t^d e(t)); this file supplies the series-level automorphism it induces. For a continuous linear L : K^n → K^n and f ∈ Conv K n, the function evalSeries f ∘ L is analytic at 0, so the expansion of an analytic function into a convergent series (Hironaka/Analytic/ConvSeries/Bridge.lean) gives it a coefficient family of finite majorant norm: substConv L f. Uniqueness of the coefficient family makes substConv L a K-algebra map (substHom L) and, for an invertible L, an automorphism (substEquiv L, inverse substHom L.symm). exists_substEquiv_isRegularIn is the generic linear change transported: every nonzero f ∈ Conv K (m+1) becomes x_0-regular of order ord f after some linear change. These substitutions are used throughout the Nullstellensatz and the parametrization theorem, and, on the stalks of an analytic space, throughout Hironaka/Space (the coherence theorem, the dimension theory, the regular components).

The coefficient field K is ℝ or ℂ ([RCLike K]).

theorem Analytic.analyticAt_evalSeries_zero {K : Type u_1} [RCLike K] {n : ℕ} {f : MvPowerSeries (Fin n) K} (hf : f ∈ Conv K n) : AnalyticAt K (evalSeries f) 0

The sum of a convergent series is analytic at 0.

theorem Analytic.analyticAt_evalSeries_comp {K : Type u_1} [RCLike K] {n : ℕ} {f : MvPowerSeries (Fin n) K} (hf : f ∈ Conv K n) (L : (Fin n → K) →L[K] Fin n → K) : AnalyticAt K (evalSeries f ∘ ⇑L) 0

A convergent series composed with a linear map is analytic at 0.

theorem Analytic.evalSeries_mul_eventually {K : Type u_1} [RCLike K] {n : ℕ} {f g : MvPowerSeries (Fin n) K} (hf : f ∈ Conv K n) (hg : g ∈ Conv K n) : evalSeries (f * g) =ᶠ[nhds 0] fun (x : Fin n → K) => evalSeries f x * evalSeries g x

Near 0, evalSeries of a product is the product.

theorem Analytic.evalSeries_add_eventually {K : Type u_1} [RCLike K] {n : ℕ} {f g : MvPowerSeries (Fin n) K} (hf : f ∈ Conv K n) (hg : g ∈ Conv K n) : evalSeries (f + g) =ᶠ[nhds 0] fun (x : Fin n → K) => evalSeries f x + evalSeries g x

Near 0, evalSeries of a sum is the sum.

theorem Analytic.evalSeries_C' {K : Type u_1} [RCLike K] {n : ℕ} (r : K) (x : Fin n → K) : evalSeries (MvPowerSeries.C r) x = r

theorem Analytic.Conv.ext_of_evalSeries_eventuallyEq {K : Type u_1} [RCLike K] {n : ℕ} {f g : ↥(Conv K n)} (h : evalSeries ↑f =ᶠ[nhds 0] evalSeries ↑g) : f = g

Two elements of Conv K n whose sums agree near 0 are equal (uniqueness of coefficients).

theorem Analytic.tendsto_clm_zero {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) →L[K] Fin n → K) : Filter.Tendsto (⇑L) (nhds 0) (nhds 0)

theorem Analytic.exists_substConv_spec {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) →L[K] Fin n → K) (f : ↥(Conv K n)) : ∃ (g : ↥(Conv K n)), evalSeries ↑g =ᶠ[nhds 0] evalSeries ↑f ∘ ⇑L

evalSeries f ∘ L is the sum of a convergent series near 0 (the expansion of an analytic function).

noncomputable def Analytic.substConv {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) →L[K] Fin n → K) (f : ↥(Conv K n)) : ↥(Conv K n)

The coefficient family at 0 of evalSeries f ∘ L, for f ∈ Conv K n and a continuous linear L: the series f(L x) (the change of coordinates of [GR65, Chapter II, §B]).

Equations

• Analytic.substConv L f = Classical.choose ⋯

theorem Analytic.evalSeries_substConv {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) →L[K] Fin n → K) (f : ↥(Conv K n)) : evalSeries ↑(substConv L f) =ᶠ[nhds 0] evalSeries ↑f ∘ ⇑L

The defining property of substConv: its sum is evalSeries f ∘ L near 0.

theorem Analytic.substConv_one {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) →L[K] Fin n → K) : substConv L 1 = 1

theorem Analytic.substConv_mul {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) →L[K] Fin n → K) (f g : ↥(Conv K n)) : substConv L (f * g) = substConv L f * substConv L g

theorem Analytic.substConv_add {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) →L[K] Fin n → K) (f g : ↥(Conv K n)) : substConv L (f + g) = substConv L f + substConv L g

theorem Analytic.substConv_algebraMap {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) →L[K] Fin n → K) (r : K) : substConv L ((algebraMap K ↥(Conv K n)) r) = (algebraMap K ↥(Conv K n)) r

noncomputable def Analytic.substHom {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) →L[K] Fin n → K) : ↥(Conv K n) →ₐ[K] ↥(Conv K n)

f ↦ f ∘ L as a K-algebra map of Conv K n.

Equations

• Analytic.substHom L = { toFun := Analytic.substConv L, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯, commutes' := ⋯ }

@[simp]

theorem Analytic.substHom_apply {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) →L[K] Fin n → K) (f : ↥(Conv K n)) : (substHom L) f = substConv L f

theorem Analytic.substConv_substConv {K : Type u_1} [RCLike K] {n : ℕ} (L L' : (Fin n → K) →L[K] Fin n → K) (f : ↥(Conv K n)) : substConv L (substConv L' f) = substConv (L' ∘SL L) f

theorem Analytic.substConv_id {K : Type u_1} [RCLike K] {n : ℕ} (f : ↥(Conv K n)) : substConv (ContinuousLinearMap.id K (Fin n → K)) f = f

noncomputable def Analytic.substEquiv {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) ≃L[K] Fin n → K) : ↥(Conv K n) ≃ₐ[K] ↥(Conv K n)

A linear automorphism of K^n induces a K-algebra automorphism of Conv K n, f ↦ f ∘ L.

Equations

• Analytic.substEquiv L = AlgEquiv.ofAlgHom (Analytic.substHom ↑L) (Analytic.substHom ↑L.symm) ⋯ ⋯

@[simp]

theorem Analytic.substEquiv_apply {K : Type u_1} [RCLike K] {n : ℕ} (L : (Fin n → K) ≃L[K] Fin n → K) (f : ↥(Conv K n)) : (substEquiv L) f = substConv (↑L) f

theorem Analytic.isRegularIn_of_eventually_axis {K : Type u_1} [RCLike K] {m : ℕ} {F : MvPowerSeries (Fin (m + 1)) K} (hF : F ∈ Conv K (m + 1)) {d : ℕ} {e : K → K} (he : AnalyticAt K e 0) (he0 : e 0 ≠ 0) (hfe : ∀ᶠ (t : K) in nhds 0, evalSeries F (Pi.single 0 t) = t ^ d * e t) : IsRegularIn F d

If the sum of F ∈ Conv K (m+1) restricted to the x_0-axis is t^d e(t) near 0 with e(0) ≠ 0, then F is x_0-regular of order d (the printed f_a(0, …, 0, x_m) ∼ x_m^e of [BM88, proof of Theorem 4.4, p. 24], read through the expansion on the axis).

theorem Analytic.exists_substEquiv_isRegularIn {K : Type u_1} [RCLike K] {m : ℕ} {f : ↥(Conv K (m + 1))} (hf0 : f ≠ 0) : ∃ (L : (Fin (m + 1) → K) ≃L[K] Fin (m + 1) → K), IsRegularIn (↑((substEquiv L) f)) (↑f).order.toNat

Every nonzero f ∈ Conv K (m+1) becomes x_0-regular of order ord f after a linear change of variables: "there are local coordinates … such that f_a(0, …, 0, x_m) ∼ x_m^e" [BM88, proof of Theorem 4.4, p. 24] (the generic linear change of Hironaka/Analytic/Germ/Axis.lean, transported to Conv).