pith. machine review for the scientific record. sign in
theorem proved term proof

hpOperator_eigenvector_neg

show as:
view Lean formalization →

No prose has been written for this declaration yet. The Lean source and graph data below render without it.

generate prose now

formal statement (Lean)

  79theorem hpOperator_eigenvector_neg (q : ℕ) (a : ℤ) :
  80    (hpOperator q a).mulVec ![1, -1] = (-frobeniusAngle q a) • ![1, -1] := by

proof body

Term-mode proof.

  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]`. -/

used by (1)

From the project-wide theorem graph. These declarations reference this one in their body.

depends on (11)

Lean names referenced from this declaration's body.