lemmas about ereal

- case analysis for x * y = oo
- about abse and fin_num

CHANGELOG_UNRELEASED.md

@@ -7,6 +7,9 @@
 - in `topology.v`:
   + definitions `kolmogorov_space`, `accessible_space`
   + lemmas `accessible_closed_set1`, `accessible_kolmogorov`
+- in `ereal.v`:
+  + lemmas `mule_eqpinfty`, `mule_eqninfty`
+  + lemmas `fine_eq0`, `abse_eq0`
 
 ### Changed
 

theories/ereal.v

@@ -495,6 +495,9 @@ Section ERealArithTh_numDomainType.
 Context {R : numDomainType}.
 Implicit Types (x y z : \bar R) (r : R).
 
+Lemma fine_eq0 x : x \is a fin_num -> (fine x == 0%R) = (x == 0).
+Proof. by move: x => [//| |] /=; rewrite fin_numE. Qed.
+
 Lemma EFinN r : (- r)%:E = (- r%:E). Proof. by []. Qed.
 
 Lemma fineN x : fine (- x) = (- fine x)%R.
@@ -583,6 +586,9 @@ Proof. by move: x => [r| |] //=; rewrite /mule/= ?mulr0// eqxx. Qed.
 Lemma mul0e x : 0 * x = 0.
 Proof. by move: x => [r| |]/=; rewrite /mule/= ?mul0r// eqxx. Qed.
 
+Lemma abse_eq0 x : (`|x| == 0) = (x == 0).
+Proof. by move: x => [| |] //= r; rewrite !eqe normr_eq0. Qed.
+
 Lemma abse0 : `|0| = 0 :> \bar R. Proof. by rewrite /abse normr0. Qed.
 
 Lemma abseN x : `|- x| = `|x|.
@@ -1097,6 +1103,33 @@ Proof. by rewrite muleC mulrninfty. Qed.
 
 Definition mulrinfty := (mulrpinfty, mulpinftyr, mulrninfty, mulninftyr).
 
+Lemma mule_eqpinfty x y : (x * y == +oo) =
+  [|| (x > 0) && (y == +oo), (x < 0) && (y == -oo),
+     (x == +oo) && (y > 0) | (x == -oo) && (y < 0)].
+Proof.
+move: x y => [x| |] [y| |]; rewrite ?(lte_fin,andbF,andbT,orbF,eqxx,andbT)//=.
+- by rewrite mulrpinfty; have [/ltr0_sg|/gtr0_sg|] := ltgtP x 0%R;
+    move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
+- by rewrite mulrninfty; have [/ltr0_sg|/gtr0_sg|] := ltgtP x 0%R;
+    move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
+- by rewrite mulpinftyr; have [/ltr0_sg|/gtr0_sg|] := ltgtP y 0%R;
+    move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
+- by rewrite mule_pinfty_pinfty lte_pinfty.
+- by rewrite mule_pinfty_ninfty.
+- by rewrite mulninftyr; have [/ltr0_sg|/gtr0_sg|] := ltgtP y 0%R;
+    move=> ->; rewrite ?(mulN1e,mul1e,sgr0,mul0e).
+- by rewrite mule_ninfty_pinfty.
+- by rewrite lte_ninfty.
+Qed.
+
+Lemma mule_eqninfty x y : (x * y == -oo) =
+  [|| (x > 0) && (y == -oo), (x < 0) && (y == +oo),
+     (x == -oo) && (y > 0) | (x == +oo) && (y < 0)].
+Proof.
+have := mule_eqpinfty x (- y); rewrite muleN eqe_oppLR => ->.
+by rewrite !eqe_oppLR lte_oppr lte_oppl oppe0 (orbC _ ((x == -oo) && _)).
+Qed.
+
 Lemma lte_opp x y : (- x < - y) = (y < x).
 Proof. by rewrite lte_oppl oppeK. Qed.