Germ-level weighted coefficient reconstruction

The explicit weighted reconstruction theorem uses three radius inequalities. This file packages their simultaneous neighborhood shrinking into the germ identity needed by preparation and uniqueness.

theorem ClassicalComplexWPT.eventually_eval_weightedCoefficientSeries_eq_of_hasFPowerSeriesAt {n : ℕ} {f : Ambient n → ℂ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hp : HasFPowerSeriesAt f p 0) (hr0 : 0 < r) (hrp : ↑r < p.radius) : (fun (x : Ambient n) => evalL1PowerSeries ((weightedCoefficientSeries p r).sum x.1) ((↑↑r)⁻¹ * x.2)) =ᶠ[nhds 0] f

On a sufficiently small common neighborhood, evaluating the weighted moving-coefficient sequence recovers the analytic function represented by the ambient formal multilinear series.