/
undergrad.yaml
662 lines (649 loc) · 26.4 KB
/
undergrad.yaml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
# The list of topics was originally gathered from
# http://media.devenirenseignant.gouv.fr/file/agreg_externe/59/7/p2020_agreg_ext_maths_1107597.pdf
# 1.
Linear algebra:
Fundamentals:
vector space: 'vector_space'
product of vector spaces: 'prod.semimodule'
vector subspace: 'subspace'
quotient space: 'submodule.quotient'
sum of subspaces: 'submodule.complete_lattice'
direct sum: '' # this is supposed to be the internal direct sum
complementary subspaces: 'submodule.exists_is_compl'
linear independence: 'linear_independent'
generating sets: 'submodule.span'
bases: 'is_basis'
existence of bases: 'exists_is_basis'
linear map: 'linear_map'
range of a linear map: 'linear_map.range'
kernel of a linear map: 'linear_map.ker'
algebra of endomorphisms of a vector space: 'module.endomorphism_algebra'
general linear group: 'linear_map.general_linear_group'
Duality:
dual vector space: 'module.dual'
dual basis: 'is_basis.dual_basis'
transpose of a linear map: 'module.dual.transpose'
orthogonality: ''
Finite-dimensional vector spaces:
finite-dimensionality : 'finite_dimensional'
isomorphism with $K^n$: 'module_equiv_finsupp'
rank of a linear map: 'rank'
rank of a set of vectors: ''
rank of a system of linear equations: ''
isomorphism with bidual: 'vector_space.eval_equiv'
Multilinearity:
multilinear map: 'multilinear_map'
determinant of vectors: 'is_basis.det'
determinant of endomorphisms: ''
special linear group: ''
orientation of a $\R$-valued vector space: ''
Matrices:
commutative-ring-valued matrices: 'matrix'
field-valued matrices: 'matrix'
matrix representation of a linear map: 'linear_map.to_matrix'
change of basis: ''
rank of a matrix: ''
determinant: 'matrix.det'
invertibility: 'matrix.nonsing_inv'
elementary row operations: ''
elementary column operations: ''
Gaussian elimination: ''
row-reduced matrices: ''
Endomorphism polynomials:
annihilating polynomials: ''
minimal polynomial: 'minpoly'
characteristic polynomial: 'char_poly'
Cayley-Hamilton theorem: 'aeval_self_char_poly'
Structure theory of endomorphisms:
eigenvalue: 'module.End.has_eigenvalue'
eigenvector: 'module.End.has_eigenvector'
diagonalization: ''
triangularization: ''
invariant subspaces of an endomorphism: ''
generalized eigenspaces: 'module.End.generalized_eigenspace'
kernels lemma: ''
Dunford decomposition: ''
Jordan normal form: ''
Linear representations:
irreducible representation: ''
Schur's lemma: ''
examples: ''
Exponential:
endomorphism exponential: ''
matrix exponential: ''
# 2.
Group Theory:
Basic definitions:
group: 'group'
group morphism: 'monoid_hom'
direct product of groups: 'prod.group'
subgroup: 'subgroup'
subgroup generated by a subset: 'subgroup.closure'
order of an element: 'group_theory/order_of_element.html'
normal subgroup: 'normal_subgroup'
quotient group: 'quotient_group.quotient.group'
group action: 'mul_action'
stabilizer of a point: 'mul_action.stabilizer'
orbit: 'mul_action.orbit'
quotient space: 'mul_action.orbit_equiv_quotient_stabilizer'
class formula: ''
conjugacy classes: 'conj_classes'
Abelian group:
cyclic group: 'is_cyclic'
finite type abelian groups: ''
complex roots of unity: 'complex.mem_roots_of_unity'
primitive complex roots of unity: 'complex.is_primitive_root_iff'
Permutation group:
permutation group of a type: 'equiv.perm'
decomposition into transpositions: 'equiv.perm.trunc_swap_factors'
decomposition into cycles with disjoint support: 'equiv.perm.trunc_cycle_factors'
signature: 'equiv.perm.sign'
alternating group: 'alternating_subgroup'
Classical automorphism groups:
general linear group: 'linear_map.general_linear_group'
special linear group: 'matrix.special_linear_group'
orthogonal group: 'matrix.orthogonal_group '
special orthogonal group: ''
unitary group: 'matrix.unitary_group'
special unitary group: ''
Representation theory of finite groups:
representations of abelian groups: ''
dual groups: ''
Maschke theorem: ''
orthogonality of irreducible characters: ''
Fourier transform for finite abelian groups: ''
convolution: ''
class function over a group: ''
characters of a finite dimensional representation: ''
orthonormal basis of irreducible characters: ''
examples of groups with small cardinality: ''
# 3.
Ring Theory:
Fundamentals:
ring: 'ring'
subrings: 'is_subring'
ring morphisms: 'ring_hom'
ring structure $\Z$: 'int.comm_ring'
product of rings: 'pi.ring'
Ideals and Quotients:
ideal of a commutative ring: 'ideal'
quotient rings: 'ideal.quotient'
prime ideals: 'ideal.is_prime'
maximal ideals: 'ideal.is_maximal'
Chinese remainder theorem: 'ideal.quotient_inf_ring_equiv_pi_quotient'
Algebra:
algebra over a commutative ring:
associative algebra over a commutative ring: 'algebra'
Divisibility in integral domains:
irreducible elements: 'irreducible'
invertible elements: 'invertible'
coprime elements: 'is_coprime'
unique factorisation domain (UFD): 'unique_factorization_monoid'
greatest common divisor: 'gcd_monoid.gcd'
least common multiple: 'gcd_monoid.lcm'
$A[X]$ is a UFD when $A$ is a UFD: 'polynomial.unique_factorization_monoid'
principal ideal domain: 'submodule.is_principal'
Euclidean rings: 'euclidean_domain'
Euclid's' algorithm: 'nat.xgcd'
$\Z$ is a euclidean ring: 'int.euclidean_domain'
congruence in $\Z$: 'int.modeq'
prime numbers: 'prime'
Bezout's identity: '' # todo: prove this for PIDs https://en.wikipedia.org/wiki/B%C3%A9zout%27s_identity
$\Z/n\Z$ and its invertible elements: 'zmod.unit_of_coprime'
Euler's totient function ($\varphi$): 'nat.totient'
Polynomial rings:
$K[X]$ is a euclidean ring when $K$ is a field: 'polynomial.euclidean_domain'
irreducible polynomial: 'irreducible'
cyclotomic polynomials in $\Q[X]$: polynomial.cyclotomic'
Eisenstein's criterion: 'polynomial.irreducible_of_eisenstein_criterion'
polynomial algebra in one or several indeterminates over a commutative ring: 'mv_polynomial'
roots of a polynomial: 'polynomial.roots'
multiplicity: 'polynomial.root_multiplicity'
relationship between the coefficients and the roots of a split polynomial:
Newton's identities:
polynomial derivative: 'polynomial.derivative'
decomposition into sums of homogeneous polynomials: 'mv_polynomial.sum_homogeneous_component'
symmetric polynomials: 'mv_polynomial.is_symmetric'
Field Theory:
fields: 'field'
characteristic of a ring: 'ring_char'
characteristic zero: 'char_zero'
characteristic p: 'char_p'
Subfields: 'field_theory/subfield.html'
Frobenius morphisms: 'frobenius'
field $\Q$ of rational numbers: 'rat.division_ring'
field $\R$ of real numbers: 'real.division_ring'
field $\C$ of complex numbers: 'complex.field'
$\C$ is algebraically closed: 'complex.exists_root'
field of fractions of an integral domain: 'fraction_map'
algebraic elements: 'is_algebraic'
transcendental elements:
algebraic extensions: 'algebra.is_algebraic'
algebraically closed fields: 'is_alg_closed'
rupture fields: 'adjoin_root'
splitting fields: 'polynomial.splitting_field'
finite fields: 'field_theory/finite.html'
rational fraction fields with one indeterminate over a field:
$\R(X)$-partial fraction decomposition:
$\C(X)$-partial fraction decomposition:
# 4.
Bilinear and Quadratic Forms Over a Vector Space:
Bilinear forms:
bilinear forms: 'bilin_form'
alternating bilinear forms: 'alt_bilin_form.is_alt'
symmetric bilinear forms: 'sym_bilin_form.is_sym'
nondegenerate forms: 'bilin_form.nondegenerate'
matrix representation: 'bilin_form.to_matrix'
change of coordinates: 'bilin_form.to_matrix_comp'
rank of a bilinear form:
Quadratic forms:
quadratic form: 'quadratic_form'
polar form of a quadratic: 'quadratic_form.polar'
Orthogonality:
orthogonal elements: 'bilin_form.is_ortho'
adjoint endomorphism: 'bilin_form.left_adjoint_of_nondegenerate'
Sylvester's law of inertia:
real classification:
complex classification:
Gram-Schmidt orthogonalisation:
Euclidean and Hermitian spaces:
Euclidean vector spaces: 'inner_product_space'
Hermitian vector spaces: 'inner_product_space'
dual isomorphism in the euclidean case: 'inner_product_space.isometric.to_dual'
orthogonal complement: 'submodule.orthogonal'
Cauchy-Schwarz inequality: 'inner_mul_inner_self_le'
norm: 'inner_product_space.of_core.to_has_norm'
orthonormal bases: 'maximal_orthonormal_iff_is_basis_of_finite_dimensional'
Endomorphisms:
orthogonal group:
unitary group:
special orthogonal group:
special unitary group:
self-adjoint endomorphism: 'bilin_form.is_self_adjoint'
normal endomorphism:
diagonalization of a self-adjoint endomorphism:
diagonalization of normal endomorphisms:
simultaneous diagonalization of two real quadratic forms, with one positive-definite:
decomposition of an orthogonal transformation as a product of reflections:
polar decompositions in $\mathrm{GL}(n, \R)$:
polar decompositions in $\mathrm{GL}(n, \C)$:
Low dimensions:
cross product:
triple product:
classification of elements of $\mathrm{O}(2, \R)$:
classification of elements of $\mathrm{O}(3, \R)$:
# 5.
Affine and Euclidean Geometry:
General definitions:
affine space: 'add_torsor'
affine function: 'affine_map'
affine subspace: 'affine_subspace'
barycenter: 'finset.affine_combination'
affine span: 'span_points'
equations of affine subspace:
affine groups:
affine property:
group generated by homotheties and translations:
transformations fixing a basis of directions: # "affinité", no good English translation
Convexity:
convex subsets:
convex hull of a subset of an affine real space:
extreme point:
Euclidean affine spaces:
isometries of a Euclidean affine space:
group of isometries of a Euclidean affine space:
isometries that do and do not preserve orientation:
direct and opposite similarities of the plane:
classification of isometries in two and three dimensions:
angles between vectors: 'inner_product_geometry.angle'
angles between planes:
inscribed angle theorem:
cocyclicity:
group of isometries stabilizing a subset of the plane or of space:
regular polygons:
metric relations in the triangle:
using complex numbers in plane geometry:
Application of quadratic forms to study proper conic sections of the affine euclidean plane:
focus:
eccentricity:
quadric surfaces in 3-dimensional Euclidean affine spaces:
# 6.
Single Variable Real Analysis:
Real numbers:
definition of $\R$: 'real'
field structure: 'real.division_ring'
order: 'real.linear_order'
Sequences of real numbers:
convergence: 'filter.tendsto'
limit point: 'map_cluster_pt'
recurrent sequences: 'nat'
limit infimum and supremum: 'order/liminf_limsup.html'
Cauchy sequences: 'cauchy_seq'
Topology of R:
metric structure: 'real.metric_space'
completeness of R: 'real.complete_space'
Bolzano-Weierstrass theorem: 'tendsto_subseq_of_bounded'
compact subsets of $\R$: 'metric.compact_iff_closed_bounded'
connected subsets of $\R$: 'set_of_is_preconnected_eq_of_ordered'
additive subgroups of $\R$: 'real.subgroup_dense_or_cyclic'
Numerical series:
Convergence of real valued-series:
Geometric series: 'tsum_geometric_of_norm_lt_1'
convergence of $p$-series for $p>1$: 'nnreal.summable_one_rpow_inv'
positive valued series:
summation of comparison relations:
comparison of a series and an integral:
error estimation:
absolute convergence:
products of series:
alternating series:
Real-valued functions defined on a subset of $\R$:
continuity: 'continuous'
limits: 'filter.tendsto'
intermediate value theorem: 'intermediate_value_Icc'
image of a segment: 'real.image_Icc'
continuity of monotonic functions: 'order_iso.continuous'
continuity of inverse functions: 'order_iso.to_homeomorph'
Differentiability:
derivative at a point: 'has_deriv_at'
differentiable functions: 'has_deriv_at'
derivative of a composition of functions: 'deriv.comp'
derivative of the inverse of a function: 'has_strict_deriv_at.of_local_left_inverse'
Rolle's theorem: 'exists_deriv_eq_zero'
mean value theorem: 'exists_ratio_deriv_eq_ratio_slope'
higher order derivatives of functions: 'iterated_deriv'
$C^k$ functions: 'times_cont_diff'
piecewise $C^k$ functions:
Leibniz formula: 'deriv_mul'
Taylor-like theorems:
Taylor's theorem with little-o remainder:
Taylor's theorem with integral form for remainder:
Taylor's theorem with Lagrange form for remainder:
Taylor series expansions:
Elementary functions (trigonometric, rational, $\exp$, $\log$, etc):
polynomial functions: 'polynomial.eval'
rational functions:
logarithms: 'real.log'
exponential: 'real.exp'
power functions: 'real.rpow'
trigonometric functions: 'real.sin'
hyperbolic trigonometric functions: 'real.sinh'
inverse trigonometric functions: 'real.arcsin'
inverse hyperbolic trigonometric functions: 'real.arsinh'
Integration:
integral over a segment of piecewise continuous functions:
antiderivatives:
Riemann sums:
antiderivative of a continuous function: 'interval_integral.integral_has_strict_deriv_at_of_tendsto_ae_right'
change of variable:
integration by parts: 'interval_integral.integral_mul_deriv_eq_deriv_mul'
improper integrals:
absolute vs conditional convergence of improper integrals:
comparison test for improper integrals:
Sequences and series of functions:
pointwise convergence:
uniform convergence: 'tendsto_uniformly'
normal convergence:
continuity of the limit: 'continuous_of_uniform_approx_of_continuous'
differentiability of the limit:
Weierstrass polynomial approximation theorem:
Weierstrass trigonometric approximation theorem:
Convexity:
convex functions of a real variable: 'convex_on'
continuity and differentiability of convex functions:
characterizations of convexity: 'convex_on_of_deriv2_nonneg'
convexity inequalities: 'analysis/mean_inequalities.html'
# 7.
Single Variable Complex Analysis:
Complex Valued series:
radius of convergence: 'formal_multilinear_series.radius'
# properties of sums of complex valued series on their disks of convergence: (this is a heading?)
continuity: 'has_fpower_series_on_ball.continuous_on'
differentiability with respect to the complex variable: 'has_fpower_series_on_ball.differentiable_on'
antiderivative:
complex exponential: 'complex.exp'
extension of trigonometric functions to the complex plane: 'complex.sin'
power series expansion of elementary functions:
Functions on one complex variable:
holomorphic functions:
Cauchy-Riemann conditions:
contour integrals of continuous functions in $\C$:
antiderivatives of a holomorphic function:
representations of the $\log$ function on $\C$:
theorem of holomorphic functions under integral domains:
winding number of a closed curve in $\C$ with respect to a point:
Cauchy formulas:
analyticity of a holomorphic function:
principle of isolated zeros:
principle of analytic continuation:
maximum principle:
isolated singularities:
Laurent series:
meromorphic functions:
residue theorem:
sequences and series of holomorphic functions:
holomorphic stability under uniform convergence:
# 8.
Topology:
Topology and Metric Spaces:
topology of a metric space: 'metric.is_open_iff'
induced topology: 'topological_space.induced'
finite product of metric spaces: 'metric_space_pi'
limits of sequences: 'metric.tendsto_at_top'
cluster points: 'cluster_pt'
continuous functions: 'continuous'
homeomorphisms: 'homeomorph'
compactness in terms of open covers (Borel-Lebesgue): 'compact_iff_finite_subcover'
sequential compactness is equivalent to compactness (Bolzano-Weierstrass): 'metric.compact_iff_seq_compact'
connectedness: 'connected_space'
connected components: 'connected_component'
path connectedness: 'is_path_connected'
Lipschitz functions: 'lipschitz_with'
uniformly continuous functions: 'metric.uniform_continuous_iff'
Heine-Cantor theorem: 'compact_space.uniform_continuous_of_continuous'
complete metric spaces: 'metric.complete_of_cauchy_seq_tendsto'
contraction mapping theorem: 'contracting_with.exists_fixed_point'
Normed vector spaces on $\R$ and $\C$:
topology on a normed vector space: 'semi_normed_space.has_continuous_smul'
equivalent norms:
Banach open mapping theorem: 'open_mapping'
equivalence of norms in finite dimension: 'linear_equiv.to_continuous_linear_equiv'
norms $\lVert\cdot\rVert_p$ on $\R^n$ and $\C^n$: 'pi_Lp.normed_space'
absolutely convergent series in Banach spaces: 'summable_of_summable_norm'
continuous linear maps: 'continuous_linear_map'
norm of a continuous linear map: 'linear_map.mk_continuous'
uniform convergence norm (sup-norm): 'emetric.tendsto_uniformly_on_iff'
normed space of bounded continuous normed-space-valued functions: 'bounded_continuous_function.normed_space'
its completeness: 'bounded_continuous_function.complete_space'
Heine-Borel theorem (closed bounded subsets are compact in finite dimension): 'finite_dimensional.proper'
Riesz' lemma (unit-ball characterization of finite dimension):
Arzela-Ascoli theorem: 'bounded_continuous_function.arzela_ascoli'
Hilbert Spaces:
Hilbert projection theorem: 'exists_norm_eq_infi_of_complete_convex'
orthogonal projection onto closed vector subspaces: 'orthogonal_projection_fn'
dual space: 'normed_space.dual.normed_space'
Riesz representation theorem: 'inner_product_space.to_dual'
inner product spaces $l^2$ and $L^2$: 'measure_theory.L2.inner_product_space'
their completeness: 'measure_theory.Lp.complete_space'
Hilbert (orthonormal) bases (in the separable case): 'exists_is_orthonormal_dense_span'
Hilbert basis of trigonometric polynomials:
Hilbert bases of orthogonal polynomials:
Lax-Milgram theorem:
$H^1_0([0,1])$ and its application to the one-dimensional Dirichlet problem:
# 9.
Multivariable calculus:
Differential Calculus:
differentiable functions on an open subset of $\R^n$: 'differentiable_on'
differentials (linear tangent functions): 'fderiv'
directional derivative:
partial derivatives:
Jacobian matrix:
gradient vector:
Hessian matrix:
chain rule: 'fderiv.comp'
mean value theorem: 'exists_ratio_deriv_eq_ratio_slope'
differentiable functions: 'differentiable'
$k$-times continuously differentiable functions: 'times_cont_diff'
$k$-th order partial derivatives:
partial derivatives commute:
Taylor's theorem with little-o remainder:
Taylor's theorem with integral form for remainder:
local extrema: 'is_local_min.fderiv_eq_zero'
convexity of functions on an open convex subset of $\R^n$: 'convex_on'
diffeomorphisms: 'structomorph'
inverse function theorem: 'has_strict_deriv_at.to_local_inverse'
implicit function theorem: 'implicit_function_data.implicit_function'
Differential equations:
Cauchy-Lipschitz Theorem:
maximal solutions:
Grönwall lemma: 'norm_le_gronwall_bound_of_norm_deriv_right_le'
exit theorem of a compact subspace:
autonomous differential equations:
phase portraits:
qualitative behavior:
stability of equilibrium points (linearisation theorem):
linear differential systems:
method of constant variation (Duhamel’s formula):
constant coefficient case:
solving systems of differential equations of order $> 1$:
Submanifolds of $\R^n$:
local graphs:
local parameterization:
local equation:
tangent space:
position with respect to the tangent plane:
gradient:
line integral:
curve length:
Lagrange multipliers:
# 10.
Measures and integral Calculus:
Measure theory:
measurable spaces: 'measurable_space'
sigma-algebras: 'measurable_space'
product of sigma-algebras: 'measurable_space.pi'
Borel sigma-algebras: 'borel_space'
positive measure: 'measure_theory.measure'
counting measure: 'measure_theory.measure.count'
Lebesgue measure: 'measure_theory.measure_space'
product measure: 'measurable_space.pi'
measurable functions: 'measurable'
approximation by step functions: 'measure_theory/simple_func_dense.html'
Integration:
integral of positive measurable functions: 'measure_theory.lintegral'
monotone convergence theorem: 'measure_theory.lintegral_infi_ae'
Fatou's lemma: 'measure_theory.lintegral_liminf_le'
integrable functions: 'measure_theory.integrable'
dominated convergence theorem: 'measure_theory.tendsto_integral_of_dominated_convergence'
finite dimensional vector-valued integrable functions: 'measure_theory.integrable'
continuity of integrals with respect to parameters:
differentiability of integrals with respect to parameters:
$\mathrm{L}^p$ spaces where $1 ≤ p ≤ ∞$: 'measure_theory.Lp'
Completeness of $\mathrm{L}^p$ spaces: 'measure_theory.Lp.complete_space'
Holder's inequality: 'nnreal.lintegral_mul_le_Lp_mul_Lq'
Fubini's theorem: 'measure_theory.integral_prod'
change of variables for multiple integrals:
change of variables to polar co-ordinates:
change of variables to spherical co-ordinates:
convolution:
regularization and approximation by convolution:
Fourier Analysis:
Fourier series of locally integrable periodic real-valued functions:
Riemann-Lebesgue lemma:
convolution product of periodic functions:
Dirichlet theorem:
Fejer theorem:
Parseval theorem:
Fourier transforms on $\mathrm{L}^1(\R^d)$ and $\mathrm{L}^2(R^d)$:
Plancherel’s theorem:
# 11.
Probability Theory:
Definitions of a probability space:
probability measure: 'measure_theory.probability_measure'
events:
independent events: 'probability_theory.Indep_set'
sigma-algebra: 'measurable_space'
independent sigma-algebra: 'probability_theory.Indep'
$0$-$1$ law:
Borel-Cantelli lemma (easy direction): 'measure_theory.measure_limsup_eq_zero'
Borel-Cantelli lemma (difficult direction):
conditional probability:
law of total probability:
Random variables and their laws:
discrete law: 'pmf'
absolute continuity of probability laws:
probability density function:
law of joint probability:
independence of random variables: 'probability_theory.Indep_fun'
mean and variance of a real-valued random variable:
transfer theorem:
moments:
Bernoulli law: 'pmf.bernoulli'
binomial law:
geometric law:
Poisson law:
uniform law:
exponential law:
Gaussian law:
characteristic function:
probability generating functions:
applications of probability generating functions to sums of independent random variables:
Convergence of series of random variables:
convergence in probability:
$\mathrm{L}^p$ convergence:
almost surely convergence: 'measure_theory.measure.ae'
Markov inequality:
Tchebychev inequality:
Levy's theorem:
weak law of large numbers:
strong law of large numbers:
central limit theorem:
# 12.
Distribution calculus:
Spaces $\mathcal{D}(\R^d)$:
smooth functions with compact support on $\R^d$:
stability by derivation:
stability by multiplication by a smooth function:
partitions of unity:
constructing approximations of probability density functions in spaces of common functions (trig, exp, rational, log, etc):
Distributions on $\R^d$:
definition of distributions:
locally integrable functions:
dirac measures:
Cauchy principal values:
multiplication by a smooth function:
probability distribution function from a dataset:
convergent distribution series:
support of a distribution:
Spaces $\mathcal{S}(\R^d)$:
Schwartz space of rapidly decreasing functions:
stability by derivation:
stability by multiplication by a slowly growing smooth function:
gaussian functions:
Fourier transforms on $\mathcal{S}(\R^d)$:
convolution of two functions of $\mathcal{S}(\R^d)$:
Tempered distributions:
definition:
derivation of tempered distributions:
multiplication by a function $C^\infty$ of slow growth:
$L^2$ functions and Riesz representation:
$L^p$ functions:
periodic functions:
Dirac comb:
Fourier transforms:
inverse Fourier transform:
Fourier transform and derivation:
Fourier transform and convolution product:
Applications:
Poisson’s formula:
using convolution and Fourier-Laplace transform to solve one dimensional linear differential equations:
weak solution of partial derivative equation:
fundamental solution of the Laplacian:
solving the Laplace equations:
heat equations:
wave equations:
# 13.
Numerical Analysis:
Solving systems of linear inequalities:
conditioning:
Gershgorin-Hadamard theorem:
Gauss’s pivot:
LU decomposition:
Iterative methods:
Jacobian:
Gauss-Seidel:
convergence analysis:
spectral ray:
singular value decomposition:
example of discretisation matrix by finite differences of the laplacian in one dimension:
Iterative methods of solving systems of real and vector valued equations:
linear systems case:
proper element search:
brute force method:
optimization of convex function in finite dimension:
gradient descent square root:
nonlinear problems with real and vector values:
bisection method:
Picard method:
Newton’s method:
rate of convergence and estimation of error:
Numerical integration:
Rectangle method:
error estimation:
Monte-Carlo method:
rate of convergence:
application to the calculation of multiple integrals:
Approximation of numerical functions:
Lagrange interpolation:
Lagrange polynomial of a function at (n + 1) points:
estimation of the error:
Ordinary differential equations:
numerical aspects of Cauchy's problem:
explicit Euler method:
consistency:
stability:
convergence:
order:
Fourier transform:
discrete Fourier transform on a finite abelian group:
fast Fourier transform: