fixes

- fix changelog
- spurious parentheses
- tentative CI fix

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -63,6 +63,15 @@
   + `measurable_function.v`
   + `measure.v`
 
+- in `realfun.v`:
+  + lemmas `derivable_oy_continuous_within_itvcy`,
+           `derivable_oy_continuous_within_itvNyc`
+  + lemmas `derivable_oo_continuousW`,
+           `derivable_oy_continuousWoo`,
+           `derivable_oy_continuousW`,
+           `derivable_Nyo_continuousWoo`,
+           `derivable_Nyo_continuousW`
+
 - in `pseudometric_normed_Zmodule.v`:
   + lemma `continuous_comp_cvg`
 
@@ -72,14 +81,6 @@
 - in `ftc.v`:
   + lemmas `integration_by_substitution_onem`, `Rintegration_by_substitution_onem`
 
-- in `realfun.v`:
-  + lemmas `derivable_oy_continuous_within_itvcy`,
-           `derivable_oy_continuous_within_itvNyc`
-  + lemmas `derivable_oo_continuousW`,
-           `derivable_oy_continuousWoo`,
-           `derivable_oy_continuousW`,
-           `derivable_Nyo_continuousWoo`,
-           `derivable_Nyo_continuousW`
 - in `probability.v`:
   + lemmas `continuous_onemXn`, `onemXn_derivable`,
     `derivable_oo_continuous_bnd_onemXnMr`, `derive_onemXn`,
@@ -380,19 +381,6 @@
   + `le_ereal_inf` -> `ereal_inf_le_tmp`
   + `lb_ereal_inf` -> `le_ereal_inf_tmp`
   + `ereal_sup_ge` -> `le_ereal_sup_tmp`
-- in `measure.v`
-  + definition `ess_sup` moved to `ess_sup_inf.v`
-
-- in `convex.v`
-  + lemma `conv_gt0` to `convR_gt0`
-- in `tvs.v`
-  + HB class `TopologicalNmodule` moved to `PreTopologicalNmodule`
-  + HB class `TopologicalZmodule` moved to `PreTopologicalZmodule`
-  + HB class `TopologicalLmodule` moved to `PreTopologicalLmodule`
-  + structure `topologicalLmodule` moved to `preTopologicalLmodule`
-  + HB class `UniformNmodule` moved to `PreUniformNmodule`
-  + HB class `UniformZmodule` moved to `PreUniformZmodule`
-  + HB class `UniformLmodule` moved to `PreUniformLmodule`
 
 - in `probability.v`:
   + `bernoulli` -> `bernoulli_prob`

theories/ftc.v

@@ -1801,8 +1801,8 @@ Local Open Scope ereal_scope.
 Lemma integration_by_substitution_onem (G : R -> R) (r : R) :
   (0 < r <= 1)%R ->
   {within `[0%R, r], continuous G} ->
-  (\int[mu]_(x in `[0%R, r]) (G x)%:E =
-  \int[mu]_(x in `[`1-r, 1%R]) (G `1-x)%:E).
+  \int[mu]_(x in `[0%R, r]) (G x)%:E =
+  \int[mu]_(x in `[`1-r, 1%R]) (G `1-x)%:E.
 Proof.
 move=> r01 cG.
 have := @integration_by_substitution_decreasing R onem G `1-r 1.

theories/probability.v

@@ -2756,7 +2756,7 @@ apply: integrableB => //=.
     by rewrite lee_fin invr_ge0 beta_fun_ge0.
   rewrite (_ : integral _ _ _ = \int[lebesgue_measure]_x
     (((@XMonemX R a.-1 b.-1) \_ `[0, 1]) x)%:E)%E; last first.
-    rewrite integral_mkcond/=; apply: eq_integral => /= x _.
+    rewrite [LHS]integral_mkcond/=; apply: eq_integral => /= x _.
     by rewrite !patchE; case: ifPn => // ->.
   have /integrableP[_] := @integrable_XMonemX_restrict R a b.
   under eq_integral.