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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,561 to 1,566 of 2,569 results.
LinearPMap.IsSelfAdjoint.mem_resolventSet_of_range_eq_top
Mathematical statement
(T - z • 1).range = ⊤ is a sufficient condition for z ∈ ρ T (and it is a necessary condition by definition of ρ).
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsSymmetric.closure
Mathematical statement
The closure of a symmetric densely-defined operator is symmetric: T†† is a symmetric closed extension of T, so it extends T.closure, whose symmetry then descends.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsSymmetric.Iio_subset_regularityDomain
Mathematical statement
If m is a lower bound on the numerical range then the regularity domain contains (-∞,m).
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsSymmetric.isEssentiallySelfAdjoint_of_defectNumber_eq_zero
Mathematical statement
The basic criterion for essential self-adjointness: a symmetric, densely-defined operator whose defect numbers at I and -I both vanish is essentially self-adjoint.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsSymmetric.isSelfAdjoint_of_range_eq_top
Mathematical statement
Self-adjointness from surjectivity of T ± i: a symmetric, densely-defined operator T for which T + I • 1 and T - I • 1 both have full range is self-adjoint.
Source project: Physlib
Person-level attribution pending.
LinearPMap.IsSymmetric.pointSpectrum_real
Mathematical statement
Eigenvalues of a symmetric unbounded operator are real.
Source project: Physlib
Person-level attribution pending.