From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap.
From mathcomp Require Import mathcomp_extra boolp classical_sets functions.
From mathcomp Require Import cardinality.
# Finitely-supported big operators
```
finite_support idx D F := D `&` F @^-1` [set~ idx]
\big[op/idx]_(i \in A) F i == iterated application of the operator op
with neutral idx over finite_support idx A F
\sum_(i \in A) F i == iterated addition, in ring_scope
```
Reserved Notation "\big [ op / idx ]_ ( i '\in' A ) F"
(
at level 36, F at level 36, op, idx at level 10, i, A at level 50,
format "'[' \big [ op / idx ]_ ( i '\in' A ) '/ ' F ']'").
Reserved Notation "\sum_ ( i '\in' A ) F"
(
at level 41, F at level 41, i, A at level 50,
format "'[' \sum_ ( i '\in' A ) '/ ' F ']'").
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
Notation
"\big [ op / idx ]_ ( i '\in' A ) F"
:=
(
\big[op/idx]_(
i
<- fset_set (
A `&` ((
fun
i
=> F)
@^-1` [set~ idx])))
F)
(
only parsing)
: big_scope.
Lemma
finite_index_key
: unit
Proof.
Definition
finite_support
{I : choiceType} {T : Type} (
idx
: T) (
D
: set I)
(
F
: I -> T)
: seq I :=
locked_with finite_index_key (
fset_set (
D `&` F @^-1` [set~ idx] : set I)).
Notation
"\big [ op / idx ]_ ( i '\in' D ) F"
:=
(
\big[op/idx]_(
i
<- finite_support idx D (
fun
i
=> F))
F)
: big_scope.
Lemma
in_finite_support
(
T
: Type) (
J
: choiceType) (
i
: T) (
P
: set J)
(
F
: J -> T)
: finite_set (
P `&` F @^-1` [set~ i])
->
finite_support i P F =i P `&` F @^-1` [set~ i].
Proof.
Lemma
finite_support_uniq
(
T
: Type) (
J
: choiceType) (
i
: T) (
P
: set J)
(
F
: J -> T)
: uniq (
finite_support i P F).
Proof.
#[global] Hint Resolve finite_support_uniq : core.
Lemma
no_finite_support
(
T
: Type) (
J
: choiceType) (
i
: T) (
P
: set J)
(
F
: J -> T)
: infinite_set (
P `&` F @^-1` [set~ i])
->
finite_support i P F = [::].
Proof.
move=> infinF; rewrite /finite_support unlock.
by rewrite /fset_set/=; case: pselect => //.
Qed.
Lemma
eq_finite_support
{I : choiceType} {T : Type} (
idx
: T) (
D
: set I)
(
F
G
: I -> T)
: {in D, F =1 G} ->
finite_support idx D F = finite_support idx D G.
Proof.
by move=> eqFG; rewrite /finite_support !unlock// (
eq_preimage _ eqFG).
Qed.
Variant
finite_support_spec
R
(
T
: choiceType)
(
P
: set T) (
F
: T -> R) (
idx
: R)
: seq T -> Type :=
|
NoFiniteSupport
of infinite_set (
P `&` F @^-1` [set~ idx])
:
finite_support_spec P F idx [::]
|
FiniteSupport
(
X
: {fset T})
of [set` X] `<=` P
& (
forall
i,
P i -> i \notin X -> F i = idx)
& [set` X] = (
P `&` F @^-1` [set~ idx])
:
finite_support_spec P F idx X.
Lemma
finite_supportP
R
(
T
: choiceType) (
P
: set T) (
F
: T -> R) (
idx
: R)
:
finite_support_spec P F idx (
finite_support idx P F).
Proof.
rewrite /finite_support unlock/= /fset_set.
case: pselect=> // Xfin; last by constructor.
case: cid => //= X eqX; constructor; rewrite -?eqX//.
move=> i Pi NXi /=; have : (
P `\` [set` X])
i by split=> //=; apply/negP.
by rewrite -eqX /= => -[_]; apply: contra_notP.
Qed.
Notation
"\sum_ ( i '\in' A ) F"
:= (
\big[+%R/0%R]_(
i
\in A)
F)
: ring_scope.
Lemma
eq_fsbigl
(
R
: Type) (
idx
: R) (
op
: R -> R -> R)
(
T
: choiceType) (
f
: T -> R) (
P
Q
: set T)
:
P = Q -> \big[op/idx]_(
x
\in P)
f x = \big[op/idx]_(
x
\in Q)
f x.
Proof.
by move=> ->. Qed.
Lemma
eq_fsbigr
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx)
(
T
: choiceType) (
f
g
: T -> R) (
P
: set T)
:
{in P, f =1 g} -> (
\big[op/idx]_(
x
\in P)
f x = \big[op/idx]_(
x
\in P)
g x).
Proof.
Arguments eq_fsbigr {R idx op T f} g.
Lemma
fsbigTE
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx) (
T
: choiceType)
(
A
: {fset T}) (
f
: T -> R)
:
(
forall
i,
i \notin A -> f i = idx)
->
\big[op/idx]_(
i
\in [set: T])
f i = \big[op/idx]_(
i
<- A)
f i.
Proof.
Arguments fsbigTE {R idx op T} A f.
Lemma
fsbig_mkcond
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx)
(
T
: choiceType) (
A
: set T) (
f
: T -> R)
:
\big[op/idx]_(
i
\in A)
f i =
\big[op/idx]_(
i
\in [set: T])
patch (
fun=> idx)
A f i.
Proof.
Lemma
fsbig_mkcondr
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx)
(
T
: choiceType) (
I
J
: set T) (
a
: T -> R)
:
\big[op/idx]_(
i
\in I `&` J)
a i =
\big[op/idx]_(
i
\in I)
if i \in J then a i else idx.
Proof.
Lemma
fsbig_mkcondl
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx)
(
T
: choiceType) (
I
J
: set T) (
a
: T -> R)
:
\big[op/idx]_(
i
\in I `&` J)
a i =
\big[op/idx]_(
i
\in J)
if i \in I then a i else idx.
Proof.
Lemma
bigfs
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx) (
T
: choiceType)
(
r
: seq T) (
P
: {pred T}) (
f
: T -> R)
: uniq r ->
(
forall
i,
P i -> i \notin r -> f i = idx)
->
\big[op/idx]_(
i
<- r | P i)
f i = \big[op/idx]_(
i
\in [set` P])
f i.
Proof.
Lemma
fsbigE
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx) (
T
: choiceType)
(
A
: set T) (
r
: seq T) (
f
: T -> R)
:
uniq r ->
[set` r] `<=` A ->
(
forall
i,
A i -> i \notin r -> f i = idx)
->
\big[op/idx]_(
i
\in A)
f i = \big[op/idx]_(
i
<- r | i \in A)
f i.
Proof.
move=> r_uniq rQ fidx; rewrite [RHS]bigfs ?set_mem_set//=.
by move=> i; rewrite inE; apply: fidx.
Qed.
Arguments fsbigE {R idx op T A}.
Lemma
fsbig_seq
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx)
(
I
: choiceType) (
r
: seq I) (
F
: I -> R)
:
uniq r ->
\big[op/idx]_(
a
<- r)
F a = \big[op/idx]_(
a
\in [set` r])
F a.
Proof.
Lemma
fsbig1
(
R
: Type) (
idx
: R) (
op
: Monoid.law idx) (
I
: choiceType)
(
P
: set I) (
F
: I -> R)
:
(
forall
i,
P i -> F i = idx)
-> \big[op/idx]_(
i
\in P)
F i = idx.
Proof.
Lemma
fsbig_dflt
(
R
: Type) (
idx
: R) (
op
: Monoid.law idx) (
I
: choiceType)
(
P
: set I) (
F
: I -> R)
:
infinite_set (
P `&` F @^-1` [set~ idx])
-> \big[op/idx]_(
i
\in P)
F i = idx.
Proof.
Lemma
fsbig_widen
(
T
: choiceType)
[R : Type] [idx : R]
(
op
: Monoid.com_law idx) (
P
D
: set T) (
f
: T -> R)
:
P `<=` D ->
D `\` P `<=` f @^-1` [set idx] ->
\big[op/idx]_(
i
\in P)
f i = \big[op/idx]_(
i
\in D)
f i.
Proof.
Arguments fsbig_widen {T R idx op} P D f.
Lemma
fsbig_supp
(
T
: choiceType)
[R : Type] [idx : R]
(
op
: Monoid.com_law idx) (
P
: set T) (
f
: T -> R)
:
\big[op/idx]_(
i
\in P)
f i = \big[op/idx]_(
i
\in P `&` f @^-1` [set~ idx])
f i.
Proof.
by apply/esym/fsbig_widen => // x [Px /not_andP[]//=]; rewrite notK. Qed.
Lemma
fsbig_fwiden
(
T
: choiceType)
[R : eqType] [idx : R]
(
op
: Monoid.com_law idx)
(
r
: seq T) (
P
: set T) (
f
: T -> R)
:
P `<=` [set` r] ->
uniq r ->
[set
i
| i \in r] `\` P `<=` f @^-1` [set idx] ->
\big[op/idx]_(
i
\in P)
f i = \big[op/idx]_(
i
<- r)
f i.
Proof.
Arguments fsbig_fwiden {T R idx op} r P f.
Lemma
fsbig_set0
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx) (
T
: choiceType)
(
F
: T -> R)
: \big[op/idx]_(
x
\in set0)
F x = idx.
Proof.
Lemma
fsbig_set1
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx) (
T
: choiceType)
x
(
F
: T -> R)
: \big[op/idx]_(
y
\in [set x])
F y = F x.
Proof.
rewrite (
fsbigE [:: x])
//= ?big_cons ?big_nil ?ifT ?inE ?Monoid.
simpm//.
by move=> y /=; rewrite inE => /eqP.
by move=> i ->; rewrite inE eqxx.
Qed.
Lemma
__deprecated__full_fsbigID
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx)
(
I
: choiceType) (
B
: set I) (
A
: set I) (
F
: I -> R)
:
finite_set (
A `&` F @^-1` [set~ idx])
->
\big[op/idx]_(
i
\in A)
F i = op (
\big[op/idx]_(
i
\in A `&` B)
F i)
(
\big[op/idx]_(
i
\in A `&` ~` B)
F i).
Proof.
Arguments __deprecated__full_fsbigID {R idx op I} B.
Lemma
fsbigID
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx)
(
I
: choiceType) (
B
: set I) (
A
: set I) (
F
: I -> R)
:
finite_set A ->
\big[op/idx]_(
i
\in A)
F i = op (
\big[op/idx]_(
i
\in A `&` B)
F i)
(
\big[op/idx]_(
i
\in A `&` ~` B)
F i).
Proof.
Arguments fsbigID {R idx op I} B.
#[deprecated(
note="Use fsbigID instead")
]
Notation
full_fsbigID
:= __deprecated__full_fsbigID (
only parsing).
Lemma
fsbigU
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx)
(
I
: choiceType) (
A
B
: set I) (
F
: I -> R)
:
finite_set A -> finite_set B -> A `&` B `<=` F @^-1` [set idx] ->
\big[op/idx]_(
i
\in A `|` B)
F i =
op (
\big[op/idx]_(
i
\in A)
F i) (
\big[op/idx]_(
i
\in B)
F i).
Proof.
Arguments fsbigU {R idx op I} [A B F].
Lemma
fsbigU0
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx)
(
I
: choiceType) (
A
B
: set I) (
F
: I -> R)
:
finite_set A -> finite_set B -> A `&` B `<=` set0 ->
\big[op/idx]_(
i
\in A `|` B)
F i =
op (
\big[op/idx]_(
i
\in A)
F i) (
\big[op/idx]_(
i
\in B)
F i).
Proof.
by move=> Af Bf AB0; rewrite fsbigU// => x /AB0. Qed.
Lemma
fsbigD1
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx)
(
I
: choiceType) (
i
: I) (
A
: set I) (
F
: I -> R)
:
finite_set A -> A i ->
\big[op/idx]_(
j
\in A)
F j = op (
F i) (
\big[op/idx]_(
j
\in A `\ i)
F j).
Proof.
by move=> *; rewrite (
fsbigID [set i])
?setI1 ?ifT ?inE ?fsbig_set1. Qed.
Arguments fsbigD1 {R idx op I} i A F.
Lemma
full_fsbig_distrr
(
R
: Type) (
zero
: R) (
times
: Monoid.mul_law zero)
(
plus
: Monoid.add_law zero times) (
I
: choiceType) (
a
: R) (
P
: set I)
(
F
: I -> R)
:
finite_set (
P `&` F @^-1` [set~ zero])
->
times a (
\big[plus/zero]_(
i
\in P)
F i)
=
\big[plus/zero]_(
i
\in P)
times a (
F i).
Proof.
Lemma
fsbig_distrr
(
R
: Type) (
zero
: R) (
times
: Monoid.mul_law zero)
(
plus
: Monoid.add_law zero times) (
I
: choiceType) (
a
: R) (
P
: set I)
(
F
: I -> R)
:
finite_set P ->
times a (
\big[plus/zero]_(
i
\in P)
F i)
=
\big[plus/zero]_(
i
\in P)
times a (
F i).
Proof.
Lemma
mulr_fsumr
(
R
: idomainType) (
I
: choiceType)
a
(
P
: set I) (
F
: I -> R)
:
a * (
\sum_(
i
\in P)
F i)
= \sum_(
i
\in P)
a * F i.
Proof.
Lemma
mulr_fsuml
(
R
: idomainType) (
I
: choiceType)
a
(
P
: set I) (
F
: I -> R)
:
(
\sum_(
i
\in P)
F i)
* a = \sum_(
i
\in P) (
F i * a).
Proof.
Lemma
fsbig_ord
R
(
idx
: R) (
op
: Monoid.com_law idx)
n
(
F
: nat -> R)
:
\big[op/idx]_(
a
< n)
F a = \big[op/idx]_(
a
\in `I_n)
F a.
Proof.
Lemma
fsbig_finite
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx) (
T
: choiceType)
(
D
: set T) (
F
: T -> R)
: finite_set D ->
\big[op/idx]_(
x
\in D)
F x = \big[op/idx]_(
x
<- fset_set D)
F x.
Proof.
elim/Peq: R => R in idx op F * => Dfin.
by apply: fsbig_fwiden; rewrite ?fset_setK// setDv.
Qed.
Section
fsbig2
.
Variables (
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx).
Lemma
reindex_fsbig
{I
J
: choiceType} (
h
: I -> J)
P
Q
(
F
: J -> R)
: set_bij P Q h ->
\big[op/idx]_(
j
\in Q)
F j = \big[op/idx]_(
i
\in P)
F (
h i).
Proof.
elim/choicePpointed: I => I in h P *.
rewrite !emptyE => /Pbij[{}h ->].
by rewrite -[in LHS](
image_eq h)
image_set0 !fsbig_set0.
elim/choicePpointed: J => J in F h Q *; first by have := no (
h point).
move=> /(
@pPbij _ _ _)
[{}h ->].
pose A := P `&` (
F \o h)
@^-1` [set~ idx].
pose B := Q `&` F @^-1` [set~ idx].
have /(
@pPbij _ _ _)
[g gh] : set_bij A B h.
apply: splitbij_sub; rewrite /A /B /preimage //=.
by move=> x [Px Fhx]; split=> //; apply: funS.
by move=> x [Qx Fx]; split; rewrite ?invK ?inE//; apply: funS.
case: finite_supportP; rewrite ?big_nil//=.
case: finite_supportP; rewrite ?big_nil//=.
move=> X XP _ XE []; rewrite -/B -(
image_eq g)
/A.
by apply: finite_image; rewrite -XE.
move=> Y YQ Fidx YE; case: finite_supportP.
move=> []; rewrite -/A -(
image_eq [bij of g^-1%FUN]).
by apply: finite_image; rewrite /B -YE.
move=> X XP Fhidx XE; suff -> : Y = (
h @` X)
%fset.
by rewrite big_imfset// => ? ? ? ? /inj; apply; rewrite inE; apply: XP.
have BY j : (
B j)
= (
j \in Y)
by rewrite -[RHS]/(
[set` Y] j)
YE.
have AX i : (
A i)
= (
i \in X)
by rewrite -[RHS]/(
[set` X] i)
XE.
rewrite gh; apply/fsetP=> j; apply/idP/imfsetP => [Yj | [i iX ->]]; last first.
by rewrite -BY; apply: funS; rewrite AX.
by exists (
g^-1%FUN j)
; rewrite ?invK ?inE ?BY// -AX; apply: funS; rewrite BY.
Qed.
Lemma
fsbig_image
{I
J
: choiceType}
P
(
h
: I -> J) (
F
: J -> R)
: set_inj P h ->
\big[op/idx]_(
j
\in h @` P)
F j = \big[op/idx]_(
i
\in P)
F (
h i).
Proof.
Lemma
__deprecated__reindex_inside
{I
J
: choiceType}
P
Q
(
h
: I -> J) (
F
: J -> R)
:
bijective h -> P `<=` h @` Q -> Q `<=` h @^-1` P ->
\big[op/idx]_(
j
\in P)
F j = \big[op/idx]_(
i
\in Q)
F (
h i).
Proof.
Lemma
reindex_fsbigT
{I
J
: choiceType} (
h
: I -> J) (
F
: J -> R)
:
bijective h ->
\big[op/idx]_(
j
\in [set: J])
F j = \big[op/idx]_(
i
\in [set: I])
F (
h i).
Proof.
by rewrite -setTT_bijective => -[? ? ?]; apply: reindex_fsbig. Qed.
End fsbig2.
Arguments reindex_fsbig {R idx op I J} _ _ _.
Arguments fsbig_image {R idx op I J} _ _.
Arguments __deprecated__reindex_inside {R idx op I J} _ _.
Arguments reindex_fsbigT {R idx op I J} _ _.
#[deprecated(
note="use reindex_fsbig, fsbig_image or reindex_fsbigT instead")
]
Notation
reindex_inside
:= __deprecated__reindex_inside (
only parsing).
#[deprecated(
note="use reindex_fsbigT instead")
]
Notation
reindex_inside_setT
:= reindex_fsbigT (
only parsing).
Lemma
fsbigN1
(
R
: eqType) (
idx
: R) (
op
: Monoid.com_law idx)
(
T1
T2
: choiceType) (
Q
: set T2) (
f
: T1 -> T2 -> R) (
x
: T1)
:
\big[op/idx]_(
y
\in Q)
f x y != idx -> exists2
y,
Q y & f x y != idx.
Proof.
apply: contra_neqP => /forall2NP Qf; apply/fsbig1 => y Qy.
by case: (
Qf y)
=> // /negP/negPn/eqP->.
Qed.
Lemma
fsbig_split
(
T
: choiceType) (
R
: eqType) (
idx
: R)
(
op
: Monoid.com_law idx) (
P
: set T) (
f
g
: T -> R)
: finite_set P ->
\big[op/idx]_(
x
\in P)
op (
f x) (
g x)
=
op (
\big[op/idx]_(
x
\in P)
f x) (
\big[op/idx]_(
x
\in P)
g x).
Proof.
by move=> Pfin; rewrite !fsbig_finite// big_split. Qed.
Lemma
fsumr_ge0
(
R
: numDomainType) (
I
: choiceType) (
P
: set I) (
F
: I -> R)
:
(
forall
i,
P i -> 0 <= F i)
-> 0 <= \sum_(
i
\in P)
F i.
Proof.
Lemma
fsumr_le0
(
R
: numDomainType) (
I
: choiceType) (
P
: set I) (
F
: I -> R)
:
(
forall
i,
P i -> F i <= 0)
-> \sum_(
i
\in P)
F i <= 0.
Proof.
Lemma
fsumr_gt0
(
R
: realDomainType) (
I
: choiceType) (
r
: seq I) (
P
: set I)
(
F
: I -> R)
:
0 < \sum_(
i
\in P)
F i -> exists2
i,
P i & 0 < F i.
Proof.
Lemma
fsumr_lt0
(
R
: realDomainType) (
I
: choiceType) (
P
: set I)
(
F
: I -> R)
:
\sum_(
i
\in P)
F i < 0 -> exists2
i,
P i & F i < 0.
Proof.
Lemma
pfsumr_eq0
(
R
: realDomainType) (
I
: choiceType) (
P
: set I)
(
F
: I -> R)
:
finite_set P ->
(
forall
i,
P i -> 0 <= F i)
->
\sum_(
i
\in P)
F i = 0 -> forall
i,
P i -> F i = 0.
Proof.
Lemma
fsbig_setU
{T} {I : choiceType} (
A
: set I) (
F
: I -> set T)
:
finite_set A ->
\big[setU/set0]_(
i
\in A)
F i = \bigcup_(
i
in A)
F i.
Proof.
Lemma
fsbig_setU_set1
{T : choiceType} (
A
: set T)
:
finite_set A -> \big[setU/set0]_(
x
\in A)
[set x] = A.
Proof.
move=> fA; rewrite fsbig_setU//.
by apply/seteqP; split=> [t [x Ax ->]//|t At]; exists t.
Qed.
Lemma
pair_fsbig
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx)
(
I
J
: choiceType) (
P
: set I) (
Q
: set J) (
F
: I -> J -> R)
:
finite_set P -> finite_set Q ->
\big[op/idx]_(
i
\in P)
\big[op/idx]_(
j
\in Q)
F i j
= \big[op/idx]_(
p
\in P `*` Q)
F p.
1 p.
2.
Proof.
Lemma
exchange_fsbig
(
R
: Type) (
idx
: R) (
op
: Monoid.com_law idx)
(
I
J
: choiceType) (
P
: set I) (
Q
: set J) (
F
: I -> J -> R)
:
finite_set P -> finite_set Q ->
\big[op/idx]_(
i
\in P)
\big[op/idx]_(
j
\in Q)
F i j
= \big[op/idx]_(
j
\in Q)
\big[op/idx]_(
i
\in P)
F i j.
Proof.
move=> Pfin Qfin; rewrite 2?pair_fsbig//; pose swap (
x
: I * J)
:= (
x.
2, x.
1).
apply/esym/(
reindex_fsbig swap).
split=> [? [? ?]//|[? ?] [? ?] /set_mem[? ?] /set_mem[? ?] [-> ->]//|].
by move=> [i j] [? ?]; exists (
j, i).
Qed.