Library Reals_compl
Some needed definitions and lemmas about real numbers
Discretization of real values to integers or to natural numbers
Definition jx (x:R) (dx:R) : Z :=
(Int_part (x/dx)).
Definition kt (t:R) (dt:R) : nat :=
Zabs_nat (Int_part (t/dt)).
Missing lemmas
Lemma Rmult_eq_compat_r : forall r r1 r2, r1 = r2 -> r1 * r = r2 * r.
Lemma Rplus_eq_compat_r
: forall r r1 r2 : R, r1 = r2 -> r1 + r = r2 + r.
Lemma sqrt_pos: forall x, 0 <= sqrt x.
About Int_part
Lemma Int_part_pos: forall r, 0 <= r -> (0 <= (Int_part r))%Z.
Lemma Int_part_IZR: forall n : Z, Int_part (IZR n) = n.
Lemma Int_part_monotone: forall r1 r2,
r1 <= r2 -> (Int_part r1 <= Int_part r2)%Z.
Lemma Rminus_Int_part_le:
forall r1 r2 : R,
(Int_part (r1 - r2) <= Int_part r1 - Int_part r2)%Z.
Lemma Rplus_Int_part_ge:
forall r1 r2 : R,
(Int_part r1 + Int_part r2 <= Int_part (r1 + r2))%Z.
Lemma up_gt_zero: forall r,
0 < r -> (0 < up r)%Z.
About discretizations
Lemma kt_eq: forall dt i, dt<>0 -> kt (INR i*dt) dt = i.
Lemma kt_le: forall t dt, 0 <= t -> 0 < dt -> INR(kt t dt) <= t/dt.
Finite sum from s to n, whose value is zero if s > n
Definition sum_f (s n:nat) (f: nat -> R) :=
if (le_gt_dec s n)
then sum_f_R0 (fun x : nat => f (x + s)%nat) (n - s)
else 0.
Lemma sum_f_triang : forall s n f,
Rabs (sum_f s n f) <= sum_f s n (fun x => Rabs (f x)).
Lemma sum_f_pos: forall s n f,
(forall i, 0 <= f i)
-> 0 <= sum_f s n (fun x => f x).
Lemma sum_f_le: forall s n f M,
(forall i, (s <= i <= n)%nat -> Rabs (f i) <= M)
-> 0 <= M
-> sum_f s n (fun x => Rabs (f x)) <= (INR (n-s)+1)*M.
Lemma sum_f_Rabs_minus1: forall s n f,
Rabs (sum_f s (n-1) f) <= Rabs (sum_f s n f) + Rabs (f n).
Lemma sum_f_S: forall s n f,
(s <= S n)%nat ->
sum_f s (S n) f = sum_f s n f + f (S n).
Lemma sum_f_S_Rabs_minus1: forall s n f,
Rabs (sum_f s (n-1) (fun j => f (S j))) <= Rabs (sum_f s n f) + Rabs (f s) + Rabs (f 1%nat).
If a degree-2 polynomial is always nonnegative, its dicriminant is nonpositive