Section ∫_I.

Integral

Having proved the main properties of partitions and refinements, we will define the integral of a continuous function F in the interval [a,b] as the limit of the sequence of Sums of for even partitions of increasing number of points.

All throughout, a,b will be real numbers, the interval [a,b] will be denoted by I and F,G will be continuous functions in I.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Section Darboux_Sum.

Definition integral_seq : N -> IR.
Defined.

Lemma Cauchy_Darboux_Seq : Cauchy_prop integral_seq.

Definition ∫_I := Lim (Build_CauchySeq _ _ Cauchy_Darboux_Seq).

End Darboux_Sum.

Section Integral_Thm.

The following shows that in fact the integral of F is the limit of any sequence of partitions of mesh converging to 0.

Let e be a positive real number and P be a partition of I with n points and mesh smaller than the modulus of continuity of F for e. Let fP be a choice of points respecting P.

Variable n : N.

Variable P : Partition Hab n.

Variable e : IR.
Hypothesis He : 0 [<] e.

Hypothesis HmeshP : Mesh P [<] d.

Variable fP : forall i : N, i < n -> IR.
Hypothesis HfP : Points_in_Partition P fP.
Hypothesis HfP' : nat_less_n_fun fP.

Hypothesis incF : ⊆ (Compact Hab) (Dom F).

Lemma partition_Sum_conv_integral : AbsIR (∑_P HfP incF[-]∫_I) [<=] e[*] (b[-]a).

End Integral_Thm.

End ∫_I.

Section Basic_Properties.

The usual extensionality and strong extensionality results hold.

Variables a b : IR.
Hypothesis Hab : a [<=] b.

Notation ∫_I := (∫_I _ _ Hab).

Section Well_Definedness.

Variables F G : PartIR.
Hypothesis contF : Continuous_I Hab F.
Hypothesis contG : Continuous_I Hab G.

Lemma integral_strext : ∫_I F contF [#] ∫_I G contG ->
{x : IR | I x | forall Hx Hx', F x Hx [#] G x Hx'}.

Lemma integral_strext' : forall c d Hcd HF1 HF2,
∫_I a b Hab F HF1 [#] ∫_I c d Hcd F HF2 -> a [#] c or b [#] d.

Lemma integral_wd : ≈ (Compact Hab) F G -> ∫_I F contF [=] ∫_I G contG.

Lemma integral_wd' : forall a' b' Hab' contF',
a [=] a' -> b [=] b' -> ∫_I F contF [=] ∫_I a' b' Hab' F contF'.

End Well_Definedness.

Section Linearity_and_Monotonicity.

The integral is a linear and monotonous function; in order to prove these facts we also need the important equalities ∫_a^bdx=b-a and ∫_a^a=0.

Lemma integral_one : forall H, ∫_I ( [-C-] 1) H [=] b[-]a.

Variables F G : PartIR.
Hypothesis contF : Continuous_I Hab F.
Hypothesis contG : Continuous_I Hab G.

Lemma integral_comm_scal : forall (c : IR) Hf', ∫_I (c{**}F) Hf' [=] c[*]∫_I F contF.

Lemma integral_plus : forall Hfg, ∫_I (F{+}G) Hfg [=] ∫_I F contF[+]∫_I G contG.

Lemma integral_empty : a [=] b -> ∫_I F contF [=] 0.

End Linearity_and_Monotonicity.

Section Linearity_and_Monotonicity'.

Variables F G : PartIR.
Hypothesis contF : Continuous_I Hab F.
Hypothesis contG : Continuous_I Hab G.

Let α, β : IR and assume that h := α{**}F{+}beta{**}G is continuous.

Variables α β : IR.
Hypothesis contH : Continuous_I Hab h.

Lemma linear_integral : ∫_I h contH [=] α[*]∫_I F contF[+]β[*]∫_I G contG.

Lemma monotonous_integral : (forall x, I x -> forall Hx Hx', F x Hx [<=] G x Hx') ->
∫_I F contF [<=] ∫_I G contG.

End Linearity_and_Monotonicity'.

Section Corollaries.

Variables F G : PartIR.
Hypothesis contF : Continuous_I Hab F.
Hypothesis contG : Continuous_I Hab G.

As corollaries we can calculate integrals of group operations applied to functions.

Lemma integral_const : forall c H, ∫_I ( [-C-]c)H [=] c[*] (b[-]a).

Lemma integral_minus : forall H, ∫_I (F{-}G) H [=] ∫_I F contF[-]∫_I G contG.

Lemma integral_inv : forall H, ∫_I ( {--}F) H [=] [--] (∫_I F contF).

We can also bound integrals by bounding the integrated functions.

Lemma lb_integral : forall c, (forall x, I x -> forall Hx, c [<=] F x Hx) -> c[*] (b[-]a) [<=] ∫_I F contF.

Lemma ub_integral : forall c, (forall x, I x -> forall Hx, F x Hx [<=] c) -> ∫_I F contF [<=] c[*] (b[-]a).

Lemma integral_leEq_norm : AbsIR (∫_I F contF) [<=] Norm_Funct contF[*] (b[-]a).

End Corollaries.

Section Integral_Sum.

We now relate the sum of integrals in adjoining intervals to the integral over the union of those intervals.

Let c be a real number such that c∈[a,b].

Variable F : PartIR.

Variable c : IR.

Hypothesis Hac : a [<=] c.
Hypothesis Hcb : c [<=] b.

Hypothesis Hab' : Continuous_I Hab F.
Hypothesis Hac' : Continuous_I Hac F.
Hypothesis Hcb' : Continuous_I Hcb F.

Section Partition_Join.

We first prove that every pair of partitions, one of [a,c] and another of [c,b] defines a partition of [a,b] the mesh of which is less or equal to the maximum of the mesh of the original partitions (actually it is equal, but we don't need the other inequality).

Let P,Q be partitions respectively of [a,c] and [c,b] with n and m points.

Variables n m : N.
Variable P : Partition Hac n.
Variable Q : Partition Hcb m.

Definition partition_join_fun : forall i, i <= S (n + m) -> IR.
Defined.

fP, fQ are choices of points respecting P and Q.

Variable fP : forall i : N, i < n -> IR.
Hypothesis HfP : Points_in_Partition P fP.
Hypothesis HfP' : nat_less_n_fun fP.

Variable fQ : forall i : N, i < m -> IR.
Hypothesis HfQ : Points_in_Partition Q fQ.
Hypothesis HfQ' : nat_less_n_fun fQ.

Definition partition_join_pts : forall i, i < S (n + m) -> IR.
Defined.

Lemma partition_join_Pts_in_partition : Points_in_Partition partition_join partition_join_pts.

Lemma partition_join_Pts_wd : forall i j,
i = j -> forall Hi Hj, partition_join_pts i Hi [=] partition_join_pts j Hj.

Lemma partition_join_Sum_lemma :
∑_P HfP (contin_imp_inc _ _ _ _ Hac') [+] ∑_P HfQ (contin_imp_inc _ _ _ _ Hcb') [=]
∑_P partition_join_Pts_in_partition (contin_imp_inc _ _ _ _ Hab').

Lemma partition_join_mesh : Mesh partition_join [<=] Max (Mesh P) (Mesh Q).

End Partition_Join.

With these results in mind, the following is a trivial consequence:

Lemma integral_plus_integral : ∫_I _ _ Hac _ Hac'[+]∫_I _ _ Hcb _ Hcb' [=] ∫_I _ Hab'.

End Integral_Sum.

End Basic_Properties.

The following are simple consequences of this result and of previous ones.

Lemma integral_less_norm : forall a b Hab (F : PartIR) contF,
let N := Norm_Funct contF in a [<] b -> forall x, Compact Hab x -> forall Hx,
AbsIR (F x Hx) [<] N -> AbsIR (∫_I a b Hab F contF) [<] N[*] (b[-]a).
Lemma integral_gt_zero : forall a b Hab (F : PartIR) contF, let N := Norm_Funct contF in
a [<] b -> forall x, Compact Hab x -> forall Hx, 0 [<] F x Hx ->
(forall x, Compact Hab x -> forall Hx, 0 [<=] F x Hx) -> 0 [<] ∫_I a b Hab F contF.