PFR/ImprovedPFR.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

18 declarations, 0 contain sorry, 0 declared as axioms

Improved PFR

An improvement to PFR that lowers the exponent from 12 to 11.

The entropy form (entropic_PFR_conjecture_improv) gives $d[X_1^0; U_H] + d[X_2^0; U_H] \le 10 d[X_1^0; X_2^0]$. Combining with the Ruzsa triangle inequality, each summand is at most $\frac{11}{2} d[X_1^0; X_2^0]$.

Imports (1)
Imported by 3 files
  1. lemma gen_ineq_aux1 line 40 source

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasurableAdd₂, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LE.le, Real and 9 more

    Proof uses: Measurable.add, Eq, ProbabilityTheory.condMutualInfo, sum_of_rdist_eq_char_2, ProbabilityTheory.iIndepFun.reindex_four_cadb, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt, Nat.le_refl, List.nil, eq_of_heq and 111 more

    142 instances, coercions and auxiliary constants left out.

    Tactic trace: 32 steps

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

  2. lemma gen_ineq_aux2 line 76 source

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasurableAdd₂, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LE.le, Real and 10 more

    Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, Measurable.add, ProbabilityTheory.IndepFun, ProbabilityTheory.iIndepFun.indepFun_prodMk_prodMk, List, List.Mem, List.finRange, HEq, Membership.mem, Finset, Fintype.elems, Fintype.complete, List.cons, List.Mem.head, Fin.mk, Nat.le_of_lt and 203 more

    198 instances, coercions and auxiliary constants left out.

    Tactic trace: 127 steps

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

  3. lemma gen_ineq_00 Let Z₁, Z₂, Z₃, Z₄ be independent G-valued random variables, and let Y be another G-valued random variable line 203 source

    Source documentation

    Let Z₁, Z₂, Z₃, Z₄ be independent G-valued random variables, and let Y be another G-valued random variable. Set S := Z₁ + Z₂ + Z₃ + Z₄. Then d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Sum⟩] - d[Y # Z₁] ≤ (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4 + (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4 + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8.

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasurableAdd₂, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LE.le, Real and 11 more

    Proof uses: gen_ineq_aux1, gen_ineq_aux2, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, congrArg, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, Ring, Int.negOfNat, Mathlib.Meta.NormNum.instAddMonoidWithOne, Mathlib.Tactic.Ring.Common.sub_congr, Mathlib.Tactic.Ring.Common.mul_congr and 65 more

    120 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

    lemma gen_ineq_00 : d[Y # Z₁ + Z₂ | ⟨Z₁ + Z₃, Sum⟩] - d[Y # Z₁] ≤
    (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4
    + (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4
    + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8 := by
…
  4. lemma gen_ineq_01 Other version of gen_ineq_00, in which we switch to the complement in the second term line 213 source

    Source documentation

    Other version of gen_ineq_00, in which we switch to the complement in the second term.

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasurableAdd₂, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LE.le, Real and 11 more

    Proof uses: Eq.mpr, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, HSub, Equiv, Equiv.mk, Prod.mk, Prod.snd, Prod.fst, Neg.neg, of_eq_true, Eq.trans, True, congrFun' and 19 more

    84 instances, coercions and auxiliary constants left out.

    Tactic trace: 12 steps

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

    lemma gen_ineq_01 : d[Y # Z₁ + Z₂ | ⟨Z₂ + Z₄, Sum⟩] - d[Y # Z₁] ≤
    (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4
    + (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4
    + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8 := by
…
  5. lemma gen_ineq_10 Other version of gen_ineq_00, in which we switch to the complement in the first term line 230 source

    Source documentation

    Other version of gen_ineq_00, in which we switch to the complement in the first term.

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasurableAdd₂, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LE.le, Real and 11 more

    Proof uses: Eq.mpr, eq_of_heq, LE, Eq, HEq, Eq.refl, HEq.refl, Eq.symm, outParam, HSub, Measurable.add, Equiv, Equiv.prodComm, Function.comp, funext, Prod.ext, Prod.fst, Prod.snd, id, congrArg and 28 more

    77 instances, coercions and auxiliary constants left out.

    Tactic trace: 28 steps

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

    lemma gen_ineq_10 : d[Y # Z₃ + Z₄ | ⟨Z₁ + Z₃, Sum⟩] - d[Y # Z₁] ≤
    (d[Z₁ # Z₂] + 2 * d[Z₁ # Z₃] + d[Z₂ # Z₄]) / 4
    + (d[Z₁ | Z₁ + Z₃ # Z₂ | Z₂ + Z₄] - d[Z₁ | Z₁ + Z₂ # Z₃ | Z₃ + Z₄]) / 4
    + (H[Z₁ + Z₂] - H[Z₃ + Z₄] + H[Z₂] - H[Z₃] + H[Z₂ | Z₂ + Z₄] - H[Z₁ | Z₁ + Z₃]) / 8 := by
…
  6. lemma construct_good_prelim' Documented declaration: construct_good_prelim' line 327 source

    Source documentation

    For any $T_1, T_2, T_3$ adding up to $0$, then $k$ is at most $$ \delta + \eta (d[X^0_1;T_1|T_3]-d[X^0_1;X_1]) + \eta (d[X^0_2;T_2|T_3]-d[X^0_2;X_2])$$ where $\delta = I[T₁ : T₂ ; μ] + I[T₂ : T₃ ; μ] + I[T₃ : T₁ ; μ]$.

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.MeasureSpace, refPackage, TauMinimizes, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Eq, HAdd.hAdd, Measurable, LE.le, Real, rdist, ProbabilityTheory.mutualInfo and 6 more

    Proof uses: MeasureTheory.integral, MeasureTheory.Measure.map, ProbabilityTheory.cond, Set.preimage, Singleton.singleton, Set, Trans.trans, of_eq_true, Eq.trans, True, congrArg, Neg.neg, congrFun', zero_sub, ZModModule.neg_eq_self, eq_self, Eq.mpr, id, add_sub_cancel_right, Eq.refl and 116 more

    175 instances, coercions and auxiliary constants left out.

    Tactic trace: 40 steps

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

    lemma construct_good_prelim' : k ≤ δ + p.η * c[T₁ | T₃ # T₂ | T₃] := by
…
  7. lemma construct_good_improved' In fact $k$ is at most $$ \delta + \frac{\eta}{6} \sum_{i=1}^2 \sum_{1 \leq j,l \leq 3; j \neq l} (d[X^0_i;T_j|T_l] - d[X^0_i; X_i]).$$ line 380 source

    Source documentation

    In fact $k$ is at most $$ \delta + \frac{\eta}{6} \sum_{i=1}^2 \sum_{1 \leq j,l \leq 3; j \neq l} (d[X^0_i;T_j|T_l] - d[X^0_i; X_i]).$$

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.MeasureSpace, refPackage, TauMinimizes, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Eq, HAdd.hAdd, Measurable, LE.le, Real, rdist, ProbabilityTheory.mutualInfo and 7 more

    Proof uses: ProbabilityTheory.mutualInfo_comm, construct_good_prelim', Eq.mpr, id, congrArg, Eq.symm, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo, Mathlib.Tactic.Ring.of_eq, Mathlib.Tactic.Ring.Common.add_congr, HPow.hPow, Nat.rawCast, Int.rawCast, Ring and 73 more

    135 instances, coercions and auxiliary constants left out.

    Tactic trace: 26 steps

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

    lemma construct_good_improved' :
    k ≤ δ + (p.η / 6) *
     ((d[p.X₀₁ # T₁ | T₂] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₁ | T₃] - d[p.X₀₁ # X₁])
    + (d[p.X₀₁ # T₂ | T₁] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₂ | T₃] - d[p.X₀₁ # X₁])
    + (d[p.X₀₁ # T₃ | T₁] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # T₃ | T₂] - d[p.X₀₁ # X₁])
    + (d[p.X₀₂ # T₁ | T₂] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₁ | T₃] - d[p.X₀₂ # X₂])
    + (d[p.X₀₂ # T₂ | T₁] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₂ | T₃] - d[p.X₀₂ # X₂])
    + (d[p.X₀₂ # T₃ | T₁] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # T₃ | T₂] - d[p.X₀₂ # X₂])) := by
…
  8. lemma construct_good_improved'' Rephrase construct_good_improved' with an explicit probability measure, as we will apply it to (varying) conditional measures line 410 source

    Source documentation

    Rephrase construct_good_improved' with an explicit probability measure, as we will apply it to (varying) conditional measures.

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.MeasureSpace, refPackage, TauMinimizes, MeasureTheory.Measure, MeasureTheory.IsProbabilityMeasure, Eq, HAdd.hAdd, Measurable, LE.le, Real, rdist, MeasureTheory.MeasureSpace.volume and 8 more

    Proof uses: MeasureTheory.MeasureSpace.mk, construct_good_improved'

    51 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

    lemma construct_good_improved'' {Ω' : Type*} [MeasurableSpace Ω'] (μ : Measure Ω')
    [IsProbabilityMeasure μ] {T₁ T₂ T₃ : Ω' → G}
    (hT : T₁ + T₂ + T₃ = 0) (hT₁ : Measurable T₁) (hT₂ : Measurable T₂) (hT₃ : Measurable T₃) :
    k ≤ I[T₁ : T₂ ; μ] + I[T₂ : T₃ ; μ] + I[T₃ : T₁ ; μ] + (p.η / 6) *
    ((d[p.X₀₁ ; ℙ # T₁ | T₂ ; μ] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ ; ℙ # T₁ | T₃ ; μ] - d[p.X₀₁ # X₁])
      + (d[p.X₀₁ ; ℙ # T₂ | T₁ ; μ] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ ; ℙ # T₂ | T₃ ; μ] - d[p.X₀₁ # X₁])
      + (d[p.X₀₁ ; ℙ # T₃ | T₁ ; μ] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ ; ℙ # T₃ | T₂ ; μ] - d[p.X₀₁ # X₁])
      + (d[p.X₀₂ ; ℙ # T₁ | T₂ ; μ] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ ; ℙ # T₁ | T₃ ; μ] - d[p.X₀₂ # X₂])
      + (d[p.X₀₂ ; ℙ # T₂ | T₁ ; μ] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ ; ℙ # T₂ | T₃ ; μ] - d[p.X₀₂ # X₂])
      + (d[p.X₀₂ ; ℙ # T₃ | T₁ ; μ] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ ; ℙ # T₃ | T₂ ; μ] - d[p.X₀₂ # X₂]))
    := by
…
  9. lemma averaged_construct_good Documented declaration: averaged_construct_good line 432 source

    Source documentation

    $k$ is at most $$ \leq I(U : V \, | \, S) + I(V : W \, | \,S) + I(W : U \, | \, S) + \frac{\eta}{6} \sum_{i=1}^2 \sum_{A,B \in \{U,V,W\}: A \neq B} (d[X^0_i;A|B,S] - d[X^0_i; X_i]).$$

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.MeasureSpace, refPackage, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, Measurable, TauMinimizes, LE.le, Real, rdist, HAdd.hAdd, ProbabilityTheory.condMutualInfo, HMul.hMul and 8 more

    Proof uses: Fintype, Nonempty, Eq, nonempty_fintype, Nonempty.intro, Measurable.add, sum_uvw_eq_zero, Finset.sum, Finset.univ, MeasureTheory.Measure.real, Set.preimage, Singleton.singleton, Set, Eq.mpr, id, congrArg, Eq.symm, Finset.sum_mul, Finset, Membership.mem and 115 more

    167 instances, coercions and auxiliary constants left out.

    Tactic trace: 29 steps

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

    lemma averaged_construct_good :
    k ≤ (I[U : V | S] + I[V : W | S] + I[W : U | S]) + p.η / 6 *
      (((d[p.X₀₁ # U | ⟨V, S⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # U | ⟨W, S⟩] - d[p.X₀₁ # X₁])
      + (d[p.X₀₁ # V | ⟨U, S⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # V | ⟨W, S⟩] - d[p.X₀₁ # X₁])
      + (d[p.X₀₁ # W | ⟨U, S⟩] - d[p.X₀₁ # X₁]) + (d[p.X₀₁ # W | ⟨V, S⟩] - d[p.X₀₁ # X₁]))
      + ((d[p.X₀₂ # U | ⟨V, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # U | ⟨W, S⟩] - d[p.X₀₂ # X₂])
      + (d[p.X₀₂ # V | ⟨U, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # V | ⟨W, S⟩] - d[p.X₀₂ # X₂])
      + (d[p.X₀₂ # W | ⟨U, S⟩] - d[p.X₀₂ # X₂]) + (d[p.X₀₂ # W | ⟨V, S⟩] - d[p.X₀₂ # X₂])))
    := by
…
  10. lemma dist_diff_bound_1 line 470 source

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, refPackage, Measurable, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LE.le and 12 more

    Proof uses: condRuzsaDist, gen_ineq_01, refPackage.hmeas1, ProbabilityTheory.iIndepFun.reindex_four_abcd, gen_ineq_00, ProbabilityTheory.iIndepFun.reindex_four_abdc, gen_ineq_10, ProbabilityTheory.iIndepFun.reindex_four_acbd, ProbabilityTheory.iIndepFun.reindex_four_acdb, ProbabilityTheory.iIndepFun.reindex_four_adbc, ProbabilityTheory.iIndepFun.reindex_four_adcb, Eq, ProbabilityTheory.IdentDistrib.rdist_congr_right, Measurable.aemeasurable, ProbabilityTheory.IdentDistrib.symm, rdist_symm, ProbabilityTheory.IdentDistrib.rdist_congr, ProbabilityTheory.IdentDistrib.rdist_congr_left, ProbabilityTheory.IdentDistrib.entropy_congr, ProbabilityTheory.IdentDistrib.prodMk and 120 more

    162 instances, coercions and auxiliary constants left out.

    Tactic trace: 93 steps

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

  11. lemma dist_diff_bound_2 line 563 source

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, refPackage, Measurable, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, LE.le and 12 more

    Proof uses: condRuzsaDist, gen_ineq_01, refPackage.hmeas2, ProbabilityTheory.iIndepFun.reindex_four_bacd, gen_ineq_00, ProbabilityTheory.iIndepFun.reindex_four_badc, gen_ineq_10, ProbabilityTheory.iIndepFun.reindex_four_bcad, ProbabilityTheory.iIndepFun.reindex_four_bcda, ProbabilityTheory.iIndepFun.reindex_four_bdac, ProbabilityTheory.iIndepFun.reindex_four_bdca, Eq, rdist_symm, ProbabilityTheory.IdentDistrib.rdist_congr_right, Measurable.aemeasurable, ProbabilityTheory.IdentDistrib.symm, Eq.mpr, id, congrArg, ProbabilityTheory.IdentDistrib.rdist_congr_left and 120 more

    162 instances, coercions and auxiliary constants left out.

    Tactic trace: 99 steps

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

  12. lemma averaged_final line 667 source

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, refPackage, Measurable, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, TauMinimizes and 9 more

    Proof uses: LE.le.trans, condRuzsaDist', Prod, refPackage.X₀₁, prod, refPackage.X₀₂, averaged_construct_good, LT.lt.le, refPackage.hη, sum_condMutual_le, ProbabilityTheory.iIndepFun.reindex_four_abdc, id, add_le_add, mul_le_mul_of_nonneg_left, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, inferInstance, AddMonoidWithOne and 82 more

    131 instances, coercions and auxiliary constants left out.

    Tactic trace: 5 steps

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

  13. theorem tau_strictly_decreases_aux' Suppose $0 < \eta < 1/8$ line 681 source

    Source documentation

    Suppose $0 < \eta < 1/8$. Let $X_1, X_2$ be tau-minimizers. Then $d[X_1;X_2] = 0$. The proof of this lemma uses copies X₁', X₂' already in the context. For a version that does not assume these are given and constructs them instead, use tau_strictly_decreases'.

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, refPackage, Measurable, ProbabilityTheory.IdentDistrib, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, TauMinimizes and 6 more

    Proof uses: refPackage.hη, LE.le, Trans.trans, HSub.hSub, HDiv.hDiv, ProbabilityTheory.condMutualInfo, HAdd.hAdd, averaged_final, add_le_add, le_refl, mul_le_mul_of_nonneg_left, second_estimate_aux, Prod, ProbabilityTheory.iIndepFun.reindex_four_abdc, le_of_lt, Mathlib.Meta.Positivity.pos_of_isNat, Mathlib.Meta.NormNum.isNat_ofNat, Eq.refl, Mathlib.Meta.NormNum.instAtLeastTwo, Bool and 112 more

    157 instances, coercions and auxiliary constants left out.

    Tactic trace: 14 steps

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

    theorem tau_strictly_decreases_aux' (hp : 8 * p.η < 1) : d[X₁ # X₂] = 0 := by
…
  14. theorem tau_strictly_decreases' line 702 source

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

    Statement uses: AddCommGroup, Finite, MeasurableSpace, MeasurableSingletonClass, Module, ZMod, OfNat.ofNat, Nat, MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, refPackage, Measurable, TauMinimizes, LT.lt, Real, HMul.hMul, refPackage.η, Eq, rdist

    Proof uses: Exists, MeasureTheory.Measure, And, ProbabilityTheory.iIndepFun, Fin, Nat.succ, Matrix.vecCons, Matrix.vecEmpty, ProbabilityTheory.IdentDistrib, ProbabilityTheory.independent_copies4_nondep, Eq.mpr, id, congrArg, Eq.symm, ProbabilityTheory.IdentDistrib.rdist_congr, MeasureTheory.MeasureSpace.mk, tau_strictly_decreases_aux', ProbabilityTheory.IdentDistrib.trans, ProbabilityTheory.IdentDistrib.symm, ProbabilityTheory.iIndepFun.reindex_four_abdc and 3 more

    35 instances, coercions and auxiliary constants left out.

    Tactic trace: 6 steps

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

  15. lemma tau_minimizer_exists_rdist_eq_zero For p.η ≤ 1/8, there exist τ-minimizers X₁, X₂ at zero Rusza distance line 732 source

    Source documentation

    For p.η ≤ 1/8, there exist τ-minimizers X₁, X₂ at zero Rusza distance. For p.η < 1/8, all minimizers are fine, by tau_strictly_decreases'. For p.η = 1/8, we use a limit of minimizers for η < 1/8, which exists by compactness.

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

    Statement uses: MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Finite, MeasurableSpace, MeasurableSingletonClass, refPackage, Exists, And, Measurable, TauMinimizes, Eq, Real, rdist

    Proof uses: StrictMono, Membership.mem, Set, Set.Ioo, refPackage.η, Filter.Tendsto, Filter.atTop, nhds, exists_seq_strictMono_tendsto', refPackage.hη, refPackage.mk, refPackage.X₀₁, refPackage.X₀₂, refPackage.hmeas1, refPackage.hmeas2, And.left, LT.lt, le_of_not_gt, HMul.hMul, Mathlib.Tactic.Linarith.lt_irrefl and 119 more

    155 instances, coercions and auxiliary constants left out.

    Tactic trace: 50 steps

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

    lemma tau_minimizer_exists_rdist_eq_zero :
    ∃ (Ω : Type uG) (_ : MeasureSpace Ω) (X₁ : Ω → G) (X₂ : Ω → G),
      Measurable X₁ ∧ Measurable X₂ ∧ IsProbabilityMeasure (ℙ : Measure Ω) ∧ TauMinimizes p X₁ X₂
      ∧ d[X₁ # X₂] = 0 := by
…

    Mentions: TauMinimizes

  16. theorem entropic_PFR_conjecture_improv Entropic PFR, improved constants (10 and 11/2) line 813 source

    Source documentation

    entropic_PFR_conjecture_improv: For two $G$-valued random variables $X_1^0, X_2^0$, there is some subgroup $H \leq G$ such that $d[X_1^0;U_H] + d[X_2^0;U_H] \le 10 d[X_1^0;X_2^0]$, and both $d[X_1^0; U_H]$ and $d[X_2^0; U_H]$ are at most $\frac{11}2 d[X_1^0;X_2^0]$.

    L4DEL explanation

    The same entropic statement with eta = 1/8, giving sum of distances at most 10 d and each distance at most 11/2 d.

    1. Take a tau-minimizing pair whose Ruzsa distance is already zero (tau_minimizer_exists_rdist_eq_zero). Its proof uses the sharper estimate tau_strictly_decreases' valid for 8 * eta < 1, plus a limiting argument for eta = 1/8.
    2. As before, get a subgroup H and uniform U from zero Ruzsa distance.
    3. Minimality of tau against the swapped pair and two uses of the triangle inequality give the 10 bound on the sum and the 11/2 bound on each distance.

    Prerequisites: tau_minimizer_exists_rdist_eq_zero, rdist_triangle, exists_isUniform_of_rdist_eq_zero

    See also: entropic_PFR_conjecture

    Sources and attribution: Pinned Lean source (ce7ac95e620a)

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

    Statement uses: MeasureTheory.MeasureSpace, MeasureTheory.IsProbabilityMeasure, MeasureTheory.MeasureSpace.volume, AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Finite, MeasurableSpace, MeasurableSingletonClass, refPackage, Eq, Real, refPackage.η, HDiv.hDiv, Exists, Submodule, And, Measurable and 7 more

    Proof uses: TauMinimizes, tau_minimizer_exists_rdist_eq_zero, AddSubgroup, exists_isUniform_of_rdist_eq_zero, Prod, rdist_symm, tau, is_tau_min, refPackage.hmeas2, refPackage.hmeas1, rdist_triangle, le_of_not_gt, LT.lt, Mathlib.Tactic.Linarith.lt_irrefl, Eq.mp, Neg.neg, HSub.hSub, inferInstance, AddMonoidWithOne, Mathlib.Meta.NormNum.instAtLeastTwo and 92 more

    134 instances, coercions and auxiliary constants left out.

    Tactic trace: 16 steps

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

    theorem entropic_PFR_conjecture_improv (hpη : p.η = 1 / 8) :
    ∃ (H : Submodule (ZMod 2) G) (Ω : Type uG) (mΩ : MeasureSpace Ω) (U : Ω → G),
    IsProbabilityMeasure (ℙ : Measure Ω) ∧ Measurable U ∧
    IsUniform H U ∧ d[p.X₀₁ # U] + d[p.X₀₂ # U] ≤ 10 * d[p.X₀₁ # p.X₀₂] ∧
      d[p.X₀₁ # U] ≤ 11/2 * d[p.X₀₁ # p.X₀₂] ∧
      d[p.X₀₂ # U] ≤ 11/2 * d[p.X₀₁ # p.X₀₂] := by
…
  17. lemma PFR_conjecture_improv_aux Documented declaration: PFR_conjecture_improv_aux line 847 source

    Source documentation

    Auxiliary statement towards the polynomial Freiman-Ruzsa (PFR) conjecture: if $A$ is a subset of an elementary abelian 2-group of doubling constant at most $K$, then there exists a subgroup $H$ such that $A$ can be covered by at most $K^6 |A|^{1/2} / |H|^{1/2}$ cosets of $H$, and $H$ has the same cardinality as $A$ up to a multiplicative factor $K^10$.

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

    Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Finite, Set, Real, Set.Nonempty, LE.le, Nat.card, HAdd.hAdd, Set.add, HMul.hMul, Set.ncard, Exists, Submodule, And, HPow.hPow, HDiv.hDiv and 1 more

    Proof uses: inferInstance, Membership.mem, MeasurableSpace, Top.top, MeasurableSingletonClass, MeasurableSingletonClass.mk, trivial, LT.lt, PFR_conjecture_pos_aux', Set.toFinite, Finset, Set.Finite.toFinset, Finset.Nonempty, Eq.mpr, id, Eq, congrArg, funext, Set.Finite.coe_toFinset, MeasureTheory.MeasureSpace and 224 more

    225 instances, coercions and auxiliary constants left out.

    Tactic trace: 91 steps

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

    lemma PFR_conjecture_improv_aux (h₀A : A.Nonempty) (hA : Nat.card (A + A) ≤ K * A.ncard) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G),
      Nat.card c ≤ K ^ 6 * A.ncard ^ (1/2) * (H : Set G).ncard ^ (-1/2) ∧
      (H : Set G).ncard ≤ K ^ 10 * A.ncard ∧
      A.ncard ≤ K ^ 10 * (H : Set G).ncard ∧ A ⊆ c + H := by
…
  18. theorem PFR_conjecture_improv PFR with exponent 11 line 953 source

    Source documentation

    The polynomial Freiman-Ruzsa (PFR) conjecture: if $A$ is a subset of an elementary abelian 2-group of doubling constant at most $K$, then $A$ can be covered by at most $2K^{11$} cosets of a subgroup of cardinality at most $|A|$.

    The ambient group need not be finite, in which case H and c are finite.

    L4DEL explanation

    The improved form of PFR: fewer than 2 * K^11 cosets of a subgroup of size at most |A| cover A.

    1. Statement: if A is nonempty and finite in an F2-vector space with |A + A| at most K |A|, there are a subspace H and a finite c with fewer than 2 * K^11 elements, |H| at most |A|, and A inside c + H.
    2. Reduce to finite G by passing to the span of A, as in PFR_conjecture.
    3. Use PFR_conjecture_improv_aux (covering by K^6 |A|^(1/2) |H|^(-1/2) cosets, |H| within K^10 of |A|), which is derived from entropic_PFR_conjecture_improv.
    4. Shrink H to a subspace of size between |A|/2 and |A| when |H| exceeds |A|, and cover H by its cosets.

    Prerequisites: PFR_conjecture_improv_aux, entropic_PFR_conjecture_improv

    See also: PFR_conjecture

    Sources and attribution: Pinned Lean source (ce7ac95e620a)

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

    Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Set, Real, Set.Nonempty, Set.Finite, LE.le, Nat.card, HAdd.hAdd, Set.add, HMul.hMul, Set.ncard, Exists, Submodule, And, LT.lt, HPow.hPow

    Proof uses: Classical.byCases, Finite, PFR_conjecture_pos_aux', Set.toFinite, Membership.mem, HDiv.hDiv, Neg.neg, PFR_conjecture_improv_aux, Nat.card_pos, Iff.mpr, Nat.cast_pos', Or, le_or_gt, Exists.intro, And.intro, Trans.trans, Eq, mul_le_mul_of_nonneg_right, mul_le_mul_of_nonneg_left, Real.rpow_le_rpow and 207 more

    208 instances, coercions and auxiliary constants left out.

    Tactic trace: 63 steps

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

    theorem PFR_conjecture_improv {G : Type*} [AddCommGroup G] [Module (ZMod 2) G]
    {A : Set G} {K : ℝ} (h₀A : A.Nonempty) (Afin : A.Finite)
    (hA : Nat.card (A + A) ≤ K * A.ncard) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G), c.Finite ∧ (H : Set G).Finite ∧
      Nat.card c < 2 * K ^ 11 ∧ (H : Set G).ncard ≤ A.ncard ∧ A ⊆ c + H := by
…