Skip to content

Commit c96d796

Browse files
YaelDilliesYaelDillies
committed
Bound on the size of Δ' in ap_in_ff
Co-authored-by: dannyply <danny.plymesser@gmail.com>
1 parent be304c7 commit c96d796

8 files changed

Lines changed: 162 additions & 5 deletions

File tree

‎APAP.lean‎

Lines changed: 6 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -7,16 +7,22 @@ public import APAP.Mathlib.Algebra.BigOperators.Pi
77
public import APAP.Mathlib.Algebra.Group.Action.Pointwise.Set.Basic
88
public import APAP.Mathlib.Algebra.Group.Pointwise.Set.Basic
99
public import APAP.Mathlib.Algebra.Group.Translate
10+
public import APAP.Mathlib.Algebra.Module.AddChar
11+
public import APAP.Mathlib.Algebra.Module.ZMod
1012
public import APAP.Mathlib.Algebra.Order.Group.Parity
1113
public import APAP.Mathlib.Algebra.Star.Conjneg
1214
public import APAP.Mathlib.Algebra.Star.SelfAdjoint
1315
public import APAP.Mathlib.Analysis.Complex.Circle
1416
public import APAP.Mathlib.Analysis.Convolution
17+
public import APAP.Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
1518
public import APAP.Mathlib.Analysis.Normed.Ring.Basic
1619
public import APAP.Mathlib.Analysis.RCLike.Basic
1720
public import APAP.Mathlib.Analysis.SpecialFunctions.Complex.Circle
1821
public import APAP.Mathlib.Data.Complex.Basic
1922
public import APAP.Mathlib.Data.NNReal.Defs
23+
public import APAP.Mathlib.Data.ZMod.Basic
24+
public import APAP.Mathlib.LinearAlgebra.Dimension.Finrank
25+
public import APAP.Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
2026
public import APAP.Mathlib.MeasureTheory.Function.LpSeminorm.CompareExp
2127
public import APAP.Mathlib.Topology.Algebra.PontryaginDual
2228
public import APAP.Physics.AlmostPeriodicity

‎APAP/FiniteField.lean‎

Lines changed: 7 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -11,6 +11,7 @@ public import Mathlib.MeasureTheory.MeasurableSpace.Defs
1111

1212
import AddCombi.Mathlib.Algebra.Order.GroupWithZero.Indicator
1313
import APAP.Mathlib.Algebra.Order.Group.Parity
14+
import APAP.Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
1415
import APAP.Physics.AlmostPeriodicity
1516
import APAP.Physics.DRC
1617
import APAP.Physics.Unbalancing
@@ -189,7 +190,7 @@ public lemma ap_in_ff [DecidableEq G] (hq : q.Prime) (hα₀ : 0 < α) (hα₂ :
189190
let V : Submodule (ZMod q) G := AddSubgroup.toZModSubmodule _ <| ⨅ γ ∈ Δ, γ.toAddMonoidHom.ker
190191
let V' : Finset G := Set.toFinset V
191192
refine ⟨V, inferInstance, ?_, ?_⟩
192-
· obtain ⟨Δ', hΔ'Δ, hΔ'card, hfΔ'⟩ : ∃ Δ' ⊆ Δ, _ := chang (mu_ne_zero.2 hT) (by norm_num)
193+
· obtain ⟨Δ', -, hΔ'card, hfΔ'⟩ : ∃ Δ' ⊆ Δ, _ := chang (mu_ne_zero.2 hT) (by norm_num)
193194
let W : Submodule (ZMod q) G := AddSubgroup.toZModSubmodule _ <| ⨅ γ ∈ Δ', γ.toAddMonoidHom.ker
194195
have mem_W {x} : x ∈ W ↔ ∀ γ ∈ Δ', γ x = 1 := by simp [W]
195196
have hWV : W ≤ V := by
@@ -221,10 +222,11 @@ public lemma ap_in_ff [DecidableEq G] (hq : q.Prime) (hα₀ : 0 < α) (hα₂ :
221222
_ = 2 ^ 3 * 𝓛 (ε * α) := by ring
222223
_ = 2 ^ 19 * 𝓛 α ^ 2 * 𝓛 (ε * α) ^ 2 * ε⁻¹ ^ 2 := by ring_nf
223224
calc
224-
(↑(finrank (ZMod q) G - finrank (ZMod q) V) : ℝ)
225-
≤ ↑(finrank (ZMod q) G - finrank (ZMod q) W) := by
226-
gcongr; exact Submodule.finrank_mono hWV
227-
_ ≤ #Δ' := sorry
225+
(↑(finrank (ZMod q) G - V.finrank) : ℝ)
226+
≤ ↑(finrank (ZMod q) G - W.finrank) := by gcongr; exact Submodule.finrank_mono hWV
227+
_ ≤ #Δ' := by
228+
let : Fact q.Prime := ⟨hq⟩
229+
simpa [W] using AddChar.codim_iInf_ker_le_finsetCard (s := Δ')
228230
_ ≤ ⌈changConst * exp 1 * ⌈𝓛 ↑(‖μ T‖_[1] ^ 2 / ‖μ T‖_[2] ^ 2 / card G)⌉₊ / 2⁻¹ ^ 2⌉₊ := by
229231
gcongr
230232
_ = ⌈2 ^ 7 * exp 1 ^ 2 * ⌈𝓛 T.dens⌉₊⌉₊ := by

‎APAP/Mathlib/Algebra/Module/AddChar.lean‎

Lines changed: 23 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,23 @@
1+
module
2+
3+
public import Mathlib.Algebra.Group.AddChar
4+
public import Mathlib.Algebra.Module.Defs
5+
6+
public section
7+
8+
namespace AddChar
9+
variable {R M N : Type*} [CommMonoid M] [Semiring R] [AddCommMonoid N] [Module R N]
10+
11+
/-- Interpret a character of the `R`-module `N` as a homomorphism from `N` to character of `R`,
12+
via precomposition by scalar multiplication. -/
13+
@[expose, simps]
14+
def toAddMonoidHomAddChar (γ : AddChar N M) : N →+ AddChar R M where
15+
toFun x := {
16+
toFun r := γ (r • x)
17+
map_zero_eq_one' := by simp
18+
map_add_eq_mul' r s := by simp [add_smul, map_add_eq_mul]
19+
}
20+
map_zero' := by ext; simp
21+
map_add' x y := by ext; simp [map_add_eq_mul, smul_add]
22+
23+
end AddChar

‎APAP/Mathlib/Algebra/Module/ZMod.lean‎

Lines changed: 20 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,20 @@
1+
module
2+
3+
public import APAP.Mathlib.Data.ZMod.Basic
4+
public import Mathlib.Algebra.Group.AddChar
5+
public import Mathlib.Algebra.Module.ZMod
6+
7+
public section
8+
9+
namespace AddChar
10+
variable {R M : Type*} [Semiring R] {q : ℕ} [AddCommMonoid M] [Module (ZMod q) M] {γ : AddChar M R}
11+
{r : ZMod q} {x : M}
12+
13+
variable (γ r x) in
14+
lemma map_zmod_smul [NeZero q] : γ (r • x) = γ x ^ r.val := by
15+
obtain _ | q := q
16+
· simp_all
17+
obtain ⟨n, hn⟩ := r
18+
simp [Nat.cast_smul_eq_nsmul, map_nsmul_eq_pow]
19+
20+
end AddChar

‎APAP/Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean‎

Lines changed: 50 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,50 @@
1+
module
2+
3+
public import APAP.Mathlib.Algebra.Module.AddChar
4+
public import APAP.Mathlib.Algebra.Module.ZMod
5+
public import APAP.Mathlib.LinearAlgebra.Dimension.Finrank
6+
public import Mathlib.Analysis.Fourier.FiniteAbelian.PontryaginDuality
7+
public import Mathlib.Algebra.Field.ZMod
8+
9+
import APAP.Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
10+
11+
public section
12+
13+
open scoped Finset
14+
15+
namespace AddChar
16+
variable {ι G : Type*} {q : ℕ} [AddCommGroup G] [Module (ZMod q) G] {γ : AddChar G ℂ}
17+
{r : ZMod q} {x : G}
18+
19+
variable (q γ) in
20+
/-- Characters of a `q`-group `G` are (noncanonically) the same as `ZMod q`-linear forms on `G`. -/
21+
@[expose, simps! -isSimp]
22+
noncomputable def toZModLinearMap [NeZero q] : G →ₗ[ZMod q] ZMod q :=
23+
(zmodAddEquiv.symm.toAddMonoidHom.comp <| γ.toAddMonoidHomAddChar).toZModLinearMap q
24+
25+
@[simp]
26+
lemma toZModLinearMap_eq_zero [Fact <| 1 < q] : toZModLinearMap q γ x = 0 ↔ γ x = 1 := by
27+
simp +contextual only [toZModLinearMap_apply, EmbeddingLike.map_eq_zero_iff, DFunLike.ext_iff,
28+
toAddMonoidHomAddChar_apply_apply, map_zmod_smul, zero_apply, iff_iff_implies_and_implies,
29+
one_pow, implies_true, and_true]
30+
rintro h
31+
simpa [ZMod.val_one] using h 1
32+
33+
@[simp]
34+
lemma ker_toZModLinearMap [Fact <| 1 < q] :
35+
(toZModLinearMap q γ).ker = γ.toAddMonoidHom.ker.toZModSubmodule q := by ext; simp
36+
37+
variable [Fact q.Prime] [FiniteDimensional (ZMod q) G] {γ : ι → AddChar G ℂ}
38+
{s : Finset ι}
39+
40+
lemma codim_iInf_ker_le_fintypeCard [Fintype ι] :
41+
Module.finrank (ZMod q) G - (⨅ i, (γ i).toAddMonoidHom.ker.toZModSubmodule q).finrank
42+
≤ Fintype.card ι := by
43+
simpa using Module.codim_iInf_ker_le_fintypeCard (f := fun i ↦ (γ i).toZModLinearMap q)
44+
45+
lemma codim_iInf_ker_le_finsetCard :
46+
Module.finrank (ZMod q) G - ((⨅ i ∈ s, (γ i).toAddMonoidHom.ker).toZModSubmodule q).finrank
47+
≤ #s := by
48+
simpa [iInf_subtype] using codim_iInf_ker_le_fintypeCard (ι := s) (γ := fun i ↦ γ i)
49+
50+
end AddChar

‎APAP/Mathlib/Data/ZMod/Basic.lean‎

Lines changed: 17 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,17 @@
1+
module
2+
3+
public import Mathlib.Data.ZMod.Basic
4+
5+
public section
6+
7+
namespace ZMod
8+
variable {M : Type*} {q : ℕ}
9+
10+
-- FIXME: The LHS has type `Fin (q + 1)`. See
11+
@[simp↓] lemma val_mk (n : ℕ) (hn) : val (n := q + 1) (⟨n, hn⟩ : ZMod (q + 1)) = n := rfl
12+
13+
-- FIXME: The LHS has type `Fin (q + 1)`. See
14+
@[simp] lemma mk_eq_natCast (n : ℕ) (hn) : ⟨n, hn⟩ = (n : ZMod (q + 1)) :=
15+
(Fin.natCast_eq_mk _).symm
16+
17+
end ZMod

‎APAP/Mathlib/LinearAlgebra/Dimension/Finrank.lean‎

Lines changed: 9 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,9 @@
1+
module
2+
3+
public import Mathlib.LinearAlgebra.Dimension.Finrank
4+
5+
public section
6+
7+
@[expose]
8+
noncomputable def Submodule.finrank {R M : Type*} [Semiring R] [AddCommMonoid M] [Module R M]
9+
(s : Submodule R M) : ℕ := Module.finrank R s

‎APAP/Mathlib/LinearAlgebra/FiniteDimensional/Lemmas.lean‎

Lines changed: 30 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,30 @@
1+
module
2+
3+
public import APAP.Mathlib.LinearAlgebra.Dimension.Finrank
4+
public import Mathlib.LinearAlgebra.FiniteDimensional.Lemmas
5+
6+
public section
7+
8+
open scoped Finset
9+
10+
variable {K V ι : Type*}
11+
[DivisionRing K] [AddCommGroup V] [Module K V] [FiniteDimensional K V]
12+
{s : Finset ι} {f : ι → V →ₗ[K] K}
13+
14+
namespace Module
15+
16+
lemma codim_iInf_ker_le_fintypeCard [Fintype ι] :
17+
finrank K V - (⨅ i, (f i).ker).finrank ≤ Fintype.card ι := by
18+
let F : V →ₗ[K] (ι → K) := {
19+
toFun x i := f i x
20+
map_add' x y := by ext i; simp
21+
map_smul' c x := by ext i; simp
22+
}
23+
have hker : F.ker = ⨅ i, (f i).ker := by ext x; simp [F, funext_iff]
24+
grw [← hker, ← F.finrank_range_add_finrank_ker, Submodule.finrank_le]
25+
simp [Submodule.finrank]
26+
27+
lemma codim_biInf_ker_le_finsetCard : finrank K V - (⨅ i ∈ s, (f i).ker).finrank ≤ #s := by
28+
simpa [iInf_subtype] using codim_iInf_ker_le_fintypeCard (ι := s) (f := fun i ↦ f i)
29+
30+
end Module

0 commit comments

Comments
 (0)