Skip to content

Add Erdős Problem 524 (Salem–Zygmund sup norm) #3758

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

Closed
kieranmcshane wants to merge 58 commits into from
Closed

Add Erdős Problem 524 (Salem–Zygmund sup norm) #3758

Changes from all commits
Commits
Show all changes
58 commits
Select commit Hold shift + click to select a range
eed4c3a
feat: Add Erdős Problem 524 (Salem-Zygmund sup norm)
kieranmcshane Apr 16, 2026
a4f8960
feat: Add Erdős Problem 524 with machine-checked proofs
kieranmcshane Apr 16, 2026
ee95f22
feat: restore proof version and add Doob assembly skeleton
kieranmcshane Apr 16, 2026
8112438
feat: prove sub-Gaussian MGF bound for one_sided_running_max
kieranmcshane Apr 16, 2026
84703a1
feat: prove Doob maximal inequality assembly — one_sided_running_max …
kieranmcshane Apr 16, 2026
a6fab72
feat: add LIL upper bound skeleton with walk_tail_bound
kieranmcshane Apr 16, 2026
194c427
feat: add LIL upper bound proof skeleton with modular structure
kieranmcshane Apr 16, 2026
b936dae
feat: prove lil_tail_at_scale — exponential Chebyshev at LIL scale
kieranmcshane Apr 16, 2026
6b292c7
feat: modular LIL upper bound structure with 4 sorry'd components
kieranmcshane Apr 16, 2026
c515bf7
feat: prove Borel-Cantelli structure for LIL sparse subsequence
kieranmcshane Apr 16, 2026
47155cf
feat: prove kolmogorov_lil_upper_bound assembly (countable intersection)
kieranmcshane Apr 16, 2026
e8643c1
feat: refine LIL sorry structure — isolate real-analysis estimates
kieranmcshane Apr 16, 2026
6b9ac89
chore: document hsum sorry route (toReal↔ofReal + split at large k)
kieranmcshane Apr 16, 2026
4c38bdb
feat: prove lil_upper_for_eps assembly structure
kieranmcshane Apr 16, 2026
c473265
feat: document interpolation proof route and refine limsup assembly
kieranmcshane Apr 16, 2026
e8f639b
feat: prove p-series convergence structure in lil_tail_summable
kieranmcshane Apr 16, 2026
3b4d719
chore: clean up lil_tail_summable and fix build errors
kieranmcshane Apr 16, 2026
0fd9d5b
chore: clean hsum sorry
kieranmcshane Apr 16, 2026
d0dbe69
feat: remove unused levy_maximal_ineq — sorry count 10 → 9
kieranmcshane Apr 16, 2026
f2baf69
feat: verify Summable→tsum_ne_top bridge in lil_tail_summable
kieranmcshane Apr 16, 2026
c9cd4e7
chore: document Summable proof approach in lil_tail_summable
kieranmcshane Apr 16, 2026
4cb7acf
chore: simplify kolmogorov_lil_upper_bound sorry
kieranmcshane Apr 16, 2026
0b8480c
feat: verify ae extraction + threshold logic in lil_upper_for_eps
kieranmcshane Apr 16, 2026
b45e212
chore: simplify lil_tail_summable Summable sorry (avoid timeout)
kieranmcshane Apr 16, 2026
eda85f8
docs: detailed interpolation proof route for lil_interpolation
kieranmcshane Apr 16, 2026
db9de7c
chore: clean up and document all remaining sorrys
kieranmcshane Apr 16, 2026
1b72719
feat: prove floor_exp_tendsto — ⌊c^k⌋₊ → ∞ for c > 1
kieranmcshane Apr 16, 2026
3c1162d
feat: prove summability framework in lil_tail_summable
kieranmcshane Apr 16, 2026
22ef57e
chore: document IsCoboundedUnder issue in LIL assembly
kieranmcshane Apr 16, 2026
8290cec
chore: refine lil_upper_for_eps sorry documentation
kieranmcshane Apr 16, 2026
6ea4fab
feat: prove log log ⌊c^k⌋₊ → ∞ and document summability route
kieranmcshane Apr 16, 2026
817c924
feat: prove floor_c_pow_lower and log_floor_c_pow_lower
kieranmcshane Apr 16, 2026
85665e1
feat: prove exp_neg_p_log_log_floor_le — rpow comparison sorry-free!
kieranmcshane Apr 16, 2026
a77e3e8
feat: lil_tail_summable is sorry-free! Full summability chain verified.
kieranmcshane Apr 16, 2026
d75be29
feat: lil_sparse_bc is sorry-free! BC summability chain complete.
kieranmcshane Apr 16, 2026
e9ae181
chore: document lil_interpolation blockers + IsCobounded analysis
kieranmcshane Apr 16, 2026
f9d11e8
chore: clean lil_interpolation sorry
kieranmcshane Apr 16, 2026
91a39b8
feat: prove isRademacherSequence_shift via iIndepFun.precomp
kieranmcshane Apr 16, 2026
3675ec0
chore: document lil_interpolation proof route with all ingredients
kieranmcshane Apr 16, 2026
bf1eeee
chore: consolidate lil_interpolation documentation
kieranmcshane Apr 16, 2026
d92bc87
chore: simplify lil_interpolation sorry
kieranmcshane Apr 16, 2026
83eb6ec
feat: prove lil_interpolation BC structure
kieranmcshane Apr 16, 2026
8959719
chore: document hFsum proof route
kieranmcshane Apr 16, 2026
8be8a66
chore: consolidate all LIL sorrys with proof routes
kieranmcshane Apr 16, 2026
98dbead
chore: refine kolmogorov_lil_upper_bound route
kieranmcshane Apr 16, 2026
8f56fc4
feat: redefine F_k with 2√(Δn_k·log(k+2)) threshold
kieranmcshane Apr 16, 2026
8181178
chore: document hFsum proof
kieranmcshane Apr 16, 2026
3283940
chore: simplify hFsum sorry doc
kieranmcshane Apr 16, 2026
f1652d6
chore: refine set inclusion sorry
kieranmcshane Apr 16, 2026
0d9f2eb
feat: prove hFsum summability framework
kieranmcshane Apr 16, 2026
a3bcfe7
feat: prove hFsum Δ=0 case (F k = ∅ when no steps)
kieranmcshane Apr 16, 2026
450ac73
feat: prove running_max_tail application compiles in hFsum
kieranmcshane Apr 16, 2026
6877a04
feat: prove exp arithmetic in hFsum (exp(-2log(k+2)) = 1/(k+2)²)
kieranmcshane Apr 16, 2026
cc411a6
feat: prove exp arithmetic + framework in hFsum
kieranmcshane Apr 16, 2026
bf5a5d2
chore: isolate hFsum sorry to Nat.cast_sub + sqrt identity
kieranmcshane Apr 16, 2026
b2fe58d
feat: hFsum is sorry-free! Interpolation BC summability complete.
kieranmcshane Apr 16, 2026
9d44f88
chore: refine set inclusion sorry
kieranmcshane Apr 16, 2026
c6a9d39
feat: complete Kolmogorov LIL upper bound proof chain
kieranmcshane Apr 17, 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
Loading