From 13f007ed069fac721edf28d4d68d94a683c7c6a2 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Mon, 2 Sep 2024 15:00:11 +0000 Subject: [PATCH] Don't use `curlog` in the finite field case --- LeanAPAP/FiniteField/Basic.lean | 125 ++++++++++++++---------- LeanAPAP/Physics/AlmostPeriodicity.lean | 1 - 2 files changed, 73 insertions(+), 53 deletions(-) diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean index bbf3951630..196725d42b 100644 --- a/LeanAPAP/FiniteField/Basic.lean +++ b/LeanAPAP/FiniteField/Basic.lean @@ -2,7 +2,6 @@ import Mathlib.FieldTheory.Finite.Basic import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic import LeanAPAP.Prereqs.Convolution.ThreeAP -import LeanAPAP.Prereqs.Curlog import LeanAPAP.Prereqs.LargeSpec import LeanAPAP.Physics.AlmostPeriodicity import LeanAPAP.Physics.Unbalancing @@ -19,17 +18,38 @@ 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} {γ ε : ℝ} + [DiscreteMeasurableSpace G] {A C : Finset G} {x γ ε : ℝ} + +local notation "𝓛" x:arg => 1 + log x⁻¹ + +private lemma curlog_pos (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : 0 < 𝓛 x := by + obtain rfl | hx₀ := hx₀.eq_or_lt + · simp + have : 0 ≤ log x⁻¹ := log_nonneg $ one_le_inv (by positivity) hx₁ + positivity + +private lemma rpow_inv_neg_curlog_le (hx₀ : 0 ≤ x) (hx₁ : x ≤ 1) : x⁻¹ ^ (𝓛 x)⁻¹ ≤ exp 1 := by + obtain rfl | hx₀ := hx₀.eq_or_lt + · simp; positivity + obtain rfl | hx₁ := hx₁.eq_or_lt + · simp + have hx := one_lt_inv hx₀ hx₁ + calc + x⁻¹ ^ (𝓛 x)⁻¹ ≤ x⁻¹ ^ (log x⁻¹)⁻¹ := by + gcongr + · exact hx.le + · exact log_pos hx + · 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|) : - ε / (2 * card G) ≤ - ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[↑(2 * ⌈γ.curlog⌉₊), const _ (card G)⁻¹] := by + ε / (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) - set p := 2 * ⌈γ.curlog⌉₊ + set p := 2 * ⌈𝓛 γ⌉₊ have hp : 1 < p := - Nat.succ_le_iff.1 (le_mul_of_one_le_right zero_le' $ Nat.ceil_pos.2 $ curlog_pos hγ hγ₁) + Nat.succ_le_iff.1 (le_mul_of_one_le_right zero_le' $ Nat.ceil_pos.2 $ curlog_pos hγ.le hγ₁) have hp' : (p⁻¹ : ℝ≥0) < 1 := inv_lt_one $ mod_cast hp have hp'' : (p : ℝ≥0).IsConjExponent _ := .conjExponent $ mod_cast hp rw [mul_comm, ← div_div, div_le_iff₀ (zero_lt_two' ℝ)] @@ -41,7 +61,7 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ) _ ≤ ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[p] * (card G ^ (-(p : ℝ)⁻¹) * γ ^ (-(p : ℝ)⁻¹)) := mul_le_mul (dLpNorm_conv_le_dLpNorm_dconv' (by positivity) (even_two_mul _) _) ?_ (by positivity) (by positivity) - _ = ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[↑(2 * ⌈γ.curlog⌉₊), const _ (card G)⁻¹] * + _ = ‖balance (μ_[ℝ] A) ○ balance (μ A)‖_[↑(2 * ⌈𝓛 γ⌉₊), const _ (card G)⁻¹] * γ ^ (-(p : ℝ)⁻¹) := ?_ _ ≤ _ := mul_le_mul_of_nonneg_left ?_ $ by positivity · rw [← balance_conv, balance, dL2Inner_sub_left, dL2Inner_const_left, expect_conv, sum_mu ℝ hA, @@ -55,14 +75,18 @@ lemma global_dichotomy (hA : A.Nonempty) (hγC : γ ≤ C.dens) (hγ : 0 < γ) congr any_goals positivity exact ENNReal.natCast_ne_top _ - · dsimp [p] - push_cast - norm_num - rw [← neg_mul, rpow_mul, one_div, rpow_inv_le_iff_of_pos] - exact (rpow_le_rpow_of_exponent_ge hγ hγ₁ $ neg_le_neg $ - inv_le_inv_of_le (curlog_pos hγ hγ₁) $ Nat.le_ceil _).trans $ - (rpow_neg_inv_curlog_le hγ.le hγ₁).trans $ exp_one_lt_d9.le.trans $ by norm_num - all_goals positivity + · have : 1 ≤ γ⁻¹ := one_le_inv hγ hγ₁ + have : 0 ≤ log γ⁻¹ := log_nonneg this + calc + γ ^ (-(↑p)⁻¹ : ℝ) = √(γ⁻¹ ^ ((↑⌈1 + log γ⁻¹⌉₊)⁻¹ : ℝ)) := by + rw [rpow_neg hγ.le, inv_rpow hγ.le] + unfold_let p + push_cast + rw [mul_inv_rev, rpow_mul, sqrt_eq_rpow, one_div, inv_rpow] <;> positivity + _ ≤ √(γ⁻¹ ^ ((1 + log γ⁻¹)⁻¹ : ℝ)) := by gcongr; assumption; exact Nat.le_ceil _ + _ ≤ √ (exp 1) := by gcongr; exact rpow_inv_neg_curlog_le hγ.le hγ₁ + _ ≤ √ 2.7182818286 := by gcongr; exact exp_one_lt_d9.le + _ ≤ 2 := by rw [sqrt_le_iff]; norm_num variable {q n : ℕ} [Module (ZMod q) G] {A₁ A₂ : Finset G} (S : Finset G) {α : ℝ} @@ -71,7 +95,7 @@ lemma ap_in_ff (hS : S.Nonempty) (hα₀ : 0 < α) (hε₀ : 0 < ε) (hε₁ : ∃ (V : Submodule (ZMod q) G) (V' : Finset G), (V : Set G) = V' ∧ ↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤ - 2 ^ 27 * α.curlog ^ 2 * (ε * α).curlog ^ 2 / ε ^ 2 ∧ + 2 ^ 27 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 / ε ^ 2 ∧ |∑ x in S, (μ V' ∗ μ A₁ ∗ μ A₂) x - ∑ x in S, (μ A₁ ∗ μ A₂) x| ≤ ε := by classical have hA₁ : A₁.Nonempty := by simpa using hα₀.trans_le hαA₁ @@ -81,7 +105,7 @@ lemma ap_in_ff (hS : S.Nonempty) (hα₀ : 0 < α) (hε₀ : 0 < ε) (hε₁ : _ ≤ (A₁.dens⁻¹ : ℝ) := by norm_cast; exact addConst_le_inv_dens _ ≤ α⁻¹ := by gcongr obtain ⟨T, hST, hT⟩ := AlmostPeriodicity.linfty_almost_periodicity_boosted ε hε₀ hε₁ - ⌈(ε * α / 4).curlog⌉₊ (Nat.ceil_pos.2 $ curlog_pos (by positivity) sorry).ne' sorry hA₁ + ⌈𝓛 (ε * α / 4)⌉₊ (Nat.ceil_pos.2 $ curlog_pos (by positivity) sorry).ne' sorry hA₁ univ_nonempty S A₂ hS hA₂ let Δ := largeSpec (μ T) 2⁻¹ let V : AddSubgroup G := ⨅ γ ∈ Δ, γ.toAddMonoidHom.ker @@ -100,7 +124,7 @@ lemma di_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε < (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 * α.curlog ^ 4 * γ.curlog ^ 4 / ε ^ 24 ∧ + 2 ^ 171 * 𝓛 α ^ 4 * 𝓛 γ ^ 4 / ε ^ 24 ∧ (1 + ε / 32) * α ≤ ‖𝟭_[ℝ] A ∗ μ (Set.toFinset V)‖_[⊤] := by obtain rfl | hA := A.eq_empty_or_nonempty · stop @@ -112,7 +136,7 @@ lemma di_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε < exact ⟨by positivity, mul_nonpos_of_nonneg_of_nonpos (by positivity) hαA⟩ have hγ₁ : γ ≤ 1 := hγC.trans (by norm_cast; exact dens_le_one) have hG : (card G : ℝ) ≠ 0 := by positivity - have := unbalancing _ (mul_ne_zero two_ne_zero (Nat.ceil_pos.2 $ curlog_pos hγ hγ₁).ne') (ε / 2) + have := unbalancing _ (mul_ne_zero two_ne_zero (Nat.ceil_pos.2 $ curlog_pos hγ.le hγ₁).ne') (ε / 2) (by positivity) (div_le_one_of_le (hε₁.le.trans $ by norm_num) $ by norm_num) (const _ (card G)⁻¹) (card G • (balance (μ A) ○ balance (μ A))) (sqrt (card G) • balance (μ A)) (const _ (card G)⁻¹) ?_ ?_ ?_ ?_ @@ -127,14 +151,14 @@ lemma di_in_ff (hq₃ : 3 ≤ q) (hq : q.Prime) (hε₀ : 0 < ε) (hε₁ : ε < sorry -- simp only [Nonneg.coe_one, inv_one, rpow_one, norm_inv, norm_coe_nat, -- mul_inv_cancel₀ (show (card G : ℝ) ≠ 0 by positivity)] - · have hγ' : (1 : ℝ≥0) ≤ 2 * ⌈γ.curlog⌉₊ := sorry + · have hγ' : (1 : ℝ≥0) ≤ 2 * ⌈𝓛 γ⌉₊ := sorry sorry -- simpa [wLpNorm_nsmul hγ', ← nsmul_eq_mul, div_le_iff' (show (0 : ℝ) < card G by positivity), -- ← div_div, *] using global_dichotomy hA hγC hγ hAC 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 * curlog A.dens ^ 9 := by + (hA : ThreeAPFree (α := G) A) : finrank (ZMod q) G ≤ 2 ^ 203 * 𝓛 A.dens ^ 9 := by let n : ℝ := finrank (ZMod q) G let α : ℝ := A.dens have : 1 < (q : ℝ) := mod_cast hq₃.trans_lt' (by norm_num) @@ -145,31 +169,30 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty) have : 1 ≤ α⁻¹ := one_le_inv (by positivity) (by simp [α]) have hα₀ : 0 < α := by positivity have : 0 ≤ log α⁻¹ := log_nonneg ‹_› - have : 0 ≤ curlog α := curlog_nonneg (by positivity) (by simp [α]) + have : 0 < 𝓛 α := by positivity have : 0 < log q := log_pos ‹_› obtain hα | hα := le_total (q ^ (n / 2) : ℝ) (2 * α⁻¹ ^ 2) · rw [rpow_le_iff_le_log, log_mul, log_pow, Nat.cast_two, ← mul_div_right_comm, mul_div_assoc, ← le_div_iff₀] at hα calc _ ≤ (log 2 + 2 * log α⁻¹) / (log q / 2) := hα - _ = 4 / log q * (log α⁻¹ + log 2 / 2) := by ring - _ ≤ 2 ^ 203 * (0 + 2) ^ 8 * (log α⁻¹ + 2) := by + _ = 4 / log q * (log 2 / 2 + log α⁻¹) := by ring + _ ≤ 2 ^ 203 * (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 * (0 + 2) ^ 8 := by norm_num + _ ≤ 2 ^ 203 * (1 + 0) ^ 8 := by norm_num · calc log 2 / 2 ≤ 0.6931471808 / 2 := by gcongr; exact log_two_lt_d9.le - _ ≤ 2 := by norm_num - _ ≤ 2 ^ 203 * (log α⁻¹ + 2) ^ 8 * (log α⁻¹ + 2) := by gcongr - _ = 2 ^ 203 * curlog α ^ 9 := by - rw [curlog_eq_log_inv_add_two, pow_succ _ 8, mul_assoc]; positivity + _ ≤ 1 := by norm_num + _ ≤ 2 ^ 203 * 𝓛 α ^ 8 * 𝓛 α := by gcongr + _ = 2 ^ 203 * 𝓛 α ^ 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 * curlog α ^ 8 ∧ ThreeAPFree (B : Set V) + (B : Finset V), n ≤ finrank (ZMod q) V + 2 ^ 195 * i * 𝓛 α ^ 8 ∧ ThreeAPFree (B : Set V) ∧ α ≤ B.dens ∧ (B.dens < (65 / 64 : ℝ) ^ i * α → 2⁻¹ ≤ card V * ⟪μ B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ]) := by @@ -182,7 +205,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty) hV.trans (by gcongr; exact i.le_succ), hB, hαβ, fun _ ↦ hB'⟩ let _ : MeasurableSpace V := ⊤ have : DiscreteMeasurableSpace V := ⟨fun _ ↦ trivial⟩ - have : 0 ≤ curlog B.dens := curlog_nonneg (by positivity) (by simp) + have : 0 < 𝓛 B.dens := curlog_pos (by positivity) (by simp) have : 2⁻¹ ≤ |card V * ⟪μ B ∗ μ B, μ (B.image (2 • ·))⟫_[ℝ] - 1| := by rw [abs_sub_comm, le_abs, le_sub_comm] norm_num at hB' ⊢ @@ -198,13 +221,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 * curlog α ^ 8 := hV + n ≤ finrank (ZMod q) V + 2 ^ 195 * i * 𝓛 α ^ 8 := hV _ ≤ finrank (ZMod q) V' + ↑(finrank (ZMod q) V - finrank (ZMod q) V') + - 2 ^ 195 * i * curlog α ^ 8 := by gcongr; norm_cast; exact le_add_tsub - _ ≤ finrank (ZMod q) V' + 2 ^ 171 * curlog B.dens ^ 4 * curlog α ^ 4 / 2⁻¹ ^ 24 + - 2 ^ 195 * i * curlog α ^ 8 := by gcongr - _ ≤ finrank (ZMod q) V' + 2 ^ 171 * curlog α ^ 4 * curlog α ^ 4 / 2⁻¹ ^ 24 + - 2 ^ 195 * i * curlog α ^ 8 := by gcongr; sorry + 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 gcongr; sorry _ = _ := by push_cast; ring · exact .of_image .subtypeVal Set.injOn_subtype_val (Set.subset_univ _) (hB.vadd_set (a := -x) |>.mono $ by simp [B']) @@ -217,7 +240,7 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty) (65 / 64) ^ (i + 1) * α = (1 + 64⁻¹) * ((65 / 64) ^ i * α) := by ring _ ≤ (1 + 64⁻¹) * B.dens := by gcongr; simpa [hB'.not_le] using hBV _ ≤ B'.dens := hβ - obtain ⟨V, _, _, _, _, B, hV, hB, hαβ, hBV⟩ := ind ⌊curlog α / log (65 / 64)⌋₊ + obtain ⟨V, _, _, _, _, B, hV, hB, hαβ, hBV⟩ := ind ⌊𝓛 α / log (65 / 64)⌋₊ let β : ℝ := B.dens have aux : 0 < log (65 / 64) := log_pos (by norm_num) specialize hBV $ by @@ -228,19 +251,17 @@ theorem ff (hq₃ : 3 ≤ q) (hq : q.Prime) {A : Finset G} (hA₀ : A.Nonempty) calc log α⁻¹ / log (65 / 64) < ⌊log α⁻¹ / log (65 / 64)⌋₊ + 1 := Nat.lt_floor_add_one _ - _ = ⌊(log α⁻¹ + log (65 / 64)) / log (65 / 64)⌋₊ := by - rw [← div_add_one aux.ne', Nat.floor_add_one, Nat.cast_succ] + _ = ⌊(log (65 / 64) + log α⁻¹) / log (65 / 64)⌋₊ := by + rw [add_comm (log _), ← div_add_one aux.ne', Nat.floor_add_one, Nat.cast_succ] exact div_nonneg (log_nonneg $ one_le_inv (by positivity) (by simp [α])) aux.le - _ ≤ ⌊curlog α / log (65 / 64)⌋₊ := by - rw [curlog_eq_log_inv_add_two] + _ ≤ ⌊𝓛 α / log (65 / 64)⌋₊ := by gcongr - · calc - log (65 / 64) ≤ 65/64 - 1 := log_le_sub_one_of_pos $ by norm_num - _ ≤ 2 := by norm_num - · positivity + calc + log (65 / 64) ≤ 65/64 - 1 := log_le_sub_one_of_pos $ by norm_num + _ ≤ 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 * curlog α ^ 9) : ℝ) ≤ q ^ (n / 2) by + suffices h : (q ^ (n - 2 ^ 202 * 𝓛 α ^ 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 @@ -249,18 +270,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 * ⌊curlog α / log (65 / 64)⌋₊ * curlog α ^ 8 := by + n - finrank (ZMod q) V ≤ 2 ^ 195 * ⌊𝓛 α / log (65 / 64)⌋₊ * 𝓛 α ^ 8 := by rwa [sub_le_iff_le_add'] - _ ≤ 2 ^ 195 * (curlog α / log (65 / 64)) * curlog α ^ 8 := by + _ ≤ 2 ^ 195 * (𝓛 α / log (65 / 64)) * 𝓛 α ^ 8 := by gcongr; exact Nat.floor_le (by positivity) - _ = 2 ^ 195 * (log (65 / 64)) ⁻¹ * curlog α ^ 9 := by ring - _ ≤ 2 ^ 195 * 2 ^ 7 * curlog α ^ 9 := by + _ = 2 ^ 195 * (log (65 / 64)) ⁻¹ * 𝓛 α ^ 9 := by ring + _ ≤ 2 ^ 195 * 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 * curlog α ^ 9 := by ring + _ = 2 ^ 202 * 𝓛 α ^ 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, diff --git a/LeanAPAP/Physics/AlmostPeriodicity.lean b/LeanAPAP/Physics/AlmostPeriodicity.lean index 7d9aa25366..366dad4bab 100644 --- a/LeanAPAP/Physics/AlmostPeriodicity.lean +++ b/LeanAPAP/Physics/AlmostPeriodicity.lean @@ -89,7 +89,6 @@ open scoped BigOperators Pointwise NNReal ENNReal variable {G : Type*} [Fintype G] {A S : Finset G} {f : G → ℂ} {x ε K : ℝ} {k m : ℕ} -variable {x : ℝ} local notation "𝓛" x => 1 + log (min 1 x)⁻¹ private lemma curlog_pos (hx₀ : 0 < x) : 0 < 𝓛 x := by