OAI/Analysis/Pureness/Divisibility/SourceRankLimit.lean
3 declarations, 0 contain sorry, 0 declared as axioms
- lemma
OAI.CuntzPureness.nnrpow_smul_realline 9 - lemma
OAI.CuntzPureness.normalizedRoot_trace_tendsto_realRankline 23 - theorem
OAI.CuntzPureness.source_root_trace_tendsto_rankline 32