OAI/NumberTheory/Ostmann/Quadratic/RootPopulationGeometry.lean

GitHub source file

2 declarations, 0 contain sorry, 0 declared as axioms

Diameter control for roots belonging to one signed quadratic kernel

  1. theorem OAI.Ostmann.square_sub_le_abs_square_difference line 10
  2. theorem OAI.Ostmann.kernel_root_diameter line 23

    Source documentation

    Both signs of the squarefree kernel are allowed. Nonnegative root parameters in an endpoint interval of diameter X have this diameter.

    theorem kernel_root_diameter (u m h x y a b X : ℝ)
    (hu : u ≠ 0) (hm : 0 ≤ m) (ha : 0 ≤ a) (hb : 0 ≤ b)
    (hx : u * a ^ 2 = m * x - h) (hy : u * b ^ 2 = m * y - h)
    (hxy : |x - y| ≤ X) :
    |a - b| ≤ Real.sqrt (m * X / |u|) := by
…