Conjugation symmetry of divided differences

Over a nontrivially normed field with a norm-preserving star ring structure (such as ℂ), local conjugation symmetry of a function at a self-conjugate centre passes to its divided difference at that centre, including the value there, which is the derivative. A normalization constant is allowed: this is useful when a holomorphic regular factor carries a fixed complex phase.

Main results

• TauCeti.eventually_dslope_div_const_conj: if f (conj z) / c = conj (f z / c) near a centre a with conj a = a, then the same holds for dslope f a near a.

theorem TauCeti.eventually_dslope_div_const_conj {𝕜 : Type u_1} [NontriviallyNormedField 𝕜] [StarRing 𝕜] [NormedStarGroup 𝕜] {f : 𝕜 → 𝕜} {a : 𝕜} (ha : (starRingEnd 𝕜) a = a) (c : 𝕜) (hf : ∀ᶠ (z : 𝕜) in nhds a, f ((starRingEnd 𝕜) z) / c = (starRingEnd 𝕜) (f z / c)) : ∀ᶠ (z : 𝕜) in nhds a, dslope f a ((starRingEnd 𝕜) z) / c = (starRingEnd 𝕜) (dslope f a z / c)

Dividing a function by a constant and taking its divided difference at a self-conjugate centre preserves local conjugation symmetry. No differentiability assumption is needed: at the centre, conjugation also respects the convention that the derivative is zero when absent.