The Taylor series of an analytic germ

In coordinates ψ : E ≃L[𝕜] 𝕜ⁿ, an analytic germ g at b ∈ E has a unique convergent power series c ∈ Conv 𝕜 n (the ring of convergent series of Hironaka/Analytic/) with g(ψ⁻¹ y) = c(y − ψ b) near ψ b (IsSeriesOf, exists_isSeriesOf, IsSeriesOf.unique, from AnalyticAt.exists_eventuallyEq_evalSeries and eq_of_evalSeries_eventuallyEq). Taking the series is a ring homomorphism taylorGerm ψ b : analyticGermsAt 𝕜 E b →+* Conv 𝕜 n (multiplicativity and additivity of the evaluation of convergent series on a common polydisc, evalSeries_mul, evalSeries_add), and it is injective (taylorGerm_injective). Composed with the chart transport of Hironaka/Manifold/Germ/ChartTransport.lean this is Bierstone–Milman's Taylor series homomorphism T_a [BM97, (0.3)] (taylorHom in Hironaka/Manifold/Germ/TaylorHom.lean).

theorem Manifold.tendsto_coord_symm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) : Filter.Tendsto (⇑ψ.symm) (nhds (ψ b)) (nhds b)

The coordinates ψ⁻¹ tend to b at ψ b.

@[reducible, inline]

abbrev Manifold.germCompCoord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) : (nhds b).Germ 𝕜 →+* (nhds (ψ b)).Germ 𝕜

Composition with the coordinates ψ⁻¹, as a ring homomorphism of germs Filter.Germ (𝓝 b) 𝕜 →+* Filter.Germ (𝓝 (ψ b)) 𝕜 (an instance of germCompRingHom).

Equations

• Manifold.germCompCoord ψ b = Manifold.germCompRingHom ⇑ψ.symm ⋯

theorem Manifold.germCompCoord_coe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) (f : E → 𝕜) : (germCompCoord ψ b) ↑f = ↑(f ∘ ⇑ψ.symm)

theorem Manifold.germCompCoord_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) : Function.Injective ⇑(germCompCoord ψ b)

def Manifold.IsSeriesOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) (g : (nhds b).Germ 𝕜) (c : MvPowerSeries (Fin n) 𝕜) : Prop

c is the power series of the germ g at b in the coordinates ψ: c is a convergent series and g(ψ⁻¹ y) = c(y − ψ b) for y near ψ b.

Equations

• Manifold.IsSeriesOf ψ b g c = (c ∈ Analytic.Conv 𝕜 n ∧ (Manifold.germCompCoord ψ b) g = ↑fun (y : Fin n → 𝕜) => Analytic.evalSeries c (y - ψ b))

theorem Manifold.tendsto_add_coord {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) : Filter.Tendsto (fun (y : Fin n → 𝕜) => y + ψ b) (nhds 0) (nhds (ψ b))

The translation y ↦ y + ψ b sends 𝓝 0 to 𝓝 (ψ b).

theorem Manifold.eq_of_evalSeries_sub_eventuallyEq {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) {c c' : MvPowerSeries (Fin n) 𝕜} (hc : c ∈ Analytic.Conv 𝕜 n) (hc' : c' ∈ Analytic.Conv 𝕜 n) (h : (fun (y : Fin n → 𝕜) => Analytic.evalSeries c (y - ψ b)) =ᶠ[nhds (ψ b)] fun (y : Fin n → 𝕜) => Analytic.evalSeries c' (y - ψ b)) : c = c'

Two convergent series with the same germ of evaluations at ψ b are equal.

theorem Manifold.IsSeriesOf.unique {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {b : E} {g : (nhds b).Germ 𝕜} {c c' : MvPowerSeries (Fin n) 𝕜} (hc : IsSeriesOf ψ b g c) (hc' : IsSeriesOf ψ b g c') : c = c'

The power series of a germ is unique.

theorem Manifold.exists_isSeriesOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {b : E} {g : (nhds b).Germ 𝕜} (hg : g ∈ analyticGermsAt 𝕜 E b) : ∃ (c : MvPowerSeries (Fin n) 𝕜), IsSeriesOf ψ b g c

Every analytic germ has a power series (AnalyticAt.exists_eventuallyEq_evalSeries).

theorem Manifold.IsSeriesOf.mul {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {b : E} {g g' : (nhds b).Germ 𝕜} {c c' : MvPowerSeries (Fin n) 𝕜} (hc : IsSeriesOf ψ b g c) (hc' : IsSeriesOf ψ b g' c') : IsSeriesOf ψ b (g * g') (c * c')

The power series of a product is the product of the power series (evaluation is multiplicative on a common polydisc, evalSeries_mul).

theorem Manifold.IsSeriesOf.add {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {b : E} {g g' : (nhds b).Germ 𝕜} {c c' : MvPowerSeries (Fin n) 𝕜} (hc : IsSeriesOf ψ b g c) (hc' : IsSeriesOf ψ b g' c') : IsSeriesOf ψ b (g + g') (c + c')

The power series of a sum is the sum of the power series (evalSeries_add).

theorem Manifold.IsSeriesOf.one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) : IsSeriesOf ψ b 1 1

theorem Manifold.IsSeriesOf.zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) : IsSeriesOf ψ b 0 0

noncomputable def Manifold.taylorGermFun {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) (g : (nhds b).Germ 𝕜) (hg : g ∈ analyticGermsAt 𝕜 E b) : MvPowerSeries (Fin n) 𝕜

The power series of an analytic germ, the unique convergent series c with g(ψ⁻¹ y) = c(y − ψ b) near ψ b.

Equations

• Manifold.taylorGermFun ψ b g hg = ⋯.choose

theorem Manifold.isSeriesOf_taylorGermFun {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) (g : (nhds b).Germ 𝕜) (hg : g ∈ analyticGermsAt 𝕜 E b) : IsSeriesOf ψ b g (taylorGermFun ψ b g hg)

theorem Manifold.taylorGermFun_eq_of_isSeriesOf {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {b : E} {g : (nhds b).Germ 𝕜} (hg : g ∈ analyticGermsAt 𝕜 E b) {c : MvPowerSeries (Fin n) 𝕜} (hc : IsSeriesOf ψ b g c) : taylorGermFun ψ b g hg = c

theorem Manifold.taylorGermFun_one {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) : taylorGermFun ψ b 1 ⋯ = 1

theorem Manifold.taylorGermFun_zero {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) : taylorGermFun ψ b 0 ⋯ = 0

theorem Manifold.taylorGermFun_mul {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) {g g' : (nhds b).Germ 𝕜} (hg : g ∈ analyticGermsAt 𝕜 E b) (hg' : g' ∈ analyticGermsAt 𝕜 E b) : taylorGermFun ψ b (g * g') ⋯ = taylorGermFun ψ b g hg * taylorGermFun ψ b g' hg'

theorem Manifold.taylorGermFun_add {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) {g g' : (nhds b).Germ 𝕜} (hg : g ∈ analyticGermsAt 𝕜 E b) (hg' : g' ∈ analyticGermsAt 𝕜 E b) : taylorGermFun ψ b (g + g') ⋯ = taylorGermFun ψ b g hg + taylorGermFun ψ b g' hg'

noncomputable def Manifold.taylorGerm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) : ↥(analyticGermsAt 𝕜 E b) →+* ↥(Analytic.Conv 𝕜 n)

Taking the power series is a ring homomorphism into the ring Conv 𝕜 n of convergent series.

Equations

• Manifold.taylorGerm ψ b = { toFun := fun (g : ↥(Manifold.analyticGermsAt 𝕜 E b)) => ⟨Manifold.taylorGermFun ψ b ↑g ⋯, ⋯⟩, map_one' := ⋯, map_mul' := ⋯, map_zero' := ⋯, map_add' := ⋯ }

theorem Manifold.coe_taylorGerm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) (g : ↥(analyticGermsAt 𝕜 E b)) : ↑((taylorGerm ψ b) g) = taylorGermFun ψ b ↑g ⋯

theorem Manifold.isSeriesOf_taylorGerm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) (g : ↥(analyticGermsAt 𝕜 E b)) : IsSeriesOf ψ b ↑g ↑((taylorGerm ψ b) g)

theorem Manifold.taylorGerm_injective {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) : Function.Injective ⇑(taylorGerm ψ b)

The power series determines the germ: a germ whose series vanishes is eventually zero.