fixes

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -111,19 +111,24 @@
 - in `measurable_realfun.v`:
   + lemmas `measurable_funrpos`, `measurable_funrneg`
 
+- in `classical_sets.v`:
+  + lemmas `setI_closed_setT`, `setI_closed_set0`
+
+- in `measurable_function.v`:
+  + lemma `g_sigma_algebra_preimage_comp`
+
+- in `measure_function.v`:
+  + lemma `g_sigma_algebra_finite_measure_unique`
+
 - new file `independence.v`:
   + definition `independent_events`
   + definition `mutual_independence`
   + lemma `eq_mutual_independence`
   + definition `independence2`, `independence2P`
-  + lemmas `setI_closed_setT`, `setI_closed_set0`
-  + lemma `g_sigma_algebra_finite_measure_unique`
   + lemma `mutual_independence_fset`
   + lemma `mutual_independence_finiteS`
   + theorem `mutual_independence_finite_g_sigma`
   + lemma `mutual_dependence_bigcup`
-  + lemmas `g_sigma_algebra_preimage_comp`, `g_sigma_algebra_preimage_funrpos`,
-    `g_sigma_algebra_preimage_funrneg`
   + definition `independent_RVs`
   + lemma `independent_RVsD1`
   + theorem `independent_generators`
@@ -135,9 +140,9 @@
   + lemmas `independent_RVs2_product_measure1`
   + lemmas `independent_RVs2_setI_preimage`,
     `independent_Lfun1_expectation_product_measure_lty`
-  + lemmas `expectationM_nnsfun`, `expectationM_ge0`,
-    `ge0_independent_expectationM`, `independent_Lfun1_expectationM_lty`,
-    `independent_Lfun1M`, `independent_expectationM`
+  + lemma `ge0_independent_expectationM`
+  + lemmas `independent_Lfun1_expectationM_lty`, `independent_Lfun1M`,
+    `independent_expectationM`
 
 - in `ereal.v`:
   + lemma `ge0_addBefctE`

classical/classical_sets.v

@@ -1651,6 +1651,22 @@ Definition setU_closed := forall A B, G A -> G B -> G (A `|` B).
 
 End set_systems.
 
+Lemma setI_closed_setT T (F : set_system T) :
+  setI_closed F -> setI_closed (F `|` [set setT]).
+Proof.
+move=> IF=> C D [FC|/= ->{C}].
+- by move=> [FD|/= ->{D}]; [left; exact: IF|rewrite setIT; left].
+- by move=> [FD|->{D}]; [rewrite setTI; left|rewrite !setTI; right].
+Qed.
+
+Lemma setI_closed_set0 T (F : set_system T) :
+  setI_closed F -> setI_closed (F `|` [set set0]).
+Proof.
+move=> IF=> C D [FC|/= ->{C}].
+- by move=> [FD|/= ->{D}]; [left; exact: IF|rewrite setI0; right].
+- by move=> [FD|->{D}]; [rewrite set0I; right|rewrite !set0I; right].
+Qed.
+
 Section rectangle.
 Context {T1 T2 : Type}.
 Implicit Types (X : set_system T1) (Y : set_system T2).

theories/hoelder.v

@@ -538,7 +538,7 @@ Lemma convex_powR p : 1 <= p ->
   convex_function (`[0, +oo[%classic : set R) (@powR R ^~ p).
 Proof.
 move=> p1 t x y /[!inE] /= /[!in_itv] /= /[!andbT] x_ge0 y_ge0.
-have p0 : 0 < p by rewrite (lt_le_trans _ p1).  
+have p0 : 0 < p by rewrite (lt_le_trans _ p1).
 rewrite convRE [X in X `^ _ <= _]convRE; set w1 := t%:num; set w2 := t%:inum.~.
 have [->|w20] := eqVneq w2 0.
   rewrite !mul0r !addr0; have [->|w10] := eqVneq w1 0.