Library Stdlib.Reals.Rsqrt_def
From Stdlib Require Import Sumbool.
From Stdlib Require Import Rbase.
From Stdlib Require Import Rfunctions.
From Stdlib Require Import SeqSeries.
From Stdlib Require Import Ranalysis1.
From Stdlib Require Import Lra.
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 characterisation of continuity
Lemma continuity_seq :
forall (f:R -> R) (Un:nat -> R) (l:R),
continuity_pt f l -> Un_cv Un l -> Un_cv (fun i:nat => f (Un i)) (f l).
Lemma dicho_lb_car :
forall (x y:R) (P:R -> bool) (n:nat),
P x = false -> P (dicho_lb x y P n) = false.
Lemma dicho_up_car :
forall (x y:R) (P:R -> bool) (n:nat),
P y = true -> P (dicho_up x y P n) = true.
Lemma cv_pow_half : forall a, Un_cv (fun n => a/2^n) 0.
forall (f:R -> R) (Un:nat -> R) (l:R),
continuity_pt f l -> Un_cv Un l -> Un_cv (fun i:nat => f (Un i)) (f l).
Lemma dicho_lb_car :
forall (x y:R) (P:R -> bool) (n:nat),
P x = false -> P (dicho_lb x y P n) = false.
Lemma dicho_up_car :
forall (x y:R) (P:R -> bool) (n:nat),
P y = true -> P (dicho_up x y P n) = true.
Lemma cv_pow_half : forall a, Un_cv (fun n => a/2^n) 0.
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 }.
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 function