Library Coq.Reals.NewtonInt
Require Import Rbase.
Require Import Rfunctions.
Require Import SeqSeries.
Require Import Rtrigo.
Require Import Ranalysis.
Open Local 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.