How statement and proof provenance work

The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.

Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.

These labels describe origin, not correctness: citations and verification chips remain separate evidence.

✓ 21 results · all verified · 1 also independently AI-judged

Every result on this page is machine-checked by a proof checker and read in full and owner-audited; the judge is an additional, independent cross-model AI review of the proofs. The 20 not AI-judged were verified by owner audit (typically over a confirmed judge false positive), not failures.

The Logarithm and General Powers

1 · Prerequisites

2 · Summary

The exponential function is a continuous increasing bijection onto the positive reals. Its inverse, the natural logarithm, therefore inherits order and continuity; the exponential addition law becomes the logarithm's product, quotient, and reciprocal laws. Positive-base real powers are then defined by $a^{x} = \exp (x \log a)$ , reconciled with rational powers and with a rational-supremum construction, and differentiated directly.

The page develops the logarithmic power series, a square-summable infinite-product criterion, logarithmic growth, real-exponent $p$ -series, and a two-point exponential inequality. These yield weighted AM--GM, Young, Hölder, and Minkowski inequalities for finite real exponents. It concludes with hyperbolic functions, their identities and derivatives, and logarithm formulas for their inverse functions.

3 · Logical flowchart

4 · Definitions, theorems and proofs

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-02Open item page →

The natural logarithm as the inverse of the exponential function

Definition

For $x > 0$ , define $\log x$ to be the unique real $y$ such that $\exp (y) = x$ . This is well-defined because The exponential is a continuous bijection from $R$ onto $(0, \infty)$ states that $\exp : R \to (0, \infty)$ is a bijection.

Thus $\log : (0, \infty) \to R$ is the inverse function of $\exp$ . In particular, $\log (\exp y) = y$ for every $y \in R$ and $\exp (\log x) = x$ for every $x > 0$ .

Remarks

The domain is exactly $(0, \infty)$ . This definition assigns no real logarithm to $0$ or to a negative number.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm

Statement

The function $\log : (0, \infty) \to R$ is continuous and strictly increasing, is onto $R$ , and satisfies, for $x, y > 0$ , $\log (x y) = \log x + \log y, \log (x / y) = \log x - \log y, \log (1 / x) = - \log x .$ Also $\log 1 = 0$ .

Facts & Assumptions

Given: Positive reals $x, y$ .

[L1]

The exponential is a continuous strictly increasing bijection from $R$ onto $(0, \infty)$ , and $\log$ is its inverse (The natural logarithm as the inverse of the exponential function, 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] \to I$ is continuous and strictly monotone in the same sense as $f$ ).

[L2]

For all reals $u, v$ , $\exp (u + v) = \exp (u) \exp (v)$ (The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ ).

[L3]

$\exp (- u) = 1 / \exp (u)$ and $\exp (u) > 0$ for every real $u$ (The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

Proof

technique · direct

1.1

Since it is the inverse of the continuous strictly increasing exponential, $\log$ is continuous, strictly increasing, and maps $(0, \infty)$ onto $R$ .

1.2

The equality $\exp (\log x + \log y) = \exp (\log x) \exp (\log y) = x y = \exp (\log (x y))$ and injectivity of $\exp$ give $\log (x y) = \log x + \log y$ .

L1L2

2.1

Since $x / y = x (1 / y)$ and $\exp (- \log y) = 1 / y$ by [L3], step 1.2 gives $\log (x / y) = \log x - \log y$ and $\log (1 / x) = - \log x$ .

step 1.2L3

3.1

As $\exp (0) = 1$ , the inverse identity gives $\log 1 = 0$ .

L1∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t

Statement

For $x > 0$ , $\log$ is differentiable and $\log^{'} (x) = \frac{1}{x}, \log x = \int_{1}^{x} \frac{d t}{t} .$

Facts & Assumptions

Given: A positive real $x$ .

[L1]

If a differentiable injective function has nonzero derivative, its inverse is differentiable at an image point and its derivative is the reciprocal of the original derivative (Derivative of an inverse: if $f$ is continuous and injective on a nondegenerate interval $I$ and differentiable at $c \in I$ with $f^{'} (c) \neq 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)$ ).

[L2]

$\exp^{'} (u) = \exp (u)$ for every real $u$ (The exponential function is smooth and $(\exp)^{'} = \exp$ ).

[L3]

The reciprocal of a nonvanishing continuous real function is continuous, and the first FTC differentiates $x \mapsto \int_{1}^{x} f (t) d t$ when $f$ is continuous (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, 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: $\int_{a}^{a} f : = 0$ and $\int_{b}^{a} f : = - \int_{a}^{b} f$ ).

[L4]

A differentiable real function with zero derivative on an interval is constant (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).

Proof

technique · direct

1.1

At $u = \log x$ , $\exp^{'} (u) = \exp (u) = x \neq 0$ ; hence the inverse rule gives $\log^{'} (x) = 1 / \exp (\log x) = 1 / x$ .

L1L2

1.2

The function $t \mapsto 1 / t$ is continuous on $(0, \infty)$ , so $I (x) : = \int_{1}^{x} d t / t$ satisfies $I^{'} (x) = 1 / x$ and $I (1) = 0$ .

2.1

The difference $x \mapsto \log x - I (x)$ has derivative zero on $(0, \infty)$ , and is zero at $1$ , so it is identically zero.

step 1.1step 1.2L4∎

TheoremStatement: Literature-sourcedProof: AI-adaptedprecheck passjudge pass (deepseek-v4-pro + gpt-5.6-terra)audited 2026-08-14Open item page →

The Euler–Mascheroni constant and the harmonic asymptotic

Statement

For $n \geq 1$ , let

$H_{n} = \sum_{k = 1}^{n} \frac{1}{k}, γ_{n} = H_{n} - \log n .$

The sequence $(γ_{n})$ is strictly decreasing and is bounded below by $1 - \log 2$ . It therefore converges to a constant $γ$ satisfying $0 < γ < 1$ , and

$H_{n} = \log n + γ + o (1) .$

Consequently, $H_{n} / \log n \to 1$ as $n \to \infty$ , with the quotient considered for $n \geq 2$ .

Facts & Assumptions

Given: The sequences $(H_{n})$ and $(γ_{n})$ displayed in the statement.

[A1]

For every $n \geq 1$ , $H_{n} = \sum_{k = 1}^{n} 1 / k$ and $γ_{n} = H_{n} - \log n$ .

[L1]

For $x > 0$ , $\log x = \int_{1}^{x} d t / t$ , and the derivative of $\log$ is $1 / x$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[L2]

Let $a < b$ and let $f, g : [a, b] \to R$ be integrable. If $f (x) \geq 0$ for every $x \in [a, b]$ , then $\int_{a}^{b} f \geq 0$ ; if $f (x) \leq g (x)$ for every $x \in [a, b]$ , then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and if $m \leq f (x) \leq M$ for every $x \in [a, b]$ , with $m, M$ real, then $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ (If $f \leq g$ on $[a, b]$ and both are integrable then $\int_{a}^{b} f \leq \int_{a}^{b} g$ ; and $m (b - a) \leq \int_{a}^{b} f \leq M (b - a)$ ).

[L3]

If $a < c < b$ , then a bounded function on $[a, b]$ is integrable there exactly when its restrictions to $[a, c]$ and $[c, b]$ are integrable, and in that case $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ (For $a < c < b$ : $f$ is integrable on $[a, b]$ if and only if it is integrable on $[a, c]$ and on $[c, b]$ , and then $\int_{a}^{b} f = \int_{a}^{c} f + \int_{c}^{b} f$ ; with the oriented form for arbitrary $a, b, c$ ).

[L4]

Every nonincreasing real sequence that is bounded below converges to its infimum (A nondecreasing sequence bounded above converges to the supremum of its range, and a nonincreasing sequence bounded below to the infimum).

Proof

technique · direct

1.1

For every $n \geq 1$ , $γ_{n + 1} - γ_{n} = 1 / (n + 1) - \int_{n}^{n + 1} d t / t$ .

A1L1L3algebra

1.2

Splitting the integral at $n + 1 / 2$ gives $\int_{n}^{n + 1} d t / t \geq (1 / 2) / (n + 1 / 2) + (1 / 2) / (n + 1) > 1 / (n + 1)$ .

L2L3algebra

1.3

If $n \geq 2$ , additivity and $1 / t \leq 1 / k$ on $[k, k + 1]$ give $\log n = \log 2 + \sum_{k = 2}^{n - 1} \int_{k}^{k + 1} d t / t \leq \log 2 + \sum_{k = 2}^{n - 1} 1 / k$ , where the sum is empty when $n = 2$ ; thus $γ_{n} \geq 1 - \log 2 + 1 / n > 1 - \log 2$ .

A1L1L2L3algebra

1.4

Splitting $[1, 2]$ at $3 / 2$ gives $\log 2 = \int_{1}^{2} d t / t \leq 1 / 2 + 1 / 3 = 5 / 6 < 1$ ; in particular, $γ_{1} = 1 \geq 1 - \log 2 > 0$ .

A1L1L2L3algebra

1.5

For every integer $m \geq 1$ , splitting $[1, 2^{m}]$ into $[2^{j}, 2^{j + 1}]$ gives $\log (2^{m}) = \sum_{j = 0}^{m - 1} \int_{2^{j}}^{2^{j + 1}} d t / t \geq \sum_{j = 0}^{m - 1} 1 / 2 = m / 2$ .

L1L2L3algebra

2.1

Hence $γ_{n + 1} < γ_{n}$ for every $n \geq 1$ .

step 1.1step 1.2algebra

2.2

Therefore $γ_{n} \geq 1 - \log 2$ for every $n \geq 1$ .

step 1.3step 1.4

2.3

It follows that $\log n \to \infty$ . Let $m \geq 1$ and $n \geq 2^{m}$ . If $n = 2^{m}$ then $\log n = \log (2^{m})$ . If $n > 2^{m}$ then $1 < 2^{m} < n$ , so $\log n = \int_{1}^{n} d t / t = \int_{1}^{2^{m}} d t / t + \int_{2^{m}}^{n} d t / t = \log (2^{m}) + \int_{2^{m}}^{n} d t / t$ , and $1 / t \geq 0$ on $[2^{m}, n]$ makes that last integral nonnegative. Either way $\log n \geq \log (2^{m}) \geq m / 2$ .

L1L2L3step 1.5algebra

3.1

By monotone convergence, there is a real number $γ$ such that $γ_{n} \to γ$ .

L4step 2.1step 2.2

3.2

The lower bound and strict decrease give $0 < γ_{n} \leq γ_{1} = 1$ for every $n \geq 1$ .

step 1.4step 2.1step 2.2

4.1

Since $γ$ is the infimum of the $γ_{n}$ , $γ \geq 1 - \log 2 > 0$ ; and since the sequence is strictly decreasing, $γ \leq γ_{2} < γ_{1} = 1$ . Hence $0 < γ < 1$ .

step 1.4step 2.1step 2.2step 3.1algebra

4.2

The identity $H_{n} = \log n + γ_{n}$ and the convergence $γ_{n} \to γ$ give $H_{n} = \log n + γ + (γ_{n} - γ) = \log n + γ + o (1)$ .

A1step 3.1algebra

4.3

Consequently, $γ_{n} / \log n \to 0$ as $n \to \infty$ .

step 2.3step 3.2algebra

5.1

Finally, for $n \geq 2$ , $H_{n} / \log n = 1 + γ_{n} / \log n \to 1$ .

A1step 4.3algebra∎

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-02Open item page →

Real powers for positive bases, with the zero-base positive-exponent convention

Definition

For $a > 0$ and $x \in R$ , define $a^{x} : = \exp (x \log a) .$ For the supplementary zero-base convention, define $0^{x} : = 0$ when $x > 0$ .

The expressions $0^{0}$ and $0^{x}$ for $x < 0$ are left undefined. Negative bases are not assigned arbitrary real powers.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

The exponential definition of real powers agrees with the existing rational powers

Statement

If $a > 0$ and $r \in Q$ , then the real power $a^{r} = \exp (r \log a)$ agrees with the rational power of Rational powers $a^{r}$ of a positive base. For $r > 0$ , both conventions also give $0^{r} = 0$ .

Facts & Assumptions

Given: A positive real $a$ and a rational $r = p / q$ with $q \geq 1$ .

[L1]

Rational powers satisfy $(a^{p / q})^{q} = a^{p}$ , are positive for positive base, and obey the rational power laws (Rational powers $a^{r}$ of a positive base, Laws of rational exponents).

[L2]

For positive reals, $\log (x y) = \log x + \log y$ , $\log (1 / x) = - \log x$ , and $\log$ is injective (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L3]

The real-power definition is $a^{u} = \exp (u \log a)$ (Real powers for positive bases, with the zero-base positive-exponent convention).

Proof

technique · direct

1.1

For $q \geq 1$ , the product law for $\log$ gives $\log ((a^{p / q})^{q}) = q \log (a^{p / q}) = p \log a = \log (a^{p})$ .

L1L2

2.1

Injectivity of $\log$ gives $\log (a^{p / q}) = (p / q) \log a$ , and exponentiating gives $a^{p / q} = \exp ((p / q) \log a)$ .

step 1.1L2L3

3.1

This is the new real power at exponent $p / q$ ; negative rational exponents follow by reciprocals, and the stated $0^{r}$ convention agrees with Rational powers $a^{r}$ of a positive base for $r > 0$ .

step 2.1L1L3∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents

Statement

For $a, b > 0$ and $r, s \in R$ , $a^{r + s} = a^{r} a^{s}, (a b)^{r} = a^{r} b^{r}, (a / b)^{r} = a^{r} / b^{r}, (a^{r})^{s} = a^{r s} .$

Facts & Assumptions

Given: Positive reals $a, b$ and real exponents $r, s$ .

[L1]

$a^{u} = \exp (u \log a)$ for $a > 0$ (Real powers for positive bases, with the zero-base positive-exponent convention).

[L2]

$\log (a b) = \log a + \log b$ , $\log (a / b) = \log a - \log b$ , and $\log (\exp u) = u$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L3]

$\exp (u + v) = \exp (u) \exp (v)$ and $\exp (- u) = 1 / \exp (u)$ (The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

Proof

technique · direct

1.1

Expanding $a^{r + s}$ by [L1] and applying [L3] gives $a^{r + s} = \exp (r \log a) \exp (s \log a) = a^{r} a^{s}$ .

L1L3

1.2

Expanding $(a b)^{r}$ and using $\log (a b) = \log a + \log b$ gives $(a b)^{r} = a^{r} b^{r}$ .

L1L2L3

1.3

The same calculation with $\log (a / b) = \log a - \log b$ and [L3] gives $(a / b)^{r} = a^{r} / b^{r}$ .

L1L2L3

2.1

Since $\log (a^{r}) = \log (\exp (r \log a)) = r \log a$ , expanding $(a^{r})^{s}$ gives $a^{r s}$ .

L1L2∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

Continuity and derivatives of positive-base real powers

Statement

For $a > 0$ , the function $x \mapsto a^{x}$ is continuous on $R$ and $(a^{x})^{'} = a^{x} \log a .$ For $α \in R$ , the function $x \mapsto x^{α}$ is continuous and differentiable on $(0, \infty)$ , with $(x^{α})^{'} = α x^{α - 1} .$

Facts & Assumptions

Given: A positive base $a$ , a real exponent $α$ , and $x > 0$ .

[L1]

$a^{x} = \exp (x \log a)$ and $x^{α} = \exp (α \log x)$ (Real powers for positive bases, with the zero-base positive-exponent convention).

[L2]

$\log^{'} (x) = 1 / x$ on $(0, \infty)$ and $\exp^{'} (u) = \exp (u)$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, The exponential function is smooth and $(\exp)^{'} = \exp$ ).

[L3]

The chain rule and algebra of derivatives apply to differentiable real functions, and differentiability implies continuity (The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ , A function differentiable at $c$ is continuous at $c$ ).

Proof

technique · direct

1.1

The chain rule applied to $a^{x} = \exp (x \log a)$ gives $(a^{x})^{'} = \exp (x \log a) \log a = a^{x} \log a$ .

L1L2L3

1.2

The chain rule applied to $x^{α} = \exp (α \log x)$ gives $(x^{α})^{'} = \exp (α \log x) α / x = α x^{α - 1}$ .

L1L2L3

2.1

Both functions are continuous on their stated domains because the displayed derivatives exist there.

step 1.1step 1.2L3∎

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-02Open item page →

The logarithm to a positive base other than one

Definition

For $b > 0$ with $b \neq 1$ and $x > 0$ , define $\log_{b} x : = \frac{\log x}{\log b} .$

The denominator is nonzero: $\log b = 0$ would imply $b = \exp (0) = 1$ by the inverse identities of The natural logarithm as the inverse of the exponential function.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

Change of base and inversion of the positive-base real exponential

Statement

If $b > 0$ , $b \neq 1$ , and $x > 0$ , then $\log_{b} x = \frac{\log x}{\log b}, b^{\log_{b} x} = x, \log_{b} (b^{u}) = u (u \in R) .$ In particular, $\log_{b} x = \log_{c} x / \log_{c} b$ for every second base $c > 0$ , $c \neq 1$ .

Facts & Assumptions

Given: $b, c > 0$ with $b, c \neq 1$ , $x > 0$ , and $u \in R$ .

[L1]

$\log_{b} x = \log x / \log b$ , with $\log b \neq 0$ (The logarithm to a positive base other than one).

[L2]

$b^{v} = \exp (v \log b)$ and the real-power laws hold for positive bases (Real powers for positive bases, with the zero-base positive-exponent convention, The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents).

[L3]

$\log (\exp v) = v$ and $\exp (\log x) = x$ for $x > 0$ (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

Proof

technique · direct

1.1

By [L1] and [L2], $b^{\log_{b} x} = \exp ((\log x / \log b) \log b) = \exp (\log x) = x$ .

L1L2L3

1.2

Likewise $\log_{b} (b^{u}) = \log (\exp (u \log b)) / \log b = u$ .

L1L2L3

2.1

Dividing $\log x$ first by $\log c$ and then by $\log b / \log c$ gives $\log_{b} x = \log_{c} x / \log_{c} b$ .

L1algebra∎

DefinitionDefinition: AI-adaptedProof: Not applicableverified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

Real powers from suprema of rational powers, with the reciprocal convention below base one

Definition

For $a > 1$ and $x \in R$ , set $S_{a} (x) : = {a^{q} : q \in Q, q < x}, a^{[x]} : = \sup S_{a} (x) .$ The set is nonempty because a rational lies below $x$ (The rationals embed densely in the reals). It is bounded above: choose a natural $m > x$ (Every complete ordered field is Archimedean), so every $q < x$ satisfies $q < m$ and $a^{q} \leq a^{m}$ (Monotonicity of $r \mapsto a^{r}$ and of $a \mapsto a^{r}$ ). The supremum therefore exists in $R$ by the least-upper-bound property of a complete ordered field (Complete ordered field (least-upper-bound property), Upper bound, least upper bound, and strict upper bound), and it is strictly positive, because it is at least the element $a^{q}$ of $S_{a} (x)$ for any rational $q < x$ and every rational power of a positive base is positive (Rational powers $a^{r}$ of a positive base).

For $0 < a < 1$ , define $a^{[x]} : = 1 / ((a^{- 1})^{[x]})$ ; for $a = 1$ , define $1^{[x]} : = 1$ . The notation $a^{[x]}$ distinguishes this rational-supremum construction from the exponential construction until their agreement is proved.

Remarks

The direct supremum formula is intentionally restricted to $a > 1$ . When $0 < a < 1$ , the set ${a^{q} : q < x}$ is unbounded above as $q$ tends to negative infinity.

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passverified 2026-08-04 (gpt-5.6-sol-codex-subscription)Open item page →

The rational-supremum construction of real powers agrees with the exponential construction

Statement

For every $a > 0$ and $x \in R$ , the rational-supremum value $a^{[x]}$ of Real powers from suprema of rational powers, with the reciprocal convention below base one equals the exponential real power $a^{x}$ of Real powers for positive bases, with the zero-base positive-exponent convention.

Facts & Assumptions

Given: A real $x$ and a positive base $a$ .

[L1]

For $a > 1$ , $S_{a} (x) : = {a^{q} : q \in Q, q < x}$ and $a^{[x]} : = \sup S_{a} (x)$ ; for $0 < a < 1$ , $a^{[x]} : = 1 / ((a^{- 1})^{[x]})$ ; and $1^{[x]} : = 1$ (Real powers from suprema of rational powers, with the reciprocal convention below base one).

[L2]

Rational powers agree with exponential real powers, and $t \mapsto a^{t}$ is continuous; if $a > 1$ , then $\log a > 0$ , so $t \mapsto a^{t} = \exp (t \log a)$ is strictly increasing (The exponential definition of real powers agrees with the existing rational powers, Continuity and derivatives of positive-base real powers, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The exponential function is strictly increasing, Real powers for positive bases, with the zero-base positive-exponent convention).

[L3]

Rational numbers are dense in $R$ , and the epsilon characterisation identifies a supremum of a nonempty bounded-above set (The rationals embed densely in the reals, Epsilon characterisation of the supremum).

[L4]

For $a, b > 0$ and $r, s \in R$ : $a^{r + s} = a^{r} a^{s}$ , $(a b)^{r} = a^{r} b^{r}$ , $(a / b)^{r} = a^{r} / b^{r}$ , and $(a^{r})^{s} = a^{r s}$ (The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents).

Proof

technique · direct

1.1

Assume $a > 1$ . For every rational $q < x$ , strict increase of $t \mapsto a^{t}$ gives $a^{q} < a^{x}$ , so $a^{x}$ is an upper bound of $S_{a} (x)$ .

L1L2

1.2

Given $ε > 0$ , continuity of $t \mapsto a^{t}$ at $x$ supplies $δ > 0$ such that $∣ t - x ∣ < δ$ implies $∣ a^{t} - a^{x} ∣ < ε$ ; density supplies rational $q$ with $x - δ < q < x$ , hence $a^{x} - ε < a^{q} \in S_{a} (x)$ .

L2L3choose

2.1

By the supremum characterisation, steps 1.1 and 1.2 give $a^{[x]} = a^{x}$ when $a > 1$ .

step 1.1step 1.2L3

3.1

For $a = 1$ both values are $1$ . For $0 < a < 1$ the base $a^{- 1}$ exceeds $1$ , so step 2.1 applied to that base and the same exponent $x$ gives $(a^{- 1})^{[x]} = (a^{- 1})^{x}$ ; the subunit clause of [L1] then gives $a^{[x]} = 1 / ((a^{- 1})^{x})$ . By [L4] with $r = - 1$ and $s = x$ , $(a^{- 1})^{x} = a^{- x}$ ; and by [L4] again, $a^{- x} a^{x} = a^{- x + x} = a^{0} = 1$ , so $1 / a^{- x} = a^{x}$ . Hence $a^{[x]} = a^{x}$ .

step 2.1L1L2L4∎

CorollaryStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

Every rational approximation to a real exponent gives the same limiting real power

Statement

Let $a > 0$ , let $x \in R$ , and let $(q_{n})$ be a rational sequence converging to $x$ . Then $a^{q_{n}} \to a^{x}$ . Hence the limit is independent of the rational approximating sequence and equals the rational-supremum value $a^{[x]}$ .

Facts & Assumptions

Given: $a > 0$ , $x \in R$ , and rational $q_{n} \to x$ .

[L1]

The rational-supremum and exponential constructions agree (The rational-supremum construction of real powers agrees with the exponential construction).

[L2]

Rational powers agree with real powers, and $t \mapsto a^{t}$ is continuous (The exponential definition of real powers agrees with the existing rational powers, Continuity and derivatives of positive-base real powers).

Proof

technique · direct

1.1

For every $n$ , rational-exponent agreement gives $a^{q_{n}} = \exp (q_{n} \log a)$ .

1.2

Continuity of $t \mapsto a^{t}$ gives $a^{q_{n}} \to a^{x}$ .

2.1

Since $a^{[x]} = a^{x}$ , this limit is independent of the chosen rational sequence and has the asserted supremum value.

step 1.2L1∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

Landau's root limit: log x is the limit of 2^n times (x^(1/2^n) minus 1)

Statement

For every $x > 0$ , $\log x = \lim_{n \to \infty} 2^{n} (x^{1 / 2^{n}} - 1) .$

Facts & Assumptions

Given: A positive real $x$ .

[L1]

$x^{r} = \exp (r \log x)$ for real $r$ , and this agrees with rational powers (Real powers for positive bases, with the zero-base positive-exponent convention, The exponential definition of real powers agrees with the existing rational powers).

[L2]

$\exp^{'} (0) = 1$ , so $\lim_{h \to 0} (\exp h - 1) / h = 1$ (The exponential function is smooth and $(\exp)^{'} = \exp$ , The derivative $f^{'} (c) = \lim_{x \to c} \frac{f (x) - f (c)}{x - c}$ of $f : A \to R$ at a point $c \in A$ that is a limit point of $A$ , and differentiability on a set).

[L3]

$(1 / 2)^{n} \to 0$ , and limits respect sums, products, and scalar multiples (For $∣ r ∣ < 1$ the sequence $r^{k}$ is null, and for $∣ r ∣ > 1$ the sequence $∣ r ∣^{k}$ diverges to $+ \infty$ , Algebra of limits: sums, scalar multiples, products and quotients).

Proof

technique · direct

1.1

If $x = 1$ , every displayed summand is $0$ , so the limit is $\log 1 = 0$ .

L1algebra

1.2

Suppose $x \neq 1$ and put $h_{n} = (\log x) / 2^{n}$ . Then $h_{n} \to 0$ and $x^{1 / 2^{n}} = \exp (h_{n})$ .

L1L3

2.1

We have $2^{n} (x^{1 / 2^{n}} - 1) = \log x (\exp (h_{n}) - 1) / h_{n}$ .

step 1.2algebra

3.1

The derivative limit in [L2] makes the right-hand side tend to $\log x$ , proving the claim together with step 1.1.

step 1.1step 2.1L2∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

The power series for log(1+x) on (-1,1], including the Abel endpoint

Statement

For $- 1 < x \leq 1$ , $\log (1 + x) = \sum_{n = 1}^{\infty} \frac{(- 1)^{n + 1} x^{n}}{n} .$ The series converges at $x = 1$ to $\log 2$ and diverges at $x = - 1$ .

Facts & Assumptions

Given: A real $x$ with $- 1 < x < 1$ .

[L1]

$\log^{'} (u) = 1 / u$ on $(0, \infty)$ , so $(\log (1 + x))^{'} = 1 / (1 + x)$ and $\log 1 = 0$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t).

[L2]

For $∣ x ∣ < 1$ , $\sum_{n \geq 0} (- x)^{n} = 1 / (1 + x)$ (For $∣ r ∣ < 1$ , $\sum_{k \geq 0} r^{k} = 1 / (1 - r)$ , and for $∣ r ∣ \geq 1$ the series diverges).

[L3]

A real power series may be integrated term by term inside its radius of convergence (Inside its radius a real power series may be integrated term by term on every closed subinterval).

[L4]

The alternating harmonic series converges, Abel's limit theorem identifies the limit at $r ↑ 1$ of a convergent power series with its sum, and the harmonic series diverges (The alternating series test: if $(b_{k})$ is nonincreasing with $b_{k} \to 0$ then $\sum_{k} (- 1)^{k} b_{k}$ converges, the sum lies between any two consecutive partial sums, and the error after $n$ terms is at most $b_{n}$ , Abel's limit theorem: if a real series converges to $s$ , then its power series tends to $s$ as $x ↑ 1$ , For rational $p > 0$ , $\sum 1 / k^{p}$ converges iff $p > 1$ ).

Proof

technique · direct

1.1

Integrating the series of [L2] from $0$ to $x$ gives $\sum_{n \geq 1} (- 1)^{n + 1} x^{n} / n$ .

L2L3

2.1

By [L1], the integral of $1 / (1 + t)$ from $0$ to $x$ is $\log (1 + x)$ , so the displayed series formula holds for $- 1 < x < 1$ .

L1step 1.1

3.1

At $x = 1$ the series is alternating harmonic and converges by [L4]; Abel's theorem and step 2.1 identify its sum with $\log 2$ .

step 2.1L4

4.1

At $x = - 1$ every term is $- 1 / n$ , so the series is the negative harmonic series and diverges.

L4algebra∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

Under square summability, the signed product of (1+p_n) converges iff the series of p_n converges

Statement

Let $(p_{n})$ be a real sequence such that $\sum_{n} p_{n}^{2}$ converges. Then $\prod_{n} (1 + p_{n}) converges ⟺ \sum_{n} p_{n} converges .$ The product uses the tail convention of Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors, so finitely many zero factors are allowed.

Facts & Assumptions

Given: A real sequence $(p_{n})$ with $\sum_{n} p_{n}^{2}$ convergent.

[L1]

A convergent series has terms tending to zero (If a series converges then its terms tend to $0$ ).

[L2]

$\log (1 + t) = t + \sum_{k \geq 2} (- 1)^{k + 1} t^{k} / k$ for $∣ t ∣ < 1$ ([The power series for log(1+x) on (-1,1], including the Abel endpoint](/item/thm-log-one-plus-x-power-series)).

[L3]

Direct comparison and absolute convergence give convergence of a series dominated by a convergent nonnegative series (If $0 \leq a_{k} \leq b_{k}$ eventually, convergence of $\sum b_{k}$ gives convergence of $\sum a_{k}$ , and divergence of $\sum a_{k}$ gives divergence of $\sum b_{k}$ , If $\sum ∣ a_{k} ∣$ converges then $\sum a_{k}$ converges).

[L4]

Convergent series are closed under termwise addition and subtraction, and deleting a finite initial segment preserves convergence (Convergent series add and scale termwise, A series converges iff each of its tail series converges, and the sum splits as $s_{N}$ plus the $N$ -th tail, Series, partial sums, convergence and the sum, divergence, and the tail series).

[L5]

$\exp (u + v) = \exp (u) \exp (v)$ , while $\exp$ and $\log$ are continuous inverse functions on their stated domains (The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , The exponential function is strictly increasing, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L6]

An infinite product converges when a tail of nonzero factors has nonzero limiting tail products; initial factors may be arbitrary (Infinite products: partial products, and convergence to a nonzero limit after finitely many vanishing factors).

Proof

technique · direct

1.1

By [L1], choose $N$ such that $∣ p_{n} ∣ \leq 1 / 2$ for $n \geq N$ ; then $1 + p_{n} \geq 1 / 2 > 0$ on that tail.

L1choose

1.2

For $∣ t ∣ \leq 1 / 2$ , the tail of the series in [L2] has absolute value at most $\sum_{k \geq 2} ∣ t ∣^{k} \leq 2 t^{2}$ , hence $∣ \log (1 + t) - t ∣ \leq 2 t^{2}$ .

L2algebra

1.3

Conversely, a nonzero limit of those positive tail products has a logarithm; continuity of $\log$ and the same finite-product identity make the tail logarithm partial sums converge.

L5L6

2.1

Applying step 1.2 to $p_{n}$ and using [L3] shows that $\sum_{n \geq N} (\log (1 + p_{n}) - p_{n})$ converges absolutely.

step 1.1step 1.2L3

3.1

By [L4], $\sum_{n} p_{n}$ converges if and only if $\sum_{n \geq N} \log (1 + p_{n})$ converges.

step 2.1L4

4.1

The $m$ -th tail product equals $\exp (\sum_{n = N}^{N + m - 1} \log (1 + p_{n}))$ by repeated use of [L5], so convergence of the logarithm series gives a nonzero tail-product limit.

step 3.1L5L6

5.1

Steps 3.1, 4.1, and 1.3 prove both directions, and [L6] makes finite initial zero factors harmless.

step 3.1step 4.1step 1.3L6∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

The logarithm grows more slowly than every positive real power

Statement

For every $α > 0$ , $\lim_{x \to + \infty} \frac{\log x}{x^{α}} = 0.$

Facts & Assumptions

Given: A real $α > 0$ .

[L1]

$\exp (t)$ tends to $+ \infty$ as $t \to + \infty$ , and its range is $(0, \infty)$ (The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ , The natural logarithm as the inverse of the exponential function).

[L2]

For $a > 0$ , $t / \exp (a t) \to 0$ as $t \to + \infty$ (The exponential dominates every fixed nonnegative integer power at $+ \infty$ ).

[L3]

$x^{α} = \exp (α \log x)$ for $x > 0$ , and algebra of limits permits substitution through the displayed identities (Real powers for positive bases, with the zero-base positive-exponent convention, Algebra of limits: sums, scalar multiples, products and quotients).

Proof

technique · direct

1.1

Put $t = \log x$ . As $x \to + \infty$ , the inverse relation and [L1] give $t \to + \infty$ .

1.2

By [L3], $\log x / x^{α} = t / \exp (α t)$ .

2.1

The right-hand side tends to $0$ by [L2], which proves the claim.

step 1.1step 1.2L2∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

The p-series for a real exponent p converges exactly when p is greater than one

Statement

For every real $p$ , $\sum_{k \geq 1} \frac{1}{k^{p}} converges ⟺ p > 1.$

Facts & Assumptions

Given: A real exponent $p$ .

[L1]

The integral test applies to a nonnegative nonincreasing function on $[0, \infty)$ and compares convergence with boundedness of its proper-integral sequence (The integral test: for $f \geq 0$ nonincreasing on $[0, \infty)$ , $\sum_{k} f (k)$ converges if and only if the sequence $(\int_{0}^{N} f)_{N}$ is bounded, with $\int_{0}^{N} f \leq \sum_{k < N} f (k) \leq f (0) + \int_{0}^{N} f$ ).

[L2]

Positive-base real powers are continuous and differentiable, with the stated power laws (Continuity and derivatives of positive-base real powers, The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents).

[L3]

$\int_{1}^{x} d t / t = \log x$ , and $\log x \to + \infty$ as $x \to + \infty$ (The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm, The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ ).

[L4]

A convergent series has terms tending to zero (If a series converges then its terms tend to $0$ ).

Proof

technique · direct

1.1

If $p \leq 0$ , then $1 / k^{p} \geq 1$ for $k \geq 1$ , so the terms do not tend to zero and the series diverges.

L2L4

1.2

Suppose $p > 0$ and set $f (t) = (t + 1)^{- p}$ . By [L2] this is nonnegative and nonincreasing on $[0, \infty)$ , and its sampled series is $\sum_{k \geq 0} 1 / (k + 1)^{p}$ .

L1L2

2.1

If $p = 1$ , then $\int_{0}^{N} f (t) d t = \log (N + 1)$ , which is unbounded by [L3].

step 1.2L3

2.2

If $p \neq 1$ , the power derivative gives $\int_{0}^{N} f (t) d t = ((N + 1)^{1 - p} - 1) / (1 - p)$ ; this is bounded exactly when $p > 1$ , using the exponential limits in [L3].

step 1.2L2L3

3.1

The integral test gives convergence exactly for $p > 1$ when $p > 0$ , and step 1.1 handles $p \leq 0$ .

step 1.1step 2.1step 2.2L1∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

The two-point convexity inequality for the exponential function

Statement

For all $x, y \in R$ and $0 \leq t \leq 1$ , $\exp ((1 - t) x + t y) \leq (1 - t) \exp x + t \exp y .$ If $0 < t < 1$ , equality holds exactly when $x = y$ .

Facts & Assumptions

Given: Reals $x, y$ and $t \in [0, 1]$ .

[L1]

$\exp^{'} = \exp$ ; the chain rule differentiates compositions, and the algebra of derivatives differentiates finite linear combinations (The exponential function is smooth and $(\exp)^{'} = \exp$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[L2]

The mean value theorem applies on a closed interval to a function differentiable in its interior (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 \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[L3]

The exponential is positive and strictly increasing (The exponential function is strictly increasing).

Proof

technique · direct

1.1

Put $d = y - x$ and $g (s) = 1 - s + s \exp d - \exp (s d)$ . Then $g (0) = g (1) = 0$ and $g^{''} (s) = - d^{2} \exp (s d) \leq 0$ .

L1L3

2.1

If $0 < s < 1$ , apply the mean value theorem to $g$ on $[0, s]$ and $[s, 1]$ ; since $g^{'}$ is nonincreasing by the mean value theorem applied to $g^{'}$ , their slopes give $g (s) / s \geq - g (s) / (1 - s)$ , hence $g (s) \geq 0$ .

step 1.1L1L2

3.1

Multiplying by $\exp x > 0$ converts $g (t) \geq 0$ into the displayed inequality.

step 2.1L3

4.1

When $0 < t < 1$ and $d \neq 0$ , $g^{''} < 0$ , so the slope comparison is strict and $g (t) > 0$ ; when $d = 0$ , equality is immediate.

step 1.1step 2.1L3∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

The weighted arithmetic-geometric mean inequality for real weights

Statement

Let $n \geq 1$ , let $x_{1}, \dots, x_{n} > 0$ , and let $w_{1}, \dots, w_{n} \geq 0$ satisfy $\sum_{i = 1}^{n} w_{i} = 1$ . Then $\prod_{i = 1}^{n} x_{i}^{w_{i}} \leq \sum_{i = 1}^{n} w_{i} x_{i} .$

Facts & Assumptions

Given: Positive reals $x_{i}$ and nonnegative real weights $w_{i}$ summing to $1$ .

[L1]

The two-point exponential inequality holds for every weight in $[0, 1]$ (The two-point convexity inequality for the exponential function).

[L2]

Positive-base real powers and their product laws are $x^{r} = \exp (r \log x)$ and the laws of The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents (Real powers for positive bases, with the zero-base positive-exponent convention, Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L3]

Mathematical induction is valid on natural numbers (The principle of mathematical induction).

Proof

technique · induction

1.1

For $n = 1$ , $w_{1} = 1$ and both sides are $x_{1}$ .

basegiven

1.2

Assume the result for $n$ positive entries. For weights $w_{1}, \dots, w_{n + 1}$ , if $w_{n + 1} = 1$ the claim is immediate; otherwise put $W = 1 - w_{n + 1} > 0$ , $v_{i} = w_{i} / W$ for $i \leq n$ , and $P : = \prod_{i = 1}^{n} x_{i}^{v_{i}}$ .

ihgiven

1.3

Applying [L1] to $\log P, \log x_{n + 1}$ with weights $W, w_{n + 1}$ gives $P^{W} x_{n + 1}^{w_{n + 1}} \leq W P + w_{n + 1} x_{n + 1}$ .

L1L2

2.1

The $v_{i}$ are nonnegative and sum to one, so the induction hypothesis gives $P \leq A : = \sum_{i = 1}^{n} v_{i} x_{i}$ .

step 1.2ih

3.1

The left side in step 1.3 is $\prod_{i = 1}^{n + 1} x_{i}^{w_{i}}$ , and step 2.1 makes its right side at most $\sum_{i = 1}^{n + 1} w_{i} x_{i}$ .

step 2.1step 1.3L2algebra

4.1

The base and induction steps prove the inequality for every $n \geq 1$ .

step 1.1step 3.1L3discharge-induction∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

Young's inequality for conjugate real exponents

Statement

Let $p, q > 1$ satisfy $1 / p + 1 / q = 1$ . For $u, v \geq 0$ , $u v \leq \frac{u^{p}}{p} + \frac{v^{q}}{q} .$

Facts & Assumptions

Given: Conjugate real exponents $p, q > 1$ and nonnegative reals $u, v$ .

[L1]

Weighted AM-GM applies to positive entries with nonnegative weights summing to one (The weighted arithmetic-geometric mean inequality for real weights).

[L2]

Positive-base real-power laws hold, and the zero-base convention is $0^{r} = 0$ for $r > 0$ ; positive-base real powers are positive (Real powers for positive bases, with the zero-base positive-exponent convention, The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents, The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

Proof

technique · direct

1.1

If $u = 0$ or $v = 0$ , the inequality is immediate from nonnegativity of the two terms on the right.

1.2

For $u, v > 0$ , apply [L1] to $u^{p}, v^{q}$ with weights $1 / p, 1 / q$ .

L1given

2.1

Its geometric side is $(u^{p})^{1 / p} (v^{q})^{1 / q} = u v$ , and its arithmetic side is $u^{p} / p + v^{q} / q$ .

step 1.2L2

3.1

Steps 1.1 and 2.1 cover all nonnegative $u, v$ .

step 1.1step 2.1∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

Holder's inequality for finite sums and conjugate real exponents

Statement

Let $p, q > 1$ with $1 / p + 1 / q = 1$ . For real families $(a_{i})_{i < n}$ and $(b_{i})_{i < n}$ , $\sum_{i < n} ∣ a_{i} b_{i} ∣ \leq {(\sum_{i < n} ∣ a_{i} ∣^{p})}^{1 / p} {(\sum_{i < n} ∣ b_{i} ∣^{q})}^{1 / q} .$

Facts & Assumptions

Given: A natural $n$ , conjugate exponents $p, q > 1$ , and real families $a_{i}, b_{i}$ for $i < n$ .

[L1]

Young's inequality says $u v \leq u^{p} / p + v^{q} / q$ for $u, v \geq 0$ (Young's inequality for conjugate real exponents).

[L2]

Finite sums obey termwise addition and scalar multiplication, including the empty-sum convention, and $∣ a b ∣ = ∣ a ∣ ∣ b ∣$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products, Basic properties of the absolute value).

[L3]

For $r > 0$ , the zero-base convention gives $0^{r} = 0$ , while positive-base real powers are positive and obey the real-power laws (Real powers for positive bases, with the zero-base positive-exponent convention, The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents, The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

Proof

technique · direct

1.1

Put $A = (\sum_{i < n} ∣ a_{i} ∣^{p})^{1 / p}$ and $B = (\sum_{i < n} ∣ b_{i} ∣^{q})^{1 / q}$ . If $A = 0$ or $B = 0$ , the real-power laws and zero convention show that the corresponding nonnegative power sum is zero; finite-sum order then makes every corresponding term zero, so the claim follows.

L2L3

1.2

Suppose $A, B > 0$ , and set $u_{i} = ∣ a_{i} ∣ / A$ , $v_{i} = ∣ b_{i} ∣ / B$ . Then $\sum u_{i}^{p} = \sum v_{i}^{q} = 1$ .

L2L3

2.1

Apply [L1] to $u_{i}, v_{i}$ and sum over $i < n$ to obtain $\sum u_{i} v_{i} \leq 1 / p + 1 / q = 1$ .

step 1.2L1L2

3.1

Multiplying by $A B$ and using $∣ a_{i} b_{i} ∣ = ∣ a_{i} ∣ ∣ b_{i} ∣$ gives the asserted inequality.

step 1.2step 2.1L2∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

Minkowski's inequality for finite sums and real exponent p greater than one

Statement

Let $p > 1$ . For real families $(a_{i})_{i < n}$ and $(b_{i})_{i < n}$ , ${(\sum_{i < n} ∣ a_{i} + b_{i} ∣^{p})}^{1 / p} \leq {(\sum_{i < n} ∣ a_{i} ∣^{p})}^{1 / p} + {(\sum_{i < n} ∣ b_{i} ∣^{p})}^{1 / p} .$

Facts & Assumptions

Given: A natural $n$ , a real $p > 1$ , and real families $a_{i}, b_{i}$ for $i < n$ .

[L1]

Holder's inequality holds for finite sums and conjugate real exponents (Holder's inequality for finite sums and conjugate real exponents).

[L2]

Finite sums distribute over addition, and $∣ u + v ∣ \leq ∣ u ∣ + ∣ v ∣$ (Finite sums and finite products, by recursion, Laws of finite sums and finite products, Basic properties of the absolute value).

[L3]

Positive-base real-power laws hold; the zero-base positive-exponent convention gives $0^{r} = 0$ , and positive-base real powers are positive (Real powers for positive bases, with the zero-base positive-exponent convention, The exponent, product, quotient, and iterated-power laws for positive real bases and real exponents, The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

Proof

technique · direct

1.1

Let $q = p / (p - 1)$ and put $C = (\sum_{i < n} ∣ a_{i} + b_{i} ∣^{p})^{1 / p}$ . If $C = 0$ , the claim is immediate.

L2L3

1.2

For $C > 0$ , multiply $∣ a_{i} + b_{i} ∣^{p - 1}$ by $∣ a_{i} + b_{i} ∣ \leq ∣ a_{i} ∣ + ∣ b_{i} ∣$ and sum to get $C^{p} \leq \sum ∣ a_{i} ∣ ∣ a_{i} + b_{i} ∣^{p - 1} + \sum ∣ b_{i} ∣ ∣ a_{i} + b_{i} ∣^{p - 1}$ .

L2L3

2.1

Apply Holder to both sums in step 1.2. Since $(p - 1) q = p$ , their common second factor is $C^{p - 1}$ .

step 1.2L1L3

3.1

Thus $C^{p} \leq (A + B) C^{p - 1}$ , where $A, B$ are the two right-side norms; dividing by $C^{p - 1} > 0$ proves the claim.

step 1.1step 2.1L3∎

DefinitionDefinition: AI-adaptedProof: Not applicableaudited 2026-08-02Open item page →

The six hyperbolic functions and their natural domains

Definition

For $x \in R$ , define $\sinh x : = \frac{\exp x - \exp (- x)}{2}, \cosh x : = \frac{\exp x + \exp (- x)}{2},$ $\tanh x : = \frac{\sinh x}{\cosh x}, sech x : = \frac{1}{\cosh x} .$ For $x \neq 0$ , define $\coth x : = \frac{\cosh x}{\sinh x}, csch x : = \frac{1}{\sinh x} .$

The positivity of $\exp$ makes $\cosh x > 0$ for every $x$ . If $x \neq 0$ , then $x \neq - x$ , so strict increase of $\exp$ makes $\exp x \neq \exp (- x)$ ; hence $\sinh x \neq 0$ . Thus all four quotients above are defined on exactly their stated domains (The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ , The exponential function is strictly increasing).

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

Addition formulas, identities, parity, and derivatives of the hyperbolic functions

Statement

For all real $x, y$ , $\sinh (x + y) = \sinh x \cosh y + \cosh x \sinh y, \cosh (x + y) = \cosh x \cosh y + \sinh x \sinh y,$ $\cosh^{2} x - \sinh^{2} x = 1, (\sinh x)^{'} = \cosh x, (\cosh x)^{'} = \sinh x .$ Moreover $\sinh : R \to R$ is odd, strictly increasing, and onto; $\cosh : R \to [1, \infty)$ is even and positive, and its restriction to $[0, \infty)$ is strictly increasing and onto $[1, \infty)$ ; and $\tanh : R \to (- 1, 1)$ is strictly increasing and onto. On their declared domains, $(\tanh x)^{'} = {sech}^{2} x, (\coth x)^{'} = - {csch}^{2} x, (sech x)^{'} = - sech x \tanh x, (csch x)^{'} = - csch x \coth x .$

Facts & Assumptions

Given: Real numbers $x, y$ .

[L1]

$\exp (u + v) = \exp u \exp v$ , $\exp (- u) = 1 / \exp u$ , and $\exp u > 0$ (The exponential addition formula $\exp (x + y) = \exp (x) \exp (y)$ , The exponential is positive and satisfies $\exp (- x) = 1 / \exp (x)$ ).

[L2]

$\exp^{'} = \exp$ , and the chain, product, quotient, and algebra rules differentiate the displayed formulas (The exponential function is smooth and $(\exp)^{'} = \exp$ , The chain rule, in one line from Carathéodory: if $g$ is differentiable at $c$ and $f$ is differentiable at $g (c)$ , then $f \circ g$ is differentiable at $c$ with $(f \circ g)^{'} (c) = f^{'} (g (c)) g^{'} (c)$ , Sums, scalar multiples, products and quotients: $(f + g)^{'} (c) = f^{'} (c) + g^{'} (c)$ , $(α f)^{'} (c) = α f^{'} (c)$ , $(f g)^{'} (c) = f^{'} (c) g (c) + f (c) g^{'} (c)$ , and $(f / g)^{'} (c) = (f^{'} (c) g (c) - f (c) g^{'} (c)) / g (c)^{2}$ when $g (c) \neq 0$ ).

[L3]

If $a < b$ and $f : [a, b] \to R$ is continuous on $[a, b]$ and differentiable on $(a, b)$ , then some $c \in (a, b)$ satisfies $f (b) - f (a) = f^{'} (c) (b - a)$ (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 \in (a, b)$ with $f (b) - f (a) = f^{'} (c) (b - a)$ ).

[L4]

$\exp x \to \infty$ as $x \to \infty$ and $\exp x \to 0$ as $x \to - \infty$ (The exponential tends to $+ \infty$ at $+ \infty$ and to $0$ at $- \infty$ ).

[L5]

A continuous real function takes every value between two values on a closed interval (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)$ ).

[L6]

For every real $x$ , $\sinh x = (\exp x - \exp (- x)) / 2$ and $\cosh x = (\exp x + \exp (- x)) / 2$ ; $\tanh x = \sinh x / \cosh x$ and $sech x = 1 / \cosh x$ ; and, when $x \neq 0$ , $\coth x = \cosh x / \sinh x$ and $csch x = 1 / \sinh x$ . Moreover $\cosh x > 0$ for every $x$ , and $\sinh x \neq 0$ when $x \neq 0$ (The six hyperbolic functions and their natural domains).

[L7]

Differentiability implies continuity (A function differentiable at $c$ is continuous at $c$ ).

Proof

technique · direct

1.1

Substitute the exponential definitions of [L6] and use [L1]; collecting terms gives both addition formulas, parity, and $\cosh^{2} x - \sinh^{2} x = 1$ .

L1L6algebra

2.1

Differentiating the exponential definitions of [L6] gives $(\sinh x)^{'} = \cosh x$ and $(\cosh x)^{'} = \sinh x$ ; on the domains supplied by [L6], differentiating the quotients and using step 1.1 gives the four displayed reciprocal-function derivatives.

step 1.1L2L6algebra

2.2

The exponential formulas give $\sinh x \to \infty$ , $\cosh x \to \infty$ , and $\tanh x \to 1$ as $x \to \infty$ ; oddness gives the corresponding limits $- \infty$ and $- 1$ at $- \infty$ .

step 1.1L1L4algebra

3.1

By [L6], $\cosh x > 0$ and $\sinh x$ is nonzero away from $0$ ; the defining formula gives $\sinh 0 = 0$ . Thus $\sinh^{'} = \cosh > 0$ everywhere. For $a < b$ , step 2.1 and [L7] give the hypotheses of [L3] for $\sinh$ on $[a, b]$ , so for some $c \in (a, b)$ , $\sinh b - \sinh a = \cosh c (b - a) > 0$ . Hence $\sinh$ is strictly increasing.

step 2.1L3L6L7algebra

4.1

The oddness and strict increase of $\sinh$ make $\sinh x > 0$ for $x > 0$ . Thus for $0 \leq a < b$ , step 2.1 and [L7] let [L3] give $\cosh b - \cosh a = \sinh c (b - a) > 0$ for some $c \in (a, b)$ , so $\cosh$ is strictly increasing on $[0, \infty)$ . Also $sech x > 0$ , so for $a < b$ the same argument gives $\tanh b - \tanh a = {sech}^{2} c (b - a) > 0$ for some $c \in (a, b)$ ; hence $\tanh$ is strictly increasing.

step 1.1step 2.1step 3.1L1L3L6L7

5.1

The functions are continuous by step 2.1 and [L7]. Their monotonicity, the values $\cosh 0 = 1$ , and the endpoint limits of step 2.2 let the intermediate value theorem give exactly the three stated ranges.

step 2.1step 3.1step 4.1step 2.2L5L7∎

TheoremStatement: AI-adaptedProof: AI-generatedprecheck passaudited 2026-08-02Open item page →

Logarithm formulas for inverse sinh, inverse cosh, and inverse tanh on their natural domains

Statement

The strictly increasing bijections $\sinh : R \to R$ , $\cosh : [0, \infty) \to [1, \infty)$ , and $\tanh : R \to (- 1, 1)$ have inverse functions satisfying $arsinh u = \log (u + \sqrt{u^{2} + 1}),$ $arcosh u = \log (u + \sqrt{u^{2} - 1}) (u \geq 1),$ $artanh u = \frac{1}{2} \log \frac{1 + u}{1 - u} (∣ u ∣ < 1) .$

Facts & Assumptions

Given: A real $u$ in the stated domain.

[L1]

The hyperbolic identities hold, and $\sinh : R \to R$ , $\cosh : [0, \infty) \to [1, \infty)$ , and $\tanh : R \to (- 1, 1)$ are strictly increasing bijections (Addition formulas, identities, parity, and derivatives of the hyperbolic functions, The six hyperbolic functions and their natural domains).

[L2]

$\log$ is the inverse of $\exp$ and satisfies its product and reciprocal laws (Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm).

[L3]

Positive-base real powers are continuous, and every nonnegative real has its nonnegative square root (Continuity and derivatives of positive-base real powers, Square roots exist: a unique $\sqrt{a} \geq 0$ with $(\sqrt{a})^{2} = a$ ; the positives are ${x^{2} : x \neq 0}$ ).

Proof

technique · direct

1.1

Solving $\sinh z = u$ after putting $v = \exp z > 0$ gives $v^{2} - 2 u v - 1 = 0$ , hence $v = u + \sqrt{u^{2} + 1} > 0$ and $z = \log (u + \sqrt{u^{2} + 1})$ .

L1L2L3

1.2

Solving $\cosh z = u$ with $z \geq 0$ gives $v^{2} - 2 u v + 1 = 0$ and the allowed root $v = u + \sqrt{u^{2} - 1}$ , hence the displayed arcosh formula.

L1L2L3

1.3

Solving $\tanh z = u$ gives $v^{2} = (1 + u) / (1 - u) > 0$ , so $z = \frac{1}{2} \log ((1 + u) / (1 - u))$ .

L1L2

2.1

The strict monotonicity and stated ranges in [L1] make each algebraic solution the unique inverse value on its declared domain.

step 1.1step 1.2step 1.3L1∎

5 · Examples, counterexamples and false statements

None yet.