The chord and the arc on a circle

Mathlib's Circle carries both a metric, from the inclusion into ℂ, and an arc-length API: Circle.exp parametrizes it by angles and Circle.angleDiff x y is the length of the arc running counterclockwise from x to y. This file relates the two, comparing the chord dist x y with the arc separating x from y in both directions, and transports the chord formula along the translation and real scaling that carry Circle.exp to Mathlib's circleMap ζ ρ. It also records the chord with one endpoint allowed off the circle — the distance from a point of circleMap ζ ρ to an arbitrary point of the plane, which is the law of cosines — and reads off from that law when such a point lies in a disc ball c r, whose centre c is unrelated to the centre ζ of the circle.

Main results

• TauCeti.exp_mul_I_sub_exp_mul_I — the polar form of the chord: the half-angle sine rotated a quarter turn past the midpoint direction.
• TauCeti.dist_circleExp_eq_two_mul_abs_sin — the chord subtended by an arc of angle θ of the unit circle has length 2 * |sin (θ / 2)|.
• TauCeti.dist_circleMap_eq_two_mul_abs_sin — its form for the circle circleMap ζ ρ of arbitrary centre and radius, where the chord between the angles θ and θ' has length 2 * |ρ| * |sin ((θ - θ') / 2)|, and TauCeti.dist_circleMap_eq_two_mul_sin_abs, the same formula with the sign of the angular difference cleared, valid for angles at most a full turn apart.
• TauCeti.dist_circleMap_le_dist_circleMap_of_abs_sub_le — within half a turn that chord grows with the angular gap, so the distance to a fixed point of the circle is unimodal along it, and TauCeti.ordConnected_inter_setOf_dist_circleMap_lt — consequently a ball meets an arc of angular width at most π in a set of angles that is order connected.
• TauCeti.exists_mem_Ioo_circleMap_eq_and_abs_sub_lt_of_mem_ball_circleMap_image_Ioo — the inverse comparison on an arc that does not wrap: a point of the arc close enough to a fixed point of it is the image of a nearby angle, so closeness in the plane is closeness in angle.
• TauCeti.dist_circleMap_sq — the law of cosines: the point of circleMap ζ ρ at angle θ is at distance ρ ^ 2 + dist ζ c ^ 2 - 2 * ρ * dist ζ c * cos (θ - arg (c - ζ)), squared, from an arbitrary point c of the plane.
• TauCeti.circleMap_mem_ball_iff_sq and TauCeti.circleMap_mem_closedBall_iff_sq — that law compared with r ^ 2: when the point at angle θ lies in the disc ball c r, respectively in closedBall c r.
• TauCeti.circleMap_mem_ball_of_mem_Icc — since the criterion sees the angle only through cos (θ - arg (c - ζ)), the angles it admits form an arc: it holds throughout an interval of angles inside a period centred at arg (c - ζ) as soon as it holds at both ends.
• TauCeti.lipschitzWith_one_circleExp and TauCeti.diam_circleExp_image_Icc_le — the chord is at most the arc, so an arc of angles of length b - a has image of diameter at most b - a, and TauCeti.diam_range_circlePath_le — the same bound for Mathlib's arc Circle.path x y, whose angle is Circle.angleDiff x y.
• TauCeti.min_angleDiff_le_pi_div_two_mul_dist — the shorter of the two arcs joining two points of the circle has length at most π / 2 times their distance.

The argument

The first two are Mathlib's estimates for the normalized chord ‖exp (I * θ) - 1‖, read off the factorization exp a - exp b = (exp (a - b) - 1) * exp b: the chord formula is Complex.norm_exp_I_mul_ofReal_sub_one and the Lipschitz bound is Real.norm_exp_I_mul_ofReal_sub_one_le, so neither is derived from the other. The converse comparison TauCeti.min_angleDiff_le_pi_div_two_mul_dist is Jordan's inequality Real.mul_le_sin applied to the chord formula; it is the direction that turns a hypothesis about the ambient metric into a bound on an arc, and so the one a transport argument such as TauCeti/Topology/JordanCurve/SmallArc.lean consumes.

theorem TauCeti.exp_mul_I_sub_exp_mul_I (α β : ℝ) : Complex.exp (↑α * Complex.I) - Complex.exp (↑β * Complex.I) = 2 * ↑(Real.sin ((α - β) / 2)) * Complex.I * Complex.exp (↑((α + β) / 2) * Complex.I)

The polar chord identity on the unit circle: the difference of two unit-circle points is the half-angle sine, rotated a quarter turn past the midpoint direction.

theorem TauCeti.dist_circleExp_eq_two_mul_abs_sin (a b : ℝ) : dist (Circle.exp a) (Circle.exp b) = 2 * |Real.sin ((a - b) / 2)|

The chord formula for the unit circle: two points of the circle at angles a and b are at distance 2 * |sin ((a - b) / 2)|.

theorem TauCeti.dist_circleMap_eq_two_mul_abs_sin (ζ : ℂ) (ρ θ θ' : ℝ) : dist (circleMap ζ ρ θ) (circleMap ζ ρ θ') = 2 * |ρ| * |Real.sin ((θ - θ') / 2)|

The chord of a circle of arbitrary centre and radius. The two points of circleMap ζ ρ at angles θ and θ' are at distance 2 * |ρ| * |sin ((θ - θ') / 2)|; nothing is assumed of the radius, a negative ρ tracing the same circle in the other sense.

This is the unit-circle formula TauCeti.dist_circleExp_eq_two_mul_abs_sin transported along the translation and real scaling that carry Circle.exp to circleMap ζ ρ.

theorem TauCeti.dist_circleMap_eq_two_mul_sin_abs (ζ : ℂ) (ρ : ℝ) {θ θ' : ℝ} (h : |θ - θ'| ≤ 2 * Real.pi) : dist (circleMap ζ ρ θ) (circleMap ζ ρ θ') = 2 * |ρ| * Real.sin (|θ - θ'| / 2)

The chord with the sign of the angular difference cleared. For angles at most a full turn apart the chord TauCeti.dist_circleMap_eq_two_mul_abs_sin is 2 * |ρ| * sin (|θ - θ'| / 2): the absolute value moves from outside the sine to inside it.

The width restriction is what makes the two forms differ: it puts the half-angle in [0, π], where the sine is nonnegative, and past a full turn the half-angle leaves that interval and |sin| and sin ∘ |·| part company. Up to π the right-hand side is moreover an increasing function of the angular gap, the half-angle then staying in [0, π / 2]; beyond π the formula still holds but the chord shrinks again as the gap widens.

theorem TauCeti.dist_circleMap_le_dist_circleMap_of_abs_sub_le (ζ : ℂ) (ρ : ℝ) {θ₀ u v : ℝ} (huv : |u - θ₀| ≤ |v - θ₀|) (hv : |v - θ₀| ≤ Real.pi) : dist (circleMap ζ ρ u) (circleMap ζ ρ θ₀) ≤ dist (circleMap ζ ρ v) (circleMap ζ ρ θ₀)

Within half a turn, the chord grows with the angular gap. If the angle u is no further from θ₀ than v is, and v is within half a turn of θ₀, then the point of circleMap ζ ρ at angle u is no further from the one at θ₀ than the point at v is.

Both chords are TauCeti.dist_circleMap_eq_two_mul_sin_abs, and the half-angles they feed to the sine stay in [0, π / 2], where the sine is monotone. The restriction to half a turn is sharp: antipodal points are the furthest apart, and beyond them the chord shrinks again.

theorem TauCeti.exists_mem_Ioo_circleMap_eq_and_abs_sub_lt_of_mem_ball_circleMap_image_Ioo (ζ : ℂ) (ρ : ℝ) {a b θ₀ m : ℝ} (hab2π : b - a < 2 * Real.pi) (hθ₀ : θ₀ ∈ Set.Icc a b) (hm0 : 0 < m) {x : ℂ} (hx : x ∈ circleMap ζ ρ '' Set.Ioo a b ∩ Metric.ball (circleMap ζ ρ θ₀) (2 * |ρ| * min (Real.sin (m / 2)) (Real.sin ((b - a) / 2)))) : ∃ θ ∈ Set.Ioo a b, circleMap ζ ρ θ = x ∧ |θ - θ₀| < m

On a non-wrapping arc, closeness in the plane is closeness in angle. A point of the arc circleMap ζ ρ '' Ioo a b lying within 2 * |ρ| * min (sin (m / 2)) (sin ((b - a) / 2)) of circleMap ζ ρ θ₀ is the image of an angle within m of θ₀.

theorem TauCeti.ordConnected_inter_setOf_dist_circleMap_lt (ζ : ℂ) (ρ : ℝ) {s : Set ℝ} {θ₀ δ : ℝ} (hs : s.OrdConnected) (hsub : s ⊆ Set.Icc (θ₀ - Real.pi) (θ₀ + Real.pi)) : (s ∩ {θ : ℝ | dist (circleMap ζ ρ θ) (circleMap ζ ρ θ₀) < δ}).OrdConnected

An order-connected set of angles within half a turn of θ₀ keeps that form when cut down by the distance to the point at θ₀. For a set s of angles contained in the half-turn [θ₀ - π, θ₀ + π], the angles of s whose points lie within δ of the point at angle θ₀ form an order-connected subset of s.

The chord distance to θ₀ falls and then rises as the angle sweeps across s (TauCeti.dist_circleMap_le_dist_circleMap_of_abs_sub_le), so an angle between two admitted ones is itself no further from θ₀ than the admitted one on its side of θ₀. The angle θ₀ need not lie in s, and the radius δ is arbitrary: for large δ the trace is all of s.

theorem TauCeti.dist_circleMap_sq (ζ c : ℂ) (ρ θ : ℝ) : dist (circleMap ζ ρ θ) c ^ 2 = ρ ^ 2 + dist ζ c ^ 2 - 2 * ρ * dist ζ c * Real.cos (θ - (c - ζ).arg)

The law of cosines for a point of a circle. The point of circleMap ζ ρ at angle θ is at distance ρ ^ 2 + dist ζ c ^ 2 - 2 * ρ * dist ζ c * cos (θ - arg (c - ζ)), squared, from an arbitrary point c. For ρ ≥ 0 this is the law of cosines as usually read: in the triangle with vertices ζ, circleMap ζ ρ θ and c, the angle at ζ between the two sides of lengths ρ and dist ζ c is θ - arg (c - ζ). It is the chord formula TauCeti.dist_circleMap_eq_two_mul_abs_sin with one endpoint allowed off the circle.

Nothing is assumed, and the identity is the signed-radius extension of that reading. For ρ < 0 the point circleMap ζ ρ θ is the one at angle θ + π on the circle of radius -ρ, so the side at ζ has length -ρ and points in the direction θ + π; the identity still holds as stated because only ρ ^ 2 and ρ * cos occur, and the two sign changes cancel. For c = ζ both terms carrying dist ζ c vanish, so the junk value arg 0 = 0 does no harm and the identity reads dist (circleMap ζ ρ θ) ζ ^ 2 = ρ ^ 2.

theorem TauCeti.circleMap_mem_ball_iff_sq {c ζ : ℂ} {r : ℝ} (hr : 0 ≤ r) (ρ θ : ℝ) : circleMap ζ ρ θ ∈ Metric.ball c r ↔ ρ ^ 2 + dist ζ c ^ 2 - r ^ 2 < 2 * ρ * dist ζ c * Real.cos (θ - (c - ζ).arg)

When a point of a circle lies in a disc, read off the law of cosines. For r ≥ 0 and a disc ball c r whose centre is unrelated to the centre ζ of the circle, the point circleMap ζ ρ θ lies in ball c r exactly when ρ ^ 2 + dist ζ c ^ 2 - r ^ 2 < 2 * ρ * dist ζ c * cos (θ - arg (c - ζ)).

This is TauCeti.dist_circleMap_sq compared with r ^ 2, both sides of dist … < r being nonnegative. Nothing is assumed of ρ: for ρ > 0 the point described is the point of sphere ζ ρ at angle θ, and for ρ < 0 it is the point of sphere ζ (-ρ) at angle θ + π, the criterion following it as the law of cosines does. Since the right-hand side depends on θ only through cos (θ - arg (c - ζ)), the angles it admits form an arc (TauCeti.circleMap_mem_ball_of_mem_Icc).

At a point ζ of the boundary circle sphere c r the two squared radii cancel and, for ρ > 0, the surviving condition ρ ^ 2 < 2 * ρ * r * cos (θ - arg (c - ζ)) may be divided by ρ; that case is TauCeti.circleMap_mem_ball_iff of TauCeti/Analysis/Complex/Conformal/Crosscut/Basic.lean.

theorem TauCeti.circleMap_mem_closedBall_iff_sq {c ζ : ℂ} {r : ℝ} (hr : 0 ≤ r) (ρ θ : ℝ) : circleMap ζ ρ θ ∈ Metric.closedBall c r ↔ ρ ^ 2 + dist ζ c ^ 2 - r ^ 2 ≤ 2 * ρ * dist ζ c * Real.cos (θ - (c - ζ).arg)

When a point of a circle lies in a closed disc. The weak companion of TauCeti.circleMap_mem_ball_iff_sq: for r ≥ 0 and an arbitrary centre ζ, the point circleMap ζ ρ θ lies in closedBall c r exactly when ρ ^ 2 + dist ζ c ^ 2 - r ^ 2 ≤ 2 * ρ * dist ζ c * cos (θ - arg (c - ζ)). Nothing is assumed of ρ, whose sign is read as it is there.

At a point ζ of the boundary circle sphere c r the two squared radii cancel and, for ρ > 0, the surviving condition may be divided by ρ; that case is TauCeti.circleMap_mem_closedBall_iff of TauCeti/Analysis/Complex/Conformal/Crosscut/Endpoints.lean.

theorem TauCeti.circleMap_mem_ball_of_mem_Icc {c ζ : ℂ} {r ρ : ℝ} (hρ : 0 ≤ ρ) {a b θ : ℝ} (ha : -Real.pi ≤ a - (c - ζ).arg) (hb : b - (c - ζ).arg ≤ Real.pi) (hθ : θ ∈ Set.Icc a b) (hain : circleMap ζ ρ a ∈ Metric.ball c r) (hbin : circleMap ζ ρ b ∈ Metric.ball c r) : circleMap ζ ρ θ ∈ Metric.ball c r

A circle meets a disc in a connected set of angles. If the angles a and b both lie within π of the direction arg (c - ζ) from the centre ζ of the circle to the centre c of the disc, and both put the point of sphere ζ ρ they name inside ball c r, then so does every angle in [a, b].

This is TauCeti.circleMap_mem_ball_iff_sq read through the unimodality of cos on a period centred at arg (c - ζ), which is Real.lt_cos_of_mem_Icc. Neither 0 < r nor any relation between ζ and the disc is assumed: the first is forced by the hypotheses, and the second is not needed, so the conclusion covers a cutting circle centred anywhere and not only the circular crosscut at a boundary point ζ of the disc. Two degenerate cases are covered as well, in both of which the criterion is independent of the angle: a circle centred at c itself, whose points are all at the same distance from c, and the circle of radius ρ = 0, which is the single point ζ.

theorem TauCeti.lipschitzWith_one_circleExp : LipschitzWith 1 ⇑Circle.exp

The chord is at most the arc: Circle.exp is 1-Lipschitz.

theorem TauCeti.diam_circleExp_image_Icc_le {a b : ℝ} (hab : a ≤ b) : Metric.diam (⇑Circle.exp '' Set.Icc a b) ≤ b - a

An arc of the circle spanning the angles Set.Icc a b has diameter at most b - a.

theorem TauCeti.diam_range_circlePath_le (x y : Circle) : Metric.diam (Set.range ⇑(x.path y)) ≤ x.angleDiff y

A closed arc is no wider than its angle. Mathlib's arc Circle.path x y, which runs counterclockwise from x to y, has range of diameter at most the length Circle.angleDiff x y of that arc.

This is TauCeti.diam_circleExp_image_Icc_le read through Circle.range_path, which presents the closed arc as the Circle.exp image of an interval of angles of length Circle.angleDiff x y. It is stated for the range rather than for the path so that it applies unchanged to the reversed arc, whose range is the same by Path.symm_range.

theorem TauCeti.min_angleDiff_le_pi_div_two_mul_dist (x y : Circle) : min (x.angleDiff y) (y.angleDiff x) ≤ Real.pi / 2 * dist x y

The shorter arc is controlled by the chord: of the two arcs joining x to y on the circle, the shorter has length at most π / 2 times the distance from x to y.

This is the direction of the comparison that converts a hypothesis about the ambient metric into a bound on an arc, and so the one a transport argument consumes.