6.3 Toeplitz operators and finite sections
The first-kind Volterra analysis uses the Toeplitz and finite-section results collected here. Convergence requires stability in addition to a formula for the matrix; the theorems state the needed assumptions.
Reference details: Unilateral shifts on real and complex \(\ell ^2\)
For \(\mathbb K=\mathbb R\) or \(\mathbb C\), the forward shift \(S\) on \(\ell ^2(\mathbb N;\mathbb K)\) is an isometry with \((Su)_0=0\) and \((Su)_{n+1}=u_n\). Its adjoint \(B=S^*\) satisfies \((Bu)_n=u_{n+1}\), \(BS=I\) and \(SB=I-P_1\), where \(P_1\) projects onto coordinate zero. In particular \(Se_n=e_{n+1}\). Reference: Böttcher–Silbermann, Introduction to Large Truncated Toeplitz Matrices, Chapter 1.
Lean Formalisation
theorem lp.norm_sq_eq_tsum_sq.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (u : ↥(lp (fun x => 𝕜) 2)) : ‖u‖ ^ 2 = ∑' (n : ℕ), ‖↑u n‖ ^ 2Lean proof
/-- The square of an ℓ² norm is the sum of the squared coordinate norms. -/
theorem norm_sq_eq_tsum_sq (u : lp (fun _ : ℕ ↦ 𝕜) 2) :
‖u‖^2 = ∑' n, ‖u n‖^2 := by
simpa using lp.norm_rpow_eq_tsum (by norm_num : 0 < (2 : ℝ≥0∞).toReal) uThe construction uses square summability and \(\| u\| ^2=\sum _n\| u_n\| ^2\).
A bounded operator \(T\) on real or complex \(\ell ^2\) is called Toeplitz when \((Te_{j+1})_{i+1}=(Te_j)_i\) for all \(i,j\ge 0\). This is equivalent to \(S^*TS=T\). These operators form a closed linear subspace, preserved by Hilbert adjoints, containing \(I\), \(S\), \(S^*\) and every nonnegative power of either shift. Bounded operators are determined by their coordinate columns. No finite-band or polynomial-symbol assumption is imposed in this definition.
Lean Formalisation
theorem lp.continuousLinearMap_ext_single.{u_1} {𝕜 : Type u_1} [RCLike 𝕜]
{T U : ↥(lp (fun x => 𝕜) 2) →L[𝕜] ↥(lp (fun x => 𝕜) 2)} (h : ∀ (n : ℕ), T (lp.single 2 n 1) = U (lp.single 2 n 1)) :
T = ULean proof
/-- A bounded operator on ℓ² is determined by its coordinate columns. -/
theorem continuousLinearMap_ext_single {T U : H →L[𝕜] H}
(h : ∀ n, T (lp.single 2 n 1) = U (lp.single 2 n 1)) : T = U := by
have hs (n : ℕ) (a : 𝕜) : T (lp.single 2 n a) = U (lp.single 2 n a) := by
have he : lp.single 2 n a = a • (lp.single 2 n (1 : 𝕜) : H) := by
rw [← lp.single_smul]
simp
rw [he, map_smul, map_smul, h]
apply ContinuousLinearMap.ext
intro u
have he (N : ℕ) : T (initialL2Projection N u) = U (initialL2Projection N u) := by
simp only [initialL2Projection_apply, map_sum, hs]
have ht := (T.continuous.tendsto u).comp (tendsto_initialL2Projection u)
have hu := (U.continuous.tendsto u).comp (tendsto_initialL2Projection u)
exact tendsto_nhds_unique ht (by simpa only [Function.comp_def, he] using hu)Put \(V_k=S^k\) for \(k\ge 0\), and \(V_k=(S^*)^{-k}\) for \(k{\lt}0\). For a Laurent polynomial \(p(z)=\sum _k a_kz^k\) over \(\mathbb R\) or \(\mathbb C\), define \(T_p=\sum _k a_kV_k\). This map is linear, \(T_{az^k}=aV_k\), and \(T_p\) is bounded and Toeplitz, with
The basic product defect is \(V_1V_{-1}=I-P_1\); hence \(I-V_1V_{-1}\) is compact.
Lean Formalisation
theorem lp.isToeplitz_laurentShiftL2.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (k : ℤ) : lp.IsToeplitz (lp.laurentShiftL2 k)Lean proof
/-- Every signed shift has constant matrix diagonals. -/
theorem isToeplitz_laurentShiftL2 (k : ℤ) :
IsToeplitz (laurentShiftL2 (𝕜 := 𝕜) k) := by
cases k with
| ofNat n => exact isToeplitz_forwardShiftL2_pow n
| negSucc n => exact isToeplitz_backwardShiftL2_pow (n+1)This does not assert multiplicativity of the symbol map or a general finite-section stability theorem.
For real or complex Laurent polynomials \(p,q\), \(T_pT_q-T_{pq}\) has finite-dimensional range and is compact. More precisely, its output is supported on finitely many initial coordinates. For individual shifts \(V_k,V_l\), all coordinates \(i\ge |k|+|l|\) vanish. The finite-coordinate-range operators form a linear subspace; an initial coordinate projection fixes every such operator.
Lean Formalisation
theorem lp.forwardShiftL2_pow_apply.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (n : ℕ) (u : ↥(lp (fun x => 𝕜) 2)) (i : ℕ) (h : n ≤ i) :
↑((lp.forwardShiftL2.toContinuousLinearMap ^ n) u) i = ↑u (i - n)Lean proof
/-- Forward shift powers act by translation above the boundary. -/
theorem forwardShiftL2_pow_apply (n : ℕ) (u : H) (i : ℕ) (h : n ≤ i) :
(forwardShiftL2.toContinuousLinearMap ^ n) u i = u (i-n) := by
induction n generalizing i with
| zero => simp
| succ n ih =>
obtain ⟨j, rfl⟩ := Nat.exists_eq_succ_of_ne_zero (by omega : i ≠ 0)
rw [pow_succ']
change forwardShiftL2 ((forwardShiftL2.toContinuousLinearMap ^ n) u) (j+1) = _
rw [forwardShiftL2_succ, ih j (by omega)]
exact congrArg (fun j : ℕ ↦ u j) (by omega)On a circle of period \(T{\gt}0\) with normalized Haar measure, let \(E\) synthesize the nonnegative orthonormal Fourier modes into complex \(L^2\). For a continuous complex symbol \(f\), multiplication \(M_f\) is bounded and \(T_f=E^*M_fE\) satisfies \(\| T_f\| \le \| f\| _\infty \) and \((T_f)_{ij}=\widehat f(i-j)\). This defines a bounded linear map from continuous symbols to Toeplitz operators; uniform convergence of symbols implies operator-norm convergence.
Lean Formalisation
theorem AddCircle.orthonormal_nonnegativeFourier {T : ℝ} [Fact (0 < T)] : Orthonormal ℂ fun n => fourierLp 2 ↑nLean proof
/-- The nonnegative Fourier modes are an orthonormal family. -/
theorem orthonormal_nonnegativeFourier :
Orthonormal ℂ (fun n : ℕ ↦ (fourierLp (T := T) 2 (n : ℤ))) :=
orthonormal_fourier.comp (fun n : ℕ ↦ (n : ℤ)) (by intro m n h; change (m : ℤ) = (n : ℤ) at h; omega)Reference details: Laurent symbols on a circle and related results
Let \(T\in \mathbb R\setminus \{ 0\} \) and let \(\mathbb R/T\mathbb Z\) be the circle with signed period \(T\). For a Laurent polynomial \(p=\sum _{k\in \mathbb Z}p_kz^k\) with finite support, its continuous circle symbol is
This defines a complex-linear map from Laurent polynomials over \(\mathbb C\) to continuous complex-valued functions on the circle.
Lean Formalisation
def AddCircle.laurentSymbol {T : { T // T ≠ 0 }} : LaurentPolynomial ℂ →ₗ[ℂ] C(AddCircle ↑T, ℂ)Lean definition
/-- Realization of a Laurent polynomial on a circle with nonzero signed period. -/
def laurentSymbol {T : {T : ℝ // T ≠ 0}} : LaurentPolynomial ℂ →ₗ[ℂ] C(AddCircle (T : ℝ), ℂ) where
toFun p := Finsupp.linearCombination ℂ fourier p.coeff
map_add' p q := by simp
map_smul' a p := by simpFor every nonzero signed period \(T\), \(\mathcal L_T(az^k)(x)=a\exp (2\pi i kx/T)\), \(\mathcal L_T(pq)=\mathcal L_T(p)\mathcal L_T(q)\), \(\mathcal L_T(1)=1\), and \(\mathcal L_T(p^n)=\mathcal L_T(p)^n\) for every \(n\ge 0\).
Lean Formalisation
theorem AddCircle.laurentSymbol_single {T : { T // T ≠ 0 }} (k : ℤ) (a : ℂ) :
AddCircle.laurentSymbol (AddMonoidAlgebra.single k a) = a • fourier kLean proof
/-- A Laurent monomial realizes as the corresponding Fourier monomial. -/
theorem laurentSymbol_single {T : {T : ℝ // T ≠ 0}} (k : ℤ) (a : ℂ) :
laurentSymbol (T := T) (AddMonoidAlgebra.single k a) = a • fourier k := by
change Finsupp.linearCombination ℂ fourier (Finsupp.single k a) = _
simpFor \(T{\gt}0\), Laurent symbols are dense in the continuous complex-valued functions on the circle, and their Fourier compression agrees with Laurent quantization. Consequently \(T_fT_g-T_{fg}\) is compact for every pair of continuous symbols. If \(A-T_f\) and \(B-T_g\) are compact, so are \(A+B-T_{f+g}\), \(AB-T_{fg}\), and \(A^n-T_{f^n}\). The constant-one symbol gives the identity.
Lean Formalisation
theorem AddCircle.continuousToeplitz_fourier {T : ℝ} [Fact (0 < T)] (k : ℤ) :
AddCircle.continuousToeplitz (fourier k) = lp.laurentShiftL2 kLean proof
/-- Fourier monomial compression is precisely the signed shift. -/
theorem continuousToeplitz_fourier (k : ℤ) :
continuousToeplitz (fourier (T := T) k) = lp.laurentShiftL2 k := by
apply lp.continuousLinearMap_ext_single
intro j
apply lp.ext
funext i
rw [continuousToeplitz_entry, lp.laurentShiftL2_single_entry, fourierCoeff_fourier]
simp only [Pi.single_apply, eq_comm]Reference details: Stability under compact perturbations and related results
Let \(A_n\) and \(B\) be invertible bounded operators on a real or complex Banach space, with \(A_n\to B\) strongly and \(\sup _n\| A_n^{-1}\| \le C\). Then \(A_n^{-1}\to B^{-1}\) strongly. Uniformly bounded strong convergence becomes norm convergence after a compact right factor, including norm-convergent right factors with compact limit. If \(K_n\to K\) in norm, \(K\) is compact, and \(B+K\) is invertible, then \(A_n+K_n\) are eventually invertible with uniformly bounded inverses. For \(f_n\to f\), \((A_n+K_n)^{-1}f_n\to (B+K)^{-1}f\). An eventual inverse bound is \((\| (I+B^{-1}K)^{-1}\| +1)C\).
Lean Formalisation
theorem ContinuousLinearMap.tendsto_apply_of_strongly_tendsto_of_tendsto.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2}
[NormedAddCommGroup E] [NormedSpace 𝕜 E] (A : ℕ → E →L[𝕜] E) (B : E →L[𝕜] E) {C : ℝ} (hC : ∀ (n : ℕ), ‖A n‖ ≤ C)
(ht : ∀ (x : E), Filter.Tendsto (fun n => (A n) x) Filter.atTop (nhds (B x))) {x : ℕ → E} {y : E}
(hx : Filter.Tendsto x Filter.atTop (nhds y)) : Filter.Tendsto (fun n => (A n) (x n)) Filter.atTop (nhds (B y))Lean proof
/-- Uniformly bounded strong convergence also allows a convergent input sequence. -/
theorem tendsto_apply_of_strongly_tendsto_of_tendsto
(A : ℕ → E →L[𝕜] E) (B : E →L[𝕜] E) {C : ℝ}
(hC : ∀ n, ‖A n‖ ≤ C)
(ht : ∀ x, Tendsto (fun n ↦ A n x) atTop (𝓝 (B x)))
{x : ℕ → E} {y : E} (hx : Tendsto x atTop (𝓝 y)) :
Tendsto (fun n ↦ A n (x n)) atTop (𝓝 (B y)) := by
rw [tendsto_iff_norm_sub_tendsto_zero]
refine squeeze_zero (fun _ ↦ norm_nonneg _)
(fun n ↦ show ‖A n (x n)-B y‖ ≤ C*‖x n-y‖+‖A n y-B y‖ from ?_) ?_
· have he : A n (x n)-B y = A n (x n-y)+(A n y-B y) := by
rw [map_sub]
abel
rw [he]
exact (norm_add_le _ _).trans (add_le_add
((A n).le_opNorm _ |>.trans (mul_le_mul_of_nonneg_right (hC n) (norm_nonneg _))) le_rfl)
· simpa using ((hx.sub (tendsto_const_nhds (x := y))).norm.const_mul C).add
((ht y).sub (tendsto_const_nhds (x := B y))).normOn a real or complex Hilbert space, define \(A_P=I-P+PAP\) for a self-adjoint projection \(P\). Its quadratic form splits into \(\| u-Pu\| ^2+\langle Pu,APu\rangle \). If \(0{\lt}a\le 1\) and \(\operatorname {Re}\langle u,Au\rangle \ge a\| u\| ^2\), then every \(A_P\) is invertible and \(\| A_P^{-1}\| \le a^{-1}\). A positive coercivity bound also makes \(A\) itself invertible, with the same inverse bound.
Lean Formalisation
theorem ContinuousLinearMap.inner_coerciveFiniteSection.{u_1, u_2} {𝕜 : Type u_1} [RCLike 𝕜] {E : Type u_2}
[NormedAddCommGroup E] [InnerProductSpace 𝕜 E] [CompleteSpace E] (P A : E →L[𝕜] E)
(hP : ContinuousLinearMap.adjoint P = P) (hPP : P ∘SL P = P) (u : E) :
inner 𝕜 u ((P.coerciveFiniteSection A) u) = ↑(‖u - P u‖ ^ 2) + inner 𝕜 (P u) (A (P u))Lean proof
/-- The compressed quadratic form splits into a complement norm and a resolved form. -/
theorem inner_coerciveFiniteSection (P A : E →L[𝕜] E)
(hP : P.adjoint = P) (hPP : P.comp P = P) (u : E) :
⟪u, coerciveFiniteSection P A u⟫_𝕜 =
(‖u-P u‖^2 : ℝ) + ⟪P u, A (P u)⟫_𝕜 := by
have hid : P (P u) = P u := congrArg (fun B : E →L[𝕜] E ↦ B u) hPP
have hs (v w : E) : ⟪v, P w⟫_𝕜 = ⟪P v, w⟫_𝕜 := by
simpa only [hP] using adjoint_inner_right P v w
have hz : ⟪P u, u-P u⟫_𝕜 = 0 := by
rw [← hs, map_sub, hid, sub_self, inner_zero_right]
have he : ⟪u, u-P u⟫_𝕜 = (‖u-P u‖^2 : ℝ) := by
calc
_ = ⟪u-P u+P u, u-P u⟫_𝕜 := by rw [sub_add_cancel]
_ = _ := by rw [inner_add_left, hz, add_zero, inner_self_eq_norm_sq_to_K]; simp
change ⟪u, u-P u+P (A (P u))⟫_𝕜 = _
rw [inner_add_right, he, hs]For initial-coordinate projections \(P_N\) on \(\ell ^2\), the sections \(I-P_N+P_NAP_N\) converge strongly to \(A\). Suppose \(A\) has coercivity constant \(0{\lt}a\le 1\), \(K\) is compact, and \(A+K\) is invertible. Then the sections of \(A+K\) are eventually invertible, their inverses are uniformly bounded, and their solutions for right-hand sides \(P_Nf\) converge to \((A+K)^{-1}f\). Invertibility of a section gives a unique solution of \(P_Nu=u\), \(P_N(A+K)u=P_Nf\).
Lean Formalisation
theorem lp.tendsto_coerciveFiniteSection.{u_1} {𝕜 : Type u_1} [RCLike 𝕜] (A : ↥(lp (fun x => 𝕜) 2) →L[𝕜] ↥(lp (fun x => 𝕜) 2))
(u : ↥(lp (fun x => 𝕜) 2)) :
Filter.Tendsto (fun N => ((lp.initialL2Projection N).coerciveFiniteSection A) u) Filter.atTop (nhds (A u))Lean proof
/-- Orthogonal coordinate sections converge strongly to their bounded operator. -/
theorem tendsto_coerciveFiniteSection (A : H →L[𝕜] H) (u : H) :
Tendsto (fun N ↦ coerciveFiniteSection (initialL2Projection N) A u)
atTop (𝓝 (A u)) := by
have ht := tendsto_apply_of_strongly_tendsto_of_tendsto
(fun N ↦ initialL2Projection (𝕜 := 𝕜) N) 1 norm_initialL2Projection_le
tendsto_initialL2Projection ((A.continuous.tendsto u).comp (tendsto_initialL2Projection u))
change Tendsto (fun N ↦ u-initialL2Projection N u+
initialL2Projection N (A (initialL2Projection N u))) atTop (𝓝 (A u))
simpa only [Function.comp_def, one_apply_eq_self, sub_self, zero_add] using
((tendsto_const_nhds (x := u)).sub (tendsto_initialL2Projection u)).add htIf \(\operatorname {Re}f\ge a\) pointwise, the multiplier and its Toeplitz compression have quadratic forms bounded below by \(a\| u\| ^2\). For \(a{\gt}0\), \(T_f\) is invertible.
Lean Formalisation
theorem AddCircle.re_inner_continuousSymbolMultiplier_le {T : ℝ} [Fact (0 < T)] (f : C(AddCircle T, ℂ)) {a : ℝ}
(hf : ∀ (x : AddCircle T), a ≤ (f x).re) (u : ↥(MeasureTheory.Lp ℂ 2 AddCircle.haarAddCircle)) :
a * ‖u‖ ^ 2 ≤ (inner ℂ u ((AddCircle.continuousSymbolMultiplier f) u)).reLean proof
/-- A lower bound on the real part of a multiplier gives the same quadratic-form bound. -/
theorem re_inner_continuousSymbolMultiplier_le (f : C(AddCircle T, ℂ)) {a : ℝ}
(hf : ∀ x, a ≤ (f x).re) (u : L) :
a*‖u‖^2 ≤ (⟪u, continuousSymbolMultiplier f u⟫_ℂ).re := by
have hsq : Integrable (fun x ↦ ‖u x‖^2) haarAddCircle := by
simpa only [inner_self_eq_norm_sq_to_K, ← RCLike.ofReal_pow, RCLike.ofReal_re] using
(L2.integrable_inner (𝕜 := ℂ) u u).re
have he : ‖u‖^2 = ∫ x, ‖u x‖^2 ∂haarAddCircle := by
have hh := congrArg (RCLike.re (K := ℂ)) (L2.inner_def u u (𝕜 := ℂ))
rw [← integral_re (L2.integrable_inner (𝕜 := ℂ) u u)] at hh
simpa only [inner_self_eq_norm_sq_to_K, ← RCLike.ofReal_pow, RCLike.ofReal_re] using hh
change a*‖u‖^2 ≤ RCLike.re (⟪u, continuousSymbolMultiplier f u⟫_ℂ)
rw [he, ← integral_const_mul, L2.inner_def,
← integral_re (L2.integrable_inner (𝕜 := ℂ) u (continuousSymbolMultiplier f u))]
apply integral_mono_ae (hsq.const_mul a)
(L2.integrable_inner (𝕜 := ℂ) u (continuousSymbolMultiplier f u)).re
filter_upwards [continuousSymbolMultiplier_ae f u] with x hx
rw [hx]
change a*‖u x‖^2 ≤ (⟪u x, (f x) • u x⟫_ℂ).re
rw [inner_smul_right, inner_self_eq_norm_sq_to_K]
rw [← RCLike.ofReal_pow]
change a*‖u x‖^2 ≤ (f x * (↑(‖u x‖^2) : ℂ)).re
simp only [Complex.mul_re, Complex.ofReal_re, Complex.ofReal_im, mul_zero, sub_zero]
exact mul_le_mul_of_nonneg_right (hf x) (sq_nonneg ‖u x‖)Suppose \(f\) is continuous with \(\operatorname {Re}f\ge a{\gt}0\), \(K\) is compact, and \(T_f+K\) is invertible. Its initial-coordinate sections are eventually invertible and their inverse norms are eventually bounded by \((\| (I+T_f^{-1}K)^{-1}\| +1)/\min (a,1)\). The uniquely solvable projected equations converge in \(\ell ^2\) to the exact solution for every right-hand side. Invertibility of the full perturbed operator is an explicit hypothesis here; equivalently, it suffices to prove injectivity using the compact-perturbation criterion.
Lean Formalisation
theorem AddCircle.isUnit_continuousToeplitz_add_of_injective {T : ℝ} [Fact (0 < T)] (f : C(AddCircle T, ℂ))
(K : ↥(lp (fun x => ℂ) 2) →L[ℂ] ↥(lp (fun x => ℂ) 2)) {a : ℝ} (ha : 0 < a) (hf : ∀ (x : AddCircle T), a ≤ (f x).re)
(hK : IsCompactOperator ⇑K) (hinj : Function.Injective ⇑(AddCircle.continuousToeplitz f + K)) :
IsUnit (AddCircle.continuousToeplitz f + K)Lean proof
/-- Injectivity is the remaining obligation for a compact perturbation of a positive symbol. -/
theorem isUnit_continuousToeplitz_add_of_injective (f : C(AddCircle T, ℂ))
(K : H →L[ℂ] H) {a : ℝ} (ha : 0 < a) (hf : ∀ x, a ≤ (f x).re)
(hK : IsCompactOperator K) (hinj : Function.Injective (continuousToeplitz f+K)) :
IsUnit (continuousToeplitz f+K) :=
isUnit_add_of_injective_of_compact _ K
(isUnit_continuousToeplitz_of_re_pos f ha hf) hK hinjReference details: Real Laurent operators and complex symbols and related results
Coefficientwise complexification is a real-linear isometry, intertwines both unilateral shifts and every real Laurent operator, and preserves the real part of the inner product. Thus a lower bound \(\operatorname {Re}p\ge a\) on the complex circle symbol gives \(\langle u,T_pu\rangle _{\mathbb R}\ge a\| u\| ^2\) on real \(\ell ^2\).
Lean Formalisation
theorem lp.complexifyL2_apply (u : ↥(lp (fun x => ℝ) 2)) (n : ℕ) : ↑(lp.complexifyL2 u) n = ↑(↑u n)Lean proof
/-- Complexification acts coefficientwise. -/
@[simp] theorem complexifyL2_apply (u : lp (fun _ : ℕ ↦ ℝ) 2) (n : ℕ) :
complexifyL2 u n = (u n : ℂ) := rflOn a Banach space over a nontrivially normed field, an injective operator \(I+K\) with \(K\) compact is invertible. More generally, if \(A\) is invertible and \(K\) is compact, injectivity of \(A+K\) implies invertibility.
Lean Formalisation
theorem ContinuousLinearMap.isUnit_one_add_of_injective_of_compact.{u_1, u_2} {𝕜 : Type u_1} [NontriviallyNormedField 𝕜]
{E : Type u_2} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [CompleteSpace E] (K : E →L[𝕜] E) (hK : IsCompactOperator ⇑K)
(hinj : Function.Injective ⇑(1 + K)) : IsUnit (1 + K)Lean proof
/-- An injective identity-plus-compact operator is invertible. -/
theorem isUnit_one_add_of_injective_of_compact (K : E →L[𝕜] E)
(hK : IsCompactOperator K) (hinj : Function.Injective (1+K : E →L[𝕜] E)) :
IsUnit (1+K) := by
have hn : IsCompactOperator (-K : E →L[𝕜] E) := hK.neg
rcases hn.hasEigenvalue_or_mem_resolventSet (μ := (1 : 𝕜)) one_ne_zero with he | hr
· obtain ⟨u, hu⟩ := he.exists_hasEigenvector
have heq : -K u = u := by
have h := hu.apply_eq_smul
change -K u = (1 : 𝕜) • u at h
simpa only [one_smul] using h
have hz : (1+K : E →L[𝕜] E) u = (1+K : E →L[𝕜] E) 0 := by
simp only [add_apply, one_apply_eq_self, map_zero]
calc
u + K u = -K u + K u := congrArg (fun v ↦ v + K u) heq.symm
_ = 0 := neg_add_cancel _
exact (hu.2 (hinj hz)).elim
· rw [spectrum.mem_resolventSet_iff] at hr
simpa only [map_one, sub_neg_eq_add] using hrThis is a direct application of the Fredholm alternative; it does not assert injectivity of a particular integral operator.
For integers \(a\ge 0\), \(b{\gt}0\), the real \(\ell ^2\) diagonal with entries \((an+b)^{-1}\) has entries bounded by one. If \(a{\gt}0\), this diagonal operator is compact.
Lean Formalisation
theorem lp.norm_reciprocalAffine_le_one (a b n : ℕ) (hb : 0 < b) : ‖(↑a * ↑n + ↑b)⁻¹‖ ≤ 1Lean proof
/-- A reciprocal affine diagonal with positive integral offset is bounded by one. -/
theorem norm_reciprocalAffine_le_one (a b n : ℕ) (hb : 0 < b) :
‖((a : ℝ)*n+b)⁻¹‖ ≤ 1 := by
have h : (1 : ℝ) ≤ (a : ℝ)*n+b := by
have hb' : (1 : ℝ) ≤ b := by exact_mod_cast hb
nlinarith [mul_nonneg (Nat.cast_nonneg a : (0 : ℝ) ≤ a)
(Nat.cast_nonneg n : (0 : ℝ) ≤ n)]
rw [Real.norm_eq_abs, abs_of_nonneg (inv_nonneg.mpr (by linarith))]
exact inv_le_one_of_one_le₀ h