Documentation

Atlas.IntroductionToFunctionalAnalysis.code.SpectralTheory

theorem SpectralTheory.range_orthogonal_eq_ker_adjoint {๐•œ : Type u_1} [RCLike ๐•œ] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ๐•œ H] [CompleteSpace H] (A : H โ†’L[๐•œ] H) :

Let $H$ be a Hilbert space, and let $A : H \to H$ be a bounded linear operator. Then $(\operatorname{Ran}(A))^\perp = \operatorname{Null}(A^\ast)$: the orthogonal complement of the range of $A$ equals the kernel of its adjoint.

def SpectralTheory.IsSelfAdjointOperator {๐•œ : Type u_1} [RCLike ๐•œ] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ๐•œ H] [CompleteSpace H] (T : H โ†’L[๐•œ] H) :

A bounded linear operator $T : H \to H$ on a Hilbert space is self-adjoint if $T = T^\ast$. This is a wrapper around Mathlib's IsSelfAdjoint.

Instances For
    theorem SpectralTheory.IsSelfAdjointOperator.inner_real_and_norm_eq_iSup_rayleighQuotient {๐•œ : Type u_1} [RCLike ๐•œ] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ๐•œ H] [CompleteSpace H] {T : H โ†’L[๐•œ] H} (hT : IsSelfAdjointOperator T) :
    (โˆ€ (u : H), โˆƒ (r : โ„), inner ๐•œ (T u) u = โ†‘r) โˆง โ€–Tโ€– = โจ† (x : H), |T.rayleighQuotient x|

    If $T \in \mathcal{B}(H)$ is a self-adjoint operator (i.e. $T = T^\ast$), then $\langle Tu, u\rangle \in \mathbb{R}$ for every $u \in H$, and the operator norm satisfies $\|T\| = \sup_{\|x\| = 1} |\langle Tx, x\rangle|$, expressed here in terms of the Rayleigh quotient.

    theorem SpectralTheory.hasEigenvalue_iff_exists_ne_zero {๐•œ : Type u_1} [RCLike ๐•œ] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ๐•œ H] [CompleteSpace H] (T : H โ†’L[๐•œ] H) (ฮผ : ๐•œ) :
    Module.End.HasEigenvalue (โ†‘T) ฮผ โ†” โˆƒ (u : H), u โ‰  0 โˆง T u = ฮผ โ€ข u

    Characterization of eigenvalues: for $T \in \mathcal{B}(H)$ and $\mu \in \mathbb{K}$, $\mu$ is an eigenvalue of $T$ if and only if there exists a nonzero vector $u \in H$ (the associated eigenvector) such that $Tu = \mu u$.

    theorem SpectralTheory.isCompact_iff_isClosed_bounded (๐•œ : Type u_1) [RCLike ๐•œ] {E : Type u_2} [NormedAddCommGroup E] [NormedSpace ๐•œ E] [FiniteDimensional ๐•œ E] (s : Set E) :

    Heineโ€“Borel for finite-dimensional normed spaces over $\mathbb{R}$ or $\mathbb{C}$: a subset $s \subseteq E$ is compact if and only if it is closed and bounded.

    In a metric space $X$, a subset $K \subseteq X$ is compact if and only if it is sequentially compact: every sequence in $K$ has a subsequence converging to an element of $K$.

    theorem SpectralTheory.ker_smul_id_sub_eq_eigenspace {๐•œ : Type u_1} [RCLike ๐•œ] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ๐•œ H] (T : H โ†’L[๐•œ] H) (ฮผ : ๐•œ) :
    (โ†‘(ฮผ โ€ข ContinuousLinearMap.id ๐•œ H - T)).ker = Module.End.eigenspace (โ†‘T) ฮผ

    Auxiliary lemma: the kernel of $\mu I - T$ coincides with the eigenspace of $T$ associated to the eigenvalue $\mu$.

    theorem SpectralTheory.fredholm_alternative_full {๐•œ : Type u_1} [RCLike ๐•œ] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ๐•œ H] [CompleteSpace H] {T : H โ†’L[๐•œ] H} (hT : IsCompactOperator โ‡‘T) (hsa : IsSelfAdjoint T) {ฮผ : ๐•œ} (hฮผ : ฮผ โ‰  0) :
    (โ†‘(ฮผ โ€ข ContinuousLinearMap.id ๐•œ H - T)).range = (โ†‘(ฮผ โ€ข ContinuousLinearMap.id ๐•œ H - T)).kerแ—ฎ โˆง (Function.Bijective โ‡‘(ฮผ โ€ข ContinuousLinearMap.id ๐•œ H - T) โˆจ (โ†‘(ฮผ โ€ข ContinuousLinearMap.id ๐•œ H - T)).ker โ‰  โŠฅ โˆง FiniteDimensional ๐•œ โ†ฅ(โ†‘(ฮผ โ€ข ContinuousLinearMap.id ๐•œ H - T)).ker)

    Fredholm alternative. Let $A = A^\ast \in \mathcal{B}(H)$ be a self-adjoint compact operator, and let $\mu \in \mathbb{K} \setminus \{0\}$. Then $\operatorname{Range}(\mu I - A)$ is closed (equal to $\operatorname{Null}(\mu I - A)^\perp$), and either $\mu I - A$ is bijective, or its kernel โ€” the eigenspace of $A$ associated to $\mu$ โ€” is nontrivial and finite-dimensional.

    theorem SpectralTheory.compact_selfAdjoint_maximum_principle {๐•œ : Type u_1} [RCLike ๐•œ] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ๐•œ H] [CompleteSpace H] (hInfDim : ยฌFiniteDimensional ๐•œ H) (T : H โ†’L[๐•œ] H) (hT : IsSelfAdjoint T) (hc : IsCompactOperator โ‡‘T) :
    โˆƒ (s : โ„• โ†’ ๐•œ) (u : โ„• โ†’ H), (โˆ€ (n : โ„•), T (u n) = s n โ€ข u n) โˆง Orthonormal ๐•œ u โˆง (โˆ€ (n : โ„•), โ€–s (n + 1)โ€– โ‰ค โ€–s nโ€–) โˆง Filter.Tendsto (fun (n : โ„•) => โ€–s nโ€–) Filter.atTop (nhds 0) โˆง โˆ€ (n : โ„•), โ€–s nโ€– = โจ† (x : H), โจ† (_ : โ€–xโ€– = 1), โจ† (_ : โˆ€ i < n, inner ๐•œ x (u i) = 0), โ€–inner ๐•œ (T x) xโ€–

    Maximum principle. Let $A = A^\ast \in \mathcal{B}(H)$ be a self-adjoint compact operator on an infinite-dimensional Hilbert space. Then the nonzero eigenvalues of $A$ can be ordered as $|\lambda_1| \ge |\lambda_2| \ge \cdots$ (counted with multiplicity), with pairwise orthonormal eigenvectors $\{u_k\}$ such that $T u_k = \lambda_k u_k$, $|\lambda_j| \to 0$, and for each $j$, $|\lambda_j| = \sup_{\|u\|=1,\, u \in \operatorname{Span}(u_1,\dots,u_{j-1})^\perp} |\langle Au, u\rangle|$.

    theorem SpectralTheory.spectral_theorem_range_decomposition {๐•œ : Type u_1} [RCLike ๐•œ] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ๐•œ H] [CompleteSpace H] {T : H โ†’L[๐•œ] H} (hT : IsCompactOperator โ‡‘T) (hsa : IsSelfAdjoint T) :
    (โจ† (ฮผ : ๐•œ), โจ† (_ : ฮผ โ‰  0), Module.End.eigenspace (โ†‘T) ฮผ).topologicalClosure = (โ†‘T).range.topologicalClosure โˆง IsCompl (โ†‘T).range.topologicalClosure (โ†‘T).ker โˆง OrthogonalFamily ๐•œ (fun (ฮผ : ๐•œ) => โ†ฅ(Module.End.eigenspace (โ†‘T) ฮผ)) fun (ฮผ : ๐•œ) => (Module.End.eigenspace (โ†‘T) ฮผ).subtypeโ‚—แตข

    Spectral theorem for compact self-adjoint operators (range decomposition form). Let $A = A^\ast \in \mathcal{B}(H)$ be a compact self-adjoint operator on a Hilbert space $H$. Then: (1) the closure of the span of all nonzero eigenspaces of $A$ equals the closure of $\operatorname{Range}(A)$; (2) $\overline{\operatorname{Range}(A)}$ and $\operatorname{Null}(A)$ are complementary closed subspaces of $H$; and (3) the family of eigenspaces of $A$ is an orthogonal family.

    theorem SpectralTheory.rayleighQuotient_algebraMap_sub {๐•œ : Type u_1} [RCLike ๐•œ] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ๐•œ H] (T : H โ†’L[๐•œ] H) (t : โ„) (x : H) (hx : x โ‰  0) :
    ((algebraMap ๐•œ (H โ†’L[๐•œ] H)) โ†‘t - T).rayleighQuotient x = t - T.rayleighQuotient x

    Auxiliary lemma: for $t \in \mathbb{R}$ and a nonzero vector $x$, the Rayleigh quotient of $tI - T$ at $x$ equals $t$ minus the Rayleigh quotient of $T$ at $x$.

    theorem SpectralTheory.selfAdjoint_spectrum_subset_Icc {๐•œ : Type u_1} [RCLike ๐•œ] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ๐•œ H] [CompleteSpace H] [Nontrivial H] (T : H โ†’L[๐•œ] H) (hT : IsSelfAdjoint T) {mu : ๐•œ} (hmu : mu โˆˆ spectrum ๐•œ T) :
    โจ… (x : H), T.rayleighQuotient x โ‰ค RCLike.re mu โˆง RCLike.re mu โ‰ค โจ† (x : H), T.rayleighQuotient x

    The spectrum of a self-adjoint operator $T \in \mathcal{B}(H)$ is bounded by the Rayleigh quotient: for every $\mu \in \operatorname{Spec}(T)$, $\inf_{x} \langle Tx, x\rangle / \|x\|^2 \le \operatorname{Re}\mu \le \sup_{x} \langle Tx, x\rangle / \|x\|^2$.

    theorem SpectralTheory.positive_iff_spectrum_nonneg {๐•œ : Type u_1} [RCLike ๐•œ] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ๐•œ H] [CompleteSpace H] [Nontrivial H] (T : H โ†’L[๐•œ] H) (hT : IsSelfAdjoint T) :
    (โˆ€ (u : H), 0 โ‰ค T.reApplyInnerSelf u) โ†” โˆ€ ฮผ โˆˆ spectrum ๐•œ T, 0 โ‰ค RCLike.re ฮผ

    Let $A = A^\ast \in \mathcal{B}(H)$ be a self-adjoint operator. Then $A$ is positive โ€” i.e. $\langle Au, u\rangle \ge 0$ for all $u \in H$ โ€” if and only if $\operatorname{Spec}(A) \subseteq [0, \infty)$.

    theorem SpectralTheory.isOpen_invertible_operators {๐•œ : Type u_1} [RCLike ๐•œ] {H : Type u_2} [NormedAddCommGroup H] [InnerProductSpace ๐•œ H] [CompleteSpace H] :
    IsOpen {T : H โ†’L[๐•œ] H | Function.Bijective โ‡‘T}

    The space of invertible bounded linear operators $GL(H) = \{T \in \mathcal{B}(H) : T \text{ invertible}\}$ is an open subset of $\mathcal{B}(H)$.

    @[reducible, inline]

    The Hilbert space $L^2([0,1])$ of square-integrable real-valued functions on the unit interval, equipped with the restriction of Lebesgue measure to $[0,1]$.

    Instances For
      noncomputable def SpectralTheory.sineBasisFun (k : โ„•+) :

      The $k$-th orthonormal sine basis function on $[0,1]$: $u_k(x) = \sqrt{2} \sin(k\pi x)$. These form an orthonormal eigenbasis of the Green's operator with Dirichlet boundary conditions on the unit interval.

      Instances For

        The $k$-th eigenvalue of the Green's operator on $[0,1]$ with Dirichlet boundary conditions: $\lambda_k = \dfrac{1}{k^2 \pi^2}$.

        Instances For

          The square root of the $k$-th eigenvalue of the Green's operator, $\sqrt{\lambda_k} = \dfrac{1}{k\pi}$. This is the $k$-th eigenvalue of $A^{1/2}$.

          Instances For

            The square root $A^{1/2}$ of the Green's operator, defined via its action on the orthonormal eigenbasis $\{b_k\}$: if $f = \sum_k c_k\, b_k$ where $c_k = \langle b_k, f\rangle$, then $A^{1/2} f = \sum_k \frac{1}{k\pi}\, c_k\, b_k$.

            Instances For
              noncomputable def SpectralTheory.greensKernel (x t : โ„) :

              The Green's kernel for the Dirichlet Laplacian on $[0,1]$: $G(x,t) = \min(x,t)\,(1 - \max(x,t))$. The Green's operator $f \mapsto \int_0^1 G(x,t) f(t)\,dt$ is the inverse of $-\frac{d^2}{dx^2}$ subject to $u(0)=u(1)=0$.

              Instances For

                Key computation showing that the sine basis functions are eigenfunctions of the Green's operator: for $x \in [0,1]$, $\int_0^1 G(x,t)\, u_k(t)\, dt = \lambda_k\, u_k(x)$, where $G$ is the Green's kernel, $u_k(x) = \sqrt{2}\sin(k\pi x)$ and $\lambda_k = 1/(k^2\pi^2)$.

                theorem SpectralTheory.greens_operator_eigendecomposition (A : Module.End โ„ โ†ฅL2UnitInterval) (b : HilbertBasis โ„•+ โ„ โ†ฅL2UnitInterval) (hA_sa : โˆ€ (f g : โ†ฅL2UnitInterval), inner โ„ (A f) g = inner โ„ f (A g)) (hb : โˆ€ (k : โ„•+), โ†‘โ†‘(b k) =แต[MeasureTheory.volume.restrict (Set.Icc 0 1)] sineBasisFun k) (hA_greens : โˆ€ (f : โ†ฅL2UnitInterval), โ†‘โ†‘(A f) =แต[MeasureTheory.volume.restrict (Set.Icc 0 1)] fun (x : โ„) => โˆซ (t : โ„) in Set.Icc 0 1, greensKernel x t * โ†‘โ†‘f t) :

                Spectral decomposition of the Green's operator on $L^2([0,1])$. If $A$ is the self-adjoint operator on $L^2([0,1])$ given by the Green's kernel $Af(x) = \int_0^1 G(x,t)\, f(t)\, dt$, and $\{b_k\}_{k \in \mathbb{N}^+}$ is the Hilbert basis of sine functions $b_k(x) = \sqrt{2}\sin(k\pi x)$, then:

                • $\mathrm{Null}(A) = \{0\}$;
                • each $b_k$ is an eigenvector with eigenvalue $\lambda_k = 1/(k^2\pi^2)$;
                • every $f \in L^2([0,1])$ satisfies $Af = \sum_{k=1}^\infty \lambda_k\, \langle b_k, f\rangle\, b_k$.
                theorem SpectralTheory.sturm_liouville_existence (V : C(โ†‘(Set.Icc 0 1), โ„)) (hV : โˆ€ (x : โ†‘(Set.Icc 0 1)), 0 โ‰ค V x) (f : C(โ†‘(Set.Icc 0 1), โ„)) :
                โˆƒ (u : โ„ โ†’ โ„), ContDiffOn โ„ 2 u (Set.Icc 0 1) โˆง (โˆ€ (x : โ„) (hx : x โˆˆ Set.Icc 0 1), -iteratedDerivWithin 2 u (Set.Icc 0 1) x + V โŸจx, hxโŸฉ * u x = f โŸจx, hxโŸฉ) โˆง u 0 = 0 โˆง u 1 = 0

                Existence for the Sturm-Liouville Dirichlet problem on $[0,1]$: given a continuous nonnegative potential $V \in C([0,1])$ with $V \geq 0$ and a continuous right-hand side $f \in C([0,1])$, there exists a $C^2$ function $u$ on $[0,1]$ satisfying $-u''(x) + V(x)\, u(x) = f(x)$ for all $x \in [0,1]$, with the Dirichlet boundary conditions $u(0) = u(1) = 0$.

                theorem SpectralTheory.sturm_liouville_uniqueness (V : C(โ†‘(Set.Icc 0 1), โ„)) (hV : โˆ€ (x : โ†‘(Set.Icc 0 1)), 0 โ‰ค V x) (f : C(โ†‘(Set.Icc 0 1), โ„)) (uโ‚ uโ‚‚ : โ„ โ†’ โ„) (hโ‚ : ContDiffOn โ„ 2 uโ‚ (Set.Icc 0 1) โˆง (โˆ€ (x : โ„) (hx : x โˆˆ Set.Icc 0 1), -iteratedDerivWithin 2 uโ‚ (Set.Icc 0 1) x + V โŸจx, hxโŸฉ * uโ‚ x = f โŸจx, hxโŸฉ) โˆง uโ‚ 0 = 0 โˆง uโ‚ 1 = 0) (hโ‚‚ : ContDiffOn โ„ 2 uโ‚‚ (Set.Icc 0 1) โˆง (โˆ€ (x : โ„) (hx : x โˆˆ Set.Icc 0 1), -iteratedDerivWithin 2 uโ‚‚ (Set.Icc 0 1) x + V โŸจx, hxโŸฉ * uโ‚‚ x = f โŸจx, hxโŸฉ) โˆง uโ‚‚ 0 = 0 โˆง uโ‚‚ 1 = 0) :
                Set.EqOn uโ‚ uโ‚‚ (Set.Icc 0 1)

                Uniqueness for the Sturm-Liouville Dirichlet problem on $[0,1]$: any two $C^2$ solutions $u_1, u_2$ of $-u'' + Vu = f$ on $[0,1]$ with the Dirichlet boundary conditions $u(0) = u(1) = 0$ (where $V \geq 0$ is continuous) must agree on $[0,1]$. The proof uses the convexity of $u^2$ when $u'' = V u$ with $V \geq 0$.

                theorem SpectralTheory.sturm_liouville_existence_uniqueness (V : C(โ†‘(Set.Icc 0 1), โ„)) (hV : โˆ€ (x : โ†‘(Set.Icc 0 1)), 0 โ‰ค V x) (f : C(โ†‘(Set.Icc 0 1), โ„)) :
                โˆƒ (u : โ„ โ†’ โ„), (ContDiffOn โ„ 2 u (Set.Icc 0 1) โˆง (โˆ€ (x : โ„) (hx : x โˆˆ Set.Icc 0 1), -iteratedDerivWithin 2 u (Set.Icc 0 1) x + V โŸจx, hxโŸฉ * u x = f โŸจx, hxโŸฉ) โˆง u 0 = 0 โˆง u 1 = 0) โˆง โˆ€ (v : โ„ โ†’ โ„), ContDiffOn โ„ 2 v (Set.Icc 0 1) โˆง (โˆ€ (x : โ„) (hx : x โˆˆ Set.Icc 0 1), -iteratedDerivWithin 2 v (Set.Icc 0 1) x + V โŸจx, hxโŸฉ * v x = f โŸจx, hxโŸฉ) โˆง v 0 = 0 โˆง v 1 = 0 โ†’ Set.EqOn u v (Set.Icc 0 1)

                Existence and uniqueness for the Sturm-Liouville Dirichlet problem on $[0,1]$: given a continuous nonnegative potential $V \in C([0,1])$ with $V \geq 0$ and a continuous right-hand side $f \in C([0,1])$, there exists a unique $C^2$ function $u$ on $[0,1]$ such that $-u'' + Vu = f$ on $[0,1]$, with the Dirichlet boundary conditions $u(0) = u(1) = 0$.