Library Reals_ext

Require Import Rbase Rbasic_fun Rpower Fourier List.

Open Local Scope R_scope.

Definition Rdifference_lemma : forall a b c c',
  0 <= a <= c -> 0 <= b <= c' ->
  Rabs (a - b) <= Rmax c c'.
Qed.

Lemma Rmax_refl : forall r, r = Rmax r r.

Lemma Rabs_def1_eq : forall x a:R, x <= a -> - a <= x -> Rabs x <= a.

Fixpoint Sum (min span:nat) (f:nat -> R) {struct span} : R :=
  match span with
    | O => 0
    | S n' => f min + Sum (S min) n' f
  end.

Lemma Sum_cst : forall span min k f,
  (forall n, (n<min+span)%nat -> f n = k) ->
  Sum min span f = INR span * k.

Lemma Sum_gt0: forall span min f,
  (forall x, (x >= min /\ x < min + span)%nat -> f x >= 0) ->
  Sum min span f >= 0.

Lemma Sum_ext: forall span min f1 f2,
  (forall x, (x >= min /\ x < min + span)%nat -> f1 x = f2 x) ->
  Sum min span f1 = Sum min span f2.

Lemma Sum_ext2: forall span min min' f1 f2,
  (forall x, O <= x < span -> f1 (min + x) = f2 (min' + x))%nat ->
  Sum min span f1 = Sum min' span f2.

Lemma Sum_add: forall span min f1 f2,
  Sum min span f1 + Sum min span f2 = Sum min span (fun x => f1 x + f2 x).

Lemma Sum_max : forall span min f,
  span <> O ->
  exists m, (min <= m < min + span)%nat /\ Sum min span f <= (INR span) * f m.

Require Import ssreflect.

Lemma ln_2 : ln 2 <> 0.
Lemma ln_4 : ln 4 = 2 * ln 2.
Lemma ln_8 : ln 8 = 3 * ln 2.
Lemma ln_16 : ln 16 = 4 * ln 2.
Lemma ln_32 : ln 32 = 5 * ln 2.

Definition log x := ln x / ln 2.

Lemma log_1 : log 1 = 0.
Lemma log_2 : log 2 = 1.
Lemma log_4 : log 4 = 2.
Lemma log_8 : log 8 = 3.
Lemma log_16 : log 16 = 4.
Lemma log_32 : log 32 = 5.

Lemma log_mul : forall x y, 0 < x -> 0 < y -> log (x * y) = log x + log y.

Lemma log_Rinv : forall x, 0 < x -> log (/ x) = -log x.

Lemma log_inv : forall x, 0 < x -> log (1 / x) = - log x.

Fixpoint sumR (l:list R) := if l is h :: t then h + sumR t else 0.

Close Local Scope R_scope.