Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 4 research declarations. Search 10,000 more complete Mathlib declarations.
4 results
Clear filtersProximityGap.exists_large_of_finset_cover
Plain-language statement
Pigeonhole for finite covers: if U is covered by L indexed subsets and L * B < |U|, then some subset has more than B elements.
Source project: ArkLib
Person-level attribution pending.
ProximityGap.jointAgreement_implies_linSpan_proximity
Plain-language statement
Generalisation of jointAgreement_implies_second_proximity to an arbitrary word stack over a submodule code. If a stack W : Fin k → ι → F jointly agrees with a submodule C ⊆ ι → F, then every element of the linear span of the stack is δ-close to C. The pointwise case W i ∈ C is the special case x = W i (choose coefficients c to be the i-th...
Source project: ArkLib
Person-level attribution pending.
ProximityGap.prob_coeff_eq_prob_affine
Plain-language statement
The coefficient-parameterised probability equals the subtype probability. The map r ↦ u₀ + ∑ rᵢ • dᵢ has constant-cardinality fibers (cosets of the kernel of the linear part), so pushforward of uniform gives uniform.
Source project: ArkLib
Person-level attribution pending.
ProximityGap.relDistFromCode_smul_eq
Plain-language statement
Relative distance to a submodule is invariant under scaling by a unit: δᵣ(z • u, V) = δᵣ(u, V) for z ≠ 0 and V a submodule. Key step in BCIKS20 §6.3 (Step 1c).
Source project: ArkLib
Person-level attribution pending.