Source indexedtheorem · leanprover/lean4:v4.33.0-rc1

weak_PFR_int

PFR.WeakPFR · PFR/WeakPFR.lean:1036 to 1055

Source documentation

Let $A\subseteq \mathbb{Z}^d$ and $\lvert A-A\rvert\leq K\lvert A\rvert$ . There exists $A'\subseteq A$ such that $\lvert A'\rvert \geq K^{-17}\lvert A\rvert$ and $\dim A' \leq \frac{40}{\log 2} \log K$ .

Exact Lean statement

theorem weak_PFR_int
    {G : Type*} [AddCommGroup G] [Module.Free ℤ G] [Module.Finite ℤ G]
    {A : Set G} [A_fin : Finite A] (hnA : A.Nonempty) {K : ℝ}
    (hA : Nat.card (A - A) ≤ K * Nat.card A) :
    ∃ A' : Set G, A' ⊆ A ∧ Nat.card A' ≥ K ^ (-17 : ℝ) * Nat.card A ∧
      AffineSpace.finrank ℤ A' ≤ (40 / log 2) * log K

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

theorem weak_PFR_int    {G : Type*} [AddCommGroup G] [Module.Free ℤ G] [Module.Finite ℤ G]    {A : Set G} [A_fin : Finite A] (hnA : A.Nonempty) {K : ℝ}    (hA : Nat.card (A - A) ≤ K * Nat.card A) :    ∃ A' : Set G, A' ⊆ A ∧ Nat.card A' ≥ K ^ (-17 : ℝ) * Nat.card A ∧      AffineSpace.finrank ℤ A' ≤ (40 / log 2) * log K := by  have : Nonempty (A - A) := (hnA.sub hnA).coe_sort  have : Finite (A - A) := Set.Finite.sub A_fin A_fin  have hK : 0 < K := by    have : 0 < K * Nat.card A := lt_of_lt_of_le (mod_cast Nat.card_pos) hA    nlinarith  have : Countable G := countable_of_finiteDimensional ℤ G  let m : MeasurableSpace G := ⊤  apply weak_PFR hnA hK ((setRuzsaDist_le A A hnA hnA).trans _)  suffices log (Nat.card (A-A)) ≤ log K + log (Nat.card A) by linarith  rw [← log_mul (by positivity) _]  · apply log_le_log _ hA    norm_cast    exact Nat.card_pos  exact_mod_cast ne_of_gt (@Nat.card_pos _ hnA.to_subtype _)