1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
|
(************************************************************************)
(* * The Coq Proof Assistant / The Coq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
Require Import Rbase.
Require Import Rfunctions.
Require Import Rseries.
Require Import PartSum.
Require Import Lia.
Local Open Scope R_scope.
Set Implicit Arguments.
Section Sigma.
Variable f : nat -> R.
Definition sigma (low high:nat) : R :=
sum_f_R0 (fun k:nat => f (low + k)) (high - low).
Theorem sigma_split :
forall low high k:nat,
(low <= k)%nat ->
(k < high)%nat -> sigma low high = sigma low k + sigma (S k) high.
Proof.
intros; induction k as [| k Hreck].
cut (low = 0%nat).
intro; rewrite H1; unfold sigma; rewrite Nat.sub_diag, Nat.sub_0_r;
simpl; replace (high - 1)%nat with (pred high).
apply (decomp_sum (fun k:nat => f k)).
assumption.
symmetry; apply Nat.sub_1_r.
inversion H; reflexivity.
cut ((low <= k)%nat \/ low = S k).
intro; elim H1; intro.
replace (sigma low (S k)) with (sigma low k + f (S k)).
rewrite Rplus_assoc;
replace (f (S k) + sigma (S (S k)) high) with (sigma (S k) high).
apply Hreck.
assumption.
apply Nat.lt_trans with (S k); [ apply Nat.lt_succ_diag_r | assumption ].
unfold sigma; replace (high - S (S k))%nat with (pred (high - S k)).
pattern (S k) at 3; replace (S k) with (S k + 0)%nat;
[ idtac | ring ].
replace (sum_f_R0 (fun k0:nat => f (S (S k) + k0)) (pred (high - S k))) with
(sum_f_R0 (fun k0:nat => f (S k + S k0)) (pred (high - S k))).
apply (decomp_sum (fun i:nat => f (S k + i))).
apply lt_minus_O_lt; assumption.
apply sum_eq; intros; replace (S k + S i)%nat with (S (S k) + i)%nat.
reflexivity.
ring.
replace (high - S (S k))%nat with (high - S k - 1)%nat.
symmetry; apply Nat.sub_1_r.
lia.
unfold sigma; replace (S k - low)%nat with (S (k - low)).
pattern (S k) at 1; replace (S k) with (low + S (k - low))%nat.
symmetry ; apply (tech5 (fun i:nat => f (low + i))).
lia.
lia.
rewrite <- H2; unfold sigma; rewrite Nat.sub_diag; simpl;
replace (high - S low)%nat with (pred (high - low)).
replace (sum_f_R0 (fun k0:nat => f (S (low + k0))) (pred (high - low))) with
(sum_f_R0 (fun k0:nat => f (low + S k0)) (pred (high - low))).
apply (decomp_sum (fun k0:nat => f (low + k0))).
apply lt_minus_O_lt.
apply Nat.le_lt_trans with (S k); [ rewrite H2; apply Nat.le_refl | assumption ].
apply sum_eq; intros; replace (S (low + i)) with (low + S i)%nat.
reflexivity.
ring.
lia.
inversion H; [ right; reflexivity | left; assumption ].
Qed.
Theorem sigma_diff :
forall low high k:nat,
(low <= k)%nat ->
(k < high)%nat -> sigma low high - sigma low k = sigma (S k) high.
Proof.
intros low high k H1 H2; symmetry ; rewrite (sigma_split H1 H2); ring.
Qed.
Theorem sigma_diff_neg :
forall low high k:nat,
(low <= k)%nat ->
(k < high)%nat -> sigma low k - sigma low high = - sigma (S k) high.
Proof.
intros low high k H1 H2; rewrite (sigma_split H1 H2); ring.
Qed.
Theorem sigma_first :
forall low high:nat,
(low < high)%nat -> sigma low high = f low + sigma (S low) high.
Proof.
intros low high H1; generalize (proj2 (Nat.le_succ_l low high) H1); intro H2;
generalize (Nat.lt_le_incl low high H1); intro H3;
replace (f low) with (sigma low low).
apply sigma_split.
apply le_n.
assumption.
unfold sigma; rewrite Nat.sub_diag.
simpl.
replace (low + 0)%nat with low; [ reflexivity | ring ].
Qed.
Theorem sigma_last :
forall low high:nat,
(low < high)%nat -> sigma low high = f high + sigma low (pred high).
Proof.
intros low high H1; generalize (proj2 (Nat.le_succ_l low high) H1); intro H2;
generalize (Nat.lt_le_incl low high H1); intro H3;
replace (f high) with (sigma high high).
rewrite Rplus_comm; cut (high = S (pred high)).
intro; pattern high at 3; rewrite H.
apply sigma_split.
apply le_S_n; rewrite <- H; apply Nat.le_succ_l; assumption.
apply Nat.lt_pred_l, Nat.neq_0_lt_0; apply Nat.le_lt_trans with low; [ apply Nat.le_0_l | assumption ].
symmetry; apply Nat.lt_succ_pred with 0%nat; apply Nat.le_lt_trans with low;
[ apply Nat.le_0_l | assumption ].
unfold sigma; rewrite Nat.sub_diag; simpl;
replace (high + 0)%nat with high; [ reflexivity | ring ].
Qed.
Theorem sigma_eq_arg : forall low:nat, sigma low low = f low.
Proof.
intro; unfold sigma; rewrite Nat.sub_diag.
simpl; replace (low + 0)%nat with low; [ reflexivity | ring ].
Qed.
End Sigma.
|
