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 201 to 220 of 350 declarations.
lemma
ProbabilityTheory.independent_copies'
Let Xᵢ : Ωᵢ → Sᵢ be random variables for i = 1,...,k.
Then there exist jointly independent random variables Xᵢ' : Ω' → Sᵢ for i=1,...,k
such that each Xᵢ' is a copy of Xᵢ.
PFR.Mathlib.Probability.IdentDistrib · PFR/Mathlib/Probability/IdentDistrib.lean:265
lemma
ProbabilityTheory.independent_copies3_nondep
A version with exactly 3 random variables that have the same codomain. It's unfortunately incredibly painful to prove this from the general case.
PFR.Mathlib.Probability.IdentDistrib · PFR/Mathlib/Probability/IdentDistrib.lean:285
lemma
ProbabilityTheory.independent_copies4_nondep
A version with exactly 4 random variables that have the same codomain. It's unfortunately incredibly painful to prove this from the general case.
PFR.Mathlib.Probability.IdentDistrib · PFR/Mathlib/Probability/IdentDistrib.lean:329
lemma
ProbabilityTheory.iIndepFun.finsetSum
Open the record for the exact Lean statement and complete source.
PFR.Mathlib.Probability.Independence.Basic · PFR/Mathlib/Probability/Independence/Basic.lean:70
lemma
ProbabilityTheory.IndepFun.finsetSum
Open the record for the exact Lean statement and complete source.
PFR.Mathlib.Probability.Independence.Basic · PFR/Mathlib/Probability/Independence/Basic.lean:85
lemma
ProbabilityTheory.iIndepFun.finsets_comp'
A variant of iIndepFun.finsets_comp where we conclude the independence of just two functions rather than an entire family.
PFR.Mathlib.Probability.Independence.Basic · PFR/Mathlib/Probability/Independence/Basic.lean:108
lemma
ProbabilityTheory.IndepFun.comp_right
Composing independent functions with a measurable embedding of conull range gives independent functions.
PFR.Mathlib.Probability.Independence.Basic · PFR/Mathlib/Probability/Independence/Basic.lean:163
lemma
ProbabilityTheory.iIndepFun_iff'
Open the record for the exact Lean statement and complete source.
PFR.Mathlib.Probability.Independence.Basic · PFR/Mathlib/Probability/Independence/Basic.lean:181
lemma
ProbabilityTheory.iIndepFun.pi
If a family of functions (i, j) ↦ f i j is independent, then the family of function tuples
i ↦ (f i j)ⱼ is independent.
PFR.Mathlib.Probability.Independence.Basic · PFR/Mathlib/Probability/Independence/Basic.lean:226
lemma
ProbabilityTheory.iIndepFun.prod
Open the record for the exact Lean statement and complete source.
PFR.Mathlib.Probability.Independence.Basic · PFR/Mathlib/Probability/Independence/Basic.lean:293
theorem
ProbabilityTheory.EventuallyEq.finite_iInter
The new Mathlib tool Finset.eventuallyEq_iInter will supersede this result.
PFR.Mathlib.Probability.Independence.Basic · PFR/Mathlib/Probability/Independence/Basic.lean:311
theorem
ProbabilityTheory.iIndepFun.ae_eq
TODO: a kernel version of this theorem
PFR.Mathlib.Probability.Independence.Basic · PFR/Mathlib/Probability/Independence/Basic.lean:326
lemma
ProbabilityTheory.Kernel.iIndepFun.finsets
If f is a family of mutually independent random variables, (S j)ⱼ are pairwise disjoint
finite index sets, then the tuples formed by f i for i ∈ S j are mutually independent,
when seen as a family indexed by J.
PFR.Mathlib.Probability.Independence.Kernel.IndepFun · PFR/Mathlib/Probability/Independence/Kernel/IndepFun.lean:25
lemma
ProbabilityTheory.Kernel.deleteMiddle_map_prod
Open the record for the exact Lean statement and complete source.
PFR.Mathlib.Probability.Kernel.Composition.Comp · PFR/Mathlib/Probability/Kernel/Composition/Comp.lean:67
lemma
ProbabilityTheory.Kernel.deleteRight_map_prod
Open the record for the exact Lean statement and complete source.
PFR.Mathlib.Probability.Kernel.Composition.Comp · PFR/Mathlib/Probability/Kernel/Composition/Comp.lean:126
lemma
ProbabilityTheory.Kernel.condKernel_compProd_apply'
Open the record for the exact Lean statement and complete source.
PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:59
lemma
ProbabilityTheory.Kernel.disintegration
Open the record for the exact Lean statement and complete source.
PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:82
lemma
ProbabilityTheory.Kernel.condKernel_compProd_ae_eq
Open the record for the exact Lean statement and complete source.
PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:115
lemma
ProbabilityTheory.Kernel.condKernel_map_prodMk_left
Open the record for the exact Lean statement and complete source.
PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:154
lemma
ProbabilityTheory.condKernel_condDistrib_ae_eq
Open the record for the exact Lean statement and complete source.
PFR.Mathlib.Probability.Kernel.Disintegration · PFR/Mathlib/Probability/Kernel/Disintegration.lean:284
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.