Marton's conjecture: proofs

Proofs of the statements from the upstream PFRPalomar.Challenge module, which is not included in this import, obtained from the corresponding results of the PFR library.

theorem Marton.pfr_conjecture {G : Type u_1} [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).Finite ∧ ↑(Nat.card ↑c) < 2 * K ^ 12 ∧ Nat.card ↥H ≤ Nat.card ↑A ∧ A ⊆ c + ↑H

theorem Marton.pfr_conjecture_nine {G : Type u_1} [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).Finite ∧ ↑(Nat.card ↑c) < 2 * K ^ 9 ∧ Nat.card ↥H ≤ Nat.card ↑A ∧ A ⊆ c + ↑H

theorem Marton.torsion_pfr_conjecture {G : Type u_1} [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).Finite ∧ ↑(Nat.card ↑c) < ↑m * K ^ (256 * m ^ 3 + 1) ∧ Nat.card ↥H ≤ Nat.card ↑A ∧ A ⊆ c + ↑H

theorem Marton.weak_pfr_int {G : Type u_1} [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

theorem Marton.homomorphism_pfr {G : Type u_1} {G' : Type u_2} [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

theorem Marton.approx_hom_pfr {G : Type u_1} {G' : Type u_2} [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})