The Taylor homomorphism commutes with differentiation

Bierstone–Milman's Taylor series homomorphism T_a "commutes with differentiation" [BM97, (0.3)]. A convergent power series may be differentiated term by term: on the polydisc of half the radius, ∂_i (evalSeries c) = evalSeries (∂_{X_i} c) (fderiv_evalSeries_single, from Mathlib's hasDerivAt_tsum_of_isPreconnected along the i-th coordinate line, the terms being the monomials a_ν y^{ν_i} ∏_{k ≠ i} x_k^{ν_k} with the summable majorant 2/ρ_i · ‖a_ν‖ ρ^ν), and the derived series is convergent (pderiv_mem_conv, ‖∂_{X_i} c‖_{ρ/2} · ρ_i ≤ 2 ‖c‖_ρ); the formal derivative ∂_{X_i} is Mathlib's MvPowerSeries.pderiv. Hence the power series of the coordinate derivative ∂_i g of an analytic germ is ∂_{X_i} of the power series of g (IsSeriesOf.pderiv, taylorGerm_pderivGerm), and the Taylor homomorphism satisfies T_a (∂_i f) = ∂_{X_i} (T_a f) (IsTaylorHom.pderiv'; the form on the stalk operators is IsTaylorHom.pderiv in Hironaka/Manifold/Germ/CoordDerivChart.lean).

theorem Manifold.monomialEval_eq_mul_prod_erase {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (x : Fin n → 𝕜) (i : Fin n) (ν : Fin n →₀ ℕ) : Analytic.monomialEval x ν = x i ^ ν i * ∏ k ∈ Finset.univ.erase i, x k ^ ν k

x^ν with the i-th factor split off.

theorem Manifold.monomialEval_update {𝕜 : Type} [RCLike 𝕜] {n : ℕ} (x : Fin n → 𝕜) (i : Fin n) (y : 𝕜) (ν : Fin n →₀ ℕ) : Analytic.monomialEval (Function.update x i y) ν = y ^ ν i * ∏ k ∈ Finset.univ.erase i, x k ^ ν k

theorem Manifold.nat_mul_half_pow_le {r : ℝ} (hr : 0 < r) (m : ℕ) : ↑m * (r / 2) ^ (m - 1) ≤ 2 / r * r ^ m

m (r/2)^(m−1) ≤ (2/r) r^m for r > 0.

theorem Manifold.monomialEval_half_le {n : ℕ} (ρ : Fin n → NNReal) (μ : Fin n →₀ ℕ) (i : Fin n) : ↑(μ i + 1) * Analytic.monomialEval (fun (k : Fin n) => ρ k / 2) μ ≤ 2 * Analytic.monomialEval ρ μ

(m+1) (ρ/2)^μ ≤ 2 ρ^μ when m ≤ |μ| — for m = μ_i.

theorem Manifold.pderiv_mem_conv {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {c : MvPowerSeries (Fin n) 𝕜} (hc : c ∈ Analytic.Conv 𝕜 n) (i : Fin n) : (MvPowerSeries.pderiv i) c ∈ Analytic.Conv 𝕜 n

The formal derivative of a convergent series is convergent: ‖∂_{X_i} c‖_{ρ/2} · ρ_i ≤ 2 ‖c‖_ρ.

theorem Manifold.fderiv_evalSeries_single {𝕜 : Type} [RCLike 𝕜] {n : ℕ} {ρ : Analytic.Radius n} {c : MvPowerSeries (Fin n) 𝕜} (hρ : Analytic.ConvNorm (↑ρ) c ≠ ⊤) {x : Fin n → 𝕜} (hx : ∀ (k : Fin n), ‖x k‖ < ↑(↑ρ k) / 2) (i : Fin n) : (fderiv 𝕜 (Analytic.evalSeries c) x) (Pi.single i 1) = Analytic.evalSeries ((MvPowerSeries.pderiv i) c) x

Termwise differentiation of a convergent power series along the i-th coordinate (Mathlib's hasDerivAt_tsum_of_isPreconnected): on the polydisc of half the radius, ∂_i (evalSeries c) = evalSeries (∂_{X_i} c).

theorem Manifold.pderivGerm_coe {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (i : Fin n) (b : E) (f : E → 𝕜) (hf : ↑f ∈ analyticGermsAt 𝕜 E b) : ↑(pderivGerm E ψ i b ⟨↑f, hf⟩) = ↑fun (y : E) => (fderiv 𝕜 f y) (ψ.symm (Pi.single i 1))

theorem Manifold.IsSeriesOf.pderiv {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) {b : E} {f : E → 𝕜} {c : MvPowerSeries (Fin n) 𝕜} (hc : IsSeriesOf ψ b (↑f) c) (i : Fin n) : IsSeriesOf ψ b (↑fun (z : E) => (fderiv 𝕜 f z) (ψ.symm (Pi.single i 1))) ((MvPowerSeries.pderiv i) c)

The power series of the coordinate derivative ∂_i g of an analytic germ is ∂_{X_i} of the power series of g.

theorem Manifold.taylorGerm_pderivGerm {𝕜 : Type} [RCLike 𝕜] {E : Type u_1} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (b : E) (i : Fin n) (g : ↥(analyticGermsAt 𝕜 E b)) : ↑((taylorGerm ψ b) (pderivGerm E ψ i b g)) = (MvPowerSeries.pderiv i) ↑((taylorGerm ψ b) g)

taylorGerm (∂_i g) = ∂_{X_i} (taylorGerm g).

theorem Manifold.IsTaylorHom.pderiv' {𝕜 : Type} [RCLike 𝕜] (E : Type u_1) [NormedAddCommGroup E] [NormedSpace 𝕜 E] {M : Type u} [TopologicalSpace M] [ChartedSpace E M] {n : ℕ} (ψ : E ≃L[𝕜] Fin n → 𝕜) (φ : OpenPartialHomeomorph M E) {a : M} (ha : a ∈ φ.source) (hφ : φ ∈ IsManifold.maximalAtlas (modelWithCornersSelf 𝕜 E) ⊤ M) {T : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) →+* MvPowerSeries (Fin n) 𝕜} (hT : IsTaylorHom E ψ φ a T) {e : ↑((structureSheaf 𝕜 E M).presheaf.stalk a) ≃+* ↥(analyticGermsAt 𝕜 E (↑φ a))} (he : IsChartTransport 𝕜 E φ a e) (i : Fin n) (g : ↥(analyticGermsAt 𝕜 E (↑φ a))) : T (e.symm (pderivGerm E ψ i (↑φ a) g)) = (MvPowerSeries.pderiv i) (T (e.symm g))

"T_a commutes with differentiation" [BM97, (0.3)]: T_a(∂_i f) = ∂_{X_i} T_a(f) for the coordinate partial derivatives of germs in the chart, read through the chart transport.