Circles centred on the real line

For two real points c₁, c₂ of the complex plane, the difference of the two power functions |z - c|² - |C - c|² is affine in the real part of z and vanishes when z.re = C.re (Complex.normSq_sub_ofReal_sub_normSq_sub_ofReal): the radical axis of two circles centred on the real line is the vertical line through their intersection points. This file also records the real points of such a circle and on which side of a second circle its points lie.

Main results

• Complex.normSq_sub_ofReal_sub_normSq_sub_ofReal: the radical-line identity.
• Complex.norm_sub_eq_of_normSq_sub_eq: a point at squared distance ρ ^ 2 is at distance ρ.
• Complex.eq_sub_of_normSq_eq_of_lt_re, Complex.eq_add_of_normSq_eq_of_re_lt: a real point of the circle of centre m and radius ρ is m - ρ or m + ρ, according to its side.
• Complex.lt_normSq_sub_of_normSq_eq: points of one circle on one side of an intersection point with a second circle lie strictly outside the second circle.
• Complex.re_mem_Icc_of_normSq_sub_eq: the points of the circle of centre m and radius ρ have real part in [m - ρ, m + ρ].
• Complex.le_normSq_sub_of_le_normSq_sub: points on or outside one circle, between two of its points that lie on or outside a second circle, lie on or outside the second circle.

theorem Complex.normSq_sub_ofReal_sub_normSq_sub_ofReal {c₁ c₂ : ℝ} (C z : ℂ) : normSq (z - ↑c₁) - normSq (C - ↑c₁) - (normSq (z - ↑c₂) - normSq (C - ↑c₂)) = 2 * (c₂ - c₁) * (z.re - C.re)

The "radical line" identity: for real centres c₁ and c₂, the difference of the two power functions |z - c|² - |C - c|² of z is affine in z.re and vanishes at C.re.

theorem Complex.norm_sub_eq_of_normSq_sub_eq {z : ℂ} {m ρ : ℝ} (hρ : 0 ≤ ρ) (h : normSq (z - ↑m) = ρ ^ 2) : ‖z - ↑m‖ = ρ

A point at squared distance ρ ^ 2 from m, with 0 ≤ ρ, is at distance ρ.

theorem Complex.eq_sub_of_normSq_eq_of_lt_re {x m ρ : ℝ} {w : ℂ} (hρ : 0 ≤ ρ) (hx : normSq (↑x - ↑m) = ρ ^ 2) (hw : normSq (w - ↑m) = ρ ^ 2) (hxw : (↑x).re < w.re) : x = m - ρ

A real point x of the circle of centre m and radius ρ, to the left of a complex point w of that circle, is its left endpoint m - ρ.

theorem Complex.eq_add_of_normSq_eq_of_re_lt {x m ρ : ℝ} {w : ℂ} (hρ : 0 ≤ ρ) (hx : normSq (↑x - ↑m) = ρ ^ 2) (hw : normSq (w - ↑m) = ρ ^ 2) (hwx : w.re < (↑x).re) : x = m + ρ

A real point x of the circle of centre m and radius ρ, to the right of a complex point w of that circle, is its right endpoint m + ρ.

theorem Complex.lt_normSq_sub_of_normSq_eq {a w z : ℂ} {m₁ r₁ m₂ r₂ : ℝ} (ha₁ : normSq (a - ↑m₁) = r₁) (ha₂ : normSq (a - ↑m₂) = r₂) (hw₁ : normSq (w - ↑m₁) = r₁) (hw₂ : r₂ < normSq (w - ↑m₂)) (hz₁ : normSq (z - ↑m₁) = r₁) (hwa : w.re < a.re) (hza : z.re < a.re) : r₂ < normSq (z - ↑m₂)

The radical line of two circles. Let a lie on two circles centred on the real axis, the level sets |· - m₁|² = r₁ and |· - m₂|² = r₂, and let w lie on the first, to the left of a and strictly outside the second. Then every point z of the first circle to the left of a is strictly outside the second: on the first circle, |z - m₂|² - r₂ is an affine function of Re z, vanishing at a.

theorem Complex.re_mem_Icc_of_normSq_sub_eq {w : ℂ} {m ρ : ℝ} (hρ : 0 ≤ ρ) (h : normSq (w - ↑m) = ρ ^ 2) : w.re ∈ Set.Icc (m - ρ) (m + ρ)

A point at squared distance ρ ^ 2 from the real point m, with 0 ≤ ρ, has real part in [m - ρ, m + ρ].

theorem Complex.le_normSq_sub_of_le_normSq_sub {w₁ w₂ z : ℂ} {m r m' r' : ℝ} (h₁ : normSq (w₁ - ↑m) = r) (h₂ : normSq (w₂ - ↑m) = r) (h₁' : r' ≤ normSq (w₁ - ↑m')) (h₂' : r' ≤ normSq (w₂ - ↑m')) (hz : r ≤ normSq (z - ↑m)) (h₁z : w₁.re ≤ z.re) (hz₂ : z.re ≤ w₂.re) : r' ≤ normSq (z - ↑m')

Let w₁, w₂ lie on the circle |· - m|² = r and on or outside the circle |· - m'|² = r', for real centres m and m'. Then every point z on or outside the first circle with real part between those of w₁ and w₂ lies on or outside the second.