The crossing ratio

For unit vectors at angle θ, with inner product x = cos θ, the Gaussian threshold crossing bound is proportional to √(1 - x) / √(1 + x) = tan (θ / 2). This file names that ratio as a function of the inner product.

noncomputable def Algebraic.Cutwidth.Gaussian.tanHalf (x : ℝ) : ℝ

tanHalf (cos θ) = tan (θ / 2): the crossing ratio √(1 - x) / √(1 + x).

Equations

• Algebraic.Cutwidth.Gaussian.tanHalf x = √(1 - x) / √(1 + x)