theorem
proved
chi8_zero
show as:
view math explainer →
open explainer
Read the cached plain-language explainer.
open lean source
IndisputableMonolith.NumberTheory.RecognitionTheta on GitHub at line 139.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
136 | _ => 0
137
138/-- `χ₈(0) = 0`. -/
139@[simp] theorem chi8_zero : chi8 0 = 0 := by
140 unfold chi8; rfl
141
142/-- `χ₈(1) = 1`. -/
143@[simp] theorem chi8_one : chi8 1 = 1 := by
144 unfold chi8; rfl
145
146/-- `χ₈(2) = 0`. -/
147theorem chi8_two : chi8 2 = 0 := by
148 unfold chi8; rfl
149
150/-- `χ₈(3) = 1`. -/
151theorem chi8_three : chi8 3 = 1 := by
152 unfold chi8; rfl
153
154/-- `χ₈(5) = -1`. -/
155theorem chi8_five : chi8 5 = -1 := by
156 unfold chi8; rfl
157
158/-- `χ₈(7) = -1`. -/
159theorem chi8_seven : chi8 7 = -1 := by
160 unfold chi8; rfl
161
162/-- The 8-tick character is bounded by 1 in absolute value. -/
163theorem chi8_abs_le_one (n : ℕ) : |chi8 n| ≤ 1 := by
164 unfold chi8
165 have h_lt : n % 8 < 8 := Nat.mod_lt _ (by norm_num)
166 interval_cases (n % 8) <;> simp
167
168/-- The 8-tick character is periodic with period 8. -/
169theorem chi8_periodic (n : ℕ) : chi8 (n + 8) = chi8 n := by