circleMap

This file defines the circle map $θ ↦ c + R e^{θi}$, a parametrization of a circle.

Main definitions

• circleMap c R: the exponential map $θ ↦ c + R e^{θi}$.

Tags

noncomputable def circleMap (c : ℂ) (R : ℝ) : ℝ → ℂ

The exponential map $θ ↦ c + R e^{θi}$. The range of this map is the circle in ℂ with center c and radius |R|.

Equations

• circleMap c R θ = c + ↑R * Complex.exp (↑θ * Complex.I)

@[simp]

theorem circleMap_sub_center (c : ℂ) (R θ : ℝ) : circleMap c R θ - c = circleMap 0 R θ

theorem circleMap_zero (R θ : ℝ) : circleMap 0 R θ = ↑R * Complex.exp (↑θ * Complex.I)

@[simp]

theorem norm_circleMap_zero (R θ : ℝ) : ‖circleMap 0 R θ‖ = |R|

theorem circleMap_notMem_ball (c : ℂ) (R θ : ℝ) : circleMap c R θ ∉ Metric.ball c R

theorem circleMap_ne_mem_ball {c : ℂ} {R : ℝ} {w : ℂ} (hw : w ∈ Metric.ball c R) (θ : ℝ) : circleMap c R θ ≠ w

theorem circleMap_mem_sphere' (c : ℂ) (R θ : ℝ) : circleMap c R θ ∈ Metric.sphere c |R|

theorem circleMap_mem_sphere (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (θ : ℝ) : circleMap c R θ ∈ Metric.sphere c R

theorem circleMap_mem_closedBall (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (θ : ℝ) : circleMap c R θ ∈ Metric.closedBall c R

theorem norm_circleMap_sub_le (c : ℂ) (R θ : ℝ) (x : ℂ) : ‖circleMap c R θ - x‖ ≤ |R| + dist c x

theorem exists_ball_forall_le_norm_circleMap_sub {R : ℝ} {c w : ℂ} (hw : w ∉ Metric.sphere c |R|) : ∃ d > 0, ∀ x ∈ Metric.ball w d, ∀ (θ : ℝ), d ≤ ‖circleMap c R θ - x‖

If w does not lie on the circle sphere c |R|, there is a radius d > 0 such that all points of ball w d keep distance at least d from every point circleMap c R θ of the circle.

@[simp]

theorem circleMap_eq_center_iff {c : ℂ} {R θ : ℝ} : circleMap c R θ = c ↔ R = 0

@[simp]

theorem circleMap_zero_radius (c : ℂ) : circleMap c 0 = Function.const ℝ c

theorem circleMap_ne_center {c : ℂ} {R : ℝ} (hR : R ≠ 0) {θ : ℝ} : circleMap c R θ ≠ c

theorem circleMap_zero_mul (R₁ R₂ θ₁ θ₂ : ℝ) : circleMap 0 R₁ θ₁ * circleMap 0 R₂ θ₂ = circleMap 0 (R₁ * R₂) (θ₁ + θ₂)

theorem circleMap_zero_div (R₁ R₂ θ₁ θ₂ : ℝ) : circleMap 0 R₁ θ₁ / circleMap 0 R₂ θ₂ = circleMap 0 (R₁ / R₂) (θ₁ - θ₂)

theorem circleMap_zero_inv (R θ : ℝ) : (circleMap 0 R θ)⁻¹ = circleMap 0 R⁻¹ (-θ)

theorem circleMap_zero_pow (n : ℕ) (R θ : ℝ) : circleMap 0 R θ ^ n = circleMap 0 (R ^ n) (↑n * θ)

theorem circleMap_zero_zpow (n : ℤ) (R θ : ℝ) : circleMap 0 R θ ^ n = circleMap 0 (R ^ n) (↑n * θ)

theorem conj_circleMap_zero (r θ : ℝ) : (starRingEnd ℂ) (circleMap 0 r θ) = circleMap 0 r (-θ)

theorem conj_circleMap (c : ℂ) (r θ : ℝ) : (starRingEnd ℂ) (circleMap c r θ) = circleMap ((starRingEnd ℂ) c) r (-θ)

theorem circleMap_zero_re (r θ : ℝ) : (circleMap 0 r θ).re = r * Real.cos θ

theorem circleMap_zero_im (r θ : ℝ) : (circleMap 0 r θ).im = r * Real.sin θ

theorem circleMap_pi_div_two (c : ℂ) (R : ℝ) : circleMap c R (Real.pi / 2) = c + ↑R * Complex.I

theorem circleMap_neg_pi_div_two (c : ℂ) (R : ℝ) : circleMap c R (-Real.pi / 2) = c - ↑R * Complex.I

theorem periodic_circleMap (c : ℂ) (R : ℝ) : Function.Periodic (circleMap c R) (2 * Real.pi)

circleMap is 2π-periodic.

theorem Set.Countable.preimage_circleMap {s : Set ℂ} (hs : s.Countable) (c : ℂ) {R : ℝ} (hR : R ≠ 0) : (circleMap c R ⁻¹' s).Countable

theorem circleMap_eq_circleMap_iff {a b R : ℝ} (c : ℂ) (h_R : R ≠ 0) : circleMap c R a = circleMap c R b ↔ ∃ (n : ℤ), ↑a * Complex.I = ↑b * Complex.I + ↑n * (2 * ↑Real.pi * Complex.I)

theorem eq_of_circleMap_eq {a b R : ℝ} {c : ℂ} (h_R : R ≠ 0) (h_dist : |a - b| < 2 * Real.pi) (h : circleMap c R a = circleMap c R b) : a = b

theorem injOn_circleMap_of_abs_sub_le {a b R : ℝ} {c : ℂ} (h_R : R ≠ 0) : |a - b| ≤ 2 * Real.pi → Set.InjOn (circleMap c R) (Set.uIoc a b)

circleMap is injective on Ι a b if the distance between a and b is at most 2π.

theorem injOn_circleMap_of_abs_sub_le' {a b R : ℝ} {c : ℂ} (h_R : R ≠ 0) : b - a ≤ 2 * Real.pi → Set.InjOn (circleMap c R) (Set.Ico a b)

circleMap is injective on Ico a b if the distance between a and b is at most 2π.