feat(MagicFunction): estimates for the double-zero contour deformation - #466
Draft
cameronfreer wants to merge 69 commits into
Draft
cameronfreer wants to merge 69 commits into
cameronfreer wants to merge 69 commits into
Conversation
Add FourierExpansions.lean with infrastructure for Corollary 7.5-7.7 bounds: - Coefficient functions c_E₂E₄E₆ and c_E₄_sq with polynomial growth O(n^5) - norm_exp_pi_I_z_lt_one: |exp(πiz)| < 1 for z : ℍ - isBigO_shift: shifting preserves Big-O growth (sorry) - summable_fouterm_of_poly: polynomial × geometric summability (sorry) - Stubs for q-expansion identities from PR thefundamentaltheor3m#268 (sorries) Also make fouterm public in PolyFourierCoeffBound.lean for use by other files. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Add PhiBounds.lean with: - PhiBounds structure bundling Corollary 7.5-7.7 bounds on φ₀, φ₂', φ₄' - phiBounds instance using explicit DivDiscBound constants (avoids axiom of choice) - Bounds use 1/2 < z.im condition matching the blueprint Update SpherePacking.lean imports. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Complete the proof that shifting a coefficient function by a constant preserves polynomial growth (Big-O). Uses the approach from hpoly' in PolyFourierCoeffBound.lean: 1. Show shifted function c(n + n₀) is O((n + n₀)^k) via exact_mod_cast 2. Then |n + n₀| ≤ 2n for n ≥ |n₀|, so (n + n₀)^k = O(n^k) This is needed for summability of Fourier series with polynomial-growth coefficients. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Complete the proof that Fourier series with polynomial-growth coefficients are summable for z in the upper half plane. The proof: 1. Factors fouterm c z (i + n₀) = u(i) * r^i where r = cexp(πIz) 2. Shows u(i) = c(i+n₀) * const has O(n^k) growth via IsBigO.const_mul_left 3. Since ‖r‖ < 1 (by norm_exp_pi_I_z_lt_one), applies summable_real_norm_mul_geometric_of_norm_lt_one This completes the infrastructure for proving phi bounds via Fourier expansions. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
…f_poly Simplify proofs: - isBigO_shift: use omega directly instead of linarith chain - summable_fouterm_of_poly: inline hexp, use show for mul_comm Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Replace sorry stubs for E₂_mul_E₄_sub_E₆_qexp and E₄_qexp with proofs using E₂_mul_E₄_sub_E₆ and E₄_sigma_qexp from FG.lean, which were added in PR thefundamentaltheor3m#268.
Use E₂_mul_E₄_sub_E₆ and E₄_sigma_qexp from FG.lean directly instead of re-exporting with local wrappers.
Replace PhiBounds structure with individual theorems in two forms: **Explicit constant bounds:** - φ₀_bound: ‖φ₀ z‖ ≤ C_φ₀ * exp(-2πt) - φ₂'_bound: ‖φ₂' z‖ ≤ C_φ₂' - φ₄'_bound: ‖φ₄' z‖ ≤ C_φ₄' * exp(2πt) **Big O bounds (along imaginary axis):** - φ₀_isBigO: O(exp(-2πt)) - φ₂'_isBigO: O(1) - φ₄'_isBigO: O(exp(2πt)) The constants C_φ₀, C_φ₂', C_φ₄' are explicit DivDiscBound values.
…tness The φ₂' bound involves E₄(E₂E₄-E₆), which is a PRODUCT, not a square. The Fourier coefficients for this product differ from those of the square (E₂E₄-E₆)². Previously both were using c_E₂E₄E₆, which is semantically wrong even if the simplified coefficient definitions happen to match. This commit introduces c_E₄_E₂E₄E₆ for the product case to: 1. Make the mathematical intent explicit 2. Enable future refinement with proper Cauchy product coefficients 3. Ensure callsites use semantically correct coefficient functions Changes: - FourierExpansions.lean: - Add c_E₄_E₂E₄E₆ definition (currently same as c_E₂E₄E₆) - Add c_E₄_E₂E₄E₆_poly lemma - Update summable_E₄_E₂E₄E₆ to use c_E₄_E₂E₄E₆ - Update E₄_E₂E₄E₆_fourier to use c_E₄_E₂E₄E₆ - PhiBounds.lean: - Update C_φ₂' to use c_E₄_E₂E₄E₆ - Update C_φ₂'_pos to use c_E₄_E₂E₄E₆_poly - Update φ₂'_bound to use c_E₄_E₂E₄E₆ Note: On this branch, c_E₄_E₂E₄E₆ = c_E₂E₄E₆ definitionally (both are n·σ₃(n)). The distinction matters for proving the Fourier expansion identities, which require the actual Cauchy product coefficients.
- φ₂'_bound: collapse 4-line exp(0) calc into convert + norm_num - summable_fouterm_of_poly: ring → ring_nf to close cleanly (silence the ring-fallback 'Try this' info from mismatched cexp atoms)
Even-support q→fouterm reindex (q=exp(2πiz) ↦ r=exp(πiz), m-th coeff at index 2m) via Function.Injective.tsum_eq along m ↦ 2m. Foundation for the Design-B factor-and-dominate φ-bound proofs.
bE₄ coefficients + E₄_qexp_nat (ℕ-indexed q-series, reusing E₄_sigma_qexp) + E₄_eq_fouterm (n₀=0). Design B linear-factor identity for E₄.
g_qexp_nat (ℕ-form via PNat reindex, reusing E₂_mul_E₄_sub_E₆) + g_eq_fouterm (n₀=2 via (·+2) reindex; index-0,1 terms vanish). Completes Design B linear identities.
evenCoeff_isBigO (even-support preserves growth) + bg_isBigO, bE₄_isBigO (via sigma_le_pow_succ). Same O(n^5) as old placeholders, no convolution.
g_div_Δ_bound (‖(E₂E₄-E₆)/Δ‖ ≤ DivDiscBound, constant) and E₄_div_Δ_bound (‖E₄/Δ‖ ≤ DivDiscBound·exp(2π·im)) — Design B thefundamentaltheor3m#3.
norm_qseries_shift_le: ‖∑ a(m)·q^(m+n₀)‖ ≤ (∑‖a m‖·exp(-πm))·exp(-2π·n₀·im) for im ≥ 1/2. Reusable factor-norm estimate. Also drop internal section labels.
norm_E₄_le (‖E₄‖ ≤ B_E₄, const) and norm_g_le (‖E₂E₄-E₆‖ ≤ B_g·exp(-2π·im)) via norm_qseries_shift_le, plus supporting summability/shift lemmas (B_E₄, B_g defined as explicit tsums).
C_φ₀/C_φ₂'/C_φ₄' now = (factor-norm bound)·DivDiscBound(linear coeff); each
φ_bound proved as ‖factor‖·‖linear/Δ‖ via norm_{E₄,g}_le + {g,E₄}_div_Δ_bound.
No longer depends on the placeholder product/square identities.
…tities Remove c_E₂E₄E₆/c_E₄_E₂E₄E₆/c_E₄_sq, their poly/summable lemmas, and the three false product/square fouterm identities (now unused after the factor-and-dominate rewire). FourierExpansions.lean and PhiBounds.lean are now sorry-free.
Add module / public import / @[expose] public section so the module aggregator SpherePacking.lean can public-import them. Full lake build now green.
- move module docstrings before @[expose] public section (doc-string-first lint) - drop unused hσ helpers in B_g_pos / divDiscBound_bg_pos (simp closes directly) - drop unused bg simp arg in g_eq_fouterm's n≠1 case - replace 'show'-based omega proofs with term-mode (two_mul / Nat.sub_add_cancel) - remove redundant 'by exact'; ring_nf in E₄_div_Δ_bound - wrap lines to the 100-char limit
Add a small 'norm_mul_le_mul' (‖a·b‖ ≤ x·y from ‖a‖≤x, ‖b‖≤y, 0≤x) and use it in all three φ-bounds, so each reads as (factor-norm bound)·(quotient bound) — making the C_φ₀/C_φ₂'/C_φ₄' constants' shape canonical. No statement/API change.
…ound.hpoly' isBigO_shift was hpoly' + Nat.cast_pow; not part of the intended API. Remove it and use hpoly' directly in summable_fouterm_of_poly (reordering u = const * c(i+n₀) so the explicit commutativity rewrite disappears too).
- norm_exp_pi_I_z_lt_one: collapse the manual re-computation into a single simpa - keystone/g_eq_fouterm injectivity: Nat.mul_left_cancel / Nat.add_right_cancel term-mode instead of have+omega - htend: term-mode Filter.tendsto_atTop_atTop.mpr - norm_E₄_le / norm_g_le: inline the have h := …; simpa using h into one simpa
…term_of_poly Step 3 still described the old `isBigO_shift + multiplication by constant` route; the code now uses `(hpoly' c n₀ k hpoly).const_mul_left const` (PolyFourierCoeffBound.hpoly' for the n₀-shift, then const_mul_left for the constant). Comment-only.
Step 5a: the analytic estimates behind the alternate integral representation of `a` used in the double-zeroes argument, extracted from thefundamentaltheor3m#296/thefundamentaltheor3m#297 and rebuilt as a single focused module. New `a/DoubleZeroes/CuspBounds.lean`: * `norm_φ₀_S_smul_le` — the three-term S-transform bound for any z : ℍ with Im z ≥ 1, from `φ₀_S_transform` and the `PhiBounds` estimates; * `norm_φ₀''_I_div_t_le` — its specialisation to z = it (blueprint Cor 7.13); * `norm_φ₀_I_div_t_small` (thesis Lemma 4.4.3) — for t ∈ (0,2), the point i/t has Im > 1/2 and the cusp bound gives decay exp(-2π/t); * `norm_φ₀_I_div_t_large` (thesis Lemma 4.4.4) — for t ≥ 2, the S-transform bound gives growth O(t⁻² e^{2πt}). The vertical/top-edge integrands, their integrability and their vanishing at infinity are deliberately not here: they belong with the contour deformation. Claude-Session: https://claude.ai/code/session_01FvNZchX49fvqUanJQhxpx4
This was referenced Sep 1, 2026
Also deletes the hand-rolled IntegrableOn.const_mul' (mathlib's Integrable.const_mul suffices at its sole call site). Claude-Session: https://claude.ai/code/session_01FvNZchX49fvqUanJQhxpx4
norm_shiftedMobiusIntegrand_le becomes the single central bound; the vertical-ray estimate is its a = 0 case and the top edge its a = b = x case (with x² + 1 ≤ 2), so topEdgeBound and its 90-line tendsto proof, along with six other now-redundant declarations, are deleted (−167 lines). All public statements unchanged. Claude-Session: https://claude.ai/code/session_01FvNZchX49fvqUanJQhxpx4
Extracts the standalone Cauchy-product material from thefundamentaltheor3m#317: exact coefficient functions for the q-expansions entering φ₀, and the polynomial growth bound cauchyCoeff_poly with its concrete O(n^11), O(n^10), O(n^9) instances. Includes sigma_bound (σ k n ≤ n^(k+1)), which thefundamentaltheor3m#439 pruned from Eisenstein.lean. Claude-Session: https://claude.ai/code/session_01FvNZchX49fvqUanJQhxpx4
Uses mathlib's ArithmeticFunction.sigma_le_pow_succ instead of a local sigma_bound, and thefundamentaltheor3m#304's definitions verbatim so that PR can import this file and delete its copies. Claude-Session: https://claude.ai/code/session_01FvNZchX49fvqUanJQhxpx4
…-norms-standalone
…hyCoeffBounds The definitions now live in SpherePacking.MagicFunction.a.CauchyCoeffBounds (thefundamentaltheor3m#472); this PR imports them and deletes its copies. Claude-Session: https://claude.ai/code/session_01FvNZchX49fvqUanJQhxpx4
…-norms-standalone
…r/phi-bounds-qseries-integration
cameronfreer
marked this pull request as draft
September 8, 2026 16:27
…' into astra/stack304-cleanup-20260908
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.
The integrability and decay estimates needed for the double-zero contour deformation: unbounded vertical rays, the closing horizontal edge, and the integrability facts used in the deformation.
Where this sits
Depends on: #465 (estimates near the cusp), itself on #304. This branch includes the refreshed prerequisite stack. Review
ContourDeformation.leanas this PR's contribution. After #465 is merged, merge updatedmaininto this branch; the diff will then reduce to this PR's own changes.Merge order: #472 and #477 (either order) → #304 → #465 → #466, refreshing from
mainafter parent merges.Enables: a focused replacement for the double-zero theorem. Together with #425 and #467, this supplies the holomorphicity, contour-integrability, and top-edge-vanishing results needed for that extraction. The new
tendsto_topEdgeIntervalIntegral_zeroconverts the set-integral limit into the interval-integral form of #467's_of_tendsto_tophypothesis. #467 remains an independent prerequisite of the final application; it is not merged into this branch.Supersedes: with #465, this completes the replacement of #296, #297 and #298. This PR takes the contour half of #296 and #297, and all of #298. #298 can be closed: it is written against a
ContourEndpoints.PhiBoundsstructure that no longer exists, and its vanishing lemmas are pointwise consequences of the uniform vanishing proved here.Contents
New
SpherePacking/MagicFunction/a/DoubleZeroes/ContourDeformation.lean.The double-zeroes argument deforms the contour defining
aout to infinity, replacing the bounded rectangle by unbounded vertical rays. This module supplies what the deformation needs, all forr > 2— exactly the range in whichexp(-πrt)beats thee^{2πt}growth ofφ₀(i/t)established in #465.Vertical rays.
verticalIntegrandX x r twith the integrable majorantverticalBound r t(norm_verticalIntegrandX_le),integrableOn_verticalIntegrandXon[1, ∞), and vanishing ast → ∞— pointwise (tendsto_verticalIntegrandX_atTop) and uniformly inx(uniform_vanishing_verticalIntegrandX).Closing horizontal edge.
topEdgeIntegrand r x TwithtopEdgeBound,uniform_vanishing_topEdgeIntegrand,tendsto_topEdgeIntegral_zero, and its interval-integral adaptertendsto_topEdgeIntervalIntegral_zero: the closing edge contributes nothing asT → ∞. The integrand's documentation uses the scalar parameterr, matching the code.The seven integrability goals of thesis Proposition 4.4.6, which fall into two families:
verticalIntegrandX, handled byintegrableOn_Ici_of_eqOn_verticalIntegrandX/integrableOn_Ioi_of_eqOn_neg_I_verticalIntegrandX;-1/(a + it),a = ±1, all going through the unifiedintegrableOn_φ₀_shifted_Möbius.Naming
The public
goal1…goal7names are gone, replaced by contour-specific ones that say which edge they are about:integrableOn_goal1integrableOn_centreRayintegrableOn_goal2integrableOn_leftRay_IoiintegrableOn_goal3integrableOn_rightShiftedRayintegrableOn_goal4integrableOn_rightRay_IoiintegrableOn_goal5integrableOn_leftShiftedRayintegrableOn_goal6integrableOn_leftRay_IciintegrableOn_goal7integrableOn_rightRay_Iciwith the corresponding
goalN_eq_…helpers renamed to match.Dropped
atImInfty_ℂfilter andtendsto_verticalIntegrandX_atImInfty_ℂ— the latter restatedtendsto_verticalIntegrandX_atTopverbatim without ever using the filter, so neither earns its place here. If a genuineatImInftyinterface is wanted it belongs with the Cauchy–Goursat infrastructure.Verification
Full
lake buildis clean, nosorrys in either new file.