theorem
proved
chi8_five
show as:
view math explainer →
open explainer
Generate a durable explainer page for this declaration.
open lean source
IndisputableMonolith.NumberTheory.RecognitionTheta on GitHub at line 155.
browse module
All declarations in this module, on Recognition.
explainer page
depends on
formal source
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
170 unfold chi8
171 congr 1
172 omega
173
174/-! ## The Recognition Theta function
175
176For `t > 0`, the Recognition Theta function is the convergent series
177
178 `Θ̃_RS(t) := Σ_{n ≥ 1} χ₈(n) · φ^{-r(n)} · e^{-t · c(n)}`
179
180where `χ₈` is the 8-tick character, `r(n) = phiRung n` is the
181phi-rung index, and `c(n) = costSpectrumValue n` is the cost.
182-/
183
184/-- The n-th term of the Recognition Theta function. -/
185def recognitionThetaTerm (t : ℝ) (n : ℕ) : ℝ :=