Trigonometric Parametrization for a^2 + b^2 = 1 in Mathlib

Stream: mathlib4

[Zhu]

Hi everyone,

While working on a formalization project, I encountered the need for a lemma stating that if $a^2+b^2=1$, then there exists an angle $\theta$ such that a = $\cos \theta$ and $b = \sin \theta$. I couldn't find a corresponding result in mathlib, so I ended up writing the lemma myself.

I'm wondering:

1. Is there already a similar lemma in mathlib that I might have missed?

2. If not, would it be reasonable to propose adding this result? It seems like a natural and useful lemma.

here's my code

-- lemma : if $a ^ 2 + b ^ 2 = 1$, then there exists $\theta$ where $a = \cos \theta$ and $b = \sin \theta$
lemma l_1 {a b : ℝ} (h : a ^ 2 + b ^ 2 = 1) : ∃ θ, a = cos θ ∧ b = sin θ := by
  have rab : (-1 ≤ a ∧ a ≤ 1) ∧ (-1 ≤ b ∧ b ≤ 1) := by
    constructor
    all_goals
      apply abs_le.mp
      apply (sq_le_one_iff_abs_le_one _).mp
      linarith [sq_nonneg b, sq_nonneg a]
  set θ := arccos a
  have : 0 ≤ sin θ := sin_nonneg_of_nonneg_of_le_pi (arccos_nonneg a) (arccos_le_pi a)
  have ra : a = cos θ := by
    rw [Real.cos_arccos]
    all_goals simp only [rab]
  have rb : |b| = |sin θ| := by
    apply (sq_eq_sq_iff_abs_eq_abs _ _).mp
    rw [sin_sq θ, ← ra]
    linarith
  rcases le_or_lt 0 a with ha | ha
  . rcases le_or_lt 0 b with hb | hb
    . use θ
      simp [ra]
      repeat rw [abs_of_nonneg] at rb
      all_goals linarith
    . use -θ
      simp [ra]
      rw [abs_of_neg, abs_of_nonneg] at rb
      all_goals linarith
  . rcases le_or_lt 0 b with hb | hb
    . use θ
      simp [ra]
      repeat rw [abs_of_nonneg, abs_of_nonneg] at rb
      all_goals linarith
    . use -θ
      simp [ra]
      rw [abs_of_neg, abs_of_nonneg] at rb
      all_goals linarith

[Zhu]

By the way, is there a better way to structure this proof? It feels repetitive in handling cases.

[Scott Carnahan]

One problem is that your use of arccos means there is a sign ambiguity. One trick, often used when parametrizing Pythagorean triples, is to consider the line connecting (-1,0) to (a,b), since its slope is tan θ/2.

[Ruben Van de Velde]

I'm surprised to say that this seems to be legitimately missing

[Heather Macbeth]

You can get it indirectly from polar co-ordinates:

import Mathlib
open Real

lemma l_1 {a b : ℝ} (h : a ^ 2 + b ^ 2 = 1) : ∃ θ, a = cos θ ∧ b = sin θ := by
  by_cases degen : (a, b) ∈ polarCoord.source
  · set p := polarCoord (a, b)
    use p.2
    have H :=
      calc p.1 = √ (a^2 + b^2) := rfl
        _ = 1 := by simp [h]
    have hp : polarCoord.symm p = (a, b) := PartialEquiv.left_inv _ degen
    simpa [polarCoord_symm_apply, H]  using hp.symm
  · simp only [polarCoord_source, Set.mem_union, Set.mem_setOf_eq, not_or, not_lt, not_not] at degen
    obtain rfl : b = 0 := degen.2
    obtain rfl : a = -1 := by nlinarith
    use π
    simp

[Eric Wieser]

Or via complex numbers, with docs#Complex.abs_eq_one_iff

lemma l_1 {a b : ℝ} (h : a ^ 2 + b ^ 2 = 1) : ∃ θ, a = Real.cos θ ∧ b = Real.sin θ := by
  let z : ℂ := ⟨a, b⟩ -- note: not supposed to use this constructor
  have : z.abs = 1 := by
    rw [Complex.abs_eq_sqrt_sq_add_sq]
    erw [h]
    rw [Real.sqrt_one]
  simp_rw [Complex.abs_eq_one_iff, Complex.ext_iff, Complex.exp_ofReal_mul_I_re, Complex.exp_ofReal_mul_I_im] at this
  simpa [eq_comm]

[Zhu]

Ruben Van de Velde said:

I'm surprised to say that this seems to be legitimately missing

True, I think that's reasonable.