Head version
v4.32.0
afafc42a5326d770d0f853f060b2f63947c13f0f
- Toolchain
- leanprover/lean4:v4.32.0
- Revision date
- 16 Jul 2026
- Dependencies
- 11
- Versions
- 21
All packages
YaelDillies/APAP
APAP
Formalisation of the Kelley-Meka bound on Roth numbers
Therefore indexed 68 complete source declarations from the exact package revision. Individual authorship and independent verification remain unset.
mathcombinatoricsadditive-combinatoricsfourier-analysis
External build observation
Exact head commit and toolchain
Reservoir recorded build status passed and test status not observed for commit afafc42a5326 with leanprover/lean4:v4.32.0 on 20 Jul 2026. Therefore did not run this build.
Pin this source in lakefile.lean
require APAP from git "https://github.com/YaelDillies/apap.git" @ "afafc42a5326d770d0f853f060b2f63947c13f0f"
Source declarations
68 indexed proofs
Showing 1 to 20 of 68 declarations.
lemma
curlog_mul_le
Open the record for the exact Lean statement and complete source.
APAP.FiniteField · APAP/FiniteField.lean:80
lemma
global_dichotomy
Open the record for the exact Lean statement and complete source.
APAP.FiniteField · APAP/FiniteField.lean:121
lemma
ap_in_ff
Open the record for the exact Lean statement and complete source.
APAP.FiniteField · APAP/FiniteField.lean:172
lemma
di_in_ff
Open the record for the exact Lean statement and complete source.
APAP.FiniteField · APAP/FiniteField.lean:333
theorem
ff
Open the record for the exact Lean statement and complete source.
APAP.FiniteField · APAP/FiniteField.lean:512
lemma
AddChar.expect_iInf_ker_eq_zero_of_not_mem_closure
Open the record for the exact Lean statement and complete source.
APAP.Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality · APAP/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean:53
lemma
my_markov
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:68
lemma
my_other_markov
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:80
lemma
lemma28_end
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:110
lemma
lemma28_part_one
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:139
lemma
big_shifts_step2
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:154
lemma
AlmostPeriodicity.lemma28_markov
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:243
lemma
AlmostPeriodicity.lemma28_part_two
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:260
lemma
AlmostPeriodicity.lemma28
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:281
lemma
AlmostPeriodicity.just_the_triangle_inequality
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:319
lemma
AlmostPeriodicity.T_bound
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:355
lemma
AlmostPeriodicity.almost_periodicity
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:388
theorem
AlmostPeriodicity.linfty_almost_periodicity
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:424
theorem
AlmostPeriodicity.linfty_almost_periodicity_boosted
Open the record for the exact Lean statement and complete source.
APAP.Physics.AlmostPeriodicity · APAP/Physics/AlmostPeriodicity.lean:495
lemma
drc
Open the record for the exact Lean statement and complete source.
APAP.Physics.DRC · APAP/Physics/DRC.lean:97
Static source extraction only. Package code was not executed. Every result keeps its complete declaration, exact file and line range, commit, toolchain, license file, and content hash.