rebase, minor simplifications

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -33,86 +33,9 @@
     `wlength_sigma_sub_additive`, `wlength_sigma_finite`
   + measure instance of `hlength`
   + definition `lebesgue_stieltjes_measure`
-- in `kernel.v`:
-  + `kseries` is now an instance of `Kernel_isSFinite_subdef`
-- in `classical_sets.v`:
-  + lemma `setU_id2r`
-- in `lebesgue_measure.v`:
-  + lemma `compact_measurable`
-
-- in `measure.v`:
-  + lemmas `outer_measure_subadditive`, `outer_measureU2`
-
-- in `lebesgue_measure.v`:
-  + declare `lebesgue_measure` as a `SigmaFinite` instance
-  + lemma `lebesgue_regularity_inner_sup`
-- in `convex.v`:
-  + lemmas `conv_gt0`, `convRE`
-
-- in `exp.v`:
-  + lemmas `concave_ln`, `conjugate_powR`
-
-- in file `lebesgue_integral.v`,
-  + new lemmas `integral_le_bound`, `continuous_compact_integrable`, and 
-    `lebesgue_differentiation_continuous`.
-
-- in `normedtype.v`:
-  + lemmas `open_itvoo_subset`, `open_itvcc_subset`
-
-- in `lebesgue_measure.v`:
-  + lemma `measurable_ball`
-
-- in file `normedtype.v`,
-  + new lemmas `normal_openP`, `uniform_regular`,
-    `regular_openP`, and `pseudometric_normal`.
-- in file `topology.v`,
-  + new definition `regular_space`.
-  + new lemma `ent_closure`.
-
-- in `lebesgue_measure.v`:
-  + lemma `measurable_mulrr`
-
-- in `constructive_ereal.v`:
-  + lemma `eqe_pdivr_mull`
-
-- new file `hoelder.v`:
-  + definition `Lnorm`, notations `'N[mu]_p[f]`, `'N_p[f]`
-  + lemmas `Lnorm1`, `Lnorm_ge0`, `eq_Lnorm`, `Lnorm_eq0_eq0`
-  + lemma `hoelder`
-
-- in file `lebesgue_integral.v`,
-  + new lemmas `simple_bounded`, `measurable_bounded_integrable`, 
-    `compact_finite_measure`, `approximation_continuous_integrable`
-
-- in `sequences.v`:
-  + lemma `cvge_harmonic`
-
-- in `mathcomp_extra.v`:
-  + lemmas `le_bigmax_seq`, `bigmax_sup_seq`
-
-- in `constructive_ereal.v`:
-  + lemma `bigmaxe_fin_num`
-- in `ereal.v`:
-  + lemmas `uboundT`, `supremumsT`, `supremumT`, `ereal_supT`, `range_oppe`,
-    `ereal_infT`
-
-- in `measure.v`:
-  + definition `ess_sup`, lemma `ess_sup_ge0`
-- in `convex.v`:
-  + definition `convex_function`
-
-- in `exp.v`:
-  + lemmas `ln_le0`, `ger_powR`, `ler1_powR`, `le1r_powR`, `ger1_powR`,
-    `ge1r_powR`, `ge1r_powRZ`, `le1r_powRZ`
-
-- in `hoelder.v`:
-  + lemmas `lnormE`, `hoelder2`, `convex_powR`
-
-- in `lebesgue_integral.v`:
-  + lemma `ge0_integral_count`
 
 - in `exp.v`:
-  + lemmas `powRDm1`, `poweRN`, `poweR_lty`, `lty_powerRy`, `gt0_ler_poweR`
+  + lemmas `powRDm1`, `fin_num_poweR`, poweRN`, `poweR_lty`, `lty_powerRy`, `gt0_ler_poweR`
 
 - in `mathcomp_extra.v`:
   + lemma `oneminv`

classical/mathcomp_extra.v

@@ -1016,6 +1016,8 @@ Arguments max_fun {T R} _ _ _ /.
 (* End of mathComp > 1.16 additions *)
 (************************************)
 
+Reserved Notation "`1- x" (format "`1- x", at level 2).
+
 Section onem.
 Variable R : numDomainType.
 Implicit Types r : R.
@@ -1065,7 +1067,7 @@ Qed.
 End onem.
 Notation "`1- r" := (onem r) : ring_scope.
 
-Lemma oneminv (F : numFieldType) (x : F) : x != 0 -> `1- (x^-1) = (x-1)/x.
+Lemma oneminv (F : numFieldType) (x : F) : x != 0 -> `1- (x^-1) = (x - 1) / x.
 Proof. by move=> ?; rewrite mulrDl divff// mulN1r. Qed.
 
 Lemma lez_abs2 (a b : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N.

theories/exp.v

@@ -769,12 +769,8 @@ Qed.
 
 Lemma powRDm1 (x p : R) : 0 <= x -> 0 < p -> x * x `^ (p - 1) = x `^ p.
 Proof.
-move=> x0 p0.
-have [->|xneq0] := eqVneq x 0.
-  by rewrite mul0r powR0// gt_eqF.
-rewrite -{1}(@powRr1 x)// -powRD.
-  by rewrite addrCA subrr addr0.
-by rewrite xneq0 implybT.
+rewrite le_eqVlt => /predU1P[<- p0|x0 p0]; first by rewrite mul0r powR0 ?gt_eqF.
+by rewrite -{1}(powRr1 (ltW x0))// -powRD addrCA subrr addr0// gt_eqF.
 Qed.
 
 Lemma powRN x r : x `^ (- r) = (x `^ r)^-1.
@@ -892,8 +888,8 @@ Proof.
 by move: x => [x'| |]//= x0; rewrite ?powRr1// (negbTE (oner_neq0 _)).
 Qed.
 
-Lemma poweRN (x : \bar R) r : x \is a fin_num -> x `^ (- r) = (((fine x) `^ r)^-1)%:E.
-Proof. case: x => // x xf. by rewrite poweR_EFin powRN. Qed.
+Lemma poweRN x r : x \is a fin_num -> x `^ (- r) = (fine x `^ r)^-1%:E.
+Proof. by case: x => // x xf; rewrite poweR_EFin powRN. Qed.
 
 Lemma poweRNyr r : r != 0%R -> -oo `^ r = 0.
 Proof. by move=> r0 /=; rewrite (negbTE r0). Qed.
@@ -904,14 +900,14 @@ Proof. by case: x => [x| |] //=; case: ifP. Qed.
 Lemma eqy_poweR x r : (0 < r)%R -> x = +oo -> x `^ r = +oo.
 Proof. by move: x => [| |]//= r0 _; rewrite gt_eqF. Qed.
 
-Lemma poweR_lty (a : \bar R) (r : R) : a < +oo -> a `^ r < +oo.
+Lemma poweR_lty x r : x < +oo -> x `^ r < +oo.
 Proof.
-by move: a => [a| | _]//=; rewrite ?ltry//; case: ifPn => // _; rewrite ltry.
+by move: x => [x| |]//=; rewrite ?ltry//; case: ifPn => // _; rewrite ltry.
 Qed.
 
-Lemma lty_poweRy (a : \bar R) (r : R) : r != 0%R -> a `^ r < +oo -> a < +oo.
+Lemma lty_poweRy x r : r != 0%R -> x `^ r < +oo -> x < +oo.
 Proof.
-by move=> r0; move: a => [a| | _]//=; rewrite ?ltry// (negbTE r0).
+by move=> r0; move: x => [x| | _]//=; rewrite ?ltry// (negbTE r0).
 Qed.
 
 Lemma poweR0r r : r != 0%R -> 0 `^ r = 0.
@@ -950,14 +946,18 @@ Proof. by move=> + /eqP => /poweR_eq0-> /andP[/eqP]. Qed.
 Lemma gt0_ler_poweR (r : R) : (0 <= r)%R ->
   {in `[0, +oo] &, {homo poweR ^~ r : x y / x <= y >-> x <= y}}.
 Proof.
-move=> r0 x y.
-case: x => //= [x /[1!in_itv]/= /andP[xint _]| _ _].
+move=> r0 + y; case=> //= [x /[1!in_itv]/= /andP[xint _]| _ _].
 - case: y => //= [y /[1!in_itv]/= /andP[yint _] xy| _ _].
-  - rewrite !lee_fin ge0_ler_powR//.
-  - by case: eqP => [->|]; rewrite ?powRr0 ?leey.
+  + by rewrite !lee_fin ge0_ler_powR.
+  + by case: eqP => [->|]; rewrite ?powRr0 ?leey.
 - by rewrite leye_eq => /eqP ->.
 Qed.
 
+Lemma fin_num_poweR x r : x \is a fin_num -> x `^ r \is a fin_num.
+Proof.
+by move=> xfin; rewrite ge0_fin_numE ?poweR_lty ?ltey_eq ?xfin// poweR_ge0.
+Qed.
+
 Lemma poweRM x y r : 0 <= x -> 0 <= y -> (x * y) `^ r = x `^ r * y `^ r.
 Proof.
 have [->|rN0] := eqVneq r 0%R; first by rewrite !poweRe0 mule1.