Require Import Morphisms.
Require Import Equivalence.
Require Import Program.Basics.
Require Import Lra Lia.
Require Import hilbert.
Require Import utils.Utils.
Require Import List.
Require Coquelicot.Hierarchy.
Set Bullet Behavior "
Strict Subproofs".
Require Import DVector.
Section Rvector_defs.
Context {
n:
nat}.
Declare Scope Rvector_scope.
Delimit Scope Rvector_scope with Rvector.
Bind Scope Rvector_scope with vector R.
Lemma vec_Req_EM_T (
v1 v2 :
vector R n) :
{
v1 =
v2} + {
v1 <>
v2}.
Proof.
Definition Rvector_zero :
vector R n
:=
vector_const 0
n.
Notation "0" :=
Rvector_zero :
Rvector_scope.
Definition Rvector_scale (
c:
R) (
x:
vector R n) :
vector R n
:=
vector_map (
fun a =>
c *
a)
x.
Notation "
c .*
v" := (
Rvector_scale (
c%
R)
v) (
at level 41,
right associativity) :
Rvector_scope.
Definition Rvector_opp (
x:
vector R n) :
vector R n
:=
Rvector_scale (-1)
x.
Notation "-
v" := (
Rvector_opp v) (
at level 35,
right associativity) :
Rvector_scope.
Definition Rvector_plus (
x y:
vector R n) :
vector R n
:=
vector_map (
fun '(
a,
b) =>
a +
b) (
vector_zip x y).
Notation "
x +
y" := (
Rvector_plus x y) (
at level 50,
left associativity) :
Rvector_scope.
Definition Rvector_mult (
x y:
vector R n) :
vector R n
:=
vector_map (
fun '(
a,
b) =>
a *
b) (
vector_zip x y).
Notation "
x *
y" := (
Rvector_mult x y) (
at level 40,
left associativity) :
Rvector_scope.
Definition Rvector_sqr (
x:
vector R n) :
vector R n
:=
vector_map (
fun a =>
a²)
x.
Definition Rvector_abs (
x:
vector R n) :
vector R n
:=
vector_map Rabs x.
Definition Rvector_max_abs (
x:
vector R n) :
R
:=
vector_fold_left Rmax (
Rvector_abs x) 0.
Notation "
x ²" := (
Rvector_sqr x) (
at level 1) :
Rvector_scope.
Program Definition Rvector_sum (
v:
vector R n) :
R
:=
RealAdd.list_sum v.
Notation "∑
x " := (
Rvector_sum (
x%
Rvector)) (
at level 40,
left associativity) :
Rvector_scope.
Definition Rvector_inner (
x y:
vector R n) :
R
:=
Rvector_sum (
Rvector_mult x y).
Notation "
x ⋅
y" := (
Rvector_inner x%
Rvector y%
Rvector) (
at level 40,
left associativity) :
Rvector_scope.
Local Open Scope Rvector_scope.
Lemma Rvector_nth_zero i pf :
vector_nth i pf Rvector_zero = 0%
R.
Proof.
Lemma Rvector_plus_explode (
x y:
vector R n) :
x +
y =
vector_create 0
n (
fun i _ pf => (
vector_nth i pf x +
vector_nth i pf y)%
R).
Proof.
Lemma Rvector_nth_plus (
x y:
vector R n)
i pf :
vector_nth i pf (
x +
y) =
Rplus (
vector_nth i pf x) (
vector_nth i pf y).
Proof.
Lemma Rvector_mult_explode (
x y:
vector R n) :
x *
y =
vector_create 0
n (
fun i _ pf => (
vector_nth i pf x *
vector_nth i pf y)%
R).
Proof.
Lemma Rvector_nth_mult (
x y:
vector R n)
i pf :
vector_nth i pf (
x *
y) =
Rmult (
vector_nth i pf x) (
vector_nth i pf y).
Proof.
Lemma Rvector_plus_comm (
x y:
vector R n) :
x +
y =
y +
x.
Proof.
Lemma Rvector_mult_comm (
x y:
vector R n) :
x *
y =
y *
x.
Proof.
Lemma Rvector_nth_scale (
c :
R) (
v :
vector R n) (
i :
nat) (
pf : (
i <
n)%
nat):
vector_nth i pf (
Rvector_scale c v) = (
c *
vector_nth i pf v)%
R.
Proof.
Lemma Rvector_nth_opp (
v :
vector R n) (
i :
nat) (
pf : (
i <
n)%
nat):
vector_nth i pf (
Rvector_opp v) = (-1 *
vector_nth i pf v)%
R.
Proof.
Definition Rvector_minus (
x y:
vector R n) :
vector R n
:=
Rvector_plus x (
Rvector_opp y).
Lemma Rvector_nth_minus (
v1 v2 :
vector R n) (
i :
nat) (
pf : (
i <
n)%
nat):
vector_nth i pf (
Rvector_minus v1 v2) =
(
vector_nth i pf v1) - (
vector_nth i pf v2).
Proof.
Lemma Rvector_plus_eq_compat_l (
v v1 v2 :
vector R n) :
v1 =
v2 ->
Rvector_plus v v1 =
Rvector_plus v v2.
Proof.
congruence.
Qed.
Lemma combine_assoc {
A B C} (
x:
list A) (
y:
list B) (
z:
list C):
combine x (
combine y z) =
map (
fun '(
x,
y,
z) => (
x,(
y,
z))) (
combine (
combine x y)
z).
Proof.
revert y z.
induction x; simpl; trivial.
destruct y; simpl; trivial.
destruct z; simpl; trivial.
now rewrite IHx.
Qed.
Lemma combine_const_r {
A B} (
x:
list A)
c (
y:
list B) :
Forall (
fun a =>
a =
c)
y ->
(
length x <=
length y)%
nat ->
combine x y =
map (
fun a => (
a,
c))
x.
Proof.
revert y.
induction x; simpl; trivial; intros.
destruct y; simpl in *; [lia | ].
invcs H.
f_equal.
apply IHx; trivial.
lia.
Qed.
Lemma combine_map_l {
A B C :
Type} (
f :
A ->
C) (
l1 :
list A) (
l2 :
list B) :
combine (
map f l1)
l2 =
map (
fun '(
x,
y) => (
f x,
y)) (
combine l1 l2).
Proof.
Lemma combine_map_r {
A B D :
Type} (
g :
B ->
D) (
l1 :
list A) (
l2 :
list B) :
combine l1 (
map g l2) =
map (
fun '(
x,
y) => (
x,
g y)) (
combine l1 l2).
Proof.
Lemma Rvector_plus_assoc (
x y z:
vector R n) :
x + (
y +
z) = (
x +
y) +
z.
Proof.
Lemma Rvector_mult_assoc (
x y z:
vector R n) :
x * (
y *
z) = (
x *
y) *
z.
Proof.
Lemma Rvector_plus_zero (
x:
vector R n) :
x + 0 =
x.
Proof.
Lemma Rvector_mult_zero (
x:
vector R n) :
x * 0 = 0.
Proof.
Lemma Rvector_scale_zero (
c :
R) :
Rvector_scale c 0 = 0.
Proof.
Lemma Rvector_scale0 (
v:
vector R n) :
0 .*
v = 0.
Proof.
Lemma Rvector_plus_inv (
x:
vector R n) :
x + (-
x) = 0.
Proof.
Lemma Rvector_inv_plus (
x:
vector R n) : (-
x) +
x = 0.
Proof.
Lemma Rvector_plus_inv' (
x:
vector R n) :
x + (-1 .*
x) = 0.
Proof.
Lemma Rvector_inv_plus' (
x:
vector R n) : (-1 .*
x) +
x = 0.
Proof.
Definition Rvector_AbelianGroup_mixin :
AbelianGroup.mixin_of (
vector R n)
:=
AbelianGroup.Mixin (
vector R n)
Rvector_plus Rvector_opp Rvector_zero
Rvector_plus_comm Rvector_plus_assoc
Rvector_plus_zero Rvector_plus_inv.
Canonical Rvector_AbelianGroup :=
AbelianGroup.Pack (
vector R n)
Rvector_AbelianGroup_mixin (
vector R n).
Lemma Rvector_scale_scale (
a b:
R) (
v:
vector R n) :
a .* (
b .*
v) = (
a *
b) .*
v.
Proof.
Lemma Rvector_scale1 (
v:
vector R n) :
1 .*
v =
v.
Proof.
Lemma Rvector_scale_plus_l (
a:
R) (
x y:
vector R n) :
a .* (
x +
y) =
a .*
x +
a .*
y.
Proof.
Lemma Rvector_scale_plus_r (
a b:
R) (
x:
vector R n) :
(
a +
b) .*
x =
a .*
x +
b .*
x.
Proof.
Definition Rvector_ModuleSpace_mixin :
ModuleSpace.mixin_of R_Ring Rvector_AbelianGroup
:=
ModuleSpace.Mixin R_Ring Rvector_AbelianGroup
Rvector_scale Rvector_scale_scale Rvector_scale1
Rvector_scale_plus_l Rvector_scale_plus_r.
Canonical Rvector_ModuleSpace :=
ModuleSpace.Pack R_Ring (
vector R n) (
ModuleSpace.Class R_Ring (
vector R n)
Rvector_AbelianGroup_mixin Rvector_ModuleSpace_mixin) (
vector R n).
Lemma Rvector_scale_inj (
c:
R) (
x y:
vector R n) :
c <> 0%
R ->
c .*
x =
c .*
y ->
x =
y.
Proof.
Lemma Rvector_inner_comm (
x y:
vector R n) :
x ⋅
y =
y ⋅
x.
Proof.
Lemma Rvector_sum_const c : ∑ (
vector_const c n) = (
INR n *
c)%
R.
Proof.
Program Lemma Rvector_sum0 : ∑ 0 = 0%
R.
Proof.
Program Lemma Rvector_sum_pos (
x:
vector R n) :
(
forall a,
In a x -> 0%
R <=
a) -> 0 <= ∑
x.
Proof.
Lemma Rvector_sqr_mult (
x:
vector R n) :
x² =
x *
x.
Proof.
Program Lemma Rvector_sqr_pos (
x:
vector R n) :
forall a,
In a x² -> 0 <=
a.
Proof.
Lemma Rvector_inner_pos (
x:
vector R n) : 0%
R <=
x ⋅
x.
Proof.
Program Lemma Rvector_sum_pos_0 (
x:
vector R n) :
(
forall a,
In a x -> 0%
R <=
a) ->
∑
x = 0%
R ->
x = 0.
Proof.
Lemma Rvector_sqr_zero_inv (
x:
vector R n) :
x² = 0 ->
x = 0.
Proof.
Lemma Rvector_inner_zero (
x:
vector R n) :
x ⋅ 0 = 0%
R.
Proof.
Lemma Rvector_inner_one_r (
x:
vector R n) :
x ⋅
vector_const 1%
R n = ∑
x.
Proof.
Lemma Rvector_inner_one_l (
x:
vector R n) :
vector_const 1%
R n ⋅
x = ∑
x.
Proof.
Lemma Rvector_inner_zero_inv (
x:
vector R n) :
x ⋅
x = 0%
R ->
x = 0.
Proof.
Lemma Rvector_scale_mult_l (
a:
R) (
x y:
vector R n) :
((
a .*
x) *
y) =
a .* (
x *
y).
Proof.
Lemma Rvector_scale_sum (
a:
R) (
x:
vector R n) :
∑ (
a .*
x) =
Rmult a (∑
x).
Proof.
Lemma Rvector_inner_scal (
x y:
vector R n) (
l:
R) : (
l .*
x) ⋅
y =
Rmult l (
x ⋅
y).
Proof.
Lemma Rvector_scal_one c :
c .*
vector_const 1
n =
vector_const c n.
Proof.
Lemma Rvector_inner_const_l (
x:
vector R n)
c :
vector_const c n ⋅
x = (
c * ∑
x)%
R.
Proof.
Lemma Rvector_inner_const_r (
x:
vector R n)
c :
x ⋅
vector_const c n = (
c * ∑
x)%
R.
Proof.
Lemma Rvector_mult_plus_distr_r (
x y z:
vector R n) :
(
x +
y) *
z = (
x *
z) + (
y *
z).
Proof.
Lemma Rvector_sum_plus_distr (
x y:
vector R n) :
∑ (
x +
y) = (∑
x + ∑
y)%
R.
Proof.
unfold Rvector_sum,
Rvector_plus;
simpl.
destruct x;
destruct y;
simpl.
subst.
revert x0 e0.
induction x;
destruct x0;
simpl in *;
try discriminate;
intros.
-
lra.
-
invcs e0.
rewrite IHx;
trivial.
lra.
Qed.
Lemma Rvector_inner_plus (
x y z:
vector R n) : (
x +
y) ⋅
z =
Rplus (
x ⋅
z) (
y ⋅
z).
Proof.
Definition Rvector_PreHilbert_mixin :
PreHilbert.mixin_of (
Rvector_ModuleSpace)
:=
PreHilbert.Mixin (
Rvector_ModuleSpace)
Rvector_inner
Rvector_inner_comm Rvector_inner_pos Rvector_inner_zero_inv
Rvector_inner_scal Rvector_inner_plus.
Canonical Rvector_PreHilbert :=
PreHilbert.Pack (
vector R n) (
PreHilbert.Class _ _ Rvector_PreHilbert_mixin) (
vector R n).
Definition Rvector_filter_part {
T} (
F:(
vector T n ->
Prop) ->
Prop)
i (
pf:(
i <
n)%
nat) : (
T ->
Prop) ->
Prop
:=
fun (
s:
T->
Prop) =>
F (
fun v =>
s (
vector_nth i pf v)).
Definition Rvector_lim (
F:(
vector R n ->
Prop) ->
Prop) :
vector R n
:=
vector_create 0
n
(
fun i _ pf =>
Hierarchy.lim (
Rvector_filter_part F i pf
)).
Lemma Rvector_filter_part_Filter {
T} (
F:(
vector T n ->
Prop) ->
Prop)
i pf :
Filter F ->
Filter (
Rvector_filter_part F i pf).
Proof.
unfold Rvector_filter_part.
intros [???].
constructor;
intros;
auto.
-
eapply filter_imp;
try eapply H0.
simpl;
intros;
eauto.
Qed.
Lemma Rvector_filter_part_ProperFilter {
T} (
F:(
vector T n ->
Prop) ->
Prop)
i pf :
ProperFilter F ->
ProperFilter (
Rvector_filter_part F i pf).
Proof.
Lemma minus_nth (
x x0 :
vector R n) (
i:
nat) (
pf : (
i <
n)%
nat):
minus (
vector_nth i pf x0) (
vector_nth i pf x) =
vector_nth i pf (
minus x0 x).
Proof.
Lemma mult_nth (
x x0 :
vector R n) (
i:
nat) (
pf : (
i <
n)%
nat):
((
vector_nth i pf x0) * (
vector_nth i pf x))%
R =
vector_nth i pf (
Rvector_mult x0 x).
Proof.
Lemma list_sum_pos_In_le (
l:
list R) (
a:
R)
(
all_pos :
forall a :
R,
In a l -> 0 <=
a):
In a l ->
a <=
RealAdd.list_sum l.
Proof.
induction l;
simpl;
inversion 1;
simpl in *.
-
subst.
generalize (
list_sum_pos_pos'
l);
intros HH.
cut_to HH.
+
lra.
+
rewrite Forall_forall;
eauto.
-
cut_to IHl;
trivial.
+
specialize (
all_pos a0).
cut_to all_pos;
auto;
try lra.
+
eauto.
Qed.
Program Lemma vector_nth_pos_le_pos (
v:
vector R n)
i pf :
(
forall a,
In a v -> 0%
R <=
a) ->
vector_nth i pf v <= ∑
v.
Proof.
Lemma Hnorm_nth1 (
x :
vector R n) (
eps0 :
posreal) (
i:
nat) (
pf : (
i <
n)%
nat):
Hnorm x <
eps0 ->
abs (
vector_nth i pf x) <
eps0.
Proof.
Lemma Hnorm_nth (
x x0 :
vector R n) (
eps0 :
posreal) (
i:
nat) (
pf : (
i <
n)%
nat):
Hnorm (
minus x x0) <
eps0 ->
Hierarchy.ball (
vector_nth i pf x)
eps0 (
vector_nth i pf x0).
Proof.
Lemma list_sum_bound_const_lt (
l :
list R)
(
c :
R) :
l <>
nil ->
(
forall a :
R,
In a l ->
a <
c) ->
RealAdd.list_sum l <
c *
INR (
length l).
Proof.
intros nnil bounded.
induction l; simpl in *; try congruence.
destruct l; simpl.
- ring_simplify.
auto.
- simpl in *.
cut_to IHl; try congruence; auto.
specialize (bounded a).
cut_to bounded; auto.
lra.
Qed.
Lemma list_sum_bound_const_le (
l :
list R)
(
c :
R) :
l <>
nil ->
(
forall a :
R,
In a l ->
a <=
c) ->
RealAdd.list_sum l <=
c *
INR (
length l).
Proof.
intros nnil bounded.
induction l; simpl in *; try congruence.
destruct l; simpl.
- ring_simplify.
auto.
- simpl in *.
cut_to IHl; try congruence; auto.
specialize (bounded a).
cut_to bounded; auto.
lra.
Qed.
Program Lemma Rvector_sum_bound_const_lt (
x:
vector R n)
c :
n <> 0%
nat ->
(
forall a,
In a x -> (
a <
c)%
R) ->
∑
x < (
c *
INR n)%
R.
Proof.
Program Lemma Rvector_sum_bound_const_le (
x:
vector R n)
c :
n <> 0%
nat ->
(
forall a,
In a x -> (
a <=
c)%
R) ->
∑
x <= (
c *
INR n)%
R.
Proof.
Lemma Nth_Hnorm1 (
x :
vector R n) (
eps :
posreal) :
(0 <
n)%
nat ->
(
forall (
i :
nat) (
pf : (
i <
n)%
nat),
abs (
vector_nth i pf x) <
eps /
INR n) ->
Hnorm x <
eps.
Proof.
Lemma Nth_Hnorm (
v x :
vector R n) (
eps :
posreal) :
(0 <
n)%
nat ->
(
forall (
i :
nat) (
pf : (
i <
n)%
nat),
Hierarchy.ball (
vector_nth i pf v) (
eps /
INR n) (
vector_nth i pf x)) ->
Hnorm (
minus v x) <
eps.
Proof.
Lemma Rvector_filter_part_cauchy (
F:(
PreHilbert_UniformSpace ->
Prop) ->
Prop)
i pf :
Filter F ->
cauchy F ->
cauchy (
Rvector_filter_part F i pf).
Proof.
Lemma Rvector_inner_self (
x:
vector R n) :
x ⋅
x = ∑
x².
Proof.
Lemma Filter_Forall_commute_aux F P :
Filter F ->
(
forall (
i :
nat) (
pf : (
i <
n)%
nat),
F (
fun v :
vector R n =>
P i pf (
vector_nth i pf v))) ->
forall m (
pf2:(
m <=
n)%
nat),
F (
fun v :
vector R n =>
forall (
i :
nat) (
pf : (
i <
m)%
nat),
P i (
lt_le_trans _ _ _ pf pf2) (
vector_nth i (
lt_le_trans _ _ _ pf pf2)
v)).
Proof.
Lemma Filter_Forall_commute F P :
Filter F ->
(
forall (
i :
nat) (
pf : (
i <
n)%
nat),
F (
fun v :
vector R n =>
P i pf (
vector_nth i pf v))) ->
F (
fun v :
vector R n =>
forall (
i :
nat) (
pf : (
i <
n)%
nat),
P i pf (
vector_nth i pf v)).
Proof.
Lemma Rvector_lim_complete_pos (
F : (
PreHilbert_UniformSpace ->
Prop) ->
Prop) :
(0 <
n)%
nat ->
ProperFilter F ->
cauchy F ->
forall eps :
posreal,
F (
ball (
Rvector_lim F)
eps).
Proof.
Lemma vector_zero0 (
n0:
n = 0%
nat) (
v:
vector R n) :
v = 0.
Proof.
Lemma Rvector_lim_complete (
F : (
PreHilbert_UniformSpace ->
Prop) ->
Prop) :
ProperFilter F ->
cauchy F ->
forall eps :
posreal,
F (
ball (
Rvector_lim F)
eps).
Proof.
Definition Rvector_Hilbert_mixin :
Hilbert.mixin_of Rvector_PreHilbert
:=
Hilbert.Mixin Rvector_PreHilbert Rvector_lim Rvector_lim_complete.
Canonical Rvector_Hilbert :=
Hilbert.Pack (
vector R n) (
Hilbert.Class _ _ Rvector_Hilbert_mixin) (
vector R n).
End Rvector_defs.
Section more_lemmas.
Lemma Rvector_mult_rsqr {
n} (
v :
vector R n) :
Rvector_mult v v =
vector_map Rsqr v.
Proof.
Lemma rsqr_Rvector_max_abs {
n:
nat} (
v :
vector R n) :
Rsqr (
Rvector_max_abs v) =
Rvector_max_abs (
vector_map Rsqr v).
Proof.
Lemma Rvector_max_abs_in_le {
n} (
v:
vector R n)
a :
In a (
proj1_sig v) ->
Rabs a <=
Rvector_max_abs v.
Proof.
Lemma Rvector_max_abs_nth_le {
n} (
v:
vector R n)
i pf:
Rabs (
vector_nth i pf v) <=
Rvector_max_abs v.
Proof.
Lemma Rvector_max_abs_in {
n} (
v:
vector R (
S n)) :
In (
Rvector_max_abs v) (
proj1_sig (
vector_map Rabs v)).
Proof.
Lemma Rvector_max_abs_nth_in {
n} (
v:
vector R (
S n)) :
exists i pf,
Rvector_max_abs v =
Rabs (
vector_nth i pf v).
Proof.
Program Lemma Rvector_sum_pos_in_le {
n}
x (
v :
vector R n) :
(
forall a,
In a v -> 0%
R <=
a) ->
In x v ->
x <=
Rvector_sum v.
Proof.
Lemma Rvector_max_abs_nonneg {
n} (
v:
vector R n) : 0 <=
Rvector_max_abs v.
Proof.
Lemma sqr_max_abs_le_inner {
n:
nat} (
v :
vector R n) :
(
Rvector_max_abs v)² <=
Rvector_inner v v.
Proof.
Lemma inner_le_sqr_max_abs {
n:
nat} (
v :
vector R n) :
Rvector_inner v v <=
INR n * (
Rvector_max_abs v)².
Proof.
Lemma max_abs_le_sqrt_inner {
n:
nat} (
v :
vector R n) :
(
Rvector_max_abs v) <=
Rsqrt (
mknonnegreal (
Rvector_inner v v) (
Rvector_inner_pos v)).
Proof.
Lemma vector_nth_sum_n {
n:
nat}
i pf k (
f:
nat->
vector R n) :
vector_nth i pf (
sum_n f k) =
sum_n (
fun j =>
vector_nth i pf (
f j))
k.
Proof.
Lemma Rvector_max_abs_zero {
n} (
v :
vector R n) :
Rvector_max_abs v = 0 <->
v =
Rvector_zero.
Proof.
Lemma Rvector_max_abs_scale {
n}
c (
v :
vector R n) :
Rvector_max_abs (
Rvector_scale c v) =
Rabs c *
Rvector_max_abs v.
Proof.
Lemma Rvector_max_abs_scale_nneg {
n} (
c:
nonnegreal) (
v :
vector R n) :
Rvector_max_abs (
Rvector_scale c v) =
c *
Rvector_max_abs v.
Proof.
Lemma Rvector_max_abs_triang {
n} (
v1 v2 :
vector R n) :
Rvector_max_abs (
Rvector_plus v1 v2) <=
Rvector_max_abs v1 +
Rvector_max_abs v2.
Proof.
End more_lemmas.