Moving Taylor coefficients

Mathlib's FormalMultilinearSeries.changeOrigin is the bridge from one power series at the ambient origin to Taylor coefficients at the moving centers (z, 0). In particular, every coefficient in the distinguished variable is an analytic function of z, with all radii controlled by the original series.

noncomputable def ClassicalComplexWPT.lastAxis (n : ℕ) : ℂ →L[ℂ] Ambient n

Continuous-linear inclusion of the distinguished complex axis.

Equations

• ClassicalComplexWPT.lastAxis n = ContinuousLinearMap.inr ℂ (ClassicalComplexWPT.Base n) ℂ

@[simp]

theorem ClassicalComplexWPT.lastAxis_apply (n : ℕ) (w : ℂ) : (lastAxis n) w = (0, w)

def ClassicalComplexWPT.lastDirection (n : ℕ) : Ambient n

The unit vector in the distinguished complex direction.

Equations

• ClassicalComplexWPT.lastDirection n = (0, 1)

noncomputable def ClassicalComplexWPT.lastTaylorCoefficient {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (k : ℕ) (z : Base n) : ℂ

The k-th (factorial-normalized) distinguished-variable Taylor coefficient at (z, 0).

Equations

• ClassicalComplexWPT.lastTaylorCoefficient p k z = (p.changeOrigin (z, 0) k) fun (x : Fin k) => ClassicalComplexWPT.lastDirection n

theorem ClassicalComplexWPT.lastTaylorCoefficient_zero {n k : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) : lastTaylorCoefficient p k 0 = (p k) fun (x : Fin k) => lastDirection n

At the base origin, changing origin leaves the diagonal distinguished coefficient unchanged.

theorem ClassicalComplexWPT.factorial_smul_lastTaylorCoefficient_zero {n k : ℕ} {f : Ambient n → ℂ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (hp : HasFPowerSeriesAt f p 0) : k.factorial • lastTaylorCoefficient p k 0 = iteratedDeriv k (lastSlice f) 0

The moving coefficient at the base origin is the usual factorial-normalized iterated derivative of the distinguished slice.

theorem ClassicalComplexWPT.lastTaylorCoefficient_zero_iff_iteratedDeriv_zero {n k : ℕ} {f : Ambient n → ℂ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (hp : HasFPowerSeriesAt f p 0) : lastTaylorCoefficient p k 0 = 0 ↔ iteratedDeriv k (lastSlice f) 0 = 0

Vanishing of a directional Taylor coefficient is equivalent to vanishing of the derivative.

theorem ClassicalComplexWPT.exactOrderInLastVariable_iff_lastTaylorCoefficients {n d : ℕ} {f : Ambient n → ℂ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (hp : HasFPowerSeriesAt f p 0) : ExactOrderInLastVariable f d ↔ (∀ k < d, lastTaylorCoefficient p k 0 = 0) ∧ lastTaylorCoefficient p d 0 ≠ 0

The public exact-order condition is exactly the first-nonzero-coefficient condition.

theorem ClassicalComplexWPT.analyticAt_lastTaylorCoefficient {n k : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (hp : 0 < p.radius) : AnalyticAt ℂ (lastTaylorCoefficient p k) 0

Every moving distinguished-variable coefficient is analytic in the base variables.

theorem ClassicalComplexWPT.AnalyticAt.exists_powerSeries_with_analytic_lastCoefficients {n : ℕ} {f : Ambient n → ℂ} (hf : AnalyticAt ℂ f 0) : ∃ (p : FormalMultilinearSeries ℂ (Ambient n) ℂ), HasFPowerSeriesAt f p 0 ∧ ∀ (k : ℕ), AnalyticAt ℂ (lastTaylorCoefficient p k) 0

An analytic germ admits one ambient series whose moving last-variable coefficients are analytic.