Example 7.7: Taylor Series Solution of Parameterized Equilibria

We prove existence of the curve x(λ) satisfying x(λ)² - λ = 0 near lam0 using the radii polynomial approach from Section 7.7.

The Problem

Given the equation x² - λ = 0 with f(x₀, lam0) = 0 where x₀ = √lam0, find a Taylor series x(λ) = Σₙ aₙ(λ - lam0)ⁿ satisfying the equation.

Taylor Series Formulation

Substituting x(λ) = Σₙ aₙ(λ - lam0)ⁿ into x² - λ = 0:

• LHS: (Σₙ aₙtⁿ)² = Σₙ (a ⋆ a)ₙ tⁿ (Cauchy product)
• RHS: λ = lam0 + t where t = λ - lam0

This gives the zero-finding problem: F(a) = a ⋆ a - c = 0 where c = (lam0, 1, 0, 0, ...).

The Operator Structure

Following Theorem 7.7.1, the operators have block-diagonal structure:

• A† (approximate derivative): DF⁽ᴺ⁾(ā) on indices 0..N, 2ā₀ on tail
• A (approximate inverse): (DF⁽ᴺ⁾(ā))⁻¹ on indices 0..N, 1/(2ā₀) on tail

This matches the BlockDiagOp structure from OperatorNorm.lean.

Main Results

• paramSeqSpace: The constant sequence c = (lam0, 1, 0, 0, ...)
• F_eq_sq_sub: F(a) = a ⋆ a - c
• DF_eq_two_leftMul: DF(a)h = 2(a ⋆ h)
• Y₀_bound, Z₀_bound, Z₁_bound, Z₂_bound: The bounds from Theorem 7.7.1
• existence_theorem: Application of Theorem 7.6.2

References

• Section 7.7: Taylor series solution of parameterized equilibria
• Theorem 7.7.1: The radii polynomial bounds
• Equation (7.40): x² - λ = 0
• Equations (7.41)-(7.43): The sequence formulation

The Constant Sequence c

For the equation x² - λ = 0 expanded around lam0, the constant sequence is: c = (lam0, 1, 0, 0, ...)

This encodes λ = lam0 + (λ - lam0) in Taylor coefficients.

def Example_7_7.paramSeq (lam0 : ℝ) : ℕ → ℝ

The constant sequence c = (lam0, 1, 0, 0, ...) from equation (7.44). This encodes λ = lam0 + t where t = λ - lam0.

Equations

• Example_7_7.paramSeq lam0 0 = lam0
• Example_7_7.paramSeq lam0 1 = 1
• Example_7_7.paramSeq lam0 n = 0

theorem Example_7_7.paramSeq_mem {ν : PosReal} (lam0 : ℝ) : lpWeighted.Mem ν 1 (paramSeq lam0)

The constant sequence is in ℓ¹_ν

def Example_7_7.c {ν : PosReal} (lam0 : ℝ) : ↥(l1Weighted ν)

The constant sequence as an element of ℓ¹_ν

Equations

• Example_7_7.c lam0 = lpWeighted.mk (Example_7_7.paramSeq lam0) ⋯

@[simp]

theorem Example_7_7.c_zero {ν : PosReal} (lam0 : ℝ) : lpWeighted.toSeq (c lam0) 0 = lam0

c₀ = lam0

@[simp]

theorem Example_7_7.c_one {ν : PosReal} (lam0 : ℝ) : lpWeighted.toSeq (c lam0) 1 = 1

c₁ = 1

@[simp]

theorem Example_7_7.c_ge_two {ν : PosReal} (lam0 : ℝ) (n : ℕ) (hn : 2 ≤ n) : lpWeighted.toSeq (c lam0) n = 0

cₙ = 0 for n ≥ 2

theorem Example_7_7.norm_c {ν : PosReal} (lam0 : ℝ) : ‖c lam0‖ = |lam0| + ↑ν

Norm of c: ‖c‖ = |lam0| + ν

The Zero-Finding Map F

The map F(a) = a ⋆ a - c from equation (7.43).

def Example_7_7.F {ν : PosReal} (lam0 : ℝ) (a : ↥(l1Weighted ν)) : ↥(l1Weighted ν)

The zero-finding map F(a) = a ⋆ a - c

Equations

• Example_7_7.F lam0 a = l1Weighted.F_sub_const (Example_7_7.c lam0) a

theorem Example_7_7.F_eq {ν : PosReal} (lam0 : ℝ) (a : ↥(l1Weighted ν)) : F lam0 a = l1Weighted.sq a - c lam0

F(a) = sq(a) - c

theorem Example_7_7.F_component {ν : PosReal} (lam0 : ℝ) (a : ↥(l1Weighted ν)) (n : ℕ) : lpWeighted.toSeq (F lam0 a) n = (lpWeighted.toSeq a ⋆ lpWeighted.toSeq a) n - lpWeighted.toSeq (c lam0) n

Component formula for F (equation 7.43): F₀(a) = a₀² - lam0 F₁(a) = 2a₀a₁ - 1 Fₙ(a) = (a ⋆ a)ₙ for n ≥ 2

theorem Example_7_7.differentiable_F {ν : PosReal} (lam0 : ℝ) : Differentiable ℝ (F lam0)

F is Fréchet differentiable

theorem Example_7_7.fderiv_F {ν : PosReal} (lam0 : ℝ) (a : ↥(l1Weighted ν)) : fderiv ℝ (F lam0) a = 2 • l1Weighted.leftMul a

The Fréchet derivative: DF(a)h = 2(a ⋆ h)

The Approximate Solution

For the concrete example with lam0 = 1/3, we have: ā₀ ≈ √(1/3) ≈ 0.577... ā₁ ≈ 1/(2ā₀) ≈ 0.866... etc.

The approximate solution satisfies F⁽ᴺ⁾(ā⁽ᴺ⁾) ≈ 0 for the truncated system.

structure Example_7_7.ApproxSolution (N : ℕ) : Type

Structure for an approximate solution (eq. 7.46)

• aBar_fin : Fin (N + 1) → ℝ

  The truncated approximate solution ā⁽ᴺ⁾ ∈ ℝᴺ⁺¹

• aBar_zero_ne : self.aBar_fin 0 ≠ 0

  Assumption: ā₀ ≠ 0 (needed for invertibility)

def Example_7_7.ApproxSolution.toSeq {N : ℕ} (sol : ApproxSolution N) : ℕ → ℝ

Extend the finite approximate solution to a sequence (zero-padded)

Equations

• sol.toSeq n = if h : n ≤ N then sol.aBar_fin ⟨n, ⋯⟩ else 0

theorem Example_7_7.ApproxSolution.mem {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) : lpWeighted.Mem ν 1 sol.toSeq

The extended sequence is in ℓ¹_ν

def Example_7_7.ApproxSolution.toL1 {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) : ↥(l1Weighted ν)

The approximate solution as an element of ℓ¹_ν

Equations

• sol.toL1 = lpWeighted.mk sol.toSeq ⋯

@[simp]

theorem Example_7_7.ApproxSolution.toL1_toSeq {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) : lpWeighted.toSeq sol.toL1 = sol.toSeq

The Block-Diagonal Operator Structure

Following Theorem 7.7.1, the operators A† and A have block-diagonal structure:

A† = [DF⁽ᴺ⁾(ā), 0 ; 0 , 2ā₀·I] A = [(DF⁽ᴺ⁾(ā))⁻¹, 0 ; 0 , (1/2ā₀)·I]

This matches the BlockDiagOp structure from OperatorNorm.lean.

Computed Finite Projections

These definitions compute F⁽ᴺ⁾(ā) and DF⁽ᴺ⁾(ā) directly from the definitions, rather than taking them as hypotheses. This is more honest to the textbook setup.

def Example_7_7.F_fin {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) : Fin (N + 1) → ℝ

F⁽ᴺ⁾(ā): the first N+1 components of F(ā) = ā⋆ā - c

Equations

• Example_7_7.F_fin lam0 sol n = lpWeighted.toSeq (Example_7_7.F lam0 sol.toL1) ↑n

def Example_7_7.DF_fin {N : ℕ} (sol : ApproxSolution N) : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ

DF⁽ᴺ⁾(ā): the (N+1)×(N+1) lower triangular matrix with entries 2āᵢ₋ⱼ for j ≤ i

Equations

• Example_7_7.DF_fin sol = Matrix.of fun (i j : Fin (N + 1)) => if h : ↑j ≤ ↑i then 2 * sol.aBar_fin ⟨↑i - ↑j, ⋯⟩ else 0

def Example_7_7.approxInverse {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : BlockDiag.BlockDiagOp ν N

The approximate inverse A as a block-diagonal operator (equation 7.48).

• Finite block: A⁽ᴺ⁾ (numerical inverse of DF⁽ᴺ⁾(ā))
• Tail scalar: 1/(2ā₀)

Equations

• Example_7_7.approxInverse sol A_fin = { finBlock := A_fin, tailScalar := 1 / (2 * sol.aBar_fin 0) }

def Example_7_7.approxDeriv {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) : BlockDiag.BlockDiagOp ν N

The approximate derivative A† as a block-diagonal operator (equation 7.47).

• Finite block: DF⁽ᴺ⁾(ā) = lower triangular with (DF){i,j} = 2ā{i-j} for j ≤ i, 0 otherwise
• Tail scalar: 2ā₀

Equations

• Example_7_7.approxDeriv sol = { finBlock := Matrix.of fun (i j : Fin (N + 1)) => if ↑j ≤ ↑i then 2 * sol.aBar_fin ⟨↑i - ↑j, ⋯⟩ else 0, tailScalar := 2 * sol.aBar_fin 0 }

The Radii Polynomial Bounds (Theorem 7.7.1)

We now define the Y₀, Z₀, Z₁, Z₂ bounds.

def Example_7_7.Y₀_bound {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : ℝ

Y₀ bound (equation from Theorem 7.7.1): Y₀ = Σₙ₌₀ᴺ |[A⁽ᴺ⁾F⁽ᴺ⁾(ā)]ₙ| νⁿ + (1/2|ā₀|) Σₙ₌ₙ₊₁²ᴺ (Σⱼ₌₀^{2N-n} |ā_{N-j}||ā_{n-N+j}|) νⁿ

Equivalently with index k = N - j: Σₖ₌ₙ₋ₙᴺ |āₖ||āₙ₋ₖ|

Note: The textbook has a typo with inner sum ∑ⱼ₌₀^{N-n} but this is empty for n > N. The correct range is ∑ⱼ₌₀^{2N-n}, which corresponds to k ∈ [n-N, N].

This measures how close ā is to being a true solution.

Equations

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

def Example_7_7.Z₀_bound {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : ℝ

Z₀ bound (equation from Theorem 7.7.1): Z₀ = ‖I - A⁽ᴺ⁾DF⁽ᴺ⁾(ā)‖_{1,ν}

This measures how well A⁽ᴺ⁾ inverts DF⁽ᴺ⁾(ā).

Equations

• Example_7_7.Z₀_bound sol A_fin = l1Weighted.finWeightedMatrixNorm ν (1 - A_fin * Example_7_7.DF_fin sol)

def Example_7_7.Z₁_bound {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) : ℝ

Z₁ bound (equation from Theorem 7.7.1): Z₁ = (1/|ā₀|) Σₙ₌₁ᴺ |āₙ| νⁿ

This measures the tail contribution from DF(ā) - A†.

Equations

• Example_7_7.Z₁_bound sol = 1 / |sol.aBar_fin 0| * ∑ n ∈ Finset.Icc 1 N, |sol.toSeq n| * ↑ν ^ n

def Example_7_7.Z₂_bound {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : ℝ

Z₂ bound (equation from Theorem 7.7.1): Z₂ = 2 max(‖A⁽ᴺ⁾‖_{1,ν}, 1/(2|ā₀|))

This bounds ‖A[DF(c) - DF(ā)]‖ for c in a ball around ā.

Equations

• Example_7_7.Z₂_bound sol A_fin = 2 * max (l1Weighted.finWeightedMatrixNorm ν A_fin) (1 / (2 * |sol.aBar_fin 0|))

def Example_7_7.radiiPoly_7_7 {ν : PosReal} (N : ℕ) (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (r : ℝ) : ℝ

The radii polynomial for Example 7.7, using the general definition from RadiiPolyGeneral.lean.

Note: Z₂ is constant in this example (doesn't depend on r).

Equations

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

Helper Lemmas for Y₀ Bound (Theorem 7.7.1)

These lemmas break down the proof of Y₀_bound_valid into manageable subgoals.

Key observations:

1. ā is zero-padded: āₙ = 0 for n > N
2. Therefore (ā ⋆ ā)ₙ = 0 for n > 2N
3. F(ā) = ā ⋆ ā - c where c = (λ₀, 1, 0, 0, ...)
4. The block-diagonal operator A acts as A⁽ᴺ⁾ on [0,N] and 1/(2ā₀) on (N,∞)

theorem Example_7_7.toSeq_zero_of_gt {N : ℕ} (sol : ApproxSolution N) (n : ℕ) (hn : N < n) : sol.toSeq n = 0

āₙ = 0 for n > N, where ā = ApproxSolution.toSeq sol = (ā₀, ā₁, ..., āₙ, 0, 0, 0, ...)

theorem Example_7_7.toSeq_eq_aBar_fin {N : ℕ} (sol : ApproxSolution N) (n : Fin (N + 1)) : sol.toSeq ↑n = sol.aBar_fin n

The finite part of ā equals ā_fin

theorem Example_7_7.cauchyProduct_toSeq_zero_of_gt_two_N {N : ℕ} (sol : ApproxSolution N) (n : ℕ) (hn : 2 * N < n) : (sol.toSeq ⋆ sol.toSeq) n = 0

(ā ⋆ ā)ₙ = 0 for n > 2N since ā has support in [0,N]

theorem Example_7_7.F_component_tail' (lam0 : ℝ) (a : ℕ → ℝ) (n : ℕ) (hn : 2 ≤ n) : (a ⋆ a) n - paramSeq lam0 n = (a ⋆ a) n

F(ā)ₙ = (ā ⋆ ā)ₙ for n ≥ 2, since cₙ = 0, where c = (λ₀, 1, 0, 0, ...)

theorem Example_7_7.F_toSeq_zero_of_gt_two_N {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (n : ℕ) (hN : 0 < N) (hn : 2 * N < n) : (sol.toSeq ⋆ sol.toSeq) n - paramSeq lam0 n = 0

F(ā)ₙ = 0 for n > 2N (requires N ≥ 1)

theorem Example_7_7.approxInverse_action_finite {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (x : ℕ → ℝ) (n : ℕ) (hn : n ≤ N) : (approxInverse sol A_fin).action x n = ∑ j : Fin (N + 1), A_fin ⟨n, ⋯⟩ j * x ↑j

Action of approxInverse A on finite indices (n ≤ N) Needed to compute [A(F(ā))]ₙ for 0 ≤ n ≤ N

theorem Example_7_7.approxInverse_action_tail {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (x : ℕ → ℝ) (n : ℕ) (hn : N < n) : (approxInverse sol A_fin).action x n = 1 / (2 * sol.aBar_fin 0) * x n

Action of approxInverse A on tail indices (n > N) Needed to compute [A(F(ā))]ₙ for N < n ≤ 2N

theorem Example_7_7.approxInverse_F_action_zero_of_gt_two_N {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (n : ℕ) (hN : 0 < N) (hn : 2 * N < n) : (approxInverse sol A_fin).action (fun (k : ℕ) => (sol.toSeq ⋆ sol.toSeq) k - paramSeq lam0 k) n = 0

[A(F(ā))]ₙ = 0 for n > 2N

theorem Example_7_7.tail_tsum_eq_Icc_sum {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (hN : 0 < N) : ∑' (n : { n : ℕ // N < n }), |(approxInverse sol A_fin).action (fun (k : ℕ) => (sol.toSeq ⋆ sol.toSeq) k - paramSeq lam0 k) ↑n| * ↑ν ^ ↑n = ∑ n ∈ Finset.Icc (N + 1) (2 * N), |(approxInverse sol A_fin).action (fun (k : ℕ) => (sol.toSeq ⋆ sol.toSeq) k - paramSeq lam0 k) n| * ↑ν ^ n

‖A(F(ā))‖₁,ν (in summation notation) is a finite sum over [N+1, 2N]

theorem Example_7_7.cauchyProduct_middle_range {N : ℕ} (sol : ApproxSolution N) (n : ℕ) (hn_lower : N + 1 ≤ n) : (sol.toSeq ⋆ sol.toSeq) n = ∑ k ∈ Finset.Icc (n - N) N, sol.toSeq k * sol.toSeq (n - k)

Range of nonzero terms in Cauchy product for N < n ≤ 2N

theorem Example_7_7.cauchyProduct_middle_abs_bound {N : ℕ} (sol : ApproxSolution N) (n : ℕ) (hn_lower : N + 1 ≤ n) : |(sol.toSeq ⋆ sol.toSeq) n| ≤ ∑ k ∈ Finset.Icc (n - N) N, |sol.toSeq k| * |sol.toSeq (n - k)|

Bound on middle Cauchy product using absolute values

Helper Lemmas for Z₀ Bound (Theorem 7.7.1)

These lemmas break down the proof of Z₀_bound_valid into manageable subgoals.

Key observations from the textbook (page 173):

1. approxDeriv.finBlock = DF_fin sol (both are 2āᵢ₋ⱼ)
2. Tail scalars multiply to 1: (1/(2ā₀)) * (2ā₀) = 1
3. Therefore I - AA† = 0 on tail
4. On finite: I - AA† = I - A_fin * DF_fin

theorem Example_7_7.approxDeriv_finBlock_eq_DF_fin {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) : (approxDeriv sol).finBlock = DF_fin sol

approxDeriv finite block equals DF_fin

theorem Example_7_7.tail_scalars_mul_eq_one {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (h : sol.aBar_fin 0 ≠ 0) : (approxInverse sol A_fin).tailScalar * (approxDeriv sol).tailScalar = 1

Tail scalars of A and A† multiply to 1

theorem Example_7_7.comp_tail_scalar_eq_one {N : ℕ} (sol : ApproxSolution N) (h : sol.aBar_fin 0 ≠ 0) : 1 / (2 * sol.aBar_fin 0) * (2 * sol.aBar_fin 0) = 1

The composition AA† has tail scalar 1

theorem Example_7_7.approxDeriv_toSeq_eq_action {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (h : ↥(l1Weighted ν)) : lpWeighted.toSeq ((approxDeriv sol).toCLM h) = (approxDeriv sol).action (lpWeighted.toSeq h)

toSeq of A†.toCLM equals A†.action of toSeq

theorem Example_7_7.approxInverse_toSeq_eq_action {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (h : ↥(l1Weighted ν)) : lpWeighted.toSeq ((approxInverse sol A_fin).toCLM h) = (approxInverse sol A_fin).action (lpWeighted.toSeq h)

toSeq of A.toCLM equals A.action of toSeq

theorem Example_7_7.I_sub_comp_action_tail_eq_zero {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (h : ↥(l1Weighted ν)) (n : ℕ) (hn : N < n) : lpWeighted.toSeq h n - lpWeighted.toSeq ((approxInverse sol A_fin).toCLM ((approxDeriv sol).toCLM h)) n = 0

Action of (I - AA†) on tail is zero

theorem Example_7_7.I_sub_comp_action_finite_eq {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (h : ↥(l1Weighted ν)) (n : Fin (N + 1)) : lpWeighted.toSeq h ↑n - lpWeighted.toSeq ((approxInverse sol A_fin).toCLM ((approxDeriv sol).toCLM h)) ↑n = ∑ j : Fin (N + 1), (1 - A_fin * (approxDeriv sol).finBlock) n j * lpWeighted.toSeq h ↑j

Action of (I - AA†) on finite equals (I - A_fin * DF_fin) h^(N)

theorem Example_7_7.I_sub_comp_tail_tsum_zero {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (h : ↥(l1Weighted ν)) : ∑' (n : { n : ℕ // N < n }), |lpWeighted.toSeq ((ContinuousLinearMap.id ℝ ↥(l1Weighted ν) - (approxInverse sol A_fin).toCLM.comp (approxDeriv sol).toCLM) h) ↑n| * ↑ν ^ ↑n = 0

The tail contribution of (I - AA†)h is zero in the ℓ¹_ν norm. This follows from I_sub_comp_action_tail_eq_zero: each term is zero.

theorem Example_7_7.I_sub_comp_finite_toSeq_eq {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (h : ↥(l1Weighted ν)) (n : Fin (N + 1)) : lpWeighted.toSeq ((ContinuousLinearMap.id ℝ ↥(l1Weighted ν) - (approxInverse sol A_fin).toCLM.comp (approxDeriv sol).toCLM) h) ↑n = ∑ j : Fin (N + 1), (1 - A_fin * (approxDeriv sol).finBlock) n j * lpWeighted.toSeq h ↑j

The finite part of (I - AA†)h equals (I - A_fin * DF_fin) applied to h^(N). Converts CLM action to matrix multiplication form.

theorem Example_7_7.DF_sub_approxDeriv_finite_eq_zero {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (h : ↥(l1Weighted ν)) (n : Fin (N + 1)) : lpWeighted.toSeq ((fderiv ℝ (F lam0) sol.toL1) h - (approxDeriv sol).toCLM h) ↑n = 0

DF(ā) - A† is zero on finite block [0,N]. From page 173: [(DF(ā) - A†)h]_n = [DF^(N)(ā)h^(N)]_n - [DF^(N)(ā)h^(N)]_n = 0 Both operators agree on finite because A† IS defined as DF^(N)(ā) on this block.

theorem Example_7_7.DF_sub_approxDeriv_tail {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (h : ↥(l1Weighted ν)) (n : ℕ) (hn : N < n) : lpWeighted.toSeq ((fderiv ℝ (F lam0) sol.toL1) h - (approxDeriv sol).toCLM h) n = 2 * ∑ j ∈ Finset.Icc 1 N, lpWeighted.toSeq h (n - j) * sol.toSeq j

DF(ā) - A† on tail (n > N) equals 2∑{j=1}^N h{n-j}ā_j. Since ā_k = 0 for k > N, (ā⋆h)n - ā₀h_n = ∑{j=1}^N h_{n-j}ā_j.

theorem Example_7_7.A_DF_sub_approxDeriv_finite_eq_zero {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (h : ↥(l1Weighted ν)) (n : Fin (N + 1)) : lpWeighted.toSeq ((approxInverse sol A_fin).toCLM ((fderiv ℝ (F lam0) sol.toL1) h - (approxDeriv sol).toCLM h)) ↑n = 0

A(DF(ā) - A†) is zero on finite block. Since DF(ā) - A† = 0 on finite, applying A preserves this.

theorem Example_7_7.A_DF_sub_approxDeriv_tail {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (h : ↥(l1Weighted ν)) (n : ℕ) (hn : N < n) : lpWeighted.toSeq ((approxInverse sol A_fin).toCLM ((fderiv ℝ (F lam0) sol.toL1) h - (approxDeriv sol).toCLM h)) n = 1 / sol.aBar_fin 0 * ∑ j ∈ Finset.Icc 1 N, lpWeighted.toSeq h (n - j) * sol.toSeq j

A(DF(ā) - A†) on tail equals (1/ā₀)∑{j=1}^N h{n-j}ā_j. From textbook page 174.

def Example_7_7.shiftedSeq {N : ℕ} (sol : ApproxSolution N) : ℕ → ℝ

The shifted sequence â = (0, ā₁, ..., āₙ, 0, ...) used in Z₁ bound

Equations

• Example_7_7.shiftedSeq sol k = if k ∈ Finset.Icc 1 N then sol.toSeq k else 0

theorem Example_7_7.shiftedSeq_support {N : ℕ} (sol : ApproxSolution N) (k : ℕ) (hk : k ∉ Finset.Icc 1 N) : shiftedSeq sol k = 0

The shifted sequence has finite support in [1, N]

theorem Example_7_7.inner_sum_eq_cauchy {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (h : ↥(l1Weighted ν)) (n : ℕ) (hn : N < n) : ∑ j ∈ Finset.Icc 1 N, lpWeighted.toSeq h (n - j) * sol.toSeq j = (lpWeighted.toSeq h ⋆ shiftedSeq sol) n

Inner sum equals Cauchy product for n > N

theorem Example_7_7.shiftedSeq_mem {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) : lpWeighted.Mem ν 1 (shiftedSeq sol)

The shifted sequence is in ℓ¹_ν (finite support)

def Example_7_7.shiftedL1 {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) : ↥(l1Weighted ν)

The shifted sequence as an element of ℓ¹_ν

Equations

• Example_7_7.shiftedL1 sol = lpWeighted.mk (Example_7_7.shiftedSeq sol) ⋯

theorem Example_7_7.shiftedL1_norm {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) : ‖shiftedL1 sol‖ = ∑ n ∈ Finset.Icc 1 N, |sol.toSeq n| * ↑ν ^ n

Norm of shifted sequence equals finite sum

theorem Example_7_7.tail_cauchy_bound {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (h : ↥(l1Weighted ν)) : ∑' (n : { n : ℕ // N < n }), |∑ j ∈ Finset.Icc 1 N, lpWeighted.toSeq h (↑n - j) * sol.toSeq j| * ↑ν ^ ↑n ≤ ‖h‖ * ∑ n ∈ Finset.Icc 1 N, |sol.toSeq n| * ↑ν ^ n

Key bound for Z₁: tail sum bounded by Cauchy product norm

Z₂ Bound Helper Lemmas

From the textbook proof (page 174):

1. Since DF(a)h = 2a⋆h, we have DF(c) - DF(ā) = 2(c-ā)⋆(·)
2. Thus ‖A(DF(c) - DF(ā))‖ ≤ 2‖A‖·‖c-ā‖ ≤ 2‖A‖·r
3. For block-diagonal A: ‖A‖ ≤ max(‖A_fin‖_{1,ν}, 1/(2|ā₀|)) by Proposition 7.3.14
4. Hence Z₂ = 2·max(‖A_fin‖_{1,ν}, 1/(2|ā₀|))

theorem Example_7_7.leftMul_sub {ν : PosReal} (a b : ↥(l1Weighted ν)) : l1Weighted.leftMul (a - b) = l1Weighted.leftMul a - l1Weighted.leftMul b

Subtraction distributes over leftMul: leftMul (a - b) = leftMul a - leftMul b Follows from leftMul_add and leftMul_smul.

theorem Example_7_7.fderiv_F_diff_eq_leftMul_diff {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (c : ↥(l1Weighted ν)) : fderiv ℝ (F lam0) c - fderiv ℝ (F lam0) sol.toL1 = 2 • l1Weighted.leftMul (c - sol.toL1)

The difference of Fréchet derivatives equals 2·leftMul(c - ā). From textbook: Since DF(a)h = 2a⋆h, we have DF(c) - DF(ā) = 2(c-ā)⋆(·)

theorem Example_7_7.norm_fderiv_F_diff_le {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (c : ↥(l1Weighted ν)) : ‖fderiv ℝ (F lam0) c - fderiv ℝ (F lam0) sol.toL1‖ ≤ 2 * ‖c - sol.toL1‖

Operator norm bound on the derivative difference: ‖DF(c) - DF(ā)‖ ≤ 2·‖c - ā‖ Uses: ‖2·leftMul(c-ā)‖ ≤ 2·‖leftMul(c-ā)‖ ≤ 2·‖c-ā‖

theorem Example_7_7.approxInverse_norm_le {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : ‖(approxInverse sol A_fin).toCLM‖ ≤ max (l1Weighted.finWeightedMatrixNorm ν A_fin) (1 / (2 * |sol.aBar_fin 0|))

Operator norm bound for approxInverse A: ‖A‖ ≤ max(‖A_fin‖_{1,ν}, 1/(2|ā₀|)) This is Proposition 7.3.14 applied to the specific block-diagonal structure of A.

theorem Example_7_7.Z₂_bound_eq_two_mul_max {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : Z₂_bound sol A_fin = 2 * max (l1Weighted.finWeightedMatrixNorm ν A_fin) (1 / (2 * |sol.aBar_fin 0|))

The Z₂ bound equals 2 times the operator norm bound for A

Bound Verification Lemmas (Theorem 7.7.1)

These lemmas verify that the computable bounds Y₀, Z₀, Z₁, Z₂ satisfy the hypotheses of general_radii_polynomial_theorem.

theorem Example_7_7.Y₀_bound_valid {ν : PosReal} (N : ℕ) (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (hN : 0 < N) : ‖(approxInverse sol A_fin).toCLM (F lam0 sol.toL1)‖ ≤ Y₀_bound lam0 sol A_fin

Y₀ bound verification: ‖A(F(ā))‖ ≤ Y₀

theorem Example_7_7.Z₀_bound_valid {ν : PosReal} (N : ℕ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : ‖ContinuousLinearMap.id ℝ ↥(l1Weighted ν) - (approxInverse sol A_fin).toCLM.comp (approxDeriv sol).toCLM‖ ≤ Z₀_bound sol A_fin

Z₀ bound verification: ‖I - AA†‖ ≤ Z₀

From the textbook proof (page 173):

• On finite [0,N]: (I - AA†)h = (I - A_fin·DF_fin)h^(N)
• On tail (n > N): (I - AA†)h = 0 (since tail scalars multiply to 1)

Therefore ‖I - AA†‖ = ‖I - A_fin·DF_fin‖_{1,ν} = Z₀

theorem Example_7_7.Z₁_bound_valid {ν : PosReal} (N : ℕ) (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : ‖(approxInverse sol A_fin).toCLM.comp ((approxDeriv sol).toCLM - fderiv ℝ (F lam0) sol.toL1)‖ ≤ Z₁_bound sol

Z₁ bound verification: ‖A(A† - DF(ā))‖ ≤ Z₁

From the textbook proof (page 173-174):

• On finite [0,N]: (A† - DF(ā))h = 0 (they agree on finite block)
• On tail (n > N): (A† - DF(ā))h = 2ā₀h_n - 2(ā⋆h)n = -2∑{j=1}^N h_{n-j}ā_j

Therefore [A(A† - DF(ā))h]n = (1/ā₀)∑{j=1}^N h_{n-j}ā_j for n > N, and 0 for n ≤ N.

The bound uses: ‖A(A† - DF(ā))‖ ≤ (1/|ā₀|)‖ā‖ where ā is restricted to [1,N].

theorem Example_7_7.Z₂_bound_valid {ν : PosReal} (N : ℕ) (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (r : ℝ) (c : ↥(l1Weighted ν)) (hc : c ∈ Metric.closedBall sol.toL1 r) : ‖(approxInverse sol A_fin).toCLM.comp (fderiv ℝ (F lam0) c - fderiv ℝ (F lam0) sol.toL1)‖ ≤ Z₂_bound sol A_fin * r

Z₂ bound verification: ‖A(DF(c) - DF(ā))‖ ≤ Z₂·r for c ∈ B̄ᵣ(ā)

From the textbook proof (page 174): Since DF(a)h = 2a⋆h, we have DF(c) - DF(ā) = 2(c-ā)⋆(·) Thus ‖A(DF(c) - DF(ā))‖ ≤ 2‖A‖·‖c-ā‖ ≤ 2‖A‖·r

For block-diagonal A: ‖A‖ ≤ max(‖A_fin‖{1,ν}, 1/(2|ā₀|)) Hence Z₂ = 2·max(‖A_fin‖{1,ν}, 1/(2|ā₀|))

Injectivity Helper Lemmas

From the textbook (page 168), Proposition 7.6.5:

1. p(r₀) < 0 with r₀ > 0 implies Z₀ + Z₁ + Z₂r₀ < 1
2. Since Z₂r₀ ≥ 0, we have Z₀ + Z₁ < 1
3. Since Z₁ ≥ 0, we have Z₀ < 1
4. Z₀ < 1 implies ‖I - A_fin · DF_fin‖ < 1, so A_fin · DF_fin is invertible
5. For square matrices, if AB is invertible then A is invertible
6. Block-diagonal operator is injective if A_fin is invertible and tailScalar ≠ 0

theorem Example_7_7.Y₀_bound_nonneg {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : 0 ≤ Y₀_bound lam0 sol A_fin

Y₀ is non-negative (it's a norm)

theorem Example_7_7.Z₂_bound_nonneg {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : 0 ≤ Z₂_bound sol A_fin

Z₂ is non-negative (it's 2 times a max of non-negative values)

theorem Example_7_7.radiiPoly_neg_implies_Z₀_Z₁_lt_one {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (r₀ : ℝ) (hr₀ : 0 < r₀) (h_radii : radiiPoly_7_7 N lam0 sol A_fin r₀ < 0) : Z₀_bound sol A_fin + Z₁_bound sol < 1

From p(r₀) < 0, derive Z₀ + Z₁ < 1. Uses general_radii_poly_neg_implies_Z_lt_one and Z₂r₀ ≥ 0.

theorem Example_7_7.Z₀_lt_one_of_sum_lt_one {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (h : Z₀_bound sol A_fin + Z₁_bound sol < 1) : Z₀_bound sol A_fin < 1

From Z₀ + Z₁ < 1 and Z₁ ≥ 0, derive Z₀ < 1

theorem Example_7_7.approxInverse_tailScalar_ne_zero {ν : PosReal} {N : ℕ} (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) : (approxInverse sol A_fin).tailScalar ≠ 0

The tail scalar of approxInverse is nonzero

theorem Example_7_7.approxInverse_injective {ν : PosReal} (N : ℕ) (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (r₀ : ℝ) (hr₀ : 0 < r₀) (h_radii : radiiPoly_7_7 N lam0 sol A_fin r₀ < 0) : Function.Injective ⇑(approxInverse sol A_fin).toCLM

Injectivity of A follows from Proposition 7.6.5 when p(r₀) < 0

From page 168: If p(r₀) < 0 then Z₀ + Z₁ < 1 by Corollary 7.6.3, hence ‖I - AA†‖ < 1. By Proposition 7.6.5, since A has block-diagonal form with injective tail (scalar 1/(2ā₀) ≠ 0), A is injective.

theorem Example_7_7.example_7_7_main_theorem {ν : PosReal} {N : ℕ} (lam0 : ℝ) (sol : ApproxSolution N) (A_fin : Matrix (Fin (N + 1)) (Fin (N + 1)) ℝ) (r₀ : ℝ) (hr₀ : 0 < r₀) (hN : 0 < N) (h_radii : radiiPoly_7_7 N lam0 sol A_fin r₀ < 0) : ∃! aTilde : ↥(l1Weighted ν), aTilde ∈ Metric.closedBall sol.toL1 r₀ ∧ F lam0 aTilde = 0

Main Theorem: Existence and uniqueness of Taylor series solution.

Given:

• lam0 > 0 (the parameter value)
• ā⁽ᴺ⁾ ∈ ℝᴺ⁺¹ with ā₀ ≠ 0 (approximate solution)
• A⁽ᴺ⁾ (numerical inverse of DF⁽ᴺ⁾(ā))
• r₀ > 0 such that p(r₀) < 0

Then there exists a unique ã ∈ ℓ¹_ν with:

• ‖ã - ā‖ < r₀
• F(ã) = ã ⋆ ã - c = 0

In other words, x(λ) = Σₙ ãₙ(λ - lam0)ⁿ satisfies x(λ)² - λ = 0 for |λ - lam0| < ν.