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.

Research project27 GitHub starsApache-2.021 indexed versionsRepository Full history on Reservoir

mathcombinatoricsadditive-combinatoricsfourier-analysis

Head version

v4.32.0

afafc42a5326d770d0f853f060b2f63947c13f0f

Toolchain: leanprover/lean4:v4.32.0
Revision date: 16 Jul 2026
Dependencies: 11
Versions: 21

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

Package history

Showing 61 to 68 of 68 declarations.

lemma

step_three

Open the record for the exact Lean statement and complete source.

APAP.Prereqs.MarcinkiewiczZygmund · APAP/Prereqs/MarcinkiewiczZygmund.lean:113

lemma

end_step

Open the record for the exact Lean statement and complete source.

APAP.Prereqs.MarcinkiewiczZygmund · APAP/Prereqs/MarcinkiewiczZygmund.lean:164

theorem

Real.marcinkiewicz_zygmund'

The Marcinkiewicz-Zygmund inequality for real-valued functions, with a slightly better constant than Real.marcinkiewicz_zygmund.

APAP.Prereqs.MarcinkiewiczZygmund · APAP/Prereqs/MarcinkiewiczZygmund.lean:192

theorem

Real.marcinkiewicz_zygmund

The Marcinkiewicz-Zygmund inequality for real-valued functions, with a slightly easier to bound constant than Real.marcinkiewicz_zygmund'.

Note that RCLike.marcinkiewicz_zygmund is another version that works for both ℝ and ℂ at the expense of a slightly worse constant.

APAP.Prereqs.MarcinkiewiczZygmund · APAP/Prereqs/MarcinkiewiczZygmund.lean:228

lemma

RCLike.marcinkiewicz_zygmund

The Marcinkiewicz-Zygmund inequality for real- or complex-valued functions.

APAP.Prereqs.MarcinkiewiczZygmund · APAP/Prereqs/MarcinkiewiczZygmund.lean:253

lemma

rudin_exp_ineq

Rudin's inequality, exponential form.

APAP.Prereqs.Rudin · APAP/Prereqs/Rudin.lean:29

lemma

rudin_exp_abs_ineq

Rudin's inequality, exponential form with absolute values.

APAP.Prereqs.Rudin · APAP/Prereqs/Rudin.lean:61

lemma

rudin_ineq

Rudin's inequality, usual form.

APAP.Prereqs.Rudin · APAP/Prereqs/Rudin.lean:100

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.