# Library Coq.Reals.NewtonInt

Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Rtrigo1.
Require Import Ranalysis.
Local Open Scope R_scope.

Definition Newton_integrable (f:R -> R) (a b:R) : Type :=
{ g:R -> R | antiderivative f g a b \/ antiderivative f g b a }.

Definition NewtonInt (f:R -> R) (a b:R) (pr:Newton_integrable f a b) : R :=
let (g,_) := pr in g b - g a.

Lemma FTCN_step1 :
forall (f:Differential) (a b:R),
Newton_integrable (fun x:R => derive_pt f x (cond_diff f x)) a b.

Lemma FTC_Newton :
forall (f:Differential) (a b:R),
NewtonInt (fun x:R => derive_pt f x (cond_diff f x)) a b
(FTCN_step1 f a b) = f b - f a.

Lemma NewtonInt_P1 : forall (f:R -> R) (a:R), Newton_integrable f a a.

Lemma NewtonInt_P2 :
forall (f:R -> R) (a:R), NewtonInt f a a (NewtonInt_P1 f a) = 0.

Lemma NewtonInt_P3 :
forall (f:R -> R) (a b:R) (X:Newton_integrable f a b),
Newton_integrable f b a.

Lemma NewtonInt_P4 :
forall (f:R -> R) (a b:R) (pr:Newton_integrable f a b),
NewtonInt f a b pr = - NewtonInt f b a (NewtonInt_P3 f a b pr).

Lemma NewtonInt_P5 :
forall (f g:R -> R) (l a b:R),
Newton_integrable f a b ->
Newton_integrable g a b ->
Newton_integrable (fun x:R => l * f x + g x) a b.

Lemma antiderivative_P1 :
forall (f g F G:R -> R) (l a b:R),
antiderivative f F a b ->
antiderivative g G a b ->
antiderivative (fun x:R => l * f x + g x) (fun x:R => l * F x + G x) a b.

Lemma NewtonInt_P6 :
forall (f g:R -> R) (l a b:R) (pr1:Newton_integrable f a b)
(pr2:Newton_integrable g a b),
NewtonInt (fun x:R => l * f x + g x) a b (NewtonInt_P5 f g l a b pr1 pr2) =
l * NewtonInt f a b pr1 + NewtonInt g a b pr2.

Lemma antiderivative_P2 :
forall (f F0 F1:R -> R) (a b c:R),
antiderivative f F0 a b ->
antiderivative f F1 b c ->
antiderivative f
(fun x:R =>
match Rle_dec x b with
| left _ => F0 x
| right _ => F1 x + (F0 b - F1 b)
end) a c.

Lemma antiderivative_P3 :
forall (f F0 F1:R -> R) (a b c:R),
antiderivative f F0 a b ->
antiderivative f F1 c b ->
antiderivative f F1 c a \/ antiderivative f F0 a c.

Lemma antiderivative_P4 :
forall (f F0 F1:R -> R) (a b c:R),
antiderivative f F0 a b ->
antiderivative f F1 a c ->
antiderivative f F1 b c \/ antiderivative f F0 c b.

Lemma NewtonInt_P7 :
forall (f:R -> R) (a b c:R),
a < b ->
b < c ->
Newton_integrable f a b ->
Newton_integrable f b c -> Newton_integrable f a c.

Lemma NewtonInt_P8 :
forall (f:R -> R) (a b c:R),
Newton_integrable f a b ->
Newton_integrable f b c -> Newton_integrable f a c.

Lemma NewtonInt_P9 :
forall (f:R -> R) (a b c:R) (pr1:Newton_integrable f a b)
(pr2:Newton_integrable f b c),
NewtonInt f a c (NewtonInt_P8 f a b c pr1 pr2) =
NewtonInt f a b pr1 + NewtonInt f b c pr2.