Analytic evaluation of an ℓ¹ coefficient sequence

An ℓ¹ sequence defines a power series on the open unit disc. More importantly for preparation, evaluation is jointly analytic in the coefficient sequence and the scalar variable at every point whose scalar coordinate is zero. The proof packages the coordinate evaluations into an operator-valued formal multilinear series with radius at least one.

@[reducible, inline]

noncomputable abbrev ClassicalComplexWPT.L1Sequence : AddSubgroup (PreLp fun (x : ℕ) => ℂ)

Complex ℓ¹ sequences, viewed as coefficients of one-variable power series.

Equations

• ClassicalComplexWPT.L1Sequence = ClassicalComplexWPT.L1Coeff ℕ

noncomputable def ClassicalComplexWPT.coefficientEval (k : ℕ) : ↥L1Sequence →L[ℂ] ℂ

Evaluation of the k-th coefficient as a continuous linear functional.

Equations

• ClassicalComplexWPT.coefficientEval k = lp.evalCLM ℂ (fun (x : ℕ) => ℂ) 1 k

theorem ClassicalComplexWPT.norm_coefficientEval_le (k : ℕ) : ‖coefficientEval k‖ ≤ 1

noncomputable def ClassicalComplexWPT.l1OperatorSeries : FormalMultilinearSeries ℂ ℂ (↥L1Sequence →L[ℂ] ℂ)

The operator-valued series w ↦ (a ↦ ∑ k, a k * w^k).

Equations

• ClassicalComplexWPT.l1OperatorSeries k = (ContinuousMultilinearMap.mkPiAlgebraFin ℂ k ℂ).smulRight (ClassicalComplexWPT.coefficientEval k)

theorem ClassicalComplexWPT.norm_l1OperatorSeries_le (k : ℕ) : ‖l1OperatorSeries k‖ ≤ 1

theorem ClassicalComplexWPT.one_le_radius_l1OperatorSeries : 1 ≤ l1OperatorSeries.radius

noncomputable def ClassicalComplexWPT.l1EvalOperator (w : ℂ) : ↥L1Sequence →L[ℂ] ℂ

The continuous-linear evaluation operator at w.

Equations

• ClassicalComplexWPT.l1EvalOperator w = ClassicalComplexWPT.l1OperatorSeries.sum w

theorem ClassicalComplexWPT.analyticAt_l1EvalOperator : AnalyticAt ℂ l1EvalOperator 0

noncomputable def ClassicalComplexWPT.evalL1PowerSeries (a : ↥L1Sequence) (w : ℂ) : ℂ

Evaluate an ℓ¹ sequence as a one-variable power series.

Equations

• ClassicalComplexWPT.evalL1PowerSeries a w = (ClassicalComplexWPT.l1EvalOperator w) a

theorem ClassicalComplexWPT.analyticAt_evalL1PowerSeries (a : ↥L1Sequence) : AnalyticAt ℂ (fun (x : ↥L1Sequence × ℂ) => evalL1PowerSeries x.1 x.2) (a, 0)

Evaluation is jointly analytic in the sequence and scalar at scalar coordinate zero.

theorem ClassicalComplexWPT.AnalyticAt.evalL1PowerSeries {E : Type u_1} [NormedAddCommGroup E] [NormedSpace ℂ E] {q : E → ↥L1Sequence} (hq : AnalyticAt ℂ q 0) (s : ℂ) : AnalyticAt ℂ (fun (x : E × ℂ) => ClassicalComplexWPT.evalL1PowerSeries (q x.1) (s * x.2)) 0

An analytic family of ℓ¹ coefficients evaluates to a jointly analytic function.

theorem ClassicalComplexWPT.evalL1PowerSeries_eq_tsum (a : ↥L1Sequence) {w : ℂ} (hw : ‖w‖ < 1) : evalL1PowerSeries a w = ∑' (k : ℕ), ↑a k * w ^ k

Inside the unit disc, bundled evaluation is the usual scalar power-series sum.

theorem ClassicalComplexWPT.summable_norm_l1_mul_pow (a : ↥L1Sequence) {w : ℂ} (hw : ‖w‖ ≤ 1) : Summable fun (k : ℕ) => ‖↑a k * w ^ k‖

theorem ClassicalComplexWPT.summable_l1_mul_pow (a : ↥L1Sequence) {w : ℂ} (hw : ‖w‖ ≤ 1) : Summable fun (k : ℕ) => ↑a k * w ^ k

theorem ClassicalComplexWPT.evalL1PowerSeries_convolution (a b : ↥L1Sequence) {w : ℂ} (hw : ‖w‖ < 1) : evalL1PowerSeries (convolution a b) w = evalL1PowerSeries a w * evalL1PowerSeries b w

Evaluation turns ℓ¹ convolution into multiplication inside the unit disc.