The analytic order of products, power maps and derivatives

Extensions of Mathlib's analytic-order calculus: analyticOrderNatAt respects eventual equality, the order is additive over finite products, composing with q ↦ q ^ N at 0 multiplies the order by N, the power map w ↦ w ^ m recentred at 0 has order m there for m ≠ 0, the recentred function f · - f x has order 1 at x exactly when deriv f x ≠ 0, and the order is monotone under domination (=O), hence invariant under equivalence up to constant factors (=Θ). The finiteness a zero count also needs is TauCeti.finite_setOf_mem_and_eq_zero_of_isCompact, provided by TauCeti.Analysis.Analytic.IsolatedZeros, which mentions no order.

Main declarations

• AnalyticAt.exists_analyticOrderAt_monomial_sub_eq_min: outside at most two scalar coefficients, subtraction of a scalar monomial has the minimum of the two orders.
• TauCeti.analyticOrderNatAt_congr: eventual equality preserves the natural analytic order.
• TauCeti.analyticOrderAt_prod: the order of ∏ i ∈ s, F i is ∑ i ∈ s, of the orders.
• TauCeti.analyticOrderAt_comp_pow_zero: the order of q ↦ f (q ^ N) at 0 is N times the order of f at 0.
• TauCeti.analyticOrderAt_pow_sub_zero_pow: the order of w ↦ w ^ m - 0 ^ m at 0 is m for m ≠ 0.
• AnalyticAt.analyticOrderAt_sub_eq_one_iff_deriv_ne_zero: f · - f x has order 1 at x exactly when deriv f x ≠ 0, the iff form of Mathlib's AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero.
• AnalyticAt.analyticOrderAt_le_of_isBigO and AnalyticAt.analyticOrderAt_eq_of_isTheta: an analytic function dominated by f vanishes to at least the order of f, so analytic functions equivalent up to constant factors have the same order.

References

• Mathlib PR #39083 (Chris Birkbeck) — the upstream draft from which this file ports the eventual-equality, product, power-map and derivative lemmas onto the current Mathlib pin.

theorem TauCeti.analyticOrderNatAt_congr {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z₀ : 𝕜} {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f g : 𝕜 → E} (hfg : f =ᶠ[nhds z₀] g) : analyticOrderNatAt f z₀ = analyticOrderNatAt g z₀

Functions that agree near a point have the same natural analytic order there.

theorem TauCeti.analyticOrderAt_prod {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z₀ : 𝕜} {ι : Type u_2} {s : Finset ι} {F : ι → 𝕜 → 𝕜} (hF : ∀ i ∈ s, AnalyticAt 𝕜 (F i) z₀) : analyticOrderAt (∏ i ∈ s, F i) z₀ = ∑ i ∈ s, analyticOrderAt (F i) z₀

The order is additive when taking a finite product of analytic functions.

theorem TauCeti.analyticOrderAt_comp_pow_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {f : 𝕜 → E} (hf : AnalyticAt 𝕜 f 0) {N : ℕ} (hN : 0 < N) : analyticOrderAt (fun (q : 𝕜) => f (q ^ N)) 0 = analyticOrderAt f 0 * ↑N

The analytic order of q ↦ f (q ^ N) at 0 is N times the analytic order of f at 0.

theorem TauCeti.analyticOrderAt_pow_sub_zero_pow {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {m : ℕ} (hm : m ≠ 0) : analyticOrderAt (fun (w : 𝕜) => w ^ m - 0 ^ m) 0 = ↑m

The power map w ↦ w ^ m, recentred at 0, has analytic order m at 0 when m ≠ 0.

theorem AnalyticAt.analyticOrderAt_sub_eq_one_iff_deriv_ne_zero {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] [CharZero 𝕜] {f : 𝕜 → E} {x : 𝕜} (hf : AnalyticAt 𝕜 f x) : analyticOrderAt (fun (x_1 : 𝕜) => f x_1 - f x) x = 1 ↔ deriv f x ≠ 0

A function analytic at x has a simple zero of f · - f x at x exactly when its derivative at x does not vanish: the iff form of Mathlib's AnalyticAt.analyticOrderAt_sub_eq_one_of_deriv_ne_zero.

theorem AnalyticAt.analyticOrderAt_le_of_isBigO {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z₀ : 𝕜} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → E} {g : 𝕜 → F} (hg : AnalyticAt 𝕜 g z₀) (hgf : g =O[nhds z₀] f) : analyticOrderAt f z₀ ≤ analyticOrderAt g z₀

A function analytic at z₀ and dominated there by f vanishes to at least the order of f at z₀. No analyticity of f is needed: a non-analytic f has order 0.

theorem AnalyticAt.analyticOrderAt_eq_of_isTheta {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {z₀ : 𝕜} {E : Type u_2} {F : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] {f : 𝕜 → E} {g : 𝕜 → F} (hf : AnalyticAt 𝕜 f z₀) (hg : AnalyticAt 𝕜 g z₀) (hfg : f =Θ[nhds z₀] g) : analyticOrderAt f z₀ = analyticOrderAt g z₀

Two functions analytic at z₀ that are equivalent up to constant factors near z₀ vanish to the same order there.

theorem AnalyticAt.exists_analyticOrderAt_monomial_sub_eq_min {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] {f : 𝕜 → 𝕜} (hf : AnalyticAt 𝕜 f 0) (N : ℕ) : ∃ (b : 𝕜), ∀ (c : 𝕜), c ≠ 0 → c ≠ b → analyticOrderAt (fun (t : 𝕜) => c * t ^ N - f t) 0 = min (↑N) (analyticOrderAt f 0)

Outside zero and at most one additional scalar, subtracting an analytic germ from a scalar multiple of a monomial has order equal to the minimum of their orders. The exceptional scalar accounts for cancellation when the two orders coincide.