hpOperator_eigenvector_neg

formal source

  76    ring
  77
  78/-- The vector `(1, -1)` is an eigenvector with eigenvalue `-θ`. -/
  79theorem hpOperator_eigenvector_neg (q : ℕ) (a : ℤ) :
  80    (hpOperator q a).mulVec ![1, -1] = (-frobeniusAngle q a) • ![1, -1] := by
  81  ext i
  82  fin_cases i <;>
  83    simp [hpOperator, Matrix.mulVec, Matrix.cons_val', Matrix.empty_val',
  84          Matrix.cons_val_fin_one, Matrix.cons_val_zero, Matrix.cons_val_one,
  85          Matrix.head_cons, Matrix.head_fin_const,
  86          Matrix.cons_dotProduct, Matrix.dotProduct_empty, Fin.sum_univ_two] <;>
  87    ring
  88
  89/-! ## Hasse bound implies real spectrum
  90
  91For the angle `θ` to be a real number representing a meaningful spectral
  92quantity, we need `arccos`'s argument to lie in `[-1, 1]`.  This is the
  93content of the Hasse--Weil bound. -/
  94
  95/-- If the Hasse bound `a^2 ≤ 4q` holds, then `a / (2√q) ∈ [-1, 1]`. -/
  96theorem hasse_implies_arccos_valid
  97    (q : ℕ) (hq : 0 < q) (a : ℤ) (h_hasse : hasseBound q a) :
  98    ((a : ℝ) / (2 * Real.sqrt (q : ℝ))) ∈ Set.Icc (-1 : ℝ) 1 := by
  99  unfold hasseBound at h_hasse
 100  have hq_pos : (0 : ℝ) < (q : ℝ) := by exact_mod_cast hq
 101  have hsqrt_pos : 0 < Real.sqrt (q : ℝ) := Real.sqrt_pos.mpr hq_pos
 102  have h2sqrt_pos : 0 < 2 * Real.sqrt (q : ℝ) := by linarith
 103  have h_sqrt_sq : (Real.sqrt (q : ℝ)) ^ 2 = (q : ℝ) :=
 104    Real.sq_sqrt (le_of_lt hq_pos)
 105  -- |a|^2 = a^2 ≤ 4q = (2√q)^2, so |a| ≤ 2√q.
 106  have h_abs_sq : |(a : ℝ)| ^ 2 ≤ (2 * Real.sqrt (q : ℝ)) ^ 2 := by
 107    rw [_root_.sq_abs]
 108    have h_rhs : (2 * Real.sqrt (q : ℝ)) ^ 2 = 4 * (q : ℝ) := by
 109      rw [mul_pow, h_sqrt_sq]; ring