Library Reals_compl

Some needed definitions and lemmas about real numbers

Require Export Reals.
Open Local Scope nat_scope.
Open Local Scope R_scope.

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

Lemma discr_neg: forall a b c,
  (forall x, 0 <= a*x*x+b*x+c) ->
     b*b-4*a*c <= 0.