Skip to main content

Module functions

oxilean_std::coding_theory

Module functions 

Source
Expand description

Auto-generated module

πŸ€– Generated with SplitRS

Functions§

alamouti_scheme_ty
AlamoutiScheme : Prop β€” Alamouti scheme achieves full diversity order 2 with 2 transmit antennas, simple decoding.
algebraic_geometry_code_ty
AlgebraicGeometryCode : Nat β†’ Nat β†’ Type β€” AG code (Goppa code) constructed from an algebraic curve over GF(q).
app
arrow
basis_pursuit_recovery_ty
BasisPursuitRecovery : Nat β†’ Nat β†’ Prop β€” basis pursuit (L1 minimization) recovers k-sparse signals from m β‰₯ O(k log(n/k)) measurements.
bch_code_ty
BCHCode : Nat β†’ Nat β†’ Nat β†’ Type β€” BCH code of length n, design distance Ξ΄, over GF(q^m).
bch_design_distance_ty
BCHDesignDistance : Nat β†’ Nat β†’ Nat β†’ Prop β€” BCH bound: minimum distance of BCH code with design distance Ξ΄ is β‰₯ Ξ΄.
bch_roots_extension_field_ty
BCHRootsExtensionField : Nat β†’ Nat β†’ Prop β€” roots of BCH generator polynomial lie in an extension field GF(q^m).
belief_propagation_decoding_ty
BeliefPropagationDecoding : Nat β†’ Nat β†’ Prop β€” belief propagation on the Tanner graph of an LDPC code achieves capacity on BEC.
bicm_capacity_ty
BICMCapacity : Nat β†’ Nat β†’ Prop β€” BICM capacity equals the sum of mutual informations of individual bit channels.
binomial
bit_interleaved_coded_modulation_ty
BitInterleavedCodedModulation : Nat β†’ Nat β†’ Type β€” BICM scheme with code rate R and modulation order M.
blahut_arimoto_ty
BlahutArimoto : Nat β†’ Prop β€” Blahut-Arimoto algorithm computes channel capacity and rate-distortion function.
build_coding_theory_env
Populate env with all coding theory axioms and theorems.
burst_error_correction_interleaving_ty
BurstErrorCorrectionInterleaving : Nat β†’ Nat β†’ Prop β€” interleaving converts burst errors into random errors correctable by inner code.
capacity_achieving_sequence_ty
CapacityAchievingSequence : Nat β†’ Prop β€” a sequence of codes achieves capacity if rate β†’ C and error probability β†’ 0.
channel_capacity_converse_ty
ChannelCapacityConverse : Nat β†’ Prop β€” converse to channel coding theorem: no code with rate R > C and vanishing error.
channel_polarization_ty
ChannelPolarization : Nat β†’ Prop β€” after N successive cancellation steps, synthetic channels polarize to noiseless or pure-noise.
color_code_transversal_gates_ty
ColorCodeTransversalGates : Nat β†’ Prop β€” 2D color codes support transversal implementation of the full Clifford group.
color_code_ty
ColorCode : Nat β†’ Type β€” topological color code on a 2-colex (2-colorable complex) of size parameter n.
compressed_sensing_matrix_ty
CompressedSensingMatrix : Nat β†’ Nat β†’ Type β€” mΓ—n measurement matrix satisfying the restricted isometry property.
concatenated_code_decoding_ty
ConcatenatedCodeDecoding : Nat β†’ Nat β†’ Prop β€” concatenated codes decoded by generalized minimum distance (GMD) decoding can correct a fraction of errors.
concatenated_code_ty
ConcatenatedCode : Nat β†’ Nat β†’ Type β€” Forney concatenated code with outer code of length n and inner code of length m.
convolutional_code_ty
ConvolutionalCode : Nat β†’ Nat β†’ Nat β†’ Type β€” convolutional code with rate k/n and constraint length K.
crc_polar_code_ty
CRCPolarCode : Nat β†’ Nat β†’ Type β€” CRC-aided polar code with CRC length r and block length N = 2^n.
css_code_ty
CSSCode : Nat β†’ Nat β†’ Type β€” Calderbank-Shor-Steane (CSS) code constructed from two classical codes C1 βŠ‡ C2.
cst
dual_code_parity_check_is_generator_ty
dual_code_parity_check_is_generator : Nat β†’ Nat β†’ Prop β€” the parity-check matrix of C is the generator matrix of the dual code C^βŠ₯.
elias_bassalygo_ty
EliasBassalygo : Nat β†’ Nat β†’ Nat β†’ Prop β€” Elias-Bassalygo bound on maximum code size A(n, d).
erfc_approx
Approximation of erfc(x) = (2/βˆšΟ€) ∫_x^∞ e^{-tΒ²} dt.
expander_code_linear_time_decoding_ty
ExpanderCodeLinearTimeDecoding : Nat β†’ Nat β†’ Prop β€” expander codes admit linear-time decoding algorithms.
expander_code_ty
ExpanderCode : Nat β†’ Nat β†’ Type β€” code based on bipartite expander graph.
extended_hamming_code_ty
ExtendedHammingCode : Nat β†’ Nat β†’ Nat β†’ Type β€” extended Hamming code (2^r, 2^r - r - 1, 4) obtained by adding an overall parity bit.
fountain_code_ty
FountainCode : Nat β†’ Type β€” rateless erasure code (e.g., Luby Transform).
gallager_ldpc_ty
GallagerLDPC : Nat β†’ Nat β†’ Nat β†’ Type β€” Gallager-constructed LDPC code with column weight j and row weight k.
generator_matrix_ty
GeneratorMatrix : Nat β†’ Nat β†’ Type β€” a kΓ—n generator matrix G.
gilbert_varshamov_ty
GilbertVarshamov : Nat β†’ Nat β†’ Nat β†’ Prop β€” Gilbert-Varshamov lower bound: there exists a linear code with d β‰₯ Ξ΄ and rate β‰₯ 1 - H(Ξ΄/n).
goppa_code_min_distance_ty
GoppaCodeMinDistance : Nat β†’ Nat β†’ Prop β€” Goppa code minimum distance satisfies d β‰₯ n - k (Goppa bound).
griesmer_bound_ty
GreismerBound : Nat β†’ Nat β†’ Nat β†’ Prop β€” Griesmer bound on minimum length of a binary linear code with given k and d.
guruswami_sudan_decoding_ty
GuruswamiSudanDecoding : Nat β†’ Nat β†’ Prop β€” Guruswami-Sudan algorithm list-decodes RS codes up to 1 - √(k/n) fraction of errors.
hamming_ball_volume
Volume of a Hamming ball of radius t in {0,1}^n: Ξ£_{i=0}^{t} C(n,i).
hamming_bound_ty
HammingBound : Nat β†’ Nat β†’ Nat β†’ Prop β€” sphere-packing (Hamming) bound.
hamming_code_optimal_ty
HammingCodeOptimal : Nat β†’ Prop β€” Hamming codes are the unique perfect single-error-correcting codes (up to equivalence).
hamming_perfect_ty
hamming_perfect : βˆ€ (r : Nat), PerfectCode (HammingCode r) β€” Hamming codes (2^r-1, 2^r-r-1, 3) meet the Hamming bound exactly.
interleaved_code_ty
InterleavedCode : Nat β†’ Nat β†’ Type β€” interleaved code with interleaving depth d over block length n.
lattice_code_ty
LatticeCode : Nat β†’ Type β€” lattice code in R^n.
ldpc_capacity_awgn_ty
SpaghettiCodeAwgn : Nat β†’ Prop β€” LDPC codes with optimized degree distributions approach AWGN capacity.
ldpc_capacity_bec_ty
LDPCCapacityBEC : Nat β†’ Prop β€” degree-optimized LDPC codes achieve BEC capacity under belief propagation.
ldpc_code_ty
LDPCCode : Nat β†’ Nat β†’ Type β€” LDPC code defined by sparse parity-check matrix.
linear_code_ty
LinearCode : Nat β†’ Nat β†’ Nat β†’ Type β€” an (n, k, d) linear code.
linear_network_coding_ty
LinearNetworkCoding : Nat β†’ Nat β†’ Prop β€” linear network coding suffices to achieve multicast capacity.
list_decoding_ty
ListDecoding : Nat β†’ Nat β†’ Nat β†’ Type β€” list decoder that outputs a list of codewords within Hamming distance e.
locally_decodable_code_bound_ty
LocallyDecodableCodeBound : Nat β†’ Nat β†’ Nat β†’ Prop β€” lower bound on codeword length for q-query LDCs.
locally_decodable_code_ty
LocallyDecodableCode : Nat β†’ Nat β†’ Nat β†’ Type β€” LDC with codeword length N, message length K, query complexity q.
luby_transform_code_ty
LubyTransformCode : Nat β†’ Type β€” LT (Luby Transform) fountain code.
mac_williams_transform_ty
MacWilliamsTransform : Nat β†’ Nat β†’ Prop β€” MacWilliams identity: weight enumerator of C^βŠ₯ is the MacWilliams transform of weight enumerator of C.
mimo_capacity_ty
MIMOCapacity : Nat β†’ Nat β†’ Prop β€” MIMO channel capacity: C = log det(I + (SNR/n_t) H H^†) for n_t transmit, n_r receive antennas.
mimo_spacetime_diversity_ty
MIMOSpacetimeDiversity : Nat β†’ Nat β†’ Nat β†’ Prop β€” diversity-multiplexing tradeoff: d(r) = (n_t - r)(n_r - r) for MIMO channel.
minimum_bandwidth_regenerating_ty
MinimumBandwidthRegenerating : Nat β†’ Nat β†’ Nat β†’ Prop β€” MBR point: minimizes repair bandwidth subject to exact repair.
minimum_storage_regenerating_ty
MinimumStorageRegenerating : Nat β†’ Nat β†’ Nat β†’ Prop β€” MSR point: minimizes storage per node subject to exact repair.
minkowski_lattice_theorem_ty
MinkowskiLatticeTheorem : Nat β†’ Prop β€” Minkowski’s theorem: a convex body of volume > 2^n contains a nonzero lattice point.
mrrw_bound_ty
MRRWBound : Nat β†’ Nat β†’ Nat β†’ Prop β€” McEliece-Rodemich-Rumsey-Welch (MRRW) linear-programming bound.
mutual_information_ty
MutualInformation : Nat β†’ Nat β†’ cst(Real) β€” I(X;Y) : Nat β†’ Nat β†’ Real.
nat_ty
network_coding_capacity_ty
NetworkCodingCapacity : Nat β†’ Nat β†’ Prop β€” max-flow min-cut theorem: multicast capacity equals minimum cut capacity.
noisy_channel_ty
noisy_channel : βˆ€ (p : Real), BSCCapacity p = 1 - BinaryEntropy p β€” binary symmetric channel capacity is 1 - H(p).
nonbinary_ldpc_ty
NonbinaryLDPC : Nat β†’ Nat β†’ Type β€” LDPC code over GF(q) with block length n and q = 2^m.
nonbinary_turbo_code_ty
NonbinaryTurboCode : Nat β†’ Nat β†’ Type β€” turbo code over GF(q): two RSC codes over GF(q) with interleaver.
parity_check_matrix_ty
ParityCheckMatrix : Nat β†’ Nat β†’ Type β€” an (n-k)Γ—n parity-check matrix H.
parvaresh_vardy_decoding_ty
ParvareshVardyDecoding : Nat β†’ Nat β†’ Prop β€” Parvaresh-Vardy codes improve GS list-decoding radius using correlated polynomials.
plotkin_bound_ty
PlotkinBound : Nat β†’ Nat β†’ Nat β†’ Prop β€” Plotkin bound on max codewords.
polar_code_bec_capacity_ty
PolarCodeBECCapacity : Nat β†’ Prop β€” polar codes achieve BEC capacity with block-error rate O(2^{-N^{0.5}}).
polar_code_capacity_achieving_ty
PolarCodeCapacityAchieving : Nat β†’ Prop β€” polar codes achieve the capacity of any binary-input memoryless symmetric channel.
polar_code_scl_ty
PolarCodeSCL : Nat β†’ Nat β†’ Prop β€” successive cancellation list (SCL) decoding of polar codes with list size L.
polar_code_successive_cancellation_ty
PolarCodeSuccessiveCancellation : Nat β†’ Prop β€” successive cancellation (SC) decoding of polar codes achieves O(N log N) complexity.
polar_code_ty
PolarCode : Nat β†’ Type β€” polar code of block length N = 2^n.
product_code_ty
ProductCode : Nat β†’ Nat β†’ Nat β†’ Nat β†’ Type β€” tensor product code C1 βŠ— C2 with parameters (n1n2, k1k2, d1*d2).
prop
qary_polar_code_ty
QaryPolarCode : Nat β†’ Nat β†’ Type β€” polar code for q-ary symmetric channel with block length N and alphabet size q.
quantum_hamming_bound_ty
QuantumHammingBound : Nat β†’ Nat β†’ Prop β€” quantum Hamming (sphere-packing) bound for non-degenerate codes.
quantum_ldpc_code_ty
QuantumLDPCCode : Nat β†’ Nat β†’ Type β€” quantum LDPC code with n physical qubits and k logical qubits, defined by sparse check matrices.
quantum_ldpc_good_code_ty
QuantumLDPCGoodCode : Nat β†’ Prop β€” good quantum LDPC codes have linear distance and linear rate simultaneously.
quantum_singleton_ty
QuantumSingleton : Nat β†’ Nat β†’ Prop β€” quantum Singleton (Knill-Laflamme) bound: d ≀ n/2 - k/2 + 1 for non-degenerate codes.
random_linear_code_gv_ty
RandomLinearCodeGV : Nat β†’ Nat β†’ Prop β€” random linear codes over GF(q) achieve the Gilbert-Varshamov bound with high probability.
raptor_code_ty
RaptorCode : Nat β†’ Type β€” Raptor code: pre-coded LT code with linear encoding/decoding.
rate_distortion_function_ty
RateDistortionFunction : Nat β†’ Nat β†’ Prop β€” Shannon rate-distortion theorem: R(D) = min_{p(xΜ‚|x): E[d(X,XΜ‚)]≀D} I(X; XΜ‚).
reed_muller_capacity_achieving_ty
ReedMullerCapacityAchieving : Prop β€” Reed-Muller codes achieve capacity on the binary erasure channel.
reed_muller_code_ty
ReedMullerCode : Nat β†’ Nat β†’ Type β€” Reed-Muller code RM(r, m) of order r in m variables.
reed_muller_decoding_ty
ReedMullerDecoding : Nat β†’ Nat β†’ Prop β€” Reed-Muller codes of order 1 are first-order Reed-Muller codes decodable by majority logic.
reed_solomon_eval_encoding_ty
ReedSolomonEvalEncoding : Nat β†’ Nat β†’ Type β€” RS encoding: evaluate a degree-(k-1) polynomial at n distinct field points.
reed_solomon_mds_ty
reed_solomon_mds : βˆ€ (n k : Nat), MDS (ReedSolomon n k) β€” Reed-Solomon codes are maximum distance separable (meet the Singleton bound).
reed_solomon_min_distance_ty
ReedSolomonMinDistance : Nat β†’ Nat β†’ Prop β€” minimum distance of RS(n, k) over GF(q) is n - k + 1.
regenerating_code_ty
RegeneratingCode : Nat β†’ Nat β†’ Nat β†’ Nat β†’ Type β€” (n, k, d, Ξ²) regenerating code for distributed storage.
restricted_isometry_property_ty
RestrictedIsometryProperty : Nat β†’ Nat β†’ Prop β€” RIP: every set of s columns of the measurement matrix is nearly orthonormal.
shannon_channel_coding_ty
shannon_channel_coding : βˆ€ (R C : Real), R < C β†’ ReliableComm R β€” reliable communication is possible for any rate below channel capacity.
shannon_entropy_ty
ShannonEntropy : Nat β†’ cst(Real) β€” H : Nat β†’ Real, discrete Shannon entropy.
singleton_bound_ty
SingletonBound : Nat β†’ Nat β†’ Nat β†’ Prop β€” Singleton bound d ≀ n - k + 1.
space_time_code_ty
SpaceTimeCode : Nat β†’ Nat β†’ Nat β†’ Type β€” space-time block code with n_t transmit antennas, n_r receive antennas, rate R.
spatially_coupled_code_ty
SpatiallyCoupledCode : Nat β†’ Nat β†’ Type β€” spatially coupled ensemble of LDPC codes achieving MAP threshold.
stabilizer_code_ty
StabilizerCode : Nat β†’ Nat β†’ Type β€” quantum stabilizer code encoding k logical qubits into n physical qubits.
surface_code_threshold_ty
SurfaceCodeThreshold : Prop β€” surface codes have a fault-tolerance threshold above which logical error rates decrease exponentially with code distance.
surface_code_ty
SurfaceCode : Nat β†’ Type β€” Kitaev surface code on an LΓ—L planar lattice with distance L.
systematic_code_ty
SystematicCode : Nat β†’ Nat β†’ Nat β†’ Type β€” an (n, k, d) code in systematic form [I_k | P].
systematic_encoding_ty
systematic_encoding : Nat β†’ Nat β†’ Prop β€” every linear code is equivalent to a code in systematic form.
threshold_saturation_ty
ThresholdSaturation : Nat β†’ Prop β€” threshold saturation: BP threshold of spatially coupled codes equals MAP threshold.
toric_code_ty
ToricCode : Nat β†’ Type β€” Kitaev toric code on an LΓ—L torus: encodes 2 logical qubits, distance L.
trellis_coded_modulation_ty
TrellisCodedModulation : Nat β†’ Nat β†’ Type β€” TCM scheme combining coding and modulation with bandwidth efficiency b bits/s/Hz.
tsfasman_vladut_zink_ty
TsfasmanVladutZink : Nat β†’ Prop β€” Tsfasman-Vladut-Zink theorem: AG codes exceed Gilbert-Varshamov bound for large alphabet.
turbo_code_near_capacity_ty
TurboCodeNearCapacity : Nat β†’ Nat β†’ Prop β€” turbo codes can operate within a small fraction of Shannon capacity.
turbo_code_ty
TurboCode : Nat β†’ Nat β†’ Type β€” turbo code constructed from two recursive systematic codes.
type0
udm_capacity_achieving_ty
UDMCapacityAchieving : Nat β†’ Nat β†’ Prop β€” UDMs achieve capacity of the compound channel.
ungerboeck_coded_modulation_ty
UngerboeckCodedModulation : Nat β†’ Prop β€” Ungerboeck’s set-partitioning TCM achieves coding gain without bandwidth expansion.
universally_decodable_matrix_ty
UniversallyDecodableMatrix : Nat β†’ Nat β†’ Type β€” UDM of dimension nΓ—m: rows form a code universal for combinatorial channels.
viterbi_algorithm_ty
ViterbiAlgorithm : Nat β†’ Nat β†’ Prop β€” Viterbi algorithm achieves maximum-likelihood decoding for convolutional codes.
weight_enumerator_ty
WeightEnumerator : Nat β†’ Nat β†’ Type β€” weight enumerator polynomial W_C(x, y) = Ξ£_{c ∈ C} x^{n-wt(c)} y^{wt(c)}.
wozencraft_ensemble_ty
WozencraftEnsemble : Nat β†’ Nat β†’ Prop β€” Wozencraft ensemble of random linear codes: most codes achieve GV bound.