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

weak_PFR

PFR.WeakPFR · PFR/WeakPFR.lean:988 to 1031

Source documentation

If $A\subseteq \mathbb{Z}^d$ is a finite non-empty set with $d[U_A;U_A]\leq \log K$ then there exists a non-empty $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

lemma weak_PFR {A : Set G} [Finite A] {K : ℝ} (hA : A.Nonempty) (hK : 0 < K)
    (hdist : dᵤ[A # A] ≤ log K) :
    ∃ A' : Set G, A' ⊆ A ∧ K^(-17 : ℝ) * Nat.card A ≤ Nat.card A' ∧
      AffineSpace.finrank ℤ A' ≤ (40 / log 2) * log K

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma weak_PFR {A : Set G} [Finite A] {K : ℝ} (hA : A.Nonempty) (hK : 0 < K)    (hdist : dᵤ[A # A] ≤ log K) :    ∃ A' : Set G, A' ⊆ A ∧ K^(-17 : ℝ) * Nat.card A ≤ Nat.card A' ∧      AffineSpace.finrank ℤ A' ≤ (40 / log 2) * log K := by  rcases weak_PFR_asymm A A hA hA with ⟨A', A'', hA', hA'', hA'nonempty, hA''nonempty, hcard, hdim⟩  have : ∃ B : Set G, B ⊆ A ∧ Nat.card B ≥ Nat.card A' ∧ Nat.card B ≥ Nat.card A''      ∧ AffineSpace.finrank ℤ B ≤ max (AffineSpace.finrank ℤ A') (AffineSpace.finrank ℤ A'') := by    rcases lt_or_ge (Nat.card A') (Nat.card A'') with h | h    · exact ⟨A'', hA'', by linarith, by linarith, le_max_right _ _⟩    · exact ⟨A', hA', by linarith, by linarith, le_max_left _ _⟩  rcases this with ⟨B, hB, hBcard, hBcard', hBdim⟩  use B  have hApos : Nat.card A > 0 := by    rw [gt_iff_lt, Nat.card_pos_iff]    exact ⟨hA.to_subtype, inferInstance⟩  have hA'pos : Nat.card A' > 0 := by    rw [gt_iff_lt, Nat.card_pos_iff]    exact ⟨hA'nonempty.to_subtype, Finite.Set.subset _ hA'⟩  have hA''pos : Nat.card A'' > 0 := by    rw [gt_iff_lt, Nat.card_pos_iff]    exact ⟨hA''nonempty.to_subtype, Finite.Set.subset _ hA''⟩  have hBpos : Nat.card B > 0 := by linarith  refine ⟨hB, ?_, ?_⟩  · have := calc 2 * log (Nat.card A / Nat.card B)      _ = log ((Nat.card A * Nat.card A) / (Nat.card B * Nat.card B)) := by        convert! (log_pow (Nat.card A / Nat.card B) 2).symm        field_simp      _ ≤ log ((Nat.card A * Nat.card A) / (Nat.card A' * Nat.card A'')) := by        apply log_le_log        · positivity        gcongr      _ ≤ 34 * dᵤ[A # A] := hcard      _ ≤ 34 * log K := mul_le_mul_of_nonneg_left hdist (by linarith)      _ = 2 * (17 * log K) := by ring      _ = 2 * log (K^17) := by simp    rw [mul_le_mul_iff_right₀ (by norm_num), log_le_log_iff (by positivity) (by positivity),      div_le_iff₀ (by positivity), ← mul_inv_le_iff₀' (by positivity), mul_comm] at this    convert! this using 2    convert! zpow_neg K 17 using 1    norm_cast  calc (AffineSpace.finrank ℤ B : ℝ)    _ ≤ (((max (AffineSpace.finrank ℤ A') (AffineSpace.finrank ℤ A'')) : ℕ) : ℝ) := by norm_cast    _ ≤ (40 / log 2) * dᵤ[A # A] := hdim    _ ≤ (40 / log 2) * log K := mul_le_mul_of_nonneg_left hdist (by positivity)