Reconstruction from weighted ℓ¹ coefficients #
Evaluating the analytic weighted moving-coefficient map at r⁻¹ w
reconstructs the original ambient formal multilinear series wherever the
change-of-origin expansion converges. A second theorem identifies the result
with any function represented by that series on a ball.
theorem
ClassicalComplexWPT.eval_weightedCoefficientSeries_eq
{n : ℕ}
(p : FormalMultilinearSeries ℂ (Ambient n) ℂ)
(r : NNReal)
(hr0 : 0 < r)
(hrp : ↑r < p.radius)
(z : Base n)
(w : ℂ)
(hzq : z ∈ Metric.eball 0 (weightedCoefficientSeries p r).radius)
(hzw : ↑‖(z, 0)‖₊ + ↑‖(0, w)‖₊ < p.radius)
(hw : ‖w‖ < ↑r)
:
theorem
ClassicalComplexWPT.analyticAt_eval_weightedCoefficientSeries
{n : ℕ}
(p : FormalMultilinearSeries ℂ (Ambient n) ℂ)
(r : NNReal)
(hrp : ↑r < p.radius)
:
AnalyticAt ℂ (fun (x : Base n × ℂ) => evalL1PowerSeries ((weightedCoefficientSeries p r).sum x.1) ((↑↑r)⁻¹ * x.2)) 0
The weighted coefficient family can be evaluated analytically in the base
and distinguished variables. This is the specialization of
AnalyticAt.evalL1PowerSeries used for analytic quotients and units.
theorem
ClassicalComplexWPT.eval_weightedCoefficientSeries_eq_of_hasFPowerSeriesOnBall
{n : ℕ}
{f : Ambient n → ℂ}
(p : FormalMultilinearSeries ℂ (Ambient n) ℂ)
(r : NNReal)
{ρ : ENNReal}
(hp : HasFPowerSeriesOnBall f p 0 ρ)
(hr0 : 0 < r)
(hrp : ↑r < p.radius)
(z : Base n)
(w : ℂ)
(hzq : z ∈ Metric.eball 0 (weightedCoefficientSeries p r).radius)
(hzw : ↑‖(z, 0)‖₊ + ↑‖(0, w)‖₊ < ρ)
(hw : ‖w‖ < ↑r)
:
If p represents f on a ball, weighted evaluation reconstructs f on
the explicit common convergence region.