1. 1
2. 2
3. 3
4. 4
5. 5
6. 6
7. 7
8. 8
9. 9
10. 10
11. 11
12. 12
13. 13
14. 14
15. 15
16. 16
17. 17
18. 18
19. 19
20. 20
21. 21
22. 22
23. 23
24. 24
25. 25
26. 26
27. 27
28. 28
29. 29
30. 30
31. 31
32. 32
33. 33
34. 34
35. 35
36. 36
37. 37
38. 38
39. 39
40. 40
41. 41
42. 42
43. 43
44. 44
45. 45
46. 46
47. 47
48. 48
49. 49
50. 50
51. 51
52. 52
53. 53
54. 54
55. 55
56. 56
57. 57
58. 58
59. 59
60. 60
61. 61
62. 62
63. 63
64. 64
65. 65
66. 66
67. 67
68. 68
69. 69
70. 70
71. 71
72. 72
73. 73
74. 74
75. 75
76. 76
77. 77
78. 78
79. 79
80. 80
81. 81
82. 82
83. 83
84. 84
85. 85
86. 86
87. 87
88. 88
89. 89
90. 90
91. 91
92. 92
93. 93
94. 94
95. 95
96. 96
97. 97
98. 98
99. 99
100. 100
101. 101
102. 102
103. 103
104. 104
105. 105
106. 106
107. 107
108. 108
109. 109
110. 110
111. 111
112. 112
113. 113
114. 114
115. 115
116. 116
117. 117
118. 118
119. 119
120. 120
121. 121
122. 122
123. 123
124. 124
125. 125
126. 126
127. 127
128. 128
129. 129
130. 130
131. 131
132. 132
133. 133
134. 134
135. 135
136. 136
137. 137
138. 138
139. 139
140. 140
141. 141
142. 142
143. 143
144. 144
145. 145
146. 146
147. 147
148. 148
149. 149
150. 150
151. 151
152. 152
153. 153
154. 154
155. 155
156. 156
157. 157
158. 158
159. 159
160. 160
161. 161
162. 162
163. 163
164. 164
165. 165
166. 166
167. 167
168. 168
169. 169
170. 170
171. 171
172. 172
173. 173
174. 174
175. 175
176. 176
177. 177
178. 178
179. 179
180. 180
181. 181
182. 182
183. 183
184. 184
185. 185
186. 186
187. 187
188. 188
189. 189
190. 190
191. 191
192. 192
193. 193
194. 194
195. 195
196. 196
197. 197
198. 198
199. 199
200. 200
201. 201
202. 202
203. 203
204. 204
205. 205
206. 206
207. 207
208. 208
209. 209
210. 210
211. 211
212. 212
213. 213
214. 214
215. 215
216. 216
217. 217
218. 218
219. 219
220. 220
221. 221
222. 222
223. 223
224. 224
225. 225
226. 226
227. 227
228. 228
229. 229
230. 230
231. 231
232. 232
233. 233
234. 234
235. 235
236. 236
237. 237
238. 238
239. 239
240. 240
241. 241
242. 242
243. 243
244. 244
245. 245
246. 246
247. 247
248. 248
249. 249
250. 250
251. 251
252. 252
253. 253
254. 254
255. 255
256. 256
257. 257
258. 258
259. 259
260. 260
261. 261
262. 262
263. 263
264. 264
265. 265
266. 266
267. 267
268. 268
269. 269
270. 270
271. 271
272. 272
273. 273
274. 274
275. 275
276. 276
277. 277
278. 278
279. 279
280. 280
281. 281
282. 282
283. 283
284. 284
285. 285
286. 286
287. 287
288. 288
289. 289
290. 290
291. 291
292. 292
293. 293
294. 294
295. 295
296. 296
297. 297
298. 298
299. 299
300. 300
301. 301
302. 302
303. 303
304. 304
305. 305
306. 306
307. 307
308. 308
309. 309
310. 310
311. 311
312. 312
313. 313
314. 314
315. 315
316. 316
317. 317
318. 318
319. 319
320. 320
321. 321
322. 322
323. 323
324. 324
325. 325
326. 326
327. 327
328. 328
329. 329
330. 330
331. 331
332. 332
333. 333
334. 334
335. 335
336. 336
337. 337
338. 338
339. 339
340. 340
341. 341
342. 342
343. 343
344. 344
345. 345
346. 346
347. 347
348. 348
349. 349
350. 350
351. 351
352. 352
353. 353
354. 354
355. 355
356. 356
357. 357
358. 358
359. 359
360. 360
361. 361
362. 362
363. 363
364. 364
365. 365
366. 366
367. 367
368. 368
369. 369
370. 370
371. 371
372. 372
373. 373
374. 374
375. 375
376. 376
377. 377
378. 378
379. 379
380. 380
381. 381
382. 382
383. 383
384. 384
385. 385
386. 386
387. 387
388. 388
389. 389
390. 390
391. 391
392. 392
393. 393
394. 394
395. 395
396. 396
397. 397
398. 398
399. 399
400. 400
401. 401
402. 402
403. 403
404. 404
405. 405
406. 406
407. 407
408. 408
409. 409
410. 410
411. 411
412. 412
413. 413
414. 414
415. 415
416. 416
417. 417
418. 418
419. 419
420. 420
421. 421
422. 422
423. 423
424. 424
425. 425
426. 426
427. 427
428. 428
429. 429
430. 430
431. 431
432. 432
433. 433
434. 434
435. 435
436. 436
437. 437
438. 438
439. 439
440. 440
441. 441
442. 442
443. 443
444. 444
445. 445
446. 446
447. 447
448. 448
449. 449
450. 450
451. 451
452. 452
453. 453
454. 454
455. 455
456. 456
457. 457
458. 458
459. 459
460. 460
461. 461
462. 462
463. 463
464. 464
465. 465
466. 466
467. 467
468. 468
469. 469
470. 470
471. 471
472. 472
473. 473
474. 474
475. 475
476. 476
477. 477
478. 478
479. 479
480. 480
481. 481
482. 482
483. 483
484. 484

<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>12. Differential Calculus &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=b86133f3" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=e59714d7" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
      <script src="_static/jquery.js?v=5d32c60e"></script>
      <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
      <script src="_static/documentation_options.js?v=7048e04d"></script>
      <script src="_static/doctools.js?v=9bcbadda"></script>
      <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
      <script async="async" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="13. Integration and Measure Theory" href="C13_Integration_and_Measure_Theory.html" />
    <link rel="prev" title="11. Topology" href="C11_Topology.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul class="current">
<li class="toctree-l1"><a class="reference internal" href="C01_Introduction.html">1. Introduction</a></li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1 current"><a class="current reference internal" href="#">12. Differential Calculus</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#elementary-differential-calculus">12.1. Elementary Differential Calculus</a></li>
<li class="toctree-l2"><a class="reference internal" href="#differential-calculus-in-normed-spaces">12.2. Differential Calculus in Normed Spaces</a><ul>
<li class="toctree-l3"><a class="reference internal" href="#id3">12.2.1. Normed spaces</a></li>
<li class="toctree-l3"><a class="reference internal" href="#continuous-linear-maps">12.2.2. Continuous linear maps</a></li>
<li class="toctree-l3"><a class="reference internal" href="#asymptotic-comparisons">12.2.3. Asymptotic comparisons</a></li>
<li class="toctree-l3"><a class="reference internal" href="#differentiability">12.2.4. Differentiability</a></li>
</ul>
</li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active"><span class="section-number">12. </span>Differential Calculus</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C12_Differential_Calculus.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="index-0">
<span id="differential-calculus"></span><span id="id1"></span><h1><span class="section-number">12. </span>Differential Calculus<a class="headerlink" href="#index-0" title="Link to this heading">&#61633;</a></h1>
<p>We now consider the formalization of notions from <em>analysis</em>,
starting with differentiation in this chapter
and turning integration and measure theory in the next.
In <a class="reference internal" href="#elementary-differential-calculus"><span class="std std-numref">Section 12.1</span></a>, we stick with the
setting of functions from the real numbers to the real numbers,
which is familiar from any introductory calculus class.
In <a class="reference internal" href="#normed-spaces"><span class="std std-numref">Section 12.2</span></a>, we then consider the notion of a derivative in
a much broader setting.</p>
<section id="elementary-differential-calculus">
<span id="index-1"></span><span id="id2"></span><h2><span class="section-number">12.1. </span>Elementary Differential Calculus<a class="headerlink" href="#elementary-differential-calculus" title="Link to this heading">&#61633;</a></h2>
<p>Let <code class="docutils literal notranslate"><span class="pre">f</span></code> be a function from the reals to the reals. There is a difference
between talking about the derivative of <code class="docutils literal notranslate"><span class="pre">f</span></code> at a single point and
talking about the derivative function.
In Mathlib, the first notion is represented as follows.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Real</span>

<span class="sd">/-- The sin function has derivative 1 at 0. -/</span>
<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasDerivAt</span><span class="w"> </span><span class="n">sin</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simpa</span><span class="w"> </span><span class="n">using</span><span class="w"> </span><span class="n">hasDerivAt_sin</span><span class="w"> </span><span class="mi">0</span>
</pre></div>
</div>
<p>We can also express that <code class="docutils literal notranslate"><span class="pre">f</span></code> is differentiable at a point without
specifying its derivative there
by writing <code class="docutils literal notranslate"><span class="pre">DifferentiableAt</span> <span class="pre">&#8477;</span></code>.
We specify <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> explicitly because in a slightly more general context,
when talking about functions from <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code> to <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>,
we want to be able to distinguish between being differentiable in the real sense
and being differentiable in the sense of the complex derivative.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">DifferentiableAt</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">sin</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="o">(</span><span class="n">hasDerivAt_sin</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="bp">.</span><span class="n">differentiableAt</span>
</pre></div>
</div>
<p>It would be inconvenient to have to provide a proof of differentiability
every time we want to refer to a derivative.
So Mathlib provides a function <code class="docutils literal notranslate"><span class="pre">deriv</span> <span class="pre">f</span> <span class="pre">:</span> <span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code> that is defined for any
function <code class="docutils literal notranslate"><span class="pre">f</span> <span class="pre">:</span> <span class="pre">&#8477;</span> <span class="pre">&#8594;</span> <span class="pre">&#8477;</span></code>
but is defined to take the value <code class="docutils literal notranslate"><span class="pre">0</span></code> at any point where <code class="docutils literal notranslate"><span class="pre">f</span></code> is not differentiable.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">h.deriv</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#172;</span><span class="n">DifferentiableAt</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">deriv_zero_of_not_differentiableAt</span><span class="w"> </span><span class="n">h</span>
</pre></div>
</div>
<p>Of course there are many lemmas about <code class="docutils literal notranslate"><span class="pre">deriv</span></code> that do require differentiability assumptions.
For instance, you should think about a counterexample to the next lemma without the
differentiability assumptions.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">DifferentiableAt</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hg</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">DifferentiableAt</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">deriv</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">g</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">deriv_add</span><span class="w"> </span><span class="n">hf</span><span class="w"> </span><span class="n">hg</span>
</pre></div>
</div>
<p>Interestingly, however, there are statements that can avoid differentiability
assumptions by taking advantage
of the fact that the value of <code class="docutils literal notranslate"><span class="pre">deriv</span></code> defaults to zero when the function is
not differentiable.
So making sense of the following statement requires knowing the precise
definition of <code class="docutils literal notranslate"><span class="pre">deriv</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsLocalMin</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">h.deriv_eq_zero</span>
</pre></div>
</div>
<p>We can even state Rolle&#8217;s theorem without any differentiability assumptions, which
seems even weirder.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Set</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hab</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hfc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">ContinuousOn</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">Icc</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">))</span><span class="w"> </span><span class="o">(</span><span class="n">hfI</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">Ioo</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">,</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">exists_deriv_eq_zero</span><span class="w"> </span><span class="n">hab</span><span class="w"> </span><span class="n">hfc</span><span class="w"> </span><span class="n">hfI</span>
</pre></div>
</div>
<p>Of course, this trick does not work for the general mean value theorem.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hab</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">b</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">ContinuousOn</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">Icc</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">))</span>
<span class="w">    </span><span class="o">(</span><span class="n">hf&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">DifferentiableOn</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">Ioo</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">))</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">Ioo</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">b</span><span class="o">,</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">b</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="o">(</span><span class="n">b</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">exists_deriv_eq_slope</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">hab</span><span class="w"> </span><span class="n">hf</span><span class="w"> </span><span class="n">hf&#39;</span>
</pre></div>
</div>
<p>Lean can automatically compute some simple derivatives using the <code class="docutils literal notranslate"><span class="pre">simp</span></code> tactic.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">5</span><span class="o">)</span><span class="w"> </span><span class="mi">6</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">5</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="mi">6</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">deriv</span><span class="w"> </span><span class="n">sin</span><span class="w"> </span><span class="n">&#960;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">-</span><span class="mi">1</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">simp</span>
</pre></div>
</div>
</section>
<section id="differential-calculus-in-normed-spaces">
<span id="normed-spaces"></span><span id="index-2"></span><h2><span class="section-number">12.2. </span>Differential Calculus in Normed Spaces<a class="headerlink" href="#differential-calculus-in-normed-spaces" title="Link to this heading">&#61633;</a></h2>
<section id="id3">
<h3><span class="section-number">12.2.1. </span>Normed spaces<a class="headerlink" href="#id3" title="Link to this heading">&#61633;</a></h3>
<p>Differentiation can be generalized beyond <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> using the notion of a
<em>normed vector space</em>, which encapsulates both direction and distance.
We start with the notion of a <em>normed group</em>, which is an additive commutative
group equipped with a real-valued norm function
satisfying the following conditions.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">norm_nonneg</span><span class="w"> </span><span class="n">x</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">}</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">norm_eq_zero</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">y</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">norm_add_le</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>
</pre></div>
</div>
<p>Every normed space is a metric space with distance function
<span class="math notranslate nohighlight">\(d(x, y) = \| x - y \|\)</span>, and hence it is also a topological space.
Lean and Mathlib know this.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">MetricSpace</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">infer_instance</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">X</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">TopologicalSpace</span><span class="w"> </span><span class="n">X</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">X</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Continuous</span><span class="w"> </span><span class="n">f</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">Continuous</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hf.norm</span>
</pre></div>
</div>
<p>In order to use the notion of a norm with concepts from linear algebra,
we add the assumption <code class="docutils literal notranslate"><span class="pre">NormedSpace</span> <span class="pre">&#8477;</span> <span class="pre">E</span></code> on top of <code class="docutils literal notranslate"><span class="pre">NormedAddGroup</span> <span class="pre">E</span></code>.
This stipulates that <code class="docutils literal notranslate"><span class="pre">E</span></code> is a vector space over <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> and that
scalar multiplication satisfies the following condition.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">|</span><span class="n">a</span><span class="bp">|</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">norm_smul</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p>A complete normed space is known as a <em>Banach space</em>.
Every finite-dimensional vector space is complete.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">&#8477;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">infer_instance</span>
</pre></div>
</div>
<p>In all the previous examples, we used the real numbers as the base field.
More generally, we can make sense of calculus with a vector space over any
<em>nontrivially normed field</em>. These are fields that are equipped with a
real-valued norm that is multiplicative and has the property that
not every element has norm zero or one
(equivalently, there is an element whose norm is bigger than one).</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">y</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">norm_mul</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">NormedField.exists_one_lt_norm</span><span class="w"> </span><span class="n">&#120156;</span>
</pre></div>
</div>
<p>A finite-dimensional vector space over a nontrivially normed field is
complete as long as the field itself is complete.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">)</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>
<span class="w">    </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">FiniteDimensional</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">FiniteDimensional.complete</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span>
</pre></div>
</div>
</section>
<section id="continuous-linear-maps">
<h3><span class="section-number">12.2.2. </span>Continuous linear maps<a class="headerlink" href="#continuous-linear-maps" title="Link to this heading">&#61633;</a></h3>
<p>We now turn to the morphisms in the category of normed spaces, namely,
continuous linear maps.
In Mathlib, the type of <code class="docutils literal notranslate"><span class="pre">&#120156;</span></code>-linear continuous maps between normed spaces
<code class="docutils literal notranslate"><span class="pre">E</span></code> and <code class="docutils literal notranslate"><span class="pre">F</span></code> is written <code class="docutils literal notranslate"><span class="pre">E</span> <span class="pre">&#8594;L[&#120156;]</span> <span class="pre">F</span></code>.
They are implemented as <em>bundled maps</em>, which means that an element of this type
a structure that that includes the function itself and the properties
of being linear and continuous.
Lean will insert a coercion so that a continuous linear map can be treated
as a function.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>
<span class="w">  </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">F</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">ContinuousLinearMap.id</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Continuous</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.cont</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.map_add</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="bp">&#8226;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.map_smul</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">x</span>
</pre></div>
</div>
<p>Continuous linear maps have an operator norm that is characterized by the
following properties.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.le_opNorm</span><span class="w"> </span><span class="n">x</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">M</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">hMp</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">M</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hM</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">x</span><span class="bp">&#8214;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">M</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">f.opNorm_le_bound</span><span class="w"> </span><span class="n">hMp</span><span class="w"> </span><span class="n">hM</span>
</pre></div>
</div>
<p>There is also a notion of bundled continuous linear <em>isomorphism</em>.
Their type of such isomorphisms is <code class="docutils literal notranslate"><span class="pre">E</span> <span class="pre">&#8771;L[&#120156;]</span> <span class="pre">F</span></code>.</p>
<p>As a challenging exercise, you can prove the Banach-Steinhaus theorem, also
known as the Uniform Boundedness Principle.
The principle states that a family of continuous linear maps from a Banach space
into a normed space is pointwise
bounded, then the norms of these linear maps are uniformly bounded.
The main ingredient is Baire&#8217;s theorem
<code class="docutils literal notranslate"><span class="pre">nonempty_interior_of_iUnion_of_closed</span></code>. (You proved a version of this in the topology chapter.)
Minor ingredients include <code class="docutils literal notranslate"><span class="pre">continuous_linear_map.opNorm_le_of_shell</span></code>,
<code class="docutils literal notranslate"><span class="pre">interior_subset</span></code> and <code class="docutils literal notranslate"><span class="pre">interior_iInter_subset</span></code> and <code class="docutils literal notranslate"><span class="pre">isClosed_le</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>
<span class="w">  </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">F</span><span class="o">]</span>

<span class="kn">open</span><span class="w"> </span><span class="n">Metric</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#953;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">(</span><span class="n">h</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">C</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">g</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">C</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">C&#39;</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">i</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">g</span><span class="w"> </span><span class="n">i</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">C&#39;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="c1">-- sequence of subsets consisting of those `x : E` with norms `&#8214;g i x&#8214;` bounded by `n`</span>
<span class="w">  </span><span class="k">let</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Set</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="bp">&#8898;</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">,</span><span class="w"> </span><span class="o">{</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">|</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">g</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">}</span>
<span class="w">  </span><span class="c1">-- each of these sets is closed</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">hc</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">IsClosed</span><span class="w"> </span><span class="o">(</span><span class="n">e</span><span class="w"> </span><span class="n">n</span><span class="o">)</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="w">  </span><span class="c1">-- the union is the entire space; this is where we use `h`</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">hU</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="o">(</span><span class="bp">&#8899;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">e</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">univ</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="w">  </span><span class="c">/-</span><span class="cm"> apply the Baire category theorem to conclude that for some `m : &#8469;`,</span>
<span class="cm">       `e m` contains some `x` -/</span>
<span class="w">  </span><span class="n">obtain</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">hx</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">m</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">x</span><span class="o">,</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">interior</span><span class="w"> </span><span class="o">(</span><span class="n">e</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">obtain</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">&#949;</span><span class="o">,</span><span class="w"> </span><span class="n">&#949;_pos</span><span class="o">,</span><span class="w"> </span><span class="n">h&#949;</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">&#949;</span><span class="w"> </span><span class="bp">&gt;</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="n">ball</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">&#949;</span><span class="w"> </span><span class="bp">&#8838;</span><span class="w"> </span><span class="n">interior</span><span class="w"> </span><span class="o">(</span><span class="n">e</span><span class="w"> </span><span class="n">m</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">obtain</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">hk</span><span class="o">&#10217;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">,</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">k</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="c1">-- show all elements in the ball have norm bounded by `m` after applying any `g i`</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">real_norm_le</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8712;</span><span class="w"> </span><span class="n">ball</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">&#949;</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="o">(</span><span class="n">i</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#953;</span><span class="o">),</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">g</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="n">z</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">m</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">&#949;k_pos</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">&#949;</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">k</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="gr">sorry</span>
<span class="w">  </span><span class="n">refine</span><span class="w"> </span><span class="o">&#10216;(</span><span class="n">m</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="o">(</span><span class="n">&#949;</span><span class="w"> </span><span class="bp">/</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">k</span><span class="bp">&#8214;</span><span class="o">),</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">i</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">ContinuousLinearMap.opNorm_le_of_shell</span><span class="w"> </span><span class="n">&#949;_pos</span><span class="w"> </span><span class="bp">?</span><span class="n">_</span><span class="w"> </span><span class="n">hk</span><span class="w"> </span><span class="bp">?</span><span class="n">_</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="gr">sorry</span>
<span class="w">  </span><span class="gr">sorry</span>
</pre></div>
</div>
</section>
<section id="asymptotic-comparisons">
<h3><span class="section-number">12.2.3. </span>Asymptotic comparisons<a class="headerlink" href="#asymptotic-comparisons" title="Link to this heading">&#61633;</a></h3>
<p>Defining differentiability also requires asymptotic comparisons.
Mathlib has an extensive library covering the big O and little o relations,
whose definitions are shown below.
Opening the <code class="docutils literal notranslate"><span class="pre">asymptotics</span></code> locale allows us to use the corresponding
notation.
Here we will only use little o to define differentiability.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Asymptotics</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">c</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8477;</span><span class="o">)</span>
<span class="w">    </span><span class="o">(</span><span class="n">l</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Filter</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">IsBigOWith</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="n">l</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8704;&#7584;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">l</span><span class="o">,</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">c</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="bp">&#8214;</span><span class="n">g</span><span class="w"> </span><span class="n">x</span><span class="bp">&#8214;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">isBigOWith_iff</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span>
<span class="w">    </span><span class="o">(</span><span class="n">l</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Filter</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="n">O</span><span class="o">[</span><span class="n">l</span><span class="o">]</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">C</span><span class="o">,</span><span class="w"> </span><span class="n">IsBigOWith</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">l</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">isBigO_iff_isBigOWith</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span>
<span class="w">    </span><span class="o">(</span><span class="n">l</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Filter</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">=</span><span class="n">o</span><span class="o">[</span><span class="n">l</span><span class="o">]</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="bp">&gt;</span><span class="w"> </span><span class="mi">0</span><span class="o">,</span><span class="w"> </span><span class="n">IsBigOWith</span><span class="w"> </span><span class="n">C</span><span class="w"> </span><span class="n">l</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">isLittleO_iff_forall_isBigOWith</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#945;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">(</span><span class="n">l</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Filter</span><span class="w"> </span><span class="n">&#945;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#945;</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">f</span><span class="w"> </span><span class="bp">~</span><span class="o">[</span><span class="n">l</span><span class="o">]</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">g</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="n">o</span><span class="o">[</span><span class="n">l</span><span class="o">]</span><span class="w"> </span><span class="n">g</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">Iff.rfl</span>
</pre></div>
</div>
</section>
<section id="differentiability">
<h3><span class="section-number">12.2.4. </span>Differentiability<a class="headerlink" href="#differentiability" title="Link to this heading">&#61633;</a></h3>
<p>We are now ready to discuss differentiable functions between normed spaces.
In analogy the elementary one-dimensional,
Mathlib defines a predicate <code class="docutils literal notranslate"><span class="pre">HasFDerivAt</span></code> and a function <code class="docutils literal notranslate"><span class="pre">fderiv</span></code>.
Here the letter
&#8220;f&#8221; stands for <em>Fr&#233;chet</em>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">open</span><span class="w"> </span><span class="n">Topology</span>

<span class="kd">variable</span><span class="w"> </span><span class="o">{</span><span class="n">&#120156;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NontriviallyNormedField</span><span class="w"> </span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span>
<span class="w">  </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">F</span><span class="o">]</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">HasFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">x&#8320;</span><span class="w"> </span><span class="bp">&#8596;</span><span class="w"> </span><span class="o">(</span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x&#8320;</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">x&#8320;</span><span class="o">))</span><span class="w"> </span><span class="bp">=</span><span class="n">o</span><span class="o">[</span><span class="n">&#120029;</span><span class="w"> </span><span class="n">x&#8320;</span><span class="o">]</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">-</span><span class="w"> </span><span class="n">x&#8320;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hasFDerivAtFilter_iff_isLittleO</span><span class="w"> </span><span class="bp">..</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">x&#8320;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hff&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">x&#8320;</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">fderiv</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x&#8320;</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hff&#39;.fderiv</span>
</pre></div>
</div>
<p>We also have iterated derivatives that take values in the type of multilinear maps
<code class="docutils literal notranslate"><span class="pre">E</span> <span class="pre">[&#215;n]&#8594;L[&#120156;]</span> <span class="pre">F</span></code>,
and we have continuously differential functions.
The type <code class="docutils literal notranslate"><span class="pre">&#8469;&#8734;</span></code> is <code class="docutils literal notranslate"><span class="pre">&#8469;</span></code> with an additional element <code class="docutils literal notranslate"><span class="pre">&#8734;</span></code> that
is bigger than every natural number.
So <span class="math notranslate nohighlight">\(\mathcal{C}^\infty\)</span> functions are functions <code class="docutils literal notranslate"><span class="pre">f</span></code> that satisfy
<code class="docutils literal notranslate"><span class="pre">ContDiff</span> <span class="pre">&#120156;</span> <span class="pre">&#8868;</span> <span class="pre">f</span></code>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="o">[</span><span class="bp">&#215;</span><span class="n">n</span><span class="o">]</span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">iteratedFDeriv</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">f</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="bp">&#8734;</span><span class="o">)</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">ContDiff</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="bp">&#8596;</span>
<span class="w">      </span><span class="o">(</span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">WithTop</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Continuous</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">iteratedFDeriv</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">&#8743;</span>
<span class="w">        </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">WithTop</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="bp">&lt;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Differentiable</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="n">iteratedFDeriv</span><span class="w"> </span><span class="n">&#120156;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">contDiff_iff_continuous_differentiable</span>
</pre></div>
</div>
<p>The differentiability parameter in <code class="docutils literal notranslate"><span class="pre">ContDiff</span></code> can also take value <code class="docutils literal notranslate"><span class="pre">&#969;</span> <span class="pre">:</span> <span class="pre">WithTop</span> <span class="pre">&#8469;&#8734;</span></code>
to denote analytic functions.</p>
<p>There is a stricter notion of differentiability called
<code class="docutils literal notranslate"><span class="pre">HasStrictFDerivAt</span></code>, which is used in the statement
of the inverse function theorem and the statement of the implicit function
theorem, both of which are in Mathlib.
Over <code class="docutils literal notranslate"><span class="pre">&#8477;</span></code> or <code class="docutils literal notranslate"><span class="pre">&#8450;</span></code>, continuously differentiable
functions are strictly differentiable.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">&#120130;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">RCLike</span><span class="w"> </span><span class="n">&#120130;</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">E</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span><span class="w"> </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120130;</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">F</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="kt">Type</span><span class="bp">*</span><span class="o">}</span>
<span class="w">    </span><span class="o">[</span><span class="n">NormedAddCommGroup</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">[</span><span class="n">NormedSpace</span><span class="w"> </span><span class="n">&#120130;</span><span class="w"> </span><span class="n">F</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">WithTop</span><span class="w"> </span><span class="n">&#8469;</span><span class="bp">&#8734;</span><span class="o">}</span>
<span class="w">    </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">ContDiffAt</span><span class="w"> </span><span class="n">&#120130;</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">hn</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">1</span><span class="w"> </span><span class="bp">&#8804;</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasStrictFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">fderiv</span><span class="w"> </span><span class="n">&#120130;</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hf.hasStrictFDerivAt</span><span class="w"> </span><span class="n">hn</span>
</pre></div>
</div>
<p>The local inverse theorem is stated using an operation that produces an
inverse function from a
function and the assumptions that the function is strictly differentiable at a
point <code class="docutils literal notranslate"><span class="pre">a</span></code> and that its derivative is an isomorphism.</p>
<p>The first example below gets this local inverse.
The next one states that it is indeed a local inverse
from the left and from the right, and that it is strictly differentiable.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kn">section</span><span class="w"> </span><span class="n">LocalInverse</span>
<span class="kd">variable</span><span class="w"> </span><span class="o">[</span><span class="n">CompleteSpace</span><span class="w"> </span><span class="n">E</span><span class="o">]</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8771;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">}</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasStrictFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">HasStrictFDerivAt.localInverse</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">hf</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasStrictFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8704;&#7584;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">&#120029;</span><span class="w"> </span><span class="n">a</span><span class="o">,</span><span class="w"> </span><span class="n">hf.localInverse</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hf.eventually_left_inverse</span>

<span class="kd">example</span><span class="w"> </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasStrictFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="bp">&#8704;&#7584;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="k">in</span><span class="w"> </span><span class="n">&#120029;</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="o">),</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">hf.localInverse</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">x</span><span class="o">)</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">hf.eventually_right_inverse</span>

<span class="kd">example</span><span class="w"> </span><span class="o">{</span><span class="n">f</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8771;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">}</span><span class="w"> </span><span class="o">{</span><span class="n">a</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="o">}</span>
<span class="w">  </span><span class="o">(</span><span class="n">hf</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">HasStrictFDerivAt</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">E</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">F</span><span class="o">)</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:</span>
<span class="w">    </span><span class="n">HasStrictFDerivAt</span><span class="w"> </span><span class="o">(</span><span class="n">HasStrictFDerivAt.localInverse</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="n">f&#39;</span><span class="w"> </span><span class="n">a</span><span class="w"> </span><span class="n">hf</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f&#39;.symm</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">F</span><span class="w"> </span><span class="bp">&#8594;</span><span class="n">L</span><span class="o">[</span><span class="n">&#120156;</span><span class="o">]</span><span class="w"> </span><span class="n">E</span><span class="o">)</span><span class="w"> </span><span class="o">(</span><span class="n">f</span><span class="w"> </span><span class="n">a</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">HasStrictFDerivAt.to_localInverse</span><span class="w"> </span><span class="n">hf</span>

<span class="kd">end</span><span class="w"> </span><span class="n">LocalInverse</span>
</pre></div>
</div>
<p>This has been only a quick tour of the differential calculus in Mathlib.
The library contains many variations that we have not discussed.
For example, you may want to use one-sided derivatives in the
one-dimensional setting. The means to do so are found in Mathlib in a more
general context;
see <code class="docutils literal notranslate"><span class="pre">HasFDerivWithinAt</span></code> or the even more general <code class="docutils literal notranslate"><span class="pre">HasFDerivAtFilter</span></code>.</p>
</section>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="C11_Topology.html" class="btn btn-neutral float-left" title="11. Topology" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C13_Integration_and_Measure_Theory.html" class="btn btn-neutral float-right" title="13. Integration and Measure Theory" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>