For convergence of truncated solves, we precondition the bordered operator to obtain a compact perturbation of the identity \(I+K\). Stable finite sections then converge, with error controlled by the projection error of the solution. For first-order problems \(u'+pu\) with polynomial \(p\), the preconditioner is \(R=\operatorname {diag}(1,1,1/2,1/3,\ldots )\). Its decreasing diagonal compensates for the growing differentiation entries, giving a bounded operator on coefficient space.
If the infinite preconditioned operator is invertible, large finite sections are uniquely solvable, and convergence of the preconditioned coefficients in \(\ell ^2\) implies uniform convergence of the reconstructed function, including the endpoints. For \(p=0\) we prove invertibility.
Reference details: Inversion on invertible indices and related results
For a family \(A:I\to R\) in a monoid, let \(I_A=\{ i\in I:A_i\text{ is invertible}\} \). For \(i\in I_A\), define \(A_i^{-1}\) by inversion in the group of units of \(R\). There is no inverse value at an index outside \(I_A\).
Lean Formalisation
def Ring.InvertibleIndex.{u_1, u_2} {ι : Type u_1} {R : Type u_2} [Monoid R] (A : ι → R) : Type u_1
Lean definition
/-- Indices at which a family has a two-sided inverse. -/
abbrev InvertibleIndex (A : ι → R) := {i : ι // IsUnit (A i)}
def Ring.inverseAt.{u_1, u_2} {ι : Type u_1} {R : Type u_2} [Monoid R] (A : ι → R) (i : Ring.InvertibleIndex A) : R
Lean definition
/-- Inversion along a family, defined only at its invertible indices. -/
noncomputable def inverseAt (A : ι → R) (i : InvertibleIndex A) : R :=
↑(i.property.unit⁻¹)
For each \(i\in I_A\), the indexed inverse satisfies \(A_i^{-1}A_i=A_iA_i^{-1}=1\).
Lean Formalisation
theorem Ring.inverseAt_mul.{u_1, u_2} {ι : Type u_1} {R : Type u_2} [Monoid R] (A : ι → R) (i : Ring.InvertibleIndex A) :
Ring.inverseAt A i * A ↑i = 1 ∧ A ↑i * Ring.inverseAt A i = 1
Lean proof
/-- The inverse has the two defining identities. -/
theorem inverseAt_mul (A : ι → R) (i : InvertibleIndex A) :
inverseAt A i * A i = 1 ∧ A i * inverseAt A i = 1 := by
exact ⟨by simpa only [inverseAt, IsUnit.unit_spec] using Units.inv_mul i.property.unit,
by simpa only [inverseAt, IsUnit.unit_spec] using Units.mul_inv i.property.unit⟩
For a filter \(\mathcal F\) on \(I\), the induced filter on \(I_A\) is its pullback along the inclusion \(I_A\hookrightarrow I\). For \(I=\mathbb N\) and \(\mathcal F\) the filter of tails, this means tending to infinity through invertible indices.
Lean Formalisation
def Ring.invertibleIndexFilter.{u_1, u_2} {ι : Type u_1} {R : Type u_2} [Monoid R] (A : ι → R) (l : Filter ι) :
Filter (Ring.InvertibleIndex A)
Lean definition
/-- Restrict a limiting process to the indices where inversion exists. -/
def invertibleIndexFilter (A : ι → R) (l : Filter ι) : Filter (InvertibleIndex A) :=
Filter.comap Subtype.val l
If \(A_i\) is invertible eventually along \(\mathcal F\), pushing the induced filter forward to \(I\) recovers \(\mathcal F\). If \(\mathcal F\) is nontrivial, its induced filter on \(I_A\) is also nontrivial. In particular, an eventually invertible sequence has a cofinal domain of invertible indices.
Lean Formalisation
theorem Ring.map_invertibleIndexFilter.{u_1, u_2} {ι : Type u_1} {R : Type u_2} [Monoid R] (A : ι → R) (l : Filter ι)
(hA : ∀ᶠ (i : ι) in l, IsUnit (A i)) : Filter.map Subtype.val (Ring.invertibleIndexFilter A l) = l
Lean proof
/-- Eventual invertibility preserves the original limiting filter exactly. -/
theorem map_invertibleIndexFilter (A : ι → R) (l : Filter ι)
(hA : ∀ᶠ i in l, IsUnit (A i)) :
Filter.map Subtype.val (invertibleIndexFilter A l) = l := by
apply Filter.map_comap_of_mem
exact hA.mono (fun i hi ↦ ⟨⟨i, hi⟩, rfl⟩)
theorem Ring.invertibleIndexFilter_neBot.{u_1, u_2} {ι : Type u_1} {R : Type u_2} [Monoid R] (A : ι → R) (l : Filter ι)
[l.NeBot] (hA : ∀ᶠ (i : ι) in l, IsUnit (A i)) : (Ring.invertibleIndexFilter A l).NeBot
Lean proof
/-- Restriction to an eventually invertible family is nonvacuous. -/
theorem invertibleIndexFilter_neBot (A : ι → R) (l : Filter ι) [NeBot l]
(hA : ∀ᶠ i in l, IsUnit (A i)) : NeBot (invertibleIndexFilter A l) := by
apply Filter.NeBot.comap_of_range_mem ‹NeBot l›
exact hA.mono (fun i hi ↦ ⟨⟨i, hi⟩, rfl⟩)
In a complete normed ring, if \(A_i\to U\) along \(\mathcal F\) and \(U\) is a unit, then \(A_i^{-1}\to U^{-1}\) along the induced filter on invertible indices.
Lean Formalisation
theorem Ring.tendsto_inverseAt.{u_1, u_2} {ι : Type u_1} {R : Type u_2} [NormedRing R] [CompleteSpace R] {A : ι → R}
{l : Filter ι} (u : Rˣ) (hA : Filter.Tendsto A l (nhds ↑u)) :
Filter.Tendsto (Ring.inverseAt A) (Ring.invertibleIndexFilter A l) (nhds ↑u⁻¹)
Lean proof
/-- Inverse continuity restricted to genuine inverses. -/
theorem tendsto_inverseAt {A : ι → R} {l : Filter ι} (u : Rˣ)
(hA : Tendsto A l (𝓝 (u : R))) :
Tendsto (inverseAt A) (invertibleIndexFilter A l) (𝓝 (↑(u⁻¹) : R)) := by
have h := (NormedRing.inverse_continuousAt u).tendsto.comp hA
have hh := h.comp (Filter.tendsto_comap :
Tendsto (Subtype.val : InvertibleIndex A → ι) (Filter.comap Subtype.val l) l)
change Tendsto (fun i ↦ inverseAt A i) (Filter.comap Subtype.val l) _
simpa only [Function.comp_def, inverseAt_eq_ringInverse, Ring.inverse_unit] using hh
Let \(E\) be a real or complex Banach space, \(K\) compact, and \(T=I+K\) invertible. Let uniformly bounded projections \(P_n\) converge strongly to \(I\). For sufficiently large \(n\), \(A_n=I+P_nK\) is invertible with uniformly bounded inverses. For \(f=Tx\), the unique projected solution \(x_n\in \operatorname {ran}P_n\) of \(P_nTx_n=P_nf\) is \(A_n^{-1}P_nf\) and satisfies \(\| x_n-x\| \le (\| T^{-1}\| +1)\| P_nx-x\| \). The solution \(x_n\) is defined for every index \(n\) at which \(A_n\) is invertible. These indices include every sufficiently large \(n\), and \(x_n\to x\) as \(n\to \infty \) through them.
def ContinuousLinearMap.liftedFiniteSection.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2} [NormedAddCommGroup E]
[NormedSpace 𝕜 E] (P K : E →L[𝕜] E) : E →L[𝕜] E
Lean definition
/-- Lift a projected equation to the whole space by retaining the identity on
unresolved coordinates. Its restriction to a projection range is the finite section. -/
@[expose] noncomputable def liftedFiniteSection (P K : E →L[𝕜] E) : E →L[𝕜] E :=
1 + P.comp K
/-- Stability provides actual inverse values for every sufficiently large cutoff. -/
theorem eventually_stable_liftedFiniteSection
(P : ℕ → E →L[𝕜] E) {C : ℝ} (hC : ∀ n, ‖P n‖ ≤ C)
(hP : ∀ x, Tendsto (fun n ↦ P n x) atTop (𝓝 x))
(K : E →L[𝕜] E) (hK : IsCompactOperator K) (hT : IsUnit (1 + K)) :
∀ᶠ n in atTop, ∃ hn : IsUnit (liftedFiniteSection (P n) K),
‖Ring.inverseAt (fun n ↦ liftedFiniteSection (P n) K) ⟨n, hn⟩‖ ≤
‖(↑(hT.unit⁻¹) : E →L[𝕜] E)‖ + 1 := by
filter_upwards [eventually_stable_liftedFiniteSection_ringInverse P hC hP K hK hT] with n hn
refine ⟨hn.1, ?_⟩
have hunit : Ring.inverse (1 + K) = (↑(hT.unit⁻¹) : E →L[𝕜] E) := by
simpa only [IsUnit.unit_spec] using Ring.inverse_unit hT.unit
simpa only [Ring.inverseAt_eq_ringInverse, hunit] using hn.2
theorem ContinuousLinearMap.existsUnique_projected_solution.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2}
[NormedAddCommGroup E] [NormedSpace 𝕜 E] (P K : E →L[𝕜] E) (hP : P ∘SL P = P) (hA : IsUnit (P.liftedFiniteSection K))
(f : E) : ∃! x, P x = x ∧ P ((1 + K) x) = P f
Lean proof
/-- An invertible lifted section gives a unique solution of the actual
projected equations inside the projection range. -/
theorem existsUnique_projected_solution (P K : E →L[𝕜] E)
(hP : P.comp P = P) (hA : IsUnit (liftedFiniteSection P K)) (f : E) :
∃! x : E, P x = x ∧ P ((1 + K) x) = P f := by
refine ⟨Ring.inverse (liftedFiniteSection P K) (P f),
liftedFiniteSection_solution_mem P K hP hA f, ?_⟩
intro y hy
have he : liftedFiniteSection P K y = P f := by
simpa only [liftedFiniteSection, add_apply, one_apply_eq_self, comp_apply,
map_add, hy.1] using hy.2
have hi := congrArg (fun T : E →L[𝕜] E ↦ T y)
(Ring.inverse_mul_cancel (liftedFiniteSection P K) hA)
simpa only [mul_apply_eq_comp, one_apply_eq_self, he] using hi.symm
/-- The classical finite-section error bound is asserted together with existence. -/
theorem eventually_norm_liftedFiniteSection_error_le
(P : ℕ → E →L[𝕜] E) {C : ℝ} (hC : ∀ n, ‖P n‖ ≤ C)
(hP : ∀ x, Tendsto (fun n ↦ P n x) atTop (𝓝 x))
(K : E →L[𝕜] E) (hK : IsCompactOperator K) (hT : IsUnit (1 + K)) :
∀ᶠ n in atTop, ∃ hn : IsUnit (liftedFiniteSection (P n) K), ∀ x : E,
‖Ring.inverseAt (fun n ↦ liftedFiniteSection (P n) K) ⟨n, hn⟩
(P n ((1 + K) x)) - x‖ ≤
(‖(↑(hT.unit⁻¹) : E →L[𝕜] E)‖ + 1) * ‖P n x - x‖ := by
filter_upwards [eventually_stable_liftedFiniteSection_ringInverse P hC hP K hK hT,
eventually_norm_liftedFiniteSection_error_le_ringInverse P hC hP K hK hT] with n hn he
refine ⟨hn.1, fun x ↦ ?_⟩
have hunit : Ring.inverse (1 + K) = (↑(hT.unit⁻¹) : E →L[𝕜] E) := by
simpa only [IsUnit.unit_spec] using Ring.inverse_unit hT.unit
simpa only [Ring.inverseAt_eq_ringInverse, hunit] using he x
Let \(R=\operatorname {diag}(1,1,1/2,1/3,\ldots )\) and \(Bv=\sum _j(-1)^j(Rv)_j\). The endpoint functional \(B\) is bounded and \(R\) is compact. For any bounded lower-order map \(A\), the bordered operator has row zero \(Bv\) and rows \(v_{j+1}+(ARv)_j\). It is \(I+K\) with \(K\) compact.
Every \(v\in \ell ^2\) gives absolutely summable coefficients \(Rv\). The Chebyshev series with coefficients \(Rv\) takes the value \(Bv\) at \(-1\). Reconstruction errors are bounded uniformly by \(\| ((-1)^jR_{jj})_j\| _2\| v-w\| _2\). Thus convergence in the preconditioned coefficient norm implies uniform convergence including endpoints.
Lean Formalisation
theorem Polynomial.Chebyshev.hasSum_firstOrderBoundary (x : ↥(lp (fun x => ℂ) 2)) :
HasSum (fun n => (-1) ^ n * ↑(Polynomial.Chebyshev.firstOrderPreconditioner x) n)
(Polynomial.Chebyshev.firstOrderBoundary x)
Lean proof
/-- The preconditioned endpoint functional is its actual convergent series. -/
theorem hasSum_firstOrderBoundary (x : lp (fun _ : ℕ ↦ ℂ) 2) :
HasSum (fun n ↦ (-1 : ℂ) ^ n * (firstOrderPreconditioner x) n) (firstOrderBoundary x) := by
have h := lp.hasSum_inner (𝕜 := ℂ) firstOrderBoundaryVector x
convert h using 1
· funext n
rw [RCLike.inner_apply']
change (-1 : ℂ) ^ n * (firstOrderDiagonal n * x n) =
star ((-1 : ℂ) ^ n * firstOrderDiagonal n) * x n
simp [firstOrderDiagonal, mul_assoc]
· rfl
theorem Polynomial.Chebyshev.complexChebyshevSeries_firstOrderPreconditioner_neg_one (x : ↥(lp (fun x => ℂ) 2)) :
Polynomial.Chebyshev.complexChebyshevSeries (↑(Polynomial.Chebyshev.firstOrderPreconditioner x))
(Polynomial.Chebyshev.ComplexChebyshevSeriesPoint.ofFirstOrder x
⟨-1, Polynomial.Chebyshev.complexChebyshevSeries_firstOrderPreconditioner_neg_one._proof_1⟩) =
Polynomial.Chebyshev.firstOrderBoundary x
Lean proof
/-- The boundary row is the actual series value at the left endpoint. -/
theorem complexChebyshevSeries_firstOrderPreconditioner_neg_one
(x : lp (fun _ : ℕ ↦ ℂ) 2) :
complexChebyshevSeries (firstOrderPreconditioner x)
(.ofFirstOrder x ⟨-1, by constructor <;> norm_num⟩) = firstOrderBoundary x := by
apply complexChebyshevSeries_eq_of_tendsto
simpa only [ComplexChebyshevSeriesPoint.ofFirstOrder_val, ofReal_neg, ofReal_one,
T_eval_neg_one, Int.cast_negOnePow_natCast, mul_comm] using
(hasSum_firstOrderBoundary x).tendsto_sum_nat
theorem Polynomial.Chebyshev.summable_norm_firstOrderPreconditioner (x : ↥(lp (fun x => ℂ) 2)) :
(Summable fun n => ‖↑(Polynomial.Chebyshev.firstOrderPreconditioner x) n‖) ∧
∑' (n : ℕ), ‖↑(Polynomial.Chebyshev.firstOrderPreconditioner x) n‖ ≤
‖Polynomial.Chebyshev.firstOrderBoundaryVector‖ * ‖x‖
Lean proof
/-- Preconditioning makes the coefficients absolutely summable, with a uniform bound. -/
theorem summable_norm_firstOrderPreconditioner (x : lp (fun _ : ℕ ↦ ℂ) 2) :
Summable (fun n ↦ ‖firstOrderPreconditioner x n‖) ∧
(∑' n, ‖firstOrderPreconditioner x n‖) ≤ ‖firstOrderBoundaryVector‖ * ‖x‖ := by
have h := lp.tsum_mul_le_mul_norm
(by simpa using Real.HolderConjugate.two_two :
(2 : ℝ≥0∞).toReal.HolderConjugate (2 : ℝ≥0∞).toReal) firstOrderBoundaryVector x
simpa only [firstOrderBoundaryVector, firstOrderPreconditioner_apply, norm_mul,
norm_pow, norm_neg, norm_one, one_pow, one_mul] using h
theorem Polynomial.Chebyshev.tendstoUniformlyOn_firstOrder_reconstruction.{u_1} {ι : Type u_1} {l : Filter ι}
{v : ι → ↥(lp (fun x => ℂ) 2)} {x : ↥(lp (fun x => ℂ) 2)} (hv : Filter.Tendsto v l (nhds x)) :
TendstoUniformly
(fun n t =>
Polynomial.Chebyshev.complexChebyshevSeries (↑(Polynomial.Chebyshev.firstOrderPreconditioner (v n)))
(Polynomial.Chebyshev.ComplexChebyshevSeriesPoint.ofFirstOrder (v n) t))
(fun t =>
Polynomial.Chebyshev.complexChebyshevSeries (↑(Polynomial.Chebyshev.firstOrderPreconditioner x))
(Polynomial.Chebyshev.ComplexChebyshevSeriesPoint.ofFirstOrder x t))
l
Lean proof
/-- Reconstruction carries coefficient convergence to uniform interval convergence. -/
theorem tendstoUniformlyOn_firstOrder_reconstruction
{ι : Type*} {l : Filter ι} {v : ι → lp (fun _ : ℕ ↦ ℂ) 2}
{x : lp (fun _ : ℕ ↦ ℂ) 2} (hv : Tendsto v l (𝓝 x)) :
TendstoUniformly
(fun n (t : Icc (-1 : ℝ) 1) ↦ complexChebyshevSeries (firstOrderPreconditioner (v n))
(.ofFirstOrder (v n) t))
(fun t ↦ complexChebyshevSeries (firstOrderPreconditioner x) (.ofFirstOrder x t)) l := by
have hb : Tendsto (fun n ↦ ‖firstOrderBoundaryVector‖ * ‖v n - x‖) l (𝓝 0) := by
simpa using (hv.sub (tendsto_const_nhds (x := x))).norm.const_mul ‖firstOrderBoundaryVector‖
rw [Metric.tendstoUniformly_iff]
intro ε hε
filter_upwards [hb (gt_mem_nhds hε)] with n hn t
rw [dist_eq_norm, norm_sub_rev]
exact (norm_firstOrder_reconstruction_sub_le (v n) x t).trans_lt hn
For real polynomial \(p\), take \(A=S p(J)\) in the bordered assembly for \(u\mapsto (u(-1),u\prime +pu)\). This extends exactly the existing polynomial lower-order map. If the infinite preconditioned bordered operator is invertible, sufficiently large finite systems are uniquely solvable. Indexed by the invertible finite sections tending to infinity, their actual solutions reconstruct functions converging uniformly on \([-1,1]\).
theorem Polynomial.Chebyshev.eventually_existsUnique_firstOrderPolynomial_system (p : Polynomial ℝ)
(hp :
IsUnit (1 + Polynomial.Chebyshev.firstOrderCompactRemainder (Polynomial.Chebyshev.firstOrderPolynomialTerm p))) :
∀ᶠ (n : ℕ) in Filter.atTop,
∀ (f : ↥(lp (fun x => ℂ) 2)),
∃! x,
(∀ (i : ℕ), n ≤ i → ↑x i = 0) ∧
∀ i < n,
↑((1 + Polynomial.Chebyshev.firstOrderCompactRemainder (Polynomial.Chebyshev.firstOrderPolynomialTerm p)) x)
i =
↑f i
Lean proof
/-- Invertibility of the infinite polynomial operator implies unique large finite
sections. Invertibility is an explicit hypothesis, not inferred from compactness. -/
theorem eventually_existsUnique_firstOrderPolynomial_system (p : ℝ[X])
(hp : IsUnit (1 + firstOrderCompactRemainder (firstOrderPolynomialTerm p))) :
∀ᶠ n in atTop, ∀ f : lp (fun _ : ℕ ↦ ℂ) 2, ∃! x : lp (fun _ : ℕ ↦ ℂ) 2,
(∀ i, n ≤ i → x i = 0) ∧
(∀ i < n, ((1 + firstOrderCompactRemainder (firstOrderPolynomialTerm p)) x) i = f i) :=
eventually_existsUnique_firstOrder_system _ hp
/-- The normalized bordered derivative is invertible, with inverse I minus its
rank-one correction. No solvability assumption is needed in this example. -/
theorem isUnit_firstOrderDerivative : IsUnit (1 + firstOrderBoundaryCorrection) := by
have h : firstOrderBoundaryCorrection * firstOrderBoundaryCorrection = 0 := by
simpa only [pow_two] using firstOrderBoundaryCorrection_sq
refine ⟨⟨1 + firstOrderBoundaryCorrection, 1 - firstOrderBoundaryCorrection, ?_, ?_⟩, rfl⟩
· calc
_ = 1 - firstOrderBoundaryCorrection * firstOrderBoundaryCorrection := by simp only [mul_sub, add_mul, one_mul, mul_one]; abel
_ = 1 := by rw [h, sub_zero]
· calc
_ = 1 - firstOrderBoundaryCorrection * firstOrderBoundaryCorrection := by simp only [sub_mul, mul_add, one_mul, mul_one]; abel
_ = 1 := by rw [h, sub_zero]
For endpoint value \(c\in \mathbb C\) and derivative coordinates \(f\in \ell ^2\), define \(v=(I+K_B)^{-1}(c,f_0,f_1,\ldots )\), using the inverse of the invertible bordered derivative. The reconstructed solution has coefficients \(Rv\).
Lean Formalisation
def Polynomial.Chebyshev.firstOrderDerivativeSolution (c : ℂ) (f : ↥(lp (fun x => ℂ) 2)) : ↥(lp (fun x => ℂ) 2)
Lean definition
/-- An actual solution for prescribed derivative coefficients and left endpoint.
The inverse exists by the nilpotent boundary correction, not by a hypothesis. -/
noncomputable def firstOrderDerivativeSolution (c : ℂ) (f : lp (fun _ : ℕ ↦ ℂ) 2) :
lp (fun _ : ℕ ↦ ℂ) 2 :=
Ring.inverseAt (fun _ : Unit ↦ 1 + firstOrderBoundaryCorrection) ⟨(), isUnit_firstOrderDerivative⟩
(lp.single 2 0 c + lp.coefficientShiftRight f)
For \(p=0\), the boundary correction \(K_B\) satisfies \(K_B^2=0\), so the bordered derivative has explicit inverse \(I-K_B\). Given endpoint \(c\) and \(U\) coefficients \(f\in \ell ^2\), its solution has \(u(-1)=c\) and preconditioned coordinates \(v_{j+1}=f_j\). The actual finite solves, indexed by invertible sections tending to infinity, converge uniformly to the reconstructed function without an additional invertibility assumption. If the actual solution coefficients \(Rv\) satisfy a geometric bound with \(\rho {\gt}1\), the classical derivative on \(E_\rho \) is \(u\prime (z)=\sum _j f_jU_j(z)\).
Lean Formalisation
theorem Polynomial.Chebyshev.firstOrderDerivativeSolution_equation (c : ℂ) (f : ↥(lp (fun x => ℂ) 2)) :
(1 + Polynomial.Chebyshev.firstOrderBoundaryCorrection) (Polynomial.Chebyshev.firstOrderDerivativeSolution c f) =
lp.single 2 0 c + lp.coefficientShiftRight f
Lean proof
/-- The explicit inverse solves all bordered coefficient equations. -/
theorem firstOrderDerivativeSolution_equation (c : ℂ) (f : lp (fun _ : ℕ ↦ ℂ) 2) :
(1 + firstOrderBoundaryCorrection) (firstOrderDerivativeSolution c f) =
lp.single 2 0 c + lp.coefficientShiftRight f := by
have h := Ring.mul_inverse_cancel (1 + firstOrderBoundaryCorrection) isUnit_firstOrderDerivative
simpa only [firstOrderDerivativeSolution, Ring.inverseAt_eq_ringInverse,
mul_apply_eq_comp, one_apply_eq_self] using
congrArg (fun L : lp (fun _ : ℕ ↦ ℂ) 2 →L[ℂ] lp (fun _ : ℕ ↦ ℂ) 2 ↦
L (lp.single 2 0 c + lp.coefficientShiftRight f)) h
theorem Polynomial.Chebyshev.firstOrderDerivativeSolution_succ (c : ℂ) (f : ↥(lp (fun x => ℂ) 2)) (n : ℕ) :
↑(Polynomial.Chebyshev.firstOrderDerivativeSolution c f) (n + 1) = ↑f n
Lean proof
/-- The positive coordinates are precisely the given U derivative coefficients. -/
theorem firstOrderDerivativeSolution_succ (c : ℂ) (f : lp (fun _ : ℕ ↦ ℂ) 2) (n : ℕ) :
firstOrderDerivativeSolution c f (n + 1) = f n := by
have h := congrArg (fun x : lp (fun _ : ℕ ↦ ℂ) 2 ↦ x (n + 1))
(firstOrderDerivativeSolution_equation c f)
simpa [add_apply, one_apply_eq_self,
lp.single_apply, Pi.single_apply] using h
On real or complex \(\ell ^2\), \(P_n\) retains precisely coordinates \(0,\ldots ,n-1\). It is an idempotent compact operator of norm at most one, and \(P_nx\to x\) for every \(x\).
Lean Formalisation
theorem lp.coefficientProjection_apply.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (n : ℕ) (x : ↥(lp (fun x => 𝕜) 2)) (i : ℕ) :
↑((lp.coefficientProjection n) x) i = if i < n then ↑x i else 0
Lean proof
/-- Coordinate truncation has the expected entries. -/
@[simp] theorem coefficientProjection_apply (n : ℕ) (x : lp (fun _ : ℕ ↦ 𝕜) 2) (i : ℕ) :
coefficientProjection n x i = if i < n then x i else 0 := by
classical
simp only [coefficientProjection, sum_apply, ContinuousLinearMap.comp_apply,
singleContinuousLinearMap_apply, evalCLM_scalar_apply, coeFn_sum, lp.coeFn_single,
Finset.sum_apply, Finset.sum_pi_single, Finset.mem_range]
theorem lp.coefficientProjection_idempotent.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (n : ℕ) :
lp.coefficientProjection n ∘SL lp.coefficientProjection n = lp.coefficientProjection n
Lean proof
/-- A coordinate truncation is a projection. -/
theorem coefficientProjection_idempotent (n : ℕ) :
(coefficientProjection (𝕜 := 𝕜) n).comp (coefficientProjection n) = coefficientProjection n := by
ext x i
simp only [ContinuousLinearMap.comp_apply, coefficientProjection_apply]
split_ifs <;> rfl
A bounded real or complex scalar sequence \(d_j\to 0\) defines a compact diagonal operator \(D\), with \(\| D\| \le C\) whenever \(|d_j|\le C\). The finite diagonal sections converge to \(D\) in operator norm. If \(|d_j|\le \varepsilon \) for \(j\ge n\), then \(\| D-P_nD\| \le \varepsilon \).
Lean Formalisation
theorem lp.coefficientDiagonal_apply.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (d : ℕ → 𝕜) {C : ℝ} (hC : 0 ≤ C)
(hd : ∀ (i : ℕ), ‖d i‖ ≤ C) (x : ↥(lp (fun x => 𝕜) 2)) (i : ℕ) : ↑((lp.coefficientDiagonal d hC hd) x) i = d i * ↑x i
Lean proof
/-- A diagonal multiplier acts coordinatewise. -/
@[simp] theorem coefficientDiagonal_apply (d : ℕ → 𝕜) {C : ℝ} (hC : 0 ≤ C)
(hd : ∀ i, ‖d i‖ ≤ C) (x : lp (fun _ : ℕ ↦ 𝕜) 2) (i : ℕ) :
coefficientDiagonal d hC hd x i = d i * x i := rfl
theorem lp.norm_coefficientDiagonal_le.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (d : ℕ → 𝕜) {C : ℝ} (hC : 0 ≤ C)
(hd : ∀ (i : ℕ), ‖d i‖ ≤ C) : ‖lp.coefficientDiagonal d hC hd‖ ≤ C
Lean proof
/-- The operator norm is bounded by a uniform diagonal bound. -/
theorem norm_coefficientDiagonal_le (d : ℕ → 𝕜) {C : ℝ} (hC : 0 ≤ C)
(hd : ∀ i, ‖d i‖ ≤ C) : ‖coefficientDiagonal d hC hd‖ ≤ C :=
norm_mapCLM_le ..
theorem lp.tendsto_coefficientDiagonal_sections.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (d : ℕ → 𝕜) {C : ℝ} (hC : 0 ≤ C)
(hd : ∀ (i : ℕ), ‖d i‖ ≤ C) (hlim : Filter.Tendsto d Filter.atTop (nhds 0)) :
Filter.Tendsto (fun n => lp.coefficientProjection n ∘SL lp.coefficientDiagonal d hC hd) Filter.atTop
(nhds (lp.coefficientDiagonal d hC hd))
Lean proof
/-- A diagonal tending to zero is the norm limit of its finite coordinate sections. -/
theorem tendsto_coefficientDiagonal_sections (d : ℕ → 𝕜) {C : ℝ} (hC : 0 ≤ C)
(hd : ∀ i, ‖d i‖ ≤ C) (hlim : Tendsto d atTop (𝓝 0)) :
Tendsto (fun n ↦ (coefficientProjection n).comp (coefficientDiagonal d hC hd))
atTop (𝓝 (coefficientDiagonal d hC hd)) := by
rw [Metric.tendsto_atTop]
intro ε hε
obtain ⟨N, hN⟩ := Metric.tendsto_atTop.mp hlim (ε / 2) (by positivity)
refine ⟨N, fun n hn ↦ ?_⟩
rw [dist_eq_norm, norm_sub_rev]
apply lt_of_le_of_lt (norm_coefficientDiagonal_tail_le d hC hd n (by positivity)
(fun i hi ↦ ?_)) (by linarith : ε / 2 < ε)
simpa only [dist_zero_right] using (hN i (hn.trans hi)).le
On a real or complex normed space, uniformly bounded continuous linear maps \(P_n\) converging strongly to the identity converge uniformly on compact sets. For compact \(K\), \(P_nK\to K\) in operator norm.
Lean Formalisation
theorem ContinuousLinearMap.tendstoUniformlyOn_of_strongly_tendsto_id.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2}
[NormedAddCommGroup E] [NormedSpace 𝕜 E] (P : ℕ → E →L[𝕜] E) {C : ℝ} (hC : ∀ (n : ℕ), ‖P n‖ ≤ C)
(hP : ∀ (x : E), Filter.Tendsto (fun n => (P n) x) Filter.atTop (nhds x)) {S : Set E} (hS : IsCompact S) :
TendstoUniformlyOn (fun n x => (P n) x) id Filter.atTop S
Lean proof
/-- Uniformly bounded operators converging strongly to the identity converge
uniformly on compact sets. -/
theorem tendstoUniformlyOn_of_strongly_tendsto_id
(P : ℕ → E →L[𝕜] E) {C : ℝ} (hC : ∀ n, ‖P n‖ ≤ C)
(hP : ∀ x, Tendsto (fun n ↦ P n x) atTop (𝓝 x))
{S : Set E} (hS : IsCompact S) :
TendstoUniformlyOn (fun n x ↦ P n x) id atTop S := by
have he : UniformEquicontinuous (fun n x ↦ P n x) :=
Metric.uniformEquicontinuous_of_continuity_modulus (fun t ↦ C * t)
(by simpa using (tendsto_id : Tendsto (id : ℝ → ℝ) (𝓝 0) (𝓝 0)).const_mul C) _ (fun x y n ↦ by
simpa only [dist_eq_norm, ← map_sub] using
(P n).le_opNorm (x - y) |>.trans
(mul_le_mul_of_nonneg_right (hC n) (norm_nonneg _)))
let : CompactSpace S := isCompact_iff_compactSpace.mp hS
rw [tendstoUniformlyOn_iff_tendstoUniformly_comp_coe]
apply UniformFun.tendsto_iff_tendstoUniformly.mp
apply (((equicontinuous_restrict_iff _).mpr (he.equicontinuous.equicontinuousOn S)).tendsto_uniformFun_iff_pi
atTop (fun x : S ↦ (x : E))).2
exact tendsto_pi_nhds.mpr (fun x ↦ hP x)
theorem ContinuousLinearMap.tendsto_compact_comp_of_strongly_tendsto_id.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2}
[NormedAddCommGroup E] [NormedSpace 𝕜 E] (P : ℕ → E →L[𝕜] E) {C : ℝ} (hC : ∀ (n : ℕ), ‖P n‖ ≤ C)
(hP : ∀ (x : E), Filter.Tendsto (fun n => (P n) x) Filter.atTop (nhds x)) (K : E →L[𝕜] E)
(hK : IsCompactOperator ⇑K) : Filter.Tendsto (fun n => P n ∘SL K) Filter.atTop (nhds K)
Lean proof
/-- Strong convergence of uniformly bounded operators becomes norm convergence
after composition on the right with a compact operator. -/
theorem tendsto_compact_comp_of_strongly_tendsto_id
(P : ℕ → E →L[𝕜] E) {C : ℝ} (hC : ∀ n, ‖P n‖ ≤ C)
(hP : ∀ x, Tendsto (fun n ↦ P n x) atTop (𝓝 x))
(K : E →L[𝕜] E) (hK : IsCompactOperator K) :
Tendsto (fun n ↦ (P n).comp K) atTop (𝓝 K) := by
obtain ⟨S, hS, hKS⟩ := hK.image_closedBall_subset_compact (f := K.toLinearMap) 1
have h := tendstoUniformlyOn_of_strongly_tendsto_id P hC hP hS
rw [Metric.tendstoUniformlyOn_iff] at h
rw [Metric.tendsto_atTop]
intro ε hε
obtain ⟨N, hN⟩ := eventually_atTop.1 (h (ε / 2) (by positivity))
refine ⟨N, fun n hn ↦ ?_⟩
rw [dist_eq_norm]
apply lt_of_le_of_lt (b := ε / 2) _ (by linarith)
apply opNorm_le_of_unit_norm (by positivity)
intro x hx
have hxs : K x ∈ S := hKS ⟨x, by simp [Metric.mem_closedBall, dist_zero_right, hx], rfl⟩
have ht := (hN n hn (K x) hxs).le
simpa only [id_eq, dist_eq_norm, norm_sub_rev, sub_apply, comp_apply] using ht
On complex \(\ell ^2\), \(P_nx=x\) exactly when \(x_j=0\) for \(j\ge n\), and \(P_nx=P_ny\) exactly when the first \(n\) coordinates agree. For compact \(K\) on \(\ell ^2\) with \(I+K\) invertible, the first \(n\) equations of \((I+K)x_n=f\) with \(x_{n,j}=0\) for \(j\ge n\) have a unique solution for every sufficiently large \(n\). For every sufficiently large \(n\), the lifted finite section has an actual inverse and its solution obeys the preceding tail error bound. The inverse norm constant is \(\| (I+K)^{-1}\| +1\). On the cofinal set of invertible cutoffs, these actual solves converge in \(\ell ^2\); the corresponding limit filter is nontrivial. No inverse is evaluated at a singular cutoff.
theorem lp.coefficientProjection_eq_self_iff (n : ℕ) (x : ↥(lp (fun x => ℂ) 2)) :
(lp.coefficientProjection n) x = x ↔ ∀ (i : ℕ), n ≤ i → ↑x i = 0
Lean proof
/-- Fixed points of the coordinate projection are exactly the supported vectors. -/
theorem coefficientProjection_eq_self_iff (n : ℕ) (x : lp (fun _ : ℕ ↦ ℂ) 2) :
coefficientProjection n x = x ↔ ∀ i, n ≤ i → x i = 0 := by
constructor
· intro h i hi
have he := congrArg (fun v : lp (fun _ : ℕ ↦ ℂ) 2 ↦ v i) h
simpa [coefficientProjection_apply, Nat.not_lt.mpr hi] using he.symm
· intro h
ext i
by_cases hi : i < n
· simp [hi]
· simp [hi, h i (by omega)]
theorem lp.coefficientProjection_eq_iff (n : ℕ) (x y : ↥(lp (fun x => ℂ) 2)) :
(lp.coefficientProjection n) x = (lp.coefficientProjection n) y ↔ ∀ i < n, ↑x i = ↑y i
Lean proof
/-- Projected equations compare exactly the first n coordinates. -/
theorem coefficientProjection_eq_iff (n : ℕ) (x y : lp (fun _ : ℕ ↦ ℂ) 2) :
coefficientProjection n x = coefficientProjection n y ↔ ∀ i < n, x i = y i := by
constructor
· intro h i hi
have he := congrArg (fun v : lp (fun _ : ℕ ↦ ℂ) 2 ↦ v i) h
simpa [hi] using he
· intro h
ext i
by_cases hi : i < n <;> simp [hi, h]
theorem lp.eventually_existsUnique_coefficient_system (K : ↥(lp (fun x => ℂ) 2) →L[ℂ] ↥(lp (fun x => ℂ) 2))
(hK : IsCompactOperator ⇑K) (hT : IsUnit (1 + K)) :
∀ᶠ (n : ℕ) in Filter.atTop,
∀ (f : ↥(lp (fun x => ℂ) 2)), ∃! x, (∀ (i : ℕ), n ≤ i → ↑x i = 0) ∧ ∀ i < n, ↑((1 + K) x) i = ↑f i
Lean proof
/-- An invertible compact perturbation has unique leading finite coefficient
systems for every sufficiently large size and every right-hand side. -/
theorem eventually_existsUnique_coefficient_system
(K : lp (fun _ : ℕ ↦ ℂ) 2 →L[ℂ] lp (fun _ : ℕ ↦ ℂ) 2)
(hK : IsCompactOperator K) (hT : IsUnit (1 + K)) :
∀ᶠ n in atTop, ∀ f : lp (fun _ : ℕ ↦ ℂ) 2, ∃! x : lp (fun _ : ℕ ↦ ℂ) 2,
(∀ i, n ≤ i → x i = 0) ∧ (∀ i < n, ((1 + K) x) i = f i) := by
filter_upwards [eventually_stable_liftedFiniteSection (coefficientProjection (𝕜 := ℂ))
(norm_coefficientProjection_le (𝕜 := ℂ)) (tendsto_coefficientProjection (𝕜 := ℂ)) K hK hT] with n hn f
simpa only [coefficientProjection_eq_self_iff, coefficientProjection_eq_iff] using
existsUnique_projected_solution (coefficientProjection n) K
(coefficientProjection_idempotent n) hn.1 f
The full-constant Chebyshev multiplication matrix extends to a bounded operator \(J\) on complex \(\ell ^2\). For a real polynomial \(p\), \(p(J)\) agrees with multiplication by \(p\) on finite polynomial coordinates. The bounded map \(S\) with \((Sa)_0=a_0-a_2/2\) and \((Sa)_j=(a_j-a_{j+2})/2\) for \(j{\gt}0\) agrees with conversion from \(T\) to \(U=C^{(1)}\).
/-- Embed the finite coordinates of a real polynomial basis into complex lp. -/
noncomputable def coefficientLp (b : Basis ℕ ℝ ℝ[X]) :
ℝ[X] →ₗ[ℝ] lp (fun _ : ℕ ↦ ℂ) 2 where
toFun p := ⟨fun i ↦ (b.repr p i : ℂ), by
apply Memℓp.of_exponent_ge (p := 2) (q := 0) _ (by norm_num)
apply memℓp_zero_iff.mpr
apply (b.repr p).support.finite_toSet.subset
intro i hi
simp only [Finset.mem_coe, Finsupp.mem_support_iff]
exact fun hz ↦ hi (by simp [hz])⟩
map_add' p q := by
apply lp.ext
funext i
change ((b.repr (p + q) i : ℝ) : ℂ) = (b.repr p i : ℂ) + (b.repr q i : ℂ)
simp
map_smul' r p := by
apply lp.ext
funext i
change ((b.repr (r • p) i : ℝ) : ℂ) = (r : ℂ) * (b.repr p i : ℂ)
simp
For arbitrary real polynomial coefficients \(a_0,a_1\), represent \(Lu=a_0u+a_1u'\) with Chebyshev input and \(C^{(1)}\) output. Put \(d_j=\operatorname {natDegree}a_j\). The residual matrix has bandwidths
theorem Polynomial.chebyshev_firstOrder_isBanded (a : ℕ → Polynomial ℝ) :
((Polynomial.gegenbauerBasis Polynomial.chebyshev_firstOrder_isBanded._proof_1
Polynomial.chebyshev_firstOrder_isBanded._proof_2).toMatrix
fun j => (Polynomial.differentialOperator a 1) (Polynomial.chebyshevBasis j)).IsBanded
(max (a 0).natDegree (a 1).natDegree) (max ((a 0).natDegree + 2) ((a 1).natDegree + 1))
Lean proof
/-- The first-order ultraspherical residual has explicit lower and upper
bandwidths, including the conversion term and full-constant column. -/
theorem chebyshev_firstOrder_isBanded (a : ℕ → ℝ[X]) :
((gegenbauerBasis (by norm_num : -(1 / 2 : ℝ) < 1) (by norm_num : (1 : ℝ) ≠ 0)).toMatrix
(fun j ↦ differentialOperator a 1 (chebyshevBasis j))).IsBanded
(max (a 0).natDegree (a 1).natDegree)
(max ((a 0).natDegree + 2) ((a 1).natDegree + 1)) := by
let b := chebyshevBasis
let c := gegenbauerBasis (by norm_num : -(1 / 2 : ℝ) < 1) (by norm_num : (1 : ℝ) ≠ 0)
have hm (p : ℝ[X]) : (c.toMatrix (fun j ↦ p * c j)).IsBanded p.natDegree p.natDegree :=
gegenbauerBasis_polynomial_mul_isBanded _ _ p
have hc : (c.toMatrix (fun j ↦ (LinearMap.id : Module.End ℝ ℝ[X]) (b j))).IsBanded 0 2 :=
chebyshevBasis_conversion_isBanded
have hd : (c.toMatrix (fun j ↦ derivative (b j))).IsBanded 0 1 := by
simpa only [Nat.cast_zero, zero_add, Nat.zero_add, Function.iterate_one] using
chebyshevBasis_iterate_derivative_isBanded 0
have h₀ := b.toMatrix_comp_isBanded c c LinearMap.id (LinearMap.mulLeft ℝ (a 0)) hc (hm _)
have h₁ := b.toMatrix_comp_isBanded c c derivative (LinearMap.mulLeft ℝ (a 1)) hd (hm _)
have h₀' := h₀.mono (show 0 + (a 0).natDegree ≤ max (a 0).natDegree (a 1).natDegree by omega)
(show 2 + (a 0).natDegree ≤ max ((a 0).natDegree + 2) ((a 1).natDegree + 1) by omega)
have h₁' := h₁.mono (show 0 + (a 1).natDegree ≤ max (a 0).natDegree (a 1).natDegree by omega)
(show 1 + (a 1).natDegree ≤ max ((a 0).natDegree + 2) ((a 1).natDegree + 1) by omega)
intro i j hij
change c.repr (differentialOperator a 1 (b j)) i = 0
rw [differentialOperator_one_apply, map_add, Finsupp.add_apply]
have hz₀ : c.repr (a 0 * b j) i = 0 := h₀' i j hij
have hz₁ : c.repr (a 1 * derivative (b j)) i = 0 := h₁' i j hij
rw [hz₀, hz₁, add_zero]
For a normalized differential equation of order \(N\), differentiation is sparse when its output is expressed in \(C^{(N)}\). Polynomial multiplication is bounded, and conversion from a lower positive ultraspherical level is compact. These facts give a compact remainder after right preconditioning. Boundary rows must be bounded in the chosen coefficient norm; invertibility of the infinite bordered operator remains an assumption.
Weighted spaces and coefficient operators
Definition
4.4.19Degree-weighted coefficient space
For \(s\in \mathbb N\), let \(W_s\) consist of complex sequences \(v\) for which \(((n+1)^s v_n)_{n\ge 0}\in \ell ^2\), with norm \(\| v\| _s=\| ((n+1)^s v_n)_n\| _{\ell ^2}\). Write \(U_sv=((n+1)^sv_n)_n\).
def lp.degreeWeightedL2Equiv (s : ℕ) : lp.DegreeWeightedL2 s ≃ₗ[ℂ] ↥(lp (fun x => ℂ) 2)
Lean definition
/-- Degree weighting identifies the weighted coefficient space with ordinary ℓ². -/
def degreeWeightedL2Equiv : DegreeWeightedL2 s ≃ₗ[ℂ] lp (fun _ : ℕ ↦ ℂ) 2 where
toFun u := ⟨fun n : ℕ ↦ ((n : ℂ)+1)^s*u.1 n, u.2⟩
invFun v := ⟨fun n : ℕ ↦ v n / ((n : ℂ)+1)^s, by
change Memℓp (fun n : ℕ ↦ ((n : ℂ)+1)^s*(v n / ((n : ℂ)+1)^s)) 2
have he (n : ℕ) : ((n : ℂ)+1)^s*(v n / ((n : ℂ)+1)^s) = v n := by
field_simp
simpa only [he] using lp.memℓp v⟩
left_inv u := by
apply Subtype.ext
funext n
change (((n : ℂ)+1)^s*u.1 n)/((n : ℂ)+1)^s = u.1 n
field_simp
right_inv v := by
apply lp.ext
funext n
change ((n : ℂ)+1)^s*(v n / ((n : ℂ)+1)^s) = v n
field_simp
map_add' u v := by
apply lp.ext
funext n
exact mul_add _ _ _
map_smul' c u := by
apply lp.ext
funext n
change ((n : ℂ)+1)^s*(c*u.1 n) = c*(((n : ℂ)+1)^s*u.1 n)
ring
def lp.degreeWeightedL2Isometry (s : ℕ) : lp.DegreeWeightedL2 s ≃ₗᵢ[ℂ] ↥(lp (fun x => ℂ) 2)
Lean definition
/-- Degree weighting is an isometry for the weighted coefficient norm. -/
def degreeWeightedL2Isometry : DegreeWeightedL2 s ≃ₗᵢ[ℂ] lp (fun _ : ℕ ↦ ℂ) 2 :=
{ degreeWeightedL2Equiv s with norm_map' := fun _ ↦ rfl }
On \(W_s\), define the diagonal \(D_dv=(d_nv_n)_n\) for a bounded sequence \(d\), the shifts \((Lv)_n=v_{n+1}\) and \((Rv)_0=0\), \((Rv)_{n+1}=v_n\), and the truncation \((P_mv)_n=v_n\) for \(n{\lt}m\) and \(0\) otherwise. Let \(\iota _s:W_s\to \ell ^2\) be the coordinate inclusion. For a bounded linear operator \(A\) on \(\ell ^2\), its weighted transport is \(U_s^{-1}AU_s\).
Lean Formalisation
def lp.degreeWeightedTransport (s : ℕ) (A : ↥(lp (fun x => ℂ) 2) →L[ℂ] ↥(lp (fun x => ℂ) 2)) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- Conjugation of an operator by degree weighting. -/
def degreeWeightedTransport (s : ℕ)
(A : lp (fun _ : ℕ ↦ ℂ) 2 →L[ℂ] lp (fun _ : ℕ ↦ ℂ) 2) :
DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s :=
(degreeWeightedL2Isometry s).symm.toContinuousLinearEquiv.toContinuousLinearMap.comp
(A.comp (degreeWeightedL2Isometry s).toContinuousLinearEquiv.toContinuousLinearMap)
def lp.degreeWeightedDiagonal (s : ℕ) (d : ℕ → ℂ) {C : ℝ} (hC : 0 ≤ C) (hd : ∀ (n : ℕ), ‖d n‖ ≤ C) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- A bounded diagonal multiplier on weighted sequences. -/
def degreeWeightedDiagonal (s : ℕ) (d : ℕ → ℂ) {C : ℝ}
(hC : 0 ≤ C) (hd : ∀ n, ‖d n‖ ≤ C) :
DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s :=
degreeWeightedTransport s (coefficientDiagonal d hC hd)
def lp.degreeWeightedShiftLeft (s : ℕ) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- Backward shift in the weighted coefficient norm. -/
def degreeWeightedShiftLeft (s : ℕ) : DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s :=
degreeWeightedTransport s
((coefficientDiagonal (degreeWeightLeftRatio s) zero_le_one
(norm_degreeWeightLeftRatio_le s)).comp coefficientShiftLeft)
def lp.degreeWeightedProjection (s N : ℕ) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- Truncation to the first N weighted coordinates. -/
def degreeWeightedProjection (s N : ℕ) : DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s :=
degreeWeightedTransport s (coefficientProjection N)
These operators are bounded. The inclusion is injective; \(\| P_m\| \le 1\), \(P_mv\to v\) in \(W_s\), and \(P_m\) is compact. A bounded diagonal tending to zero is compact on \(W_s\). Moreover \((L^Nv)_n=v_{n+N}\) and \(R^NL^N=I-P_N\).
Lean Formalisation
theorem lp.degreeWeightedDiagonal_apply (s : ℕ) (d : ℕ → ℂ) {C : ℝ} (hC : 0 ≤ C) (hd : ∀ (n : ℕ), ‖d n‖ ≤ C)
(x : lp.DegreeWeightedL2 s) (n : ℕ) : ↑((lp.degreeWeightedDiagonal s d hC hd) x) n = d n * ↑x n
Lean proof
/-- Diagonal transport preserves the coordinatewise multiplier. -/
theorem degreeWeightedDiagonal_apply (s : ℕ) (d : ℕ → ℂ) {C : ℝ}
(hC : 0 ≤ C) (hd : ∀ n, ‖d n‖ ≤ C) (x : DegreeWeightedL2 s) (n : ℕ) :
(degreeWeightedDiagonal s d hC hd x).1 n = d n * x.1 n := by
change (d n * (((n : ℂ) + 1)^s * x.1 n)) / ((n : ℂ) + 1)^s = _
field_simp
theorem lp.degreeWeightedProjection_apply (s N : ℕ) (x : lp.DegreeWeightedL2 s) (i : ℕ) :
↑((lp.degreeWeightedProjection s N) x) i = if i < N then ↑x i else 0
Lean proof
@[simp] theorem degreeWeightedProjection_apply (s N : ℕ)
(x : DegreeWeightedL2 s) (i : ℕ) :
(degreeWeightedProjection s N x).1 i = if i < N then x.1 i else 0 := by
rw [degreeWeightedProjection, degreeWeightedTransport_apply, coefficientProjection_apply]
split_ifs
· change (((i : ℂ) + 1)^s * x.1 i) / ((i : ℂ) + 1)^s = _
field_simp
· exact zero_div _
theorem lp.tendsto_degreeWeightedProjection (s : ℕ) (x : lp.DegreeWeightedL2 s) :
Filter.Tendsto (fun N => (lp.degreeWeightedProjection s N) x) Filter.atTop (nhds x)
Lean proof
/-- Truncations converge in the weighted coefficient norm. -/
theorem tendsto_degreeWeightedProjection (s : ℕ) (x : DegreeWeightedL2 s) :
Tendsto (fun N ↦ degreeWeightedProjection s N x) atTop (𝓝 x) := by
have h := (degreeWeightedL2Isometry s).symm.continuous.continuousAt.tendsto.comp
(tendsto_coefficientProjection (degreeWeightedL2Isometry s x))
change Tendsto (fun N ↦ (degreeWeightedL2Isometry s).symm
(coefficientProjection N (degreeWeightedL2Isometry s x))) atTop (𝓝 x)
simpa only [Function.comp_def, LinearIsometryEquiv.symm_apply_apply] using h
theorem lp.degreeWeightedInclusion_injective (s : ℕ) : Function.Injective ⇑(lp.degreeWeightedInclusion s)
Lean proof
/-- The weighted inclusion does not identify distinct coefficient sequences. -/
theorem degreeWeightedInclusion_injective (s : ℕ) : Function.Injective (degreeWeightedInclusion s) := by
intro x y h
apply Subtype.ext
funext n
simpa only [degreeWeightedInclusion_apply] using congrArg (fun v : lp (fun _ : ℕ ↦ ℂ) 2 ↦ v n) h
theorem lp.isCompactOperator_degreeWeightedDiagonal (s : ℕ) (d : ℕ → ℂ) {C : ℝ} (hC : 0 ≤ C) (hd : ∀ (n : ℕ), ‖d n‖ ≤ C)
(hlim : Filter.Tendsto d Filter.atTop (nhds 0)) : IsCompactOperator ⇑(lp.degreeWeightedDiagonal s d hC hd)
Lean proof
/-- A diagonal tending to zero is compact in the weighted norm. -/
theorem isCompactOperator_degreeWeightedDiagonal (s : ℕ) (d : ℕ → ℂ) {C : ℝ}
(hC : 0 ≤ C) (hd : ∀ n, ‖d n‖ ≤ C) (hlim : Tendsto d atTop (𝓝 0)) :
IsCompactOperator (degreeWeightedDiagonal s d hC hd) :=
isCompactOperator_degreeWeightedTransport s _
(isCompactOperator_coefficientDiagonal d hC hd hlim)
theorem lp.isCompactOperator_degreeWeightedProjection (s N : ℕ) : IsCompactOperator ⇑(lp.degreeWeightedProjection s N)
Lean proof
/-- Weighted truncation is compact. -/
theorem isCompactOperator_degreeWeightedProjection (s N : ℕ) :
IsCompactOperator (degreeWeightedProjection s N) :=
isCompactOperator_degreeWeightedTransport s _ (isCompactOperator_coefficientProjection N)
theorem lp.degreeWeightedShiftLeft_pow_apply (s N : ℕ) (x : lp.DegreeWeightedL2 s) (i : ℕ) :
↑((lp.degreeWeightedShiftLeft s ^ N) x) i = ↑x (i + N)
Lean proof
/-- Iterated backward shift removes the first N coordinates. -/
theorem degreeWeightedShiftLeft_pow_apply (s N : ℕ) (x : DegreeWeightedL2 s) (i : ℕ) :
(((degreeWeightedShiftLeft s)^N) x).1 i = x.1 (i + N) := by
induction N generalizing i with
| zero => simp
| succ N ih =>
rw [pow_succ', mul_apply_eq_comp, degreeWeightedShiftLeft_apply, ih]
rw [show i + 1 + N = i + (N + 1) by omega]
theorem lp.degreeWeightedShiftRight_pow_apply (s N : ℕ) (x : lp.DegreeWeightedL2 s) (i : ℕ) :
↑((lp.degreeWeightedShiftRight s ^ N) x) i = if i < N then 0 else ↑x (i - N)
Lean proof
/-- Iterated forward shift inserts N zero coordinates. -/
theorem degreeWeightedShiftRight_pow_apply (s N : ℕ) (x : DegreeWeightedL2 s) (i : ℕ) :
(((degreeWeightedShiftRight s)^N) x).1 i = if i < N then 0 else x.1 (i - N) := by
induction N generalizing i with
| zero => simp
| succ N ih =>
rw [pow_succ', mul_apply_eq_comp]
cases i with
| zero => simp [degreeWeightedShiftRight_zero]
| succ i =>
rw [degreeWeightedShiftRight_succ, ih]
simp only [Nat.add_lt_add_iff_right, Nat.add_sub_add_right]
theorem lp.degreeWeightedShiftRight_mul_left (s N : ℕ) :
lp.degreeWeightedShiftRight s ^ N * lp.degreeWeightedShiftLeft s ^ N = 1 - lp.degreeWeightedProjection s N
Lean proof
/-- Deleting and reinserting the first N coordinates gives the complementary projection. -/
theorem degreeWeightedShiftRight_mul_left (s N : ℕ) :
(degreeWeightedShiftRight s)^N * (degreeWeightedShiftLeft s)^N =
1 - degreeWeightedProjection s N := by
apply ContinuousLinearMap.ext
intro x
apply Subtype.ext
funext i
change (((degreeWeightedShiftRight s)^N) (((degreeWeightedShiftLeft s)^N) x)).1 i =
x.1 i - (degreeWeightedProjection s N x).1 i
rw [degreeWeightedShiftRight_pow_apply, degreeWeightedProjection_apply]
split_ifs with hi
· simp
· rw [degreeWeightedShiftLeft_pow_apply, Nat.sub_add_cancel (by omega)]
simp
The map \(S_\lambda \) is compact on \(\ell ^2\) and converts polynomial \(C^{(\lambda )}\) coordinates to \(C^{(\lambda +1)}\) coordinates. The bounded maps \(J_\lambda \) and \(M_\lambda [a]\) represent multiplication by \(x\) and \(a(x)\), respectively, in the \(C^{(\lambda )}\) basis.
For a real polynomial basis \(b=(b_n)\) and \(p\in \mathbb R[x]\), let \(c_b(p)\in W_s\) be its finite coordinate sequence, regarded as complex coefficients.
Lean Formalisation
def Module.Basis.degreeWeightedCoefficient (b : Module.Basis ℕ ℝ (Polynomial ℝ)) (s : ℕ) (p : Polynomial ℝ) :
lp.DegreeWeightedL2 s
Lean definition
/-- Finite polynomial coordinates in a degree-weighted sequence space. -/
def degreeWeightedCoefficient (b : Basis ℕ ℝ ℝ[X]) (s : ℕ) (p : ℝ[X]) : lp.DegreeWeightedL2 s :=
⟨fun i ↦ (b.repr p i : ℂ), by
apply Memℓp.of_exponent_ge (p := 2) (q := 0) _ (by norm_num)
apply memℓp_zero_iff.mpr
apply (b.repr p).support.finite_toSet.subset
intro i hi
simp only [Finset.mem_coe, Finsupp.mem_support_iff]
exact fun hz ↦ hi (by simp [hz])⟩
Weighted polynomial coordinates preserve addition and real scalar multiplication. Their inclusion into \(\ell ^2\) is the ordinary finite polynomial coefficient sequence.
Lean Formalisation
theorem Module.Basis.degreeWeightedCoefficient_inclusion (b : Module.Basis ℕ ℝ (Polynomial ℝ)) (s : ℕ) (p : Polynomial ℝ) :
(lp.degreeWeightedInclusion s) (b.degreeWeightedCoefficient s p) = b.coefficientLp p
Lean proof
/-- Weighted coordinates include into the usual polynomial coefficient sequence. -/
theorem degreeWeightedCoefficient_inclusion (b : Basis ℕ ℝ ℝ[X]) (s : ℕ) (p : ℝ[X]) :
lp.degreeWeightedInclusion s (b.degreeWeightedCoefficient s p) = b.coefficientLp p := by
ext i
rw [lp.degreeWeightedInclusion_apply]
rfl
theorem Module.Basis.degreeWeightedCoefficient_smul (b : Module.Basis ℕ ℝ (Polynomial ℝ)) (s : ℕ) (a : ℝ) (p : Polynomial ℝ) :
b.degreeWeightedCoefficient s (a • p) = ↑a • b.degreeWeightedCoefficient s p
Lean proof
/-- Polynomial coordinates preserve real scalar multiplication. -/
theorem degreeWeightedCoefficient_smul (b : Basis ℕ ℝ ℝ[X]) (s : ℕ) (a : ℝ) (p : ℝ[X]) :
b.degreeWeightedCoefficient s (a • p) = (a : ℂ) • b.degreeWeightedCoefficient s p := by
apply Subtype.ext
funext i
change ((b.repr (a • p) i : ℝ) : ℂ) = (a : ℂ) * (b.repr p i : ℂ)
simp
On \(W_s\), use the same coordinate formulas for \(S_\lambda \), \(J_\lambda \) and \(M_\lambda [a]\) at integer levels \(\lambda \ge 1\). At level zero set \(S_0=\tfrac 12(I-L^2+P_1)\), \(J_0=\tfrac 12(R(I+P_1)+L)\) and \(M_0[a]=a(J_0)\). Write \(S_{j\to N}=S_{N-1}\cdots S_j\) for successive conversion, with \(S_{j\to j}=I\).
Lean Formalisation
def Polynomial.Chebyshev.weightedChebyshevConversion (s : ℕ) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- The bounded T-to-U conversion on weighted coefficients. -/
def weightedChebyshevConversion (s : ℕ) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s :=
(1 / 2 : ℂ) • (1 - (lp.degreeWeightedShiftLeft s).comp (lp.degreeWeightedShiftLeft s)) +
(1 / 2 : ℂ) • lp.degreeWeightedProjection s 1
def Polynomial.Chebyshev.weightedPositiveMulX (s k : ℕ) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- Multiplication by x in a positive ultraspherical basis on weighted coefficients. -/
def weightedPositiveMulX (s k : ℕ) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s :=
(lp.degreeWeightedShiftRight s).comp (lp.degreeWeightedDiagonal s (positiveMulXUp k)
zero_le_one (norm_positiveMulXUp_le k)) +
(lp.degreeWeightedShiftLeft s).comp (lp.degreeWeightedDiagonal s (positiveMulXDown k)
zero_le_one (norm_positiveMulXDown_le k))
def Polynomial.Chebyshev.weightedPositivePolynomialMultiplier (s k : ℕ) (p : Polynomial ℝ) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- Polynomial functional calculus of weighted ultraspherical multiplication by x. -/
def weightedPositivePolynomialMultiplier (s k : ℕ) (p : ℝ[X]) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s :=
aeval (weightedPositiveMulX s k) (p.map Complex.ofRealHom)
On \(W_s\), multiplication by \(x\) and by a polynomial, conversion from the Chebyshev basis to the first ultraspherical basis, and conversion between positive ultraspherical parameters are bounded operators. On finite polynomial coefficient vectors, their coordinates equal those of the polynomial multiplication and conversion maps in Definition 4.4.27. Every conversion \(S_{j\to N}\) with \(1\le j{\lt}N\) is compact on \(W_s\).
Lean Formalisation
theorem Polynomial.Chebyshev.weightedChebyshevConversion_coefficient (s : ℕ) (p : Polynomial ℝ) :
(Polynomial.Chebyshev.weightedChebyshevConversion s) (Polynomial.chebyshevBasis.degreeWeightedCoefficient s p) =
(Polynomial.ultrasphericalBasis 1).degreeWeightedCoefficient s p
Lean proof
/-- Weighted T-to-U conversion agrees with polynomial basis conversion. -/
theorem weightedChebyshevConversion_coefficient (s : ℕ) (p : ℝ[X]) :
weightedChebyshevConversion s (chebyshevBasis.degreeWeightedCoefficient s p) =
(ultrasphericalBasis 1).degreeWeightedCoefficient s p := by
apply lp.degreeWeightedInclusion_injective s
rw [weightedChebyshevConversion_inclusion, Module.Basis.degreeWeightedCoefficient_inclusion,
Module.Basis.degreeWeightedCoefficient_inclusion, boundedConversion_coefficientLp]
theorem Polynomial.Chebyshev.weightedChebyshevMulX_coefficient (s : ℕ) (p : Polynomial ℝ) :
(Polynomial.Chebyshev.weightedChebyshevMulX s) (Polynomial.chebyshevBasis.degreeWeightedCoefficient s p) =
Polynomial.chebyshevBasis.degreeWeightedCoefficient s (Polynomial.X * p)
Lean proof
/-- Weighted Chebyshev multiplication agrees with multiplication of polynomials. -/
theorem weightedChebyshevMulX_coefficient (s : ℕ) (p : ℝ[X]) :
weightedChebyshevMulX s (chebyshevBasis.degreeWeightedCoefficient s p) =
chebyshevBasis.degreeWeightedCoefficient s (X * p) := by
apply lp.degreeWeightedInclusion_injective s
rw [weightedChebyshevMulX_inclusion, Module.Basis.degreeWeightedCoefficient_inclusion,
Module.Basis.degreeWeightedCoefficient_inclusion, boundedMulX_coefficientLp]
theorem Polynomial.Chebyshev.weightedChebyshevPolynomialMultiplier_coefficient (s : ℕ) (p q : Polynomial ℝ) :
(Polynomial.Chebyshev.weightedChebyshevPolynomialMultiplier s p)
(Polynomial.chebyshevBasis.degreeWeightedCoefficient s q) =
Polynomial.chebyshevBasis.degreeWeightedCoefficient s (p * q)
Lean proof
/-- Weighted Chebyshev functional calculus gives polynomial multiplication. -/
theorem weightedChebyshevPolynomialMultiplier_coefficient (s : ℕ) (p q : ℝ[X]) :
weightedChebyshevPolynomialMultiplier s p
(chebyshevBasis.degreeWeightedCoefficient s q) =
chebyshevBasis.degreeWeightedCoefficient s (p * q) := by
unfold weightedChebyshevPolynomialMultiplier
induction p using Polynomial.induction_on generalizing q with
| C a =>
rw [Polynomial.map_C, Polynomial.aeval_C]
change (a : ℂ) • chebyshevBasis.degreeWeightedCoefficient s q = _
rw [← Module.Basis.degreeWeightedCoefficient_smul, smul_eq_C_mul]
| add p r hp hr =>
rw [Polynomial.map_add, map_add, add_apply, hp, hr, add_mul,
Module.Basis.degreeWeightedCoefficient_add]
| monomial n a ih =>
rw [pow_succ, ← mul_assoc, Polynomial.map_mul, map_mul, mul_apply_eq_comp,
Polynomial.map_X, aeval_X, weightedChebyshevMulX_coefficient, ih]
simp only [mul_assoc]
theorem Polynomial.Chebyshev.weightedPositiveConversion_coefficient (s k : ℕ) (p : Polynomial ℝ) :
(Polynomial.Chebyshev.weightedPositiveConversion s k)
((Polynomial.ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s p) =
(Polynomial.ultrasphericalBasis (k + 2)).degreeWeightedCoefficient s p
Lean proof
/-- Weighted conversion agrees with polynomial basis conversion. -/
theorem weightedPositiveConversion_coefficient (s k : ℕ) (p : ℝ[X]) :
weightedPositiveConversion s k ((ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s p) =
(ultrasphericalBasis (k + 2)).degreeWeightedCoefficient s p := by
apply lp.degreeWeightedInclusion_injective s
rw [weightedPositiveConversion_inclusion, Module.Basis.degreeWeightedCoefficient_inclusion,
Module.Basis.degreeWeightedCoefficient_inclusion, boundedPositiveConversion_coefficientLp]
theorem Polynomial.Chebyshev.weightedPositivePolynomialMultiplier_coefficient (s k : ℕ) (p q : Polynomial ℝ) :
(Polynomial.Chebyshev.weightedPositivePolynomialMultiplier s k p)
((Polynomial.ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s q) =
(Polynomial.ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s (p * q)
Lean proof
/-- Weighted ultraspherical functional calculus gives polynomial multiplication. -/
theorem weightedPositivePolynomialMultiplier_coefficient (s k : ℕ) (p q : ℝ[X]) :
weightedPositivePolynomialMultiplier s k p
((ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s q) =
(ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s (p * q) := by
unfold weightedPositivePolynomialMultiplier
induction p using Polynomial.induction_on generalizing q with
| C a =>
rw [Polynomial.map_C, Polynomial.aeval_C]
change (a : ℂ) • (ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s q = _
rw [← Module.Basis.degreeWeightedCoefficient_smul, smul_eq_C_mul]
| add p r hp hr =>
rw [Polynomial.map_add, map_add, add_apply, hp, hr, add_mul,
Module.Basis.degreeWeightedCoefficient_add]
| monomial n a ih =>
rw [pow_succ, ← mul_assoc, Polynomial.map_mul, map_mul, mul_apply_eq_comp,
Polynomial.map_X, aeval_X, weightedPositiveMulX_coefficient, ih]
simp only [mul_assoc]
theorem Polynomial.Chebyshev.weightedPositiveRaise_coefficient (s k d : ℕ) (p : Polynomial ℝ) :
(Polynomial.Chebyshev.weightedPositiveRaise s k d)
((Polynomial.ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s p) =
(Polynomial.ultrasphericalBasis (k + d + 1)).degreeWeightedCoefficient s p
Lean proof
/-- Successive conversions give the polynomial coordinates at the final level. -/
theorem weightedPositiveRaise_coefficient (s k d : ℕ) (p : ℝ[X]) :
weightedPositiveRaise s k d ((ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s p) =
(ultrasphericalBasis (k + d + 1)).degreeWeightedCoefficient s p := by
induction d with
| zero => rfl
| succ d ih =>
simp only [weightedPositiveRaise, comp_apply, ih, weightedPositiveConversion_coefficient]
congr 2
theorem Polynomial.Chebyshev.isCompactOperator_weightedPositiveConversion (s k : ℕ) :
IsCompactOperator ⇑(Polynomial.Chebyshev.weightedPositiveConversion s k)
Lean proof
/-- Positive-level conversion is compact in every degree-weighted norm. -/
theorem isCompactOperator_weightedPositiveConversion (s k : ℕ) :
IsCompactOperator (weightedPositiveConversion s k) := by
unfold weightedPositiveConversion
exact (lp.isCompactOperator_degreeWeightedDiagonal s (positiveConversionDiagonal k)
zero_le_one (norm_positiveConversionDiagonal_le k) (tendsto_positiveConversionDiagonal k)).clm_comp
(1 - (lp.degreeWeightedShiftLeft s).comp (lp.degreeWeightedShiftLeft s))
theorem Polynomial.Chebyshev.isCompactOperator_weightedPositiveRaise (s k d : ℕ) :
IsCompactOperator ⇑(Polynomial.Chebyshev.weightedPositiveRaise s k (d + 1))
Lean proof
/-- Any nonempty positive conversion chain is compact. -/
theorem isCompactOperator_weightedPositiveRaise (s k d : ℕ) :
IsCompactOperator (weightedPositiveRaise s k (d + 1)) :=
(isCompactOperator_weightedPositiveConversion s (k + d)).comp_clm (weightedPositiveRaise s k d)
Let \(N=k+1\) and \(c_k=2^k k!\). Define \(\mathcal R_N=c_k^{-1}\operatorname {diag}(1,1,1/2,1/3,\ldots )\) on \(W_s\). For \(j\ge 0\), define the preconditioned order-\((j+1)\) derivative by \(E_{N,j+1}=(c_j/c_k)L^{j+1}\).
Lean Formalisation
def Polynomial.Chebyshev.weightedFirstOrderPreconditioner (s : ℕ) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- Reciprocal-degree preconditioning in the weighted coefficient norm. -/
def weightedFirstOrderPreconditioner (s : ℕ) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s :=
lp.degreeWeightedDiagonal s firstOrderDiagonal zero_le_one norm_firstOrderDiagonal_le
def Polynomial.Chebyshev.weightedUltrasphericalPreconditioner (s k : ℕ) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- Order k+1 right preconditioner, with reciprocal-degree scaling on positive modes. -/
def weightedUltrasphericalPreconditioner (s k : ℕ) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s :=
(ultrasphericalDerivativeScale k)⁻¹ • weightedFirstOrderPreconditioner s
The map \(\mathcal R_N\) is compact and \(E_{N,N}=L^N\). If \(\mathcal R_Nv=c_T(p)\) for a polynomial \(p\), then \(E_{N,j+1}v=c_{C^{(j+1)}}(p^{(j+1)})\) for every \(j\ge 0\).
Lean Formalisation
theorem Polynomial.Chebyshev.ultrasphericalDerivativeScale_ne_zero (k : ℕ) :
Polynomial.Chebyshev.ultrasphericalDerivativeScale k ≠ 0
Lean proof
/-- The derivative normalization factor is nonzero. -/
theorem ultrasphericalDerivativeScale_ne_zero (k : ℕ) : ultrasphericalDerivativeScale k ≠ 0 := by
unfold ultrasphericalDerivativeScale
exact mul_ne_zero (pow_ne_zero _ (by norm_num)) (by exact_mod_cast Nat.factorial_ne_zero k)
theorem Polynomial.Chebyshev.isCompactOperator_weightedUltrasphericalPreconditioner (s k : ℕ) :
IsCompactOperator ⇑(Polynomial.Chebyshev.weightedUltrasphericalPreconditioner s k)
Lean proof
/-- The normalized right preconditioner is compact. -/
theorem isCompactOperator_weightedUltrasphericalPreconditioner (s k : ℕ) :
IsCompactOperator (weightedUltrasphericalPreconditioner s k) := by
change IsCompactOperator ((ultrasphericalDerivativeScale k)⁻¹ • ⇑(weightedFirstOrderPreconditioner s))
exact (isCompactOperator_weightedFirstOrderPreconditioner s).smul _
theorem Polynomial.Chebyshev.weightedPreconditionedDerivative_top (s k : ℕ) :
Polynomial.Chebyshev.weightedPreconditionedDerivative s k k = lp.degreeWeightedShiftLeft s ^ (k + 1)
Lean proof
/-- The highest preconditioned derivative is the backward shift of the differential order. -/
theorem weightedPreconditionedDerivative_top (s k : ℕ) :
weightedPreconditionedDerivative s k k = (lp.degreeWeightedShiftLeft s)^(k + 1) := by
simp [weightedPreconditionedDerivative, ultrasphericalDerivativeScale_ne_zero]
theorem Polynomial.Chebyshev.weightedPreconditionedDerivative_coefficient (s k j : ℕ) (v : lp.DegreeWeightedL2 s)
(p : Polynomial ℝ)
(hv :
(Polynomial.Chebyshev.weightedUltrasphericalPreconditioner s k) v =
Polynomial.chebyshevBasis.degreeWeightedCoefficient s p) :
(Polynomial.Chebyshev.weightedPreconditionedDerivative s k j) v =
(Polynomial.ultrasphericalBasis (j + 1)).degreeWeightedCoefficient s ((Polynomial.derivative ^ (j + 1)) p)
Lean proof
/-- Preconditioned derivatives agree with every polynomial derivative in its natural basis. -/
theorem weightedPreconditionedDerivative_coefficient (s k j : ℕ)
(v : lp.DegreeWeightedL2 s) (p : ℝ[X])
(hv : weightedUltrasphericalPreconditioner s k v = chebyshevBasis.degreeWeightedCoefficient s p) :
weightedPreconditionedDerivative s k j v =
(ultrasphericalBasis (j + 1)).degreeWeightedCoefficient s ((derivative ^ (j + 1)) p) := by
apply Subtype.ext
funext i
change (ultrasphericalDerivativeScale j / ultrasphericalDerivativeScale k) *
(((lp.degreeWeightedShiftLeft s)^(j + 1)) v).1 i =
((ultrasphericalBasis (j + 1)).repr ((derivative ^ (j + 1)) p) i : ℂ)
rw [lp.degreeWeightedShiftLeft_pow_apply, ultraspherical_derivative_coordinate]
have h := congrArg (fun w : lp.DegreeWeightedL2 s ↦ w.1 (i + j + 1)) hv
change (ultrasphericalDerivativeScale k)⁻¹ *
(weightedFirstOrderPreconditioner s v).1 (i + j + 1) =
(chebyshevBasis.repr p (i + j + 1) : ℂ) at h
rw [weightedFirstOrderPreconditioner_apply] at h
push_cast
rw [← h, firstOrderDiagonal_succ]
simp only [ultrasphericalDerivativeScale]
push_cast
have hn : (i : ℂ) + j + 1 ≠ 0 := by exact_mod_cast (show i + j + 1 ≠ 0 by omega)
rw [show i + (j + 1) = i + j + 1 by omega]
field_simp
The diagonal above differs from the usual order-\(N\) preconditioner only in finitely many modes below degree \(N\). These modes are annihilated by the highest derivative; the chosen normalization also makes every positive lower derivative a scalar multiple of a shift.
For bounded maps \(B,A:W_s\to W_s\), define \(K_{N,B,A}=P_N(B-I)+R^N A\). The first \(N\) coordinates of \(Bv\) specify the boundary data; coordinates of \(Bv\) with index at least \(N\) are unused.
Lean Formalisation
def lp.degreeWeightedBoundaryCorrection (s N : ℕ) (B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- Replace the first N identity rows by the bounded rows of B. -/
def degreeWeightedBoundaryCorrection (s N : ℕ)
(B : DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s) :
DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s :=
(degreeWeightedProjection s N).comp (B - 1)
def lp.degreeWeightedBorderedRemainder (s N : ℕ) (B A : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- Bordered remainder for a normalized derivative and lower-order operator. -/
def degreeWeightedBorderedRemainder (s N : ℕ)
(B A : DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s) :
DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s :=
degreeWeightedBoundaryCorrection s N B + ((degreeWeightedShiftRight s)^N).comp A
If \(A\) is compact, so is \(K_{N,B,A}\). The first \(N\) rows of \(I+K_{N,B,A}\) are \(B\), and its row \(N+i\) is \(v_{N+i}+(Av)_i\).
Lean Formalisation
theorem lp.isCompactOperator_degreeWeightedBoundaryCorrection (s N : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) :
IsCompactOperator ⇑(lp.degreeWeightedBoundaryCorrection s N B)
Lean proof
/-- A finite collection of bounded boundary rows gives a compact correction. -/
theorem isCompactOperator_degreeWeightedBoundaryCorrection (s N : ℕ)
(B : DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s) :
IsCompactOperator (degreeWeightedBoundaryCorrection s N B) :=
(isCompactOperator_degreeWeightedProjection s N).comp_clm (B - 1)
theorem lp.isCompactOperator_degreeWeightedBorderedRemainder (s N : ℕ) (B A : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s)
(hA : IsCompactOperator ⇑A) : IsCompactOperator ⇑(lp.degreeWeightedBorderedRemainder s N B A)
Lean proof
/-- Bordering a compact lower-order operator preserves compactness of the remainder. -/
theorem isCompactOperator_degreeWeightedBorderedRemainder (s N : ℕ)
(B A : DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s) (hA : IsCompactOperator A) :
IsCompactOperator (degreeWeightedBorderedRemainder s N B A) :=
(isCompactOperator_degreeWeightedBoundaryCorrection s N B).add
(hA.clm_comp ((degreeWeightedShiftRight s)^N))
theorem lp.degreeWeightedBorderedRemainder_rows (s N : ℕ) (B A : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s)
(x : lp.DegreeWeightedL2 s) (i : ℕ) :
↑((1 + lp.degreeWeightedBorderedRemainder s N B A) x) i = if i < N then ↑(B x) i else ↑x i + ↑(A x) (i - N)
Lean proof
/-- The bordered operator imposes the boundary rows, then the shifted interior rows. -/
theorem degreeWeightedBorderedRemainder_rows (s N : ℕ)
(B A : DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s)
(x : DegreeWeightedL2 s) (i : ℕ) :
((1 + degreeWeightedBorderedRemainder s N B A) x).1 i =
if i < N then (B x).1 i else x.1 i + (A x).1 (i - N) := by
change x.1 i + (((degreeWeightedProjection s N) ((B - 1) x)).1 i +
(((degreeWeightedShiftRight s)^N) (A x)).1 i) = _
rw [degreeWeightedProjection_apply, degreeWeightedShiftRight_pow_apply]
split_ifs
· change x.1 i + (((B x).1 i - x.1 i) + 0) = _
abel
· simp
def Polynomial.Chebyshev.weightedUltrasphericalZeroTerm (s k : ℕ) (a : Polynomial ℝ) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- The zeroth-order term raised to the final ultraspherical level. -/
def weightedUltrasphericalZeroTerm (s k : ℕ) (a : ℝ[X]) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s :=
(weightedPositiveRaise s 0 k).comp ((weightedChebyshevConversion s).comp
((weightedChebyshevPolynomialMultiplier s a).comp (weightedUltrasphericalPreconditioner s k)))
def Polynomial.Chebyshev.weightedUltrasphericalPositiveTerm (s k : ℕ) (j : Fin k) (a : Polynomial ℝ) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- A positive lower-order term raised to the final ultraspherical level. -/
def weightedUltrasphericalPositiveTerm (s k : ℕ) (j : Fin k) (a : ℝ[X]) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s :=
(weightedPositiveRaise s j (k - j)).comp
((weightedPositivePolynomialMultiplier s j a).comp (weightedPreconditionedDerivative s k j))
def Polynomial.Chebyshev.weightedUltrasphericalLowerTerms (s k : ℕ) (a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- The sum of all preconditioned lower-order polynomial terms. -/
def weightedUltrasphericalLowerTerms (s k : ℕ) (a₀ : ℝ[X]) (a : Fin k → ℝ[X]) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s :=
weightedUltrasphericalZeroTerm s k a₀ + ∑ j, weightedUltrasphericalPositiveTerm s k j (a j)
def Polynomial.Chebyshev.weightedUltrasphericalRemainder (s k : ℕ) (B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s)
(a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- The bordered polynomial differential operator minus the identity. -/
def weightedUltrasphericalRemainder (s k : ℕ) (B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s)
(a₀ : ℝ[X]) (a : Fin k → ℝ[X]) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s :=
lp.degreeWeightedBorderedRemainder s (k + 1) B (weightedUltrasphericalLowerTerms s k a₀ a)
The operators \(A\) and \(K\) are compact on \(W_s\). If \(\mathcal R_Nv=c_T(p)\) for a polynomial \(p\), the first \(N\) rows of \(Tv\) are \(Bv\), and the remaining rows are the \(C^{(N)}\) coordinates of
theorem Polynomial.Chebyshev.isCompactOperator_weightedUltrasphericalZeroTerm (s k : ℕ) (a : Polynomial ℝ) :
IsCompactOperator ⇑(Polynomial.Chebyshev.weightedUltrasphericalZeroTerm s k a)
Lean proof
/-- The zeroth-order term is compact through right preconditioning. -/
theorem isCompactOperator_weightedUltrasphericalZeroTerm (s k : ℕ) (a : ℝ[X]) :
IsCompactOperator (weightedUltrasphericalZeroTerm s k a) :=
(((isCompactOperator_weightedUltrasphericalPreconditioner s k).clm_comp
(weightedChebyshevPolynomialMultiplier s a)).clm_comp
(weightedChebyshevConversion s)).clm_comp (weightedPositiveRaise s 0 k)
theorem Polynomial.Chebyshev.isCompactOperator_weightedUltrasphericalPositiveTerm (s k : ℕ) (j : Fin k) (a : Polynomial ℝ) :
IsCompactOperator ⇑(Polynomial.Chebyshev.weightedUltrasphericalPositiveTerm s k j a)
Lean proof
/-- Each positive lower-order term contains a compact conversion. -/
theorem isCompactOperator_weightedUltrasphericalPositiveTerm (s k : ℕ) (j : Fin k) (a : ℝ[X]) :
IsCompactOperator (weightedUltrasphericalPositiveTerm s k j a) := by
have h : k - j = (k - j - 1) + 1 := by omega
have hc := (isCompactOperator_weightedPositiveRaise s j (k - j - 1)).comp_clm
((weightedPositivePolynomialMultiplier s j a).comp (weightedPreconditionedDerivative s k j))
rw [← h] at hc
exact hc
theorem Polynomial.Chebyshev.isCompactOperator_weightedUltrasphericalLowerTerms (s k : ℕ) (a₀ : Polynomial ℝ)
(a : Fin k → Polynomial ℝ) : IsCompactOperator ⇑(Polynomial.Chebyshev.weightedUltrasphericalLowerTerms s k a₀ a)
Lean proof
/-- The preconditioned lower-order differential operator is compact. -/
theorem isCompactOperator_weightedUltrasphericalLowerTerms (s k : ℕ)
(a₀ : ℝ[X]) (a : Fin k → ℝ[X]) :
IsCompactOperator (weightedUltrasphericalLowerTerms s k a₀ a) := by
apply (isCompactOperator_weightedUltrasphericalZeroTerm s k a₀).add
have h (t : Finset (Fin k)) :
IsCompactOperator (∑ j ∈ t, weightedUltrasphericalPositiveTerm s k j (a j) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) := by
induction t using Finset.induction_on with
| empty => simpa using (isCompactOperator_zero : IsCompactOperator
(0 : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s))
| @insert j t hj ih =>
rw [Finset.sum_insert hj]
exact (isCompactOperator_weightedUltrasphericalPositiveTerm s k j (a j)).add ih
exact h Finset.univ
theorem Polynomial.Chebyshev.isCompactOperator_weightedUltrasphericalRemainder (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ) :
IsCompactOperator ⇑(Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a)
Lean proof
/-- The higher-order bordered polynomial system is identity plus compact. -/
theorem isCompactOperator_weightedUltrasphericalRemainder (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : ℝ[X]) (a : Fin k → ℝ[X]) :
IsCompactOperator (weightedUltrasphericalRemainder s k B a₀ a) :=
lp.isCompactOperator_degreeWeightedBorderedRemainder s (k + 1) B _
(isCompactOperator_weightedUltrasphericalLowerTerms s k a₀ a)
theorem Polynomial.Chebyshev.weightedUltraspherical_polynomial_equation (s k : ℕ) (a₀ p : Polynomial ℝ)
(a : Fin k → Polynomial ℝ) (v : lp.DegreeWeightedL2 s)
(hv :
(Polynomial.Chebyshev.weightedUltrasphericalPreconditioner s k) v =
Polynomial.chebyshevBasis.degreeWeightedCoefficient s p) :
(lp.degreeWeightedShiftLeft s ^ (k + 1)) v + (Polynomial.Chebyshev.weightedUltrasphericalLowerTerms s k a₀ a) v =
(Polynomial.ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s
((Polynomial.derivative ^ (k + 1)) p + a₀ * p + ∑ j, a j * (Polynomial.derivative ^ (↑j + 1)) p)
Lean proof
/-- The assembled interior operator agrees with the entire polynomial differential expression. -/
theorem weightedUltraspherical_polynomial_equation (s k : ℕ) (a₀ p : ℝ[X])
(a : Fin k → ℝ[X]) (v : lp.DegreeWeightedL2 s)
(hv : weightedUltrasphericalPreconditioner s k v = chebyshevBasis.degreeWeightedCoefficient s p) :
((lp.degreeWeightedShiftLeft s)^(k + 1)) v + weightedUltrasphericalLowerTerms s k a₀ a v =
(ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s
((derivative^(k + 1)) p + a₀ * p + ∑ j : Fin k, a j * ((derivative^(j.val + 1)) p)) := by
have htop := weightedPreconditionedDerivative_coefficient s k k v p hv
rw [weightedPreconditionedDerivative_top] at htop
rw [weightedUltrasphericalLowerTerms, add_apply, sum_apply, htop,
weightedUltrasphericalZeroTerm_coefficient s k a₀ p v hv]
simp only [weightedUltrasphericalPositiveTerm_coefficient s k _ _ p v hv]
rw [Module.Basis.degreeWeightedCoefficient_add, Module.Basis.degreeWeightedCoefficient_add]
have hsum (t : Finset (Fin k)) :
(ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s
(∑ j ∈ t, a j * ((derivative^(j.val + 1)) p)) =
∑ j ∈ t, (ultrasphericalBasis (k + 1)).degreeWeightedCoefficient s
(a j * ((derivative^(j.val + 1)) p)) := by
induction t using Finset.induction_on with
| empty =>
simp only [Finset.sum_empty]
apply Subtype.ext
funext i
change (((ultrasphericalBasis (k + 1)).repr 0 i : ℝ) : ℂ) = 0
simp
| @insert j t hj ih =>
rw [Finset.sum_insert hj, Finset.sum_insert hj,
Module.Basis.degreeWeightedCoefficient_add, ih]
rw [hsum]
abel
theorem Polynomial.Chebyshev.weightedUltraspherical_boundary_rows (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ)
(v : lp.DegreeWeightedL2 s) (i : Fin (k + 1)) :
↑((1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a) v) ↑i = ↑(B v) ↑i
Lean proof
/-- The first k+1 rows impose the chosen bounded boundary conditions. -/
theorem weightedUltraspherical_boundary_rows (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : ℝ[X]) (a : Fin k → ℝ[X])
(v : lp.DegreeWeightedL2 s) (i : Fin (k + 1)) :
((1 + weightedUltrasphericalRemainder s k B a₀ a) v).1 i = (B v).1 i := by
rw [weightedUltrasphericalRemainder, lp.degreeWeightedBorderedRemainder_rows,
ite_eq_left i.isLt]
theorem Polynomial.Chebyshev.weightedUltraspherical_interior_polynomial_rows (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ p : Polynomial ℝ) (a : Fin k → Polynomial ℝ)
(v : lp.DegreeWeightedL2 s)
(hv :
(Polynomial.Chebyshev.weightedUltrasphericalPreconditioner s k) v =
Polynomial.chebyshevBasis.degreeWeightedCoefficient s p)
(i : ℕ) :
↑((1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a) v) (i + k + 1) =
↑(((Polynomial.ultrasphericalBasis (k + 1)).repr
((Polynomial.derivative ^ (k + 1)) p + a₀ * p + ∑ j, a j * (Polynomial.derivative ^ (↑j + 1)) p))
i)
Lean proof
/-- Every interior row is the corresponding ultraspherical coordinate of the polynomial residual. -/
theorem weightedUltraspherical_interior_polynomial_rows (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ p : ℝ[X]) (a : Fin k → ℝ[X])
(v : lp.DegreeWeightedL2 s)
(hv : weightedUltrasphericalPreconditioner s k v = chebyshevBasis.degreeWeightedCoefficient s p)
(i : ℕ) :
((1 + weightedUltrasphericalRemainder s k B a₀ a) v).1 (i + k + 1) =
((ultrasphericalBasis (k + 1)).repr
((derivative^(k + 1)) p + a₀ * p + ∑ j : Fin k, a j * ((derivative^(j.val + 1)) p)) i : ℂ) := by
have h := congrArg (fun x : lp.DegreeWeightedL2 s ↦ x.1 i)
(weightedUltraspherical_polynomial_equation s k a₀ p a v hv)
change (((lp.degreeWeightedShiftLeft s)^(k + 1)) v).1 i +
(weightedUltrasphericalLowerTerms s k a₀ a v).1 i = _ at h
rw [lp.degreeWeightedShiftLeft_pow_apply] at h
rw [weightedUltrasphericalRemainder, lp.degreeWeightedBorderedRemainder_rows,
ite_eq_right (by omega), show i + k + 1 - (k + 1) = i by omega]
simpa only [Nat.add_assoc, Module.Basis.degreeWeightedCoefficient] using h
Let \(K\) be compact on \(W_s\) and \(T=I+K\) invertible. For all sufficiently large \(n\), the equations \(P_nTx_n=P_nf\), \(P_nx_n=x_n\) have a unique solution. For \(f=Tx\), along the cofinal set of invertible lifted sections, \(x_n\to x\) and, eventually,
theorem lp.degreeWeightedProjection_idempotent (s n : ℕ) :
lp.degreeWeightedProjection s n ∘SL lp.degreeWeightedProjection s n = lp.degreeWeightedProjection s n
Lean proof
/-- Weighted truncation is idempotent. -/
theorem degreeWeightedProjection_idempotent (n : ℕ) :
(degreeWeightedProjection s n).comp (degreeWeightedProjection s n) =
degreeWeightedProjection s n := by
apply ContinuousLinearMap.ext
intro x
apply Subtype.ext
funext i
simp only [comp_apply, degreeWeightedProjection_apply]
split_ifs <;> rfl
theorem lp.degreeWeightedProjection_eq_self_iff (s n : ℕ) (x : lp.DegreeWeightedL2 s) :
(lp.degreeWeightedProjection s n) x = x ↔ ∀ (i : ℕ), n ≤ i → ↑x i = 0
Lean proof
/-- Fixed points of the coordinate projection are exactly the supported vectors. -/
theorem degreeWeightedProjection_eq_self_iff (n : ℕ) (x : DegreeWeightedL2 s) :
degreeWeightedProjection s n x = x ↔ ∀ i, n ≤ i → x.1 i = 0 := by
constructor
· intro h i hi
have he := congrArg (fun v : DegreeWeightedL2 s ↦ v.1 i) h
simpa [degreeWeightedProjection_apply, Nat.not_lt.mpr hi] using he.symm
· intro h
apply Subtype.ext
funext i
by_cases hi : i < n
· simp [hi]
· simp [hi, h i (by omega)]
theorem lp.degreeWeightedProjection_eq_iff (s n : ℕ) (x y : lp.DegreeWeightedL2 s) :
(lp.degreeWeightedProjection s n) x = (lp.degreeWeightedProjection s n) y ↔ ∀ i < n, ↑x i = ↑y i
Lean proof
/-- Projected equations compare exactly the first n coordinates. -/
theorem degreeWeightedProjection_eq_iff (n : ℕ) (x y : DegreeWeightedL2 s) :
degreeWeightedProjection s n x = degreeWeightedProjection s n y ↔ ∀ i < n, x.1 i = y.1 i := by
constructor
· intro h i hi
have he := congrArg (fun v : DegreeWeightedL2 s ↦ v.1 i) h
simpa [hi] using he
· intro h
apply Subtype.ext
funext i
by_cases hi : i < n <;> simp [hi, h]
theorem lp.eventually_existsUnique_degreeWeighted_system (s : ℕ) (K : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s)
(hK : IsCompactOperator ⇑K) (hT : IsUnit (1 + K)) :
∀ᶠ (n : ℕ) in Filter.atTop,
∀ (f : lp.DegreeWeightedL2 s), ∃! x, (∀ (i : ℕ), n ≤ i → ↑x i = 0) ∧ ∀ i < n, ↑((1 + K) x) i = ↑f i
Lean proof
/-- An invertible compact perturbation has unique leading finite coefficient
systems for every sufficiently large size and every right-hand side. -/
theorem eventually_existsUnique_degreeWeighted_system
(K : DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s)
(hK : IsCompactOperator K) (hT : IsUnit (1 + K)) :
∀ᶠ n in atTop, ∀ f : DegreeWeightedL2 s, ∃! x : DegreeWeightedL2 s,
(∀ i, n ≤ i → x.1 i = 0) ∧ (∀ i < n, ((1 + K) x).1 i = f.1 i) := by
filter_upwards [eventually_stable_liftedFiniteSection (degreeWeightedProjection s)
(norm_degreeWeightedProjection_le s) (tendsto_degreeWeightedProjection s) K hK hT] with n hn f
simpa only [degreeWeightedProjection_eq_self_iff, degreeWeightedProjection_eq_iff] using
existsUnique_projected_solution (degreeWeightedProjection s n) K
(degreeWeightedProjection_idempotent s n) hn.1 f
theorem lp.eventually_degreeWeighted_system_error_le (s : ℕ) (K : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s)
(hK : IsCompactOperator ⇑K) (hT : IsUnit (1 + K)) :
∀ᶠ (n : ℕ) in Filter.atTop,
∃ (hn : IsUnit ((lp.degreeWeightedProjection s n).liftedFiniteSection K)),
∀ (x : lp.DegreeWeightedL2 s),
‖(Ring.inverseAt (fun n => (lp.degreeWeightedProjection s n).liftedFiniteSection K) ⟨n, hn⟩)
((lp.degreeWeightedProjection s n) ((1 + K) x)) -
x‖ ≤
(‖↑hT.unit⁻¹‖ + 1) * ‖(lp.degreeWeightedProjection s n) x - x‖
Lean proof
/-- The coefficient error is bounded by a constant times the exact coefficient tail. -/
theorem eventually_degreeWeighted_system_error_le
(K : DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s)
(hK : IsCompactOperator K) (hT : IsUnit (1 + K)) :
∀ᶠ n in atTop, ∃ hn : IsUnit (liftedFiniteSection (degreeWeightedProjection s n) K),
∀ x : DegreeWeightedL2 s,
‖Ring.inverseAt (fun n ↦ liftedFiniteSection (degreeWeightedProjection s n) K) ⟨n, hn⟩
(degreeWeightedProjection s n ((1 + K) x)) - x‖ ≤
(‖(↑(hT.unit⁻¹) : DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s)‖ + 1) *
‖degreeWeightedProjection s n x - x‖ :=
eventually_norm_liftedFiniteSection_error_le (degreeWeightedProjection s)
(norm_degreeWeightedProjection_le s) (tendsto_degreeWeightedProjection s) K hK hT
theorem lp.degreeWeighted_system_filter_neBot (s : ℕ) (K : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s)
(hK : IsCompactOperator ⇑K) (hT : IsUnit (1 + K)) :
(Ring.invertibleIndexFilter (fun n => (lp.degreeWeightedProjection s n).liftedFiniteSection K) Filter.atTop).NeBot
Lean proof
/-- The domain of actual finite solves is cofinal and has a nontrivial limit filter. -/
theorem degreeWeighted_system_filter_neBot
(K : DegreeWeightedL2 s →L[ℂ] DegreeWeightedL2 s)
(hK : IsCompactOperator K) (hT : IsUnit (1 + K)) :
NeBot (Ring.invertibleIndexFilter
(fun n ↦ liftedFiniteSection (degreeWeightedProjection s n) K) atTop) :=
invertible_liftedFiniteSection_filter_neBot (degreeWeightedProjection s)
(norm_degreeWeightedProjection_le s) (tendsto_degreeWeightedProjection s) K hK hT
Let \(\widehat{\mathcal R}_N:W_s\to W_{s+1}\) have the same coordinate formula as \(\mathcal R_N\). For \(x\in [-1,1]\), define \(\mathcal F_N(v)(x)=\sum _{n\ge 0}(\mathcal R_Nv)_nT_n(x)\) using the convergent Chebyshev series.
Lean Formalisation
def Polynomial.Chebyshev.weightedUltrasphericalReconstruction (s k : ℕ) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 (s + 1)
Lean definition
/-- Right preconditioning gains one degree weight. -/
def weightedUltrasphericalReconstruction (s k : ℕ) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 (s + 1) :=
(ultrasphericalDerivativeScale k)⁻¹ •
(lp.degreeWeightedL2Isometry (s + 1)).symm.toContinuousLinearEquiv.toContinuousLinearMap.comp
((lp.coefficientDiagonal degreeGainDiagonal (by norm_num) norm_degreeGainDiagonal_le).comp
(lp.degreeWeightedL2Isometry s).toContinuousLinearEquiv.toContinuousLinearMap)
The map \(\widehat{\mathcal R}_N\) is bounded and has precisely the right-preconditioned coefficients. If \(v_m\to v\) in \(W_s\), then \(\widehat{\mathcal R}_Nv_m\to \widehat{\mathcal R}_Nv\) in \(W_{s+1}\) and \(\mathcal F_N(v_m)\to \mathcal F_N(v)\) uniformly on \([-1,1]\).
Lean Formalisation
theorem Polynomial.Chebyshev.hasSum_weightedUltrasphericalFunction (s k : ℕ) (x : lp.DegreeWeightedL2 s)
(t : ↑(Set.Icc (-1) 1)) :
HasSum
(fun n =>
↑((Polynomial.Chebyshev.weightedUltrasphericalPreconditioner s k) x) n *
Polynomial.eval (↑↑t) (Polynomial.Chebyshev.T ℂ ↑n))
(Polynomial.Chebyshev.weightedUltrasphericalFunction s k x t)
Lean proof
/-- The reconstructed function is the sum of the right-preconditioned Chebyshev series. -/
theorem hasSum_weightedUltrasphericalFunction (s k : ℕ) (x : lp.DegreeWeightedL2 s)
(t : Set.Icc (-1 : ℝ) 1) :
HasSum (fun n ↦ (weightedUltrasphericalPreconditioner s k x).1 n *
(T ℂ n).eval (t.val : ℂ)) (weightedUltrasphericalFunction s k x t) := by
let y := (ultrasphericalDerivativeScale k)⁻¹ • lp.degreeWeightedInclusion s x
have hs := summable_chebyshevSeries_of_absolute
(summable_norm_firstOrderPreconditioner y).1 t
have he (n : ℕ) : firstOrderPreconditioner y n =
(weightedUltrasphericalPreconditioner s k x).1 n := by
rw [firstOrderPreconditioner_apply]
change firstOrderDiagonal n * ((ultrasphericalDerivativeScale k)⁻¹ *
lp.degreeWeightedInclusion s x n) =
(ultrasphericalDerivativeScale k)⁻¹ * (weightedFirstOrderPreconditioner s x).1 n
rw [lp.degreeWeightedInclusion_apply, weightedFirstOrderPreconditioner_apply]
ring
change HasSum _ (complexChebyshevSeries (firstOrderPreconditioner y) (.ofFirstOrder y t))
rw [complexChebyshevSeries_eq_tsum (.ofFirstOrder y t) hs]
simpa only [he, ComplexChebyshevSeriesPoint.ofFirstOrder_val] using hs.hasSum
theorem Polynomial.Chebyshev.weightedUltrasphericalReconstruction_apply (s k : ℕ) (x : lp.DegreeWeightedL2 s) (n : ℕ) :
↑((Polynomial.Chebyshev.weightedUltrasphericalReconstruction s k) x) n =
(Polynomial.Chebyshev.ultrasphericalDerivativeScale k)⁻¹ * Polynomial.Chebyshev.firstOrderDiagonal n * ↑x n
Lean proof
/-- Coordinate formula for the map gaining one degree weight. -/
theorem weightedUltrasphericalReconstruction_apply (s k : ℕ) (x : lp.DegreeWeightedL2 s) (n : ℕ) :
(weightedUltrasphericalReconstruction s k x).1 n =
(ultrasphericalDerivativeScale k)⁻¹ * firstOrderDiagonal n * x.1 n := by
change (ultrasphericalDerivativeScale k)⁻¹ *
(degreeGainDiagonal n * (((n : ℂ) + 1)^s * x.1 n) / ((n : ℂ) + 1)^(s + 1)) = _
simp only [degreeGainDiagonal, pow_succ]
field_simp
theorem Polynomial.Chebyshev.weightedUltrasphericalReconstruction_eq (s k : ℕ) (x : lp.DegreeWeightedL2 s) (n : ℕ) :
↑((Polynomial.Chebyshev.weightedUltrasphericalReconstruction s k) x) n =
↑((Polynomial.Chebyshev.weightedUltrasphericalPreconditioner s k) x) n
Lean proof
/-- The gained-weight reconstruction has the original right-preconditioned coefficients. -/
theorem weightedUltrasphericalReconstruction_eq (s k : ℕ) (x : lp.DegreeWeightedL2 s) (n : ℕ) :
(weightedUltrasphericalReconstruction s k x).1 n =
(weightedUltrasphericalPreconditioner s k x).1 n := by
rw [weightedUltrasphericalReconstruction_apply]
change _ = (ultrasphericalDerivativeScale k)⁻¹ * (weightedFirstOrderPreconditioner s x).1 n
rw [weightedFirstOrderPreconditioner_apply]
ring
theorem Polynomial.Chebyshev.tendstoUniformly_weightedUltrasphericalFunction.{u_1} (s k : ℕ) {ι : Type u_1} {l : Filter ι}
{v : ι → lp.DegreeWeightedL2 s} {x : lp.DegreeWeightedL2 s} (hv : Filter.Tendsto v l (nhds x)) :
TendstoUniformly (fun n => Polynomial.Chebyshev.weightedUltrasphericalFunction s k (v n))
(Polynomial.Chebyshev.weightedUltrasphericalFunction s k x) l
Lean proof
/-- Weighted coefficient convergence gives uniform convergence of reconstructed functions. -/
theorem tendstoUniformly_weightedUltrasphericalFunction (s k : ℕ)
{ι : Type*} {l : Filter ι} {v : ι → lp.DegreeWeightedL2 s}
{x : lp.DegreeWeightedL2 s} (hv : Tendsto v l (𝓝 x)) :
TendstoUniformly (fun n ↦ weightedUltrasphericalFunction s k (v n))
(weightedUltrasphericalFunction s k x) l := by
apply tendstoUniformlyOn_firstOrder_reconstruction
exact (((lp.degreeWeightedInclusion s).continuous.tendsto x).comp hv).const_smul _
For the preceding polynomial differential system, let \(T_n=I+P_nK\). At a cutoff \(n\) for which \(T_n\) is invertible, define \(v_n=T_n^{-1}P_nf\).
Lean Formalisation
def Polynomial.Chebyshev.weightedUltrasphericalFiniteSection (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ) (n : ℕ) :
lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s
Lean definition
/-- The lifted finite section of a preconditioned polynomial differential system. -/
def weightedUltrasphericalFiniteSection (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : ℝ[X]) (a : Fin k → ℝ[X])
(n : ℕ) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s :=
liftedFiniteSection (lp.degreeWeightedProjection s n) (weightedUltrasphericalRemainder s k B a₀ a)
def Polynomial.Chebyshev.weightedUltrasphericalFiniteSolution (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ)
(n : Ring.InvertibleIndex (Polynomial.Chebyshev.weightedUltrasphericalFiniteSection s k B a₀ a))
(f : lp.DegreeWeightedL2 s) : lp.DegreeWeightedL2 s
Lean definition
/-- The finite solution at a certified invertible cutoff. -/
def weightedUltrasphericalFiniteSolution (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : ℝ[X]) (a : Fin k → ℝ[X])
(n : Ring.InvertibleIndex (weightedUltrasphericalFiniteSection s k B a₀ a))
(f : lp.DegreeWeightedL2 s) : lp.DegreeWeightedL2 s :=
Ring.inverseAt (weightedUltrasphericalFiniteSection s k B a₀ a) n
(lp.degreeWeightedProjection s n.val f)
Let \(s\in \mathbb N\), \(N\ge 1\), and let \(T\) be the preconditioned polynomial differential system above, with bounded boundary rows on \(W_s\). Assume \(T\) is invertible. For all sufficiently large cutoffs the finite systems are uniquely solvable. For \(f=Tv\), their solutions satisfy
Thus \(v_n\to v\) in \(W_s\), \(u_n\to u\) in \(W_{s+1}\), and the reconstructed functions converge uniformly on \([-1,1]\). All limits are through the cofinal set of invertible cutoffs.
theorem Polynomial.Chebyshev.eventually_existsUnique_weightedUltraspherical_system (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ)
(hT : IsUnit (1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a)) :
∀ᶠ (n : ℕ) in Filter.atTop,
∀ (f : lp.DegreeWeightedL2 s),
∃! x,
(∀ (i : ℕ), n ≤ i → ↑x i = 0) ∧
∀ i < n, ↑((1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a) x) i = ↑f i
Lean proof
/-- Invertibility of the infinite system gives unique sufficiently large finite solves. -/
theorem eventually_existsUnique_weightedUltraspherical_system (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : ℝ[X]) (a : Fin k → ℝ[X])
(hT : IsUnit (1 + weightedUltrasphericalRemainder s k B a₀ a)) :
∀ᶠ n in atTop, ∀ f : lp.DegreeWeightedL2 s, ∃! x : lp.DegreeWeightedL2 s,
(∀ i, n ≤ i → x.1 i = 0) ∧
(∀ i < n, ((1 + weightedUltrasphericalRemainder s k B a₀ a) x).1 i = f.1 i) :=
lp.eventually_existsUnique_degreeWeighted_system s _
(isCompactOperator_weightedUltrasphericalRemainder s k B a₀ a) hT
theorem Polynomial.Chebyshev.tendsto_weightedUltraspherical_system_solution (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ)
(hT : IsUnit (1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a)) (x : lp.DegreeWeightedL2 s) :
Filter.Tendsto
(fun n =>
(Ring.inverseAt
(fun n =>
(lp.degreeWeightedProjection s n).liftedFiniteSection
(Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a))
n)
((lp.degreeWeightedProjection s ↑n) ((1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a) x)))
(Ring.invertibleIndexFilter
(fun n =>
(lp.degreeWeightedProjection s n).liftedFiniteSection
(Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a))
Filter.atTop)
(nhds x)
Lean proof
/-- Finite solves converge in the weighted preconditioned coefficient norm. -/
theorem tendsto_weightedUltraspherical_system_solution (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : ℝ[X]) (a : Fin k → ℝ[X])
(hT : IsUnit (1 + weightedUltrasphericalRemainder s k B a₀ a)) (x : lp.DegreeWeightedL2 s) :
Tendsto (fun n : Ring.InvertibleIndex
(fun n ↦ liftedFiniteSection (lp.degreeWeightedProjection s n)
(weightedUltrasphericalRemainder s k B a₀ a)) ↦
Ring.inverseAt (fun n ↦ liftedFiniteSection (lp.degreeWeightedProjection s n)
(weightedUltrasphericalRemainder s k B a₀ a)) n
(lp.degreeWeightedProjection s n ((1 + weightedUltrasphericalRemainder s k B a₀ a) x)))
(Ring.invertibleIndexFilter (fun n ↦ liftedFiniteSection (lp.degreeWeightedProjection s n)
(weightedUltrasphericalRemainder s k B a₀ a)) atTop) (𝓝 x) :=
lp.tendsto_degreeWeighted_system_solution s _
(isCompactOperator_weightedUltrasphericalRemainder s k B a₀ a) hT x
theorem Polynomial.Chebyshev.weightedUltraspherical_filter_neBot (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ)
(hT : IsUnit (1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a)) :
(Ring.invertibleIndexFilter (Polynomial.Chebyshev.weightedUltrasphericalFiniteSection s k B a₀ a) Filter.atTop).NeBot
Lean proof
/-- Invertible cutoffs form a nontrivial cofinal limiting domain. -/
theorem weightedUltraspherical_filter_neBot (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : ℝ[X]) (a : Fin k → ℝ[X])
(hT : IsUnit (1 + weightedUltrasphericalRemainder s k B a₀ a)) :
NeBot (Ring.invertibleIndexFilter (weightedUltrasphericalFiniteSection s k B a₀ a) atTop) :=
lp.degreeWeighted_system_filter_neBot s _
(isCompactOperator_weightedUltrasphericalRemainder s k B a₀ a) hT
theorem Polynomial.Chebyshev.eventually_weightedUltraspherical_error_le (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ)
(hT : IsUnit (1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a)) :
∀ᶠ (n : ℕ) in Filter.atTop,
∃ (hn : IsUnit (Polynomial.Chebyshev.weightedUltrasphericalFiniteSection s k B a₀ a n)),
∀ (x : lp.DegreeWeightedL2 s),
‖Polynomial.Chebyshev.weightedUltrasphericalFiniteSolution s k B a₀ a ⟨n, hn⟩
((1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a) x) -
x‖ ≤
(‖↑hT.unit⁻¹‖ + 1) * ‖(lp.degreeWeightedProjection s n) x - x‖
Lean proof
/-- The preconditioned coefficient error is controlled by its exact weighted tail. -/
theorem eventually_weightedUltraspherical_error_le (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : ℝ[X]) (a : Fin k → ℝ[X])
(hT : IsUnit (1 + weightedUltrasphericalRemainder s k B a₀ a)) :
∀ᶠ n in atTop, ∃ hn : IsUnit (weightedUltrasphericalFiniteSection s k B a₀ a n),
∀ x : lp.DegreeWeightedL2 s,
‖weightedUltrasphericalFiniteSolution s k B a₀ a ⟨n, hn⟩
((1 + weightedUltrasphericalRemainder s k B a₀ a) x) - x‖ ≤
(‖(↑(hT.unit⁻¹) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s)‖ + 1) *
‖lp.degreeWeightedProjection s n x - x‖ :=
lp.eventually_degreeWeighted_system_error_le s _
(isCompactOperator_weightedUltrasphericalRemainder s k B a₀ a) hT
theorem Polynomial.Chebyshev.eventually_weightedUltraspherical_reconstruction_error_le (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ)
(hT : IsUnit (1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a)) :
∀ᶠ (n : ℕ) in Filter.atTop,
∃ (hn : IsUnit (Polynomial.Chebyshev.weightedUltrasphericalFiniteSection s k B a₀ a n)),
∀ (x : lp.DegreeWeightedL2 s),
‖(Polynomial.Chebyshev.weightedUltrasphericalReconstruction s k)
(Polynomial.Chebyshev.weightedUltrasphericalFiniteSolution s k B a₀ a ⟨n, hn⟩
((1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a) x)) -
(Polynomial.Chebyshev.weightedUltrasphericalReconstruction s k) x‖ ≤
‖Polynomial.Chebyshev.weightedUltrasphericalReconstruction s k‖ * (‖↑hT.unit⁻¹‖ + 1) *
‖(lp.degreeWeightedProjection s n) x - x‖
Lean proof
/-- The original coefficient error in the stronger norm is controlled by the preconditioned tail. -/
theorem eventually_weightedUltraspherical_reconstruction_error_le (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : ℝ[X]) (a : Fin k → ℝ[X])
(hT : IsUnit (1 + weightedUltrasphericalRemainder s k B a₀ a)) :
∀ᶠ n in atTop, ∃ hn : IsUnit (weightedUltrasphericalFiniteSection s k B a₀ a n),
∀ x : lp.DegreeWeightedL2 s,
‖weightedUltrasphericalReconstruction s k
(weightedUltrasphericalFiniteSolution s k B a₀ a ⟨n, hn⟩
((1 + weightedUltrasphericalRemainder s k B a₀ a) x)) -
weightedUltrasphericalReconstruction s k x‖ ≤
(‖weightedUltrasphericalReconstruction s k‖ *
(‖(↑(hT.unit⁻¹) : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s)‖ + 1)) *
‖lp.degreeWeightedProjection s n x - x‖ := by
filter_upwards [eventually_weightedUltraspherical_error_le s k B a₀ a hT] with n hn
obtain ⟨hn, herr⟩ := hn
refine ⟨hn, fun x ↦ ?_⟩
rw [← map_sub]
exact ((weightedUltrasphericalReconstruction s k).le_opNorm _).trans
(by simpa only [mul_assoc] using
mul_le_mul_of_nonneg_left (herr x) (norm_nonneg (weightedUltrasphericalReconstruction s k)))
theorem Polynomial.Chebyshev.tendsto_weightedUltraspherical_reconstruction (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ)
(hT : IsUnit (1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a)) (x : lp.DegreeWeightedL2 s) :
Filter.Tendsto
(fun n =>
(Polynomial.Chebyshev.weightedUltrasphericalReconstruction s k)
(Polynomial.Chebyshev.weightedUltrasphericalFiniteSolution s k B a₀ a n
((1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a) x)))
(Ring.invertibleIndexFilter (Polynomial.Chebyshev.weightedUltrasphericalFiniteSection s k B a₀ a) Filter.atTop)
(nhds ((Polynomial.Chebyshev.weightedUltrasphericalReconstruction s k) x))
Lean proof
/-- The original solution coefficients converge with one additional degree weight. -/
theorem tendsto_weightedUltraspherical_reconstruction (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : ℝ[X]) (a : Fin k → ℝ[X])
(hT : IsUnit (1 + weightedUltrasphericalRemainder s k B a₀ a)) (x : lp.DegreeWeightedL2 s) :
Tendsto (fun n ↦ weightedUltrasphericalReconstruction s k
(weightedUltrasphericalFiniteSolution s k B a₀ a n
((1 + weightedUltrasphericalRemainder s k B a₀ a) x)))
(Ring.invertibleIndexFilter (weightedUltrasphericalFiniteSection s k B a₀ a) atTop)
(𝓝 (weightedUltrasphericalReconstruction s k x)) :=
((weightedUltrasphericalReconstruction s k).continuous.tendsto x).comp
(tendsto_weightedUltraspherical_system_solution s k B a₀ a hT x)
theorem Polynomial.Chebyshev.tendstoUniformly_weightedUltraspherical_solution (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : Polynomial ℝ) (a : Fin k → Polynomial ℝ)
(hT : IsUnit (1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a)) (x : lp.DegreeWeightedL2 s) :
TendstoUniformly
(fun n =>
Polynomial.Chebyshev.weightedUltrasphericalFunction s k
(Polynomial.Chebyshev.weightedUltrasphericalFiniteSolution s k B a₀ a n
((1 + Polynomial.Chebyshev.weightedUltrasphericalRemainder s k B a₀ a) x)))
(Polynomial.Chebyshev.weightedUltrasphericalFunction s k x)
(Ring.invertibleIndexFilter (Polynomial.Chebyshev.weightedUltrasphericalFiniteSection s k B a₀ a) Filter.atTop)
Lean proof
/-- The represented finite solutions converge uniformly on the closed interval. -/
theorem tendstoUniformly_weightedUltraspherical_solution (s k : ℕ)
(B : lp.DegreeWeightedL2 s →L[ℂ] lp.DegreeWeightedL2 s) (a₀ : ℝ[X]) (a : Fin k → ℝ[X])
(hT : IsUnit (1 + weightedUltrasphericalRemainder s k B a₀ a)) (x : lp.DegreeWeightedL2 s) :
TendstoUniformly (fun n ↦ weightedUltrasphericalFunction s k
(weightedUltrasphericalFiniteSolution s k B a₀ a n
((1 + weightedUltrasphericalRemainder s k B a₀ a) x)))
(weightedUltrasphericalFunction s k x)
(Ring.invertibleIndexFilter (weightedUltrasphericalFiniteSection s k B a₀ a) atTop) :=
tendstoUniformly_weightedUltrasphericalFunction s k
(tendsto_weightedUltraspherical_system_solution s k B a₀ a hT x)