Skip to content

Commit

Permalink
More calculations in di_in_ff
Browse files Browse the repository at this point in the history
  • Loading branch information
@YaelDillies
YaelDillies committed Sep 3, 2024
1 parent 562a2d8 commit 50ea3d8
Showing 1 changed file with 84 additions and 28 deletions.
112 changes: 84 additions & 28 deletions LeanAPAP/FiniteField/Basic.lean
View file
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,7 @@ open Finset hiding card
open scoped NNReal BigOperators Combinatorics.Additive Pointwise

universe u
variable {G : Type u} [AddCommGroup G] [DecidableEq G] [Fintype G] [MeasurableSpace G]
[DiscreteMeasurableSpace G] {A C : Finset G} {x γ ε : ℝ}
variable {G : Type u} [AddCommGroup G] [DecidableEq G] [Fintype G] {A C : Finset G} {x y γ ε : ℝ}

local notation "𝓛" x:arg => 1 + log x⁻¹

Expand All @@ -44,8 +43,36 @@ private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻
· simp
_ ≤ exp 1 := x⁻¹.rpow_inv_log_le_exp_one

lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ)
(hAC : ε ≤ |card G * ⟪μ A ∗ μ A, μ C⟫_[ℝ] - 1|) :
private lemma curlog_mul_le (hx₀ : 0 < x) (hx₁ : x ≤ 1) (hy₀ : 0 < y) (hy₁ : y ≤ 1) :
𝓛 (x * y) ≤ x⁻¹ * 𝓛 y := by
suffices h : log x⁻¹ - (x⁻¹ - 1) ≤ (x⁻¹ - 1) * log y⁻¹ by
rw [← sub_nonneg] at h ⊢
exact h.trans_eq (by rw [mul_inv, log_mul]; ring; all_goals positivity)
calc
log x⁻¹ - (x⁻¹ - 1) ≤ 0 := sub_nonpos.2 $ log_le_sub_one_of_pos $ by positivity
_ ≤ (x⁻¹ - 1) * log y⁻¹ :=
mul_nonneg (sub_nonneg.2 $ one_le_inv hx₀ hx₁) $ log_nonneg $ one_le_inv hy₀ hy₁

private lemma curlog_rpow_le' (hx₀ : 0 < x) (hx₁ : x ≤ 1) (hy₀ : 0 < y) (hy₁ : y ≤ 1) :
𝓛 (x ^ y) ≤ y⁻¹ * 𝓛 x := by
suffices h : 1 - y⁻¹ ≤ (y⁻¹ - y) * log x⁻¹ by
rw [← sub_nonneg] at h ⊢
exact h.trans_eq (by rw [← inv_rpow, log_rpow]; ring; all_goals positivity)
calc
1 - y⁻¹ ≤ 0 := sub_nonpos.2 $ one_le_inv hy₀ hy₁
_ ≤ (y⁻¹ - y) * log x⁻¹ :=
mul_nonneg (sub_nonneg.2 $ hy₁.trans $ one_le_inv hy₀ hy₁) $ log_nonneg $ one_le_inv hx₀ hx₁

private lemma curlog_rpow_le (hx₀ : 0 < x) (hy : 1 ≤ y) : 𝓛 (x ^ y) ≤ y * 𝓛 x := by
rw [← inv_rpow, log_rpow, mul_one_add]
gcongr
all_goals positivity

private lemma curlog_pow_le {n : ℕ} (hx₀ : 0 < x) (hn : n ≠ 0) : 𝓛 (x ^ n) ≤ n * 𝓛 x := by
rw [← rpow_natCast]; exact curlog_rpow_le hx₀ $ mod_cast Nat.one_le_iff_ne_zero.2 hn

lemma global_dichotomy [MeasurableSpace G] [DiscreteMeasurableSpace G] (hA : A.Nonempty)
(hγC : γ ≤ C.dens) (hγ : 0 < γ) (hAC : ε ≤ |card G * ⟪μ A ∗ μ A, μ C⟫_[ℝ] - 1|) :
ε / (2 * card G) ≤ ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[↑(2 * ⌈𝓛 γ⌉₊), const _ (card G)⁻¹] := by
have hC : C.Nonempty := by simpa using hγ.trans_le hγC
have hγ₁ : γ ≤ 1 := hγC.trans (by norm_cast; exact dens_le_one)
Expand Down Expand Up @@ -99,6 +126,8 @@ lemma ap_in_ff (hα₀ : 0 < α) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hαA₁
2 ^ 27 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 / ε ^ 2 ∧
|∑ x ∈ S, (μ (Set.toFinset V) ∗ μ A₁ ∗ μ A₂) x - ∑ x ∈ S, (μ A₁ ∗ μ A₂) x| ≤ ε := by
classical
let _ : MeasurableSpace G := ⊤
have : DiscreteMeasurableSpace G := ⟨fun _ ↦ trivial⟩
have hA₁ : A₁.Nonempty := by simpa using hα₀.trans_le hαA₁
have hA₂ : A₂.Nonempty := by simpa using hα₀.trans_le hαA₂
have hα₁ : α ≤ 1 := hαA₁.trans $ mod_cast A₁.dens_le_one
Expand Down Expand Up @@ -126,11 +155,12 @@ lemma ap_in_ff (hα₀ : 0 < α) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (hαA₁
_ = _ := sorry
sorry

lemma di_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε < 1) (hA₀ : A.Nonempty)
lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q) (hq : q.Prime)
(hε₀ : 0 < ε) (hε₁ : ε < 1) (hA₀ : A.Nonempty)
(hγC : γ ≤ C.dens) (hγ : 0 < γ) (hAC : ε ≤ |card G * ⟪μ A ∗ μ A, μ C⟫_[ℝ] - 1|) :
∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)),
↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤
2 ^ 171 * 𝓛 A.dens ^ 4 * 𝓛 γ ^ 4 / ε ^ 24 ∧
2 ^ 179 * 𝓛 A.dens ^ 4 * 𝓛 γ ^ 4 / ε ^ 24 ∧
(1 + ε / 32) * A.dens ≤ ‖𝟭_[ℝ] A ∗ μ (Set.toFinset V)‖_[⊤] := by
have hγ₁ : γ ≤ 1 := hγC.trans (by norm_cast; exact dens_le_one)
have hG : (card G : ℝ) ≠ 0 := by positivity
Expand All @@ -139,12 +169,15 @@ lemma di_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε <
let p' : ℝ := 240 / ε * log (6 / ε) * p
let q' : ℕ := 2 * ⌈p' + 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊
let f : G → ℝ := balance (μ A)
have hα₀ : 0 < α := by positivity
have hα₁ : α ≤ 1 := by unfold_let α; exact mod_cast A.dens_le_one
have : 0 < 𝓛 γ := curlog_pos hγ.le hγ₁
have : 0 < p := by positivity
have : 0 < log (6 / ε) := log_pos $ (one_lt_div hε₀).2 (by linarith)
have : 0 < p' := by positivity
have : 0 < log (64 / ε) := log_pos $ (one_lt_div hε₀).2 (by linarith)
have : 0 < q' := by positivity
have : q' ≤ 2 ^ 30 * 𝓛 γ / ε ^ 5 := sorry
have :=
calc
1 + ε / 4 = 1 + ε / 2 / 2 := by ring
Expand Down Expand Up @@ -187,14 +220,37 @@ lemma di_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε <
ap_in_ff _ (by positivity) (by positivity) (by linarith) hA₁ hA₂
refine ⟨V, inferInstance, ?_, ?_⟩
· calc
↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤
2 ^ 27 * 𝓛 (4⁻¹ * α ^ (2 * q')) ^ 2 * 𝓛 (ε / 32 * (4⁻¹ * α ^ (2 * q'))) ^ 2 / (ε / 32) ^ 2
:= hVdim
_ ≤ 2 ^ 171 * 𝓛 α ^ 4 * 𝓛 γ ^ 4 / ε ^ 24 := sorry
↑(finrank (ZMod q) G - finrank (ZMod q) V)
≤ 2 ^ 27 * 𝓛 (4⁻¹ * α ^ (2 * q')) ^ 2 *
𝓛 (ε / 32 * (4⁻¹ * α ^ (2 * q'))) ^ 2 / (ε / 32) ^ 2 := hVdim
_ ≤ 2 ^ 27 * (8 * q' * 𝓛 α) ^ 2 *
(2 ^ 8 * q' * 𝓛 α / ε) ^ 2 / (ε / 32) ^ 2 := by
have : α ^ (2 * q') ≤ 1 := pow_le_one _ hα₀.le hα₁
have : 4⁻¹ * α ^ (2 * q') ≤ 1 := mul_le_one (by norm_num) (by positivity) ‹_›
have : ε / 32 * (4⁻¹ * α ^ (2 * q')) ≤ 1 := mul_le_one (by linarith) (by positivity) ‹_›
have : 0 ≤ log (ε / 32 * (4⁻¹ * α ^ (2 * q')))⁻¹ :=
log_nonneg $ one_le_inv (by positivity) ‹_›
have : 0 ≤ log (4⁻¹ * α ^ (2 * q'))⁻¹ := log_nonneg $ one_le_inv (by positivity) ‹_›
have : 0 ≤ log (α ^ (2 * q'))⁻¹ := log_nonneg $ one_le_inv (by positivity) ‹_›
have :=
calc
𝓛 (4⁻¹ * α ^ (2 * q')) ≤ 4⁻¹⁻¹ * 𝓛 (α ^ (2 * q')) :=
curlog_mul_le (by norm_num) (by norm_num) (by positivity) ‹_›
_ ≤ 4⁻¹⁻¹ * (↑(2 * q') * 𝓛 α) := by gcongr; exact curlog_pow_le hα₀ (by positivity)
_ = 8 * q' * 𝓛 α := by push_cast; ring
gcongr
calc
𝓛 (ε / 32 * (4⁻¹ * α ^ (2 * q'))) ≤ (ε / 32)⁻¹ * 𝓛 (4⁻¹ * (α ^ (2 * q'))) :=
curlog_mul_le (by positivity) (by linarith) (by positivity) ‹_›
_ ≤ (ε / 32)⁻¹ * (8 * q' * 𝓛 α) := by gcongr
_ = 2 ^ 8 * q' * 𝓛 α / ε := by ring
_ = 2 ^ 59 * q' ^ 4 * 𝓛 α ^ 4 / ε ^ 4 := by ring
_ ≤ 2 ^ 59 * (2 ^ 30 * 𝓛 γ / ε ^ 5) ^ 4 * 𝓛 α ^ 4 / ε ^ 4 := by gcongr
_ = 2 ^ 179 * 𝓛 α ^ 4 * 𝓛 γ ^ 4 / ε ^ 24 := by ring
· sorry

theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
(hA : ThreeAPFree (α := G) A) : finrank (ZMod q) G ≤ 2 ^ 203 * 𝓛 A.dens ^ 9 := by
(hA : ThreeAPFree (α := G) A) : finrank (ZMod q) G ≤ 2 ^ 211 * 𝓛 A.dens ^ 9 := by
let n : ℝ := finrank (ZMod q) G
let α : ℝ := A.dens
have : 1 < (q : ℝ) := mod_cast hq₃.trans_lt' (by norm_num)
Expand All @@ -213,22 +269,22 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
calc
_ ≤ (log 2 + 2 * log α⁻¹) / (log q / 2) := hα
_ = 4 / log q * (log 2 / 2 + log α⁻¹) := by ring
_ ≤ 2 ^ 203 * (1 + 0) ^ 8 * (1 + log α⁻¹) := by
_ ≤ 2 ^ 211 * (1 + 0) ^ 8 * (1 + log α⁻¹) := by
gcongr
· calc
4 / log q ≤ 4 / log 3 := by gcongr; assumption_mod_cast
_ ≤ 4 / log 2 := by gcongr; norm_num
_ ≤ 4 / 0.6931471803 := by gcongr; exact log_two_gt_d9.le
_ ≤ 2 ^ 203 * (1 + 0) ^ 8 := by norm_num
_ ≤ 2 ^ 211 * (1 + 0) ^ 8 := by norm_num
· calc
log 2 / 2 ≤ 0.6931471808 / 2 := by gcongr; exact log_two_lt_d9.le
_ ≤ 1 := by norm_num
_ ≤ 2 ^ 203 * 𝓛 α ^ 8 * 𝓛 α := by gcongr
_ = 2 ^ 203 * 𝓛 α ^ 9 := by rw [pow_succ _ 8, mul_assoc]
_ ≤ 2 ^ 211 * 𝓛 α ^ 8 * 𝓛 α := by gcongr
_ = 2 ^ 211 * 𝓛 α ^ 9 := by rw [pow_succ _ 8, mul_assoc]
all_goals positivity
have ind (i : ℕ) :
∃ (V : Type u) (_ : AddCommGroup V) (_ : Fintype V) (_ : DecidableEq V) (_ : Module (ZMod q) V)
(B : Finset V), n ≤ finrank (ZMod q) V + 2 ^ 195 * i * 𝓛 α ^ 8 ∧ ThreeAPFree (B : Set V)
(B : Finset V), n ≤ finrank (ZMod q) V + 2 ^ 203 * i * 𝓛 α ^ 8 ∧ ThreeAPFree (B : Set V)
∧ α ≤ B.dens ∧
(B.dens < (65 / 64 : ℝ) ^ i * α →
2⁻¹ ≤ card V * ⟪μ B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) := by
Expand Down Expand Up @@ -268,13 +324,13 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
refine ⟨V', inferInstance, inferInstance, inferInstance, inferInstance, B', ?_, ?_, ?_,
fun h ↦ ?_⟩
· calc
n ≤ finrank (ZMod q) V + 2 ^ 195 * i * 𝓛 α ^ 8 := hV
n ≤ finrank (ZMod q) V + 2 ^ 203 * i * 𝓛 α ^ 8 := hV
_ ≤ finrank (ZMod q) V' + ↑(finrank (ZMod q) V - finrank (ZMod q) V') +
2 ^ 195 * i * 𝓛 α ^ 8 := by gcongr; norm_cast; exact le_add_tsub
_ ≤ finrank (ZMod q) V' + 2 ^ 171 * 𝓛 B.dens ^ 4 * 𝓛 α ^ 4 / 2⁻¹ ^ 24 +
2 ^ 195 * i * 𝓛 α ^ 8 := by gcongr
_ ≤ finrank (ZMod q) V' + 2 ^ 171 * 𝓛 α ^ 4 * 𝓛 α ^ 4 / 2⁻¹ ^ 24 +
2 ^ 195 * i * 𝓛 α ^ 8 := by have := hα₀.trans_le hαβ; gcongr
2 ^ 203 * i * 𝓛 α ^ 8 := by gcongr; norm_cast; exact le_add_tsub
_ ≤ finrank (ZMod q) V' + 2 ^ 179 * 𝓛 B.dens ^ 4 * 𝓛 α ^ 4 / 2⁻¹ ^ 24 +
2 ^ 203 * i * 𝓛 α ^ 8 := by gcongr
_ ≤ finrank (ZMod q) V' + 2 ^ 179 * 𝓛 α ^ 4 * 𝓛 α ^ 4 / 2⁻¹ ^ 24 +
2 ^ 203 * i * 𝓛 α ^ 8 := by have := hα₀.trans_le hαβ; gcongr
_ = _ := by push_cast; ring
· exact .of_image .subtypeVal Set.injOn_subtype_val (Set.subset_univ _)
(hB.vadd_set (a := -x) |>.mono $ by simp [B'])
Expand Down Expand Up @@ -308,7 +364,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
_ ≤ 1 := by norm_num
all_goals positivity
rw [hB.dL2Inner_mu_conv_mu_mu_two_smul_mu] at hBV
suffices h : (q ^ (n - 2 ^ 202 * 𝓛 α ^ 9) : ℝ) ≤ q ^ (n / 2) by
suffices h : (q ^ (n - 2 ^ 210 * 𝓛 α ^ 9) : ℝ) ≤ q ^ (n / 2) by
rwa [rpow_le_rpow_left_iff ‹_›, sub_le_comm, sub_half, div_le_iff₀' zero_lt_two, ← mul_assoc,
← pow_succ'] at h
calc
Expand All @@ -317,18 +373,18 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty)
· assumption
rw [sub_le_comm]
calc
n - finrank (ZMod q) V ≤ 2 ^ 195 * ⌊𝓛 α / log (65 / 64)⌋₊ * 𝓛 α ^ 8 := by
n - finrank (ZMod q) V ≤ 2 ^ 203 * ⌊𝓛 α / log (65 / 64)⌋₊ * 𝓛 α ^ 8 := by
rwa [sub_le_iff_le_add']
_ ≤ 2 ^ 195 * (𝓛 α / log (65 / 64)) * 𝓛 α ^ 8 := by
_ ≤ 2 ^ 203 * (𝓛 α / log (65 / 64)) * 𝓛 α ^ 8 := by
gcongr; exact Nat.floor_le (by positivity)
_ = 2 ^ 195 * (log (65 / 64)) ⁻¹ * 𝓛 α ^ 9 := by ring
_ ≤ 2 ^ 195 * 2 ^ 7 * 𝓛 α ^ 9 := by
_ = 2 ^ 203 * (log (65 / 64)) ⁻¹ * 𝓛 α ^ 9 := by ring
_ ≤ 2 ^ 203 * 2 ^ 7 * 𝓛 α ^ 9 := by
gcongr
rw [inv_le ‹_› (by positivity)]
calc
(2 ^ 7)⁻¹ ≤ 1 - (65 / 64)⁻¹ := by norm_num
_ ≤ log (65 / 64) := one_sub_inv_le_log_of_pos (by positivity)
_ = 2 ^ 202 * 𝓛 α ^ 9 := by ring
_ = 2 ^ 210 * 𝓛 α ^ 9 := by ring
_ = ↑(card V) := by simp [card_eq_pow_finrank (K := ZMod q) (V := V)]
_ ≤ 2 * β⁻¹ ^ 2 := by
rw [← natCast_card_mul_nnratCast_dens, mul_pow, mul_inv, ← mul_assoc,
Expand Down

0 comments on commit 50ea3d8

Please sign in to comment.