Library Top.R_compl

This file is part of the Elfic library
Copyright (C) Boldo, Clément, Faissole, Martin, Mayero
This library is free software; you can redistribute it and/or modify it under the terms of the GNU Lesser General Public License as published by the Free Software Foundation; either version 3 of the License, or (at your option) any later version.
This library is distributed in the hope that it will be useful, but WITHOUT ANY WARRANTY; without even the implied warranty of MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the COPYING file for more details.

Require Export Reals Coquelicot.Coquelicot.

Open Local Scope R_scope.

Section RC.

If a degree-2 polynomial is always nonnegative, its dicriminant is nonpositive

Lemma discr_neg: a b c,
  ( x, 0 a×x×x+b×x+c)
     b×b-4×a×c 0.

Lemma contraction_lt_any: k d, 0 k < 1 0 < d N, pow k N < d.

Lemma contraction_lt_any': k d, 0 k < 1 0 < d N, (0 < N)%nat pow k N < d.

Lemma Rinv_le_cancel: x y : R, 0 < y / y / x x y.

Lemma Rlt_R1_pow: x n, 0 x < 1 (0 < n)%nat x ^ n < 1.

Lemma Rle_pow_le: (x : R) (m n : nat), 0 < x 1 (m n)%nat x ^ n x ^ m.

Lemma is_finite_betw: x y z,
  Rbar_le (Finite x) y Rbar_le y (Finite z) is_finite y.

Lemma Rplus_plus_reg_l : (a b c:R), b = c plus a b = a + c.

Lemma Rplus_plus_reg_r : a b c, b = c plus b a = c + a.

Context {E : NormedModule R_AbsRing}.

Lemma norm_scal_R: l (x:E), norm (scal l x) = abs l × norm x.

Lemma sum_n_eq_zero: m (L:nat E),
  ( i, (i m)%nat L i = zero)
   sum_n L m = zero.

End RC.