Analytic maps into a weighted coefficient space

An ambient formal multilinear series with positive radius determines, after choosing a smaller distinguished-variable radius r, an analytic map from the base variables into ℓ¹(ℕ, ℂ). Its k-th coordinate is r ^ k * lastTaylorCoefficient p k z.

The proof is entirely Archimedean. It uses Mathlib's explicit changeOriginSeries_summable_aux₁ binomial majorant, absolute summability, and the ordinary triangle inequality. In particular, it does not use the ultrametric multiplication estimates for restricted or Gauss-norm power series.

@[reducible, inline]

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

The Banach space of absolutely summable complex sequences.

Equations

• ClassicalComplexWPT.WeightedSeq = lp (fun (x : ℕ) => ℂ) 1

noncomputable def ClassicalComplexWPT.baseInclusion (n : ℕ) : Base n →L[ℂ] Ambient n

Include the base variables into the ambient space at last coordinate zero.

Equations

• ClassicalComplexWPT.baseInclusion n = ContinuousLinearMap.inl ℂ (ClassicalComplexWPT.Base n) ℂ

noncomputable def ClassicalComplexWPT.evalLast (n k : ℕ) : (Ambient n [×k]→L[ℂ] ℂ) →L[ℂ] ℂ

Evaluate a multilinear form on copies of the last coordinate direction.

Equations

• ClassicalComplexWPT.evalLast n k = ContinuousMultilinearMap.apply ℂ (fun (x : Fin k) => ClassicalComplexWPT.Ambient n) ℂ fun (x : Fin k) => ClassicalComplexWPT.lastDirection n

@[simp]

theorem ClassicalComplexWPT.norm_lastDirection (n : ℕ) : ‖lastDirection n‖ = 1

@[simp]

theorem ClassicalComplexWPT.baseInclusion_apply (n : ℕ) (z : Base n) : (baseInclusion n) z = (z, 0)

theorem ClassicalComplexWPT.norm_baseInclusion_le (n : ℕ) : ‖baseInclusion n‖ ≤ 1

theorem ClassicalComplexWPT.norm_evalLast_le (n k : ℕ) : ‖evalLast n k‖ ≤ 1

noncomputable def ClassicalComplexWPT.lastCoefficientSeries {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (k : ℕ) : FormalMultilinearSeries ℂ (Base n) ℂ

The base-variable series for the kth last-coordinate coefficient.

Equations

• One or more equations did not get rendered due to their size.

noncomputable def ClassicalComplexWPT.weightedSingleCLM (r : NNReal) (k : ℕ) : ℂ →L[ℂ] ↥WeightedSeq

Place a scalar in sequence coordinate k, weighted by r ^ k.

Equations

• ClassicalComplexWPT.weightedSingleCLM r k = lp.singleContinuousLinearMap ℂ (fun (x : ℕ) => ℂ) 1 k ∘SL (↑↑r ^ k • ContinuousLinearMap.id ℂ ℂ)

@[simp]

theorem ClassicalComplexWPT.weightedSingleCLM_apply (r : NNReal) (k : ℕ) (z : ℂ) : (weightedSingleCLM r k) z = lp.single 1 k (↑↑r ^ k * z)

theorem ClassicalComplexWPT.norm_weightedSingleCLM_le (r : NNReal) (k : ℕ) : ‖weightedSingleCLM r k‖ ≤ ↑r ^ k

noncomputable def ClassicalComplexWPT.weightedCoordinateSeries {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (k : ℕ) : FormalMultilinearSeries ℂ (Base n) ↥WeightedSeq

The weighted sequence-valued series supported in coordinate k.

Equations

• ClassicalComplexWPT.weightedCoordinateSeries p r k = (ClassicalComplexWPT.weightedSingleCLM r k).compFormalMultilinearSeries (ClassicalComplexWPT.lastCoefficientSeries p k)

noncomputable def ClassicalComplexWPT.weightedCoefficientSeries {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) : FormalMultilinearSeries ℂ (Base n) ↥WeightedSeq

Assemble all weighted last-coordinate coefficient series.

Equations

• ClassicalComplexWPT.weightedCoefficientSeries p r l = ∑' (k : ℕ), ClassicalComplexWPT.weightedCoordinateSeries p r k l

theorem ClassicalComplexWPT.norm_lastCoefficientSeries_le {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (k l : ℕ) : ‖lastCoefficientSeries p k l‖ ≤ ‖p.changeOriginSeries k l‖

theorem ClassicalComplexWPT.norm_weightedCoordinateSeries_le {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (k l : ℕ) : ‖weightedCoordinateSeries p r k l‖ ≤ ↑r ^ k * ‖p.changeOriginSeries k l‖

theorem ClassicalComplexWPT.nnnorm_weightedCoordinateSeries_le {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (k l : ℕ) : ‖weightedCoordinateSeries p r k l‖₊ ≤ ‖p.changeOriginSeries k l‖₊ * r ^ k

@[simp]

theorem ClassicalComplexWPT.weightedCoordinateSeries_apply {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (k l : ℕ) (v : Fin l → Base n) : (weightedCoordinateSeries p r k l) v = lp.single 1 k (↑↑r ^ k * ((p.changeOriginSeries k l) fun (i : Fin l) => (baseInclusion n) (v i)) fun (x : Fin k) => lastDirection n)

theorem ClassicalComplexWPT.radius_weightedLastCoeffs {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (x : Ambient n) (h : ↑‖x‖₊ + ↑r < p.radius) : ↑r < (p.changeOrigin x).radius

theorem ClassicalComplexWPT.summable_nnnorm_changeOriginSeries_mul_pow {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (l : ℕ) : Summable fun (k : ℕ) => ‖p.changeOriginSeries k l‖₊ * r ^ k

The ordinary (Archimedean) majorant needed to sum the weighted coordinate series. This is extracted from Mathlib's changeOriginSeries_summable_aux₁; no ultrametric inequality is used.

theorem ClassicalComplexWPT.summable_weightedCoordinateSeries {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (l : ℕ) : Summable fun (k : ℕ) => weightedCoordinateSeries p r k l

theorem ClassicalComplexWPT.summable_nnnorm_weightedCoordinateSeries {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (l : ℕ) : Summable fun (k : ℕ) => ‖weightedCoordinateSeries p r k l‖₊

theorem ClassicalComplexWPT.nnnorm_weightedCoefficientSeries_le {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (l : ℕ) : ‖weightedCoefficientSeries p r l‖₊ ≤ ∑' (k : ℕ), ‖p.changeOriginSeries k l‖₊ * r ^ k

theorem ClassicalComplexWPT.weightedCoefficientSeries_apply {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) (l : ℕ) (v : Fin l → Base n) (j : ℕ) : ↑((weightedCoefficientSeries p r l) v) j = ↑↑r ^ j * ((p.changeOriginSeries j l) fun (i : Fin l) => (baseInclusion n) (v i)) fun (x : Fin j) => lastDirection n

theorem ClassicalComplexWPT.summable_changeOrigin_weighted_majorant {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (s r : NNReal) (hsr : ↑s + ↑r < p.radius) : Summable fun (l : ℕ) => (∑' (k : ℕ), ‖p.changeOriginSeries k l‖₊ * r ^ k) * s ^ l

theorem ClassicalComplexWPT.le_radius_weightedCoefficientSeries {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (s r : NNReal) (hsr : ↑s + ↑r < p.radius) : ↑s ≤ (weightedCoefficientSeries p r).radius

theorem ClassicalComplexWPT.radius_weightedCoefficientSeries_pos {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) : 0 < (weightedCoefficientSeries p r).radius

theorem ClassicalComplexWPT.analyticAt_weightedCoefficientSeries_sum {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (hr : ↑r < p.radius) : AnalyticAt ℂ (weightedCoefficientSeries p r).sum 0

theorem ClassicalComplexWPT.AnalyticAt.exists_analytic_weightedCoefficientMap {n : ℕ} {f : Ambient n → ℂ} (hf : AnalyticAt ℂ f 0) : ∃ (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal), HasFPowerSeriesAt f p 0 ∧ 0 < r ∧ AnalyticAt ℂ (weightedCoefficientSeries p r).sum 0

theorem ClassicalComplexWPT.weightedCoefficientSeries_sum_apply {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (z : Base n) (j : ℕ) (hr : ↑r < p.radius) (hzq : z ∈ Metric.eball 0 (weightedCoefficientSeries p r).radius) (hzp : (baseInclusion n) z ∈ Metric.eball 0 p.radius) : ↑((weightedCoefficientSeries p r).sum z) j = ↑↑r ^ j * (p.changeOrigin ((baseInclusion n) z) j) fun (x : Fin j) => lastDirection n

On the common convergence neighborhood, the j-th coordinate of the ℓ¹-valued analytic sum is exactly the weighted moving Taylor coefficient.

theorem ClassicalComplexWPT.weightedCoefficientSeries_sum_apply_lastTaylorCoefficient {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (z : Base n) (j : ℕ) (hr : ↑r < p.radius) (hzq : z ∈ Metric.eball 0 (weightedCoefficientSeries p r).radius) (hzp : (z, 0) ∈ Metric.eball 0 p.radius) : ↑((weightedCoefficientSeries p r).sum z) j = ↑↑r ^ j * lastTaylorCoefficient p j z

noncomputable def ClassicalComplexWPT.weightedLastCoeffs {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (x : Ambient n) (hr : ↑r < (p.changeOrigin x).radius) : ↥WeightedSeq

The weighted last-direction Taylor coefficients at an ambient point.

Equations

• ClassicalComplexWPT.weightedLastCoeffs p r x hr = ⟨fun (k : ℕ) => ↑↑r ^ k * (p.changeOrigin x k) fun (x : Fin k) => ClassicalComplexWPT.lastDirection n, ⋯⟩

@[simp]

theorem ClassicalComplexWPT.weightedLastCoeffs_apply {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (x : Ambient n) (hr : ↑r < (p.changeOrigin x).radius) (k : ℕ) : ↑(weightedLastCoeffs p r x hr) k = ↑↑r ^ k * (p.changeOrigin x k) fun (x : Fin k) => lastDirection n

theorem ClassicalComplexWPT.norm_weightedLastCoeffs_le {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (r : NNReal) (x : Ambient n) (hr : ↑r < (p.changeOrigin x).radius) : ‖weightedLastCoeffs p r x hr‖ ≤ ∑' (k : ℕ), ‖p.changeOrigin x k‖ * ↑r ^ k

theorem ClassicalComplexWPT.exists_weightedLastCoeffs_on_baseBall {n : ℕ} (p : FormalMultilinearSeries ℂ (Ambient n) ℂ) (s r : NNReal) (hsr : ↑s + ↑r < p.radius) {z : Base n} (hz : z ∈ Metric.eball 0 ↑s) : ∃ (c : ↥WeightedSeq), (∀ (k : ℕ), ↑c k = ↑↑r ^ k * lastTaylorCoefficient p k z) ∧ ‖c‖ ≤ ∑' (k : ℕ), ‖p.changeOrigin (z, 0) k‖ * ↑r ^ k

Explicit ℓ¹ membership and norm control, uniformly on any smaller base ball whose radius plus the distinguished weight stays inside p.radius.