Documentation

Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

circleMap #

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

Main definitions #

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
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
    @[deprecated circleMap_zero_zpow (since := "2025-04-02")]
    theorem circleMap_zero_int_mul (n : ℤ) (R θ : ℝ) :
    circleMap 0 R θ ^ n = circleMap 0 (R ^ n) (↑n * θ)

    Alias of circleMap_zero_zpow.

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