PFRPalomar/Challenge.lean

GitHub source file

6 declarations, 6 contain sorry, 0 declared as axioms

1. theorem Marton.pfr_conjecture Marton's conjecture in characteristic 2, [GGMT], Theorem 1.2 sorry line 69 source

   Source documentation

   Marton's conjecture in characteristic 2, [GGMT], Theorem 1.2.

   If A is a finite non-empty subset of an abelian group G of exponent 2 — that is, 2 • x = 0 for every x : G, so that G is an 𝔽₂-vector space — and |A + A| ≤ K * |A|, then A is covered by fewer than 2 * K ^ 12 cosets of a subgroup H of G with |H| ≤ |A|.

   The ambient group G is not required to be finite; the covering set c and the subgroup H produced are then finite. This statement is superseded by Marton.pfr_conjecture_nine, and is recorded separately because it is the headline theorem of [GGMT].

   depends on sorry what this means

   Statement uses: AddCommGroup, Eq, HSMul.hSMul, Nat, OfNat.ofNat, Set, Set.Finite, Set.Nonempty, Real, LE.le, Nat.card, HAdd.hAdd, HMul.hMul, Exists, AddSubgroup, And, LT.lt, HPow.hPow, Subtype, Membership.mem

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   76 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: PFRPalomar/Solution.lean:33 (same statement text; different proof or body). Qualify references as Marton.pfr_conjecture@path.

   Tactic trace: 1 steps

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

   theorem pfr_conjecture {G : Type*} [AddCommGroup G] (h2 : ∀ x : G, 2 • x = 0) {A : Set G}
       (hA : A.Finite) (hA₀ : A.Nonempty) {K : ℝ} (hAK : Nat.card (A + A) ≤ K * Nat.card A) :
       ∃ (H : AddSubgroup G) (c : Set G), c.Finite ∧ (H : Set G).Finite ∧
         Nat.card c < 2 * K ^ 12 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by
   …

2. theorem Marton.pfr_conjecture_nine Marton's conjecture in characteristic 2 with exponent 9, [L], main theorem sorry line 84 source

   Source documentation

   Marton's conjecture in characteristic 2 with exponent 9, [L], main theorem.

   If A is a finite non-empty subset of an abelian group G of exponent 2 — that is, 2 • x = 0 for every x : G, so that G is an 𝔽₂-vector space — and |A + A| ≤ K * |A|, then A is covered by fewer than 2 * K ^ 9 cosets of a subgroup H of G with |H| ≤ |A|.

   The ambient group G is not required to be finite; the covering set c and the subgroup H produced are then finite.

   depends on sorry what this means

   Statement uses: AddCommGroup, Eq, HSMul.hSMul, Nat, OfNat.ofNat, Set, Set.Finite, Set.Nonempty, Real, LE.le, Nat.card, HAdd.hAdd, HMul.hMul, Exists, AddSubgroup, And, LT.lt, HPow.hPow, Subtype, Membership.mem

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   76 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: PFRPalomar/Solution.lean:48 (same statement text; different proof or body). Qualify references as Marton.pfr_conjecture_nine@path.

   Tactic trace: 1 steps

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

   theorem pfr_conjecture_nine {G : Type*} [AddCommGroup G] (h2 : ∀ x : G, 2 • x = 0) {A : Set G}
       (hA : A.Finite) (hA₀ : A.Nonempty) {K : ℝ} (hAK : Nat.card (A + A) ≤ K * Nat.card A) :
       ∃ (H : AddSubgroup G) (c : Set G), c.Finite ∧ (H : Set G).Finite ∧
         Nat.card c < 2 * K ^ 9 ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by
   …

3. theorem Marton.torsion_pfr_conjecture Marton's conjecture in abelian groups of bounded torsion, [GGMT2], Theorem 1.1 sorry line 98 source

   Source documentation

   Marton's conjecture in abelian groups of bounded torsion, [GGMT2], Theorem 1.1.

   Let G be an abelian group of torsion m ≥ 2, meaning that m • x = 0 for every x : G. If A is a finite non-empty subset of G with |A + A| ≤ K * |A|, then A is covered by fewer than m * K ^ (256 * m ^ 3 + 1) cosets of a subgroup H of G with |H| ≤ |A|.

   The ambient group G is not required to be finite; the covering set c and the subgroup H produced are then finite.

   depends on sorry what this means

   Statement uses: AddCommGroup, Nat, LE.le, OfNat.ofNat, Eq, HSMul.hSMul, Set, Set.Finite, Set.Nonempty, Real, Nat.card, HAdd.hAdd, HMul.hMul, Exists, AddSubgroup, And, LT.lt, HPow.hPow, Subtype, Membership.mem

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   76 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: PFRPalomar/Solution.lean:55 (same statement text; different proof or body). Qualify references as Marton.torsion_pfr_conjecture@path.

   Tactic trace: 1 steps

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

   theorem torsion_pfr_conjecture {G : Type*} [AddCommGroup G] {m : ℕ} (hm : 2 ≤ m)
       (htorsion : ∀ x : G, m • x = 0) {A : Set G} (hA : A.Finite) (hA₀ : A.Nonempty) {K : ℝ}
       (hAK : Nat.card (A + A) ≤ K * Nat.card A) :
       ∃ (H : AddSubgroup G) (c : Set G), c.Finite ∧ (H : Set G).Finite ∧
         Nat.card c < m * K ^ (256 * m ^ 3 + 1) ∧ Nat.card H ≤ Nat.card A ∧ A ⊆ c + H := by
   …

4. theorem Marton.weak_pfr_int Weak Marton's conjecture over the integers, [GGMT], Theorem 1.3 sorry line 114 source

   Source documentation

   Weak Marton's conjecture over the integers, [GGMT], Theorem 1.3.

   Let G be a finitely generated free ℤ-module, that is, a copy of ℤ ^ D. If A is a finite non-empty subset of G with |A + A| ≤ K * |A|, then A has a subset A' with |A'| ≥ K ^ (-34) * |A| whose affine dimension — the rank of the ℤ-span of its difference set — is at most (80 / log 2) * log K.

   This realises the constants C₁ = 34 and C₂ = 80 / log 2 of [GGMT], Theorem 1.3, which is stated there for unspecified absolute constants.

   depends on sorry what this means

   Statement uses: AddCommGroup, Module.Free, Int, Module.Finite, Set, Set.Finite, Set.Nonempty, Real, LE.le, Nat.card, HAdd.hAdd, HMul.hMul, Exists, And, HPow.hPow, Neg.neg, OfNat.ofNat, Nat, Module.finrank, Subtype and 5 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   66 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: PFRPalomar/Solution.lean:63 (same statement text; different proof or body). Qualify references as Marton.weak_pfr_int@path.

   Tactic trace: 1 steps

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

   theorem weak_pfr_int {G : Type*} [AddCommGroup G] [Module.Free ℤ G] [Module.Finite ℤ G]
       {A : Set G} (hA : A.Finite) (hA₀ : A.Nonempty) {K : ℝ}
       (hAK : Nat.card (A + A) ≤ K * Nat.card A) :
       ∃ A' ⊆ A, K ^ (-34 : ℝ) * Nat.card A ≤ Nat.card A' ∧
         (Module.finrank ℤ (vectorSpan ℤ A') : ℝ) ≤ (80 / Real.log 2) * Real.log K := by
   …

5. theorem Marton.homomorphism_pfr The homomorphism form of Marton's conjecture, [GGMT], Corollary 1.4 sorry line 126 source

   Source documentation

   The homomorphism form of Marton's conjecture, [GGMT], Corollary 1.4.

   Let G and G' be finite abelian groups of exponent 2 and let f : G → G' be a function whose additive defects f (x + y) - f x - f y all lie in a set S. Then f differs from a group homomorphism φ : G →+ G' by a function taking at most |S| ^ 10 values.

   depends on sorry what this means

   Statement uses: AddCommGroup, Finite, Eq, HSMul.hSMul, Nat, OfNat.ofNat, Set, Membership.mem, HSub.hSub, HAdd.hAdd, Exists, AddMonoidHom, And, LE.le, Nat.card, HPow.hPow

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   62 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: PFRPalomar/Solution.lean:77 (same statement text; different proof or body). Qualify references as Marton.homomorphism_pfr@path.

   Tactic trace: 1 steps

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

   theorem homomorphism_pfr {G G' : Type*} [AddCommGroup G] [AddCommGroup G'] [Finite G] [Finite G']
       (h2 : ∀ x : G, 2 • x = 0) (h2' : ∀ y : G', 2 • y = 0) (f : G → G') (S : Set G')
       (hS : ∀ x y : G, f (x + y) - f x - f y ∈ S) :
       ∃ (φ : G →+ G') (T : Set G'), Nat.card T ≤ Nat.card S ^ 10 ∧ ∀ x : G, f x - φ x ∈ T := by
   …

6. theorem Marton.approx_hom_pfr The approximate homomorphism form of Marton's conjecture, [GGMT], Corollary 1.5 sorry line 139 source

   Source documentation

   The approximate homomorphism form of Marton's conjecture, [GGMT], Corollary 1.5.

   Let G and G' be finite abelian groups of exponent 2 and let f : G → G' be a function such that f (x + y) = f x + f y for at least a proportion K⁻¹ of the pairs (x, y) ∈ G × G, written here as |G| ^ 2 ≤ K * |{(x, y) | f (x + y) = f x + f y}|. Then there is a group homomorphism φ : G →+ G' agreeing with f on at least (|G| / (2 ^ 144 * K ^ 122) - 1) / 2 points of G.

   depends on sorry what this means

   Statement uses: AddCommGroup, Finite, Eq, HSMul.hSMul, Nat, OfNat.ofNat, Real, LT.lt, LE.le, HPow.hPow, Nat.card, HMul.hMul, Prod, Set.ofPred, HAdd.hAdd, Prod.fst, Prod.snd, Exists, AddMonoidHom, HDiv.hDiv and 1 more

   Proof uses: sorryAx, Lean.Name, Bool.false, Lean.Name.num, Lean.Name.str, Lean.Name.anonymous

   88 instances, coercions and auxiliary constants left out.

   Distinct definitions of this name: PFRPalomar/Solution.lean:106 (same statement text; different proof or body). Qualify references as Marton.approx_hom_pfr@path.

   Tactic trace: 1 steps

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

   theorem approx_hom_pfr {G G' : Type*} [AddCommGroup G] [AddCommGroup G'] [Finite G] [Finite G']
       (h2 : ∀ x : G, 2 • x = 0) (h2' : ∀ y : G', 2 • y = 0) (f : G → G') {K : ℝ} (hK : 0 < K)
       (hf : (Nat.card G : ℝ) ^ 2 ≤ K * Nat.card {x : G × G | f (x.1 + x.2) = f x.1 + f x.2}) :
       ∃ φ : G →+ G',
         (Nat.card G / (2 ^ 144 * K ^ 122) - 1) / 2 ≤ Nat.card {x : G | f x = φ x} := by
   …