Commit 2023-11-13 10:03 87b37fc4
View on Github →feat: simplify proof of spectrum.nonempty using the cobounded filter (#8246)
This uses the API developed in these recent PRs (for the cobounded filter and some corollaries to Liouville's theorem) to greatly simplify the proof of spectrum.nonempty. Previously, this depended on the technical lemma spectrum.norm_resolvent_le_forall, and now we instead prove the greatly simplified spectrum.resolvent_isBigO_inv and spectrum.resolvent_tendsto_cobounded.