Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 187 research declarations. Search 10,000 more complete Mathlib declarations.
187 results
Clear filtersLinearPMap.IsClosed.resolventSet_eq'
Plain-language statement
For a closed operator the resolvent set consists of those regular points for which the defect number is zero.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsClosed.spectrum_eq
Project documentation
The continuous spectrum, σᶜ, of a partial linear map. A complex number z is in σᶜ T iff the range of T - z • 1 is not closed. -/ def continuousSpectrum (T : H →ₗ.[ℂ] H) : Set ℂ := {z : ℂ | ¬root.IsClosed ((T - z • 1).toFun.range : Set H)} @[inherit_doc continuousSpectrum] scoped notation "σᶜ" => continuousSpectrum lemma continuousSpectrum_eq (T...
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsUnbounded.orthogonal_adjoint_sub_ker
Plain-language statement
(T† - conj z • 1).kerᗮ = (T.closure - z • 1).range
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsUnbounded.orthogonal_closure_sub_range
Plain-language statement
(T.closure - z • 1).rangeᗮ = (T† - conj z • 1).ker
Source project: Physlib
Person-level attribution pending.
LinearPMap.mem_regularityDomain_iff
Plain-language statement
z is a regular point for T iff T - z • 1 has a continuous (equivalently, bounded) inverse.
Source project: Physlib
Person-level attribution pending.
LinearPMap.numericalRange_convex
Project documentation
The Toeplitz-Hausdorff theorem.
Source project: Physlib
Person-level attribution pending.