Library Coq.Reals.Rsqrt_def
Require Import Sumbool.
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Ranalysis1.
Local Open Scope R_scope.
Fixpoint Dichotomy_lb (
x y:
R) (
P:
R ->
bool) (
N:
nat) {
struct N} :
R :=
match N with
|
O =>
x
|
S n =>
let down :=
Dichotomy_lb x y P n in
let up :=
Dichotomy_ub x y P n in
let z :=
(down + up) / 2
in if P z then down else z
end
with Dichotomy_ub (
x y:
R) (
P:
R ->
bool) (
N:
nat) {
struct N} :
R :=
match N with
|
O =>
y
|
S n =>
let down :=
Dichotomy_lb x y P n in
let up :=
Dichotomy_ub x y P n in
let z :=
(down + up) / 2
in if P z then z else up
end.
Definition dicho_lb (
x y:
R) (
P:
R ->
bool) (
N:
nat) :
R :=
Dichotomy_lb x y P N.
Definition dicho_up (
x y:
R) (
P:
R ->
bool) (
N:
nat) :
R :=
Dichotomy_ub x y P N.
Lemma dicho_comp :
forall (
x y:
R) (
P:
R ->
bool) (
n:
nat),
x <= y ->
dicho_lb x y P n <= dicho_up x y P n.
Lemma dicho_lb_growing :
forall (
x y:
R) (
P:
R ->
bool),
x <= y ->
Un_growing (
dicho_lb x y P).
Lemma dicho_up_decreasing :
forall (
x y:
R) (
P:
R ->
bool),
x <= y ->
Un_decreasing (
dicho_up x y P).
Lemma dicho_lb_maj_y :
forall (
x y:
R) (
P:
R ->
bool),
x <= y ->
forall n:
nat,
dicho_lb x y P n <= y.
Lemma dicho_lb_maj :
forall (
x y:
R) (
P:
R ->
bool),
x <= y ->
has_ub (
dicho_lb x y P).
Lemma dicho_up_min_x :
forall (
x y:
R) (
P:
R ->
bool),
x <= y ->
forall n:
nat,
x <= dicho_up x y P n.
Lemma dicho_up_min :
forall (
x y:
R) (
P:
R ->
bool),
x <= y ->
has_lb (
dicho_up x y P).
Lemma dicho_lb_cv :
forall (
x y:
R) (
P:
R ->
bool),
x <= y ->
{ l:R | Un_cv (
dicho_lb x y P)
l }.
Lemma dicho_up_cv :
forall (
x y:
R) (
P:
R ->
bool),
x <= y ->
{ l:R | Un_cv (
dicho_up x y P)
l }.
Lemma dicho_lb_dicho_up :
forall (
x y:
R) (
P:
R ->
bool) (
n:
nat),
x <= y ->
dicho_up x y P n - dicho_lb x y P n = (y - x) / 2
^ n.
Definition pow_2_n (
n:
nat) := 2
^ n.
Lemma pow_2_n_neq_R0 :
forall n:
nat,
pow_2_n n <> 0.
Lemma pow_2_n_growing :
Un_growing pow_2_n.
Lemma pow_2_n_infty :
cv_infty pow_2_n.
Lemma cv_dicho :
forall (
x y l1 l2:
R) (
P:
R ->
bool),
x <= y ->
Un_cv (
dicho_lb x y P)
l1 ->
Un_cv (
dicho_up x y P)
l2 ->
l1 = l2.
Definition cond_positivity (
x:
R) :
bool :=
match Rle_dec 0
x with
|
left _ =>
true
|
right _ =>
false
end.
Sequential caracterisation of continuity
Intermediate Value Theorem
We can now define the square root function as the reciprocal
transformation of the square root function