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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,459 to 1,464 of 2,569 results.
JohnsonBound.sum_choose_K'
Mathematical statement
Jensen's inequality applied to choose_2 for nonzero coordinates.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.sum_hamming_weight_sum
Mathematical statement
Sum of Hamming weights equals n · |B| minus total zero-coordinate counts.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.sum_of_not_equals
Mathematical statement
Counting pairs that disagree at position i in terms of choose_2.
Source project: ArkLib
Person-level attribution pending.
JohnsonBound.sum_sum_K_i_eq_n_sub_d
Mathematical statement
Total choose_2 over all coordinates equals choose_2(|B|) · (n - d).
Source project: ArkLib
Person-level attribution pending.
KEMScheme.IND_CPA_Game_eq_IND_CCA_Game_toIND_CCA
Mathematical statement
The one-stage IND-CPA game is exactly the IND-CCA game instantiated with the trivial CPA-to-CCA embedding (toIND_CCA) that never uses the decryption oracle.
Source project: VCVio
Person-level attribution pending.
KEMScheme.ind_cpa_one_time_bias_advantage_compose_with_dem_le
Mathematical statement
Proof-ladders A1 reduction statement: the one-time IND-CPA advantage of textbook KEM+DEM is bounded by two KEM IND-CPA advantages plus one DEM IND-CPA advantage, using the canonical left/right and DEM reductions defined above. The runtime coherence hypotheses require runtime.evalDist to be a monad morphism (preserves pure and distributes >>=) and to...
Source project: VCVio
Person-level attribution pending.