QuantumLib.FTA
Require Import Polar.
Require Export Ctopology.
Require Import Setoid.
Definition poly_coef_norm (p : Polynomial) : R :=
big_sum (fun i ⇒ Cmod (nth i p C0)) (length p).
Lemma poly_coef_norm_ge_0 : ∀ (p : Polynomial),
0 ≤ poly_coef_norm p.
Lemma norm_0_iff_0 : ∀ (p : Polynomial),
p ≅ [] ↔ poly_coef_norm p = 0.
Lemma poly_coef_norm_compactify : ∀ (p : Polynomial),
poly_coef_norm p = poly_coef_norm (compactify p).
Add Parametric Morphism : poly_coef_norm
with signature Peq ==> eq as polycoefnorm_mor.
Lemma poly_bound_ge_1 : ∀ (p : Polynomial) (z : C),
1 ≤ Cmod z →
Cmod (p[[z]]) ≤ (poly_coef_norm p) × (Cmod z)^(length p - 1).
Lemma poly_bound_le_1 : ∀ (p : Polynomial) (z : C),
Cmod z ≤ 1 →
Cmod ((C0 :: p)[[z]]) ≤ (poly_coef_norm p) × (Cmod z).
Lemma half_norm_bound : ∀ (c z : C),
(Cmod c < (Cmod z) × /2)%R →
((Cmod z) × /2 < Cmod (z + c))%R.
Lemma leading_term_dom : ∀ (p : Polynomial) (a c : C),
a ≠ C0 →
Cmod c > (2 × poly_coef_norm p / (Cmod a))%R → Cmod c > 1 →
Cmod p[[c]] < Cmod (a × c^(length p)) /2.
Lemma poly_bound_leading_term : ∀ (p : Polynomial) (a : C),
a ≠ C0 →
∃ r, (∀ c, Cmod c > r → Cmod (p ++ [a])[[c]] > Cmod (a × c^(length p)) × /2).
Lemma x_to_n_bounded_below : ∀ (a c : C) (M : R) (n : nat),
a ≠ C0 → n ≠ 0%nat →
Cmod c > Rmax (2 × (M / Cmod a)) 1 →
Cmod (a × c^n) × /2 > M.
Lemma poly_to_inf_uniformly : ∀ (p : Polynomial) (M : R),
(Polynomial.degree p > 0)%nat →
∃ r, r > 0 ∧ (∀ c, Cmod c > r → Cmod p[[c]] > M).
Lemma poly_compact_closed_ball : ∀ (p : Polynomial) (r : R),
compact ((Peval p) @ (fun c' ⇒ Cmod (c') ≤ r)).
Lemma poly_min : ∀ (p : Polynomial),
∃ m, (∀ c, Cmod p[[m]] ≤ Cmod p[[c]]).
Lemma first_nonzero_coef : ∀ (p : Polynomial),
Peval p ≠ Peval [] →
∃ a n p', a ≠ C0 ∧ p = (repeat C0 n) ++ [a] ++ p'.
Lemma eval_x_to_n_plus_a : ∀ (z a0 ak : C) (ϵ : R) (k : nat),
a0 ≠ C0 → ak ≠ C0 → 0 < ϵ < 1 →
z ^ (k + 1) = (-a0 / ak) →
Cmod ((a0 :: repeat C0 k) ++ [ak]) [[ϵ × z]] = ((Cmod a0) × (1 - ϵ ^ (k + 1)))%R.
Lemma bound_lemma1 : ∀ (z a0 ak : C) (ϵ : R) (k : nat) (p : Polynomial),
a0 ≠ C0 → ak ≠ C0 → 0 < ϵ < 1 →
z ^ (k + 1) = (-a0 / ak) →
ϵ × Cmod z ≤ 1 →
Cmod (a0 :: (repeat C0 k) ++ [ak] ++ p)[[ϵ × z]] ≤
(Cmod a0) × (1 - ϵ^(k + 1)) + (poly_coef_norm p) × Cmod (z ^ (k + 2)) × ϵ^(k + 2).
Lemma bound_lemma2 : ∀ (z a0 ak : C) (ϵ : R) (k : nat) (p : Polynomial),
a0 ≠ C0 → ak ≠ C0 → 0 < ϵ < 1 →
Peval p ≠ Peval [] →
z ^ (k + 1) = (-a0 / ak) →
ϵ ≤ 1 × / Cmod z →
ϵ < (Cmod a0) / ((poly_coef_norm p) × (Cmod z) ^ (k + 2)) →
(Cmod a0) × (1 - ϵ^(k + 1)) + (poly_coef_norm p) × Cmod (z ^ (k + 2)) × ϵ^(k + 2) <
Cmod a0.
Lemma get_smaller_norm_output : ∀ (a0 ak : C) (k : nat) (p : Polynomial),
a0 ≠ C0 → ak ≠ C0 →
∃ c, Cmod (a0 :: (repeat C0 k) ++ [ak] ++ p)[[c]] < Cmod a0.
Lemma FTA_min_at_0 : ∀ (p : Polynomial) (a : C),
(Polynomial.degree (a :: p) > 0)%nat →
(∀ c, Cmod (a :: p)[[C0]] ≤ Cmod (a :: p)[[c]]) →
a = C0.
Theorem Fundamental_Theorem_Algebra : ∀ (p : Polynomial),
(Polynomial.degree p > 0)%nat → (∃ c : Complex.C, p[[c]] = C0).
Require Export Ctopology.
Require Import Setoid.
Definition poly_coef_norm (p : Polynomial) : R :=
big_sum (fun i ⇒ Cmod (nth i p C0)) (length p).
Lemma poly_coef_norm_ge_0 : ∀ (p : Polynomial),
0 ≤ poly_coef_norm p.
Lemma norm_0_iff_0 : ∀ (p : Polynomial),
p ≅ [] ↔ poly_coef_norm p = 0.
Lemma poly_coef_norm_compactify : ∀ (p : Polynomial),
poly_coef_norm p = poly_coef_norm (compactify p).
Add Parametric Morphism : poly_coef_norm
with signature Peq ==> eq as polycoefnorm_mor.
Lemma poly_bound_ge_1 : ∀ (p : Polynomial) (z : C),
1 ≤ Cmod z →
Cmod (p[[z]]) ≤ (poly_coef_norm p) × (Cmod z)^(length p - 1).
Lemma poly_bound_le_1 : ∀ (p : Polynomial) (z : C),
Cmod z ≤ 1 →
Cmod ((C0 :: p)[[z]]) ≤ (poly_coef_norm p) × (Cmod z).
Lemma half_norm_bound : ∀ (c z : C),
(Cmod c < (Cmod z) × /2)%R →
((Cmod z) × /2 < Cmod (z + c))%R.
Lemma leading_term_dom : ∀ (p : Polynomial) (a c : C),
a ≠ C0 →
Cmod c > (2 × poly_coef_norm p / (Cmod a))%R → Cmod c > 1 →
Cmod p[[c]] < Cmod (a × c^(length p)) /2.
Lemma poly_bound_leading_term : ∀ (p : Polynomial) (a : C),
a ≠ C0 →
∃ r, (∀ c, Cmod c > r → Cmod (p ++ [a])[[c]] > Cmod (a × c^(length p)) × /2).
Lemma x_to_n_bounded_below : ∀ (a c : C) (M : R) (n : nat),
a ≠ C0 → n ≠ 0%nat →
Cmod c > Rmax (2 × (M / Cmod a)) 1 →
Cmod (a × c^n) × /2 > M.
Lemma poly_to_inf_uniformly : ∀ (p : Polynomial) (M : R),
(Polynomial.degree p > 0)%nat →
∃ r, r > 0 ∧ (∀ c, Cmod c > r → Cmod p[[c]] > M).
Lemma poly_compact_closed_ball : ∀ (p : Polynomial) (r : R),
compact ((Peval p) @ (fun c' ⇒ Cmod (c') ≤ r)).
Lemma poly_min : ∀ (p : Polynomial),
∃ m, (∀ c, Cmod p[[m]] ≤ Cmod p[[c]]).
Lemma first_nonzero_coef : ∀ (p : Polynomial),
Peval p ≠ Peval [] →
∃ a n p', a ≠ C0 ∧ p = (repeat C0 n) ++ [a] ++ p'.
Lemma eval_x_to_n_plus_a : ∀ (z a0 ak : C) (ϵ : R) (k : nat),
a0 ≠ C0 → ak ≠ C0 → 0 < ϵ < 1 →
z ^ (k + 1) = (-a0 / ak) →
Cmod ((a0 :: repeat C0 k) ++ [ak]) [[ϵ × z]] = ((Cmod a0) × (1 - ϵ ^ (k + 1)))%R.
Lemma bound_lemma1 : ∀ (z a0 ak : C) (ϵ : R) (k : nat) (p : Polynomial),
a0 ≠ C0 → ak ≠ C0 → 0 < ϵ < 1 →
z ^ (k + 1) = (-a0 / ak) →
ϵ × Cmod z ≤ 1 →
Cmod (a0 :: (repeat C0 k) ++ [ak] ++ p)[[ϵ × z]] ≤
(Cmod a0) × (1 - ϵ^(k + 1)) + (poly_coef_norm p) × Cmod (z ^ (k + 2)) × ϵ^(k + 2).
Lemma bound_lemma2 : ∀ (z a0 ak : C) (ϵ : R) (k : nat) (p : Polynomial),
a0 ≠ C0 → ak ≠ C0 → 0 < ϵ < 1 →
Peval p ≠ Peval [] →
z ^ (k + 1) = (-a0 / ak) →
ϵ ≤ 1 × / Cmod z →
ϵ < (Cmod a0) / ((poly_coef_norm p) × (Cmod z) ^ (k + 2)) →
(Cmod a0) × (1 - ϵ^(k + 1)) + (poly_coef_norm p) × Cmod (z ^ (k + 2)) × ϵ^(k + 2) <
Cmod a0.
Lemma get_smaller_norm_output : ∀ (a0 ak : C) (k : nat) (p : Polynomial),
a0 ≠ C0 → ak ≠ C0 →
∃ c, Cmod (a0 :: (repeat C0 k) ++ [ak] ++ p)[[c]] < Cmod a0.
Lemma FTA_min_at_0 : ∀ (p : Polynomial) (a : C),
(Polynomial.degree (a :: p) > 0)%nat →
(∀ c, Cmod (a :: p)[[C0]] ≤ Cmod (a :: p)[[c]]) →
a = C0.
Theorem Fundamental_Theorem_Algebra : ∀ (p : Polynomial),
(Polynomial.degree p > 0)%nat → (∃ c : Complex.C, p[[c]] = C0).