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

6 declarations, 0 contain sorry, 0 declared as axioms

The approximate homomorphism form of PFR

Here we apply PFR to show that almost homomorphisms f from a 2-group to a 2-group often coincide with a (shifted) actual homomorphisms. Here, approximate is in the sense that f(x+y)=f(x)+f(y) is true for a positive proportion of x,y.

Main result

Imports (6)
Imported by 3 files
  1. theorem approx_hom_pfr Let $G, G'$ be finite abelian $2$-groups line 38 source

    Source documentation

    Let $G, G'$ be finite abelian $2$-groups. Let $f : G \to G'$ be a function, and suppose that there is a proportion of at least $K^{-1}$ pairs $(x,y) \in G^2$ such that $$ f(x+y) = f(x) + f(y).$$ Then there exists a homomorphism $\phi : G \to G'$ and a constant $c \in G'$ such that $f(x) = \phi(x)+c$ for at least $|G| / (2 ^ {144} * K ^ {122})$ values of $x \in G$.

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

    Statement uses: AddCommGroup, Fintype, DecidableEq, Finite, Module, ZMod, OfNat.ofNat, Nat, Real, GT.gt, LE.le, Inv.inv, Finset.dens, Prod, Finset.filter, Eq, HAdd.hAdd, Prod.fst, Prod.snd, Finset.univ and 8 more

    Proof uses: Nonempty, nonempty_fintype, Nonempty.intro, Finset, Set.Finite.toFinset, Set.graphOn, Set.univ, Set.toFinite, Membership.mem, Set, Finset.card, Eq.mpr, Fintype.card, Classical.propDecidable, id, congrArg, Set.Finite.card_toFinset, of_eq_true, Eq.trans, True and 291 more

    311 instances, coercions and auxiliary constants left out.

    Tactic trace: 153 steps

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

    theorem approx_hom_pfr (f : G → G') (K : ℝ) (hK : K > 0)
    (hf : K⁻¹ ≤ Finset.dens {x : G × G | f (x.1 + x.2) = f x.1 + f x.2}) :
    ∃ (φ : G →+ G') (c : G'), Nat.card {x | f x = φ x + c} ≥ Nat.card G / (2 ^ 144 * K ^ 122) := by
…
  2. def dual_iso Non canonical isomorphism between a finite 2-torsion group and its dual into ZMod 2 line 182 source

    Source documentation

    Non canonical isomorphism between a finite 2-torsion group and its dual into ZMod 2.

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

    Statement uses: AddCommGroup, Fintype, Module, ZMod, OfNat.ofNat, Nat, AddEquiv, AddMonoidHom

    Proof uses: Module.Dual, RingHom.id, AddMonoidHom.toZModLinearMapEquiv, LinearEquiv, Nonempty.some, AddEquiv.trans, LinearEquiv.toAddEquiv, AddEquiv.symm

    53 instances, coercions and auxiliary constants left out.

    Tactic trace: 3 steps

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

    noncomputable def dual_iso : G ≃+ (G →+ ZMod 2) := by
…
  3. theorem card_of_dual line 194 source

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

    Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Finite, Eq, Nat.card, AddMonoidHom

    Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Nat.card_congr, Equiv.symm, AddEquiv.toEquiv, dual_iso, Eq.refl

    40 instances, coercions and auxiliary constants left out.

    Tactic trace: 2 steps

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

  4. theorem card_of_dual_constrained line 198 source

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

    Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Finite, Ne, Eq, HMul.hMul, Nat.card, AddMonoidHom, Set.ofPred

    Proof uses: Exists, Module.Basis.ofVectorSpaceIndex, LinearMap.toAddMonoidHom, RingHom.id, Module.Basis.equivFun, Membership.mem, Set, Module.Basis.ofVectorSpace, Finsupp, LinearEquiv, Module.Basis.repr, Mathlib.Tactic.Contrapose.contrapose₂, Eq.mpr, Not, id, implies_congr, Eq.trans, binderNameHint, forall_congr, Eq.refl and 109 more

    160 instances, coercions and auxiliary constants left out.

    Tactic trace: 39 steps

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

  5. theorem card_of_slice line 249 source

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

    Statement uses: AddCommGroup, Module, ZMod, OfNat.ofNat, Nat, Finite, Set, Exists, AddMonoidHom, GE.ge, HMul.hMul, Nat.card, Set.ofPred, And, Membership.mem, Eq, HSub.hSub

    Proof uses: Fintype, Nonempty, nonempty_fintype, Nonempty.intro, Fintype.ofEquiv, AddEquiv.toEquiv, dual_iso, Finset.sum, Finset.univ, Trans.trans, Finset.erase, Classical.propDecidable, Set.toFinset, ite, rfl, of_eq_true, Eq.trans, Finset.card, Finset.filter, True and 80 more

    149 instances, coercions and auxiliary constants left out.

    Tactic trace: 35 steps

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

  6. theorem approx_hom_pfr' line 288 source

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

    Statement uses: AddCommGroup, Fintype, DecidableEq, Finite, Module, ZMod, OfNat.ofNat, Nat, Real, GT.gt, LE.le, Inv.inv, Finset.dens, Prod, Finset.filter, Eq, HAdd.hAdd, Prod.fst, Prod.snd, Finset.univ and 9 more

    Proof uses: approx_hom_pfr, Set, And, Membership.mem, card_of_slice, AddMonoidHom.mk, ZeroHom.mk, HSMul.hSMul, of_eq_true, Eq.trans, True, congrFun', congrArg, map_zero, zero_smul, eq_self, map_add, add_smul, Exists.intro, Eq.mpr and 36 more

    188 instances, coercions and auxiliary constants left out.

    Tactic trace: 25 steps

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