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 573 research declarations. Search 10,000 more complete Mathlib declarations.
573 results
Clear filtersDomain.CosetFftDomainClass.toFinset_image_toFftDomain_eq_toFinset
Plain-language statement
Scaling the normalized FFT-domain image by ω 0 recovers the original coset FFT-domain image.
Source project: ArkLib
Person-level attribution pending.
Domain.FftDomainClass.domain_implies_char_ne_2
Plain-language statement
The existence of a nontrivial smooth FFT domain rules out characteristic 2.
Source project: ArkLib
Person-level attribution pending.
Domain.FftDomainClass.neg_one_mem_domain
Plain-language statement
In a smooth FFT domain of nonzero logarithmic size, -1 belongs to the domain.
Source project: ArkLib
Person-level attribution pending.
e_mul_R_div_R_sub_1_lt_e_add_1_real
Project documentation
This lemma proves the final algebraic step in the DG25 Theorem 3.1 proof. It shows that if R > e + 1, then e * (R / (R - 1)) < e + 1. The intuition is that the fraction R / (R - 1) is always greater than 1, but as R gets larger, it gets closer to 1. The hypothesis R > e + 1 provides a strong enough bound to ensure the product e * (fraction) do...
Source project: ArkLib
Person-level attribution pending.
eagerRandomOracle_evalDist_generateSeed_bind
Plain-language statement
The eager random oracle, averaged over a uniformly sampled seed, matches the fresh independent-query semantics of evalDist. This is because the pre-sampled seed values are i.i.d. uniform, exactly matching fresh oracle queries. This is the analog of seededOracle.evalDist_liftComp_generateSeed_bind_simulateQ_run' but for eagerRandomOracle (which falls...
Source project: VCVio
Person-level attribution pending.
enforceOracle.fst_map_run_simulateQ
Plain-language statement
When the computation is within its query bound, enforcement is transparent: the output distribution is identical to running without enforcement.
Source project: VCVio
Person-level attribution pending.