Comparing an angle with an arccosine

Mathlib's Analysis/SpecialFunctions/Trigonometric/Inverse.lean carries a complete comparison family for Real.arcsin — Real.arcsin_le_iff_le_sin, Real.le_arcsin_iff_sin_le, Real.arcsin_lt_iff_lt_sin, Real.lt_arcsin_iff_sin_lt and their primed variants — turning an inequality between an angle and an arcsin into one between a real number and a sin. It carries no counterpart for Real.arccos: the pinned Mathlib knows Real.arccos_le_arccos, Real.arccos_lt_arccos and Real.cos_arccos, but nothing that compares an angle with an arccosine.

This file supplies that family, and reads it off as a description of the sublevel and superlevel sets of Real.cos on one period. Since arccos is antitone, the comparisons swap sides: arccos x ≤ y ↔ cos y ≤ x where the arcsin family has arcsin x ≤ y ↔ x ≤ sin y.

Main results

• Real.arccos_le_iff_cos_le, Real.le_arccos_iff_le_cos, Real.arccos_lt_iff_cos_lt and Real.lt_arccos_iff_lt_cos — the four comparisons on the closed domain, for x in [-1, 1] and an angle y in [0, π].
• Real.arccos_le_iff_cos_le', Real.le_arccos_iff_le_cos', Real.arccos_lt_iff_cos_lt' and Real.lt_arccos_iff_lt_cos' — the same four with nothing at all assumed of x. Exactly as for Mathlib's primed arcsin lemmas, the degenerate values x < -1 and 1 < x, where arccos is constant, are covered at the price of excluding the one endpoint of [0, π] at which the comparison would then fail.
• Real.abs_lt_arccos_iff_lt_cos and Real.abs_le_arccos_iff_le_cos — since cos is even, an angle t of the full period [-π, π] may be compared through |t|; here the excluded endpoint is paid for by a one-sided bound on x instead.
• Real.lt_cos_iff_mem_Ioo and Real.le_cos_iff_mem_Icc — the same statements read as {t ∈ [-π, π] | x < cos t} = (-arccos x, arccos x) and its closed companion: on one period centred at 0, the angles at which cos exceeds a threshold form the symmetric interval of half-width arccos x.
• Real.lt_cos_of_mem_Icc — the unimodality corollary: cos has no interior minimum on [-π, π], so a strict lower bound holding at both ends of a subinterval holds throughout it.

The argument

The closed-domain family is Real.arccos_eq_pi_div_two_sub_arcsin fed into Mathlib's arcsin family, followed by Real.sin_pi_div_two_sub; each primed form is then its unprimed form together with the two degenerate ranges of x, and the strict comparisons are negations of the weak ones — exactly the shape, and the same order of derivation, that the arcsin family has. The |t| forms split off the single degenerate angle that the half-period statement does not reach, and the interval forms are abs_lt and abs_le.

This is general real analysis, extracted from two places that had proved fragments of it privately: TauCeti/Analysis/Complex/Conformal/Crosscut/Endpoints.lean, which described a circular crosscut of a disc as an angular arc of half-width arccos (ρ / (2 * r)), and TauCeti/Topology/Circle/Metric.lean, which needed the unimodality corollary to see that a circle meets a disc in a connected set of angles. Both belong to layer L5 of TauCetiRoadmap/ConformalMapping/README.md, the Jordan-domain case of the Carathéodory boundary correspondence, but neither statement mentions a holomorphic map, a disc, or even the plane.

theorem Real.arccos_le_iff_cos_le {x y : ℝ} (hx : x ∈ Set.Icc (-1) 1) (hy : y ∈ Set.Icc 0 Real.pi) : arccos x ≤ y ↔ cos y ≤ x

An arccosine is at most an angle exactly when the angle's cosine is at most the value. For x ∈ [-1, 1] and an angle y ∈ [0, π], the two intervals on which Real.arccos and Real.cos are mutually inverse, arccos x ≤ y ↔ cos y ≤ x. The Real.arccos counterpart of Mathlib's Real.le_arcsin_iff_sin_le, with the sides swapped because Real.arccos is antitone.

theorem Real.arccos_le_iff_cos_le' {x y : ℝ} (hy : y ∈ Set.Ico 0 Real.pi) : arccos x ≤ y ↔ cos y ≤ x

An arccosine is at most an angle exactly when the angle's cosine is at most the value, with nothing assumed of x. The Real.arccos counterpart of Mathlib's Real.le_arcsin_iff_sin_le'.

The angle y is excluded from π, and in exchange the bounds on x are dropped: for x < -1 and for 1 < x, where Real.arccos is constant, both sides then agree. At y = π the left side is automatic while the right side, -1 ≤ x, is not; at the other endpoint y = 0 the statement is Real.arccos_eq_zero.

theorem Real.le_arccos_iff_le_cos {x y : ℝ} (hx : x ∈ Set.Icc (-1) 1) (hy : y ∈ Set.Icc 0 Real.pi) : y ≤ arccos x ↔ x ≤ cos y

An angle is at most an arccosine exactly when the value is at most the angle's cosine. For x ∈ [-1, 1] and an angle y ∈ [0, π], y ≤ arccos x ↔ x ≤ cos y. The Real.arccos counterpart of Mathlib's Real.arcsin_le_iff_le_sin.

theorem Real.le_arccos_iff_le_cos' {x y : ℝ} (hy : y ∈ Set.Ioc 0 Real.pi) : y ≤ arccos x ↔ x ≤ cos y

An angle is at most an arccosine exactly when the value is at most the angle's cosine, with nothing assumed of x. The Real.arccos counterpart of Mathlib's Real.arcsin_le_iff_le_sin'.

The angle y is excluded from 0, and in exchange the bounds on x are dropped. At y = 0 the left side is automatic while the right side, x ≤ 1, is not; at the other endpoint y = π the statement is Real.arccos_eq_pi.

theorem Real.arccos_lt_iff_cos_lt {x y : ℝ} (hx : x ∈ Set.Icc (-1) 1) (hy : y ∈ Set.Icc 0 Real.pi) : arccos x < y ↔ cos y < x

An arccosine is below an angle exactly when the angle's cosine is below the value. The strict form of Real.arccos_le_iff_cos_le, for x ∈ [-1, 1] and an angle y ∈ [0, π].

theorem Real.arccos_lt_iff_cos_lt' {x y : ℝ} (hy : y ∈ Set.Ioc 0 Real.pi) : arccos x < y ↔ cos y < x

An arccosine is below an angle exactly when the angle's cosine is below the value, with nothing assumed of x. The strict form of Real.arccos_le_iff_cos_le'; as in Real.le_arccos_iff_le_cos', whose negation it is, the angle y runs over Ioc 0 π.

theorem Real.lt_arccos_iff_lt_cos {x y : ℝ} (hx : x ∈ Set.Icc (-1) 1) (hy : y ∈ Set.Icc 0 Real.pi) : y < arccos x ↔ x < cos y

An angle is below an arccosine exactly when the value is below the angle's cosine. The strict form of Real.le_arccos_iff_le_cos, for x ∈ [-1, 1] and an angle y ∈ [0, π].

theorem Real.lt_arccos_iff_lt_cos' {x y : ℝ} (hy : y ∈ Set.Ico 0 Real.pi) : y < arccos x ↔ x < cos y

An angle is below an arccosine exactly when the value is below the angle's cosine, with nothing assumed of x. The strict form of Real.le_arccos_iff_le_cos'; as in Real.arccos_le_iff_cos_le', whose negation it is, the angle y runs over Ico 0 π.

theorem Real.abs_lt_arccos_iff_lt_cos {x t : ℝ} (hx : -1 ≤ x) (ht : |t| ≤ Real.pi) : |t| < arccos x ↔ x < cos t

On a full period, a strict lower bound on the cosine is a strict upper bound on the angle. Because Real.cos is even, Real.lt_arccos_iff_lt_cos' extends from [0, π] to [-π, π] read through |t|. The angle is now allowed to reach π, at the cost of the hypothesis -1 ≤ x, which is what makes the two sides agree there: both are false.

theorem Real.abs_le_arccos_iff_le_cos {x t : ℝ} (hx : x ≤ 1) (ht : |t| ≤ Real.pi) : |t| ≤ arccos x ↔ x ≤ cos t

On a full period, a lower bound on the cosine is an upper bound on the angle. The weak companion of Real.abs_lt_arccos_iff_lt_cos; here it is the angle 0 that the half-period statement does not reach, and the hypothesis x ≤ 1 that makes both sides true there.

theorem Real.lt_cos_iff_mem_Ioo {x t : ℝ} (hx : -1 ≤ x) (ht : t ∈ Set.Icc (-Real.pi) Real.pi) : x < cos t ↔ t ∈ Set.Ioo (-arccos x) (arccos x)

The cosine exceeds a threshold on a symmetric interval. On the period [-π, π] the angles at which Real.cos exceeds x are exactly those of (-arccos x, arccos x).

theorem Real.le_cos_iff_mem_Icc {x t : ℝ} (hx : x ≤ 1) (ht : t ∈ Set.Icc (-Real.pi) Real.pi) : x ≤ cos t ↔ t ∈ Set.Icc (-arccos x) (arccos x)

The cosine reaches a threshold on a symmetric closed interval. The weak companion of Real.lt_cos_iff_mem_Ioo.

theorem Real.lt_cos_of_mem_Icc {k a b θ : ℝ} (ha : -Real.pi ≤ a) (hb : b ≤ Real.pi) (hθ : θ ∈ Set.Icc a b) (hka : k < cos a) (hkb : k < cos b) : k < cos θ

The cosine has no interior minimum on [-π, π]. If k < cos a and k < cos b, with -π ≤ a and b ≤ π, then k < cos θ for every θ ∈ [a, b].

This is Real.lt_cos_iff_mem_Ioo read as unimodality: below -1 the bound is vacuous, and above it the angles admitted form an interval symmetric about 0, which therefore contains [a, b] as soon as it contains both endpoints.