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 350 research declarations. Search 10,000 more complete Mathlib declarations.
350 results
Clear filtersList.mapUnion_union_mapUnion'
Plain-language statement
mapUnion_union_mapUnion applies when you have the same function f and different input lists. mapUnion_union_mapUnion' applies when you have different functions f/g and the same input list.
Source project: Cedar Specification
Person-level attribution pending.
map_construction
Plain-language statement
The T-transform is natural in any oracle-semantics morphism that preserves both the plaintext-to-coins query capability and the distinguished lift of ProbComp.
Source project: VCVio
Person-level attribution pending.
MerkleTree.completeness
Project documentation
Completeness theorem for Merkle trees: for any full binary tree with 2 ^ n leaves, and for any index i, the honestly-generated opening proof verifies against the honestly-built root with probability one.
Source project: VCVio
Person-level attribution pending.
MerkleTree.functional_completeness
Project documentation
A functional completeness theorem for Merkle proofs built from buildMerkleTree_with_hash.
Source project: VCVio
Person-level attribution pending.
negligible_polynomial_mul
Project documentation
If f is negligible, then fun n => ↑(p.eval n) * f n is negligible for any polynomial p. This is the key lemma for handling polynomial-loss security reductions.
Source project: VCVio
Person-level attribution pending.
ofReal_tvDist_bind_left_le_const
Plain-language statement
ℝ≥0∞ form of tvDist_bind_left_le_const, matching the quantitative APIs: a per-a bound ENNReal.ofReal (tvDist (f a) (g a)) ≤ ε on the support of mx lifts through the shared bind.
Source project: VCVio
Person-level attribution pending.