Cleanup and golf FG.lean - #410
Draft
seewoo5 wants to merge 81 commits into
Draft
Conversation
- Move F₁ definition earlier in file for better organization - Add F₁_imag_axis_real: F₁ is real on the imaginary axis - Simplify F_functional_equation proof by removing intermediate steps - Simplify G_functional_equation proof using simp only - Fix sign in F_functional_equation': change -36 to +36 per blueprint Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Co-authored-by: Cameron Freer <freer@mit.edu>
Derive the real-valued functional equation for FReal(1/t) from the complex F_functional_equation by computing powers of (I*t) and showing the result is real on the imaginary axis. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
…ents - Add I_zpow_four, I_zpow_mod_four, I_mul_t_pow helper lemmas - Add I_mul_t_pow' which uses match on n % 4 to give concrete results: - n % 4 = 0: t^n - n % 4 = 1: I * t^n - n % 4 = 2: -t^n - n % 4 = 3: -I * t^n - Simplify hz_pow10, hz_pow11, hz_pow12 proofs in F_functional_equation' using I_mul_t_pow' instead of manual norm_num computations Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- F_functional_equation': use ResToImagAxis.I_mul_t_eq for hF_z, hF₁E₄_z, hE₄_z - G_functional_equation': use I_mul_t_pow' for hz_pow10, and ResToImagAxis.I_mul_t_eq for hH₂_z, hH₄_z Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Add sq_mul_FReal_tendsto_zero using Complex.ofReal_cpow - Add mul_F₁E₄_re_tendsto_zero with ring tactic - Add E₄/H₂/H₄_re_resToImagAxis_tendsto lemmas via continuous_re composition - Prove numerator_tendsto_at_infty and denominator_tendsto_at_infty - Prove G_functional_eq_real using ofReal_injective - Add helper lemmas for tendsto conversion from atImInfty to atTop Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Use Complex.ofReal_zpow to convert π power coercions - Reassociate denominator before cancelling s^10 factor - Fix linter warnings (empty lines, long lines) Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
- Simplify tendsto lemmas using direct composition with continuous_re - Remove unused intermediate variables (hG_ne, hmax_pos, hlim, etc.) - Inline have statements where possible - Use calc for cleaner s^10 factoring and cancellation - Remove redundant comments and streamline proofs - Net reduction of ~80 lines Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Use `set h4 := ...; set h2 := ...` to create local abbreviations for repeated Tendsto hypotheses, making the proof more readable. Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Prove that F₁ = E₂*E₄ - E₆ has exponential decay O(exp(-2πy)) at im-infinity using the decomposition F₁ = (E₂-1)*E₄ + (E₄-1) - (E₆-1) where each term decays exponentially. - Add import for EisensteinAsymptotics to access E₂_sub_one_isBigO_exp and ModularFormClass.exp_decay_sub_atImInfty - Use limUnder_eq to show valueAtInfty E₄ = 1 and valueAtInfty E₆ = 1 - Also complete rpow_mul_F₁E₄_resToImagAxis_tendsto_zero using similar approach Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>
Header: remove duplicate import, remove misplaced empty docstring. Golf 13 high-value declarations; file shrinks 1429 → 1332 lines. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Trim docstrings, inline single-use haves, and remove step-by-step proof comments. No behavioral changes; only the two intentional sorries on F_eq_FReal / G_eq_GReal remain. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
seewoo5
requested review from
CBirkbeck,
b-mehta,
pitmonticone,
thefundamentaltheor3m and
viazovska
as code owners
April 26, 2026 17:30
Inline more single-use haves, collapse multi-step calc blocks, and tighten intro patterns. Build is clean except the two intentional sorries on F_eq_FReal / G_eq_GReal. Co-Authored-By: Claude Opus 4.7 <noreply@anthropic.com>
Resolve the FG.lean conflict (40 hunks) in favour of main's side, which is strictly ahead: main already carries this branch's work via #307 (Qlim) and #331 (FG inequalities), plus the Lean v4.31.0 bump (#421), the ResToImagAxis API (#428), the log-derivative keystone extraction (#429) and the linter cleanup (#450). This branch's side was no longer viable on its own: it referenced `tsum_pnat_eq_tsum_succ3` and the old `ModularFormClass.hasSum_qExpansion` / `.exp_decay_sub_atImInfty` names (all gone), proved `Δ_fun_eq_Δ` via local `Delta_E4_E6_eq` machinery instead of mathlib's `discriminant_eq_E₄_cube_sub_E₆_sq`, had regressed `F_eq_FReal`/`G_eq_GReal` to `sorry`, used `L₁₀_holo` without defining it, and kept a local `div_re_of_im_eq_zero` that #428 moved into ResToImagAxis. On top of main's version, re-apply the formatting-only golf from this branch that main lacked (-22 lines): F_eq_nine_DE₄_sq, G_eq, F_aux, MLDE_F, sigma_qexp_deriv_bound_generic, and inlining the hsum_re/htsum_pos intermediates in DE₄_imag_axis_re_pos and negDE₂_imag_axis_re_pos. Main's style is kept where it was better (↦ binders, tendsto_cont lists, extracted H_poly_tendsto_atImInfty, I_mul_npow). Full project builds: 3491 jobs, no errors. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Review feedback (PR #410): - Split all `tac₁; tac₂; tac₃` chains back to one tactic per line (F_eq_nine_DE₄_sq, G_eq, F_aux, MLDE_F) per reviewer preference; short two-tactic idioms the file already used are kept. - The Δ_fun_eq_Δ comment is obsolete: that proof was replaced by the mathlib-based version when merging main. Cleanup (net −211 lines, 1244 → 1033; file is now sorry- and warning-free): - Prove the two placeholder sorries: FReal_Differentiable and GReal_Differentiable via hasDerivAt_resToImagAxis_re. - Replace E₄_sigma_qexp's 58-line manual derivation with mathlib's EisensteinSeries.q_expansion_bernoulli (2 tactics). - New private D_qexp_const_add_smul (termwise differentiation of c₀ + c•Σ aₙqⁿ expansions); DE₄_qexp and negDE₂_qexp become short applications of it. - deriv_FmodGReal: HasDerivAt.div + defeq transport to FmodGReal replaces the EventuallyEq/deriv_div detour; FmodGReal_differentiableOn collapses to a term-mode application of the new differentiability lemmas. - Golf E₂E₄_sub_E₆_div_q_tendsto (37→17), FmodG_rightLimitAt_zero, sigma_qexp_summable_generic (of_norm_bounded + gcongr), sigma_qexp_deriv_bound_generic. - Delete dead declarations: D_diff_qexp, Δ_fun_imag_axis_pos, H_poly_tendsto_atImInfty, D_H₂_div_H₂_tendsto, SerreDer_22_L₁₀_real; drop the SerreDer_22_L₁₀_pos bridge (L₁₀_pos uses the private lemma directly). All verified unused in repo and blueprint. - Style: unify fun binders to ↦, remove step-narration comments from proofs, squeeze all non-terminal bare simps (incl. the disch := fun_prop sites), fix `simp at *` in E₂_sigma_qexp. Blueprint-pinned names (checkdecls) are all unchanged. Full lake build: 3491 jobs, no errors; FG.lean emits no warnings. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Adapt FG.lean to Δ becoming notation for mathlib's ModularForm.discriminant: take main's renamed identifiers (Δ_eq_H₂_H₃_H₄, Δ_imag_axis_pos; Delta_apply and Δ_eq_discriminant are gone) while keeping this branch's cleanup. The Δ_fun_imag_axis_pos lemma main renamed remains deleted here — it is unused on both sides. Full lake build: 3491 jobs, no errors. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com>
Collaborator
Author
|
There are some results on q-expansion of (derivatives of) Eisenstein series, and I think it would be better to move these to e.g. |
seewoo5
added a commit
that referenced
this pull request
Jul 30, 2026
The golf on this branch collapsed several proofs to `ext z; simp ...; ring`. The repo owner pushed back on exactly this shape in the PR #410 review ("I'm not convinced that these triple inlined statements are better than having them on 3 separate lines"), so split the 10 affected sites: 6 in Derivative.lean, 4 in JacobiIdentity.lean. Two-tactic idioms the codebase already uses (`by unfold f; fun_prop`) and `<;>` chains are left as they are. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
seewoo5
marked this pull request as draft
July 30, 2026 03:09
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
2 participants
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.
Will continue when #439 is merged.