From 1ee095fdc0eef12edce1ec7d84e104ba0f4980dd Mon Sep 17 00:00:00 2001
From: Reynald Affeldt <reynald.affeldt@aist.go.jp>
Date: Mon, 2 Dec 2024 14:46:38 +0900
Subject: [PATCH] prod notation for ereal and lemmas

---
 CHANGELOG_UNRELEASED.md    |  4 ++++
 reals/constructive_ereal.v | 35 +++++++++++++++++++++++++++++++++++
 2 files changed, 39 insertions(+)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index acacf8db1..4b55c10d0 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -10,6 +10,10 @@
 - in `normedtype.v`:
   + lemmas `continuous_within_itvcyP`, `continuous_within_itvNycP`
 
+- in `constructive_ereal.v`:
+  + notations `\prod` in scope ereal_scope
+  + lemmas `prode_ge0`, `prode_fin_num`
+
 ### Changed
   
 ### Renamed
diff --git a/reals/constructive_ereal.v b/reals/constructive_ereal.v
index a2155ef0e..3c9cc0940 100644
--- a/reals/constructive_ereal.v
+++ b/reals/constructive_ereal.v
@@ -46,6 +46,7 @@ From mathcomp Require Import mathcomp_extra signed.
 (*  (_ <= _)%E, (_ < _)%E, == comparison relations for extended reals         *)
 (*  (_ >= _)%E, (_ > _)%E                                                     *)
 (*   (\sum_(i in A) f i)%E == bigop-like notation in scope %E                 *)
+(*  (\prod_(i in A) f i)%E == bigop-like notation in scope %E                 *)
 (*      maxe x y, mine x y == notation for the maximum/minimum of two         *)
 (*                            extended real numbers                           *)
 (* ```                                                                        *)
@@ -551,6 +552,31 @@ Notation "\sum_ ( i 'in' A ) F" :=
 Notation "\sum_ ( i 'in' A ) F" :=
   (\big[+%E/0%E]_(i in A) F%E) : ereal_scope.
 
+Notation "\prod_ ( i <- r | P ) F" :=
+  (\big[*%E/1%:E]_(i <- r | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( i <- r ) F" :=
+  (\big[*%E/1%:E]_(i <- r) F%E) : ereal_scope.
+Notation "\prod_ ( m <= i < n | P ) F" :=
+  (\big[*%E/1%:E]_(m <= i < n | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( m <= i < n ) F" :=
+  (\big[*%E/1%:E]_(m <= i < n) F%E) : ereal_scope.
+Notation "\prod_ ( i | P ) F" :=
+  (\big[*%E/1%:E]_(i | P%B) F%E) : ereal_scope.
+Notation "\prod_ i F" :=
+  (\big[*%E/1%:E]_i F%E) : ereal_scope.
+Notation "\prod_ ( i : t | P ) F" :=
+  (\big[*%E/1%:E]_(i : t | P%B) F%E) (only parsing) : ereal_scope.
+Notation "\prod_ ( i : t ) F" :=
+  (\big[*%E/1%:E]_(i : t) F%E) (only parsing) : ereal_scope.
+Notation "\prod_ ( i < n | P ) F" :=
+  (\big[*%E/1%:E]_(i < n | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( i < n ) F" :=
+  (\big[*%E/1%:E]_(i < n) F%E) : ereal_scope.
+Notation "\prod_ ( i 'in' A | P ) F" :=
+  (\big[*%E/1%:E]_(i in A | P%B) F%E) : ereal_scope.
+Notation "\prod_ ( i 'in' A ) F" :=
+  (\big[*%E/1%:E]_(i in A) F%E) : ereal_scope.
+
 Section ERealOrderTheory.
 Context {R : numDomainType}.
 Implicit Types x y z : \bar R.
@@ -928,6 +954,11 @@ Lemma fin_numM x y : x \is a fin_num -> y \is a fin_num ->
   x * y \is a fin_num.
 Proof. by move: x y => [x| |] [y| |]. Qed.
 
+Lemma prode_fin_num (I : Type) (s : seq I) (P : pred I) (f : I -> \bar R) :
+  (forall i, P i -> f i \is a fin_num) ->
+  \prod_(i <- s | P i) f i \is a fin_num.
+Proof. by move=> ffin; elim/big_ind : _ => // x y x0 y0; rewrite fin_numM. Qed.
+
 Lemma fin_numX x n : x \is a fin_num -> x ^+ n \is a fin_num.
 Proof. by elim: n x => // n ih x finx; rewrite expeS fin_numM// ih. Qed.
 
@@ -1164,6 +1195,10 @@ move: x y => [x||] [y||]//=; rewrite /mule/= ?(lee_fin, eqe, lte_fin, lt0y)//.
   by rewrite gt_eqF // y0 le0y.
 Qed.
 
+Lemma prode_ge0 (I : Type) (s : seq I) (P : pred I) (f : I -> \bar R) :
+  (forall i, P i -> 0 <= f i) -> 0 <= \prod_(i <- s | P i) f i.
+Proof. by move=> f0; elim/big_ind : _ => // x y x0 y0; rewrite mule_ge0. Qed.
+
 Lemma mule_gt0 x y : 0 < x -> 0 < y -> 0 < x * y.
 Proof.
 by rewrite !lt_def => /andP[? ?] /andP[? ?]; rewrite mule_neq0 ?mule_ge0.