Skip to content

Prove some admitted lemmas in experimental_reals #2007

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Open
ethanlee515 wants to merge 1 commit into
base: master
Choose a base branch
from
+161 −112
Open

Prove some admitted lemmas in experimental_reals #2007

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
8 changes: 8 additions & 0 deletions CHANGELOG_UNRELEASED.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -208,6 +208,14 @@
- in `realsum.v`:
+ lemma `__admitted__psumB` proved and renamed to `psumB`

- in `realsum.v`:
+ lemmas `interchange_sup`, `interchange_psum` are no longer
deprecated
- in `distr.v`:
+ lemmas `dlet_dlet`, `dmargin_dlet`, `dlet_dmargin`, `dfst_dswap`,
`dsnd_dswap`, `dsndE`, `pr_dlet` are no longer deprecated


### Changed

- moved from `measurable_structure.v` to `classical_sets.v`:
Expand Down
68 changes: 32 additions & 36 deletions experimental_reals/distr.v
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -505,15 +505,15 @@ End BindTheory.
Section DLetDLet.
Context {T U V : choiceType} (f1 : T -> distr U) (f2 : U -> distr V).

Lemma __deprecated__dlet_dlet (mu : {distr T / R}) :
Lemma dlet_dlet (mu : {distr T / R}) :
\dlet_(x <- \dlet_(y <- mu) f1 y) f2 x
=1 \dlet_(y <- mu) (\dlet_(x <- f1 y) f2 x).
Proof.
move=> z; unlock dlet => /=; rewrite /mlet /=.
pose S y x := mu x * (f1 x y * f2 y z).
rewrite (eq_psum (F2 := fun y => PosSum.psum (S^~ y))) => [x|].
by rewrite -psumZ //; apply/eq_psum => y /=.
rewrite __admitted__interchange_psum.
rewrite interchange_psum.
+ by move=> x; apply/summableZ/summable_mlet.
+ rewrite {}/S; apply/(le_summable (F2 := mu)) => //.
move=> x; rewrite ge0_psum /= psumZ ?ler_piMr //.
Expand All @@ -522,8 +522,12 @@ rewrite __admitted__interchange_psum.
apply/eq_psum=> y /=; rewrite -psumZr //.
by apply/eq_psum=> x /=; rewrite {}/S mulrA.
Qed.

End DLetDLet.

#[deprecated(since="1.17.0", note="use `dlet_dlet` instead")]
Notation __deprecated__dlet_dlet := dlet_dlet (only parsing).

(* -------------------------------------------------------------------- *)
Section DLetAlg.
Context {T U : choiceType} (mu mu1 mu2 : {distr T / R}).
Expand Down Expand Up @@ -719,32 +723,27 @@ rewrite dmarginE dletE; apply/eq_psum => x //=.
by rewrite mulrC dunit1E.
Qed.

Lemma __deprecated__dlet_dmargin (mu : {distr T / R}) (f : T -> U) (g : U -> {distr V / R}):
Lemma dlet_dmargin (mu : {distr T / R}) (f : T -> U) (g : U -> {distr V / R}):
\dlet_(u <- dmargin f mu) g u =1 \dlet_(t <- mu) (g (f t)).
Proof.
move=> x; rewrite __deprecated__dlet_dlet; apply: eq_in_dlet=> //.
move=> x; rewrite dlet_dlet; apply: eq_in_dlet=> //.
by move=> y _ z; rewrite dlet_unit.
Qed.

Lemma __deprecated__dmargin_dlet (mu : {distr T / R}) (f : U -> V) (g : T -> {distr U / R}):
Lemma dmargin_dlet (mu : {distr T / R}) (f : U -> V) (g : T -> {distr U / R}):
dmargin f (\dlet_(t <- mu) g t) =1 \dlet_(t <- mu) (dmargin f (g t)).
Proof. by apply/__deprecated__dlet_dlet. Qed.
Proof. by apply/dlet_dlet. Qed.

Lemma dmargin_dunit (t : T) (f : T -> U):
dmargin f (dunit t) =1 dunit (f t) :> {distr U / R}.
Proof. by apply/dlet_unit. Qed.
End MarginalsTh.
End Std.

#[deprecated(since="mathcomp-analysis 0.6.2",
note="relies on admitted, use __deprecated__dlet_dlet explicitly if you really want to use this lemma")]
Notation dlet_dlet := __deprecated__dlet_dlet.
#[deprecated(since="mathcomp-analysis 0.6.2",
note="relies on admitted, use __deprecated__dmargin_dlet explicitly if you really want to use this lemma")]
Notation dmargin_dlet := __deprecated__dmargin_dlet.
#[deprecated(since="mathcomp-analysis 0.6.2",
note="relies on admitted, use __deprecated__dlet_dmargin explicitly if you really want to use this lemma")]
Notation dlet_dmargin := __deprecated__dlet_dmargin.
#[deprecated(since="1.17.0", note="use `dmargin_dlet` instead")]
Notation __deprecated__dmargin_dlet := dmargin_dlet (only parsing).
#[deprecated(since="1.17.0", note="use `dlet_dmargin` instead")]
Notation __deprecated__dlet_dmargin := dlet_dmargin (only parsing).

Notation dfst mu := (dmargin fst mu).
Notation dsnd mu := (dmargin snd mu).
Expand Down Expand Up @@ -787,25 +786,23 @@ Proof.
by move=> h; apply/dinsuppP; rewrite dswapE; apply/dinsuppPn.
Qed.

Lemma __deprecated__dfst_dswap : dfst (dswap mu) =1 dsnd mu.
Lemma dfst_dswap : dfst (dswap mu) =1 dsnd mu.
Proof.
move=> z; rewrite __deprecated__dlet_dlet; apply/eq_in_dlet => // -[x y].
move=> z; rewrite dlet_dlet; apply/eq_in_dlet => // -[x y].
by move=> _ t /=; rewrite dlet_unit /=.
Qed.

Lemma __deprecated__dsnd_dswap : dsnd (dswap mu) =1 dfst mu.
Lemma dsnd_dswap : dsnd (dswap mu) =1 dfst mu.
Proof.
move=> z; rewrite __deprecated__dlet_dlet; apply/eq_in_dlet => // -[x y].
move=> z; rewrite dlet_dlet; apply/eq_in_dlet => // -[x y].
by move=> _ t /=; rewrite dlet_unit /=.
Qed.
End DSwapTheory.

#[deprecated(since="mathcomp-analysis 0.6.2",
note="relies on admitted, use __deprecated__dfst_dswap explicitly if you really want to use this lemma")]
Notation dfst_dswap := __deprecated__dfst_dswap.
#[deprecated(since="mathcomp-analysis 0.6.2",
note="relies on admitted, use __deprecated__dsnd_dswap explicitly if you really want to use this lemma")]
Notation dsnd_dswap := __deprecated__dsnd_dswap.
#[deprecated(since="1.17.0", note="use `dfst_dswap` instead")]
Notation __deprecated__dfst_dswap := dfst_dswap (only parsing).
#[deprecated(since="1.17.0", note="use `dsnd_dswap` instead")]
Notation __deprecated__dsnd_dswap := dsnd_dswap (only parsing).

(* -------------------------------------------------------------------- *)
Section DFst.
Expand Down Expand Up @@ -836,9 +833,9 @@ End DFst.
Section DSnd.
Context {R : realType} {T U : choiceType}.

Lemma __deprecated__dsndE (mu : {distr (T * U) / R}) y :
Lemma dsndE (mu : {distr (T * U) / R}) y :
dsnd mu y = PosSum.psum (fun x => mu (x, y)).
Proof. by rewrite -__deprecated__dfst_dswap dfstE; apply/eq_psum=> x; rewrite dswapE. Qed.
Proof. by rewrite -dfst_dswap dfstE; apply/eq_psum=> x; rewrite dswapE. Qed.

Lemma summable_snd (mu : {distr (T * U) / R}) y :
summable (fun x => mu (x, y)).
Expand All @@ -848,9 +845,8 @@ by move=> x /=; rewrite dswapE.
Qed.
End DSnd.

#[deprecated(since="mathcomp-analysis 0.6.2",
note="relies on admitted, use __deprecated__dsndE explicitly if you really want to use this lemma")]
Notation dsndE := __deprecated__dsndE.
#[deprecated(since="1.17.0", note="use `dsndE` instead")]
Notation __deprecated__dsndE := dsndE (only parsing).

(* -------------------------------------------------------------------- *)
Section PrCoreTheory.
Expand Down Expand Up @@ -957,15 +953,15 @@ Context {R : realType} {T U : choiceType} {I : eqType}.

Implicit Types (mu : {distr T / R}) (A B E : pred T).

Lemma __deprecated__pr_dlet E f (mu : {distr U / R}) :
Lemma pr_dlet E f (mu : {distr U / R}) :
\P_[dlet f mu] E = \E_[mu] (fun x => \P_[f x] E).
Proof.
rewrite /esp -psum_sum => [x|]; first by rewrite mulr_ge0 ?ge0_pr.
rewrite /pr; unlock dlet => /=; rewrite /mlet /=.
pose F x y := (E x)%:R * (mu y * f y x).
transitivity (PosSum.psum (fun x => PosSum.psum (fun y => F x y))); rewrite {}/F.
by apply/eq_psum => x; rewrite -psumZ ?ler0n.
rewrite __admitted__interchange_psum /=; last first.
rewrite interchange_psum /=; last first.
apply/eq_psum=> y /=; rewrite mulrC -psumZ //.
by apply/eq_psum=> x /=; rewrite mulrCA.
+ have := summable_pr E (dlet f mu); apply/eq_summable.
Expand All @@ -976,7 +972,7 @@ Qed.
Lemma pr_dmargin E f (mu : {distr U / R}) :
\P_[dmargin f mu] E = \P_[mu] [pred x | f x \in E].
Proof.
by rewrite /dmargin __deprecated__pr_dlet pr_exp; apply/eq_exp=> x _; rewrite pr_dunit.
by rewrite /dmargin pr_dlet pr_exp; apply/eq_exp=> x _; rewrite pr_dunit.
Qed.

Lemma eq0_pr A mu :
Expand Down Expand Up @@ -1208,9 +1204,9 @@ Lemma __admitted__exp_dlet mu (nu : T -> {distr U / R}) F :
Proof using Type*. Admitted.
End PrTheory.

#[deprecated(since="mathcomp-analysis 0.6.2",
note="relies on admitted, use __deprecated__pr_dlet explicitly if you really want to use this lemma")]
Notation pr_dlet := __deprecated__pr_dlet.
#[deprecated(since="1.17.0", note="use `pr_dlet` instead")]
Notation __deprecated__pr_dlet := pr_dlet (only parsing).

#[deprecated(since="mathcomp-analysis 0.6.2",
note="lacks proof, use __admitted__exp_split explicitly if you really want to use this lemma")]
Notation exp_split := __admitted__exp_split.
Expand Down
Loading
Loading