recognitionThetaTerm_two

formal source

 199  simp
 200
 201/-- The term at `n = 2` vanishes because `χ₈(2) = 0`. -/
 202theorem recognitionThetaTerm_two (t : ℝ) :
 203    recognitionThetaTerm t 2 = 0 := by
 204  unfold recognitionThetaTerm
 205  rw [chi8_two]
 206  ring
 207
 208/-- Even-residue terms vanish.  Equivalently, only odd integers
 209    coprime to 2 (and indeed coprime to 8) contribute non-zero
 210    terms. -/
 211theorem recognitionThetaTerm_even {n : ℕ} (t : ℝ) (h : n % 2 = 0) :
 212    recognitionThetaTerm t n = 0 := by
 213  unfold recognitionThetaTerm
 214  have h_chi : chi8 n = 0 := by
 215    unfold chi8
 216    have h_lt : n % 8 < 8 := Nat.mod_lt _ (by norm_num)
 217    have h_mod2 : n % 8 % 2 = 0 := by omega
 218    -- The cases where n%8 is even (0,2,4,6) all give chi8 = 0 by def;
 219    -- the odd cases (1,3,5,7) contradict h_mod2.
 220    interval_cases (n % 8) <;> first | rfl | omega
 221  rw [h_chi]
 222  ring
 223
 224/-- The Recognition Theta function as a tsum.  Convergence is part of
 225    Sub-conjecture A.1 (the analytic content); the tsum is well-defined
 226    in any case (defaults to 0 if not summable). -/
 227def recognitionTheta (t : ℝ) : ℝ :=
 228  ∑' n : ℕ, recognitionThetaTerm t n
 229
 230/-- A finite-sum approximation of the Recognition Theta, for numerical
 231    work and for finite-truncation theorems.  -/
 232def recognitionThetaTruncated (t : ℝ) (N : ℕ) : ℝ :=