sup of contract is contract of sup

theories/normedtype.v

@@ -1079,7 +1079,6 @@ Definition le_contractRL := monoRL_in
 Definition lt_contractRL := monoRL_in
   (onW_can_in predT expandK) (fun x _ => isT) (in2W lt_contract).
 
-
 Lemma contract_eq0 x : (contract x == 0) = (x == 0%:E).
 Proof. by rewrite -(can_eq contractK) contract0. Qed.
 
@@ -1101,6 +1100,47 @@ apply/eqP/eqP => [|->]; last by rewrite expandN1.
 by rewrite /expand; do![case: (altP eqP) => ?].
 Qed.
 
+Lemma sup_contract_le1 S : S !=set0 -> `|sup (contract @` S)| <= 1.
+Proof.
+case=> x Sx; rewrite ler_norml; apply/andP; split; last first.
+  apply sup_le_ub; first by exists (contract x), x.
+  by move=> r [y Sy] <-; case/ler_normlP : (contract_le1 y).
+rewrite (@le_trans _ _ (contract x)) //.
+  by case/ler_normlP : (contract_le1 x); rewrite ler_oppl.
+apply sup_ub; last by exists x.
+by exists 1 => r [y Sy <-]; case/ler_normlP : (contract_le1 y).
+Qed.
+
+Lemma contract_sup S : S !=set0 -> contract (ereal_sup S) = sup (contract @` S).
+Proof.
+move=> S0; apply/eqP; rewrite eq_le; apply/andP; split; last first.
+  apply sup_le_ub.
+    by case: S0 => x Sx; exists (contract x), x.
+  move=> x [y Sy] <-{x}; rewrite le_contract; exact/ereal_sup_ub.
+rewrite leNgt; apply/negP.
+set supc := sup _; set csup := contract _; move=> ltsup.
+suff [y [ysupS ?]] : exists y, (y < ereal_sup S)%E /\ ub S y.
+  have : (ereal_sup S <= y)%E by apply ub_ereal_sup.
+  by move/(lt_le_trans ysupS); rewrite ltxx.
+suff [x [? [ubSx x1]]] : exists x, x < csup /\ ub (contract @` S) x /\ `|x| <= 1.
+  exists (expand x); split => [|y Sy].
+    by rewrite -(contractK (ereal_sup S)) lt_expand // inE // contract_le1.
+  rewrite -(contractK y) le_expand // ?inE ?contract_le1 //.
+  by apply ubSx; exists y.
+exists ((supc + csup) / 2); split; first by rewrite midf_lt.
+split => [r [y Sy <-{r}]|].
+  rewrite (@le_trans _ _ supc) ?midf_le //; last by rewrite ltW.
+  apply sup_ub; last by exists y.
+  by exists 1 => r [z Sz <-]; case/ler_normlP : (contract_le1 z).
+rewrite ler_norml; apply/andP; split; last first.
+  rewrite ler_pdivr_mulr // mul1r (_ : 2 = 1 + 1) // ler_add //.
+  by case/ler_normlP : (sup_contract_le1 S0).
+  by case/ler_normlP : (contract_le1 (ereal_sup S)).
+rewrite ler_pdivl_mulr // (_ : 2 = 1 + 1) // mulN1r opprD ler_add //.
+by case/ler_normlP : (sup_contract_le1 S0); rewrite ler_oppl.
+by case/ler_normlP : (contract_le1 (ereal_sup S)); rewrite ler_oppl.
+Qed.
+
 End contract_expand.
 
 Section ereal_PseudoMetric.