mathlib documentation

analysis.special_functions.trigonometric.angle

The type of angles #

In this file we define real.angle to be the quotient group ℝ/2πℤ and prove a few simple lemmas about trigonometric functions and angles.

@[protected, instance]

noncomputable def real.angle.add_comm_group :

add_comm_group real.angle

@[protected, instance]

noncomputable def real.angle.topological_space :

topological_space real.angle

@[protected, instance]

def real.angle.topological_add_group :

topological_add_group real.angle

def real.angle :

Type

The type of angles

Equations

real.angle = (ℝ ⧸ add_subgroup.zmultiples (2 * real.pi))

Instances for real.angle

@[protected, instance]

noncomputable def real.angle.inhabited :

inhabited real.angle

Equations

real.angle.inhabited = {default := 0}

@[protected, instance]

noncomputable def real.angle.has_coe :

has_coe ℝ real.angle

Equations

real.angle.has_coe = {coe := ⇑(quotient_add_group.mk' (add_subgroup.zmultiples (2 * real.pi)))}

@[continuity]

theorem real.angle.continuous_coe :

noncomputable def real.angle.coe_hom :

ℝ →+ real.angle

Coercion ℝ → angle as an additive homomorphism.

Equations

real.angle.coe_hom = quotient_add_group.mk' (add_subgroup.zmultiples (2 * real.pi))

@[simp]

theorem real.angle.coe_coe_hom :

⇑real.angle.coe_hom = coe

@[protected]

theorem real.angle.induction_on {p : real.angle → Prop} (θ : real.angle) (h : ∀ (x : ℝ), p ↑x) :

p θ

An induction principle to deduce results for angle from those for ℝ, used with induction θ using real.angle.induction_on.

@[simp]

theorem real.angle.coe_zero :

↑0 = 0

@[simp]

theorem real.angle.coe_add (x y : ℝ) :

↑(x + y) = ↑x + ↑y

@[simp]

theorem real.angle.coe_neg (x : ℝ) :

@[simp]

theorem real.angle.coe_sub (x y : ℝ) :

↑(x - y) = ↑x - ↑y

theorem real.angle.coe_nsmul (n : ℕ) (x : ℝ) :

↑(n • x) = n • ↑x

theorem real.angle.coe_zsmul (z : ℤ) (x : ℝ) :

↑(z • x) = z • ↑x

@[simp, norm_cast]

theorem real.angle.coe_nat_mul_eq_nsmul (x : ℝ) (n : ℕ) :

↑(↑n * x) = n • ↑x

@[simp, norm_cast]

theorem real.angle.coe_int_mul_eq_zsmul (x : ℝ) (n : ℤ) :

↑(↑n * x) = n • ↑x

theorem real.angle.angle_eq_iff_two_pi_dvd_sub {ψ θ : ℝ} :

↑θ = ↑ψ ↔ ∃ (k : ℤ), θ - ψ = 2 * real.pi * ↑k

@[simp]

theorem real.angle.coe_two_pi :

↑(2 * real.pi) = 0

@[simp]

theorem real.angle.neg_coe_pi :

-↑real.pi = ↑real.pi

theorem real.angle.sub_coe_pi_eq_add_coe_pi (θ : real.angle) :

θ - ↑real.pi = θ + ↑real.pi

@[simp]

theorem real.angle.two_nsmul_coe_pi :

2 • ↑real.pi = 0

@[simp]

theorem real.angle.two_zsmul_coe_pi :

2 • ↑real.pi = 0

@[simp]

theorem real.angle.coe_pi_add_coe_pi :

↑real.pi + ↑real.pi = 0

theorem real.angle.zsmul_eq_iff {ψ θ : real.angle} {z : ℤ} (hz : z ≠ 0) :

z • ψ = z • θ ↔ ∃ (k : fin z.nat_abs), ψ = θ + ↑k • ↑(2 * real.pi / ↑z)

theorem real.angle.nsmul_eq_iff {ψ θ : real.angle} {n : ℕ} (hz : n ≠ 0) :

n • ψ = n • θ ↔ ∃ (k : fin n), ψ = θ + ↑k • ↑(2 * real.pi / ↑n)

theorem real.angle.two_zsmul_eq_iff {ψ θ : real.angle} :

2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑real.pi

theorem real.angle.two_nsmul_eq_iff {ψ θ : real.angle} :

2 • ψ = 2 • θ ↔ ψ = θ ∨ ψ = θ + ↑real.pi

theorem real.angle.two_nsmul_eq_zero_iff {θ : real.angle} :

2 • θ = 0 ↔ θ = 0 ∨ θ = ↑real.pi

theorem real.angle.two_nsmul_ne_zero_iff {θ : real.angle} :

2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑real.pi

theorem real.angle.two_zsmul_eq_zero_iff {θ : real.angle} :

2 • θ = 0 ↔ θ = 0 ∨ θ = ↑real.pi

theorem real.angle.two_zsmul_ne_zero_iff {θ : real.angle} :

2 • θ ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑real.pi

theorem real.angle.eq_neg_self_iff {θ : real.angle} :

θ = -θ ↔ θ = 0 ∨ θ = ↑real.pi

theorem real.angle.ne_neg_self_iff {θ : real.angle} :

θ ≠ -θ ↔ θ ≠ 0 ∧ θ ≠ ↑real.pi

theorem real.angle.neg_eq_self_iff {θ : real.angle} :

-θ = θ ↔ θ = 0 ∨ θ = ↑real.pi

theorem real.angle.neg_ne_self_iff {θ : real.angle} :

-θ ≠ θ ↔ θ ≠ 0 ∧ θ ≠ ↑real.pi

theorem real.angle.cos_eq_iff_coe_eq_or_eq_neg {θ ψ : ℝ} :

real.cos θ = real.cos ψ ↔ ↑θ = ↑ψ ∨ ↑θ = -↑ψ

theorem real.angle.sin_eq_iff_coe_eq_or_add_eq_pi {θ ψ : ℝ} :

real.sin θ = real.sin ψ ↔ ↑θ = ↑ψ ∨ ↑θ + ↑ψ = ↑real.pi

theorem real.angle.cos_sin_inj {θ ψ : ℝ} (Hcos : real.cos θ = real.cos ψ) (Hsin : real.sin θ = real.sin ψ) :

noncomputable def real.angle.sin (θ : real.angle) :

The sine of a real.angle.

Equations

θ.sin = real.sin_periodic.lift θ

@[simp]

theorem real.angle.sin_coe (x : ℝ) :

↑x.sin = real.sin x

@[continuity]

theorem real.angle.continuous_sin :

continuous real.angle.sin

noncomputable def real.angle.cos (θ : real.angle) :

The cosine of a real.angle.

Equations

θ.cos = real.cos_periodic.lift θ

@[simp]

theorem real.angle.cos_coe (x : ℝ) :

↑x.cos = real.cos x

@[continuity]

theorem real.angle.continuous_cos :

continuous real.angle.cos

theorem real.angle.cos_eq_real_cos_iff_eq_or_eq_neg {θ : real.angle} {ψ : ℝ} :

θ.cos = real.cos ψ ↔ θ = ↑ψ ∨ θ = -↑ψ

theorem real.angle.cos_eq_iff_eq_or_eq_neg {θ ψ : real.angle} :

θ.cos = ψ.cos ↔ θ = ψ ∨ θ = -ψ

theorem real.angle.sin_eq_real_sin_iff_eq_or_add_eq_pi {θ : real.angle} {ψ : ℝ} :

θ.sin = real.sin ψ ↔ θ = ↑ψ ∨ θ + ↑ψ = ↑real.pi

theorem real.angle.sin_eq_iff_eq_or_add_eq_pi {θ ψ : real.angle} :

θ.sin = ψ.sin ↔ θ = ψ ∨ θ + ψ = ↑real.pi

@[simp]

theorem real.angle.sin_zero :

0.sin = 0

@[simp]

theorem real.angle.sin_coe_pi :

↑real.pi.sin = 0

theorem real.angle.sin_eq_zero_iff {θ : real.angle} :

θ.sin = 0 ↔ θ = 0 ∨ θ = ↑real.pi

theorem real.angle.sin_ne_zero_iff {θ : real.angle} :

θ.sin ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑real.pi

@[simp]

theorem real.angle.sin_neg (θ : real.angle) :

(-θ).sin = -θ.sin

theorem real.angle.sin_antiperiodic :

function.antiperiodic real.angle.sin ↑real.pi

@[simp]

theorem real.angle.sin_add_pi (θ : real.angle) :

(θ + ↑real.pi).sin = -θ.sin

@[simp]

theorem real.angle.sin_sub_pi (θ : real.angle) :

(θ - ↑real.pi).sin = -θ.sin

@[simp]

theorem real.angle.cos_zero :

0.cos = 1

@[simp]

theorem real.angle.cos_coe_pi :

↑real.pi.cos = -1

@[simp]

theorem real.angle.cos_neg (θ : real.angle) :

(-θ).cos = θ.cos

theorem real.angle.cos_antiperiodic :

function.antiperiodic real.angle.cos ↑real.pi

@[simp]

theorem real.angle.cos_add_pi (θ : real.angle) :

(θ + ↑real.pi).cos = -θ.cos

@[simp]

theorem real.angle.cos_sub_pi (θ : real.angle) :

(θ - ↑real.pi).cos = -θ.cos

@[simp]

theorem real.angle.coe_to_Ico_mod (θ ψ : ℝ) :

↑(to_Ico_mod ψ real.two_pi_pos θ) = ↑θ

@[simp]

theorem real.angle.coe_to_Ioc_mod (θ ψ : ℝ) :

↑(to_Ioc_mod ψ real.two_pi_pos θ) = ↑θ

noncomputable def real.angle.to_real (θ : real.angle) :

Convert a real.angle to a real number in the interval Ioc (-π) π.

Equations

θ.to_real = real.angle.to_real._proof_1.lift θ

theorem real.angle.to_real_coe (θ : ℝ) :

↑θ.to_real = to_Ioc_mod (-real.pi) real.two_pi_pos θ

theorem real.angle.to_real_coe_eq_self_iff {θ : ℝ} :

↑θ.to_real = θ ↔ -real.pi < θ ∧ θ ≤ real.pi

theorem real.angle.to_real_coe_eq_self_iff_mem_Ioc {θ : ℝ} :

↑θ.to_real = θ ↔ θ ∈ set.Ioc (-real.pi) real.pi

theorem real.angle.to_real_injective :

function.injective real.angle.to_real

@[simp]

theorem real.angle.to_real_inj {θ ψ : real.angle} :

θ.to_real = ψ.to_real ↔ θ = ψ

@[simp]

theorem real.angle.coe_to_real (θ : real.angle) :

↑(θ.to_real) = θ

theorem real.angle.neg_pi_lt_to_real (θ : real.angle) :

-real.pi < θ.to_real

theorem real.angle.to_real_le_pi (θ : real.angle) :

θ.to_real ≤ real.pi

theorem real.angle.abs_to_real_le_pi (θ : real.angle) :

|θ.to_real | ≤ real.pi

theorem real.angle.to_real_mem_Ioc (θ : real.angle) :

θ.to_real ∈ set.Ioc (-real.pi) real.pi

@[simp]

theorem real.angle.to_Ioc_mod_to_real (θ : real.angle) :

to_Ioc_mod (-real.pi) real.two_pi_pos θ.to_real = θ.to_real

@[simp]

theorem real.angle.to_real_zero :

@[simp]

theorem real.angle.to_real_eq_zero_iff {θ : real.angle} :

θ.to_real = 0 ↔ θ = 0

@[simp]

theorem real.angle.to_real_pi :

↑real.pi.to_real = real.pi

@[simp]

theorem real.angle.to_real_eq_pi_iff {θ : real.angle} :

θ.to_real = real.pi ↔ θ = ↑real.pi

theorem real.angle.pi_ne_zero :

↑real.pi ≠ 0

theorem real.angle.abs_to_real_coe_eq_self_iff {θ : ℝ} :

|↑θ.to_real | = θ ↔ 0 ≤ θ ∧ θ ≤ real.pi

theorem real.angle.abs_to_real_neg_coe_eq_self_iff {θ : ℝ} :

|(-↑θ).to_real | = θ ↔ 0 ≤ θ ∧ θ ≤ real.pi

@[simp]

theorem real.angle.sin_to_real (θ : real.angle) :

real.sin θ.to_real = θ.sin

@[simp]

theorem real.angle.cos_to_real (θ : real.angle) :

real.cos θ.to_real = θ.cos

noncomputable def real.angle.sign (θ : real.angle) :

The sign of a real.angle is 0 if the angle is 0 or π, 1 if the angle is strictly between 0 and π and -1 is the angle is strictly between -π and 0. It is defined as the sign of the sine of the angle.

Equations

θ.sign = ⇑sign θ.sin

@[simp]

theorem real.angle.sign_zero :

0.sign = 0

@[simp]

theorem real.angle.sign_coe_pi :

↑real.pi.sign = 0

@[simp]

theorem real.angle.sign_neg (θ : real.angle) :

(-θ).sign = -θ.sign

theorem real.angle.sign_antiperiodic :

function.antiperiodic real.angle.sign ↑real.pi

@[simp]

theorem real.angle.sign_add_pi (θ : real.angle) :

(θ + ↑real.pi).sign = -θ.sign

@[simp]

theorem real.angle.sign_pi_add (θ : real.angle) :

(↑real.pi + θ).sign = -θ.sign

@[simp]

theorem real.angle.sign_sub_pi (θ : real.angle) :

(θ - ↑real.pi).sign = -θ.sign

@[simp]

theorem real.angle.sign_pi_sub (θ : real.angle) :

(↑real.pi - θ).sign = θ.sign

theorem real.angle.sign_eq_zero_iff {θ : real.angle} :

θ.sign = 0 ↔ θ = 0 ∨ θ = ↑real.pi

theorem real.angle.sign_ne_zero_iff {θ : real.angle} :

θ.sign ≠ 0 ↔ θ ≠ 0 ∧ θ ≠ ↑real.pi

theorem real.angle.to_real_neg_iff_sign_neg {θ : real.angle} :

θ.to_real < 0 ↔ θ.sign = -1

theorem real.angle.to_real_nonneg_iff_sign_nonneg {θ : real.angle} :

0 ≤ θ.to_real ↔ 0 ≤ θ.sign

@[simp]

theorem real.angle.sign_to_real {θ : real.angle} (h : θ ≠ ↑real.pi) :

⇑sign θ.to_real = θ.sign

theorem real.angle.coe_abs_to_real_of_sign_nonneg {θ : real.angle} (h : 0 ≤ θ.sign) :

↑|θ.to_real | = θ

theorem real.angle.neg_coe_abs_to_real_of_sign_nonpos {θ : real.angle} (h : θ.sign ≤ 0) :

-↑|θ.to_real | = θ

theorem real.angle.eq_iff_sign_eq_and_abs_to_real_eq {θ ψ : real.angle} :

θ = ψ ↔ θ.sign = ψ.sign ∧ |θ.to_real | = |ψ.to_real |

theorem real.angle.eq_iff_abs_to_real_eq_of_sign_eq {θ ψ : real.angle} (h : θ.sign = ψ.sign) :

θ = ψ ↔ |θ.to_real | = |ψ.to_real |

theorem real.angle.continuous_at_sign {θ : real.angle} (h0 : θ ≠ 0) (hpi : θ ≠ ↑real.pi) :

continuous_at real.angle.sign θ

theorem continuous_on.angle_sign_comp {α : Type u_1} [topological_space α] {f : α → real.angle} {s : set α} (hf : continuous_on f s) (hs : ∀ (z : α), z ∈ s → f z ≠ 0 ∧ f z ≠ ↑real.pi) :

continuous_on (real.angle.sign ∘ f) s

theorem real.angle.sign_eq_of_continuous_on {α : Type u_1} [topological_space α] {f : α → real.angle} {s : set α} {x y : α} (hc : is_connected s) (hf : continuous_on f s) (hs : ∀ (z : α), z ∈ s → f z ≠ 0 ∧ f z ≠ ↑real.pi) (hx : x ∈ s) (hy : y ∈ s) :

(f y).sign = (f x).sign

Suppose a function to angles is continuous on a connected set and never takes the values 0 or π on that set. Then the values of the function on that set all have the same sign.