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 6 research declarations. Search 10,000 more complete Mathlib declarations.
6 results
Clear filtersDomain.CosetFftDomain.twoNthRoot_correct
Plain-language statement
The value returned by twoNthRoot is a 2 ^ ith root of its input.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomainClass.card_block_of_mem_subdomain
Plain-language statement
If x lies in the (i + j)th subdomain, then it has exactly 2 ^ j preimages under y ↦ y ^ 2 ^ j from the ith subdomain.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomainClass.mem_subdomain_of_le_of_mem_subdomain
Plain-language statement
If j ≤ i, then we do not have x ∈ subdomain ω i → x ∈ subdomain ω j in the general case but rescaling x as ω 0 ^ 2 ^ j * (ω 0)⁻¹ ^ 2 ^ i * x gives us a member of subdomain ω j.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomainClass.pow_mem_of_mem
Plain-language statement
If x lies in the jth subdomain, then x ^ 2 ^ i lies in the (j + i)th subdomain, provided j + i ≤ n.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomainClass.square_roots_explicit
Plain-language statement
The square roots of x inside the ith subdomain are exactly y and -y, for any square root y of x.
Source project: ArkLib
Person-level attribution pending.
Domain.CosetFftDomainClass.subdomain_toFftDomain_comm
Plain-language statement
Normalizing the ith coset subdomain agrees with taking the ith FFT subdomain of the normalized domain.
Source project: ArkLib
Person-level attribution pending.