DyadicCounts.lean

1 import PaperXI.DyadicGauss
2 import Mathlib.Algebra.BigOperators.Group.Finset.Piecewise
3 import Mathlib.Tactic
4 
5 /-! Exact counts for binary quadratic coefficient spaces. -/
6 set_option autoImplicit false
7 noncomputable section
8 open scoped BigOperators Classical
9 namespace PaperXI.DyadicCounts
10 
11 variable {α : Type*} [Fintype α]
12 
13 theorem signed_sum_eq_card_difference (p : α → Prop) [DecidablePred p] :
14     (∑ x, if p x then (1 : ℤ) else -1) =
15       ((Finset.univ.filter p).card : ℤ) - (Finset.univ.filter fun x => ¬ p x).card := by
16   rw [Finset.sum_ite]
17   simp [sub_eq_add_neg]
18 
19 theorem card_partition (p : α → Prop) [DecidablePred p] :
20     (Finset.univ.filter p).card + (Finset.univ.filter fun x => ¬ p x).card =
21       Fintype.card α := by
22   simpa using (Finset.card_filter_add_card_filter_not (s := Finset.univ) p)
23 
24 open PaperXI.Dyadic
25 variable {ι : Type*} [Fintype ι]
26 
27 def evenCount (ι : Type*) [Fintype ι] : ℕ :=
28   (Finset.univ.filter fun a : ι → F2 × F2 => arf a = 0).card
29 
30 def oddCount (ι : Type*) [Fintype ι] : ℕ :=
31   (Finset.univ.filter fun a : ι → F2 × F2 => arf a = 1).card
32 
33 theorem f2_ne_zero_iff_eq_one (t : F2) : t ≠ 0 ↔ t = 1 := by
34   constructor
35   · intro h
36     apply Fin.ext
37     change Fin.val t = 1
38     have hn : Fin.val t ≠ 0 := by
39       intro hz
40       apply h
41       apply Fin.ext
42       exact hz
43     exact Nat.le_antisymm (Nat.le_of_lt_succ (Fin.isLt t)) (Nat.pos_of_ne_zero hn)
44   · intro h hz
45     exact zero_ne_one (hz.symm.trans h)
46 
47 theorem parameter_card : Fintype.card (ι → F2 × F2) = 2 ^ (2 * Fintype.card ι) := by
48   simp [Fintype.card_prod, F2, ZMod.card, pow_mul]
49 
50 theorem even_add_odd : evenCount ι + oddCount ι = 2 ^ (2 * Fintype.card ι) := by
51   have h := card_partition (fun a : ι → F2 × F2 => arf a = 0)
52   simpa [evenCount, oddCount, f2_ne_zero_iff_eq_one, F2, pow_mul] using h
53 
54 theorem even_sub_odd : (evenCount ι : ℤ) - oddCount ι = 2 ^ Fintype.card ι := by
55   have h := gauss_sum (fun _ : ι => (0, 0))
56   have he : (∑ x : ι → F2 × F2, sign (arf x)) = (2 : ℤ) ^ Fintype.card ι := by
57     simpa [quadratic, plane, arf] using h
58   simp only [sign] at he
59   rw [signed_sum_eq_card_difference] at he
60   simpa [f2_ne_zero_iff_eq_one, evenCount, oddCount] using he
61 
62 /-- Unlike the factored formula, this also applies in dimension zero. -/
63 theorem twice_even : 2 * (evenCount ι : ℤ) =
64     2 ^ (2 * Fintype.card ι) + 2 ^ Fintype.card ι := by
65   have htot : (evenCount ι : ℤ) + oddCount ι = 2 ^ (2 * Fintype.card ι) := by
66     exact_mod_cast (even_add_odd (ι := ι))
67   have hdiff := even_sub_odd (ι := ι)
68   omega
69 
70 /-- Unlike the factored formula, this also applies in dimension zero. -/
71 theorem twice_odd : 2 * (oddCount ι : ℤ) =
72     2 ^ (2 * Fintype.card ι) - 2 ^ Fintype.card ι := by
73   have htot : (evenCount ι : ℤ) + oddCount ι = 2 ^ (2 * Fintype.card ι) := by
74     exact_mod_cast (even_add_odd (ι := ι))
75   have hdiff := even_sub_odd (ι := ι)
76   omega
77 
78 theorem even_factored (hr : 0 < Fintype.card ι) :
79     (evenCount ι : ℤ) = 2 ^ (Fintype.card ι - 1) * (2 ^ Fintype.card ι + 1) := by
80   have h := twice_even (ι := ι)
81   have hsq : (2 : ℤ) ^ (2 * Fintype.card ι) = ((2 : ℤ) ^ Fintype.card ι) ^ 2 := by
82     rw [Nat.mul_comm 2, pow_mul]
83   have hp : (2 : ℤ) ^ Fintype.card ι = 2 * 2 ^ (Fintype.card ι - 1) := by
84     conv_lhs => rw [show Fintype.card ι = (Fintype.card ι - 1) + 1 by omega]
85     rw [pow_succ]
86     ring
87   rw [hsq] at h
88   nlinarith
89 
90 theorem odd_factored (hr : 0 < Fintype.card ι) :
91     (oddCount ι : ℤ) = 2 ^ (Fintype.card ι - 1) * (2 ^ Fintype.card ι - 1) := by
92   have h := twice_odd (ι := ι)
93   have hsq : (2 : ℤ) ^ (2 * Fintype.card ι) = ((2 : ℤ) ^ Fintype.card ι) ^ 2 := by
94     rw [Nat.mul_comm 2, pow_mul]
95   have hp : (2 : ℤ) ^ Fintype.card ι = 2 * 2 ^ (Fintype.card ι - 1) := by
96     conv_lhs => rw [show Fintype.card ι = (Fintype.card ι - 1) + 1 by omega]
97     rw [pow_succ]
98     ring
99   rw [hsq] at h
100   nlinarith
101 
102 theorem counts_rank_zero (hr : Fintype.card ι = 0) :
103     evenCount ι = 1 ∧ oddCount ι = 0 := by
104   have he := twice_even (ι := ι)
105   have ho := twice_odd (ι := ι)
106   simp only [hr, mul_zero, pow_zero] at he ho
107   omega
108 
109 /-- The manuscript's factored formula at every rank, with an integer exponent. -/
110 theorem even_factored_rational :
111     (evenCount ι : ℚ) = (2 : ℚ) ^ ((Fintype.card ι : ℤ) - 1) *
112       ((2 : ℚ) ^ Fintype.card ι + 1) := by
113   by_cases hr : Fintype.card ι = 0
114   · rw [(counts_rank_zero hr).1, hr]
115     norm_num
116   · have he := even_factored (Nat.pos_of_ne_zero hr)
117     have hcast : (Fintype.card ι : ℤ) - 1 = ((Fintype.card ι - 1 : ℕ) : ℤ) := by
118       omega
119     rw [hcast, zpow_natCast]
120     exact_mod_cast he
121 
122 /-- The manuscript's factored formula at every rank, with an integer exponent. -/
123 theorem odd_factored_rational :
124     (oddCount ι : ℚ) = (2 : ℚ) ^ ((Fintype.card ι : ℤ) - 1) *
125       ((2 : ℚ) ^ Fintype.card ι - 1) := by
126   by_cases hr : Fintype.card ι = 0
127   · rw [(counts_rank_zero hr).2, hr]
128     norm_num
129   · have he := odd_factored (Nat.pos_of_ne_zero hr)
130     have hcast : (Fintype.card ι : ℤ) - 1 = ((Fintype.card ι - 1 : ℕ) : ℤ) := by
131       omega
132     rw [hcast, zpow_natCast]
133     exact_mod_cast he
134 
135 end PaperXI.DyadicCounts

Back to source controls