Lean の数学ライブラリ Mathlib が公開している Undergraduate mathematics in mathlib の一覧を、分野ごとに並べ直したものです（元データ docs/undergrad.yaml・2026-09-27 取得）。項目はフランスの数学教員資格試験（agrégation）の出題範囲から集められたもので、学部数学の「大事な所」の目安になります。
全 566 項目のうち、Mathlib に形式化済み 529・未 37（未形式化の一覧）。分野名をクリックすると項目が開きます。日本語の分野名は訳です。
| 分野 | 原題 | 項目 | Mathlib 済 | 未 |
|---|---|---|---|---|
| 線形代数 | Linear algebra | 60 | 52 | 8 |
| 群論 | Group Theory | 39 | 33 | 6 |
| 環論 | Ring Theory | 61 | 58 | 3 |
| 双線形形式・二次形式 | Bilinear and Quadratic Forms Over a Vector Space | 39 | 35 | 4 |
| アフィン幾何・ユークリッド幾何 | Affine and Euclidean Geometry | 29 | 26 | 3 |
| 一変数の実解析 | Single Variable Real Analysis | 74 | 61 | 13 |
| 一変数の複素解析 | Single Variable Complex Analysis | 28 | 28 | 0 |
| 位相 | Topology | 44 | 44 | 0 |
| 多変数の微積分 | Multivariable calculus | 41 | 41 | 0 |
| 測度と積分 | Measures and integral calculus | 38 | 38 | 0 |
| 確率論 | Probability Theory | 38 | 38 | 0 |
| 超関数 | Distribution calculus | 39 | 39 | 0 |
| 数値解析 | Numerical Analysis | 36 | 36 | 0 |
線形代数（Linear algebra）— 60 項目・Mathlib 未 8
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 基礎 Fundamentals |
vector space | Module |
| product of vector spaces | Prod.instModule |
|
| vector subspace | Subspace |
|
| quotient space | Submodule.hasQuotient |
|
| sum of subspaces | Submodule.completeLattice |
|
| direct sum | DirectSum.IsInternal |
|
| complementary subspaces | Submodule.exists_isCompl |
|
| linear independence | LinearIndependent |
|
| generating sets | Submodule.span |
|
| bases | Module.Basis |
|
| existence of bases | Module.Basis.ofVectorSpace |
|
| linear map | LinearMap |
|
| range of a linear map | LinearMap.range |
|
| kernel of a linear map | LinearMap.ker |
|
| algebra of endomorphisms of a vector space | Module.End.instAlgebra |
|
| general linear group | LinearMap.GeneralLinearGroup |
|
| 双対 Duality |
dual vector space | Module.Dual |
| dual basis | Module.Basis.dualBasis |
|
| transpose of a linear map | Module.Dual.transpose |
|
| orthogonality | Submodule.dualAnnihilator |
|
| 有限次元ベクトル空間 Finite-dimensional vector spaces |
finite-dimensionality | FiniteDimensional |
| isomorphism with Kⁿ | Module.Basis.equivFun |
|
| rank of a linear map | LinearMap.rank |
|
| rank of a set of vectors | Set.finrank |
|
| rank of a system of linear equations | 未（参考） | |
| isomorphism with bidual | Module.evalEquiv |
|
| 多重線形性 Multilinearity |
multilinear map | MultilinearMap |
| determinant of vectors | Module.Basis.det |
|
| determinant of endomorphisms | LinearMap.det |
|
| special linear group | Matrix.SpecialLinearGroup |
|
| orientation of a ℝ-vector space | Orientation |
|
| 行列 Matrices |
commutative-ring-valued matrices | Matrix |
| field-valued matrices | Matrix |
|
| matrix representation of a linear map | LinearMap.toMatrix |
|
| change of basis | basis_toMatrix_mul_linearMap_toMatrix_mul_basis_toMatrix |
|
| rank of a matrix | Matrix.rank |
|
| determinant | Matrix.det |
|
| invertibility | Matrix.inv |
|
| elementary row operations | 未（参考） | |
| elementary column operations | 未（参考） | |
| Gaussian elimination | Matrix.Pivot.exists_list_transvec_mul_mul_list_transvec_eq_diagonal |
|
| row-reduced matrices | 未（参考） | |
| 自己準同型の多項式 Endomorphism polynomials |
annihilating polynomials | Polynomial.annIdeal |
| minimal polynomial | minpoly |
|
| characteristic polynomial | Matrix.charpoly |
|
| Cayley-Hamilton theorem | Matrix.aeval_self_charpoly |
|
| 自己準同型の構造論 Structure theory of endomorphisms |
eigenvalue | Module.End.HasEigenvalue |
| eigenvector | Module.End.HasEigenvector |
|
| diagonalization | 未（参考） | |
| triangularization | 未（参考） | |
| invariant subspaces of an endomorphism | Module.End.invtSubmodule |
|
| generalized eigenspaces | Module.End.genEigenspace |
|
| kernels lemma | 未（参考） | |
| Jordan-Chevalley-Dunford decomposition | Module.End.exists_isNilpotent_isSemisimple |
|
| Jordan normal form | 未（参考） | |
| 線形表現 Linear representations |
irreducible representation | Representation.IsIrreducible |
| Schur's lemma | FDRep.finrank_hom_simple_simple |
|
| examples | |
|
| 指数関数 Exponential |
endomorphism exponential | |
| matrix exponential | NormedSpace.exp |
群論（Group Theory）— 39 項目・Mathlib 未 6
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 基本的な定義 Basic definitions |
group | Group |
| group morphism | MonoidHom |
|
| direct product of groups | Prod.instGroup |
|
| subgroup | Subgroup |
|
| subgroup generated by a subset | Subgroup.closure |
|
| order of an element | orderOf |
|
| normal subgroup | Subgroup.Normal |
|
| quotient group | QuotientGroup.Quotient.group |
|
| group action | MulAction |
|
| stabilizer of a point | MulAction.stabilizer |
|
| orbit | MulAction.orbit |
|
| quotient space | MulAction.orbitEquivQuotientStabilizer |
|
| class formula | MulAction.selfEquivSigmaOrbitsQuotientStabilizer |
|
| conjugacy classes | ConjClasses |
|
| アーベル群 Abelian group |
cyclic group | IsCyclic |
| finite type abelian groups | AddCommGroup.equiv_free_prod_directSum_zmod |
|
| complex roots of unity | Complex.mem_rootsOfUnity |
|
| primitive complex roots of unity | Complex.isPrimitiveRoot_iff |
|
| 置換群 Permutation group |
permutation group of a type | Equiv.Perm |
| decomposition into transpositions | Equiv.Perm.truncSwapFactors |
|
| decomposition into cycles with disjoint support | Equiv.Perm.truncCycleFactors |
|
| signature | Equiv.Perm.sign |
|
| alternating group | alternatingGroup |
|
| 古典的な自己同型群 Classical automorphism groups |
general linear group | Matrix.GeneralLinearGroup |
| special linear group | Matrix.SpecialLinearGroup |
|
| orthogonal group | Matrix.orthogonalGroup |
|
| special orthogonal group | Matrix.specialOrthogonalGroup |
|
| unitary group | Matrix.unitaryGroup |
|
| special unitary group | Matrix.specialUnitaryGroup |
|
| 有限群の表現論 Representation theory of finite groups |
representations of abelian groups | 未（参考） |
| dual groups | 未（参考） | |
| Maschke theorem | MonoidAlgebra.Submodule.exists_isCompl |
|
| orthogonality of irreducible characters | FDRep.char_orthonormal |
|
| Fourier transform for finite abelian groups | 未（参考） | |
| convolution | 未（参考） | |
| class function over a group | 未（参考） | |
| characters of a finite-dimensional representation | FDRep.character |
|
| orthonormal basis of irreducible characters | 未（参考） | |
| examples of groups with small cardinality | |
環論（Ring Theory）— 61 項目・Mathlib 未 3
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 基礎 Fundamentals |
ring | Ring |
| subrings | Subring |
|
| ring morphisms | RingHom |
|
| ring structure ℤ | Int.instCommRing |
|
| product of rings | Pi.ring |
|
| イデアルと剰余環 Ideals and Quotients |
ideal of a commutative ring | Ideal |
| quotient rings | Ideal.Quotient.ring |
|
| prime ideals | Ideal.IsPrime |
|
| maximal ideals | Ideal.IsMaximal |
|
| Chinese remainder theorem | Ideal.quotientInfRingEquivPiQuotient |
|
| 多元環 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 | IsCoprime |
|
| unique factorisation domain (UFD) | UniqueFactorizationMonoid |
|
| greatest common divisor | GCDMonoid.gcd |
|
| least common multiple | GCDMonoid.lcm |
|
| A[X_i] is a UFD when A is a UFD | MvPolynomial.uniqueFactorizationMonoid |
|
| principal ideal domain | Submodule.IsPrincipal |
|
| Euclidean rings | EuclideanDomain |
|
| Euclid's' algorithm | Nat.xgcd |
|
| ℤ is a Euclidean ring | Int.euclideanDomain |
|
| congruence in ℤ | Int.ModEq |
|
| prime numbers | Prime |
|
| Bézout's identity | exists_gcd_eq_mul_add_mul |
|
| ℤ/nℤ and its invertible elements | ZMod.unitOfCoprime |
|
| Euler's totient function (φ) | Nat.totient |
|
| 多項式環 Polynomial rings |
K[X] is a Euclidean ring when K is a field | Polynomial.instEuclideanDomain |
| irreducible polynomial | Irreducible |
|
| cyclotomic polynomials in ℚ[X] | Polynomial.cyclotomic |
|
| Eisenstein's criterion | Polynomial.irreducible_of_eisenstein_criterion |
|
| polynomial algebra in one or several indeterminates over a commutative ring | MvPolynomial |
|
| roots of a polynomial | Polynomial.roots |
|
| multiplicity | Polynomial.rootMultiplicity |
|
| relationship between the coefficients and the roots of a split polynomial | Polynomial.coeff_eq_esymm_roots_of_card |
|
| Newton's identities | MvPolynomial.mul_esymm_eq_sum |
|
| polynomial derivative | Polynomial.derivative |
|
| decomposition into sums of homogeneous polynomials | MvPolynomial.sum_homogeneousComponent |
|
| symmetric polynomials | MvPolynomial.IsSymmetric |
|
| 体論 Field Theory |
fields | Field |
| characteristic of a ring | ringChar |
|
| characteristic zero | CharZero |
|
| characteristic p | CharP |
|
| Subfields | Subfield |
|
| Frobenius morphisms | frobenius |
|
| field ℚ of rational numbers | Rat.instField |
|
| field ℝ of real numbers | Real.instField |
|
| field ℂ of complex numbers | Complex.instField |
|
| ℂ is algebraically closed | Complex.exists_root |
|
| field of fractions of an integral domain | IsFractionRing |
|
| algebraic elements | IsAlgebraic |
|
| transcendental elements | Transcendental |
|
| algebraic extensions | Algebra.IsAlgebraic |
|
| algebraically closed fields | IsAlgClosed |
|
| rupture fields | AdjoinRoot |
|
| splitting fields | Polynomial.SplittingField |
|
| finite fields | Mathlib/FieldTheory/Finite/Basic.html |
|
| rational fraction fields with one indeterminate over a field | RatFunc |
|
| ℝ(X)-partial fraction decomposition | 未（参考） | |
| ℂ(X)-partial fraction decomposition | 未（参考） |
双線形形式・二次形式（Bilinear and Quadratic Forms Over a Vector Space）— 39 項目・Mathlib 未 4
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 双線形形式 Bilinear forms |
bilinear forms | LinearMap.BilinForm |
| alternating bilinear forms | LinearMap.BilinForm.IsAlt |
|
| symmetric bilinear forms | LinearMap.BilinForm.IsSymm |
|
| nondegenerate forms | LinearMap.BilinForm.Nondegenerate |
|
| matrix representation | LinearMap.BilinForm.toMatrix |
|
| change of coordinates | LinearMap.BilinForm.toMatrix_comp |
|
| rank of a bilinear form | |
|
| 二次形式 Quadratic forms |
quadratic form | QuadraticForm |
| polar form of a quadratic | QuadraticMap.polar |
|
| 直交性 Orthogonality |
orthogonal elements | LinearMap.BilinForm.iIsOrtho |
| adjoint endomorphism | LinearMap.BilinForm.leftAdjointOfNondegenerate |
|
| Sylvester's law of inertia (existence) | QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared |
|
| Sylvester's law of inertia (uniqueness) | QuadraticForm.sigPos_of_equiv_weightedSumSquares |
|
| real classification | QuadraticForm.equivalent_one_zero_neg_one_weighted_sum_squared |
|
| complex classification | QuadraticForm.equivalent_weightedSumSquares_of_isAlgClosed |
|
| Gram-Schmidt orthogonalisation | InnerProductSpace.gramSchmidt_orthogonal |
|
| ユークリッド空間・エルミート空間 Euclidean and Hermitian spaces |
Euclidean vector spaces | InnerProductSpace |
| Hermitian vector spaces | InnerProductSpace |
|
| dual isomorphism in the Euclidean case | InnerProductSpace.toDual |
|
| orthogonal complement | Submodule.orthogonal |
|
| Cauchy-Schwarz inequality | inner_mul_inner_self_le |
|
| norm | InnerProductSpace.Core.toNorm |
|
| orthonormal bases | maximal_orthonormal_iff_basis_of_finiteDimensional |
|
| 自己準同型 Endomorphisms |
orthogonal group | Matrix.orthogonalGroup |
| unitary group | Matrix.unitaryGroup |
|
| special orthogonal group | Matrix.specialOrthogonalGroup |
|
| special unitary group | Matrix.specialUnitaryGroup |
|
| self-adjoint endomorphism | IsSelfAdjoint |
|
| normal endomorphism | IsStarNormal |
|
| diagonalization of a self-adjoint endomorphism | LinearMap.IsSymmetric.eigenvectorBasis_apply_self_apply |
|
| 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 | LinearIsometryEquiv.reflections_generate |
|
| polar decompositions in GL(n, ℝ) | 未（参考） | |
| polar decompositions in GL(n, ℂ) | 未（参考） | |
| 低次元 Low dimensions |
cross product | crossProduct |
| triple product | triple_product_eq_det |
|
| classification of elements of O(2, ℝ) | |
|
| classification of elements of O(3, ℝ) | |
アフィン幾何・ユークリッド幾何（Affine and Euclidean Geometry）— 29 項目・Mathlib 未 3
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 一般の定義 General definitions |
affine space | AddTorsor |
| affine function | AffineMap |
|
| affine subspace | AffineSubspace |
|
| barycenter | Finset.affineCombination |
|
| affine span | affineSpan |
|
| equations of affine subspace | |
|
| affine groups | AffineEquiv.group |
|
| affine property | 未（参考） | |
| group generated by homotheties and translations | 未（参考） | |
| transformations fixing a basis of directions | 未（参考） | |
| 凸性 Convexity |
convex subsets | Convex |
| convex hull of a subset of an affine real space | convexHull |
|
| extreme point | Set.extremePoints |
|
| ユークリッドアフィン空間 Euclidean affine spaces |
isometries of a Euclidean affine space | AffineIsometryEquiv |
| group of isometries of a Euclidean affine space | AffineIsometryEquiv.instGroup |
|
| 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 | InnerProductGeometry.angle |
|
| angles between planes | |
|
| inscribed angle theorem | Orientation.two_zsmul_oangle_sub_eq_two_zsmul_oangle_sub_of_norm_eq |
|
| cocyclicity | EuclideanGeometry.Concyclic |
|
| 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 | |
一変数の実解析（Single Variable Real Analysis）— 74 項目・Mathlib 未 13
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 実数 Real numbers |
definition of ℝ | Real |
| field structure | Real.instField |
|
| order | Real.linearOrder |
|
| 実数列 Sequences of real numbers |
convergence | Filter.Tendsto |
| limit point | MapClusterPt |
|
| recurrent sequences | Nat |
|
| limit infimum and supremum | Mathlib/Order/LiminfLimsup.html |
|
| Cauchy sequences | CauchySeq |
|
| ℝ の位相 Topology of R |
metric structure | Real.metricSpace |
| completeness of R | Real.instCompleteSpace |
|
| Bolzano-Weierstrass theorem | tendsto_subseq_of_bounded |
|
| compact subsets of ℝ | Metric.isCompact_iff_isClosed_bounded |
|
| connected subsets of ℝ | setOfPred_isPreconnected_eq_of_ordered |
|
| additive subgroups of ℝ | AddSubgroup.dense_or_cyclic |
|
| 数の級数 Numerical series |
Convergence of real-valued series | 未（参考） |
| Geometric series | tsum_geometric_of_norm_lt_one |
|
| convergence of p-series for p>1 | Real.summable_one_div_nat_rpow |
|
| summation of comparison relations | 未（参考） | |
| comparison of a series and an integral | AntitoneOn.tsum_le_integral |
|
| error estimation | 未（参考） | |
| absolute convergence | 未（参考） | |
| products of series | 未（参考） | |
| alternating series | Antitone.tendsto_alternating_series_of_tendsto_zero |
|
| ℝ の部分集合上の実数値関数 Real-valued functions defined on a subset of ℝ |
continuity | Continuous |
| limits | Filter.Tendsto |
|
| intermediate value theorem | intermediate_value_Icc |
|
| image of a segment | ContinuousOn.image_Icc |
|
| continuity of monotone functions | OrderIso.continuous |
|
| continuity of inverse functions | OrderIso.toHomeomorph |
|
| 微分可能性 Differentiability |
derivative at a point | HasDerivAt |
| differentiable functions | HasDerivAt |
|
| derivative of a composition of functions | deriv_comp |
|
| derivative of the inverse of a function | HasStrictDerivAt.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 | iteratedDeriv |
|
| Cᵏ functions | ContDiff |
|
| piecewise Cᵏ functions | 未（参考） | |
| Leibniz formula | deriv_mul |
|
| テイラー型の定理 Taylor-like theorems |
Taylor's theorem with little-o remainder | 未（参考） |
| Taylor's theorem with integral form for remainder | taylor_integral_remainder_of_absolutelyContinuous |
|
| Taylor's theorem with Lagrange form for remainder | taylor_mean_remainder_lagrange |
|
| Taylor series expansions | 未（参考） | |
| 初等関数（三角・有理・exp・log など） Elementary functions (trigonometric, rational, exp, log, etc) |
polynomial functions | Polynomial.eval |
| rational functions | RatFunc.eval |
|
| 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 | |
| Riemann sums | BoxIntegral.integralSum |
|
| antiderivative of a continuous function | Continuous.deriv_integral |
|
| change of variable | intervalIntegral.integral_deriv_smul_comp |
|
| integration by parts | intervalIntegral.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 | tendsto_pi_nhds |
| uniform convergence | TendstoUniformly |
|
| normal convergence | 未（参考） | |
| continuity of the limit of a sequence of functions | continuous_of_uniform_approx_of_continuous |
|
| continuity of the sum of a series of functions | continuous_tsum |
|
| differentiability of the limit of a sequence of functions | hasFDerivAt_of_tendstoUniformly |
|
| differentiability of the sum of a series of functions | differentiable_tsum |
|
| Weierstrass polynomial approximation theorem | polynomialFunctions_closure_eq_top |
|
| Weierstrass trigonometric approximation theorem | span_fourier_closure_eq_top |
|
| 凸性 Convexity |
convex functions of a real variable | ConvexOn |
| continuity and differentiability of convex functions（continuity） | ConvexOn.continuousOn |
|
| continuity and differentiability of convex functions（differentiability） | 未（参考） | |
| characterizations of convexity | convexOn_of_deriv2_nonneg |
|
| convexity inequalities | Mathlib/Analysis/MeanInequalities.html |
一変数の複素解析（Single Variable Complex Analysis）— 28 項目・Mathlib 未 0
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 複素数値の級数 Complex-valued series |
radius of convergence | FormalMultilinearSeries.radius |
| continuity | HasFPowerSeriesOnBall.continuousOn |
|
| differentiability with respect to the complex variable | HasFPowerSeriesOnBall.differentiableOn |
|
| antiderivative | |
|
| complex exponential | Complex.exp |
|
| extension of trigonometric functions to the complex plane（cos） | Complex.cos |
|
| extension of trigonometric functions to the complex plane（sin） | Complex.sin |
|
| power series expansion of elementary functions（cos） | Complex.hasSum_cos |
|
| power series expansion of elementary functions（sin） | Complex.hasSum_sin |
|
| power series expansion of elementary functions（log） | Complex.hasSum_taylorSeries_log |
|
| 一複素変数の関数 Functions on one complex variable |
holomorphic functions | DifferentiableOn |
| Cauchy-Riemann conditions | |
|
| contour integrals of continuous functions in ℂ | |
|
| antiderivatives of a holomorphic function | |
|
| representations of the log function on ℂ | |
|
| theorem of holomorphic functions under integral domains | |
|
| winding number of a closed curve in ℂ with respect to a point | |
|
| Cauchy formulas | Complex.two_pi_I_inv_smul_circleIntegral_sub_inv_smul_of_differentiable_on_off_countable |
|
| analyticity of a holomorphic function | DifferentiableOn.analyticAt |
|
| principle of isolated zeros | AnalyticAt.eventually_eq_zero_or_eventually_ne_zero |
|
| principle of analytic continuation | AnalyticOnNhd.eqOn_of_preconnected_of_frequently_eq |
|
| maximum principle | Complex.eventually_eq_of_isLocalMax_norm |
|
| isolated singularities | |
|
| Laurent series | |
|
| meromorphic functions | |
|
| residue theorem | |
|
| sequences and series of holomorphic functions | |
|
| holomorphic stability under uniform convergence | TendstoLocallyUniformlyOn.differentiableOn |
位相（Topology）— 44 項目・Mathlib 未 0
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 位相空間と距離空間 Topology and Metric Spaces |
topology of a metric space | Metric.isOpen_iff |
| induced topology | TopologicalSpace.induced |
|
| finite product of metric spaces | metricSpacePi |
|
| limits of sequences | Metric.tendsto_atTop |
|
| cluster points | ClusterPt |
|
| continuous functions | Continuous |
|
| homeomorphisms | Homeomorph |
|
| compactness in terms of open covers (Borel-Lebesgue) | isCompact_iff_finite_subcover |
|
| sequential compactness is equivalent to compactness (Bolzano-Weierstrass) | isCompact_iff_isSeqCompact |
|
| connectedness | ConnectedSpace |
|
| connected components | connectedComponent |
|
| path connectedness | IsPathConnected |
|
| Lipschitz functions | LipschitzWith |
|
| uniformly continuous functions | Metric.uniformContinuous_iff |
|
| Heine-Cantor theorem | CompactSpace.uniformContinuous_of_continuous |
|
| complete metric spaces | Metric.complete_of_cauchySeq_tendsto |
|
| contraction mapping theorem | ContractingWith.exists_fixedPoint |
|
| ℝ・ℂ 上のノルム空間 Normed vector spaces on ℝ and ℂ |
topology on a normed vector space | NormSMulClass.toIsBoundedSMul |
| equivalent norms | |
|
| Banach open mapping theorem | ContinuousLinearMap.isOpenMap |
|
| equivalence of norms in finite dimension | LinearEquiv.toContinuousLinearEquiv |
|
| norms ‖·‖ₚ on ℝⁿ and ℂⁿ | PiLp.normedSpace |
|
| absolutely convergent series in Banach spaces | Summable.of_norm |
|
| continuous linear maps | ContinuousLinearMap |
|
| norm of a continuous linear map | LinearMap.mkContinuous |
|
| uniform convergence norm (sup-norm) | EMetric.tendstoUniformlyOn_iff |
|
| normed space of bounded continuous functions | BoundedContinuousFunction.instNormedSpace |
|
| completeness of the space of bounded continuous functions | BoundedContinuousFunction.instCompleteSpace |
|
| Heine-Borel theorem (closed bounded subsets are compact in finite dimension) | FiniteDimensional.proper |
|
| Riesz' lemma (unit-ball characterization of finite dimension) | FiniteDimensional.of_isCompact_closedBall |
|
| Arzela-Ascoli theorem | BoundedContinuousFunction.arzela_ascoli |
|
| ヒルベルト空間 Hilbert spaces |
Hilbert projection theorem | exists_norm_eq_iInf_of_complete_convex |
| orthogonal projection onto closed vector subspaces | Submodule.orthogonalProjectionOnto |
|
| dual space | StrongDual |
|
| Riesz representation theorem | InnerProductSpace.toDual |
|
| inner product space l² | lp.instInnerProductSpace |
|
| completeness of l² | lp.completeSpace |
|
| inner product space L² | MeasureTheory.L2.innerProductSpace |
|
| completeness of L² | MeasureTheory.Lp.instCompleteSpace |
|
| Hilbert bases | HilbertBasis |
|
| example, the Hilbert basis of trigonometric polynomials | fourierBasis |
|
| example, classical Hilbert bases of orthogonal polynomials | |
|
| Lax-Milgram theorem | IsCoercive.continuousLinearEquivOfBilin |
|
| H¹₀([0,1]) and its application to the one-dimensional Dirichlet problem | |
多変数の微積分（Multivariable calculus）— 41 項目・Mathlib 未 0
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 微分 Differential calculus |
differentiable functions on an open subset of ℝⁿ | DifferentiableOn |
| differentials (linear tangent functions) | fderiv |
|
| directional derivative | lineDeriv |
|
| partial derivatives | |
|
| Jacobian matrix | |
|
| gradient vector | gradient |
|
| Hessian matrix | |
|
| chain rule | fderiv_comp |
|
| mean value theorem | exists_ratio_deriv_eq_ratio_slope |
|
| differentiable functions | Differentiable |
|
| k-times continuously differentiable functions | ContDiff |
|
| k-th order partial derivatives | |
|
| partial derivatives commute | second_derivative_symmetric |
|
| Taylor's theorem with little-o remainder | |
|
| Taylor's theorem with integral form for remainder | map_add_eq_sum_add_integral_iteratedFDeriv |
|
| local extrema | IsLocalMin.fderiv_eq_zero |
|
| convexity of functions on an open convex subset of ℝⁿ | ConvexOn |
|
| diffeomorphisms | Structomorph |
|
| inverse function theorem | HasStrictDerivAt.to_localInverse |
|
| implicit function theorem | ImplicitFunctionData.implicitFunction |
|
| 微分方程式 Differential equations |
Cauchy-Lipschitz Theorem | IsPicardLindelof.exists_eq_forall_mem_Icc_hasDerivWithinAt |
| maximal solutions | |
|
| Grönwall lemma | norm_le_gronwallBound_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 ℝⁿ |
local graphs | |
| local parameterization | |
|
| local equation | |
|
| tangent space | |
|
| position with respect to the tangent plane | |
|
| gradient | |
|
| line integral | |
|
| curve length | |
|
| Lagrange multipliers | |
測度と積分（Measures and integral calculus）— 38 項目・Mathlib 未 0
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 測度論 Measure theory |
measurable spaces | MeasurableSpace |
| sigma-algebras | MeasurableSpace |
|
| product of sigma-algebras | MeasurableSpace.pi |
|
| Borel sigma-algebras | BorelSpace |
|
| positive measure | MeasureTheory.Measure |
|
| counting measure | MeasureTheory.Measure.count |
|
| Lebesgue measure | MeasureTheory.MeasureSpace |
|
| product measure | MeasurableSpace.pi |
|
| measurable functions | Measurable |
|
| approximation by step functions | MeasureTheory.SimpleFunc.tendsto_approxOn |
|
| 積分 Integration |
integral of positive measurable functions | MeasureTheory.lintegral |
| monotone convergence theorem | MeasureTheory.lintegral_iInf_ae |
|
| Fatou's lemma | MeasureTheory.lintegral_liminf_le |
|
| integrable functions | MeasureTheory.Integrable |
|
| dominated convergence theorem | MeasureTheory.tendsto_integral_of_dominated_convergence |
|
| finite-dimensional vector-valued integrable functions | MeasureTheory.Integrable |
|
| continuity of integrals with respect to parameters | intervalIntegral.continuous_of_dominated_interval |
|
| differentiability of integrals with respect to parameters | IntervalIntegrable.ae_hasDerivAt_integral |
|
| Lᵖ spaces where 1 ≤ p ≤ ∞ | MeasureTheory.Lp |
|
| Completeness of Lᵖ spaces | MeasureTheory.Lp.instCompleteSpace |
|
| Holder's inequality | NNReal.lintegral_mul_le_Lp_mul_Lq |
|
| Fubini's theorem | MeasureTheory.integral_prod |
|
| change of variables for multiple integrals | MeasureTheory.integral_image_eq_integral_abs_det_fderiv_smul |
|
| change of variables to polar co-ordinates | integral_comp_polarCoord_symm |
|
| change of variables to spherical co-ordinates | |
|
| convolution | MeasureTheory.convolution |
|
| approximation by convolution | ContDiffBump.convolution_tendsto_right |
|
| regularization by convolution | HasCompactSupport.contDiff_convolution_left |
|
| フーリエ解析 Fourier analysis |
Fourier series of locally integrable periodic real-valued functions | fourierBasis |
| Riemann-Lebesgue lemma | tendsto_integral_exp_smul_cocompact |
|
| convolution product of periodic functions | |
|
| Dirichlet theorem | |
|
| Fejer theorem | |
|
| Parseval theorem | tsum_sq_fourierCoeff |
|
| Fourier transform on L¹(ℝᵈ) | Real.fourier_eq |
|
| Fourier transform on L²(ℝᵈ) | MeasureTheory.Lp.fourierTransformₗᵢ |
|
| Plancherel’s theorem | SchwartzMap.integral_inner_fourier_fourier |
|
| Fourier inversion formula | Continuous.fourierInv_fourier_eq |
確率論（Probability Theory）— 38 項目・Mathlib 未 0
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 確率空間の定義 Definitions of a probability space |
probability measure | MeasureTheory.IsProbabilityMeasure |
| events | MeasurableSet |
|
| independent events | ProbabilityTheory.iIndepSet |
|
| sigma-algebra | MeasurableSpace |
|
| independent sigma-algebra | ProbabilityTheory.iIndep |
|
| 0-1 law | ProbabilityTheory.measure_zero_or_one_of_measurableSet_limsup_atTop |
|
| Borel-Cantelli lemma (easy direction) | MeasureTheory.measure_limsup_atTop_eq_zero |
|
| Borel-Cantelli lemma (difficult direction) | ProbabilityTheory.measure_limsup_eq_one |
|
| conditional probability | ProbabilityTheory.cond |
|
| law of total probability | |
|
| 確率変数とその分布 Random variables and their laws |
discrete law | PMF |
| absolute continuity of probability laws | |
|
| probability density function | MeasureTheory.HasPDF |
|
| law of joint probability | |
|
| independence of random variables | ProbabilityTheory.iIndepFun |
|
| mean of a random variable | MeasureTheory.integral |
|
| variance of a real-valued random variable | ProbabilityTheory.variance |
|
| transfer theorem | |
|
| moments | ProbabilityTheory.moment |
|
| Bernoulli law | ProbabilityTheory.bernoulliMeasure |
|
| binomial law | ProbabilityTheory.binomial |
|
| geometric law | ProbabilityTheory.geometricMeasure |
|
| Poisson law | ProbabilityTheory.poissonMeasure |
|
| uniform law | |
|
| exponential law | ProbabilityTheory.expMeasure |
|
| Gaussian law | ProbabilityTheory.gaussianReal |
|
| characteristic function | MeasureTheory.charFun |
|
| probability generating functions | |
|
| applications of probability generating functions to sums of independent random variables | |
|
| 確率変数列の収束 Convergence of a sequence of random variables |
convergence in probability | MeasureTheory.TendstoInMeasure |
| Lᵖ convergence | MeasureTheory.Lp |
|
| almost surely convergence | MeasureTheory.ae |
|
| Markov inequality | MeasureTheory.mul_meas_ge_le_lintegral |
|
| Chebyshev inequality | ProbabilityTheory.meas_ge_le_variance_div_sq |
|
| Lévy's theorem | |
|
| weak law of large numbers | |
|
| strong law of large numbers | ProbabilityTheory.strong_law_ae |
|
| central limit theorem | ProbabilityTheory.tendstoInDistribution_inv_sqrt_mul_sum_sub |
超関数（Distribution calculus）— 39 項目・Mathlib 未 0
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 空間 𝒟(ℝᵈ) Spaces 𝒟(ℝᵈ) |
smooth functions with compact support on ℝᵈ | TestFunction |
| 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 ℝᵈ |
definition of distributions | Distribution |
| locally integrable functions as distributions | |
|
| derivative of a distribution | |
|
| Dirac measures | |
|
| derivatives of Dirac measures | |
|
| derivative of the Heaviside function | |
|
| Cauchy principal values | |
|
| multiplication by a smooth function | |
|
| convergence of sequences of distributions | |
|
| support of a distribution | |
|
| 空間 𝒮(ℝᵈ) Spaces 𝒮(ℝᵈ) |
Schwartz space of rapidly decreasing functions | SchwartzMap |
| stability by derivation | SchwartzMap.fderivCLM |
|
| stability by multiplication by a slowly growing smooth function | SchwartzMap.bilinLeftCLM |
|
| Gaussian functions | |
|
| Fourier transforms on 𝒮(ℝᵈ) | SchwartzMap.fourierTransformCLM |
|
| convolution of two functions of 𝒮(ℝᵈ) | SchwartzMap.convolution |
|
| 緩増加超関数 Tempered distributions |
definition | TemperedDistribution |
| derivation of tempered distributions | TemperedDistribution.instLineDeriv |
|
| multiplication by a function C^∞ of slow growth | TemperedDistribution.smulLeftCLM |
|
| L² functions and Riesz representation | |
|
| Lᵖ functions | MeasureTheory.Lp.toTemperedDistributionCLM |
|
| periodic functions | |
|
| Dirac comb | |
|
| Fourier transforms | FourierTransform.fourierCLM |
|
| inverse Fourier transform | FourierTransform.fourierInvCLM |
|
| Fourier transform and derivation | |
|
| Fourier transform and convolution product | |
|
| 応用 Applications |
Poisson’s formula | SchwartzMap.tsum_eq_tsum_fourier |
| 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 | |
数値解析（Numerical Analysis）— 36 項目・Mathlib 未 0
| 小分類 | 項目 | Mathlib での名前 |
|---|---|---|
| 線形不等式系の解法 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.interpolate |
| Lagrange polynomial of a function at (n + 1) points | Lagrange.interpolate |
|
| 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 | |