PR #748 asymptotics and the Fréchet derivative

asymptotics and the Fréchet derivative #748

avigad merged 11 commits into leanprover-community:master from fderiv

digama0 commented on 2019-02-22

kckennylau commented on 2019-02-22

digama0 commented on 2019-02-22

kckennylau commented on 2019-02-22

digama0 commented on 2019-02-22

kckennylau commented on 2019-02-22

digama0 commented on 2019-02-22

kckennylau commented on 2019-02-22

digama0 commented on 2019-02-22

kckennylau commented on 2019-02-22

digama0 commented on 2019-02-22

kckennylau commented on 2019-02-22

digama0 commented on 2019-02-22

jdsalchow commented on 2019-02-22

cipher1024 assigned

digama0 6 years ago

sgouezel commented on 2019-02-23

feat(*): add various small lemmas

91c55d42

feat(analysis/asymptotics): start on bigo and littlo

876d392e

feat(analysis/normed_space/deriv): start on derivative

e5cb19a8

feat(analysis/asymptotics,analysis/normed_space/deriv): improvements …

e8c62d17

fix(asymptotics, deriv): minor formatting fixes

ea963a96

add has_fderiv_at_filter

36b42137

fix(*): fix things from change tendsto_congr -> tendsto.congr'

b76e1477

feat(analysis/*): is_bigo -> is_O, is_littleo -> is_o

ee4e4608

feat(analysis/normed_space/deriv): add readable proof of chain rule

28ce4b64

feat(analysis/normed_space/deriv): generalize to spaces over any norm…

fa6a3bfb

refactor(analysis/asymptotics): minor formatting changes

da399869

avigad merged 04b5f885 into master 6 years ago

Reviewers

kckennylau

sgouezel

jdsalchow

digama0

Assignees

digama0

Labels

None yet

Milestone

No milestone

mathlib3 asymptotics and the Fréchet derivative #748 Merged

asymptotics and the Fréchet derivative #748

mathlib3
asymptotics and the Fréchet derivative
#748

Merged