diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 59c48b1a3..092b3bf78 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -49,6 +49,39 @@ - in `lebesgue_integral.v`: + lemma `abse_integralP` +- in `classical_sets.v`: + + lemma `set_cons1` + + lemma `trivIset_bigcup` + + definition `maximal_disjoint_subcollection` + + lemma `ex_maximal_disjoint_subcollection` + +- in `mathcomp_extra.v`: + + lemma `leq_ltn_expn` + +- in `lebesgue_measure.v`: + + lemma `lebesgue_measurable_ball` + + lemmas `measurable_closed_ball`, `lebesgue_measurable_closed_ball` + +- in `normedtype.v`: + + lemmas `ball0`, `ball_itv`, `closed_ball0`, `closed_ball_itv` + + definitions `cpoint`, `radius`, `is_ball` + + definition `scale_ball`, notation notation ``` *` ``` + + lemmas `sub_scale_ball`, `scale_ball1`, `sub1_scale_ball` + + lemmas `ball_inj`, `radius0`, `cpoint_ball`, `radius_ball_num`, + `radius_ball`, `is_ballP`, `is_ball_ball`, `scale_ball0`, + `ballE`, `is_ball_closure`, `scale_ballE`, `cpoint_scale_ball`, + `radius_scale_ball` + + lemmas `vitali_lemma_finite`, `vitali_lemma_finite_cover` + + definition `vitali_collection_partition` + + lemmas `vitali_collection_partition_ub_gt0`, + `ex_vitali_collection_partition`, `cover_vitali_collection_partition`, + `disjoint_vitali_collection_partition` + + lemma `separate_closed_ball_countable` + + lemmas `vitali_lemma_infinite`, `vitali_lemma_infinite_cover` + +- in `topology.v`: + + lemmas `closure_eq0`, `separated_open_countable` + ### Changed - in `hoelder.v`: @@ -134,6 +167,8 @@ - in `lebesgue_integral.v`: + weaken an hypothesis of `integral_ae_eq` +- in `classical_sets.v`: + + `set_nil` generalized to `eqType` ### Deprecated diff --git a/theories/normedtype.v b/theories/normedtype.v index 9785df0a0..9e8285c6d 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -99,9 +99,13 @@ Require Import ereal reals signed topology prodnormedzmodule. (* the Heine-Borel theorem, which states that the compact sets of R^n are *) (* the closed and bounded sets. *) (* *) +(* cpoint A == the center of the set A if it is an open ball *) +(* radius A == the radius of the set A if it is an open ball *) +(* radius A has type {nonneg R} *) +(* is_ball A == boolean predicate that holds when A is an open ball *) +(* k *` A == open ball with center cpoint A and radius k * radius A *) (* vitali_collection_partition B V r n == subset of indices of V such the *) -(* the ball B i as a radius between r/2^n+1 *) -(* and r/2^n *) +(* the ball B i as a radius between r/2^n+1 and r/2^n *) (* *) (******************************************************************************) @@ -6311,7 +6315,7 @@ rewrite [in LHS](ballE ballA) (scale_ballE _ _ (ltW k0))// cpoint_ball//. by rewrite mulr_gt0. Qed. -Lemma radius_sball (A : set R) (k : R) : 0 <= k -> is_ball A -> +Lemma radius_scale_ball (A : set R) (k : R) : 0 <= k -> is_ball A -> (radius (k *` A))%:num = k * (radius A)%:num. Proof. move=> k0 ballA. @@ -6608,7 +6612,7 @@ exists j; split => //. rewrite (ballE (is_ballB j)) scale_ballE; last by []. by rewrite radius_ball_num ?mulr_ge0// mulr_gt0. rewrite /closed_ball_ /= cpoint_scale_ball; [|by []..]. - rewrite radius_sball//. + rewrite radius_scale_ball//. apply: (@le_trans _ _ (2 * (radius (B i))%:num + (radius (B j))%:num)). case: BiBj => y [Biy Bjy]. rewrite (le_trans (ler_dist_add y _ _))// [in leRHS]addrC ler_add//.