Skip to content

feat(Expander): Poincaré inequality for elementary moves on the nonzero vectors of (ZMod P)^H #1703

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
SamuelSchlesinger merged 14 commits into from
Oct 31, 2026
Merged

feat(Expander): Poincaré inequality for elementary moves on the nonzero vectors of (ZMod P)^H #1703

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
14 commits
Select commit Hold shift + click to select a range
da700d5
feat(Expander): uniform spectral gap for the shear-translation graph …
chris-ai1 Oct 29, 2026
6553d6d
refactor(Expander): share the shears of R × R; credit the OpenAI prep…
chris-ai1 Oct 30, 2026
c1e205d
docs(Expander): credit the OpenAI Lean development for the Fourier pi…
chris-ai1 Oct 30, 2026
4ab043b
Merge remote-tracking branch 'origin/main' into feat/box-product-poin…
chris-ai1 Oct 30, 2026
40d6f14
feat(Expander): relative Poincaré inequality for shears and translati…
chris-ai1 Oct 30, 2026
3db1f8f
refactor(Expander): move the dftProd lemmas to ZModProd and drop impo…
chris-ai1 Oct 30, 2026
0736143
feat(Expander): Efron–Stein and the pair-move bound on Y × (Fin H → Z…
chris-ai1 Oct 30, 2026
a547de3
doc(Probability): cite Efron–Stein and Steele; numeric Efron–Stein te…
chris-ai1 Oct 30, 2026
0e29346
feat(Expander): Poincaré inequality for elementary moves on nonzero v…
chris-ai1 Oct 30, 2026
30c83e2
Merge origin/main into feat/shear-translation-gap-1444
chris-ai1 Oct 30, 2026
d72e8e9
Merge refreshed #1678 (30c83e230) into feat/relative-shear-translatio…
chris-ai1 Oct 30, 2026
71f089e
Merge refreshed #1695 (d72e8e9e6) into feat/coordinate-pairs-1444
chris-ai1 Oct 30, 2026
efd5aa2
Merge refreshed #1699 (71f089ecb) into feat/frame-gap-1444
chris-ai1 Oct 30, 2026
7ce5586
chore(Expander): restack nonzero-vector gap on main
SamuelSchlesinger Oct 31, 2026
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
1 change: 1 addition & 0 deletions Complexity.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -2495,6 +2495,7 @@ public import Complexity.Foundations.Combinatorics.Expander.Cayley
public import Complexity.Foundations.Combinatorics.Expander.Cheeger
public import Complexity.Foundations.Combinatorics.Expander.Connected
public import Complexity.Foundations.Combinatorics.Expander.Contraction
public import Complexity.Foundations.Combinatorics.Expander.ElementaryMove
public import Complexity.Foundations.Combinatorics.Expander.Existence
public import Complexity.Foundations.Combinatorics.Expander.Family
public import Complexity.Foundations.Combinatorics.Expander.FourthMoment
Expand Down
Loading
Loading