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

better_PFR_conjecture

PFR.RhoFunctional · PFR/RhoFunctional.lean:2069 to 2130

Source documentation

If $A \subset {\bf F}_2^n$ is finite non-empty with $|A+A| \leq K|A|$ , then there exists a subgroup $H$ of ${\bf F}_2^n$ with $|H| \leq |A|$ such that $A$ can be covered by at most $2K^9$ translates of $H$ .

Exact Lean statement

lemma better_PFR_conjecture {A : Set G} (h₀A : A.Nonempty) {K : ℝ}
    (hA : Nat.card (A + A) ≤ K * Nat.card A) :
    ∃ (H : Submodule (ZMod 2) G) (c : Set G),
      Nat.card c < 2 * K ^ 9 ∧ (H : Set G).ncard ≤ Nat.card A ∧ A ⊆ c + H

Complete declaration

Lean source

Canonical source

Full Lean sourceLean 4

lemma better_PFR_conjecture {A : Set G} (h₀A : A.Nonempty) {K : ℝ}    (hA : Nat.card (A + A) ≤ K * Nat.card A) :    ∃ (H : Submodule (ZMod 2) G) (c : Set G),      Nat.card c < 2 * K ^ 9 ∧ (H : Set G).ncard ≤ Nat.card A ∧ A ⊆ c + H := by  obtain ⟨A_pos, -, K_pos⟩ : (0 : ℝ) < Nat.card A ∧ (0 : ℝ) < Nat.card (A + A) ∧ 0 < K :=    PFR_conjecture_pos_aux' (Set.toFinite _) h₀A hA  -- consider the subgroup `H` given by Lemma `PFR_conjecture_aux`.  obtain ⟨H, c, hc, IHA, IAH, A_subs_cH⟩ : ∃ (H : Submodule (ZMod 2) G) (c : Set G),    Nat.card c ≤ K ^ 5 * Nat.card A ^ (1 / 2 : ℝ) * (H : Set G).ncard ^ (-1 / 2 : ℝ)      ∧ (H : Set G).ncard ≤ K ^ 8 * Nat.card A ∧ Nat.card A ≤ K ^ 8 * (H : Set G).ncard      ∧ A ⊆ c + H :=    better_PFR_conjecture_aux h₀A hA  have H_pos : (0 : ℝ) < (H : Set G).ncard := by    have : 0 < (H : Set G).ncard := Nat.card_pos; positivity  rcases le_or_gt ((H : Set G).ncard) (Nat.card A) with h|h  -- If `#H ≤ #A`, then `H` satisfies the conclusion of the theorem  · refine ⟨H, c, ?_, h, A_subs_cH⟩    calc    Nat.card c ≤ K ^ 5 * Nat.card A ^ (1 / 2 : ℝ) * (H : Set G).ncard ^ (-1 / 2 : ℝ) := hc    _ ≤ K ^ 5 * (K ^ 8 * (H : Set G).ncard) ^ (1 / 2 : ℝ) * (H : Set G).ncard ^ (-1 / 2 : ℝ) := by      gcongr    _ = K ^ 9 := by simp_rw [← rpow_natCast]; rpow_ring; norm_num    _ < 2 * K ^ 9 := by linarith [show 0 < K ^ 9 by positivity]  -- otherwise, we decompose `H` into cosets of one of its subgroups `H'`, chosen so that  -- `#A / 2 < #H' ≤ #A`. This `H'` satisfies the desired conclusion.  · obtain ⟨H', IH'A, IAH', H'H⟩ : ∃ H' : Submodule (ZMod 2) G, Nat.card H' ≤ Nat.card A          ∧ Nat.card A < 2 * Nat.card H' ∧ H' ≤ H := by      have A_pos' : 0 < Nat.card A := mod_cast A_pos      exact ZModModule.exists_submodule_subset_card_le Nat.prime_two H h.le A_pos'.ne'    have : (Nat.card A / 2 : ℝ) < Nat.card H' := by      rw [div_lt_iff₀ zero_lt_two, mul_comm]; norm_cast    have H'_pos : (0 : ℝ) < Nat.card H' := by      have : 0 < Nat.card H' := Nat.card_pos; positivity    obtain ⟨u, HH'u, hu⟩ :=      H'.toAddSubgroup.exists_left_transversal_of_le (H := H.toAddSubgroup) H'H    dsimp at HH'u    refine ⟨H', c + u, ?_, IH'A, by rwa [add_assoc, HH'u]⟩    calc    (Nat.card (c + u) : ℝ)      ≤ Nat.card c * Nat.card u := mod_cast natCard_add_le    _ ≤ (K ^ 5 * Nat.card A ^ (1 / 2 : ℝ) * ((H : Set G).ncard ^ (-1 / 2 : ℝ)))          * ((H : Set G).ncard / Nat.card H') := by        gcongr        apply le_of_eq        rw [eq_div_iff H'_pos.ne']        norm_cast    _ < (K ^ 5 * Nat.card A ^ (1 / 2 : ℝ) * ((H : Set G).ncard ^ (-1 / 2 : ℝ)))          * ((H : Set G).ncard / (Nat.card A / 2)) := by        gcongr    _ = (K ^ 5 * Nat.card A ^ (1 / 2 : ℝ) * ((H : Set G).ncard ^ (-1 / 2 : ℝ)))          * ((H : Set G).ncard * (Nat.card A : ℝ)⁻¹ * 2) := by        field_simp    _ = 2 * K ^ 5 * Nat.card A ^ (-1 / 2 : ℝ) * (H : Set G).ncard ^ (1 / 2 : ℝ) := by        rpow_ring        field_simp        norm_num    _ ≤ 2 * K ^ 5 * Nat.card A ^ (-1 / 2 : ℝ) * (K ^ 8 * Nat.card A) ^ (1 / 2 : ℝ) := by        gcongr    _ = 2 * K ^ 9 := by        simp_rw [← rpow_natCast]        rpow_ring        norm_num