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 41 to 60 of 68 declarations.
lemma
expect_iInf_ker_eq_expect_ite
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.FourierTransform.Discrete · APAP/Prereqs/FourierTransform/Discrete.lean:141
lemma
RCLike.wInner_cWeight_le_cL2Norm_mul_cL2Norm
Cauchy-Schwarz inequality
APAP.Prereqs.Inner.Hoelder.Compact · APAP/Prereqs/Inner/Hoelder/Compact.lean:37
lemma
MeasureTheory.cLpNorm_mul_le
Hölder's inequality, binary case.
APAP.Prereqs.Inner.Hoelder.Compact · APAP/Prereqs/Inner/Hoelder/Compact.lean:60
lemma
MeasureTheory.wInner_cWeight_le_cLpNorm_mul_cLpNorm
Hölder's inequality, binary case.
APAP.Prereqs.Inner.Hoelder.Compact · APAP/Prereqs/Inner/Hoelder/Compact.lean:93
lemma
MeasureTheory.cLpNorm_prod_le
Hölder's inequality, finitary case.
APAP.Prereqs.Inner.Hoelder.Compact · APAP/Prereqs/Inner/Hoelder/Compact.lean:148
lemma
MeasureTheory.wInner_one_le_dLpNorm_mul_dLpNorm
Hölder's inequality, binary case.
APAP.Prereqs.Inner.Hoelder.Discrete · APAP/Prereqs/Inner/Hoelder/Discrete.lean:51
lemma
MeasureTheory.dLpNorm_mul_le
Hölder's inequality, binary case.
APAP.Prereqs.Inner.Hoelder.Discrete · APAP/Prereqs/Inner/Hoelder/Discrete.lean:103
lemma
MeasureTheory.dLpNorm_prod_le
Hölder's inequality, finitary case.
APAP.Prereqs.Inner.Hoelder.Discrete · APAP/Prereqs/Inner/Hoelder/Discrete.lean:112
lemma
MeasureTheory.cLpNorm_pow
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.LpNorm.Compact · APAP/Prereqs/LpNorm/Compact.lean:294
lemma
MeasureTheory.cLpNorm_translate
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.LpNorm.Compact · APAP/Prereqs/LpNorm/Compact.lean:386
lemma
MeasureTheory.cLpNorm_conjneg
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.LpNorm.Compact · APAP/Prereqs/LpNorm/Compact.lean:398
lemma
MeasureTheory.cLpNorm_translate_sum_sub_le
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.LpNorm.Compact · APAP/Prereqs/LpNorm/Compact.lean:410
lemma
MeasureTheory.dLpNorm_translate
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.LpNorm.Discrete.Basic · APAP/Prereqs/LpNorm/Discrete/Basic.lean:88
lemma
MeasureTheory.dLpNorm_conjneg
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.LpNorm.Discrete.Basic · APAP/Prereqs/LpNorm/Discrete/Basic.lean:100
lemma
MeasureTheory.dLpNorm_translate_sum_sub_le
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.LpNorm.Discrete.Basic · APAP/Prereqs/LpNorm/Discrete/Basic.lean:112
lemma
MeasureTheory.dLpNorm_pow
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.LpNorm.Discrete.Defs · APAP/Prereqs/LpNorm/Discrete/Defs.lean:289
lemma
wLpNorm_mono_right
Monotonicity of weighted L^p norms in the exponent, for probability weights.
APAP.Prereqs.LpNorm.Weighted · APAP/Prereqs/LpNorm/Weighted.lean:110
lemma
step_one
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.MarcinkiewiczZygmund · APAP/Prereqs/MarcinkiewiczZygmund.lean:29
lemma
step_one'
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.MarcinkiewiczZygmund · APAP/Prereqs/MarcinkiewiczZygmund.lean:53
lemma
step_two
Open the record for the exact Lean statement and complete source.
APAP.Prereqs.MarcinkiewiczZygmund · APAP/Prereqs/MarcinkiewiczZygmund.lean:99
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.