Roots of Real Numbers


Section NRoot.

Existence of roots



Let n be a natural number and c a nonnegative real. p is the auxiliary polynomial _X_^n− (_C_ c).

Variable n : N.
Hypothesis n_pos : 0 < n.
Variable c : IR.
Hypothesis c_nonneg : 0 [<=] c.


Lemma CnrootIR : {x : IR | 0 [<=] x | x[^]n [=] c}.









End NRoot.

We define the root of order n for any nonnegative real number and prove its main properties:
  • (sqrt(n) x)^n =x;
  • 0≤sqrt(n)x;
  • if 0 < x then 0<sqrt(n)x;
  • sqrt(n) x^n =x;
  • the nth root is monotonous;
  • in particular, if x < 1 then sqrt(n) x<1.


(nroot ??) will be written as NRoot.

Section Nth_Root.

Lemma nroot : forall x k, 0 [<=] x -> 0 < k -> {y : IR | 0 [<=] y | y[^]k [=] x}.


Definition NRoot x n Hx Hn : IR := proj1_sig2T _ _ _ (nroot x n Hx Hn).

Lemma NRoot_power : forall x k Hx Hk, NRoot x k Hx Hk[^]k [=] x.


Lemma NRoot_nonneg : forall x k Hx Hk, 0 [<=] NRoot x k Hx Hk.

Lemma NRoot_pos : forall x Hx k Hk, 0 [<] x -> 0 [<] NRoot x k Hx Hk.



Lemma NRoot_power' : forall x k Hx' Hk, 0 [<=] x -> NRoot (x[^]k) k Hx' Hk [=] x.

Lemma NRoot_pres_less : forall x Hx y Hy k Hk, x [<] y -> NRoot x k Hx Hk [<] NRoot y k Hy Hk.

Lemma NRoot_less_one : forall x Hx k Hk, x [<] 1 -> NRoot x k Hx Hk [<] 1.

Lemma NRoot_cancel : forall x Hx y Hy k Hk, NRoot x k Hx Hk [=] NRoot y k Hy Hk -> x [=] y.

Let x,y be nonnegative real numbers.

Variables x y : IR.
Hypothesis Hx : 0 [<=] x.
Hypothesis Hy : 0 [<=] y.

Lemma NRoot_wd : forall k Hk Hk', x [=] y -> NRoot x k Hx Hk [=] NRoot y k Hy Hk'.

Lemma NRoot_unique : forall k Hk, 0 [<] x -> x[^]k [=] y -> x [=] NRoot y k Hy Hk.


End Nth_Root.



Lemma NRoot_resp_leEq : forall x y xpos ypos k kpos,
 x [<=] y -> NRoot (x:=x) (n:=k) xpos kpos [<=] NRoot (x:=y) (n:=k) ypos kpos.

Lemma NRoot_cancel_less : forall x (Hx:Zero[<=]x) y (Hy:Zero[<=]y) k (Hk Hk':0<k), NRoot Hx Hk [<] NRoot Hy Hk' -> x [<] y.

Lemma NRoot_str_ext : forall k (Hk Hk':0 < k) x y (Hx:Zero[<=]x) (Hy:Zero[<=]y), NRoot Hx Hk [#] NRoot Hy Hk' -> x[#]y.

Section Square_root.

Square root


Definition sqrt x xpos : IR := NRoot (x:=x) (n:=2) xpos (lt_O_Sn 1).

Lemma sqrt_sqr : forall x xpos, sqrt x xpos[^]2 [=] x.


Lemma sqrt_nonneg : forall x xpos, 0 [<=] sqrt x xpos.

Lemma sqrt_wd : forall x y xpos ypos, x [=] y -> sqrt x xpos [=] sqrt y ypos.


Lemma sqrt_to_nonneg : forall x, 0 [<=] x -> forall x2pos, sqrt (x[^]2) x2pos [=] x.


Lemma sqrt_to_nonpos : forall x, x [<=] 0 -> forall x2pos, sqrt (x[^]2) x2pos [=] [--]x.



Lemma sqrt_mult : forall x y xpos ypos xypos, sqrt (x[*]y) xypos [=] sqrt x xpos[*]sqrt y ypos.


Lemma sqrt_mult_wd : forall x y z xpos ypos zpos,
 z [=] x[*]y -> sqrt z zpos [=] sqrt x xpos[*]sqrt y ypos.


Lemma sqrt_less : forall x y ypos, x[^]2 [<] y -> x [<] sqrt y ypos.


Lemma sqrt_less' : forall x y ypos, x[^]2 [<] y -> [--]x [<] sqrt y ypos.


Lemma sqrt_resp_leEq : forall x y xpos ypos, x [<=] y -> sqrt x xpos [<=] sqrt y ypos.

Lemma sqrt_resp_less : forall x y xpos ypos, x [<] y -> sqrt x xpos [<] sqrt y ypos.

End Square_root.


Section Absolute_Props.

More on absolute value



With the help of square roots, we can prove some more properties of absolute values in IR.

Lemma AbsIR_sqrt_sqr : forall x x2pos, AbsIR x [=] sqrt (x[^]2) x2pos.








Lemma AbsIR_resp_mult : forall x y, AbsIR (x[*]y) [=] AbsIR x[*]AbsIR y.


Lemma AbsIR_mult_pos : forall x y, 0 [<=] y -> AbsIR (x[*]y) [=] AbsIR x[*]y.

Lemma AbsIR_mult_pos' : forall x y, 0 [<=] x -> AbsIR (x[*]y) [=] x[*]AbsIR y.

Lemma AbsIR_nexp : forall x n, AbsIR (nexp _ n x) [=] nexp _ n (AbsIR x).

Lemma AbsIR_nexp_op : forall n x, AbsIR (x[^]n) [=] AbsIR x[^]n.

Lemma AbsIR_less_square : forall x y, AbsIR x [<] y -> x[^]2 [<] y[^]2.

Lemma AbsIR_leEq_square : forall x y, AbsIR x [<=] y -> x[^]2 [<=] y[^]2.

Lemma AbsIR_division : forall x y y_ y__, AbsIR (x[/] y[//]y_) [=] (AbsIR x[/] AbsIR y[//]y__).

Some special cases.

Lemma AbsIR_recip : forall x x_ x__, AbsIR (1[/] x[//]x_) [=] (1[/] AbsIR x[//]x__).

Lemma AbsIR_div_two : forall x, AbsIR (x [/]2) [=] AbsIR x [/]2.

Cauchy-Schwartz for IR and variants on that subject.

Lemma triangle_IR : forall x y, AbsIR (x[+]y) [<=] AbsIR x[+]AbsIR y.






Lemma triangle_SumIR : forall k l s,
 k <= S l -> AbsIR (∑ k l s) [<=] ∑ k l (fun i => AbsIR (s i)).










Lemma triangle_IR_minus : forall x y, AbsIR (x[-]y) [<=] AbsIR x[+]AbsIR y.

Lemma weird_triangleIR : forall x y, AbsIR x[-]AbsIR (y[-]x) [<=] AbsIR y.

Lemma triangle_IR_minus' : forall x y, AbsIR x[-]AbsIR y [<=] AbsIR (x[-]y).

Lemma triangle_SumxIR : forall n (f : forall i, i < n -> IR),
 AbsIR (Sumx f) [<=] Sumx (fun i H => AbsIR (f i H)).

Lemma triangle_Sum2IR : forall m n (f : forall i, m <= i -> i <= n -> IR),
 m <= S n -> AbsIR (∑2 f) [<=] ∑2 (fun i Hm Hn => AbsIR (f i Hm Hn)).

Lemma AbsIR_str_bnd_AbsIR : forall a b e, AbsIR (a[-]b) [<] e -> AbsIR b [<] AbsIR a[+]e.


Lemma AbsIR_bnd_AbsIR : forall a b e, AbsIR (a[-]b) [<=] e -> AbsIR b [<=] AbsIR a[+]e.

End Absolute_Props.

Section Consequences.

Cauchy sequences



With these results, we can also prove that the sequence of reciprocals of a Cauchy sequence that is never zero and whose Limit is not zero is also a Cauchy sequence.

Lemma Cauchy_Lim_recip : forall seq y, Cauchy_Lim_prop2 seq y ->
 forall seq_ y_, Cauchy_Lim_prop2 (fun n : N => 1[/] seq n[//]seq_ n) (1[/] y[//]y_).

Lemma Cauchy_recip : forall seq seq_, Lim seq [#] (0:IR) ->
 Cauchy_prop (fun n => 1[/] seq n[//]seq_ n).

Lemma Lim_recip : forall seq seq_ seq__,
 Lim (Build_CauchySeq _ _ (Cauchy_recip seq seq_ seq__)) [=] (1[/] _[//]seq__).

End Consequences.

Section Part_Function_NRoot.

Functional Operators



Let F:PartIR and denote by P its domain, which must be entirely nonnegative.

Variables F : PartIR.

Let P := Dom F.

Let R := extend P (fun x Hx => 0[<=]F x Hx).

Let Ext2R := ext2 (P:=P) (R:=fun x Hx => 0[<=]F x Hx).

Variable n : N.

Hypothesis Hn : 0 < n.

Lemma part_function_NRoot_strext : forall x y Hx Hy,
 NRoot (Ext2R x Hx) Hn [#] NRoot (Ext2R y Hy) Hn -> x [#] y.

Lemma part_function_NRoot_pred_wd : pred_wd _ R.

Definition FNRoot := Build_PartFunct IR _ part_function_NRoot_pred_wd
 (fun x Hx => NRoot (Ext2R x Hx) Hn) part_function_NRoot_strext.

Section Included.

Variable S:IR -> CProp.

Lemma included_FNRoot : ⊆ S P ->
 (forall x, S x -> forall Hx, 0[<=]F x Hx) -> ⊆ S (Dom FNRoot).

Lemma included_FNRoot' : ⊆ S (Dom FNRoot) -> ⊆ S P.

End Included.

End Part_Function_NRoot.