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 21 to 40 of 68 declarations.
lemma
sifting_cor
Special case of sifting when B₁ = B₂ = univ.
APAP.Physics.DRC · APAP/Physics/DRC.lean:267
lemma
pow_inner_nonneg'
Note that we do the physical proof in order to avoid the Fourier transform.
APAP.Physics.Unbalancing · APAP/Physics/Unbalancing.lean:27
lemma
unbalancing'
The unbalancing step. Note that we do the physical proof in order to avoid the Fourier transform.
APAP.Physics.Unbalancing · APAP/Physics/Unbalancing.lean:205
lemma
BohrSet.mem_arcSet_iff_nnnorm_width
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.Bohr.Arc · APAP/Prereqs/Bohr/Arc.lean:21
lemma
BohrSet.chordSet_subset_smul_arcSet
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.Bohr.Arc · APAP/Prereqs/Bohr/Arc.lean:48
lemma
BohrSet.ext_width
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.Bohr.Basic · APAP/Prereqs/Bohr/Basic.lean:67
lemma
BohrSet.mem_chordSet_iff_nnnorm_width
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.Bohr.Basic · APAP/Prereqs/Bohr/Basic.lean:99
lemma
BohrSet.le_iff_width
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.Bohr.Basic · APAP/Prereqs/Bohr/Basic.lean:168
lemma
BohrSet.eq_zero_of_ewidth_eq_zero
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.Bohr.Basic · APAP/Prereqs/Bohr/Basic.lean:303
lemma
BohrSet.add_subset_of_ewidth
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.Bohr.Basic · APAP/Prereqs/Bohr/Basic.lean:338
lemma
AddDissociated.boringEnergy_le
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.Chang · APAP/Prereqs/Chang.lean:67
lemma
general_hoelder
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.Chang · APAP/Prereqs/Chang.lean:98
lemma
chang
Chang's lemma.
APAP.Prereqs.Chang · APAP/Prereqs/Chang.lean:177
lemma
wInner_one_dddconv
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.Convolution.Norm · APAP/Prereqs/Convolution/Norm.lean:37
lemma
dLpNorm_ddconv_le
A special case of Young's convolution inequality.
APAP.Prereqs.Convolution.Norm · APAP/Prereqs/Convolution/Norm.lean:81
lemma
ThreeAPFree.wInner_one_mu_ddconv_mu_mu_two_smul_mu
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.Convolution.ThreeAP · APAP/Prereqs/Convolution/ThreeAP.lean:20
lemma
cLpNorm_dft_indicator_one_pow
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.Energy · APAP/Prereqs/Energy.lean:53
lemma
wInner_one_cft
Parseval-Plancherel identity for the discrete Fourier transform.
APAP.Prereqs.FourierTransform.Compact · APAP/Prereqs/FourierTransform/Compact.lean:50
lemma
cLpNorm_conv_le_cLpNorm_dconv
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.FourierTransform.Convolution · APAP/Prereqs/FourierTransform/Convolution.lean:18
lemma
dLpNorm_ddconv_le_dLpNorm_dddconv
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.FourierTransform.Convolution · APAP/Prereqs/FourierTransform/Convolution.lean:46
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.