Alphabeta Math
ExampleConstruction: AI-adaptedVerification: AI-adaptedPipeline-generatedprecheck pass
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.

Density inversion for a triangular characteristic function

Example

Assume AC. The triangular function τ(t)=(1−∣t∣)+ is the characteristic function of the probability density f(x)=1−cos⁡xπx2(x≠0),f(0)=12π. This value makes f continuous at zero.

Facts & Assumptions

Given: The hypotheses and conventions in the example.

[F1]

The characteristic function integrates the exponential componentwise. Characteristic function of a real random variable.

[F2]

Inversion of an already known integrable characteristic function gives a continuous density. Density inversion from an integrable characteristic function.

[F3]
[F6]

AC covers the bridge and density inversion. The Axiom of Choice.

[F7]

The sine and cosine derivatives give their real primitives. The derivatives of sine and cosine are cosine and minus sine.

[F9]

Nonnegative tests against a density integrate the product. Integrating against a density agrees with integrating the product.

[F10]

Characteristic functions are continuous, bounded by one and normalized at zero. Basic properties of characteristic functions.

[F11]

Nonnegative expanding compact truncations recover their full integral. Monotone convergence for the integral.

Verification

technique · direct
1.1F1F3F4F5F7F8F9F10F11

First use h(u)=(1−∣u∣)+ as a density in the space variable u. It is nonnegative Borel and ∫h=2∫01(1−u) du=1, so it defines a probability. Its characteristic function q has vanishing imaginary part by the oddness of h(u)sin⁡(su). For s≠0, integration by parts with 1−u and sin⁡(su)/s yields q(s)=2∫01(1−u)cos⁡(su) du=2s∫01sin⁡(su) du=2(1−cos⁡s)s2. All factors and derivatives are continuous on [0,1], so FTC and the bridge apply. Density integration is applied to the real and imaginary positive/negative parts. At s=0, q(0)=1, and continuity follows from the characteristic-function lemma. Thus q is nonnegative everywhere and bounded by one, with q(s)≤4/s2 for ∣s∣≥1. The primitive −1/s on [1,R], the bridge and monotone convergence give ∫1∞s−2 ds=1; reflection gives the other tail. Hence q is integrable.

2.1step 1.1F2F3

Apply density inversion to that probability with characteristic function q. It supplies the continuous density H(y)=(2π)−1∫e−isyq(s) ds. This equals h everywhere: if the two continuous densities differed at y, continuity would give a small interval where their difference had one strict sign, contradicting that both densities integrate to the same interval mass. In particular 1=h(0)=H(0)=(2π)−1∫q. Therefore f=q/(2π) is nonnegative and integrates to one, so defines a probability. It has exactly the displayed formula and the continuous value 1/(2π) at zero.

3.1step 2.1F1F6F9∎

Density integration and the identity in step 2.1 now give φf(t)=12π∫eitxq(x) dx=H(−t)=h(−t)=(1−∣t∣)+. This includes t=0 and both endpoints t=±1, where the value is zero; outside the closed interval it is zero as well. The density value at x=0 was fixed by continuity, not division by zero. AC is inherited from the compact bridge and density inversion. The argument applied inversion only to the known law h before establishing that the triangle is a characteristic function.

Remarks

The paired graphs distinguish the compactly supported characteristic function from its density, which has nonnegative oscillatory lobes extending beyond the displayed window. The Fourier convention is τ(t)=∫Reitxf(x) dx and f(x)=(2π)−1∫Re−itxτ(t) dt. The density graph uses the continuous value at zero; its other zeros are x=2πk for nonzero integers k. The verification above is independent of this illustration.

t¿(t)¡1011xf(x)12¼0¡4¼¡2¼2¼4¼

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

65 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