PFR/HundredPercent.lean

GitHub source file

Explanation legend Lean4 Domain Explanation Language (L4DEL)

L4DEL explanations are a separate layer. They do not change the Lean source. Intuition is explanatory prose; numbered items are a reading path; sources link the wording back to evidence.

L4DEL
Lean4 Domain Explanation Language

Credit: The upstream authors and contributors retain credit for the project and mathematics. lean4-explainer only renders their pinned source and adds the separately disclosed explanation layer.

Project sources: Pinned project documentation, Polynomial Freiman-Ruzsa proof paper, arXiv v2

7 declarations, 0 contain sorry, 0 declared as axioms

The 100% version of entropic PFR

Here we show entropic PFR in the case of doubling constant zero.

Main results

Imports (1)
Imported by 3 files
  1. def symmGroup The symmetry group Sym of $X$: the set of all $h ∈ G$ such that $X + h$ has an identical distribution to $X$ line 25 source

    Source documentation

    The symmetry group Sym of $X$: the set of all $h ∈ G$ such that $X + h$ has an identical distribution to $X$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, AddCommGroup, MeasurableAdd₂, Measurable, AddSubgroup

    Proof uses: AddSubgroup.mk, AddSubmonoid.mk, AddSubsemigroup.mk, Set.ofPred, ProbabilityTheory.IdentDistrib, HAdd.hAdd, MeasureTheory.MeasureSpace.volume

    21 instances, coercions and auxiliary constants left out.

    Tactic trace: 23 steps

    Open to load the checked before-and-after goal states.

    def symmGroup (X : Ω → G) (hX : Measurable X) : AddSubgroup G where
…
  2. lemma mem_symmGroup line 51 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, AddCommGroup, MeasurableAdd₂, Measurable, Iff, Membership.mem, AddSubgroup, symmGroup, ProbabilityTheory.IdentDistrib, HAdd.hAdd, MeasureTheory.MeasureSpace.volume

    Proof uses: Iff.rfl

    17 instances, coercions and auxiliary constants left out.

  3. lemma ProbabilityTheory.IdentDistrib.symmGroup_eq line 54 source

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, AddCommGroup, MeasurableAdd₂, Measurable, ProbabilityTheory.IdentDistrib, MeasureTheory.MeasureSpace.volume, Eq, AddSubgroup, symmGroup

    Proof uses: AddSubgroup.ext, HAdd.hAdd, MeasurableAdd.measurable_add_const, Iff.intro, Membership.mem, ProbabilityTheory.IdentDistrib.trans, ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.IdentDistrib.comp

    16 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

    Open to load the checked before-and-after goal states.

  4. lemma sub_mem_symmGroup If $d[X ;X]=0$, and $x,y \in G$ are such that $P[X=x], P[X=y]>0$, then $x-y \in \mathrm{Sym}[X]$ line 65 source

    Source documentation

    If $d[X ;X]=0$, and $x,y \in G$ are such that $P[X=x], P[X=y]>0$, then $x-y \in \mathrm{Sym}[X]$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, AddCommGroup, MeasurableAdd₂, Finite, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Eq, Real, rdist, OfNat.ofNat, Ne, ENNReal, MeasureTheory.Measure, Set, Set.preimage, Singleton.singleton, Membership.mem and 3 more

    Proof uses: Exists, And, ProbabilityTheory.IndepFun, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies_two, Eq.mpr, id, congrArg, ProbabilityTheory.IdentDistrib.symmGroup_eq, ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.condEntropy, ProbabilityTheory.entropy, Trans.trans, ProbabilityTheory.condEntropy_sub_right, ProbabilityTheory.IndepFun.condEntropy_eq_entropy, ProbabilityTheory.IdentDistrib.rdist_congr, Mathlib.Tactic.Linarith.eq_of_not_lt_of_not_gt, Not.intro, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl and 130 more

    145 instances, coercions and auxiliary constants left out.

    Tactic trace: 52 steps

    Open to load the checked before-and-after goal states.

    lemma sub_mem_symmGroup (hX : Measurable X) (hdist : d[X # X] = 0)
    {x y : G} (hx : ℙ (X ⁻¹' {x}) ≠ 0) (hy : ℙ (X ⁻¹' {y}) ≠ 0) : x - y ∈ symmGroup X hX := by
…

    Mentions: symmGroup

  5. lemma isUniform_sub_const_of_rdist_eq_zero If d[X # X] = 0, then X - x₀ is the uniform distribution on the subgroup of G stabilizing the distribution of X, for any x₀ of positive probability line 117 source

    Source documentation

    If d[X # X] = 0, then X - x₀ is the uniform distribution on the subgroup of G stabilizing the distribution of X, for any x₀ of positive probability.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, AddCommGroup, MeasurableAdd₂, Finite, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Eq, Real, rdist, OfNat.ofNat, Ne, ENNReal, MeasureTheory.Measure, Set, Set.preimage, Singleton.singleton, ProbabilityTheory.IsUniform and 3 more

    Proof uses: ProbabilityTheory.IsUniform.mk, HAdd.hAdd, Set.ext, of_eq_true, Iff, Membership.mem, Eq.trans, True, congr, congrArg, iff_self, add_comm, eq_self, Eq.mpr, id, add_zero, congrFun', ProbabilityTheory.IdentDistrib, Neg.neg, Iff.mp and 17 more

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 21 steps

    Open to load the checked before-and-after goal states.

    lemma isUniform_sub_const_of_rdist_eq_zero (hX : Measurable X) (hdist : d[X # X] = 0) {x₀ : G}
    (hx₀ : ℙ (X ⁻¹' {x₀}) ≠ 0) : IsUniform (symmGroup X hX) (fun ω ↦ X ω - x₀) where
…

    Mentions: symmGroup

  6. theorem exists_isUniform_of_rdist_self_eq_zero If $d[X ;X]=0$, then there exists a subgroup $H \leq G$ such that $d[X ;U_H] = 0$ line 142 source

    Source documentation

    If $d[X ;X]=0$, then there exists a subgroup $H \leq G$ such that $d[X ;U_H] = 0$.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, AddCommGroup, MeasurableAdd₂, Finite, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Eq, Real, rdist, OfNat.ofNat, Exists, AddSubgroup, And, ProbabilityTheory.IsUniform

    Proof uses: Ne, ENNReal, MeasureTheory.Measure, Set, Set.preimage, Singleton.singleton, Classical.byContradiction, Not, MeasureTheory.Measure.map, Eq.mpr, id, congrArg, MeasureTheory.Measure.map_apply, MeasurableSet.of_discrete, Eq.mp, Eq.trans, binderNameHint, forall_congr, MeasureTheory.Measure.sum, HSMul.hSMul and 23 more

    64 instances, coercions and auxiliary constants left out.

    Tactic trace: 11 steps

    Open to load the checked before-and-after goal states.

    theorem exists_isUniform_of_rdist_self_eq_zero (hX : Measurable X) (hdist : d[X # X] = 0) :
    ∃ H : AddSubgroup G, ∃ U : Ω → G, Measurable U ∧ IsUniform H U ∧ d[X # U] = 0 := by
…
  7. theorem exists_isUniform_of_rdist_eq_zero If $d[X_1;X_2]=0$, then there exists a subgroup $H \leq G$ such that $d[X_1;U_H] = d[X_2;U_H] = 0$ line 160 source

    Source documentation

    If $d[X_1;X_2]=0$, then there exists a subgroup $H \leq G$ such that $d[X_1;U_H] = d[X_2;U_H] = 0$. Follows from the preceding claim by the triangle inequality.

    standard axioms: Classical.choice, Quot.sound, propext what this means

    Statement uses: MeasureTheory.MeasureSpace, MeasurableSpace, AddCommGroup, MeasurableAdd₂, Finite, MeasurableSingletonClass, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, Eq, Real, rdist, OfNat.ofNat, Exists, AddSubgroup, And, ProbabilityTheory.IsUniform

    Proof uses: le_antisymm, Trans.trans, LE.le, HAdd.hAdd, rdist_triangle, Eq.mpr, id, congrArg, rdist_symm, zero_add, Eq.refl, rdist_nonneg, exists_isUniform_of_rdist_self_eq_zero, Exists.intro, And.intro

    36 instances, coercions and auxiliary constants left out.

    Tactic trace: 9 steps

    Open to load the checked before-and-after goal states.

    theorem exists_isUniform_of_rdist_eq_zero
    {Ω' : Type*} [MeasureSpace Ω'] [IsProbabilityMeasure (ℙ : Measure Ω')] {X' : Ω' → G}
    (hX : Measurable X) (hX' : Measurable X') (hdist : d[X # X'] = 0) :
    ∃ H : AddSubgroup G, ∃ U : Ω → G,
      Measurable U ∧ IsUniform H U ∧ d[X # U] = 0 ∧ d[X' # U] = 0 := by
…