mathlib3
feat(analysis/special_functions): add `is_o`/`is_Theta` lemmas about `real.exp`
#14835
Open
Open
feat(analysis/special_functions): add `is_o`/`is_Theta` lemmas about `real.exp` #14835
urkud
wants to merge
87 commits into
master
from
YK-is-o-pow-exp
Snapshot
afc12c66
Snapshot
170100c8
Snapshot
d83a0814
Snapshot
60719809
Fix
a34520e7
Fix
0b0cc5cf
Merge branch 'master' into YK-is-o-calc
08e1c96c
Fix
9a8ab4bb
Fix
e2925703
Fix
691965b9
Fix
ac04dce4
Fix
15ee5fb6
Merge branch 'master' into YK-is-o-calc
19277ff3
Merge branch 'master' into YK-is-o-calc
09d738ef
Merge branch 'master' into YK-is-o-calc
a77105f4
Fix docs
997f63cb
Fix
21a7195e
Fix
d6b56045
Snapshot
c1ed8768
Merge branch 'master' into YK-is-o-calc
c35a475f
Merge branch 'YK-is-o-calc' into YK-is-o-pow-exp
6422bb98
Drop #check
4e407337
feat(order/liminf_limsup): composition `f ∘ g` is bounded iff `g` is …
7f878f56
...
8549c82b
feat(analysis/asymptotics/asymptotics): generalize `is_*.inv_rev`
99601d4d
Merge branch 'YK-O-inv-rev' into YK-is-o-pow-exp
4d80e5eb
feat(analysis/asymptotics/asymptotics): generalize `is_O.smul` etc
76872e79
Merge branch 'YK-is-o-smul' into YK-is-theta
6df1b63d
Snapshot
7194983e
Merge branch 'master' into YK-bounded-under-exp
545c99cc
Snapshot
c428657a
Merge branch 'YK-O-const-exp' into YK-is-theta
bb81876c
...
093c9b74
Merge branch 'YK-is-theta' into YK-is-o-pow-exp
12a210c8
Revert
f2a50d02
Snapshot
18eaa1c0
Merge branch 'master' into YK-is-o-pow-exp
e3c8e9ee
Fix merge
8aa7ceb9
Snapshot
396aeda9
Fix
e5c11943
Drop an unneeded import
1cd41a08
Merge branch 'master' into YK-is-o-pow-exp
15856e4c
Merge branch 'master' into YK-is-o-pow-exp
f85d4623
Fix, update
24df171f
Move some lemmas to a new file
6767f138
urkud
changed the title
urkud
changed the title 
sgouezel
commented
on 2022-06-24
Snapshot
72efc153
Merge branch 'master' into YK-is-o-pow-exp
296aaa65
Snapshot
38967395
Snapshot
b708b3e6
Add `@[simp]`
878692ab
Long line
48742293
Snapshot
92f5a521
Fix, golf
2342304b
Add `abs` versions
a06bf943
Fix
2345993b
Drop duplicate args
00092b47
Merge branch 'master' into YK-is-oO
1868cb52
Fix `alias`
939ba9f5
Merge branch 'master' into YK-is-o-pow-exp
c40b8daf
Merge branch 'YK-is-oO' into YK-is-o-pow-exp
9c667cc1
Merge branch 'master' into YK-is-oO
2ac207e7
Merge branch 'YK-is-oO' into YK-is-o-pow-exp
758e526d
Merge branch 'master' into YK-is-o-pow-exp
bb3d7313
Revert
90d0f479
Fix
3431376d
Merge branch 'master' into YK-is-o-pow-exp
1de4b900
Merge branch 'master' into YK-is-o-pow-exp
f3656072
Snapshot
7fc7bacb
Fix
c08e10b5
Fix
61e6b43f
Merge branch 'YK-rpow-pow-assumptions' into YK-is-o-pow-exp
462dbc2f
Merge branch 'master' into YK-is-o-pow-exp
864f743f
Update
b73e79e8
Merge branch 'master' into YK-is-o-pow-exp
a0644e52
Merge branch 'master' into YK-is-o-pow-exp
a293f043
Merge branch 'master' into YK-is-o-pow-exp
3acad0b9
Snapshot
2f396f41
Merge branch 'master' into YK-is-o-pow-exp
962b8d49
Snapshot
aab85dcb
Update
96a60f2f
Merge branch 'master' into YK-tendsto-const-mul
bcfc6ee2
Merge branch 'YK-tendsto-const-mul' into YK-is-o-pow-exp
e76b1b45
Snapshot
4923b989
Merge branch 'master' into YK-tendsto-const-mul
d70104b6
Merge branch 'YK-tendsto-const-mul' into YK-is-o-pow-exp
42508050
Snapshot
998142f3
Merge branch 'master' into YK-is-o-pow-exp
532141f5
urkud
changed the title 
Login to write a write a comment.
Login via GitHub