# 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 #

source
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)

Instances For

source
@[simp]
theorem circleMap_sub_center (c : ℂ) (R θ : ℝ) :
circleMap c R θ - c = circleMap 0 R θ
source
theorem circleMap_zero (R θ : ℝ) :
circleMap 0 R θ = ↑R * Complex.exp (↑θ * Complex.I)
source
@[simp]
theorem norm_circleMap_zero (R θ : ℝ) :
‖circleMap 0 R θ‖ = |R|
source
theorem circleMap_notMem_ball (c : ℂ) (R θ : ℝ) :
circleMap c R θ ∉ Metric.ball c R
source
@[deprecated circleMap_notMem_ball (since := "2025-05-23")]
theorem circleMap_not_mem_ball (c : ℂ) (R θ : ℝ) :
circleMap c R θ ∉ Metric.ball c R

Alias of `circleMap_notMem_ball`.

source
theorem circleMap_ne_mem_ball {c : ℂ} {R : ℝ} {w : ℂ} (hw : w ∈ Metric.ball c R) (θ : ℝ) :
circleMap c R θ ≠ w
source
theorem circleMap_mem_sphere' (c : ℂ) (R θ : ℝ) :
circleMap c R θ ∈ Metric.sphere c |R|
source
theorem circleMap_mem_sphere (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (θ : ℝ) :
circleMap c R θ ∈ Metric.sphere c R
source
theorem circleMap_mem_closedBall (c : ℂ) {R : ℝ} (hR : 0 ≤ R) (θ : ℝ) :
circleMap c R θ ∈ Metric.closedBall c R
source
@[simp]
theorem circleMap_eq_center_iff {c : ℂ} {R θ : ℝ} :
circleMap c R θ = c ↔ R = 0
source
@[simp]
theorem circleMap_zero_radius (c : ℂ) :
circleMap c 0 = Function.const ℝ c
source
theorem circleMap_ne_center {c : ℂ} {R : ℝ} (hR : R ≠ 0) {θ : ℝ} :
circleMap c R θ ≠ c
source
theorem circleMap_zero_mul (R₁ R₂ θ₁ θ₂ : ℝ) :
circleMap 0 R₁ θ₁ * circleMap 0 R₂ θ₂ = circleMap 0 (R₁ * R₂) (θ₁ + θ₂)
source
theorem circleMap_zero_div (R₁ R₂ θ₁ θ₂ : ℝ) :
circleMap 0 R₁ θ₁ / circleMap 0 R₂ θ₂ = circleMap 0 (R₁ / R₂) (θ₁ - θ₂)
source
theorem circleMap_zero_inv (R θ : ℝ) :
(circleMap 0 R θ)⁻¹ = circleMap 0 R⁻¹ (-θ)
source
theorem circleMap_zero_pow (n : ℕ) (R θ : ℝ) :
circleMap 0 R θ ^ n = circleMap 0 (R ^ n) (↑n * θ)
source
theorem circleMap_zero_zpow (n : ℤ) (R θ : ℝ) :
circleMap 0 R θ ^ n = circleMap 0 (R ^ n) (↑n * θ)
source
theorem circleMap_pi_div_two (c : ℂ) (R : ℝ) :
circleMap c R (Real.pi / 2) = c + ↑R * Complex.I
source
theorem circleMap_neg_pi_div_two (c : ℂ) (R : ℝ) :
circleMap c R (-Real.pi / 2) = c - ↑R * Complex.I
source
theorem periodic_circleMap (c : ℂ) (R : ℝ) :
Function.Periodic (circleMap c R) (2 * Real.pi)

`circleMap` is `2π`-periodic.

source
theorem Set.Countable.preimage_circleMap {s : Set ℂ} (hs : s.Countable) (c : ℂ) {R : ℝ} (hR : R ≠ 0) :
(circleMap c R ⁻¹' s).Countable
source
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)
source
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
source
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π`.

source
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π`.