OAI/Analysis/Pureness/Projections/FiniteSpectralIntegralRankRecovery.lean
4 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CuntzPureness.finiteSpectralIntegral_root_cut_lowerline 11 - theorem
OAI.CuntzPureness.finiteSpectralIntegral_cut_le_iSup_rootsline 23 - theorem
OAI.CuntzPureness.finiteSpectralIntegral_iSup_rootsline 60 - theorem
OAI.CuntzPureness.finiteSpectralIntegral_roots_tendsto_contractionline 72