From bd2be03acc45083cefba9b2469dc41bd8e3b27fd Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Ya=C3=ABl=20Dillies?= Date: Thu, 5 Sep 2024 18:18:31 +0000 Subject: [PATCH] Disparate progress on `di_in_ff` --- LeanAPAP.lean | 2 + LeanAPAP/FiniteField/Basic.lean | 89 ++++++++++--------- .../Mathlib/Algebra/Order/Ring/Basic.lean | 3 + LeanAPAP/Mathlib/Data/ENNReal/Real.lean | 3 + LeanAPAP/Physics/Unbalancing.lean | 48 ++++++---- LeanAPAP/Prereqs/Function/Indicator/Defs.lean | 3 + LeanAPAP/Prereqs/LpNorm/Weighted.lean | 1 + 7 files changed, 91 insertions(+), 58 deletions(-) create mode 100644 LeanAPAP/Mathlib/Algebra/Order/Ring/Basic.lean create mode 100644 LeanAPAP/Mathlib/Data/ENNReal/Real.lean diff --git a/LeanAPAP.lean b/LeanAPAP.lean index 133e504444..12fbdfc180 100644 --- a/LeanAPAP.lean +++ b/LeanAPAP.lean @@ -7,12 +7,14 @@ import LeanAPAP.Mathlib.Algebra.Order.Floor import LeanAPAP.Mathlib.Algebra.Order.Group.Unbundled.Basic import LeanAPAP.Mathlib.Algebra.Order.GroupWithZero.Unbundled import LeanAPAP.Mathlib.Algebra.Order.Module.Rat +import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic import LeanAPAP.Mathlib.Algebra.Star.Rat import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Complex.CircleAddChar import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.NNReal import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Pow.Real import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom +import LeanAPAP.Mathlib.Data.ENNReal.Real import LeanAPAP.Mathlib.Data.Finset.Pointwise.Basic import LeanAPAP.Mathlib.Data.Finset.Preimage import LeanAPAP.Mathlib.MeasureTheory.Function.EssSup diff --git a/LeanAPAP/FiniteField/Basic.lean b/LeanAPAP/FiniteField/Basic.lean index ad26f49d97..696a67bfce 100644 --- a/LeanAPAP/FiniteField/Basic.lean +++ b/LeanAPAP/FiniteField/Basic.lean @@ -1,6 +1,5 @@ import Mathlib.FieldTheory.Finite.Basic -import LeanAPAP.Mathlib.Algebra.Order.Floor -import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic +import LeanAPAP.Mathlib.Algebra.Order.Ring.Basic import LeanAPAP.Mathlib.Combinatorics.Additive.FreimanHom import LeanAPAP.Mathlib.Data.Finset.Preimage import LeanAPAP.Prereqs.Convolution.ThreeAP @@ -174,58 +173,51 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q) have hG : (card G : ℝ) ≠ 0 := by positivity let α : ℝ := A.dens let p : ℕ := 2 * ⌈𝓛 γ⌉₊ - let p' : ℝ := 240 / ε * log (6 / ε) * p - let q' : ℕ := 2 * ⌈p' + 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊ let f : G → ℝ := balance (μ A) - have : 0 < 𝓛 γ := curlog_pos hγ.le hγ₁ obtain rfl | hA₀ := A.eq_empty_or_nonempty · exact ⟨⊤, Classical.decPred _, by simp; positivity⟩ + obtain ⟨p', hp', unbalancing⟩ : + ∃ p' : ℕ, p' ≤ 2 ^ 10 * (ε / 2)⁻¹ ^ 2 * p ∧ + 1 + ε / 2 / 2 ≤ card G ^ (-(p'⁻¹ : ℝ)) * ‖card G • (f ○ f) + 1‖_[p'] := by + refine 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) + (card G • (balance (μ A) ○ balance (μ A))) (sqrt (card G) • balance (μ A)) + (const _ (card G)⁻¹) ?_ ?_ ?_ + · ext a : 1 + simp [smul_dconv, dconv_smul, smul_smul, ← mul_assoc, ← sq, ← Complex.ofReal_pow] + · simp [card_univ] + · have global_dichotomy := global_dichotomy hA₀ hγC hγ hAC + rw [wLpNorm_const_right (ENNReal.natCast_ne_top _)] at global_dichotomy + simpa [dLpNorm_nsmul, ← nsmul_eq_mul, div_le_iff₀' (show (0 : ℝ) < card G by positivity), + ← div_div, rpow_neg, inv_rpow] using global_dichotomy + let q' : ℕ := 2 * ⌈p' + 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊ + have : 0 < 𝓛 γ := curlog_pos hγ.le hγ₁ have hα₀ : 0 < α := by positivity have hα₁ : α ≤ 1 := by unfold_let α; exact mod_cast A.dens_le_one 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 < p' := pos_iff_ne_zero.2 $ by rintro rfl; simp at unbalancing; linarith have : 0 < log (64 / ε) := log_pos $ (one_lt_div hε₀).2 (by linarith) - have : 0 < q' := by positivity have : 1 ≤ 𝓛 γ := one_le_curlog hγ.le hγ₁ + have : 0 < q' := by positivity + have : 1 ≤ ε⁻¹ := one_le_inv hε₀ hε₁.le have := calc - (q' : ℝ) - = 2 * ⌈480 * ε⁻¹ ^ 1 * log (6 * ε⁻¹) * ⌈𝓛 γ⌉₊ + - 2 ^ 8 * ε⁻¹ ^ 2 * log (2 ^ 6 * ε⁻¹) * 1⌉₊ := by unfold_let q' p' p; push_cast; ring_nf - _ ≤ 2 * ⌈2 ^ 10 * ε⁻¹ ^ 2 * (2 ^ 3 * ε⁻¹) * (2 * 𝓛 γ) + - 2 ^ 8 * ε⁻¹ ^ 2 * (2 ^ 6 * ε⁻¹) * 𝓛 γ⌉₊ := by + (q' : ℝ) ≤ ↑(2 * ⌈2 ^ 10 * (ε / 2)⁻¹ ^ 2 * p + 2 ^ 8 * ε⁻¹ ^ 2 * (64 / ε)⌉₊) := by + unfold_let q'; gcongr; exact log_le_self (by positivity) + _ = 2 * ⌈2 ^ 13 * ε⁻¹ ^ 2 * ⌈𝓛 γ⌉₊ + 2 ^ 14 * ε⁻¹ ^ 3 * 1⌉₊ := by + unfold_let p; push_cast; ring_nf + _ ≤ 2 * ⌈2 ^ 13 * ε⁻¹ ^ 3 * (2 * 𝓛 γ) + 2 ^ 14 * ε⁻¹ ^ 3 * 𝓛 γ⌉₊ := by gcongr + · assumption · norm_num - · exact one_le_inv hε₀ hε₁.le - · norm_num - · calc - log (6 * ε⁻¹) ≤ 6 * ε⁻¹ := log_le_self (by positivity) - _ ≤ 2 ^ 3 * ε⁻¹ := by gcongr; norm_num - · exact (Nat.ceil_lt_two_mul $ one_le_curlog hγ.le hγ₁).le - · exact log_le_self (by positivity) + · exact (Nat.ceil_lt_two_mul ‹_›).le _ = 2 * ⌈2 ^ 15 * ε⁻¹ ^ 3 * 𝓛 γ⌉₊ := by ring_nf _ ≤ 2 * (2 * (2 ^ 15 * ε⁻¹ ^ 3 * 𝓛 γ)) := by - gcongr; exact (Nat.ceil_lt_two_mul $ one_le_mul_of_one_le_of_one_le - (one_le_mul_of_one_le_of_one_le (by norm_num) sorry) ‹_›).le + gcongr + exact (Nat.ceil_lt_two_mul $ one_le_mul_of_one_le_of_one_le (one_le_mul_of_one_le_of_one_le + (by norm_num) $ one_le_pow₀ (one_le_inv hε₀ hε₁.le) _) ‹_›).le _ = 2 ^ 17 * 𝓛 γ / ε ^ 3 := by ring - have global_dichotomy := global_dichotomy hA₀ hγC hγ hAC - have := - calc - 1 + ε / 4 = 1 + ε / 2 / 2 := by ring - _ ≤ _ := by - refine 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) - (card G • (balance (μ A) ○ balance (μ A))) (sqrt (card G) • balance (μ A)) - (const _ (card G)⁻¹) ?_ ?_ ?_ - · ext a : 1 - simp [smul_dconv, dconv_smul, smul_smul, ← mul_assoc, ← sq, ← Complex.ofReal_pow] - · simp [card_univ] - · rw [wLpNorm_const_right (ENNReal.natCast_ne_top _)] at global_dichotomy - simpa [dLpNorm_nsmul, ← nsmul_eq_mul, div_le_iff₀' (show (0 : ℝ) < card G by positivity), - ← div_div, rpow_neg, inv_rpow] using global_dichotomy - _ = card G ^ (-(↑p')⁻¹ : ℝ) * ‖card G • (f ○ f) + 1‖_[.ofReal p'] := by - congr 3 <;> ring_nf; simp [hε₀.ne']; ring obtain ⟨A₁, A₂, hA, hA₁, hA₂⟩ : ∃ (A₁ A₂ : Finset G), 1 - ε / 32 ≤ ∑ x ∈ s q' (ε / 16) univ univ A, (μ A₁ ○ μ A₂) x ∧ (4⁻¹ : ℝ) * A.dens ^ (2 * q') ≤ A₁.dens ∧ (4⁻¹ : ℝ) * A.dens ^ (2 * q') ≤ A₂.dens := @@ -241,9 +233,26 @@ lemma di_in_ff [MeasurableSpace G] [DiscreteMeasurableSpace G] (hq₃ : 3 ≤ q) · norm_num _ ≤ ⌈2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊ := Nat.le_ceil _ _ = ↑(1 * ⌈0 + 2 ^ 8 * ε⁻¹ ^ 2 * log (64 / ε)⌉₊) := by rw [one_mul, zero_add] - _ ≤ q' := by unfold_let q'; gcongr; norm_num) hA₀ + _ ≤ q' := by unfold_let q'; gcongr; norm_num; positivity) hA₀ + have := + calc + p' = 1 * ⌈(p' + 0 : ℝ)⌉₊ := by simp + _ ≤ q' := by unfold_let q'; gcongr; norm_num; positivity + have : card G • (f ○ f) + 1 = card G • (μ A ○ μ A) := by + unfold_let f + rw [← balance_dconv, balance, smul_sub, smul_const, Fintype.card_smul_expect] + sorry + have := + calc + 1 + ε / 4 = 1 + ε / 2 / 2 := by ring + _ ≤ card G ^ (-(↑p')⁻¹ : ℝ) * ‖card G • (f ○ f) + 1‖_[p'] := unbalancing + _ = card G ^ (-(↑p')⁻¹ : ℝ) * ‖card G • (μ_[ℝ] A ○ μ A)‖_[p'] := by congr + _ ≤ card G ^ (-(↑p')⁻¹ : ℝ) * ‖card G • (μ_[ℝ] A ○ μ A)‖_[q'] := by gcongr let s' : Finset G := {x | 1 + ε / 8 ≤ card G • (μ A ○ μ A) x} - have hss' : s q' (ε / 16) univ univ A ⊆ s' := sorry + have hss' : s q' (ε / 16) univ univ A ⊆ s' := by + simp only [nsmul_eq_mul, subset_iff, mem_s, ENNReal.coe_natCast, mu_univ_dconv_mu_univ, + mem_filter, mem_univ, true_and, s'] + sorry obtain ⟨V, _, hVdim, hV⟩ : ∃ (V : Submodule (ZMod q) G) (_ : DecidablePred (· ∈ V)), ↑(finrank (ZMod q) G - finrank (ZMod q) V) ≤ 2 ^ 27 * 𝓛 (4⁻¹ * α ^ (2 * q')) ^ 2 * 𝓛 (ε / 32 * (4⁻¹ * α ^ (2 * q'))) ^ 2 / (ε / 32) ^ 2 ∧ diff --git a/LeanAPAP/Mathlib/Algebra/Order/Ring/Basic.lean b/LeanAPAP/Mathlib/Algebra/Order/Ring/Basic.lean new file mode 100644 index 0000000000..d13893bb83 --- /dev/null +++ b/LeanAPAP/Mathlib/Algebra/Order/Ring/Basic.lean @@ -0,0 +1,3 @@ +import Mathlib.Algebra.Order.Ring.Basic + +alias one_le_pow₀ := one_le_pow_of_one_le diff --git a/LeanAPAP/Mathlib/Data/ENNReal/Real.lean b/LeanAPAP/Mathlib/Data/ENNReal/Real.lean new file mode 100644 index 0000000000..f72528d6e4 --- /dev/null +++ b/LeanAPAP/Mathlib/Data/ENNReal/Real.lean @@ -0,0 +1,3 @@ +import Mathlib.Data.ENNReal.Real + +attribute [norm_cast] ENNReal.ofReal_le_natCast diff --git a/LeanAPAP/Physics/Unbalancing.lean b/LeanAPAP/Physics/Unbalancing.lean index dbcfbaed9d..544ab3068b 100644 --- a/LeanAPAP/Physics/Unbalancing.lean +++ b/LeanAPAP/Physics/Unbalancing.lean @@ -1,5 +1,8 @@ import Mathlib.Algebra.Order.Group.PosPart import Mathlib.Data.Complex.ExponentialBounds +import LeanAPAP.Mathlib.Algebra.Order.Floor +import LeanAPAP.Mathlib.Analysis.SpecialFunctions.Log.Basic +import LeanAPAP.Mathlib.Data.ENNReal.Real import LeanAPAP.Prereqs.Convolution.Discrete.Defs import LeanAPAP.Prereqs.Inner.Discrete.Defs import LeanAPAP.Prereqs.LpNorm.Weighted @@ -201,39 +204,48 @@ transform. -/ lemma unbalancing' (p : ℕ) (hp : p ≠ 0) (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (ν : G → ℝ≥0) (f : G → ℝ) (g h : G → ℂ) (hf : (↑) ∘ f = g ○ g) (hν : (↑) ∘ ν = h ○ h) (hν₁ : ‖((↑) ∘ ν : G → ℝ)‖_[1] = 1) (hε : ε ≤ ‖f‖_[p, ν]) : - 1 + ε / 2 ≤ ‖f + 1‖_[.ofReal (120 / ε * log (3 / ε) * p), ν] := by + ∃ p' : ℕ, p' ≤ 2 ^ 10 * ε⁻¹ ^ 2 * p ∧ 1 + ε / 2 ≤ ‖f + 1‖_[p', ν] := by have := log_ε_pos hε₀ hε₁ have := calc 5 = 2 * 1 + 3 := by norm_num _ ≤ 2 * p + 3 := add_le_add_right (mul_le_mul_left' (Nat.one_le_iff_ne_zero.2 hp) _) _ + rw [← Nat.one_le_iff_ne_zero] at hp + refine ⟨⌈120 / ε * log (3 / ε) * p⌉₊, ?_, ?_⟩ + · calc + (⌈120 / ε * log (3 / ε) * p⌉₊ : ℝ) + = ⌈120 * ε⁻¹ * log (3 * ε⁻¹) * p⌉₊ := by simp [div_eq_mul_inv] + _ ≤ 2 * (120 * ε⁻¹ * log (3 * ε⁻¹) * p) := + (Nat.ceil_lt_two_mul $ one_le_mul_of_one_le_of_one_le + (one_le_mul_of_one_le_of_one_le (one_le_mul_of_one_le_of_one_le (by norm_num) $ + one_le_inv hε₀ hε₁) $ sorry) $ by simpa [Nat.one_le_iff_ne_zero]).le + _ ≤ 2 * (120 * ε⁻¹ * (3 * ε⁻¹) * p) := by gcongr; exact Real.log_le_self (by positivity) + _ ≤ 2 * (2 ^ 7 * ε⁻¹ * (2 ^ 2 * ε⁻¹) * p) := by gcongr <;> norm_num + _ = 2 ^ 10 * ε⁻¹ ^ 2 * p := by ring calc _ ≤ ↑‖f + 1‖_[.ofReal (24 / ε * log (3 / ε) * ↑(2 * p + 3)), ν] := unbalancing'' (2 * p + 3) this ((even_two_mul _).add_odd $ by decide) hε₀ hε₁ hf hν hν₁ $ - hε.trans $ - wLpNorm_mono_right - (Nat.cast_le.2 $ le_add_of_le_left $ le_mul_of_one_le_left' one_le_two) _ _ + hε.trans $ wLpNorm_mono_right + (Nat.cast_le.2 $ le_add_of_le_left $ le_mul_of_one_le_left' one_le_two) _ _ _ ≤ _ := wLpNorm_mono_right ?_ _ _ - rw [← Nat.one_le_iff_ne_zero] at hp - gcongr ENNReal.ofReal ?_ + norm_cast calc _ = 24 / ε * log (3 / ε) * ↑(2 * p + 3 * 1) := by simp _ ≤ 24 / ε * log (3 / ε) * ↑(2 * p + 3 * p) := by gcongr - _ = _ := by push_cast; ring + _ = 120 / ε * log (3 / ε) * p := by push_cast; ring + _ ≤ ⌈120 / ε * log (3 / ε) * p⌉₊ := Nat.le_ceil _ /-- The unbalancing step. Note that we do the physical proof in order to avoid the Fourier transform. -/ lemma unbalancing (p : ℕ) (hp : p ≠ 0) (ε : ℝ) (hε₀ : 0 < ε) (hε₁ : ε ≤ 1) (f : G → ℝ) (g h : G → ℂ) (hf : (↑) ∘ f = g ○ g) (hh : ∀ x, (h ○ h) x = (card G : ℝ)⁻¹) - (hε : ε ≤ (card G) ^ (-(↑p)⁻¹ : ℝ) * ‖f‖_[p]) : - 1 + ε / 2 ≤ card G ^ (-(ε / 120 * (log (3 / ε))⁻¹ * (↑p)⁻¹)) * - ‖f + 1‖_[.ofReal (120 / ε * log (3 / ε) * p)] := - calc - 1 + ε / 2 ≤ ‖f + 1‖_[.ofReal (120 / ε * log (3 / ε) * p), const _ (card G)⁻¹] := - unbalancing' p hp ε hε₀ hε₁ _ _ g h hf (funext fun x ↦ (hh x).symm) - (by simp; simp [← const_def]) (by simpa [rpow_neg, inv_rpow] using hε) - _ ≤ _ := by - have : 0 ≤ log (3 / ε) := log_nonneg $ (one_le_div hε₀).2 (by linarith) - have : 0 ≤ 120 / ε * log (3 / ε) * p := by positivity - simp [*, inv_rpow, ← rpow_neg, -mul_inv_rev, mul_inv] + (hε : ε ≤ card G ^ (-(↑p)⁻¹ : ℝ) * ‖f‖_[p]) : + ∃ p' : ℕ, p' ≤ 2 ^ 10 * ε⁻¹ ^ 2 * p ∧ 1 + ε / 2 ≤ card G ^ (-(p'⁻¹ : ℝ)) * ‖f + 1‖_[p'] := by + obtain ⟨p', hp', h⟩ : + ∃ p' : ℕ, p' ≤ 2 ^ 10 * ε⁻¹ ^ 2 * p ∧ 1 + ε / 2 ≤ ‖f + 1‖_[p', const _ (card G)⁻¹] := + unbalancing' p hp ε hε₀ hε₁ _ _ g h hf (funext fun x ↦ (hh x).symm) + (by simp; simp [← const_def]) (by simpa [rpow_neg, inv_rpow] using hε) + refine ⟨p', hp', h.trans ?_⟩ + have : 0 ≤ log (3 / ε) := log_nonneg $ (one_le_div hε₀).2 (by linarith) + simp [*, inv_rpow, ← rpow_neg, -mul_inv_rev, mul_inv] diff --git a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean index 183a320ff4..c10f4195af 100644 --- a/LeanAPAP/Prereqs/Function/Indicator/Defs.lean +++ b/LeanAPAP/Prereqs/Function/Indicator/Defs.lean @@ -148,6 +148,9 @@ lemma mu_apply (x : α) : μ s x = (s.card : β)⁻¹ * ite (x ∈ s) 1 0 := rfl lemma map_mu (f : β →+* γ) (s : Finset α) (x : α) : f (μ s x) = μ s x := by simp_rw [mu, Pi.smul_apply, smul_eq_mul, map_mul, map_indicate, map_inv₀, map_natCast] +lemma mu_univ_eq_const [Fintype α] : μ_[β] (univ : Finset α) = const _ (card α : β)⁻¹ := by + ext; simp [mu] + section Nontrivial variable [CharZero β] {a : α} diff --git a/LeanAPAP/Prereqs/LpNorm/Weighted.lean b/LeanAPAP/Prereqs/LpNorm/Weighted.lean index fbe3ea1ce0..cf87533a4f 100644 --- a/LeanAPAP/Prereqs/LpNorm/Weighted.lean +++ b/LeanAPAP/Prereqs/LpNorm/Weighted.lean @@ -108,6 +108,7 @@ lemma wL1Norm_eq_sum_nnnorm (w : α → ℝ≥0) (f : α → E) : ‖f‖_[1, w] lemma wL1Norm_eq_sum_norm (w : α → ℝ≥0) (f : α → E) : ‖f‖_[1, w] = ∑ i, w i • ‖f i‖ := by simp [wLpNorm_eq_sum_norm] +@[gcongr] lemma wLpNorm_mono_right (hpq : p ≤ q) (w : α → ℝ≥0) (f : α → E) : ‖f‖_[p, w] ≤ ‖f‖_[q, w] := sorry