Head version
v4.33.0-rc1
a177b2e4abe4b31c8024b9afebe646bf6bb8f91b
- Toolchain
- leanprover/lean4:v4.33.0-rc1
- Revision date
- 16 Jul 2026
- Dependencies
- 11
- Versions
- 23
All packages
teorth/PFR
PFR
Repository for formalization of the Polynomial Freiman Ruzsa conjecture (and related results)
Therefore indexed 350 complete source declarations from the exact package revision. Individual authorship and independent verification remain unset.
mathadditive-combinatoricsinformation-theory
External build observation
Exact head commit and toolchain
Reservoir recorded build status passed and test status not observed for commit a177b2e4abe4 with leanprover/lean4:v4.33.0-rc1 on 20 Jul 2026. Therefore did not run this build.
Pin this source in lakefile.lean
require PFR from git "https://github.com/teorth/pfr.git" @ "a177b2e4abe4b31c8024b9afebe646bf6bb8f91b"
Source declarations
350 indexed proofs
Showing 81 to 100 of 350 declarations.
lemma
ProbabilityTheory.Kernel.rdist_zero_kernel_right
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Kernel.RuzsaDist · PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean:86
lemma
ProbabilityTheory.Kernel.rdist_dirac_zero_right
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Kernel.RuzsaDist · PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean:107
lemma
ProbabilityTheory.Kernel.abs_sub_entropy_le_rdist
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Kernel.RuzsaDist · PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean:149
lemma
ProbabilityTheory.Kernel.ent_of_diff_le
The improved entropic Ruzsa triangle inequality.
PFR.ForMathlib.Entropy.Kernel.RuzsaDist · PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean:176
lemma
ProbabilityTheory.Kernel.rdist_triangle_aux1
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Kernel.RuzsaDist · PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean:279
lemma
ProbabilityTheory.Kernel.rdist_triangle_aux2
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Kernel.RuzsaDist · PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean:310
lemma
ProbabilityTheory.Kernel.rdist_triangle
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Kernel.RuzsaDist · PFR/ForMathlib/Entropy/Kernel/RuzsaDist.lean:350
lemma
ProbabilityTheory.measure_compl_support
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:62
lemma
ProbabilityTheory.integrable_of_finiteSupport
The countability hypothesis can probably be dropped here. Proof is unwieldy and can probably be golfed.
PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:151
theorem
ProbabilityTheory.Measure.ext_iff_singleton_finiteSupport
This generalizes Measure.ext_iff_singleton ∈ MeasureReal
PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:185
lemma
ProbabilityTheory.measureEntropy_le_log_card_of_mem
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:359
lemma
ProbabilityTheory.entropy_of_uniformOn
The entropy of a uniform measure is the log of the cardinality of its support.
PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:385
lemma
ProbabilityTheory.measureEntropy_eq_card_iff_measure_eq
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:406
lemma
ProbabilityTheory.measureEntropy_map_of_injective
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:419
lemma
ProbabilityTheory.measureEntropy_comap
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:444
lemma
ProbabilityTheory.measureEntropy_prod
An ambitious goal would be to replace FiniteSupport with finite entropy.
PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:470
lemma
ProbabilityTheory.measureMutualInfo_of_not_isFiniteMeasure
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:523
lemma
ProbabilityTheory.measureMutualInfo_univ_smul
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:538
lemma
ProbabilityTheory.measureMutualInfo_swap
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.Measure · PFR/ForMathlib/Entropy/Measure.lean:557
lemma
continuous_measureEntropy_probabilityMeasure
Open the record for the exact Lean statement and complete source.
PFR.ForMathlib.Entropy.RuzsaDist · PFR/ForMathlib/Entropy/RuzsaDist.lean:42
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.