Taylor coefficients via iterated difference quotients (residue-calculus)

RS.taylorCoeffAt g z₀ j is the j-th Taylor coefficient of g at z₀, extracted by the iterated dslope operator — no iteratedDeriv, no factorials. For g analytic at z₀ with power series p it equals p.coeff j (RS.HasFPowerSeriesAt.taylorCoeffAt_eq).

Main exports:

• RS.taylorCoeffAt_congr — dependence on the 𝓝 z₀-germ only;
• RS.taylorCoeffAt_add / _const_mul / _sub / _fun_sum — ℂ-linearity on analytic germs;
• RS.taylorCoeffAt_sub_pow_mul, RS.taylorCoeffAt_monomial — the monomial shift workhorse;
• RS.AnalyticAt.exists_taylor_remainder — exact, pointwise Taylor remainder factorization.

noncomputable def RS.taylorCoeffAt (g : ℂ → ℂ) (z₀ : ℂ) (j : ℕ) : ℂ

The j-th Taylor coefficient of g at z₀, extracted by iterated difference quotients. For g analytic at z₀ with power series p this equals p.coeff j. Junk for non-smooth g (whatever the iterated dslope evaluates to).

Equations

• RS.taylorCoeffAt g z₀ j = (Function.swap dslope z₀)^[j] g z₀

@[simp]

theorem RS.taylorCoeffAt_zero_apply {g : ℂ → ℂ} {z₀ : ℂ} : taylorCoeffAt g z₀ 0 = g z₀

theorem RS.taylorCoeffAt_succ {g : ℂ → ℂ} {z₀ : ℂ} (j : ℕ) : taylorCoeffAt g z₀ (j + 1) = taylorCoeffAt (dslope g z₀) z₀ j

theorem RS.AnalyticAt.iterate_dslope {g : ℂ → ℂ} {z₀ : ℂ} (hg : AnalyticAt ℂ g z₀) (j : ℕ) : AnalyticAt ℂ ((Function.swap dslope z₀)^[j] g) z₀

dslope iterates of analytic germs are analytic.

theorem RS.HasFPowerSeriesAt.taylorCoeffAt_eq {g : ℂ → ℂ} {z₀ : ℂ} {p : FormalMultilinearSeries ℂ ℂ ℂ} (hp : HasFPowerSeriesAt g p z₀) (j : ℕ) : taylorCoeffAt g z₀ j = p.coeff j

Bridge to power series (for consumers that hold a HasFPowerSeriesAt; not used internally).

theorem RS.Filter.EventuallyEq.dslope_eq {f g : ℂ → ℂ} {z₀ : ℂ} (hfg : f =ᶠ[nhds z₀] g) : dslope f z₀ =ᶠ[nhds z₀] dslope g z₀

dslope respects 𝓝 z₀-germs.

theorem RS.taylorCoeffAt_congr {f g : ℂ → ℂ} {z₀ : ℂ} (hfg : f =ᶠ[nhds z₀] g) (j : ℕ) : taylorCoeffAt f z₀ j = taylorCoeffAt g z₀ j

Germ invariance: taylorCoeffAt only depends on the 𝓝 z₀-germ.

theorem RS.dslope_const_mul (c : ℂ) (g : ℂ → ℂ) (z₀ : ℂ) : dslope (fun (z : ℂ) => c * g z) z₀ = fun (b : ℂ) => c * dslope g z₀ b

theorem RS.dslope_const (c z₀ : ℂ) : dslope (fun (x : ℂ) => c) z₀ = fun (x : ℂ) => 0

theorem RS.taylorCoeffAt_const_mul {g : ℂ → ℂ} {z₀ : ℂ} (c : ℂ) (j : ℕ) : taylorCoeffAt (fun (z : ℂ) => c * g z) z₀ j = c * taylorCoeffAt g z₀ j

theorem RS.taylorCoeffAt_zero_fun {z₀ : ℂ} (j : ℕ) : taylorCoeffAt (fun (x : ℂ) => 0) z₀ j = 0

@[simp]

theorem RS.taylorCoeffAt_const {z₀ : ℂ} (c : ℂ) (j : ℕ) : taylorCoeffAt (fun (x : ℂ) => c) z₀ j = if j = 0 then c else 0

theorem RS.taylorCoeffAt_neg {g : ℂ → ℂ} {z₀ : ℂ} (j : ℕ) : taylorCoeffAt (fun (z : ℂ) => -g z) z₀ j = -taylorCoeffAt g z₀ j

theorem RS.taylorCoeffAt_add {f g : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) (hg : AnalyticAt ℂ g z₀) (j : ℕ) : taylorCoeffAt (f + g) z₀ j = taylorCoeffAt f z₀ j + taylorCoeffAt g z₀ j

ℂ-additivity of Taylor coefficients on analytic germs.

theorem RS.taylorCoeffAt_fun_add {f g : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) (hg : AnalyticAt ℂ g z₀) (j : ℕ) : taylorCoeffAt (fun (z : ℂ) => f z + g z) z₀ j = taylorCoeffAt f z₀ j + taylorCoeffAt g z₀ j

theorem RS.taylorCoeffAt_sub {f g : ℂ → ℂ} {z₀ : ℂ} (hf : AnalyticAt ℂ f z₀) (hg : AnalyticAt ℂ g z₀) (j : ℕ) : taylorCoeffAt (fun (z : ℂ) => f z - g z) z₀ j = taylorCoeffAt f z₀ j - taylorCoeffAt g z₀ j

theorem RS.taylorCoeffAt_fun_sum {z₀ : ℂ} {ι : Type u_1} {s : Finset ι} {G : ι → ℂ → ℂ} (hG : ∀ i ∈ s, AnalyticAt ℂ (G i) z₀) (j : ℕ) : taylorCoeffAt (fun (z : ℂ) => ∑ i ∈ s, G i z) z₀ j = ∑ i ∈ s, taylorCoeffAt (G i) z₀ j

theorem RS.dslope_sub_mul {F : ℂ → ℂ} {z₀ : ℂ} (hF : DifferentiableAt ℂ F z₀) : dslope (fun (z : ℂ) => (z - z₀) * F z) z₀ = F

theorem RS.taylorCoeffAt_sub_pow_mul {g : ℂ → ℂ} {z₀ : ℂ} (hg : AnalyticAt ℂ g z₀) (d j : ℕ) : taylorCoeffAt (fun (z : ℂ) => (z - z₀) ^ d * g z) z₀ j = if j < d then 0 else taylorCoeffAt g z₀ (j - d)

Shift: prepending a monomial factor shifts Taylor coefficients. THE workhorse identity.

@[simp]

theorem RS.taylorCoeffAt_monomial {z₀ : ℂ} (d j : ℕ) : taylorCoeffAt (fun (z : ℂ) => (z - z₀) ^ d) z₀ j = if j = d then 1 else 0

theorem RS.AnalyticAt.exists_taylor_remainder {g : ℂ → ℂ} {z₀ : ℂ} (hg : AnalyticAt ℂ g z₀) (m : ℕ) : ∃ (r : ℂ → ℂ), AnalyticAt ℂ r z₀ ∧ (∀ (j : ℕ), taylorCoeffAt r z₀ j = taylorCoeffAt g z₀ (j + m)) ∧ ∀ (z : ℂ), g z = ∑ d ∈ Finset.range m, taylorCoeffAt g z₀ d * (z - z₀) ^ d + (z - z₀) ^ m * r z

Taylor remainder factorization, EXACT (pointwise): subtracting the degree-< m Taylor polynomial leaves an honest (z - z₀) ^ m-divisible function with analytic quotient.