From Coefficient Space to Analytic Functions

This file bridges the gap between:

• Coefficient space: ã ∈ ℓ¹_ν with F(ã) = ã ⋆ ã - c = 0
• Function space: x̃(z) = Σ ãₙ zⁿ satisfies x̃(z)² - (λ₀ + z) = 0

Main Results

• l1Weighted.toPowerSeries: Embedding of ℓ¹_ν into formal power series ℝ⟦X⟧
• l1Weighted.eval: Evaluation of power series at points in the disk of convergence
• l1Weighted.eval_mul: Evaluation commutes with multiplication (Mertens' theorem)
• l1Weighted.eval_sq_eq: If F(ã) = 0, then eval(ã, z)² = λ₀ + z
• Example_7_7.analyticSolution_eq_sqrt: Branch selection via IVT shows x̃(λ - λ₀) = √λ

Architecture

We separate the formal and analytic levels:

1. Formal level: l1Weighted.toPowerSeries embeds sequences into PowerSeries ℝ
   • Multiplication in PowerSeries is the Cauchy product by definition
   • No convergence issues at this level
2. Analytic level: l1Weighted.eval evaluates the series at |z| ≤ ν
   • Uses absolute convergence from ℓ¹_ν membership
   • Mertens' theorem shows evaluation commutes with multiplication

References

This completes the formalization of Example 7.7 from the radii polynomial textbook.

Formal Power Series Embedding

def l1Weighted.toPowerSeries {ν : PosReal} (a : ↥(l1Weighted ν)) : PowerSeries ℝ

Embed an ℓ¹_ν sequence as a formal power series in ℝ⟦X⟧

Equations

• l1Weighted.toPowerSeries a = PowerSeries.mk (lpWeighted.toSeq a)

@[simp]

theorem l1Weighted.coeff_toPowerSeries {ν : PosReal} (a : ↥(l1Weighted ν)) (n : ℕ) : (PowerSeries.coeff n) (toPowerSeries a) = lpWeighted.toSeq a n

Coefficient extraction agrees with the underlying sequence

def l1Weighted.paramPowerSeries (lam0 : ℝ) : PowerSeries ℝ

The formal power series for the parameter sequence c = (λ₀, 1, 0, 0, ...)

Equations

• l1Weighted.paramPowerSeries lam0 = PowerSeries.mk (Example_7_7.paramSeq lam0)

@[simp]

theorem l1Weighted.coeff_paramPowerSeries (lam0 : ℝ) (n : ℕ) : (PowerSeries.coeff n) (paramPowerSeries lam0) = Example_7_7.paramSeq lam0 n

theorem l1Weighted.paramPowerSeries_eq (lam0 : ℝ) : paramPowerSeries lam0 = PowerSeries.C lam0 + PowerSeries.X

The parameter series equals C(λ₀) + X in the ring of power series

Cauchy Product is PowerSeries Multiplication

The key insight: multiplication in PowerSeries ℝ is defined as the Cauchy product. This is purely algebraic—no convergence needed at the formal level.

theorem l1Weighted.coeff_mul_eq_cauchyProduct {ν : PosReal} (a b : ↥(l1Weighted ν)) (n : ℕ) : (PowerSeries.coeff n) (toPowerSeries a * toPowerSeries b) = (lpWeighted.toSeq a ⋆ lpWeighted.toSeq b) n

PowerSeries multiplication agrees with Cauchy product coefficient-wise

theorem l1Weighted.coeff_sq_eq_cauchyProduct {ν : PosReal} (a : ↥(l1Weighted ν)) (n : ℕ) : (PowerSeries.coeff n) (toPowerSeries a ^ 2) = (lpWeighted.toSeq a ⋆ lpWeighted.toSeq a) n

Squaring in PowerSeries equals self-convolution

theorem l1Weighted.toPowerSeries_sq_eq_param {ν : PosReal} (a : ↥(l1Weighted ν)) (lam0 : ℝ) (hF : ∀ (n : ℕ), (lpWeighted.toSeq a ⋆ lpWeighted.toSeq a) n = Example_7_7.paramSeq lam0 n) : toPowerSeries a ^ 2 = paramPowerSeries lam0

The fixed-point equation F(a) = 0 means a² = c in PowerSeries

Analytic Evaluation

theorem l1Weighted.norm_term_le {ν : PosReal} {a : ℕ → ℝ} {z : ℝ} (hz : |z| ≤ ↑ν) (n : ℕ) : |a n * z ^ n| ≤ |a n| * ↑ν ^ n

If a ∈ ℓ¹_ν and |z| ≤ ν, then the terms |aₙ zⁿ| are bounded by |aₙ| νⁿ

theorem l1Weighted.summable_eval {ν : PosReal} (a : ↥(l1Weighted ν)) {z : ℝ} (hz : |z| ≤ ↑ν) : Summable fun (n : ℕ) => lpWeighted.toSeq a n * z ^ n

If a ∈ ℓ¹_ν and |z| ≤ ν, then Σ aₙ zⁿ converges absolutely

theorem l1Weighted.summable_abs_eval {ν : PosReal} (a : ↥(l1Weighted ν)) {z : ℝ} (hz : |z| ≤ ↑ν) : Summable fun (n : ℕ) => |lpWeighted.toSeq a n * z ^ n|

Absolute summability

def l1Weighted.eval {ν : PosReal} (a : ↥(l1Weighted ν)) (z : ℝ) : ℝ

Evaluate a power series at z ∈ ℝ with |z| ≤ ν

Equations

• l1Weighted.eval a z = ∑' (n : ℕ), lpWeighted.toSeq a n * z ^ n

theorem l1Weighted.eval_eq_tsum {ν : PosReal} (a : ↥(l1Weighted ν)) (z : ℝ) : eval a z = ∑' (n : ℕ), (PowerSeries.coeff n) (toPowerSeries a) * z ^ n

eval agrees with summing coefficients times powers

Mertens' Theorem: Evaluation Commutes with Multiplication

theorem l1Weighted.eval_mul {ν : PosReal} (a b : ↥(l1Weighted ν)) {z : ℝ} (hz : |z| ≤ ↑ν) : eval a z * eval b z = ∑' (n : ℕ), (lpWeighted.toSeq a ⋆ lpWeighted.toSeq b) n * z ^ n

Key lemma: (Σ aₙ zⁿ) * (Σ bₙ zⁿ) = Σ (a ⋆ b)ₙ zⁿ

theorem l1Weighted.eval_sq {ν : PosReal} (a : ↥(l1Weighted ν)) {z : ℝ} (hz : |z| ≤ ↑ν) : eval a z ^ 2 = ∑' (n : ℕ), (lpWeighted.toSeq a ⋆ lpWeighted.toSeq a) n * z ^ n

Squaring: (Σ aₙ zⁿ)² = Σ (a ⋆ a)ₙ zⁿ

Evaluation of the Parameter Series

theorem l1Weighted.eval_paramSeq (lam0 z : ℝ) : ∑' (n : ℕ), Example_7_7.paramSeq lam0 n * z ^ n = lam0 + z

Σ cₙ zⁿ = λ₀ + z

Main Semantic Theorems

theorem l1Weighted.eval_sq_eq {ν : PosReal} (a : ↥(l1Weighted ν)) (lam0 : ℝ) {z : ℝ} (hz : |z| ≤ ↑ν) (hF : ∀ (n : ℕ), (lpWeighted.toSeq a ⋆ lpWeighted.toSeq a) n = Example_7_7.paramSeq lam0 n) : eval a z ^ 2 = lam0 + z

If F(a) = 0, then eval(a, z)² = λ₀ + z

theorem l1Weighted.eval_zero {ν : PosReal} (a : ↥(l1Weighted ν)) : eval a 0 = lpWeighted.toSeq a 0

eval(a, 0) = a₀

Connection to Example 7.7

@[reducible, inline]

abbrev Example_7_7.analyticSolution {ν : PosReal} (a : ↥(l1Weighted ν)) (z : ℝ) : ℝ

Alias for backward compatibility

Equations

• Example_7_7.analyticSolution a z = l1Weighted.eval a z

theorem Example_7_7.analyticSolution_is_sqrt {ν : PosReal} (aTilde : ↥(l1Weighted ν)) (lam0 : ℝ) (hF : ∀ (n : ℕ), (lpWeighted.toSeq aTilde ⋆ lpWeighted.toSeq aTilde) n = paramSeq lam0 n) {lam : ℝ} (hlam : |lam - lam0| ≤ ↑ν) : analyticSolution aTilde (lam - lam0) ^ 2 = lam

The analytic function x̃(λ) = Σ ãₙ (λ - λ₀)ⁿ satisfies x̃(λ)² = λ

theorem Example_7_7.analyticSolution_eq_sqrt {ν : PosReal} (aTilde : ↥(l1Weighted ν)) (lam0 : ℝ) (hF : ∀ (n : ℕ), (lpWeighted.toSeq aTilde ⋆ lpWeighted.toSeq aTilde) n = paramSeq lam0 n) (hlam0_pos : 0 < lam0) {lam : ℝ} (hlam : |lam - lam0| ≤ ↑ν) (hlam_pos : 0 < lam) (ha0_pos : 0 < lpWeighted.toSeq aTilde 0) : analyticSolution aTilde (lam - lam0) = √lam

The function x̃ defines a branch of √λ near λ₀