Alphabeta MathArticle items · 05 — The principle of mathematical induction
Presents 29 items from the article and its immediate prerequisites, covering published library prerequisites and dependency level 0.
1 · Prerequisites
- The natural numbers ℕ (von Neumann)
- Inductive set
- The natural numbers exist: a smallest inductive set
- L(1/x)=-L(x), L(xⁿ)=nL(x), and in particular L(2ⁿ)=nL(2)
- Every complete ordered field is Archimedean
- Continuity of f : A → ℝ at a point of A and on A: the ε-δ condition, its agreement with lim_x → c f(x) = f(c) at a limit point, and continuity at an isolated point
- Sums, scalar multiples, products, absolute values, maxima, minima and quotients with nonvanishing denominator of continuous functions are continuous, as are constants, the identity and every polynomial function
- f is continuous at c ∈ A if and only if f(xₖ) → f(c) for every sequence in A converging to c, the converse direction costing countable choice
- A nested sequence of nonempty closed bounded intervals has nonempty intersection, and the intersection is a single point exactly when the lengths tend to 0
- Intervals of ℝ: the nine order-convex forms, nondegeneracy, and length
- Complete ordered field (least-upper-bound property)
- The recursion theorem
- For |r| < 1 the sequence rᵏ is null, and for |r| > 1 the sequence |r|ᵏ diverges to +∞
- Algebra of limits: sums, scalar multiples, products and quotients
- Limits preserve non-strict inequalities
- Limits and Cauchy sequences of reals
- Sequences of reals: bounded, eventually, frequently, tails, subsequences
- Integer powers aᵐ
- Laws of integer exponents
- Basic properties of the absolute value
- Ordered field
- Lebesgue measurable sets, the family L(ℝⁿ), and the restricted set function λₙ
- Carathéodory's theorem: measurable sets form a sigma-algebra carrying a complete measure
- Assuming countable choice, every source-algebra set is measurable for the induced outer measure
- Assuming countable choice, a premeasure extends through its induced outer measure
- Every outer-null set is Carathéodory measurable
- Measures on sigma-algebras
- Complete measure spaces
- The Axiom of Countable Choice (AC_ω)
- Elementary sets: the finite unions of half-open boxes in ℝⁿ
- Lebesgue outer measure on ℝⁿ
- Elementary volume is a sigma-finite premeasure on the algebra of elementary sets
- The sum of the volumes of a disjoint box decomposition of an elementary set does not depend on the decomposition
- Half-open boxes in ℝⁿ and their volume
- Assuming countable choice, every Borel subset of ℝⁿ is Lebesgue measurable
- Outer measures
- Axis-parallel rectangles in ℝᵐ and their volume
- Finite sums and finite products, by recursion
- Laws of finite sums and finite products
- For every ε > 0 in a complete ordered field there is a natural n ≥ 1 with 1/n < ε
- The metric topology: a set is open when every one of its points has a ball around it inside the set; closed means open complement
- Assuming countable choice, the outer set function induced by a premeasure is an outer measure
- The induced outer measure agrees with the premeasure on the source algebra
- Expectation of a real random variable on a finite probability space
- Finite commutative-monoid sums are invariant under bijective reindexing, split over disjoint unions, and satisfy the finite Fubini rule
- Integrable real and complex functions, and their integrals
- Additivity of the nonnegative Lebesgue integral
- Monotonicity and nonnegative homogeneity of the nonnegative integral
- Closure properties of measurable functions used by the integral
- The natural logarithm as the inverse of the exponential function
- Derivative of an inverse: if f is continuous and injective on a nondegenerate interval I and differentiable at c ∈ I with f'(c) ≠ 0, then the inverse g is differentiable at f(c) with g'(f(c)) = 1/f'(c); and if f'(c) = 0 then g is not differentiable at f(c)
- The exponential function is smooth and (exp)'=exp
- The first fundamental theorem: if f is integrable on [a,b] and continuous at c, then F'(c) = f(c); in particular a continuous f has F as a primitive
- The integral with oriented limits: ∫ₐᵃ f := 0 and ∫_bᵃ f := -∫ₐᵇ f
- A function continuous on an interval I whose derivative vanishes at every interior point of I is constant on I; consequently two such functions with the same derivative differ by a constant
- The exponential dominates every fixed nonnegative integer power at +∞
- Real powers for positive bases, with the zero-base positive-exponent convention
- The exponential tends to +∞ at +∞ and to 0 at -∞
- Expectation preserves pointwise order and lies between the minimum and maximum attained values
- Indicators turn event probabilities, intersections, and finite counts into expectations and products
- The derivative and the Riemann integral of a vector-valued function: an intrinsic derivative and a componentwise integral
- Vector-valued functions f : A → ℝᵐ, their limits and continuity, with the dictionary to the metric notions
- A vector-valued function has a limit, or is continuous, if and only if each of its components does; with the algebra of continuous vector-valued functions
- The Euclidean inner product ⟨ x,y⟩ = ∑_k<n xₖ yₖ on ℝⁿ
- Cauchy-Schwarz |⟨ x,y⟩| ≤ ‖ x‖₂‖ y‖₂ with its equality case, the triangle inequality for ‖·‖₂, the parallelogram law and polarisation
- The p-norms ‖ x‖ₚ for rational p ≥ 1, and ‖ x‖_∞
- A norm on a real vector space, the induced metric, and the dictionary with the metric axioms
- The mean value theorem, as the case g(x) = x of Cauchy's: for f continuous on [a,b] with a < b and differentiable on (a,b) there is c ∈ (a,b) with f(b) - f(a) = f'(c)(b-a)
- Sums, scalar multiples, products and quotients: (f+g)'(c) = f'(c) + g'(c), (α f)'(c) = α f'(c), (fg)'(c) = f'(c)g(c) + f(c)g'(c), and (f/g)'(c) = (f'(c)g(c) - f(c)g'(c))/g(c)² when g(c) ≠ 0
- Dictionary: for A ⊆ ℝ with the metric d(x,y) = |x-y|, continuity and uniform continuity of f : A → ℝ agree with the metric-space notions, the Lipschitz and Hölder conditions are the metric ones instantiated, and a subset of ℝ is compact in the open-cover sense of ℝ exactly when it is a compact metric subspace
- The derivative f'(c) = lim_x → c f(x) - f(c)/x - c of f : A → ℝ at a point c ∈ A that is a limit point of A, and differentiability on a set
- A function differentiable at c is continuous at c
- Inverses of positives are positive, and reciprocation reverses order
- Limit point, isolated point, adherent point, derived set, and dense subset of ℝ
- Holder's inequality for integrals, including the endpoint cases
- The function space Lᵖ(μ) for 0 < p < ∞
- The space L^∞(μ) of essentially bounded measurable functions
- The essential supremum is attained as the least essential bound
- Monotone convergence for the integral
- Holder's inequality for finite sums and conjugate real exponents
- Nondecreasing, increasing (strictly increasing), nonincreasing, decreasing, monotone and strictly monotone real functions on a subset of ℝ, with the dictionary to monotone sequences
- If f ≤ g on a punctured neighbourhood of c then lim f ≤ lim g, non-strictly
- The ε-δ limit lim_x → c f(x) = L of f : A → ℝ at a limit point c of A
- Interior, closure, boundary and exterior of a subset of ℝ
- Sign rules for products and monotonicity of multiplication
- The ε-neighbourhood and the punctured ε-neighbourhood of a point of ℝ
- The exponential addition formula exp(x+y)=exp(x)exp(y)
- The exponential is positive and satisfies exp(-x)=1/exp(x)
- The exponential function is strictly increasing
- Continuous inverse theorem: a continuous injective f on an interval I is a bijection onto the order-convex set f[I], and the inverse g : f[I] → I is continuous and strictly monotone in the same sense as f
- The operator norm is zero on the zero domain and otherwise is max_‖ v‖=1‖ Tv‖
- Every linear map between finite-dimensional real or complex inner product spaces admits a singular value decomposition
- A real-analytic function on an open subset of ℝ is locally represented by a convergent real power series
- A power-series sum may be re-expanded about every interior point, with coefficients given by its derivatives there
- The finite product of finite probability spaces
- Independent events, pairwise independence, and mutual independence of a finite family
- Pi as twice the smallest positive zero of cosine
- Cosine has a smallest positive zero, lying strictly between zero and two
- Parity and the Pythagorean identity for sine and cosine
- Sine is positive and cosine is strictly decreasing on (0,2), with cos 2 at most -1/3
- Order on the reals
- The real numbers
- The reals form a field
- A non-null Cauchy sequence is eventually bounded away from zero, with constant sign
- The rationals form a totally ordered field
- Null sequence
- The product measure of two sigma-finite measure spaces
- For sigma-finite measures, the two section-measure integrals of a measurable set agree
- Pi-systems
- Measures agreeing on a generating pi-system are equal under an increasing finite-measure exhaustion from that pi-system
- Finite, sigma-finite, and semifinite measures
- The nonnegative integral agrees with the simple integral on simple functions
- The integral of a nonnegative simple function
- The product sigma-algebra and its finite iterates
- Existence and uniqueness for y''=-y with prescribed initial data
- The derivatives of sine and cosine are cosine and minus sine
- The chain rule, in one line from Carathéodory: if g is differentiable at c and f is differentiable at g(c), then f ∘ g is differentiable at c with (f ∘ g)'(c) = f'(g(c)) g'(c)
- Pi is the first positive zero of sine
- Integer part: for every real x there is exactly one integer m with m ≤ x < m + 1
- The cardinality | A| of a finite set
- Finite, countably infinite, countable, uncountable
- Equinumerous sets, A ≈ B and A ⪯ B
- Injection, surjection, bijection
- On ℕ the order is membership: m < n ⟺ m ∈ n
- Order on the natural numbers
- Addition of natural numbers
- Addition is cancellative
- Order is compatible with addition
- Discreteness: σ(n) is the immediate successor
- The well-ordering principle
- The sum ∑_i ∈ S aᵢ over a finite index set, and its product form
- A finite sum is unchanged by a permutation of its index range: ∑_k<n a_π(k) = ∑_k<n aₖ for every bijection π : n → n
- Finite sums and finite products of natural numbers, ∑_k<n aₖ and ∏_k<n aₖ in ℕ
- Laws of finite sums and products in ℕ, and ι(∑_k<n aₖ) = ∑_k<n ι(aₖ)
- Addition is commutative
- Sequences, convergence, Cauchyness, monotonicity, boundedness and closed intervals in an arbitrary ordered field
- Probability measures and probability spaces
- Finite probability spaces, outcome weights, events, and event probabilities
- A finite simple graph is a finite vertex set together with a set of two-element vertex subsets
- Adjacency, incidence, open and closed neighbourhoods, vertex degree, minimum degree and maximum degree
- The uniform probability space on a nonempty finite set
- Filtration and filtered probability space
- Discrete stopping time
- Independent random elements
- The Borel product of ℝᵐ and ℝⁿ is the Borel sigma-algebra of ℝᵐ⁺ⁿ
- The sigma-algebra generated by a function
- Walks, closed walks, trails, paths and cycles, with length equal to the number of traversed edges
- The finite union bound
- The adjacency matrix of a finite simple graph
- Finite weighted graph Laplacian
- Finite rectangular matrices over a commutative ring, their entries, rows and columns
- A finite sum in a commutative monoid indexed by an arbitrary finite set
2 · Logical flowchart
Arrows show item dependencies. A grouped prerequisite node points to items that use one or more of its members; their exact links are listed above.
3 · Items
TheoremLibrary prerequisite
The principle of mathematical induction
TheoremLibrary prerequisite
The integral logarithm is unbounded above and below
TheoremLibrary prerequisite
Intermediate value theorem, by bisection with a canonical left-half rule: a continuous function on [a,b] takes every value between f(a) and f(b)
TheoremLibrary prerequisite
Assuming countable choice, L(ℝⁿ) is a sigma-algebra containing every elementary set and λₙ is a complete measure extending elementary volume
TheoremLibrary prerequisite
A box in ℝⁿ with parameters aᵢ≤ bᵢ is Lebesgue measurable of measure ∏_i<n(bᵢ-aᵢ), whichever of its faces are included
TheoremLibrary prerequisite
Assuming countable choice, Lebesgue outer measure is an outer measure that restricts to elementary volume
TheoremLibrary prerequisite
Expectation is linear for every finite family of random variables, without any independence hypothesis
TheoremLibrary prerequisite
The Lebesgue integral is linear on L¹(μ)
TheoremLibrary prerequisite
The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t
TheoremLibrary prerequisite
The logarithm grows more slowly than every positive real power
TheoremLibrary prerequisite
Markov's inequality on a finite probability space
TheoremLibrary prerequisite
The mean value inequality: if f : [a,b] → ℝᵐ is continuous and differentiable on (a,b) with ‖ f'‖₂ ≤ M, then ‖ f(b)-f(a)‖₂ ≤ M(b-a)
TheoremLibrary prerequisite
Minkowski's inequality for integrals, including p = ∞
TheoremLibrary prerequisite
On an interval I, for f continuous on I and differentiable at every interior point: f' ≥ 0 throughout gives f nondecreasing, f' > 0 gives f increasing, f' ≤ 0 and f' < 0 give the two decreasing forms; conversely a nondecreasing f has f' ≥ 0 and a nonincreasing f has f' ≤ 0 wherever it is differentiable, and no strict converse is claimed
TheoremLibrary prerequisite
Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm
TheoremLibrary prerequisite
The operator norm is 0 on the zero domain and otherwise equals the largest singular value, attained at a right-singular vector
TheoremLibrary prerequisite
The sum of a real power series is real analytic throughout the open interval determined by its radius
TheoremLibrary prerequisite
Product weights normalize, and coordinate events are mutually independent
TheoremLibrary prerequisite
Quarter-turn values and shifts by pi/2 and pi
TheoremLibrary prerequisite
The reals form a totally ordered field
TheoremLibrary prerequisite
For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique
TheoremLibrary prerequisite
The addition formulas for sine and cosine
TheoremLibrary prerequisite
Signs, monotonicity intervals, and ranges of sine and cosine
TheoremLibrary prerequisite
The zero sets of sine and cosine and the least positive common period 2 pi
TheoremLibrary prerequisite
A subset of a finite set is finite, with | B| ≤ | A|, and equality holds if and only if B = A
TheoremLibrary prerequisite
The sum rule: a finite disjoint union is finite with | A ∪ B| = | A| + | B| and |⋃_i ∈ I Aᵢ| = ∑_i ∈ I| Aᵢ|, and a sum over a finite index set splits along a partition
DefinitionDependency level 0
Asymptotic quantifiers and uniform parameter ranges
DefinitionDependency level 0
Uniform edge orderings, graph-process times and independent labels
DefinitionDependency level 0