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.