Level sets of first-order trigonometric polynomials

A real combination a cos x + b sin x is a single shifted cosine: with z = a + b i,

a cos x + b sin x = ‖z‖ cos (x - arg z)

(Real.mul_cos_add_mul_sin_eq_norm_mul_cos_sub_arg), the harmonic addition formula. Each level set of cos is a union of two cosets of 2πℤ, so it is countable (Real.countable_setOf_cos_eq), and hence so is each level set of a cos x + b sin x unless a = b = 0 (Real.countable_setOf_mul_cos_add_mul_sin_eq). Since an interval of positive length is uncountable, the complement of such a level set, or of a countable union of them, is dense.

This is the form in which a one-parameter family of 2 × 2 matrices such as θ ↦ R(θ) A, with R(θ) a rotation, has trace avoiding a prescribed countable set of values for all but countably many parameters.

theorem Real.mul_cos_add_mul_sin_eq_norm_mul_cos_sub_arg (a b x : ℝ) : a * cos x + b * sin x = ‖↑a + ↑b * Complex.I‖ * cos (x - (↑a + ↑b * Complex.I).arg)

Harmonic addition. A real combination of cos x and sin x is a shifted multiple of cos: a cos x + b sin x = ‖a + b i‖ cos (x - arg (a + b i)).

theorem Real.countable_setOf_cos_eq (c : ℝ) : {x : ℝ | cos x = c}.Countable

The level sets of cos are countable: cos x = c only on the two cosets ±arccos c + 2πℤ, and nowhere if |c| > 1.

theorem Real.countable_setOf_mul_cos_add_mul_sin_eq {a b : ℝ} (hab : a ≠ 0 ∨ b ≠ 0) (c : ℝ) : {x : ℝ | a * cos x + b * sin x = c}.Countable

The level sets of a cos x + b sin x are countable unless a = b = 0.