hasseBound

formal source

  41  Real.arccos ((a : ℝ) / (2 * Real.sqrt (q : ℝ)))
  42
  43/-- The Hasse--Weil bound: `a^2 ≤ 4 q`, equivalently `|a| ≤ 2 √q`. -/
  44def hasseBound (q : ℕ) (a : ℤ) : Prop :=
  45  ((a : ℝ) ^ 2) ≤ 4 * (q : ℝ)
  46
  47/-! ## The Hilbert--Pólya operator -/
  48
  49/-- The Hilbert--Pólya operator `T_E` for an elliptic curve `E / F_q` with
  50    Frobenius trace `a`.  This is the real symmetric `2 × 2` matrix
  51    `[[0, θ], [θ, 0]]` where `θ` is the Frobenius angle. -/
  52def hpOperator (q : ℕ) (a : ℤ) : Matrix (Fin 2) (Fin 2) ℝ :=
  53  !![0, frobeniusAngle q a; frobeniusAngle q a, 0]
  54
  55/-- The operator is symmetric: `T_E^T = T_E`. -/
  56theorem hpOperator_isSymm (q : ℕ) (a : ℤ) :
  57    (hpOperator q a).IsSymm := by
  58  unfold hpOperator Matrix.IsSymm
  59  ext i j
  60  fin_cases i <;> fin_cases j <;> rfl
  61
  62/-! ## Eigenvalues
  63
  64The characteristic polynomial of `[[0, θ], [θ, 0]]` is `λ² - θ²`, with
  65roots `±θ`.  We exhibit eigenvectors directly. -/
  66
  67/-- The vector `(1, 1)` is an eigenvector with eigenvalue `+θ`. -/
  68theorem hpOperator_eigenvector_pos (q : ℕ) (a : ℤ) :
  69    (hpOperator q a).mulVec ![1, 1] = frobeniusAngle q a • ![1, 1] := by
  70  ext i
  71  fin_cases i <;>
  72    simp [hpOperator, Matrix.mulVec, Matrix.cons_val', Matrix.empty_val',
  73          Matrix.cons_val_fin_one, Matrix.cons_val_zero, Matrix.cons_val_one,
  74          Matrix.head_cons, Matrix.head_fin_const,