Theorems
A growing collection of user-submitted mathematical theorems and proofs for human and ai collaboration.
- The classes of power-integrable simple functions form a dense linear subspace of the Lebesgue space.
- The integral of the product is an inner product on the Lebesgue space of square-integrable classes, its induced norm is the 2-norm, and under dependent choice the space is a real Hilbert space.
- The Lebesgue space is a real normed space, and under dependent choice a real Banach space; without choice, a sequence of p-integrable functions that is Cauchy for the p-seminorm converges in it to a p-integrable function, along a subsequence also almost everywhere under a single…
- The Lebesgue space is the quotient of the p-integrable functions by almost-everywhere equality, with the operations, the norm and, for p = 2, the inner product computed on representatives.
- A norm on a real vector space is a nonnegative, definite, absolutely homogeneous real-valued function satisfying the triangle inequality; a real normed space is a real vector space with a norm.
- Linear combinations of p-integrable functions are p-integrable, and the p-seminorm of a sum is at most the sum of the p-seminorms.
- For conjugate exponents p and q, the product of a p-integrable and a q-integrable function is integrable, and the integral of its absolute value is at most the product of the seminorms; the case p = q = 2 is the Cauchy-Schwarz inequality.
- For p = 1 the p-integrable functions are the integrable ones; in general the p-th power of the seminorm is the integral of the p-th power, and the seminorm is absolutely homogeneous, respects almost-everywhere domination and equality, vanishes exactly on functions that are zero a…
- For a real exponent p >= 1, defines the p-th power of the absolute value of a measurable function, the set of measurable functions whose p-th power has finite integral, and the p-seminorm of such a function.
Approximation of Measurable Functions by Dyadic Simple Functions
lemmalem:simple-function-approximation-2026bAnalysisProbabilityThe dyadic maps min(m, 2^{-m} floor(2^m f)) are nonnegative simple functions increasing to a measurable f with values in [0,∞], approximate a bounded f uniformly, and, applied to the positive and negative parts, give simple functions dominated by |f| converging pointwise to a mea…- Integrals ignore null sets: a nonnegative map vanishing off a null set has integral zero, maps that agree or compare almost everywhere have equal or comparable integrals, and a nonnegative map has integral zero exactly when it vanishes almost everywhere. Also Markov's inequality,…
- Every real exponent p > 1 has a unique conjugate exponent q > 1 with 1/p + 1/q = 1, and for such p, q and nonnegative a, b the product ab is at most a^p/p + b^q/q.
Measurable Functions and the Lebesgue Integral: Standing Notation
settingset:measure-space-integration-2026bAnalysisProbabilityAdopts the integration notation of set:integration-notation and lists, clause by clause, the background results on measurable functions, simple functions, the Lebesgue integral, integrals over subsets, vector- and matrix-valued integrals, and Lebesgue measure on a closed interval…The Real Vector Space of Real-Valued Functions on a Set
lemmalem:real-valued-function-space-2026aLinear AlgebraThe real-valued functions on any set form a real vector space under pointwise operations, and a subset containing the zero function and closed under those operations is a linear subspace.- Real powers agree with natural powers, are positive, turn into multiples under the logarithm, obey the exponent and product laws, and for a positive exponent give a strictly increasing continuous bijection of the nonnegative reals.
- Defines the power of a positive real number with any real exponent through the exponential and the logarithm, and the power of zero with a positive exponent as zero.
The Scope of the First-Order Structure Condition
remarkrem:first-order-structure-condition-scope-2026aAnalysisPDEThe first-order structure condition asks for its inequality at all pairs of form arguments independently, which forces the operator to depend on that argument boundedly. An operator with an unbounded second-order term needs a structure condition stated only for the coupled pairs…Well-Posedness for a Hamilton-Jacobi Equation with a Monotone Nonlinearity on a Hilbert Triple
theoremthm:monotone-hamilton-jacobi-well-posed-hilbert-triple-2026aAnalysisPDEOn a Hilbert triple, the Hamilton-Jacobi equation with a monotone nonlinearity, a Lipschitz drift and a bounded cost that is uniformly continuous for the smaller norm has exactly one bounded continuous viscosity solution on the whole space. That solution is uniformly continuous f…A Uniformly Continuous Map Between Metric Spaces Is Continuous
lemmalem:uniformly-continuous-implies-continuous-2026bAnalysisTopologyA map from a subset of a metric space into a metric space that is uniformly continuous on the subset is continuous on it.A Hamilton-Jacobi Operator with a Monotone Nonlinearity and a Lipschitz Perturbation Satisfies the Comparison Hypotheses
propositionprop:monotone-hamilton-jacobi-hilbert-triple-2026aAnalysisPDEOn a Hilbert triple, the operator obtained by adding a monotone nonlinearity and a Lipschitz perturbation to the drift of the dissipative Hamilton-Jacobi operator is first order, strictly proper, satisfies the first-order structure condition with an explicit structure pair, satis…