Add Erdős Problem 524 (Salem–Zygmund sup norm)#3787
Open
kieranmcshane wants to merge 59 commits intogoogle-deepmind:mainfrom
Open
Add Erdős Problem 524 (Salem–Zygmund sup norm)#3787kieranmcshane wants to merge 59 commits intogoogle-deepmind:mainfrom
kieranmcshane wants to merge 59 commits intogoogle-deepmind:mainfrom
Conversation
Formalize and partially certify Chojecki (Jan 2026) resolution of Erdős Problem 524 on sup norm of random ±1 polynomials on [-1,1]. Machine-verified proofs (sorry-free, Lean kernel checked): - Two-walk sandwich (Corollary 3): Abel summation + weight telescoping - Subgaussian tails assembly: measure_mono + union bound + 2+2=4 - Running-max tail bound: set decomposition + neg Rademacher + arithmetic - Submartingale adapted + integrable cases: Filtration.natural + exp composition - isRademacherSequence_neg_mul: iIndepFun.comp + parity case split - rademacher_ae_mem_pm_one, rademacher_walk_nonneg_prob, identDistrib helpers Remaining sorry's (infrastructure gaps, not paper errors): - one_sided_running_max: Doob maximal_ineq wiring (~50 lines) - sharp_upper_envelope: Kolmogorov LIL (not in Mathlib) - sparse_lower_envelope: 2D KMT coupling (multi-year project) - exact_lower_constant: open problem in mathematics Paper: https://www.ulam.ai/research/erdos524.pdf
Restore the 1073-line proof version from reflog (831ff19). Break the one_sided_running_max sorry into two modular pieces: - hdobo: Doob's maximal inequality application (sorry) - hmgf: sub-Gaussian MGF bound via Hoeffding's lemma (sorry) - Combination step: fully proven via exp_sub + field_simp algebra Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Prove E[exp(λ·S_n)] ≤ exp(λ²n/2) via: - iIndepFun.mgf_sum: factorize MGF of walk as product of individual MGFs - hasSubgaussianMGF_of_mem_Icc_of_integral_eq_zero (Hoeffding's lemma): each Rademacher a_j ∈ [-1,1] with E[a_j]=0 gives mgf ≤ exp(lam²/2) - Product of exp = exp of sum: ∏ exp(lam²/2) = exp(n·lam²/2) Also prove the Doob+MGF combination step: P(walk≥t) ≤ E[f_n]/exp(λt) ≤ exp(λ²n/2)/exp(λt) = exp(-t²/(2n)) Only sorry remaining in one_sided_running_max: the Doob maximal inequality application (connecting maximal_ineq to the probability bound). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
…is sorry-free
Complete the final sorry in one_sided_running_max by applying Doob's
maximal inequality (maximal_ineq) to the exponential submartingale:
- Set containment: {walk ≥ t} ⊆ {sup' f ≥ exp(λt)} via exp monotonicity
- Doob bound: ε·ℙ(sup'≥ε) ≤ E[f_n·1_{sup'≥ε}] ≤ E[f_n]
- ENNReal→ℝ conversion: ℙ(A) ≤ E[f_n]/exp(λt)
Combined with the previously proven sub-Gaussian MGF bound and
combination algebra, one_sided_running_max is now fully proven.
Sorry count: 6 → 5. Remaining sorrys:
- erdos_524 (meta-wrapper)
- sharp_upper_envelope (Kolmogorov LIL not in Mathlib)
- levy_maximal_ineq (first-crossing decomposition)
- sparse_lower_envelope (2D KMT, multi-year)
- exact_lower_constant (open in mathematics)
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add section LIL with: - lilNorm: normalizing function √(2n log log n) - walk_tail_bound: ℙ(S_n ≥ t) ≤ exp(-t²/(2n)), proven via one_sided_running_max (corollary of Doob's maximal inequality) - kolmogorov_lil_upper_bound: limsup S_n/√(2n log log n) ≤ 1 a.s. (sorry'd — proof sketch via sparse subsequence + first BC + interpolation documented in docstring) The walk_tail_bound is the key input for the Borel-Cantelli argument. The full LIL proof requires ~300 more lines of real-analysis estimates. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Add lil_upper_for_eps (core: sparse subsequence + first BC + interpolation) and kolmogorov_lil_upper_bound (assembly: take ε → 0). Both sorry'd pending ~300 lines of real-analysis estimates. walk_tail_bound is proven (ℙ(S_n ≥ t) ≤ exp(-t²/(2n)) via one_sided_running_max). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Prove ℙ(S_n ≥ (1+ε)·√(2n log log n)) ≤ exp(-(1+ε)²·log log n) via walk_tail_bound + algebraic simplification of the exponent. This is the key input for the first Borel-Cantelli argument on the sparse subsequence in the LIL upper bound proof. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Break kolmogorov_lil_upper_bound into 4 modular components:
1. lil_tail_at_scale (PROVEN): ℙ(S_n ≥ (1+ε)·φ(n)) ≤ exp(-(1+ε)²·log log n)
2. lil_sparse_bc (sorry): a.s. eventually S_{n_k} < (1+ε)·φ(n_k)
on sparse subsequence, via summability + first Borel-Cantelli
3. lil_interpolation (sorry): |S_n - S_{n_k}| ≤ ε·φ(n) a.s. eventually,
via running-max bound on increments + Borel-Cantelli
4. lil_upper_for_eps (sorry): assembly combining 2+3
5. kolmogorov_lil_upper_bound (sorry): take ε → 0
Each sorry has a clear proof sketch. The main blockers are:
- Summability estimates (∑ k^{-p} for p > 1)
- Real-analysis bounds on ⌊c^k⌋ growth and log log asymptotics
- Independence of walk increments for the interpolation step
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
In lil_sparse_bc, prove the first Borel-Cantelli application:
- Define events E_k = {S_{n_k} ≥ (1+ε)·φ(n_k)}
- Apply measure_setOf_frequently_eq_zero (first BC)
- Convert "not frequently E_k" to "eventually S_{n_k} < bound"
Remaining sorry: hsum (∑ ℙ(E_k) < ∞), which requires:
- lil_tail_at_scale to bound each ℙ(E_k)
- lil_tail_summable (sorry) for the series comparison
Also added lil_tail_summable as a separate sorry for the
real-analysis estimate that ∑ exp(-(1+ε)²·log log ⌊c^k⌋₊) < ∞.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Prove the ε → 0 step: if for each m ≥ 1 a.s. eventually f(n) ≤ 1+1/m, then a.s. limsup f ≤ 1. Uses ae_all_iff for the countable intersection. The final limsup_le step is sorry'd pending IsCobounded/IsBounded conditions for the walk ratio (straightforward from walk growth bounds). Also proves the Borel-Cantelli logic in lil_sparse_bc: the conversion from "not frequently" to "eventually not" is machine-verified. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Refine the sorry decomposition in the LIL upper bound: - lil_sparse_bc: BC logic proven, hsum sorry isolated to pointwise ℙ(E_k) ≤ ofReal(exp(...)) comparison - kolmogorov_lil_upper_bound: countable intersection proven, final limsup_le sorry isolated to IsCobounded/IsBounded conditions - lil_tail_summable: sorry isolated to p-series convergence estimate The logical backbone (Doob → tail → Chebyshev → BC → countable ∩) is fully machine-verified. Remaining sorrys are pure real-analysis estimates (floor asymptotics, p-series, log growth, toReal↔ofReal). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The hsum comparison requires splitting the tsum at k=N where n_k becomes large enough for lil_tail_at_scale. For k < N, use ℙ ≤ 1 (finite sum). For k ≥ N, use the exponential tail bound + comparison with lil_tail_summable. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Show how sparse BC + interpolation combine to give the full result:
- Choose δ = ε/3 and c = 1 + δ
- Apply lil_sparse_bc (a.s. eventually S_{n_k} < (1+δ)·φ(n_k))
- Apply lil_interpolation (a.s. eventually |increment| ≤ δ·φ(n))
- Combine: S_n ≤ S_{n_k} + |increment| < (1+2δ)·φ(n) ≤ (1+ε)·φ(n)
Remaining sorry: the arithmetic combining step
(S_n decomposition + φ monotonicity + 2δ ≤ ε).
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
- lil_interpolation: detailed 5-step proof route documented (shifted walk independence, running-max tail, summability, asymptotics, BC) - kolmogorov_lil_upper_bound: by_contra + Archimedean structure (find m with 1+1/m < limsup, contradict eventually ≤ 1+1/m) - lil_upper_for_eps: assembly structure proven (δ=ε/3, c=1+δ, combine) All sorry routes are clearly documented. The logical backbone is verified. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Apply Summable.of_norm_bounded_eventually_nat with comparison function
k^{-(1+ε)²} and Real.summable_nat_rpow for the convergence (since
(1+ε)² > 1 implies -(1+ε)² < -1).
Remaining sorry: the pointwise eventually bound
‖exp(-(1+ε)²·log log ⌊c^k⌋₊)‖ ≤ k^{-(1+ε)²}
which is a floor/log asymptotic estimate (log ⌊c^k⌋₊ ≥ k for large k).
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Simplify lil_tail_summable sorry to a clean single sorry with documented proof route (p-series comparison via summable_nat_rpow + floor/log asymptotics). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Remove levy_maximal_ineq (unused standalone sorry) since one_sided_running_max provides the stronger exp(-t²/(2n)) bound via Doob's inequality. This eliminates one sorry warning. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Structure lil_tail_summable as: prove Summable f (sorry'd), then exact hsummable.tsum_ofReal_ne_top. The bridge from Summable to ∑' ENNReal.ofReal ≠ ⊤ is now machine-verified. Remaining sorry: the Summable proof itself (p-series comparison via Summable.of_norm_bounded_eventually_nat + floor/log asymptotics). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The Summable sorry needs Summable.of_norm_bounded_eventually_nat
with floor/log asymptotic estimates. Documented multiple approaches
(sharp k^{-p} bound, crude 1/k² bound).
9 sorrys remain, 0 errors. All proof structures verified.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The limsup ≤ 1 from "∀ m, eventually ≤ 1+1/m" needs IsCoboundedUnder for limsup_le_of_le, which requires a lower bound on the walk ratio. Sorry'd pending the coboundedness plumbing. 9 sorrys, 0 errors. Countable intersection (ae_all_iff) is verified. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Extract both ae events via filter_upwards, obtain thresholds K₁, K₂ via eventually_atTop.mp, set K = max K₁ K₂. Remaining sorry: the arithmetic combining step (find k for each n, decompose S_n, bound via φ monotonicity, verify 2δ ≤ ε). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Replace verbose comparison attempt (caused timeout) with clean sorry. The Summable proof needs Summable.of_norm_bounded_eventually_nat with floor/log asymptotic estimates — documented but not formalized. 1338 lines, 34 theorems (25 sorry-free), 9 sorrys, 0 errors. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Document the 4-step interpolation strategy:
1. Bound ℙ(F_k) via running_max_tail with threshold C·√(Δn_k·log k)
2. Summability of k^{-C²/2} for C > √2
3. Asymptotic comparison: C·√(Δn_k·log k) ≤ ε·φ(n) for c near 1
4. First BC gives a.s. control
The formal proof needs: shifted walk independence, running_max_tail
application, p-series summability, and floor/log asymptotic comparison.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
All 9 sorry locations have detailed proof routes documented. The logical backbone is fully machine-verified: - Submartingale construction → Doob → one_sided_running_max (sorry-free) - running_max_tail → subgaussian_tails (sorry-free) - two_walk_sandwich (sorry-free) - LIL infrastructure: tail bound, Chebyshev, BC logic, countable ∩ Remaining sorrys are all real-analysis estimates or blocked: - lil_tail_summable: Summable via p-series comparison - lil_sparse_bc (hsum): ENNReal tsum splitting - lil_interpolation: increment running-max + asymptotic comparison - lil_upper_for_eps: S_n decomposition + φ monotonicity - kolmogorov_lil_upper_bound: IsCoboundedUnder + Archimedean - erdos_524, sharp_upper_envelope: need full LIL - sparse_lower_envelope: blocked (2D KMT) - exact_lower_constant: open mathematics Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Prove that ⌊c^k⌋₊ → ∞ as k → ∞ for c > 1, using: - tendsto_pow_atTop_atTop_of_one_lt: c^k → ∞ - Nat.sub_one_lt_floor: x - 1 < ⌊x⌋₊ This is a key asymptotic ingredient for the LIL summability estimates. Sorry-free, 0 errors. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Structure: summable_one_div_nat_pow (p=2>1, proven) → of_norm_bounded_eventually_nat (comparison, proven) → eventually pointwise bound (sorry: floor/log asymptotics). The sorry is now a single estimate: ∀ᶠ k, (1+ε)²·log log ⌊c^k⌋₊ ≥ 2·log k which follows from floor_exp_tendsto + log monotonicity. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The kolmogorov_lil_upper_bound sorry requires IsCoboundedUnder, which needs a lower bound on walk/φ. By symmetry of the Rademacher walk (walk and -walk have the same distribution), the upper bound for -walk gives the needed lower bound for walk. 1365 lines, 9 sorrys, 0 errors. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Prove that exp(-p·log log ⌊c^k⌋₊) ≤ (log c/2)^{-p} · k^{-p} eventually,
using:
- log_floor_c_pow_lower for the floor/log bound
- Real.rpow_def_of_pos for exp(log x · y) = x^y
- mul_rpow for (a·b)^p = a^p · b^p
This replaces the old log_log_floor_ge_log which required p ≥ 2.
The new comparison works for ALL p > 0, avoiding the p < 2 issue.
Sorry count: 10 → 9. Three new sorry-free lemmas in this session:
floor_c_pow_lower, log_floor_c_pow_lower, exp_neg_p_log_log_floor_le.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Close the last sorry in lil_tail_summable by chaining:
- exp_neg_p_log_log_floor_le: exp(-p·log log n_k) ≤ C·k^{-p} eventually
- Real.summable_nat_rpow: ∑ k^{-p} converges for p > 1
- Summable.of_norm_bounded_eventually_nat: comparison test
The full chain floor_c_pow_lower → log_floor_c_pow_lower →
exp_neg_p_log_log_floor_le → lil_tail_summable is machine-verified.
Sorry count: 9 → 8.
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Close the hsum sorry in lil_sparse_bc by pointwise comparison: - ℙ(E k) ≤ ofReal(exp(-(1+ε)²·log log n_k)) for ALL k - When log log n_k ≤ 0: exp(nonneg) ≥ 1 ≥ ℙ(E k) - When log log n_k > 0 and n_k ≥ 1: lil_tail_at_scale - When n_k = 0: log 0 = 0, so exp(0) = 1 ≥ ℙ(E k) - Sum comparison via lil_tail_summable (now sorry-free) Uses le_ofReal_iff_toReal_le for the ENNReal↔ℝ conversion. Sorry count: 8 → 7. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The 3 remaining LIL sorrys form a chain: lil_interpolation → lil_upper_for_eps → kolmogorov_lil_upper_bound lil_interpolation needs: (1) shifted walk Rademacher property (iIndepFun.comp with injective shift) (2) running_max_tail on the increment (3) second BC application with summable tails (4) asymptotic comparison C·√(Δn_k·log k) vs ε·φ(n) kolmogorov_lil_upper_bound needs IsCoboundedUnder, which requires applying lil_upper_for_eps to -walk (Rademacher symmetry). 7 sorrys, 0 errors. ~30 sorry-free theorems. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The shifted Rademacher sequence (fun j => a (m+j)) is i.i.d. Rademacher because iIndepFun.precomp with the injective shift (m+·) preserves independence, and the marginals are unchanged. This is the key ingredient for lil_interpolation's shifted walk argument. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
All ingredients for lil_interpolation are now proven and available: - isRademacherSequence_shift (sorry-free): shifted walk is Rademacher - running_max_tail (sorry-free): bounds running max of Rademacher walk - measure_setOf_frequently_eq_zero (Mathlib): first Borel-Cantelli - floor_exp_tendsto (sorry-free): ⌊c^k⌋₊ → ∞ The sorry is pure assembly: reindex the walk sum, apply running_max_tail, BC summability, and asymptotic comparison (~50 lines). 7 sorrys, 0 errors, ~35 sorry-free theorems. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
All ingredients proven. Sorry is pure assembly (~50 lines): - Finset sum reindexing for walk difference identity - running_max_tail on shifted Rademacher walk - BC summability with 2/(k+2)² - Asymptotic: Δn_k·log(k+2)/(n·log log n) → 0 1465 lines, 7 sorrys, 0 errors, ~35 sorry-free theorems. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The outer Borel-Cantelli structure of lil_interpolation is verified: - Define events F_k (increment running max exceeds ε·lilNorm) - hFsum: ∑ ℙ(F_k) < ∞ (sorry — needs running_max_tail + comparison) - measure_setOf_frequently_eq_zero: a.s. eventually ¬F_k - calc chain: convert ¬(eventually bounded) to frequently F_k (sorry) The BC logic itself is machine-verified. Two inner sorrys remain: (1) hFsum summability (running_max_tail application) (2) set inclusion (walk difference = shifted walk + lilNorm monotonicity) Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
1483 lines, 8 sorrys, 0 errors, ~35 sorry-free theorems. LIL sorry chain (4 sorrys, all pure assembly): - hFsum (1199): running_max_tail on shifted walk + summability comparison - set inclusion (1212): walk difference identity + lilNorm monotonicity - lil_upper_for_eps (1239): covering + decomposition + δ-arithmetic - kolmogorov_lil_upper_bound (1272): IsCoboundedUnder + Archimedean Non-LIL sorrys (4): - erdos_524 (385): meta-wrapper - sharp_upper_envelope (414): needs full LIL + Chung - sparse_lower_envelope (1448): blocked (2D KMT) - exact_lower_constant (1481): open mathematics All mathematical ingredients are sorry-free. Remaining work is Lean API plumbing for connecting proven components. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Redefine the bad events in lil_interpolation to use threshold 2√(Δn_k·log(k+2)) instead of ε·lilNorm(n_k). This gives: - ℙ(F_k) ≤ 2/(k+2)² via running_max_tail with u=2√(log(k+2)) - Summable tails (∑ 2/(k+2)² converges) for ALL ε > 0 and c > 1 - Eventually 2√(Δn_k·log(k+2)) ≤ ε·lilNorm(n) (asymptotic comparison) The old threshold ε·lilNorm(n_k) required ε²/c > 1 which fails for small ε. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The tsum comparison structure for hFsum in lil_interpolation is verified: - ne_top_of_le_ne_top with summable bound - ENNReal.tsum_le_tsum for pointwise comparison - Summable bound: 2 * (summable_one_div_nat_pow shifted by +2) via comp_injective with Nat.add_right_cancel Remaining sorry: pointwise ℙ(F k) ≤ ofReal(2*exp(-2*log(k+2))) (running_max_tail on shifted walk + exp↔rpow conversion). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
When Δn_k = ⌊c^(k+1)⌋₊ - ⌊c^k⌋₊ = 0, the Finset.Icc 1 0 is empty, so F k = ∅ and ℙ(F k) = 0. Proved via Finset.mem_Icc + omega. The Δ > 0 case (running_max_tail application) remains sorry'd. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The running_max_tail on the shifted Rademacher walk (isRademacherSequence_shift) compiles with u = 2√(log(k+2)) and Δ steps. Remaining sorry: set equality (F k = running_max event) + ENNReal conversion + exp(-2log(k+2)) = 1/(k+2)² arithmetic. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Close the exp↔rpow conversion step in the hFsum calc:
- u² = 4·log(k+2) via sq_sqrt
- exp(-2·log(k+2)) = (k+2)^{-2} via rpow_def_of_pos
- (k+2)^{-2} = 1/(k+2)² via rpow_neg + rpow_natCast + push_cast
Remaining sorry in hFsum: connecting F_k set to running_max_tail
(set containment + measure_mono + toReal conversion).
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The hFsum calc proof is nearly complete: - Δ=0 case: proven (empty Finset.Icc) - Δ>0 case: running_max_tail compiles, exp(-2log(k+2))=1/(k+2)² proven - Remaining: set containment F_k = running_max event (~5 lines, Nat.cast issue) The exp↔rpow conversion chain is fully verified: u²=4log(k+2) → exp(-2log(k+2)) → rpow_neg → rpow_natCast → 1/(k+2)² Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
The hFsum proof structure is nearly complete: - Δ=0 case: proven - Δ>0 case: running_max_tail compiles, exp arithmetic proven - Remaining: threshold equality (Nat.cast_sub + √(a·b)=√a·√b) and measure_mono from set containment. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Close the hFsum sorry in lil_interpolation: - Set equality: F_k = running_max event via hthresh (Nat.cast_sub + sqrt_mul + mul_assoc) and hthresh ▸ for both Iff directions - Running_max_tail on shifted walk: isRademacherSequence_shift - Exp arithmetic: exp(-2log(k+2)) = 1/(k+2)² via rpow chain - Summability: ∑ 2/(k+2)² via summable_one_div_nat_pow + comp_injective - First BC: measure_setOf_frequently_eq_zero Sorry count: 8 → 7. Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
All closeable proof obligations discharged. The full LIL upper bound chain is machine-verified: Rademacher infrastructure, submartingale construction, Doob maximal inequality, sub-Gaussian MGF, running max tail bound, LIL summability, sparse Borel-Cantelli, interpolation, assembly, and limsup bound. 4 blocked sorrys remain (Chung's exact LIL / LIL lower bound — not in Mathlib). Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Keep definitions, docstrings, and theorem signatures with sorry. Remove all proof bodies (Abel summation helpers, LIL infrastructure, subgaussian tails proof, two-walk sandwich proof). Full proofs available at: https://github.com/kieranmcshane/formal-conjectures/tree/add-erdos-524 Fixes google-deepmind#770 Co-Authored-By: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
|
Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA). View this failed invocation of the CLA check for more information. For the most up to date status, view the checks section at the bottom of the pull request. |
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Formalizes Erdős Problem 524 (Salem–Zygmund sup norm of random ±1 polynomials on [-1, 1]).
IsRademacherSequence,randomPoly,supNorm,walk,alternatingWalk,GaoLiWellnerConstantserdos_524) and five variant theorems from Chojecki's January 2026 resolution:sharp_upper_envelope: lim sup M_n / √(2n log log n) = 1 a.s.subgaussian_tails: ℙ(M_n ≥ u√n) ≤ 4 exp(-cu²)two_walk_sandwich: max(|S_n|, |T_n|) ≤ M_n ≤ max(max_k |S_k|, max_k |T_k|)sparse_lower_envelope: lower envelope on subsequence n_m = ⌊e^{m³}⌋exact_lower_constant(open): exact small-ball constant for Y(u) = ∫₀¹ e^{-us} dB(s)Statements only per repo guidelines. Extended proofs (Abel summation, LIL upper bound, subgaussian tails) are in the
add-erdos-524branch.Fixes #770
🤖 Generated with Claude Code