Hadamard's lemma for analytic functions

A function f analytic at c can be written near c as f z - f c = G z (z - c), where G z = ∫ t in 0..1, fderiv 𝕜 f (c + t • (z - c)) is the average of the derivative of f along the segment from c to z. The averaged derivative G is again analytic at c, by AnalyticAt.intervalIntegral_comp, and G c is the derivative of f at c (AnalyticAt.exists_analyticAt_eventually_sub_eq).

In finite dimensions, expanding z - c in a basis turns this into the statement that f - f c lies in the ideal of analytic germs at c generated by the affine coordinates vanishing at c. This is the analytic counterpart of the smooth factorization ContDiff.sub_eq_hadamardFactor_apply in TauCeti.Analysis.Calculus.Hadamard.

theorem AnalyticAt.exists_analyticAt_eventually_sub_eq {𝕜 : Type u_1} {E : Type u_2} {F : Type u_3} [RCLike 𝕜] [NormedAddCommGroup E] [NormedSpace 𝕜 E] [NormedAddCommGroup F] [NormedSpace 𝕜 F] [CompleteSpace F] {f : E → F} {c : E} (hf : AnalyticAt 𝕜 f c) : ∃ (G : E → E →L[𝕜] F), AnalyticAt 𝕜 G c ∧ G c = fderiv 𝕜 f c ∧ ∀ᶠ (z : E) in nhds c, f z - f c = (G z) (z - c)

Hadamard's lemma for analytic functions: a function f analytic at c satisfies f z - f c = G z (z - c) near c for a map G into continuous linear maps which is analytic at c, with G c = fderiv 𝕜 f c.