QuantumLib.Polar
Require Export Complex.
Definition get_arg (p : C) : R :=
match Rcase_abs (snd p) with
| left _ ⇒ 2 × PI - acos (fst p / Cmod p)
| right _ ⇒ acos (fst p / Cmod p)
end.
Definition rect_to_polar (z : C) : R × R :=
(Cmod z, get_arg z).
Definition polar_to_rect (p : R × R) : C :=
fst p × (Cexp (snd p)).
Definition WF_polar (p : R × R) : Prop :=
0 < fst p ∧ 0 ≤ snd p < 2 × PI.
Definition polar_mult (p1 p2 : R × R) : R × R :=
match Rcase_abs (snd p1 + snd p2 - 2 × PI) with
| left _ ⇒ (fst p1 × fst p2, snd p1 + snd p2)%R
| right _ ⇒ (fst p1 × fst p2, snd p1 + snd p2 - 2 × PI)%R
end.
Fixpoint polar_pow (p : R × R) (n : nat) : R × R :=
match n with
| O ⇒ (1, 0)%R
| S n' ⇒ polar_mult p (polar_pow p n')
end.
Lemma cos_2PI_minus_x : ∀ (x : R), cos (2 × PI - x) = cos x.
Lemma sin_2PI_minus_x : ∀ (x : R), sin (2 × PI - x) = (- sin x)%R.
Lemma fst_div_Cmod : ∀ (x y : R),
(x, y) ≠ C0 →
-1 ≤ x / Cmod (x, y) ≤ 1.
Lemma fst_div_Cmod_lt : ∀ (x y : R),
(y ≠ 0)%R →
-1 < x / Cmod (x, y) < 1.
Lemma get_arg_ver : ∀ (r θ : R),
0 < r → 0 ≤ θ < 2 × PI →
get_arg (r × Cexp θ) = θ.
Lemma get_arg_bound : ∀ (z : C),
0 ≤ get_arg z < 2 × PI.
Lemma polar_to_rect_to_polar : ∀ (p : R × R),
WF_polar p →
rect_to_polar (polar_to_rect p) = p.
Lemma div_subtract_helper : ∀ (x y : R),
(x, y) ≠ C0 →
(1 - (x / Cmod (x, y))²)%R = (y² × / (Cmod (x, y))²)%R.
Lemma rect_to_polar_to_rect : ∀ (z : C),
z ≠ C0 →
polar_to_rect (rect_to_polar z) = z.
Lemma WF_rect_to_polar : ∀ (z : C),
z ≠ C0 → WF_polar (rect_to_polar z).
Lemma WF_polar_mult : ∀ (p1 p2 : R × R),
WF_polar p1 → WF_polar p2 →
WF_polar (polar_mult p1 p2).
Lemma WF_polar_pow : ∀ (p : R × R) (n : nat),
WF_polar p →
WF_polar (polar_pow p n).
Lemma polar_to_rect_mult_compat : ∀ (p1 p2 : R × R),
WF_polar p1 → WF_polar p2 →
polar_to_rect (polar_mult p1 p2) = (polar_to_rect p1) × (polar_to_rect p2).
Lemma rect_to_polar_mult_compat : ∀ (z1 z2 : C),
z1 ≠ C0 → z2 ≠ C0 →
rect_to_polar (z1 × z2) = polar_mult (rect_to_polar z1) (rect_to_polar z2).
Lemma polar_to_rect_pow_compat : ∀ (p : R × R) (n : nat),
WF_polar p →
polar_to_rect (polar_pow p n) = (polar_to_rect p) ^ n.
Lemma rect_to_polar_pow_compat : ∀ (z : C) (n : nat),
z ≠ C0 →
rect_to_polar (z ^ n) = polar_pow (rect_to_polar z) n.
Definition pow_n (n : nat) : R → R :=
fun r ⇒ (r ^ n)%R.
Lemma pow_n_reduce : ∀ (n : nat),
mult_fct (pow_n 1) (pow_n n) = pow_n (S n).
Lemma continuous_const : continuity (pow_n 0).
Lemma continuous_linear : continuity (pow_n 1).
Lemma continuous_pow_n : ∀ (n : nat), continuity (pow_n n).
Lemma nth_root_nonnegR : ∀ (r : R) (n : nat),
0 ≤ r → (n > 0)%nat →
∃ r', 0 ≤ r' ∧ (r' ^ n = r)%R.
Lemma polar_pow_n : ∀ (r θ : R) (n : nat),
0 < r → 0 ≤ θ → (INR n × θ < 2 × PI)%R →
polar_pow (r, θ) n = (r ^ n, INR n × θ)%R.
Lemma nth_root_polar : ∀ (r θ : R) (n : nat),
(n > 0)%nat →
WF_polar (r, θ) →
∃ p, WF_polar p ∧ polar_pow p n = (r, θ).
Theorem nth_root_C : ∀ (z : C) (n : nat),
(n > 0)%nat →
∃ z', (Cpow z' n = z)%C.
Lemma nonzero_nth_root : ∀ (c c' : C) (n : nat),
(n > 0)%nat → c' ^ n = c →
c ≠ C0 →
c' ≠ C0.
Definition get_arg (p : C) : R :=
match Rcase_abs (snd p) with
| left _ ⇒ 2 × PI - acos (fst p / Cmod p)
| right _ ⇒ acos (fst p / Cmod p)
end.
Definition rect_to_polar (z : C) : R × R :=
(Cmod z, get_arg z).
Definition polar_to_rect (p : R × R) : C :=
fst p × (Cexp (snd p)).
Definition WF_polar (p : R × R) : Prop :=
0 < fst p ∧ 0 ≤ snd p < 2 × PI.
Definition polar_mult (p1 p2 : R × R) : R × R :=
match Rcase_abs (snd p1 + snd p2 - 2 × PI) with
| left _ ⇒ (fst p1 × fst p2, snd p1 + snd p2)%R
| right _ ⇒ (fst p1 × fst p2, snd p1 + snd p2 - 2 × PI)%R
end.
Fixpoint polar_pow (p : R × R) (n : nat) : R × R :=
match n with
| O ⇒ (1, 0)%R
| S n' ⇒ polar_mult p (polar_pow p n')
end.
Lemma cos_2PI_minus_x : ∀ (x : R), cos (2 × PI - x) = cos x.
Lemma sin_2PI_minus_x : ∀ (x : R), sin (2 × PI - x) = (- sin x)%R.
Lemma fst_div_Cmod : ∀ (x y : R),
(x, y) ≠ C0 →
-1 ≤ x / Cmod (x, y) ≤ 1.
Lemma fst_div_Cmod_lt : ∀ (x y : R),
(y ≠ 0)%R →
-1 < x / Cmod (x, y) < 1.
Lemma get_arg_ver : ∀ (r θ : R),
0 < r → 0 ≤ θ < 2 × PI →
get_arg (r × Cexp θ) = θ.
Lemma get_arg_bound : ∀ (z : C),
0 ≤ get_arg z < 2 × PI.
Lemma polar_to_rect_to_polar : ∀ (p : R × R),
WF_polar p →
rect_to_polar (polar_to_rect p) = p.
Lemma div_subtract_helper : ∀ (x y : R),
(x, y) ≠ C0 →
(1 - (x / Cmod (x, y))²)%R = (y² × / (Cmod (x, y))²)%R.
Lemma rect_to_polar_to_rect : ∀ (z : C),
z ≠ C0 →
polar_to_rect (rect_to_polar z) = z.
Lemma WF_rect_to_polar : ∀ (z : C),
z ≠ C0 → WF_polar (rect_to_polar z).
Lemma WF_polar_mult : ∀ (p1 p2 : R × R),
WF_polar p1 → WF_polar p2 →
WF_polar (polar_mult p1 p2).
Lemma WF_polar_pow : ∀ (p : R × R) (n : nat),
WF_polar p →
WF_polar (polar_pow p n).
Lemma polar_to_rect_mult_compat : ∀ (p1 p2 : R × R),
WF_polar p1 → WF_polar p2 →
polar_to_rect (polar_mult p1 p2) = (polar_to_rect p1) × (polar_to_rect p2).
Lemma rect_to_polar_mult_compat : ∀ (z1 z2 : C),
z1 ≠ C0 → z2 ≠ C0 →
rect_to_polar (z1 × z2) = polar_mult (rect_to_polar z1) (rect_to_polar z2).
Lemma polar_to_rect_pow_compat : ∀ (p : R × R) (n : nat),
WF_polar p →
polar_to_rect (polar_pow p n) = (polar_to_rect p) ^ n.
Lemma rect_to_polar_pow_compat : ∀ (z : C) (n : nat),
z ≠ C0 →
rect_to_polar (z ^ n) = polar_pow (rect_to_polar z) n.
Definition pow_n (n : nat) : R → R :=
fun r ⇒ (r ^ n)%R.
Lemma pow_n_reduce : ∀ (n : nat),
mult_fct (pow_n 1) (pow_n n) = pow_n (S n).
Lemma continuous_const : continuity (pow_n 0).
Lemma continuous_linear : continuity (pow_n 1).
Lemma continuous_pow_n : ∀ (n : nat), continuity (pow_n n).
Lemma nth_root_nonnegR : ∀ (r : R) (n : nat),
0 ≤ r → (n > 0)%nat →
∃ r', 0 ≤ r' ∧ (r' ^ n = r)%R.
Lemma polar_pow_n : ∀ (r θ : R) (n : nat),
0 < r → 0 ≤ θ → (INR n × θ < 2 × PI)%R →
polar_pow (r, θ) n = (r ^ n, INR n × θ)%R.
Lemma nth_root_polar : ∀ (r θ : R) (n : nat),
(n > 0)%nat →
WF_polar (r, θ) →
∃ p, WF_polar p ∧ polar_pow p n = (r, θ).
Theorem nth_root_C : ∀ (z : C) (n : nat),
(n > 0)%nat →
∃ z', (Cpow z' n = z)%C.
Lemma nonzero_nth_root : ∀ (c c' : C) (n : nat),
(n > 0)%nat → c' ^ n = c →
c ≠ C0 →
c' ≠ C0.