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.
Cauchy law and its characteristic function
Example
Assume AC. The Cauchy density defines a Borel probability law with characteristic function . Its first absolute moment is infinite. In the calculation below the unit exponential density has transform , and the symmetric Laplace density has transform .
Facts & Assumptions
Given: The hypotheses and conventions in the example.
Characteristic functions are componentwise exponential integrals. Characteristic function of a real random variable.
An integrable characteristic function gives a continuous density by inversion. Density inversion from an integrable characteristic function.
Nonnegative Borel densities define measures. The indefinite integral of a nonnegative measurable function is a measure.
Compact integrals of derivatives are primitive increments. The second fundamental theorem: if is differentiable on with and is integrable, then .
Countable choice identifies compact Riemann and Lebesgue integrals. A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral.
AC supplies the choice used in the bridge and inversion. The Axiom of Choice.
Real exponentials differentiate to themselves. The exponential function is smooth and .
Trigonometric derivatives evaluate the damped complex primitive. The derivatives of sine and cosine are cosine and minus sine.
Composition differentiates by the chain rule. The chain rule, in one line from Carathéodory: if is differentiable at and is differentiable at , then is differentiable at with .
Arctangent integrates 1/(1+x squared). Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series.
The logarithm derivative is 1/x on positive arguments. The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t.
Arctangent is an increasing bijection onto the principal open interval. The principal inverse tangent .
Logarithm is the inverse of exponential. The natural logarithm as the inverse of the exponential function.
Positive compact truncations recover the full integral. Monotone convergence for the integral.
Integrable domination permits passage from compact to full oscillatory integrals. Dominated convergence.
For nonnegative measurable test functions, density integrals are product integrals. Integrating against a density agrees with integrating the product.
Compact reflection substitution applies to continuous integrands. Substitution: if is differentiable on with integrable and is continuous on an interval containing , then .
Verification
The nonnegative exponential density has integral , using the compact primitive, bridge and monotone convergence. For real t the function is a primitive of , as direct componentwise differentiation shows; the denominator cannot vanish since its real part is -1. Therefore The boundary modulus is and the integrand modulus is , so DCT justifies the full oscillatory integral. Whenever density integration is used below for a bounded complex test , apply [F16] separately to the nonnegative functions and then reassemble their finite integrals componentwise as in [F1]; this gives without enlarging [F16]. Reflection substitution on compact intervals and then DCT show that the reflected density has transform . Splitting the two half-lines gives the probability density and transform .
The increasing arctangent has range , so its limits at the two infinities are the endpoints of that range: any smaller limiting supremum would omit values in the range, and similarly for the infimum. Consequently compact arctangent integration and monotone convergence give . The Laplace characteristic function is therefore integrable. Density inversion supplies the continuous density for the same Laplace law. It equals at every point: if two continuous densities of the same measure differed at one point, their difference would have a fixed strict sign and magnitude on a small interval, contradicting equal integrals on that interval. Hence The preceding arctangent integral also normalizes c, and density integration identifies the left side as its characteristic function, including t=0. No first moment of this law has been used.
For , logarithmic differentiation with the chain rule and the compact integral bridge give This tends to infinity: log is increasing by its positive derivative, and its inverse relation implies that log of an unbounded positive argument eventually exceeds every real level. Monotone convergence and density integration imply , already from the positive half-line. The density is finite at x=0 and has total mass one; it is not a zero or point-mass law. AC is retained from density inversion and the compact integration bridge. The auxiliary Laplace density has a corner at zero, but all differentiations above were on individual half-lines and its use in inversion required continuity, not differentiability there.
Depends on
- Characteristic function of a real random variable
- Density inversion from an integrable characteristic function
- The indefinite integral of a nonnegative measurable function is a measure
- The second fundamental theorem: if $G$ is differentiable on $[a,b]$ with $G' = f$ and $f$ is integrable, then $\int_a^b f = G(b)-G(a)$
- A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral
- The Axiom of Choice
- The exponential function is smooth and $(\exp)'=\exp$
- 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 \circ g$ is differentiable at $c$ with $(f \circ g)'(c) = f'(g(c))\,g'(c)$
- Principal arctangent: derivative, integral, power series, and the Gregory–Leibniz series
- The natural logarithm has derivative 1/x and equals the integral from 1 to x of 1/t
- The principal inverse tangent $\arctan:\mathbb R\to(-\pi/2,\pi/2)$
- The natural logarithm as the inverse of the exponential function
- Monotone convergence for the integral
- Dominated convergence
- Integrating against a density agrees with integrating the product
- Substitution: if $\varphi$ is differentiable on $[c,d]$ with $\varphi'$ integrable and $f$ is continuous on an interval containing $\varphi([c,d])$, then $\int_{\varphi(c)}^{\varphi(d)} f = \int_c^d (f\circ\varphi)\,\varphi'$
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
96 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
- Durrett, Probability: Theory and Examples, fifth edition (standard reference, not scraped)
- Norris, Probability and Measure (standard reference, not scraped)