Alphabeta Math
LemmaStatement: Literature-sourcedProof: AI-adaptedPipeline-generated
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.

Threshold decoding bound for memoryless channels with densities

Statement

Let PX be an input law, let ν be a sigma-finite reference measure on the output space, and let w(y∣x) be a measurable single-use channel density satisfying ∫w(y∣x) dν(y)=1. Let q(y)=∫w(y∣x) PX(dx) be the induced output density and assume q>0 on its probability-one support. For independent uses define ı(xn;yn):=∑t=1nln⁡w(yt∣xt)q(yt) on the joint support. For every n≥1, M≥2, and τ>0, the IID random-code ensemble's expected average error is at most Pr⁡ ⁣[ı(Xn;Yn)≤ln⁡(M−1)+τ]+e−τ, where (Xn,Yn) has input law PX⊗n followed by the product channel. Consequently, some deterministic length-n code with M messages and the threshold decoder has average error no greater than this bound.

Facts & Assumptions

Given: The channel density, input law, induced positive output density, product channel, and blocklength/message/threshold parameters in the Statement.

[F1]

Tonelli's theorem for nonnegative measurable functions on a sigma-finite product: nonnegative measurable functions on a sigma-finite product space can be integrated in either order.

[F2]

For sigma-finite factors, the product measure exists, has the rectangle formula, is sigma-finite, and is unique: the finite product of the input and output reference measures has the stated rectangular sections and product integrals.

[F3]

Order, continuity, range, and the product, quotient, and reciprocal laws for the natural logarithm and The natural logarithm as the inverse of the exponential function: ln⁡ is strictly increasing on (0,∞), obeys the product law, and is inverse to the exponential, so eln⁡a=a for a>0.

[F4]

Chebyshev-Markov inequality for the integral: if L≥0 is measurable and a>0, then Pr⁡[L≥a]≤EL/a.

[F5]

The finite union bound: the probability that one of finitely many events occurs is at most the sum of their probabilities.

[F6]

The Lebesgue integral is linear on L1(μ): the integral is linear on integrable real-valued functions.

[F7]

A nonnegative measurable function has integral 0 exactly when it vanishes almost everywhere: a nonnegative measurable random variable with expectation zero vanishes almost surely.

Proof

1.1F1F3givenconstruct

Draw M codewords independently from PX⊗n. Put S={y:0<q(y)<∞}; normalization and [F1] give PY(S)=1. For yn∈Sn define L(xn;yn)=∏tw(yt∣xt)/q(yt), with a zero factor making the product zero, and define the score ℓ=ln⁡L with ln⁡0=−∞ and ln⁡(+∞)=+∞. Set ℓ=−∞ outside Sn. These are measurable extended-real scores. Under the transmitted joint law, each channel density is positive and finite almost surely by row normalization, so ℓ=ı almost surely. Declare message m if it is the unique codeword whose score exceeds ln⁡(M−1)+τ; otherwise output a fixed default. An error is contained in the event that the transmitted score fails the threshold or that some independent competing word passes it.

1.2F1F2givenalgebra

The first event has probability exactly the miss probability in the Statement. For one competing word Xˉn independent of Yn, the latter has density q⊗n under the ensemble. Define L=0 outside Sn. By [F1, F2] and normalization of the product channel rows, EL=∫PX⊗n(dxˉn)∫Snw⊗n(yn∣xˉn) dν⊗n(yn)≤1. Thus the likelihood ratio is well-defined even for a competitor with zero channel density.

2.1F3F4F5step 1.1step 1.2givenalgebra

If a competitor passes, [F3] makes L>(M−1)eτ, hence the event is contained in {L≥(M−1)eτ}. Markov's integral inequality [F4] bounds this probability by e−τ/(M−1). The finite union bound [F5] over the M−1 competitors contributes at most e−τ. Combining this with the miss event in step 1.1 proves the asserted bound on ensemble expected average error.

3.1F6F7step 1.1step 2.1givenchoose∎

Let E be the random codebook's average error and set b=EE; then 0≤E≤1, so both E and the constant b are integrable. If every sampled codebook had E>b, the nonnegative variable E−b would be positive everywhere, while linearity [F6] and P(Ω)=1 give E(E−b)=0. By [F7], E−b=0 almost surely, a contradiction. Hence some codebook has error at most b, which is bounded by the result of steps 1.1 and 2.1.

Depends on

Used by

Dependency tree · two levels

36 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