Normalising a real angle into [0, 2π)

Real.Angle is ℝ modulo 2π, and toIcoMod Real.two_pi_pos 0 is the section of the quotient map picking the representative in [0, 2π). Mathlib records one direction of the relationship between the two, as Real.Angle.coe_toIcoMod: normalising and then projecting to Real.Angle changes nothing.

This file records that the section is injective on angles — the normalisations of two reals agree exactly when the reals agree in Real.Angle. That is the transport step behind any computation of a normalised angle: the identity is proved in Real.Angle, where 2π is invisible, and then read back as an equality of representatives.

It also records how the representative Real.Angle.toReal ∈ (-π, π] behaves on differences of angles of the same sign, the difference counterpart of Mathlib's toReal_add_of_sign_eq_neg_sign.

Main results

• Real.Angle.toIcoMod_eq_toIcoMod_iff_coe_eq: two reals have the same [0, 2π) representative exactly when they are equal in Real.Angle.
• Real.Angle.toReal_sub_of_sign_eq: for angles of the same sign, the subtracted one not π, toReal of the difference is the difference of the toReals.
• Real.Angle.sign_sub_pos_iff_toReal_lt_of_sign_eq: for angles of the same nonzero sign, the difference has positive sign exactly when the representatives increase.

theorem Real.Angle.toIcoMod_eq_toIcoMod_iff_coe_eq {x y : ℝ} : toIcoMod two_pi_pos 0 x = toIcoMod two_pi_pos 0 y ↔ ↑x = ↑y

Equal angles are exactly equal normalisations. Two reals agree in Real.Angle — that is, differ by an integer multiple of 2π — exactly when their representatives in [0, 2π) agree, since the normalisation discards precisely such a multiple.

The forward direction is Mathlib's Real.Angle.coe_toIcoMod applied on both sides; the reverse shifts one argument by the multiple and uses toIcoMod_add_zsmul.

theorem Real.Angle.toReal_sub_of_sign_eq {θ ψ : Angle} (hψ : ψ ≠ ↑Real.pi) (hs : θ.sign = ψ.sign) : (θ - ψ).toReal = θ.toReal - ψ.toReal

The representative of a difference of two angles of the same sign is the difference of the representatives, provided the subtracted angle is not π.

theorem Real.Angle.sign_sub_pos_iff_toReal_lt_of_sign_eq {θ ψ : Angle} (hs : θ.sign = ψ.sign) (h0 : θ.sign ≠ 0) : (ψ - θ).sign = 1 ↔ θ.toReal < ψ.toReal

For two angles of the same nonzero sign, their difference has positive sign exactly when their representatives are in increasing order.