Exact inverse trigonometric values divided by pi

On [-1, 1], inverse sine and cosine return rational multiples of pi at five rational inputs. Inverse tangent has three such inputs. The classifiers return these answers exactly. Niven's theorem rules out all other rational answers, supplying the termination premise for interval comparison. Domain checks belong to the numerical operation using the classifier.

theorem FloatLib.Numerics.TrigonometricComparison.arctanPiExact_eq_real (argument value : ℚ) (hvalue : arctanPiExact argument = some value) : Real.arctan ↑argument / Real.pi = ↑value

Every classified inverse tangent value is exact.

theorem FloatLib.Numerics.TrigonometricComparison.irrational_arctanPi_of_exact_none (argument : ℚ) (hnone : arctanPiExact argument = none) : Irrational (Real.arctan ↑argument / Real.pi)

Every unclassified inverse tangent divided by pi is irrational.

theorem FloatLib.Numerics.TrigonometricComparison.arcsinPiExact_eq_real (argument value : ℚ) (hvalue : arcsinPiExact argument = some value) : Real.arcsin ↑argument / Real.pi = ↑value

Every classified inverse sine value is exact.

theorem FloatLib.Numerics.TrigonometricComparison.irrational_arcsinPi_of_exact_none (argument : ℚ) (hlower : -1 ≤ argument) (hupper : argument ≤ 1) (hnone : arcsinPiExact argument = none) : Irrational (Real.arcsin ↑argument / Real.pi)

Niven's theorem makes the inverse sine classifier complete on [-1, 1].

theorem FloatLib.Numerics.TrigonometricComparison.arccosPiExact_eq_real (argument value : ℚ) (hvalue : arccosPiExact argument = some value) : Real.arccos ↑argument / Real.pi = ↑value

Every classified inverse cosine value is exact.

theorem FloatLib.Numerics.TrigonometricComparison.irrational_arccosPi_of_exact_none (argument : ℚ) (hlower : -1 ≤ argument) (hupper : argument ≤ 1) (hnone : arccosPiExact argument = none) : Irrational (Real.arccos ↑argument / Real.pi)

An unclassified inverse cosine divided by pi is irrational on its real domain.