Documentation

Mathlib.Analysis.SpecialFunctions.Complex.CircleMap

circleMap #

This file defines the circle map θc+Reθi, a parametrization of a circle.

Main definitions #

Tags #

def circleMap (c : ) (R : ) :

The exponential map θc+Reθi. The range of this map is the circle in with center c and radius |R|.

Equations
@[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 θ : ) :
@[deprecated norm_circleMap_zero (since := "2025-02-17")]
theorem abs_circleMap_zero (R θ : ) :

Alias of norm_circleMap_zero.

theorem circleMap_notMem_ball (c : ) (R θ : ) :
circleMap c R θMetric.ball c R
@[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.

theorem circleMap_ne_mem_ball {c : } {R : } {w : } (hw : w Metric.ball c R) (θ : ) :
circleMap c R θ w
theorem circleMap_mem_sphere' (c : ) (R θ : ) :
theorem circleMap_mem_sphere (c : ) {R : } (hR : 0 R) (θ : ) :
theorem circleMap_mem_closedBall (c : ) {R : } (hR : 0 R) (θ : ) :
@[simp]
theorem circleMap_eq_center_iff {c : } {R θ : } :
circleMap c R θ = c R = 0
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 * θ)
@[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.

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

circleMap is -periodic.

theorem Set.Countable.preimage_circleMap {s : Set } (hs : s.Countable) (c : ) {R : } (hR : R 0) :
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.piSet.InjOn (circleMap c R) (Set.uIoc a b)

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

theorem injOn_circleMap_of_abs_sub_le' {a b R : } {c : } (h_R : R 0) :
b - a 2 * Real.piSet.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 .