spectrum.exists_nnnorm_eq_spectralRadius
theorem spectrum.exists_nnnorm_eq_spectralRadius :
∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A]
[inst_3 : Nontrivial A] (a : A), ∃ z ∈ spectrum ℂ a, ↑‖z‖₊ = spectralRadius ℂ a
In the context of a complex Banach algebra, this theorem states that for every element of the algebra, there exists an element in its spectrum such that the non-negative norm of this spectral element is equal to the spectral radius of the original element. In other words, the spectral radius of any element in a complex Banach algebra is always attained by some element in its spectrum.
More concisely: In a complex Banach algebra, every element has a spectral value with equal norm to its spectral radius.
|
spectrum.spectralRadius_lt_of_forall_lt
theorem spectrum.spectralRadius_lt_of_forall_lt :
∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A]
[inst_3 : Nontrivial A] (a : A) {r : NNReal}, (∀ z ∈ spectrum ℂ a, ‖z‖₊ < r) → spectralRadius ℂ a < ↑r
This theorem states that in a complex Banach algebra, if the norm of every element of the spectrum of a given element 'a' is strictly less than a non-negative real number 'r', then the spectral radius of 'a' is also strictly less than 'r'. In other words, the spectral radius of an element in a complex Banach algebra is bounded above by the supremum of the norms of the elements in its spectrum.
More concisely: In a complex Banach algebra, the spectral radius of an element is less than the supremum of the norms of its spectrum elements.
|
spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius
theorem spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius :
∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A] (a : A),
Filter.Tendsto (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop (nhds (spectralRadius ℂ a))
**Gelfand's formula**: The theorem states that for any element `a` in a complex Banach algebra `A`, the spectral radius of `a` is obtained as the limit of the sequence `‖a ^ n‖₊ ^ (1 / n)` as `n` goes to infinity. In other words, when we take the `n`-th power of `a`, compute its non-negative norm, and then raise that to the power of `1/n`, as `n` grows larger and larger, this sequence converges to the spectral radius of `a`.
More concisely: The spectral radius of an element `a` in a complex Banach algebra is the limit of the sequence `‖a ^ n‖₊ ^ (1/n)` as `n` approaches infinity.
|
spectrum.isCompact
theorem spectrum.isCompact :
∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
[inst_3 : CompleteSpace A] [inst_4 : ProperSpace 𝕜] (a : A), IsCompact (spectrum 𝕜 a)
The theorem `spectrum.isCompact` states that for any normed field `𝕜`, any normed ring `A` that is also a `𝕜`-algebra, where `A` is a complete space and `𝕜` is a proper space, the spectrum of any element `a` of `A` is a compact set. In other words, for every nontrivial filter that contains the spectrum, there exists an element in the spectrum such that every set of the filter meets every neighborhood of that element.
More concisely: The spectrum of any complete, compact, normed `𝕜`-algebra over a proper normed field `𝕜` is a compact set.
|
spectrum.nonempty
theorem spectrum.nonempty :
∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A]
[inst_3 : Nontrivial A] (a : A), (spectrum ℂ a).Nonempty
This theorem states that in a nontrivial complex Banach algebra, the spectrum of any element is always nonempty. In more detail, for any given type `A` which is a normed ring and also a normed algebra over the complex numbers, and which additionally is a complete space (i.e., a Banach algebra), and is nontrivial (i.e., it consists of more than one element), then for any element `a` of `A`, the spectrum of `a` (as defined in the complex numbers) is a nonempty set. The spectrum of an element in this context is the set of complex numbers for which subtracting the element times 1 from the number does not yield a unit of the algebra.
More concisely: In a complex Banach algebra that is a nontrivial normed ring and algebra, the spectrum of any element is a nonempty set of complex numbers.
|
spectrum.map_pow
theorem spectrum.map_pow :
∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A]
[inst_3 : Nontrivial A] (a : A) (n : ℕ), spectrum ℂ (a ^ n) = (fun x => x ^ n) '' spectrum ℂ a
The `spectrum.map_pow` theorem is a specialization of the spectral mapping theorem for polynomials in a Banach algebra over the complex numbers, specifically for monic monomials. It states that for any Banach algebra `A` over the complex numbers, which is also a nontrivial complete normed ring, the spectrum of the `n`-th power of an element `a` from `A` is equal to the image of the `n`-th power function applied to the spectrum of `a` itself.
More concisely: For any monic monomial `a` in a nontrivial complete normed ring and Banach algebra `A` over the complex numbers, the spectrum of `a^n` is equal to the image of the `n`-th power function applied to the spectrum of `a`.
|
spectrum.map_polynomial_aeval
theorem spectrum.map_polynomial_aeval :
∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A]
[inst_3 : Nontrivial A] (a : A) (p : Polynomial ℂ),
spectrum ℂ ((Polynomial.aeval a) p) = (fun k => Polynomial.eval k p) '' spectrum ℂ a
The spectral mapping theorem for polynomials states that, given a Banach algebra `A` over the complex numbers `ℂ` which is also a normed ring and a complete space, for any element `a` of the algebra and any polynomial `p` with complex coefficients, the spectrum of the result of applying the algebra homomorphism `aeval` — which evaluates the polynomial at `a` — is equal to the image of the spectrum of `a` under the function that evaluates the polynomial at each point in the spectrum. In other words, it states that the spectrum of a polynomial evaluated at `a` maps to the spectrum of `a` evaluated at the polynomial.
More concisely: The spectrum of a polynomial evaluated at an element in a Banach algebra maps to the set of eigenvalues of that element.
|
spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius
theorem spectrum.pow_norm_pow_one_div_tendsto_nhds_spectralRadius :
∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A] (a : A),
Filter.Tendsto (fun n => ENNReal.ofReal (‖a ^ n‖ ^ (1 / ↑n))) Filter.atTop (nhds (spectralRadius ℂ a))
**Gelfand's formula**: For any element `a` of a complex Banach algebra `A`, the spectral radius of `a` is the limit as `n` goes to infinity of the `n`-th root of the nonnegative norm of `a` to the power `n`. Here, the spectral radius is the supremum of the nonnegative norms of elements in the spectrum, and this limit is taken in the sense of filter convergence, specifically from the filter `atTop` (representing going to infinity) to the neighborhood filter at the spectral radius of `a`. This theorem assures that the sequence `‖a ^ n‖₊ ^ (1 / n)` tends to the spectral radius of `a` as `n` goes to infinity.
More concisely: The spectral radius of an element `a` in a complex Banach algebra is equal to the limit, as `n` approaches infinity, of the `n`-th root of the norm of `a` raised to the power of `n`.
|
spectrum.exp_mem_exp
theorem spectrum.exp_mem_exp :
∀ {𝕜 : Type u_1} {A : Type u_2} [inst : RCLike 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
[inst_3 : CompleteSpace A] (a : A) {z : 𝕜},
z ∈ spectrum 𝕜 a → NormedSpace.exp 𝕜 z ∈ spectrum 𝕜 (NormedSpace.exp 𝕜 a)
The theorem states that for `𝕜` being either real numbers `ℝ` or complex numbers `ℂ`, the exponential function `exp 𝕜` transforms the spectrum of an element `a` into the spectrum of `exp 𝕜 a`. In other words, if a scalar `z` belongs to the spectrum of `a`, then the exponential of `z` (or `exp 𝕜 z`) belongs to the spectrum of `exp 𝕜 a`. This holds under several conditions: `A` is a normed ring, `𝕜` and `A` form a normed algebra, and `A` is a complete space.
More concisely: For any normed ring `A` with complete norm, if `𝕜` is a commutative normed algebra over `A` and `z` is an eigenvalue of `a` in `A`, then `exp 𝕜 z` is an eigenvalue of `exp 𝕜 a` in `A`.
|
spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul
theorem spectrum.hasFPowerSeriesOnBall_inverse_one_sub_smul :
∀ (𝕜 : Type u_1) {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A]
[inst_2 : NormedAlgebra 𝕜 A] [inst_3 : CompleteSpace A] (a : A),
HasFPowerSeriesOnBall (fun z => Ring.inverse (1 - z • a))
(fun n => ContinuousMultilinearMap.mkPiRing 𝕜 (Fin n) (a ^ n)) 0 (↑‖a‖₊)⁻¹
This theorem states that in a Banach algebra `A` over a nontrivially normed field `𝕜`, for any element `a` of `A`, the power series with coefficients being the `n`th power of `a` represents the function `(1 - z • a)⁻¹` in a disk of radius `‖a‖₊⁻¹`. In more mathematical terms, for any `a` in `A`, the power series ∑ a^n converges to the function (1 - z • a)⁻¹ on the open ball of radius 1/‖a‖₊ centered at 0. The coefficients of this power series are given by the `n`th power of `a`, and the convergence is understood in the sense of uniform convergence on compact subsets.
More concisely: In a Banach algebra over a nontrivially normed field, for any element `a`, the power series with coefficients `a^n` converges uniformly on compact subsets to the function `(1 - z • a)⁻¹` in the open ball of radius `1/‖a‖₊`.
|
spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius
theorem spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius :
∀ {A : Type u_2} [inst : NormedRing A] [inst_1 : NormedAlgebra ℂ A] [inst_2 : CompleteSpace A] (a : A),
Filter.limsup (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) Filter.atTop ≤ spectralRadius ℂ a
The theorem `spectrum.limsup_pow_nnnorm_pow_one_div_le_spectralRadius` states that for any complex normed algebra A which is also a complete space, and for any element 'a' in A, the limit superior (limsup) as n approaches infinity of the nth power of the non-negative norm of 'a' raised to the power of the reciprocal of n, is less than or equal to the spectral radius of 'a'. In simpler terms, this theorem relates the growth rate of the powers of 'a' to the spectral radius of 'a', and is used in the proof of Gelfand's formula in spectral theory.
More concisely: For any complex normed algebra A that is complete, and for any element a in A with non-negative norm, the limsup as n goes to infinity of (||a||^(1/n))^n is less than or equal to the spectral radius of a.
|
spectrum.mem_resolventSet_of_norm_lt_mul
theorem spectrum.mem_resolventSet_of_norm_lt_mul :
∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
[inst_3 : CompleteSpace A] {a : A} {k : 𝕜}, ‖a‖ * ‖1‖ < ‖k‖ → k ∈ resolventSet 𝕜 a
The theorem `spectrum.mem_resolventSet_of_norm_lt_mul` states that for any normed field `𝕜`, normed ring `A`, normed algebra over `𝕜` on `A`, and `A` being a complete space, given an element `a` from `A` and an element `k` from `𝕜`, if the norm of `a` multiplied by the norm of `1` is less than the norm of `k`, then `k` belongs to the resolvent set of `a` with respect to `𝕜`. In other words, `k` is a scalar in `𝕜` such that `k•1 - a` is a unit in the algebra `A`.
More concisely: If `𝕜` is a normed field, `A` is a normed ring and algebra over `𝕜` that is complete, and `a ∈ A`, `k ∈ 𝕜` satisfy `||a|| ||1|| < ||k||`, then `k` is in the resolvent set of `a` in `A` with respect to `𝕜`.
|
spectrum.differentiableOn_inverse_one_sub_smul
theorem spectrum.differentiableOn_inverse_one_sub_smul :
∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NontriviallyNormedField 𝕜] [inst_1 : NormedRing A]
[inst_2 : NormedAlgebra 𝕜 A] [inst_3 : CompleteSpace A] {a : A} {r : NNReal},
↑r < (spectralRadius 𝕜 a)⁻¹ → DifferentiableOn 𝕜 (fun z => Ring.inverse (1 - z • a)) (Metric.closedBall 0 ↑r)
In the context of a Banach algebra `A` over a field `𝕜`, for a given element `a : A`, the function defined by `z ↦ (1 - z • a)⁻¹` is differentiable on any closed ball centered at zero with radius `r` less than the reciprocal of the spectral radius of `a`. Here, `r` is a nonnegative real number, the spectral radius of `a` is the supremum of the norms of elements in the spectrum of `a`, and the differentiability is in the sense of `𝕜`. The closed ball is the set of all points within a distance `r` from the center (zero in this case).
More concisely: For any Banach algebra `A` over a field `𝕜` and element `a` in `A`, the function `z ↦ (1 - z • a)⁻¹` is differentiable on the closed ball centered at zero with radius less than the reciprocal of the spectral radius of `a`.
|
spectrum.norm_le_norm_of_mem
theorem spectrum.norm_le_norm_of_mem :
∀ {𝕜 : Type u_1} {A : Type u_2} [inst : NormedField 𝕜] [inst_1 : NormedRing A] [inst_2 : NormedAlgebra 𝕜 A]
[inst_3 : CompleteSpace A] [inst_4 : NormOneClass A] {a : A} {k : 𝕜}, k ∈ spectrum 𝕜 a → ‖k‖ ≤ ‖a‖
This theorem states that for any type 𝕜 which is a NormedField, and any type A which is a NormedRing and a NormedAlgebra over 𝕜, if the space A is complete and has a norm-one class, then for any element 'a' of type A and any element 'k' of type 𝕜, if 'k' belongs to the spectrum of 'a', the norm of 'k' is less than or equal to the norm of 'a'. In mathematical symbols, this can be written as: if $k \in spectrum(a)$, then $\|k\| \leq \|a\|$.
More concisely: For any NormedField 𝕜, NormedRing and NormedAlgebra A over 𝕜 with a complete, norm-one class, the spectrum of any element 'a' in A contains only norms less than or equal to the norm of 'a'.
|