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,543 to 1,548 of 2,569 results.
LinearPMap.ball_subset_regularityDomain
Mathematical statement
The regularity domain of T contains open balls with radii controlled by the lower bounds.
Source project: Physlib
Person-level attribution pending.
LinearPMap.closure_domain_eq_domain_closure_of_continuous
Mathematical statement
A strengthening of closure_domain_le_domain_closure for continuous operators.
Source project: Physlib
Person-level attribution pending.
LinearPMap.compl_closure_numericalRange_subset_regularityDomain
Mathematical statement
The regularity domain contains the exterior of the numerical range.
Source project: Physlib
Person-level attribution pending.
LinearPMap.covariance_comm
Mathematical statement
Swapping the two observables does not change the covariance.
Source project: Physlib
Person-level attribution pending.
LinearPMap.covariance_eq_re_symm_centered
Mathematical statement
Covariance as the real part of the symmetrized centered inner product.
Source project: Physlib
Person-level attribution pending.
LinearPMap.HasDenseDomain.orthogonal_range
Mathematical statement
U.rangeᗮ = U†.ker c.f. LinearMap.orthogonal_range and ContinuousLinearMap.orthogonal_range
Source project: Physlib
Person-level attribution pending.