From 47aa95455b57ae4d5095ed4234f7b073ee717ffd Mon Sep 17 00:00:00 2001
From: IshiguroYoshihiro <jb.15r.1213@s.thers.ac.jp>
Date: Mon, 11 Dec 2023 16:08:58 +0900
Subject: [PATCH] add max_cvg_0_cvg_0

---
 CHANGELOG_UNRELEASED.md |  9 +++++
 theories/charge.v       | 78 ++++++++++++++++++++++++++++++++++++++++-
 2 files changed, 86 insertions(+), 1 deletion(-)

diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md
index 65779b3a4..f77f4dc42 100644
--- a/CHANGELOG_UNRELEASED.md
+++ b/CHANGELOG_UNRELEASED.md
@@ -98,6 +98,15 @@
   + lemma `Radon_Nikodym_cadd`
   + lemma `Radon_Nikodym_chain_rule`
 
+  + lemma `minr_cvg_0_cvg_0`
+  + lemma `mine_cvg_0_cvg_fin_num`
+  + lemma `mine_cvg_minr_cvg`
+  + lemma `mine_cvg_0_cvg_0`
+  + lemma `maxr_cvg_0_cvg_0`
+  + lemma `maxe_cvg_0_cvg_fin_num`
+  + lemma `maxe_cvg_maxr_cvg`
+  + lemma `maxe_cvg_0_cvg_0`
+
 ### Changed
 
 - in `charge.v`
diff --git a/theories/charge.v b/theories/charge.v
index f7403f3fc..29fc22448 100644
--- a/theories/charge.v
+++ b/theories/charge.v
@@ -583,7 +583,7 @@ Qed.
 
 End positive_negative_set_realFieldType.
 
-
+(* TODO: generalize *)
 Section min_cvg_0_cvg_0.
 Context (R : realFieldType).
 
@@ -651,6 +651,82 @@ Qed.
 
 End min_cvg_0_cvg_0.
 
+Section max_cvg_0_cvg_0.
+Context (R : realFieldType).
+
+Lemma maxr_cvg_0_cvg_0 (x : R^nat) (np : R) :
+ (np < 0)%R -> (forall k, x k <= 0)%R ->
+  (fun n => maxr (x n) np)%R --> (0:R)%R -> x --> (0:R)%R.
+Proof.
+move=> np0 x_le0.
+under eq_fun do rewrite -(opprK (x _)) -{1}(opprK np) -oppr_min.
+rewrite -oppr0.
+move/(@cvgNP _ [normedModType R of R^o]).
+move/minr_cvg_0_cvg_0.
+rewrite -oppr0 ltr_oppr in np0.
+move/(_ np0).
+have oppx_ge0 : (forall k : nat, (0 <= - x k)%R); first by move=> n; rewrite ler_oppr oppr0.
+move/(_ oppx_ge0).
+move/(@cvgNP _ [normedModType R of R^o]).
+by rewrite opprK.
+Qed.
+
+Lemma maxe_cvg_0_cvg_fin_num (x : (\bar R)^nat) (np : \bar R) :
+  (np < 0) -> (forall k, x k <= 0) ->
+  (fun n => maxe (x n) np) --> 0 ->
+  \forall n \near \oo, x n \is a fin_num.
+Proof.
+move=> np0 x_le0.
+under eq_fun do rewrite -(oppeK (x _)) -{1}(oppeK np) -oppe_min.
+rewrite -oppe0.
+move/cvgeNP.
+move/mine_cvg_0_cvg_fin_num.
+rewrite -oppe0 lte_oppr in np0.
+move/(_ np0).
+have oppx_ge0 : (forall k : nat, 0 <= - x k); first by move=> n; rewrite lee_oppr oppe0.
+move/(_ oppx_ge0).
+move=> [] n _ Hn.
+exists n => // k nk.
+rewrite -fin_numN.
+by apply: Hn.
+Qed.
+
+Lemma maxe_cvg_maxr_cvg (x : (\bar R)^nat) (np : R) :
+  (np < 0)%R -> (forall k, x k <= 0) ->
+  (fun n => maxe (x n) np%:E) --> 0 ->
+  (fun n => maxr ((fine \o x) n) np) --> (0:R)%R.
+Proof.
+move=> np0 x_le0.
+under eq_fun do rewrite -(oppeK (x _)) -{1}(oppeK np%:E) -oppe_min.
+rewrite -oppr0 EFinN.
+move/cvgeNP.
+move/mine_cvg_minr_cvg.
+rewrite -oppr0 ltr_oppr in np0.
+move/(_ np0).
+have oppx_ge0 : (forall k : nat, 0 <= - x k); first by move=> n; rewrite lee_oppr oppe0.
+move/(_ oppx_ge0).
+move/(@cvgNP _ [normedModType R of R^o]).
+by under eq_cvg do rewrite /GRing.opp /= oppr_min fineN !opprK.
+Qed.
+
+Lemma maxe_cvg_0_cvg_0 (x : (\bar R)^nat) (np : \bar R) :
+  (np < 0) -> (forall k, x k <= 0) ->
+  (fun n => maxe (x n) np) --> 0 -> x --> 0.
+Proof.
+move=> np0 x_le0.
+under eq_fun do rewrite -(oppeK (x _)) -{1}(oppeK np) -oppe_min.
+rewrite -oppe0.
+move/cvgeNP.
+move/mine_cvg_0_cvg_0.
+rewrite -oppe0 lte_oppr in np0.
+move/(_ np0).
+have oppx_ge0 : (forall k : nat, 0 <= - x k); first by move=> n; rewrite lee_oppr oppe0.
+move/(_ oppx_ge0) /cvgeNP.
+by under eq_cvg do rewrite oppeK.
+Qed.
+
+End max_cvg_0_cvg_0.
+
 Section hahn_decomposition_lemma.
 Context d (T : measurableType d) (R : realType).
 Variables (nu : {charge set T -> \bar R}) (D : set T).