Theorem asymptotics.is_O.of_bound'

refactor(analysis): change the symbol for norm to align with the unicode spec (#17575) …

feat(analysis/asymptotics): prove that a function has derivative 0 using asymptotics (#16934) …