Compact operators and nonarchimedean Fredholm theory

The declarations the status of Tau Ceti's roadmap names, and the other results named in the modules where only this status names declarations, or in folders below the areas where only it names 2 or more, as Tau Ceti has them at commit ace60277.

TheoremSerre's criterion over a field#

over a complete ultrametric nontrivially normed field K, a continuous linear map between model spaces is row compact exactly when it is completely continuous. Neither a discrete valuation nor spherical completeness is needed.

ContinuousLinearMap.isRowCompact_iff_isCompletelyContinuous.{u_1, u_2, u_4} {I : Type u_1}
  {J : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J] [DiscreteTopology J]
  [DecidableEq J] {K : Type u_4} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
  {u : ZeroAtInftyContinuousMap J K →L[K] ZeroAtInftyContinuousMap I K} :
  u.IsRowCompact ↔ u.IsCompletelyContinuous
Lean

Formalized in Tau Ceti as ContinuousLinearMap.isRowCompact_iff_isCompletelyContinuous.

Other forms

Serre's criterion. Formalized in Tau Ceti as ContinuousLinearMap.IsCompletelyContinuous.isRowCompact_of_forall_fg_isClosed.

ContinuousLinearMap.IsCompletelyContinuous.isRowCompact_of_forall_fg_isClosed.{u_1, u_2, u_3}
  {I : Type u_1} {J : Type u_2} {R : Type u_3} [TopologicalSpace I] [DiscreteTopology I]
  [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [NormedRing R] [IsUltrametricDist R]
  [CompleteSpace R] [TauCeti.NormedRing.IsTate R]
  {u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R}
  (hu : u.IsCompletelyContinuous)
  (hclosed : ∀ (L : Submodule R (ZeroAtInftyContinuousMap I R)), L.FG → IsClosed ↑L) :
  u.IsRowCompact

Serre's criterion for diagonal operators. Formalized in Tau Ceti as ZeroAtInftyContinuousMap.isCompletelyContinuous_diagonalCLM_iff.

ZeroAtInftyContinuousMap.isCompletelyContinuous_diagonalCLM_iff.{u_1, u_3} {I : Type u_1}
  [TopologicalSpace I] [DiscreteTopology I] {K : Type u_3} [NontriviallyNormedField K]
  [IsUltrametricDist K] [CompleteSpace K] {d : BoundedContinuousFunction I K} :
  (ZeroAtInftyContinuousMap.diagonalCLM d).IsCompletelyContinuous ↔
    Filter.Tendsto (⇑d) Filter.cofinite (nhds 0)

Serre's criterion for orthonormalisability. Formalized in Tau Ceti as TauCeti.isONable_iff_free_residueModule.

TauCeti.isONable_iff_free_residueModule.{u_4, u} {R : Type u_4} [NormedCommRing R]
  [IsUltrametricDist R] [NormOneClass R] [CompleteSpace R] {M : Type u} [NormedAddCommGroup M]
  [IsUltrametricDist M] [_root_.Module R M] [IsBoundedSMul R M] [CompleteSpace M]
  (ϖ : TauCeti.NormedRing.PseudoUniformizer R)
  (hR : ∀ (a : R), TauCeti.zpowCeil ‖↑ϖ.unit‖ ‖a‖ = ‖a‖)
  (hM : ∀ (m : M), TauCeti.zpowCeil ‖↑ϖ.unit‖ ‖m‖ = ‖m‖) :
  TauCeti.IsONable R M ↔
    Module.Free (↥(Subring.unitClosedBall R) ⧸ TauCeti.unitBallIdeal R) (TauCeti.ResidueModule R M)
Sources
LeanContinuousLinearMap.isRowCompact_iff_isCompletelyContinuous · ContinuousLinearMap.IsCompletelyContinuous.isRowCompact_of_forall_fg_isClosed · ZeroAtInftyContinuousMap.isCompletelyContinuous_diagonalCLM_iff · TauCeti.isONable_iff_free_residueModule
Uses 3 · Used by 1
Statement usesContinuousLinearMap.IsRowCompact
Proof usesQuantitative Open Mapping Theorem · Serre's theorem (TauCeti.ResidueModule.isOrthonormalBasis_iff)
Used bySerre's potential orthonormalisation theorem

TheoremRow compactness is compactoid image#

over an ultrametric nontrivially normed field, a map between model spaces is row compact exactly when it maps the closed unit ball to a compactoid set.

ContinuousLinearMap.isRowCompact_iff_hasCompactoidImage.{u_1, u_2, u_3} {I : Type u_1}
  {J : Type u_2} {K : Type u_3} [TopologicalSpace I] [DiscreteTopology I] [TopologicalSpace J]
  [DiscreteTopology J] [DecidableEq J] [NontriviallyNormedField K] [IsUltrametricDist K]
  {u : ZeroAtInftyContinuousMap J K →L[K] ZeroAtInftyContinuousMap I K} :
  u.IsRowCompact ↔ u.HasCompactoidImage
Lean

Formalized in Tau Ceti as ContinuousLinearMap.isRowCompact_iff_hasCompactoidImage.

Sources
LeanContinuousLinearMap.isRowCompact_iff_hasCompactoidImage
Uses 1
Statement usesContinuousLinearMap.IsRowCompact

TheoremThe Fredholm determinant is entire#

For a row-compact u, the principal-minor series det (1 - T u) is a restricted power series at every radius.

ContinuousLinearMap.IsRowCompact.isEntire_charPowerSeries.{u_1, u_2} {I : Type u_1} {R : Type u_2}
  [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedCommRing R] [NormOneClass R]
  [IsUltrametricDist R] {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R}
  (hu : u.IsRowCompact) : u.matrixCoeff.charPowerSeries.IsEntire
Lean

Formalized in Tau Ceti as ContinuousLinearMap.IsRowCompact.isEntire_charPowerSeries.

Sources
LeanContinuousLinearMap.IsRowCompact.isEntire_charPowerSeries
Uses 1 · Used by 5
Statement usesContinuousLinearMap.IsRowCompact
Used byContinuousLinearMap.IsRowCompact.evalAt_charPowerSeries_eq_zero_iff_hasEigenvalue · Invertibility and the Fredholm series · Strassmann's bound for the spectrum · The nonzero spectrum of a row-compact operator · The Riesz identity at a good zero

TheoremInvertibility and the Fredholm series#

For a row-compact endomorphism u of C₀(I, R), the operator 1 - a • u is invertible if and only if the value H_u(a) of the Fredholm series det (1 - T u) is a unit of R.

ContinuousLinearMap.IsRowCompact.isUnit_one_sub_smul_iff.{u_1, u_2} {I : Type u_1}
  [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {R : Type u_2} [NormedCommRing R]
  [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R]
  {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact)
  {a : R} : IsUnit (1 - a • u) ↔ IsUnit (u.matrixCoeff.charPowerSeries.evalAt a)
Lean

Formalized in Tau Ceti as ContinuousLinearMap.IsRowCompact.isUnit_one_sub_smul_iff.

Sources
LeanContinuousLinearMap.IsRowCompact.isUnit_one_sub_smul_iff
Uses 2
Statement usesContinuousLinearMap.IsRowCompact
Proof usesThe Fredholm determinant is entire

TheoremThe nonzero spectrum of a row-compact operator#

For a row-compact endomorphism u of C₀(I, K) over a complete ultrametric field and μ ≠ 0, μ lies in the spectrum of u if and only if μ⁻¹ is a zero of the Fredholm series det (1 - T u).

ContinuousLinearMap.IsRowCompact.mem_spectrum_iff_evalAt_inv_eq_zero.{u_1, u_2} {I : Type u_1}
  [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {K : Type u_2}
  [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
  {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact)
  {μ : K} (hμ : μ ≠ 0) : μ ∈ spectrum K u ↔ u.matrixCoeff.charPowerSeries.evalAt μ⁻¹ = 0
Lean

Formalized in Tau Ceti as ContinuousLinearMap.IsRowCompact.mem_spectrum_iff_evalAt_inv_eq_zero.

Sources
LeanContinuousLinearMap.IsRowCompact.mem_spectrum_iff_evalAt_inv_eq_zero
Uses 4 · Used by 1
Statement usesContinuousLinearMap.IsRowCompact
Proof usesContinuousLinearMap.charPowerSeries · The Fredholm determinant is entire · Independence of the presentation
Used byStrassmann's bound for the spectrum

TheoremContinuousLinearMap.IsCompletelyContinuous.isFredholm_one_sub#

A completely continuous perturbation of the identity is a Fredholm operator, over any complete nontrivially normed field.

ContinuousLinearMap.IsCompletelyContinuous.isFredholm_one_sub.{u_1, u_2} {K : Type u_1}
  {E : Type u_2} [NontriviallyNormedField K] [CompleteSpace K] [NormedAddCommGroup E]
  [NormedSpace K E] [CompleteSpace E] {u : E →L[K] E} (hu : u.IsCompletelyContinuous) :
  (1 - u).IsFredholm
Lean

Formalized in Tau Ceti as ContinuousLinearMap.IsCompletelyContinuous.isFredholm_one_sub.

Sources
LeanContinuousLinearMap.IsCompletelyContinuous.isFredholm_one_sub
Used by 1
Used byContinuousLinearMap.IsRowCompact.evalAt_charPowerSeries_eq_zero_iff_hasEigenvalue

TheoremContinuousLinearMap.IsRowCompact.evalAt_charPowerSeries_eq_zero_iff_hasEigenvalue#

The zeros of the Fredholm series of a row-compact operator are exactly the inverses of its nonzero eigenvalues. This conclusion concerns eigenvalues in the given coefficient field.

ContinuousLinearMap.IsRowCompact.evalAt_charPowerSeries_eq_zero_iff_hasEigenvalue.{u_1, u_2}
  {K : Type u_1} {I : Type u_2} [NontriviallyNormedField K] [CompleteSpace K] [IsUltrametricDist K]
  [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I]
  {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact)
  {a : K} : u.matrixCoeff.charPowerSeries.evalAt a = 0 ↔ a ≠ 0 ∧ Module.End.HasEigenvalue (↑u) a⁻¹
Lean

Formalized in Tau Ceti as ContinuousLinearMap.IsRowCompact.evalAt_charPowerSeries_eq_zero_iff_hasEigenvalue.

Sources
LeanContinuousLinearMap.IsRowCompact.evalAt_charPowerSeries_eq_zero_iff_hasEigenvalue
Uses 5
Statement usesContinuousLinearMap.IsRowCompact
Proof usesContinuousLinearMap.charPowerSeries · ContinuousLinearMap.IsCompletelyContinuous.isFredholm_one_sub · The Fredholm determinant is entire · Independence of the presentation

TheoremThe Riesz projector at a good zero#

Let u be row compact, and let a be a good zero of order h of its Fredholm determinant H_u: ΔʲH_u(a) = 0 for j < h and ΔʰH_u(a) is a unit. Then 1 - (C b) ^ h is a Riesz projection of u at a of order h.

ContinuousLinearMap.IsRowCompact.isRieszProjection_rieszProjection.{u_1, u_2} {I : Type u_1}
  {R : Type u_2} [TopologicalSpace I] [NormedCommRing R] [TauCeti.NormedRing.IsTate R]
  [DiscreteTopology I] [DecidableEq I] [IsUltrametricDist R] [CompleteSpace R]
  {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact)
  {a : R} {h : ℕ}
  (hH : ∀ j < h, ((PowerSeries.hasseDeriv j) u.matrixCoeff.charPowerSeries).evalAt a = 0)
  (hc : IsUnit (((PowerSeries.hasseDeriv h) u.matrixCoeff.charPowerSeries).evalAt a)) :
  u.IsRieszProjection a h (u.rieszProjection a h)
Lean

Formalized in Tau Ceti as ContinuousLinearMap.IsRowCompact.isRieszProjection_rieszProjection.

Sources
LeanContinuousLinearMap.IsRowCompact.isRieszProjection_rieszProjection
Uses 2
Statement usesContinuousLinearMap.IsRowCompact
Proof usesThe Riesz identity at a good zero

DefinitionContinuousLinearMap.IsRowCompact#

A continuous linear map between model spaces is row compact if the entries of its matrix are uniformly bounded and its row norms tend to zero along the cofinite filter of output indices. The bound is automatic over Tate scalars (ContinuousLinearMap.isRowCompact_iff_tendsto_rowNorm); it is part of the definition so that the real suprema defining the row norms are meaningful.

ContinuousLinearMap.IsRowCompact.{u_1, u_2, u_5} {I : Type u_1} {J : Type u_2} {R : Type u_5}
  [TopologicalSpace I] [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J] [SeminormedRing R]
  (u : ZeroAtInftyContinuousMap J R →L[R] ZeroAtInftyContinuousMap I R) : Prop
Lean

Formalized in Tau Ceti as ContinuousLinearMap.IsRowCompact.

Sources
LeanContinuousLinearMap.IsRowCompact
Used by 12
Used byA row-compact idempotent has projective range · ContinuousLinearMap.IsRowCompact.evalAt_charPowerSeries_eq_zero_iff_hasEigenvalue · Independence of the presentation · Invertibility and the Fredholm series · Row compactness is compactoid image · Row Hodge lower bound for a row-compact operator · Serre's criterion over a field · Strassmann's bound for the spectrum · The Fredholm determinant is entire · The nonzero spectrum of a row-compact operator · The Riesz identity at a good zero · The Riesz projector at a good zero

TheoremA row-compact idempotent has projective range# 

ContinuousLinearMap.IsRowCompact.projective_range_of_isIdempotentElem.{u_1, u_2} {I : Type u_1}
  {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] [NormedRing R]
  [IsUltrametricDist R] [TauCeti.NormedRing.IsTate R] [CompleteSpace R]
  {e : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : e.IsRowCompact)
  (he : IsIdempotentElem e) : Module.Projective R ↥(↑e).range
Lean

Formalized in Tau Ceti as ContinuousLinearMap.IsRowCompact.projective_range_of_isIdempotentElem.

Sources
LeanContinuousLinearMap.IsRowCompact.projective_range_of_isIdempotentElem
Uses 1
Statement usesContinuousLinearMap.IsRowCompact

DefinitionContinuousLinearMap.charPowerSeries#

The Fredholm series det (1 - T u) of an endomorphism u of a module M with property (Pr): the principal-minor series of the extension i ∘ u ∘ r of u through a retract presentation r ∘ i = id of M by a model space C₀(J, R), fixed by choice. If u is row compact, it does not depend on the presentation (ContinuousLinearMap.IsPrCompact.charPowerSeries_eq). If M does not have property (Pr) the series is 1.

ContinuousLinearMap.charPowerSeries.{u, w} {R : Type w} [SeminormedCommRing R] {M : Type u}
  [SeminormedAddCommGroup M] [_root_.Module R M] (u : M →L[R] M) : PowerSeries R
Lean

Formalized in Tau Ceti as ContinuousLinearMap.charPowerSeries.

Sources
LeanContinuousLinearMap.charPowerSeries
Used by 3
Used byContinuousLinearMap.IsRowCompact.evalAt_charPowerSeries_eq_zero_iff_hasEigenvalue · Independence of the presentation · The nonzero spectrum of a row-compact operator

TheoremIndependence of the presentation#

The Fredholm series of a row-compact endomorphism u of a module with property (Pr) is the principal-minor series of its extension i ∘ u ∘ r through any retract presentation r ∘ i = id of the module by a model space.

ContinuousLinearMap.IsPrCompact.charPowerSeries_eq.{u, w, u_1} {R : Type w} [NormedCommRing R]
  [NormOneClass R] [IsUltrametricDist R] [CompleteSpace R] [TauCeti.NormedRing.IsTate R]
  {M : Type u} [SeminormedAddCommGroup M] [_root_.Module R M] {u : M →L[R] M} (hu : u.IsPrCompact)
  {J : Type u_1} [TopologicalSpace J] [DiscreteTopology J] [DecidableEq J]
  {i : M →L[R] ZeroAtInftyContinuousMap J R} {r : ZeroAtInftyContinuousMap J R →L[R] M}
  (hri : r ∘SL i = ContinuousLinearMap.id R M) :
  u.charPowerSeries = (i ∘SL u ∘SL r).matrixCoeff.charPowerSeries
Lean

Formalized in Tau Ceti as ContinuousLinearMap.IsPrCompact.charPowerSeries_eq.

Sources
LeanContinuousLinearMap.IsPrCompact.charPowerSeries_eq
Uses 2 · Used by 2
Statement usesContinuousLinearMap.charPowerSeries · ContinuousLinearMap.IsRowCompact
Used byContinuousLinearMap.IsRowCompact.evalAt_charPowerSeries_eq_zero_iff_hasEigenvalue · The nonzero spectrum of a row-compact operator

DefinitionPowerSeries.IsGoodZero#

A power series f has a good zero of order h at a if its Hasse derivatives of order less than h vanish at a and its Hasse derivative of order h is a unit at a. For h = 0 this says that f(a) is a unit. Values at a are the infinite sums PowerSeries.evalAt, so the notion is meaningful for entire series over a complete normed ring.

PowerSeries.IsGoodZero.{u_1} {R : Type u_1} [CommRing R] [TopologicalSpace R] (f : PowerSeries R)
  (a : R) (h : ℕ) : Prop
Lean

Formalized in Tau Ceti as PowerSeries.IsGoodZero.

Sources
LeanPowerSeries.IsGoodZero

TheoremThe Riesz identity at a good zero#

Let u be row compact, put C = 1 - a • u, and suppose ΔʲH_u(a) = 0 for j < h while c = ΔʰH_u(a) is a unit, so that a is a good zero of order h of the Fredholm determinant. Then b = c⁻¹ • ΔʰV(a) satisfies C ^ (h + 1) b = C ^ h, that is, C ^ h (C b - 1) = 0. This is the identity from which the Riesz projector 1 - (C b) ^ h at a and its complementary projector (C b) ^ h are built.

ContinuousLinearMap.IsRowCompact.one_sub_smul_pow_succ_mul_inverse_smul_resolventHasseDerivAt.{u_1,
    u_2}
  {I : Type u_1} {R : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I]
  [NormedCommRing R] [TauCeti.NormedRing.IsTate R] [IsUltrametricDist R] [CompleteSpace R]
  {u : ZeroAtInftyContinuousMap I R →L[R] ZeroAtInftyContinuousMap I R} (hu : u.IsRowCompact)
  {a : R} {h : ℕ}
  (hH : ∀ j < h, ((PowerSeries.hasseDeriv j) u.matrixCoeff.charPowerSeries).evalAt a = 0)
  (hc : IsUnit (((PowerSeries.hasseDeriv h) u.matrixCoeff.charPowerSeries).evalAt a)) :
  (1 - a • u) ^ (h + 1) *
      Ring.inverse (((PowerSeries.hasseDeriv h) u.matrixCoeff.charPowerSeries).evalAt a) •
        u.resolventHasseDerivAt h a =
    (1 - a • u) ^ h
Lean

Formalized in Tau Ceti as ContinuousLinearMap.IsRowCompact.one_sub_smul_pow_succ_mul_inverse_smul_resolventHasseDerivAt.

Sources
LeanContinuousLinearMap.IsRowCompact.one_sub_smul_pow_succ_mul_inverse_smul_resolventHasseDerivAt
Uses 2 · Used by 1
Statement usesContinuousLinearMap.IsRowCompact
Proof usesThe Fredholm determinant is entire
Used byThe Riesz projector at a good zero

TheoremRow Hodge lower bound for a row-compact operator#

Let v be a real additive valuation on an ultrametric normed field with ‖x‖ = b ^ (-v x) for x ≠ 0, where b > 1. For a row-compact endomorphism u of C₀(I, K), the row Hodge polygon of its row norms lies below the Newton polygon of its principal-minor series u.matrixCoeff.charPowerSeries. When K is complete, these principal-minor sums converge and the series is the Fredholm series det (1 - T u).

ContinuousLinearMap.IsRowCompact.rowHodgePolygon_rowNorm_le_newtonPolygon_charPowerSeries.{u_1, u_2}
  {I : Type u_1} {K : Type u_2} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {b : ℝ}
  [NormedField K] [IsUltrametricDist K] {v : AddValuation K (WithTop ℝ)}
  {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact)
  (hb : 1 < b) (hv : ∀ (x : K), x ≠ 0 → ‖x‖ = b ^ (-(v x).untop₀)) :
  TauCeti.rowHodgePolygon b u.rowNorm ≤ u.matrixCoeff.charPowerSeries.newtonPolygon v
Lean

Formalized in Tau Ceti as ContinuousLinearMap.IsRowCompact.rowHodgePolygon_rowNorm_le_newtonPolygon_charPowerSeries.

Sources
LeanContinuousLinearMap.IsRowCompact.rowHodgePolygon_rowNorm_le_newtonPolygon_charPowerSeries
Uses 2
Statement usesContinuousLinearMap.IsRowCompact
Proof usesRow Hodge lower bound for the principal-minor series

TheoremStrassmann's bound for the spectrum#

Let u be a row-compact endomorphism of C₀(I, K), and let its Fredholm series H_u be distinguished of degree s at the radius ε⁻¹. Then the extension of u to C₀(I, L), for a complete normed field extension L of K, has at most s spectral values of norm at least ε.

ContinuousLinearMap.IsRowCompact.encard_setOf_mem_spectrum_mapCoeffs_le.{u_1, u_2, u_3}
  {I : Type u_1} [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {K : Type u_2}
  {L : Type u_3} [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
  [NontriviallyNormedField L] [NormedAlgebra K L] [IsUltrametricDist L] [CompleteSpace L]
  {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact)
  {ε : ℝ} (hε : 0 < ε) {s : ℕ}
  (hs : TauCeti.PowerSeries.IsDistinguished ε⁻¹ s u.matrixCoeff.charPowerSeries) :
  {μ | μ ∈ spectrum L (u.mapCoeffs (algebraMap K L) ⋯) ∧ ε ≤ ‖μ‖}.encard ≤ ↑s
Lean

Formalized in Tau Ceti as ContinuousLinearMap.IsRowCompact.encard_setOf_mem_spectrum_mapCoeffs_le.

Other forms

Strassmann's bound for the spectrum over the coefficient field. Formalized in Tau Ceti as ContinuousLinearMap.IsRowCompact.encard_setOf_mem_spectrum_le.

ContinuousLinearMap.IsRowCompact.encard_setOf_mem_spectrum_le.{u_1, u_2} {I : Type u_1}
  [TopologicalSpace I] [DiscreteTopology I] [DecidableEq I] {K : Type u_2}
  [NontriviallyNormedField K] [IsUltrametricDist K] [CompleteSpace K]
  {u : ZeroAtInftyContinuousMap I K →L[K] ZeroAtInftyContinuousMap I K} (hu : u.IsRowCompact)
  {ε : ℝ} (hε : 0 < ε) {s : ℕ}
  (hs : TauCeti.PowerSeries.IsDistinguished ε⁻¹ s u.matrixCoeff.charPowerSeries) :
  {μ | μ ∈ spectrum K u ∧ ε ≤ ‖μ‖}.encard ≤ ↑s
Sources
LeanContinuousLinearMap.IsRowCompact.encard_setOf_mem_spectrum_mapCoeffs_le · ContinuousLinearMap.IsRowCompact.encard_setOf_mem_spectrum_le
Uses 4
Statement usesContinuousLinearMap.IsRowCompact
Proof usesThe Fredholm determinant is entire · The nonzero spectrum of a row-compact operator · Strassmann's theorem

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.