Skip to content

Cleanup and golf FG.lean #410

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

Draft
seewoo5 wants to merge 81 commits into
base: main
Choose a base branch
from
Draft

Cleanup and golf FG.lean #410

Changes from all commits
Commits
Show all changes
81 commits
Select commit Hold shift + click to select a range
1954e20
wip: functional equation
seewoo5 Jan 4, 2026
6a0f8df
Merge branch 'main' into Qlim
seewoo5 Jan 18, 2026
11bd5cd
merge main
seewoo5 Jan 21, 2026
e5255d7
F_functional_equation and G_functional_equation
seewoo5 Jan 23, 2026
4edcf96
refactor(FG): Simplify functional equation proofs and add F₁ lemma
seewoo5 Jan 23, 2026
afbb969
remove unnecessary commits
seewoo5 Jan 23, 2026
0ffbd0a
real_part_eq
seewoo5 Jan 23, 2026
812dc4b
Merge branch 'main' into res-imag-real-part
seewoo5 Jan 23, 2026
a90089d
Merge branch 'main' into Qlim
seewoo5 Jan 25, 2026
5e217fb
Update SpherePacking/ModularForms/ResToImagAxis.lean
seewoo5 Jan 25, 2026
0d2eddc
Merge branch 'res-imag-real-part' into Qlim
seewoo5 Jan 25, 2026
40f5647
working proof from claude
seewoo5 Jan 26, 2026
2a5c99e
slightly better proof by claude
seewoo5 Jan 26, 2026
15c7484
Prove F_functional_equation' using F_functional_equation
seewoo5 Jan 26, 2026
831a3ee
slightly better proof by claude
seewoo5 Jan 26, 2026
9582ed3
factor our Hi_S_action'
seewoo5 Jan 27, 2026
7b2c6b2
Add I_mul_t_pow' lemma for computing (I * t)^n with concrete coeffici…
seewoo5 Jan 27, 2026
07ba518
Simplify proofs using I_mul_t_pow' and ResToImagAxis.I_mul_t_eq
seewoo5 Jan 27, 2026
e0df720
I_mul_t_eq
seewoo5 Jan 27, 2026
59b205c
Merge branch 'main' into Qlim
seewoo5 Jan 27, 2026
f2eb094
wip
seewoo5 Jan 27, 2026
8de3faf
lint 100chars
seewoo5 Jan 27, 2026
801a3e1
Merge branch 'main' into res-imag-real-part
seewoo5 Jan 27, 2026
9369eb7
add .Real
seewoo5 Jan 27, 2026
b2ff88a
Merge branch 'res-imag-real-part' into Qlim
seewoo5 Jan 27, 2026
63eabc9
fill in tendsto lemmas for FmodG limit computation
seewoo5 Jan 28, 2026
5f4b61b
Complete proof of hEq in FmodG_rightLimitAt_zero
seewoo5 Jan 28, 2026
e28e9a1
Refactor FmodG_rightLimitAt_zero and related lemmas
seewoo5 Jan 28, 2026
d24b4d2
Use set abbreviations for cleaner Tendsto proofs
seewoo5 Jan 28, 2026
d9a0016
Complete proof of F₁_isBigO_exp_atImInfty
seewoo5 Jan 28, 2026
c3f9e37
Simplify F₁_mul_E₄_isBoundedAtImInfty and move tendsto lemma
seewoo5 Jan 28, 2026
edf4fb7
Merge branch 'main' into Qlim
seewoo5 Jan 28, 2026
0c7b710
Simplify I_mul_t_pow lemma to use natural powers directly
seewoo5 Jan 28, 2026
d9911d3
move more have's
seewoo5 Jan 28, 2026
ce20892
Merge branch 'main' into Qlim
seewoo5 Jan 28, 2026
c63054d
merge & resolve conflicts
seewoo5 Feb 2, 2026
edab399
golf
seewoo5 Feb 2, 2026
dea2ba1
small golf
seewoo5 Feb 3, 2026
4f71cc7
factor out one_div_eq_S_smul
seewoo5 Feb 3, 2026
d08faaf
golf F_functional_equation' and G_functional_equation'
seewoo5 Feb 3, 2026
1ab9007
prove FG_inequality_1 and FG_inequality_2
seewoo5 Feb 3, 2026
fd51cff
update blueprint
seewoo5 Feb 3, 2026
413d926
Apply suggestions from code review
seewoo5 Feb 9, 2026
a8535b6
Merge branch 'Qlim' into FG-ineqs
seewoo5 Feb 9, 2026
a6ac7db
Apply suggestions from code review
seewoo5 Feb 17, 2026
6da3596
merge main
seewoo5 Feb 21, 2026
3575612
golf functional equation and limit proofs in FG
seewoo5 Feb 21, 2026
ab922c0
merge main
seewoo5 Feb 22, 2026
2eee8c7
resolve conflicts
seewoo5 Feb 25, 2026
c5ecf23
Merge branch 'main' into FG-ineqs
seewoo5 Mar 4, 2026
c12dedf
merge main
seewoo5 Mar 6, 2026
c93f6ef
resolve merge conflicts
seewoo5 Mar 9, 2026
8cf229b
Merge branch 'main' into Qlim
seewoo5 Mar 16, 2026
7b632a2
Apply suggestions from code review
seewoo5 Mar 16, 2026
fd175e5
Merge branch 'Qlim' of github.com:thefundamentaltheor3m/Sphere-Packin…
seewoo5 Mar 16, 2026
1df713e
address more comments
seewoo5 Mar 16, 2026
5d4f068
minor
seewoo5 Mar 16, 2026
3e59e6d
Merge branch 'main' into Qlim
seewoo5 Mar 17, 2026
46e2301
more golf
seewoo5 Mar 17, 2026
8e406cd
Merge branch 'main' into Qlim
seewoo5 Mar 17, 2026
93d1d73
weird way
seewoo5 Mar 18, 2026
bd8fcbf
Merge branch 'main' into Qlim
seewoo5 Mar 19, 2026
0eb9147
Merge branch 'Qlim' into Qlim_tendsto
seewoo5 Mar 19, 2026
4e5feb8
denominator_tendsto_at_infty
seewoo5 Mar 19, 2026
e7bd5c8
golf: numerator_tendsto_at_infty
seewoo5 Mar 19, 2026
1fe744f
merge main
seewoo5 Apr 10, 2026
56a1d52
merge main & remove unused theorems
seewoo5 Apr 10, 2026
cd66ada
Merge branch 'main' into FG-ineqs
seewoo5 Apr 21, 2026
1999c5b
Merge branch 'main' into Qlim
seewoo5 Apr 21, 2026
91a64a1
fix imports
seewoo5 Apr 21, 2026
691b5de
Golf and clean up FG.lean
seewoo5 Apr 21, 2026
4dfc099
Merge branch 'main' into Qlim
seewoo5 Apr 23, 2026
1cbaf6a
inline proof & tendsto
seewoo5 Apr 23, 2026
3ed3df4
Merge branch 'main' into FG-ineqs
seewoo5 Apr 26, 2026
b89f072
merge Qlim
seewoo5 Apr 26, 2026
950b32c
remove proofs of F_eq_FReal and G_eq_GReal, which will be added from …
seewoo5 Apr 26, 2026
8fbfbbc
cleanup and golf FG.lean
seewoo5 Apr 26, 2026
b0dfc0f
second cleanup pass on FG.lean
seewoo5 Apr 26, 2026
37427e6
Merge branch 'main' into FG-refactor
seewoo5 Jul 29, 2026
258b9b9
Address review + full cleanup pass on FG.lean
seewoo5 Jul 29, 2026
c3af7b9
Merge origin/main (#438 Delta refactor) into FG-refactor
seewoo5 Jul 30, 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