From 7608ef027fc4276c63e05b95af211761652eb0c1 Mon Sep 17 00:00:00 2001
From: affeldt-aist <33154536+affeldt-aist@users.noreply.github.com>
Date: Fri, 21 Apr 2023 22:03:04 +0900
Subject: [PATCH] clarify status of lemmas in altreals (#833)

---
 CHANGELOG_UNRELEASED.md     |  7 ++++
 theories/altreals/distr.v   | 76 +++++++++++++++++++++++++++----------
 theories/altreals/realsum.v | 18 +++++++--
 3 files changed, 79 insertions(+), 22 deletions(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 46e67a0e4..6f1bdbb83 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -264,6 +264,13 @@
     (use `emeasurable_itv` instead)
 - in `measure.v`:
   + lemma `measurable_fun_ext`
+- in `realsum.v`:
+  + `psumB`, `interchange_sup`, `interchange_psum`
+- in `distr.v`:
+  + `dlet_lim`, `dlim_let`, `exp_split`, `exp_dlet`,
+    `dlet_dlet`, `dmargin_dlet`, `dlet_dmargin`,
+    `dfst_dswap`, `dsnd_dswap`, `dsndE`, `pr_dlet`,
+    `exp_split`, `exp_dlet`
 
 ### Removed
 
diff --git a/theories/altreals/distr.v b/theories/altreals/distr.v
index ab093e019..e7744c7dc 100644
--- a/theories/altreals/distr.v
+++ b/theories/altreals/distr.v
@@ -504,7 +504,7 @@ End BindTheory.
 Section DLetDLet.
 Context {T U V : choiceType} (f1 : T -> distr U) (f2 : U -> distr V).
 
-Lemma dlet_dlet (mu : {distr T / R}) :
+Lemma __deprecated__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.
@@ -512,7 +512,7 @@ move=> z; unlock dlet => /=; rewrite /mlet /=.
 pose S y x := mu x * (f1 x y * f2 y z).
 rewrite (eq_psum (F2 := fun y => psum (S^~ y))) => [x|].
   by rewrite -psumZ //; apply/eq_psum => y /=.
-rewrite interchange_psum.
+rewrite __admitted__interchange_psum.
 + by move=> x; apply/summableZ/summable_mlet.
 + rewrite {}/S; apply/(le_summable (F2 := mu)) => //.
   move=> x; rewrite ge0_psum /= psumZ ?ler_pimulr //.
@@ -680,17 +680,24 @@ move/dcvg_homo: mn_f => /dcvgP /(_ x) [l _].
 by move=> cv; rewrite (nlimE cv).
 Qed.
 
-Lemma dlet_lim f h : (forall n m, (n <= m)%N -> f n <=1 f m) ->
+Lemma __admitted__dlet_lim f h : (forall n m, (n <= m)%N -> f n <=1 f m) ->
   \dlet_(x <- dlim f) h x =1 \dlim_(n) \dlet_(x <- f n) h x.
 Proof. Admitted.
 
-Lemma dlim_let (f : nat -> T -> {distr U / R}) (mu : {distr T / R}) :
+Lemma __admitted__dlim_let (f : nat -> T -> {distr U / R}) (mu : {distr T / R}) :
   (forall x n m, (n <= m)%N -> f n x <=1 f m x) ->
   \dlim_(n) \dlet_(x <- mu) (f n x) =1
     \dlet_(x <- mu) \dlim_(n) (f n x).
 Proof using Type. Admitted.
 End DLimTheory.
 
+#[deprecated(since="mathcomp-analysis 0.6.2",
+  note="lacks proof, use __admitted__dlet_lim explicitly if you really want to use this lemma")]
+Notation dlet_lim := __admitted__dlet_lim.
+#[deprecated(since="mathcomp-analysis 0.6.2",
+  note="lacks proof, use __admitted__dlim_let explicitly if you really want to use this lemma")]
+Notation dlim_let := __admitted__dlim_let.
+
 (* -------------------------------------------------------------------- *)
 Section Marginals.
 Variable (T U : choiceType) (h : T -> U) (mu : distr T).
@@ -712,16 +719,16 @@ rewrite dmarginE dletE; apply/eq_psum => x //=.
 by rewrite mulrC dunit1E.
 Qed.
 
-Lemma dlet_dmargin (mu : {distr T / R}) (f : T -> U) (g : U -> {distr V / R}):
+Lemma __deprecated__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 dlet_dlet; apply: eq_in_dlet=> //.
+move=> x; rewrite __deprecated__dlet_dlet; apply: eq_in_dlet=> //.
 by move=> y _ z; rewrite dlet_unit.
 Qed.
 
-Lemma dmargin_dlet (mu : {distr T / R}) (f : U -> V) (g : T -> {distr U / R}):
+Lemma __deprecated__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/dlet_dlet. Qed.
+Proof. by apply/__deprecated__dlet_dlet. Qed.
 
 Lemma dmargin_dunit (t : T) (f : T -> U):
   dmargin f (dunit t) =1 dunit (f t) :> {distr U / R}.
@@ -729,6 +736,16 @@ 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.
+
 Notation dfst mu := (dmargin fst mu).
 Notation dsnd mu := (dmargin snd mu).
 
@@ -770,19 +787,26 @@ Proof.
 by move=> h; apply/dinsuppP; rewrite dswapE; apply/dinsuppPn.
 Qed.
 
-Lemma dfst_dswap : dfst (dswap mu) =1 dsnd mu.
+Lemma __deprecated__dfst_dswap : dfst (dswap mu) =1 dsnd mu.
 Proof.
-move=> z; rewrite dlet_dlet; apply/eq_in_dlet => // -[x y].
+move=> z; rewrite __deprecated__dlet_dlet; apply/eq_in_dlet => // -[x y].
 by move=> _ t /=; rewrite dlet_unit /=.
 Qed.
 
-Lemma dsnd_dswap : dsnd (dswap mu) =1 dfst mu.
+Lemma __deprecated__dsnd_dswap : dsnd (dswap mu) =1 dfst mu.
 Proof.
-move=> z; rewrite dlet_dlet; apply/eq_in_dlet => // -[x y].
+move=> z; rewrite __deprecated__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.
+
 (* -------------------------------------------------------------------- *)
 Section DFst.
 Context {R : realType} {T U : choiceType}.
@@ -812,9 +836,9 @@ End DFst.
 Section DSnd.
 Context {R : realType} {T U : choiceType}.
 
-Lemma dsndE (mu : {distr (T * U) / R}) y :
+Lemma __deprecated__dsndE (mu : {distr (T * U) / R}) y :
   dsnd mu y = psum (fun x => mu (x, y)).
-Proof. by rewrite -dfst_dswap dfstE; apply/eq_psum=> x; rewrite dswapE. Qed.
+Proof. by rewrite -__deprecated__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)).
@@ -824,6 +848,10 @@ 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.
+
 (* -------------------------------------------------------------------- *)
 Section PrCoreTheory.
 Context {R : realType} {T : choiceType}.
@@ -929,7 +957,7 @@ Context {R : realType} {T U : choiceType} {I : eqType}.
 
 Implicit Types (mu : {distr T / R}) (A B E : pred T).
 
-Lemma pr_dlet E f (mu : {distr U / R}) :
+Lemma __deprecated__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.
@@ -937,7 +965,7 @@ rewrite /pr; unlock dlet => /=; rewrite /mlet /=.
 pose F x y := (E x)%:R * (mu y * f y x).
 transitivity (psum (fun x => psum (fun y => F x y))); rewrite {}/F.
   by apply/eq_psum => x; rewrite -psumZ ?ler0n.
-rewrite interchange_psum /=; last first.
+rewrite __admitted__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.
@@ -948,7 +976,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 pr_dlet pr_exp; apply/eq_exp=> x _; rewrite pr_dunit.
+by rewrite /dmargin __deprecated__pr_dlet pr_exp; apply/eq_exp=> x _; rewrite pr_dunit.
 Qed.
 
 Lemma eq0_pr A mu :
@@ -1134,7 +1162,7 @@ move=> x mux; move/pr_eq0: zPB' => /(_ x) h; rewrite !inE.
 by apply/negP=> /andP[_ /h] /dinsuppP.
 Qed.
 
-Lemma exp_split A f mu : \E?_[mu] f -> \E_[mu] f =
+Lemma __admitted__exp_split A f mu : \E?_[mu] f -> \E_[mu] f =
     \P_[mu]        A  * \E_[mu,       A] f
   + \P_[mu] (predC A) * \E_[mu, predC A] f.
 Proof using Type. Admitted.
@@ -1174,12 +1202,22 @@ move=> ge0M bd; apply/(@le_trans _ _ (\E_[mu] (fun _ => M))).
 by rewrite exp_cst ler_pimull // le1_pr.
 Qed.
 
-Lemma exp_dlet mu (nu : T -> {distr U / R}) F :
+Lemma __admitted__exp_dlet mu (nu : T -> {distr U / R}) F :
   (forall eta, \E?_[eta] F) ->
     \E_[dlet nu mu] F = \E_[mu] (fun x => \E_[nu x] 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="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.
+#[deprecated(since="mathcomp-analysis 0.6.2",
+  note="lacks proof, use __admitted__exp_dlet explicitly is you really want to use this lemma")]
+Notation exp_dlet := __admitted__exp_dlet.
+
 (* -------------------------------------------------------------------- *)
 Section Jensen.
 Context {R : realType} {I : finType}.
diff --git a/theories/altreals/realsum.v b/theories/altreals/realsum.v
index 43ec07ada..7b9989a0e 100644
--- a/theories/altreals/realsum.v
+++ b/theories/altreals/realsum.v
@@ -821,7 +821,7 @@ rewrite /D big_split /=; apply/ler_add; apply/big_fset_subset=> //.
 Qed.
 
 (* -------------------------------------------------------------------- *)
-Lemma psumB S1 S2 :
+Lemma __admitted__psumB S1 S2 :
     (forall x, 0 <= S2 x <= S1 x) -> summable S1
   -> psum (S1 \- S2) = (psum S1 - psum S2).
 Proof using Type. Admitted.
@@ -909,6 +909,10 @@ by rewrite eq_le le_psum /=; apply/gerfinseq_psum.
 Qed.
 End StdSum.
 
+#[deprecated(since="mathcomp-analysis 0.6.2",
+  note="lacks proof, use __admitted__psumB explicitly if you really want to")]
+Notation psumB := __admitted__psumB.
+
 (* -------------------------------------------------------------------- *)
 Section PSumReindex.
 Context {R : realType} {T U : choiceType}.
@@ -1098,7 +1102,7 @@ End PSumPair.
 Section SupInterchange.
 Context {R : realType} {T U : Type}.
 
-Lemma interchange_sup (S : T -> U -> R) :
+Lemma __admitted__interchange_sup (S : T -> U -> R) :
     (forall x, has_sup [set r | exists y, r = S x y])
   -> has_sup [set r | exists x, r = sup [set r | exists y, r = S x y]]
   -> sup [set r | exists x, r = sup [set r | exists y, r = S x y]]
@@ -1106,17 +1110,25 @@ Lemma interchange_sup (S : T -> U -> R) :
 Proof using Type. Admitted.
 End SupInterchange.
 
+#[deprecated(since="mathcomp-analysis 0.6.2",
+  note="lacks proof, use __admitted__interchange_sup explicitly if you really want to use this lemma")]
+Notation interchange_sup := __admitted__interchange_sup.
+
 (* -------------------------------------------------------------------- *)
 Section PSumInterchange.
 Context {R : realType} {T U : choiceType}.
 
-Lemma interchange_psum (S : T -> U -> R) :
+Lemma __admitted__interchange_psum (S : T -> U -> R) :
     (forall x, summable (S x))
   -> summable (fun x => psum (fun y => S x y))
   -> psum (fun x => psum (fun y => S x y)) = psum (fun y => psum (fun x => S x y)).
 Proof using Type. Admitted.
 End PSumInterchange.
 
+#[deprecated(since="mathcomp-analysis 0.6.2",
+  note="lacks proof, use __admitted__interchange_psum explicitly if you really want to use this lemma")]
+Notation interchange_psum := __admitted__interchange_psum.
+
 (* -------------------------------------------------------------------- *)
 Section SumTheory.
 Context {R : realType} {T : choiceType}.