Module mathcomp.experimental_reals.xfinmap

From mathcomp Require Import boot order algebra.
From mathcomp Require Export finmap.

Unset SsrOldRewriteGoalsOrder.  
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Set Asymmetric Patterns.

Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope ring_scope.
Local Open Scope fset_scope.

Lemma

uniq_fset_keysUsed by

• mathcomp.experimental_reals.realsum

---

Source code

{

KSource code

: choiceType} (

JSource code

: {fset K}) : uniq (enum_fset J).

Proof.

by case: J => J /= /canonical_uniq. Qed.

#[global] Hint Resolve uniq_fset_keys : core.

Lemma

enum_fset0Source code

 (

TSource code

: choiceType) :
  enum (fset0 : finType) = [::] :> seq (@fset0 T).

Proof.

by rewrite enumT unlock. Qed.

Lemma

enum_fset1Source code

 (

TSource code

: choiceType) (

xSource code

: T) :
  enum ([fset x] : finType) = [:: [`fset11 x]].

Proof.

apply/perm_small_eq=> //; apply/uniq_perm => //.
  by apply/enum_uniq.
case=> [y hy]; rewrite mem_seq1 mem_enum /in_mem /=.
by rewrite eqE /=; rewrite in_fset1 in hy.
Qed.

Section BigFSet.
Variable (

RSource code

: Type) (

idxSource code

: R) (

opSource code

: Monoid.law idx).
Variable (

ISource code

: choiceType).

Lemma

big_fset0_condSource code

 (

PSource code

: pred _) (

FSource code

: _ -> R) :
  \big[op/idx]_(

iSource code

: @fset0 I | P i) F i = idx :> R.

Proof.

by apply: big_pred0 => -[j hj]; have := hj; rewrite in_fset0. Qed.

Lemma

big_fset0Used by

• mathcomp.experimental_reals.distr
• mathcomp.experimental_reals.realsum

---

Source code

 (

FSource code

: @fset0 I -> R) :
  \big[op/idx]_(

iSource code

: fset0) F i = idx.

Proof.

by rewrite /index_enum -enumT /= enum_fset0 big_nil. Qed.

Lemma

big_fset1Source code

 (

aSource code

: I) (

FSource code

: [fset a] -> R) :
  \big[op/idx]_(

iSource code

: [fset a]) F i = F (FSetSub (fset11 a)).

Proof.

by rewrite /index_enum -enumT enum_fset1 big_seq1. Qed.

End BigFSet.

Section BigFSetCom.
Variable (

RSource code

: Type) (

idxSource code

: R).

Local Notation 

"1"Source code

:= idx.

Variable

opSource code

: Monoid.com_law 1.

Local Notation 

"'*%M'"Source code

:= op (at level 0).
Local Notation 

"x * y"Source code

:= (op x y).

Lemma

big_fset_seq_condSource code

 (

TSource code

: choiceType) (

JSource code

: {fset T})

PSource code

FSource code

:
    \big[*%M/1]_(

xSource code

: J | P (val x)) F (val x)
  = \big[*%M/1]_(

xSource code

<- enum_fset J | P x) F x.

Proof.

case: J=> J c; rewrite -(big_map val) /index_enum.
by rewrite !unlock val_fset_sub_enum ?canonical_uniq.
Qed.

Lemma

big_fset_seqUsed by

• mathcomp.experimental_reals.distr
• mathcomp.experimental_reals.realsum

---

Source code

 (

TSource code

: choiceType) (

JSource code

: {fset T})

FSource code

:
    \big[*%M/1]_(

xSource code

: J) F (val x)
  = \big[*%M/1]_(

xSource code

<- enum_fset J) F x.

Proof.

by apply/big_fset_seq_cond. Qed.

Lemma

big_seq_fset_condSource code

 (

TSource code

: choiceType) (

sSource code

: seq T)

PSource code

FSource code

: uniq s ->
    \big[*%M/1]_(

xSource code

: [fset

xSource code

in s] | P (val x)) F (val x)
  = \big[*%M/1]_(

xSource code

<- s | P x) F x.

Proof.

move=> eq_s; rewrite big_fset_seq_cond; apply/perm_big.
by apply/uniq_perm=> //= x; rewrite in_fset.
Qed.

Lemma

big_seq_fsetUsed by

• mathcomp.experimental_reals.realsum

---

Source code

 (

TSource code

: choiceType) (

sSource code

: seq T)

FSource code

: uniq s ->
    \big[*%M/1]_(

xSource code

: [fset

xSource code

in s]) F (val x)
  = \big[*%M/1]_(

xSource code

<- s) F x.

Proof.

by apply/big_seq_fset_cond. Qed.

End BigFSetCom.

Arguments big_fset_seq_cond [R idx op T J] P F.
Arguments big_fset_seq [R idx op T J] F.
Arguments big_seq_fset_cond [R idx op T s] P F _.
Arguments big_seq_fset [R idx op T s] F _.

Section BigFSetU.
Context {

RSource code

: Type} {

TSource code

: choiceType} (

idxSource code

: R) (

opSource code

: Monoid.com_law idx).

Lemma

big_fsetUSource code

 (

ASource code

BSource code

: {fset T})

FSource code

: [disjoint A & B] ->
  \big[op/idx]_(

jSource code

: A `|` B) F (val j) =
    op (\big[op/idx]_(

jSource code

: A) F (val j))
       (\big[op/idx]_(

jSource code

: B) F (val j)).

Proof.

move=> dj_AB; rewrite !big_fset_seq -big_cat; apply/perm_big.
apply/uniq_perm=> //.
+ rewrite cat_uniq ?uniq_fset_keys !(andbT, andTb); apply/hasPn => x /=.
  by apply/fdisjointP; rewrite fdisjoint_sym.
+ by move=> x; rewrite mem_cat in_fsetE.
Qed.

End BigFSetU.

Section BigFSetOrder.
Variable (

RSource code

: realDomainType) (

TSource code

: choiceType).

Lemma

big_fset_subsetUsed by

• mathcomp.experimental_reals.realsum

---

Source code

 (

ISource code

JSource code

: {fset T}) (

FSource code

: T -> R) :
  (forall

xSource code

, 0 <= F x) -> {subset I <= J} ->
    \sum_(

iSource code

: I) F (val i) <= \sum_(

jSource code

: J) F (val j).

Proof.

move=> ge0_F le_IJ; rewrite !big_fset_seq /=.
rewrite [X in _<=X](bigID [pred

jSource code

: T | j \in I]) /=.
rewrite ler_wpDr ?sumr_ge0 // -[X in _<=X]big_filter.
rewrite le_eqVlt; apply/orP; left; apply/eqP/perm_big.
apply/uniq_perm; rewrite ?filter_uniq //; last move=> i.
rewrite mem_filter; case/boolP: (_ \in _) => //=.
by move/le_IJ => ->.
Qed.

Lemma

big_nat_mkfsetSource code

 (

FSource code

: nat -> R)

nSource code

:
  \sum_(0 <=

iSource code

< n) F i =
    \sum_(

iSource code

: [fset

xSource code

in (iota 0 n)]) F (val i).

Proof.

rewrite -(big_map val xpredT) /=; apply/perm_big.
apply/uniq_perm; rewrite ?iota_uniq //.
  rewrite map_inj_uniq /=; first apply/val_inj.
  by rewrite /index_enum -enumT enum_uniq.
by move=> i; rewrite /index_enum -enumT -enum_fsetE in_fset /index_iota subn0.
Qed.

Lemma

big_ord_mkfsetUsed by

• mathcomp.experimental_reals.realsum

---

Source code

 (

FSource code

: nat -> R)

nSource code

:
  \sum_(

iSource code

< n) F i =
    \sum_(

iSource code

: [fset

xSource code

in (iota 0 n)]) F (val i).

Proof.

by rewrite -(big_mkord xpredT) big_nat_mkfset. Qed.

End BigFSetOrder.

Lemma

enum_fsetTUsed by

• mathcomp.experimental_reals.realsum

---

Source code

{

ISource code

: finType} :
  perm_eq (enum [fset i |

iSource code

in I]) (enum I).

Proof.

apply/uniq_perm; rewrite ?enum_uniq //.
by move=> i /=; rewrite !mem_enum in_imfset.
Qed.