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
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
|
(*
Require Import
Unicode.Utf8
Setoid Arith List Program Permutation metric2.Classified
CSetoids CPoly_ApZero CRings CPoly_Degree
CRArith Qmetric Qring CReals
stdlib_omissions.Pair stdlib_omissions.Q
list_separates SetoidPermutation
util.Container NewAbstractIntegration
algebra.CPoly_Newton Ranges.
Require ne_list.
Import ne_list.notations.
Opaque CR.
Section contents.
Notation QPoint := (Q * CR)%type.
Notation CRPoint := (CR * CR)%type.
Local Notation Σ := cm_Sum.
Require Import Qabs.
(* Some utility operations and lemmas for ne_list/vector (todo: move these): *)
Definition Vec_to_ne_list {A}: ∀ {n}, Vector.t A (S n) → ne_list A :=
@Vector.rectS A (fun _ _ => ne_list A) ne_list.one (fun a _ _ x => ne_list.cons a x).
Lemma ne_list_head_map {A B} (f: A → B) (l: ne_list A): ne_list.head (ne_list.map f l) = f (ne_list.head l).
Proof. induction l. reflexivity. simpl. congruence. Qed.
Lemma ne_list_tail_map {A B} (f: A → B) (l: ne_list A): ne_list.tail (ne_list.map f l) = map f (ne_list.tail l).
Proof. destruct l. reflexivity. simpl. induction l. reflexivity. simpl. congruence. Qed.
Lemma ding_vec n A (v: Vector.t A (S n)): v = Vector.cons _ (Vector.hd v) _ (Vector.tl v).
Proof. dependent destruction v. simpl. reflexivity. Qed.
Lemma through_ne A n (v: Vector.t A (S n)):
ne_list.to_list (Vec_to_ne_list _ v) = v.
Proof with auto.
induction n.
dependent destruction v.
dependent destruction v.
simpl.
reflexivity.
dependent destruction v.
simpl.
rewrite IHn.
reflexivity.
Qed.
Lemma Vec_cons_to_ne_list {A} n (a: A) (v: Vector.t A (S n)): Vec_to_ne_list _ (Vector.cons _ a _ v) = ne_list.cons a (Vec_to_ne_list _ v).
Admitted.
Lemma Vec_cons_to_ne_list' {A} n (v: Vector.t A n): ∀ a, Vec_to_ne_list _ (Vector.cons _ a _ v) = ne_list.from_list a v.
Proof with auto.
induction n.
dependent destruction v.
reflexivity.
dependent destruction v.
intros.
change (Vec_to_ne_list (S n) (Vector.cons A a (S n) (Vector.cons A h n v)) = a ::: ne_list.from_list h v).
rewrite <- IHn.
reflexivity.
Qed.
Lemma ne_head_from_list {X} (x: X) (xs: list X): ne_list.head (ne_list.from_list x xs) = x.
Proof. destruct xs; reflexivity. Qed.
Lemma ne_to_from_list {X} (xs: list X): ∀ x, ne_list.to_list (ne_list.from_list x xs) = x :: xs.
Proof. induction xs. reflexivity. simpl. rewrite IHxs. reflexivity. Qed.
Lemma ne_tail_from_list {X} (x: X) (xs: list X): ne_list.tail (ne_list.from_list x xs) = xs.
Proof.
induction xs.
reflexivity.
simpl.
rewrite ne_to_from_list.
reflexivity.
Qed.
Lemma ne_list_map_from_list {X Y} (f: X → Y) (xs: list X): ∀ h,
ne_list.map f (ne_list.from_list h xs) = ne_list.from_list (f h) (map f xs).
Proof. induction xs; simpl; congruence. Qed.
(*
Section inner_space.
(* Need vector space, norm, inner product, metric from norm, Lipschitz continuity from boundedness *)
Definition norm `(x: Vector.t Q n):=Σ (map Qabs x).
Definition inner (n:nat)(x y : Vector.t Q n):=Σ(map (λ p, Qmult (fst p) (snd p)) (zip x y)).
End inner_space.*)
Section divdiff_as_repeated_integral.
Context
(nth_deriv_bound: Range CR)
(nth_deriv: Q → sig ((∈ nth_deriv_bound)))
(* Todo: only require boundedness on the interval that contains the points. *)
`{!UniformlyContinuous_mu nth_deriv}
`{!UniformlyContinuous nth_deriv}.
(* Todo: This should be replaced with some "n times differentiable" requirement on a subject function. *)
Context
(n: nat) (points: Vector.t Q (S n)).
Opaque Qmult Qplus Qminus.
(* Without these, instance resolution gets a little too enthusiastic and breaks these operations open when
looking for PointFree instances below. It's actually kinda neat that it can put these in PointFree form though. *)
Definition totalweight {n} (ws: Vector.t Q n): Q := cm_Sum ws.
Notation SomeWeights n := (sig (λ ts: Vector.t Q n, totalweight ts <= 1)%Q).
(** apply_weights: *)
(** Note that this an innerproduct *)
(** |<points,w>|≤|points| |w|
|<points,w>-<points,v>|=|<points,w-v>| ≤||points|| ||w-v||
, the function is Lipshitz with constant norm ||points||*)
Definition apply_weights (w: Vector.t Q (S n)): Q :=
cm_Sum (map (λ p, Qmult (fst p) (snd p)) (zip points (Vector.to_list w))).
Instance apply_weights_mu: UniformlyContinuous_mu apply_weights.
constructor. exact (fun x => x).
Defined.
Instance apply_weights_uc: UniformlyContinuous apply_weights.
constructor; try apply _.
intros ??? H.
(*Check apply_weights. *)
Admitted.
Obligation Tactic := idtac.
(** "inner", the function of n weights: *)
Program Definition inner: SomeWeights n → sig ((∈ nth_deriv_bound))
:= λ ts, nth_deriv (apply_weights (Vector.cons _ (1 - totalweight ts) _ ts))%Q.
Instance inner_mu: UniformlyContinuous_mu inner.
unfold inner.
apply compose_mu.
apply _.
apply (@compose_mu (SomeWeights n) (Vector.t Q (S n)) Q (apply_weights)).
apply _.
Admitted.
Instance inner_uc: UniformlyContinuous inner.
Admitted.
(** Next up is "reduce" *)
Definition G (n: nat): Type := UCFunction (SomeWeights n) (sig ((∈ nth_deriv_bound))).
Local Open Scope CR_scope.
Section reduce.
Variables (m: nat) (X: G (S m)).
Program Definition integrand (ts: SomeWeights m) (t: sig ((∈ (0, (1 - totalweight ts))))%Q): sig ((∈ nth_deriv_bound)) :=
X (@uncurry_Vector_cons Q m (` t, ` ts)).
Next Obligation. intros. change (`t + Σ (` ts) <= 1)%Q. admit. Qed.
Instance integrand_mu: ∀ ts, UniformlyContinuous_mu (integrand ts).
unfold integrand.
intros.
apply compose_mu.
apply _.
constructor.
intro.
apply Qpos2QposInf.
exact H.
Defined.
Instance integrand_uc: ∀ ts, UniformlyContinuous (integrand ts).
Proof.
unfold integrand. intros.
apply compose_uc. apply _.
constructor; try apply _.
simpl. intros.
constructor. assumption.
simpl.
admit. (* doable *)
Qed.
Program Definition reduce_raw: SomeWeights m → sig ((∈ nth_deriv_bound))
:= λ ts, @integrate_ucFunc_wrapped_for_continuity nth_deriv_bound (existT _ (0, 1 - totalweight (` ts))%Q
(ucFunction (integrand ts))).
Next Obligation.
intros.
unfold integrate_ucFunc_wrapped_for_continuity.
simpl.
Admitted. (* need to show that the result is bounded *)
Instance reduce_mu: UniformlyContinuous_mu reduce_raw.
Proof with auto.
unfold reduce_raw.
apply exist_mu.
set (integrate_ucFunc_wrapped_for_continuity nth_deriv_bound).
apply (@compose_mu (SomeWeights m) {r : Range Q & UCFunction (sig ((∈r))) (sig ((∈nth_deriv_bound)))} CR s).
apply _.
admit.
Defined.
Instance reduce_uc: UniformlyContinuous reduce_raw.
Proof with auto.
unfold reduce_raw.
apply exist_uc.
set (integrate_ucFunc_wrapped_for_continuity nth_deriv_bound).
apply (@compose_uc (SomeWeights m) _ _ {r : Range Q & UCFunction (sig ((∈r))) (sig ((∈nth_deriv_bound)))} _ _ CR _ _ s).
apply _.
admit.
Qed.
Definition reduce: G m := ucFunction reduce_raw.
End reduce.
(** Finally, the divided difference arises from iterated reduction of the inner function: *)
Definition alt_divdiff: CR.
refine (proj1_sig (iterate reduce (ucFunction inner) _)).
exists (Vector.nil Q).
abstract (unfold totalweight; simpl; auto).
Defined. (* Todo: Why won't Program work here? *)
End divdiff_as_repeated_integral.
Section divdiffs_equal.
Context (f: Q → CR) (nth_deriv_bound: Range CR) (nth_deriv: Q → sig (∈nth_deriv_bound)).
Lemma divdiffs_equal: ∀ n (xs: Vector.t Q (S n)),
(divdiff (ne_list.map (λ x, (x, f x)) (Vec_to_ne_list _ xs)) == alt_divdiff nth_deriv_bound nth_deriv _ xs)%CR.
Proof with auto.
induction n.
intros.
assert (xs = Vector.cons _ (Vector.hd xs) _ (Vector.nil _)) as E.
do 2 dependent destruction xs.
reflexivity.
rewrite E.
change (f (Vector.hd xs) [=] proj1_sig (nth_deriv (Vector.hd xs * (1 - 0) + 0))).
admit. (* in this case the nth derivative is f itself *)
intros.
simpl in *.
unfold Basics.compose.
dependent destruction xs.
dependent destruction xs.
rewrite Vec_cons_to_ne_list.
unfold divdiff.
rewrite ne_list_head_map.
rewrite ne_list_tail_map.
simpl @ne_list.head.
change (divdiff_l (h, f h) (map (λ x : Q, (x, f x)) (Vec_to_ne_list n (Vector.cons Q h0 n xs)))[=]
alt_divdiff nth_deriv_bound nth_deriv (S n) (Vector.cons Q h (S n) (Vector.cons Q h0 n xs))).
rewrite through_ne.
change (divdiff_l (h, f h) ((h0, f h0) :: map (λ x : Q, (x, f x)) xs)[=]
alt_divdiff nth_deriv_bound nth_deriv (S n) (Vector.cons Q h (S n) (Vector.cons Q h0 n xs))).
simpl.
replace (divdiff_l (h, f h) (map (λ x : Q, (x, f x)) xs)) with (divdiff (ne_list.from_list (h, f h) (map (λ x : Q, (x, f x)) xs))).
Focus 2.
unfold divdiff.
rewrite ne_head_from_list.
rewrite ne_tail_from_list.
reflexivity.
replace (divdiff_l (h0, f h0) (map (λ x : Q, (x, f x)) xs)) with (divdiff (ne_list.from_list (h0, f h0) (map (λ x : Q, (x, f x)) xs))).
Focus 2.
unfold divdiff.
rewrite ne_head_from_list.
rewrite ne_tail_from_list.
reflexivity.
rewrite <- (ne_list_map_from_list (λ x: Q, (x, f x)) xs h).
rewrite <- (ne_list_map_from_list (λ x: Q, (x, f x)) xs h0).
rewrite <- Vec_cons_to_ne_list'.
rewrite <- Vec_cons_to_ne_list'.
rewrite IHn.
rewrite IHn.
clear IHn.
unfold alt_divdiff.
(* now it's "just" an equation between repeated integrals *)
admit.
Qed.
End divdiffs_equal.
End contents.
*)
|
