LemmaStatement: AI-adaptedProof: AI-adaptedPipeline-generatedprecheck passjudge pass (gpt-6-luna)

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.

A positive C1 point density has a C2 cumulative inverse

Statement

Let $a < b$ and let $g : [a, b] \to (0, \infty)$ be $C^{1}$ with $\int_{a}^{b} g = 1$ , and let $G_{g}$ be as in Cumulative coordinate of a point density on a compact interval. Then $G_{g}$ is a strictly increasing $C^{2}$ bijection from $[a, b]$ onto $[0, 1]$ . Its inverse $ϕ : [0, 1] \to [a, b]$ is $C^{2}$ (with one-sided derivatives at the endpoints), and

$ϕ^{'} (u) = \frac{1}{g (ϕ (u))}, ϕ^{''} (u) = - \frac{g^{'} (ϕ (u))}{g (ϕ (u))^{3}} .$

Facts & Assumptions

Given: A nondegenerate compact interval $[a, b]$ and a positive normalized $C^{1}$ function $g$ .

[F1]

Cumulative coordinate of a point density on a compact interval: $G_{g} (x) = \int_{a}^{x} g (t) d t$ and $\int_{a}^{b} g = 1$ .

[F2]

Every continuous function on an interval has a primitive; two primitives differ by a constant; and $\int_{a}^{b} f = G (b) - G (a)$ for any primitive $G$ : a continuous function on an interval has a primitive $G (x) = \int_{c_{0}}^{x} g$ , with $G^{'} = g$ and $\int_{x}^{y} g = G (y) - G (x)$ .

[F3]

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)$ : if a real function is continuous on $[x, y]$ and differentiable on $(x, y)$ , then $G (y) - G (x) = G^{'} (c) (y - x)$ for some interior $c$ .

[F4]

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)$ : a continuous real function on a closed interval takes every value between its endpoint values.

[F5]

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$ : sums, products and quotients of differentiable real functions obey the corresponding derivative rules when the quotient denominator is nonzero.

[F6]

The chain rule for total derivatives: $D (g \circ f) (a) = D g (f (a)) \circ D f (a)$ : the derivative of a composition of differentiable maps between Euclidean spaces is the composition of their derivatives.

[F7]

A continuous real-valued function on a nonempty compact metric space is bounded and attains a greatest and a least value: a continuous real-valued function on a nonempty compact metric space is bounded and attains a minimum.

Proof

1.1givenF1F2F7

By [F2], $G_{g}$ is continuous and $G_{g}^{'} = g$ on $(a, b)$ , so it is $C^{2}$ because $g$ is $C^{1}$ ; also $G_{g} (a) = 0$ and $G_{g} (b) = 1$ by [F1]. Since $g$ is positive and continuous on compact $[a, b]$ , [F7] gives a positive minimum, and in particular $G_{g}^{'} (x) > 0$ at every interior point.

2.1givenF3F4step 1.1

For $x < y$ in $[a, b]$ , [F3] applied to $G_{g}$ gives $G_{g} (y) - G_{g} (x) = g (c) (y - x) > 0$ . Thus $G_{g}$ is strictly increasing; [F4] and step 1.1 show its image is all of $[0, 1]$ . Strict increase makes each preimage unique, so an inverse $ϕ : [0, 1] \to [a, b]$ exists.

3.1givenstep 2.1construct

Fix $u_{0} \in [0, 1]$ and set $x_{0} = ϕ (u_{0})$ . For $ε > 0$ put $x_{-} = \max (a, x_{0} - ε)$ and $x_{+} = \min (b, x_{0} + ε)$ . At least one of $x_{-} < x_{0}$ and $x_{0} < x_{+}$ holds because $a < b$ . Whenever $x_{-} < x_{0}$ or $x_{0} < x_{+}$ , strict increase gives respectively $u_{0} - G_{g} (x_{-}) > 0$ or $G_{g} (x_{+}) - u_{0} > 0$ . Choose $δ > 0$ smaller than each of the positive margins that exists. For $u \in [0, 1]$ with $∣ u - u_{0} ∣ < δ$ , monotonicity gives $x_{-} \leq ϕ (u) \leq x_{+}$ ; at a missing margin $x_{-} = x_{0} = a$ or $x_{+} = x_{0} = b$ , the domain endpoint supplies that inequality. Hence $∣ ϕ (u) - x_{0} ∣ < ε$ , proving continuity of $ϕ$ .

4.1givenF3step 2.1step 3.1

Fix $u \in (0, 1)$ , let $x = ϕ (u)$ , and for nonzero $h$ with $u + h \in [0, 1]$ let $x_{h} = ϕ (u + h)$ . Continuity from step 3.1 gives $x_{h} \to x$ , and injectivity gives $x_{h} \neq x$ . By [F3], for some $ξ_{h}$ between $x$ and $x_{h}$ , $(ϕ (u + h) - ϕ (u)) / h = 1 / g (ξ_{h})$ . As $h \to 0$ , $ξ_{h} \to x$ and $g (ξ_{h}) \to g (x) > 0$ , so $ϕ^{'} (u) = 1 / g (ϕ (u))$ . The same one-sided quotient argument applies at $u = 0, 1$ .

5.1givenF3F5F6step 3.1step 4.1∎

The formula for $ϕ^{'}$ is continuous on $[0, 1]$ because $g \circ ϕ$ is continuous and positive. Differentiating it on $(0, 1)$ using [F5] and [F6] gives $ϕ^{''} (u) = - g^{'} (ϕ (u)) / g (ϕ (u))^{3}$ . The right-hand side extends continuously to $[0, 1]$ because $g^{'}$ and $ϕ$ are continuous and the denominator stays positive. Applying [F3] to $ϕ^{'}$ on intervals with an endpoint at $0$ or $1$ shows its one-sided difference quotient tends to that continuous extension. Together with step 4.1, this proves the stated $C^{2}$ regularity and formulas.

Depends on

Used by

Dependency tree · two levels

62 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.

Sources

Robert M. Gray, Source Coding Theory, first edition (standard reference, not scraped)
Robert Gallager, 6.450 Principles of Digital Communications I, Chapter 3: Quantization (standard reference, not scraped)
Robert M. Gray and David L. Neuhoff, Quantization, IEEE Transactions on Information Theory 44(6) (1998) (standard reference, not scraped)