Alphabeta Math
TheoremStatement: AI-adaptedProof: AI-adaptedPipeline-generatedjudge pass (gpt-5.6-terra)audited 2026-09-12
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.

Tightness from characteristic function equicontinuity at zero

Statement

Assume AC. Let A be a family of Borel probability laws on R. For δ>0 put wδ(t)=δ−1(1−∣t∣/δ)+. Every μ∈A satisfies μ{∣x∣≥4/δ}≤43∫Rwδ(t)(1−Re⁡ϕμ(t)) dt. If the characteristic functions are equicontinuous at zero, meaning that for every η>0 some r>0 satisfies ∣ϕμ(t)−1∣<η for every μ∈A and ∣t∣<r, then A is tight. AC supplies the countable choice used by the compact-interval integration bridge and the continuous-integrand calculus.

Facts & Assumptions

Given: The hypotheses and conventions in the statement.

[F1]

The real part of the characteristic function is the integral of cosine. Characteristic function of a real random variable.

[F2]

Fubini applies to absolutely integrable functions on sigma-finite products. Fubini's theorem for L1 functions on a sigma-finite product.

[F4]

Under countable choice the bounded Riemann integral agrees with the Lebesgue integral. A bounded Riemann integrable function on a closed bounded interval is Lebesgue measurable and has the same integral.

[F5]

AC implies the countable choice used by the integration bridge. The Axiom of Choice.

[F6]

Tightness requires a single compact set for each error and the whole family. Tight family of probability measures.

[F7]

Sine and cosine have derivatives cosine and minus sine. The derivatives of sine and cosine are cosine and minus sine.

Proof

technique · direct
1.1F3F4F5F7F8F10

The continuous nonnegative weight is supported on [−δ,δ] and has integral 2δ−1∫0δ(1−t/δ) dt=1. Set Kδ(x)=∫wδ(t)cos⁡(tx) dt. At x=0 it equals one. For x≠0, integration by parts on [0,δ], with u=1−t/δ and v=sin⁡(tx)/x, gives Kδ(x)=2δ2x∫0δsin⁡(tx) dt=2(1−cos⁡(δx))δ2x2. All functions and their derivatives here are continuous on that interval; the primitive and integration bridge therefore apply. The formula gives Kδ≥0, while its defining integral and cos⁡≤1 give Kδ≤1. Also Kδ(x)≤4/(δ2x2)≤1/4 when ∣x∣≥4/δ, including equality in the cutoff.

2.1F1F2step 1.1

The function wδ(t)(1−cos⁡(tx)) is jointly Borel, nonnegative, and has product integral at most 2∫wδ=2: Lebesgue measure is sigma-finite and μ is finite. Fubini and the characteristic-function definition yield ∫wδ(t)(1−Re⁡ϕμ(t)) dt=∫(1−Kδ(x)) μ(dx)≥34μ{∣x∣≥4/δ}. Nonnegativity off the tail justifies discarding its complement. Rearrangement proves the quantitative assertion.

3.1step 1.1step 2.1F6F9∎

Given ε>0, equicontinuity supplies r>0 with ∣1−ϕμ(t)∣<3ε/8 whenever ∣t∣<r, uniformly in μ. Choose 0<δ<r. The weight has mass one, so the integral in the bound is at most 3ε/8. Thus μ(R∖[−4/δ,4/δ])≤ε/2<ε for every member. The interval is compact, proving tightness. For an empty family the empty compact set suffices. A singleton family and an atom at zero satisfy the same calculation (the latter has zero right-hand side). There is no assertion at δ=0, where the weight is undefined.

Depends on

Used by

Dependency tree · two levels

80 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