Library Coq.Reals.Rsqrt_def
Require Import Sumbool.
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Ranalysis1.
Open Local Scope R_scope.
Boxed 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
Lemma IVT :
forall (
f:R ->
R) (
x y:R),
continuity f ->
x <
y ->
f x < 0 -> 0 <
f y -> {
z:R |
x <=
z <=
y /\
f z = 0 }.
Lemma IVT_cor :
forall (
f:R ->
R) (
x y:R),
continuity f ->
x <=
y ->
f x *
f y <= 0 -> {
z:R |
x <=
z <=
y /\
f z = 0 }.
We can now define the square root function as the reciprocal
transformation of the square root function