From cc6d238f5688d7bfe3deb87c32225f0be45083c2 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Tue, 17 May 2022 16:13:16 +0900 Subject: [PATCH] shorten proof --- CHANGELOG_UNRELEASED.md | 10 ---- theories/ereal.v | 110 ++++++++++++++++++---------------------- theories/topology.v | 4 +- 3 files changed, 50 insertions(+), 74 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index ea70d08e05..1e029fa124 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -6,16 +6,6 @@ ### Changed -- in `esumv`: - + remove one hypothesis in lemmas `reindex_esum`, `esum_image` -- moved from `lebesgue_integral.v` to `lebesgue_measure.v` and generalized - + hint `measurable_set1`/`emeasurable_set1` -- in `sequences.v`: - + generalize `eq_nneseries`, `nneseries0` -- in `mathcomp_extra.v`: - + generalize `card_fset_sum1` -- in `lebesgue_integral.v`: - + change the notation `\int_` - in `ereal.v`: + lemmas `lee_paddl`, `lte_addl`, `lee_paddr`, `lte_paddr`, `lee_lt_add` - in `ereal.v`: diff --git a/theories/ereal.v b/theories/ereal.v index 8c8e316521..3d2d8f541c 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -3390,14 +3390,17 @@ Definition ereal_dnbhs (x : \bar R) (P : \bar R -> Prop) : Prop := | +oo => exists M, M \is Num.real /\ forall y, M%:E <= y -> P y | -oo => exists M, M \is Num.real /\ forall y, y <= M%:E -> P y end. + Definition ereal_nbhs (x : \bar R) (P : \bar R -> Prop) : Prop := match x with | x%:E => nbhs x (fun r => P r%:E) | +oo => exists M, M \is Num.real /\ forall y, M%:E <= y -> P y | -oo => exists M, M \is Num.real /\ forall y, y <= M%:E -> P y end. + Canonical ereal_ereal_filter := FilteredType (extended R) (extended R) (ereal_nbhs). + End ereal_nbhs. Lemma ereal_nbhs_pinfty_ge (R : numFieldType) (e : {posnum R}) : @@ -3416,70 +3419,53 @@ Context {R : numFieldType}. Global Instance ereal_dnbhs_filter : forall x : \bar R, ProperFilter (ereal_dnbhs x). Proof. -case=> [x||]. -- case: (Proper_dnbhs_numFieldType x) => x0 [//= xT xI xS]. - apply Build_ProperFilter' => //=; apply Build_Filter => //=. - move=> P Q lP lQ; exact: xI. - by move=> P Q PQ /xS; apply => y /PQ. -- apply Build_ProperFilter. - move=> P [x [xr xP]] //; exists (x + 1)%:E; apply xP => /=. - by rewrite lee_fin ler_addl. - split=> /= [|P Q [MP [MPr geMP]] [MQ [MQr geMQ]] |P Q sPQ [M [Mr geM]]]. - + by exists 0%R; rewrite real0. - + have [MP0|MP0] := eqVneq MP 0%R. - have [MQ0|MQ0] := eqVneq MQ 0%R. - by exists 0%R; rewrite real0; split => // x x0; split; - [apply/geMP; rewrite MP0 | apply/geMQ; rewrite MQ0]. - exists `|MQ|%R; rewrite realE normr_ge0; split => // x MQx; split. - by apply: geMP; rewrite (le_trans _ MQx) // MP0 lee_fin. - by apply geMQ; rewrite (le_trans _ MQx)// lee_fin real_ler_normr ?lexx. - have [MQ0|MQ0] := eqVneq MQ 0%R. - exists `|MP|%R; rewrite realE normr_ge0; split => // x MPx; split. - by apply geMP; rewrite (le_trans _ MPx)// lee_fin real_ler_normr ?lexx. - by apply geMQ; rewrite (le_trans _ MPx) // lee_fin MQ0. - have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0. - have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0. - exists (Num.max (PosNum MP0) (PosNum MQ0))%:num. - rewrite realE /= ge0 /=; split => //. - case=> [r| |//]. - * rewrite lee_fin /= num_max num_le_maxl /= => /andP[MPx MQx]; split. - by apply/geMP; rewrite lee_fin (le_trans _ MPx)// real_ler_normr ?lexx. - by apply/geMQ; rewrite lee_fin (le_trans _ MQx)// real_ler_normr ?lexx. - * by move=> _; split; [apply/geMP | apply/geMQ]. - + by exists M; split => // ? /geM /sPQ. -- apply Build_ProperFilter. - + move=> P [M [Mr ltMP]]; exists (M - 1)%:E. - by apply: ltMP; rewrite lee_fin ger_addl oppr_le0. - + split=> /= [|P Q [MP [MPr leMP]] [MQ [MQr leMQ]] |P Q sPQ [M [Mr leM]]]. - * by exists 0%R; rewrite real0. - * have [MP0|MP0] := eqVneq MP 0%R. - have [MQ0|MQ0] := eqVneq MQ 0%R. - by exists 0%R; rewrite real0; split => // x x0; split; - [apply/leMP; rewrite MP0 | apply/leMQ; rewrite MQ0]. - exists (- `|MQ|)%R; rewrite realN realE normr_ge0; split => // x xMQ. - split. - by apply leMP; rewrite (le_trans xMQ)// lee_fin MP0 ler_oppl oppr0. - apply leMQ; rewrite (le_trans xMQ) // lee_fin ler_oppl -normrN. - by rewrite real_ler_normr ?realN // lexx. - * have [MQ0|MQ0] := eqVneq MQ 0%R. - exists (- `|MP|)%R; rewrite realN realE normr_ge0; split => // x MPx. - split. - apply leMP; rewrite (le_trans MPx) // lee_fin ler_oppl -normrN. +move=> [r| |]. +- apply Build_ProperFilter' => //=; first exact: filter_not_empty. + by apply Build_Filter => //=; [exact: filterT|exact: filterI|exact: filterS]. +- apply: Build_ProperFilter => [P [x [_ xP]]|]; first by exists x%:E; exact: xP. + apply Build_Filter => /= [|P Q [r +] [s +] |P Q PQ [r [rr rP]]]. + + by exists 0%R. + + have [-> [_ rP] [sr sQ]|r0 [rr rP]] := eqVneq r 0%R. + exists `|s|%R; rewrite normr_real; split => // x sx; split. + exact/rP/(le_trans _ sx). + by apply/sQ/(le_trans _ sx); rewrite lee_fin real_ler_normr ?lexx. + have [-> [_ sQ]|s0 [sr sQ]] := eqVneq s 0%R. + exists `|r|%R; rewrite normr_real; split => // x rx; split. + by apply/rP/(le_trans _ rx); rewrite lee_fin real_ler_normr ?lexx. + exact/sQ/(le_trans _ rx). + have /andP[{}r0 {}s0]: ((0 < `|r|) && (0 < `|s|))%R by rewrite !normr_gt0 r0. + exists (Num.max (PosNum r0) (PosNum s0))%:num. + rewrite realE /= ge0 /=; split => // -[t|_|//]. + * rewrite lee_fin /= num_max num_le_maxl /= => /andP[rx sx]; split. + by apply/rP; rewrite lee_fin (le_trans _ rx)// real_ler_normr ?lexx. + by apply/sQ; rewrite lee_fin (le_trans _ sx)// real_ler_normr ?lexx. + * by split; [exact/rP|exact/sQ]. + + by exists r; split => // ? /rP /PQ. +- apply Build_ProperFilter => [P [x [_ xP]]|]. + + by exists (x - 1)%:E; apply: xP; rewrite lee_fin ger_addl. + + split=> /= [|P Q [r +] [s +] |P Q PQ [r [rr rP]]]. + * by exists 0%R. + * have [-> [_ rP] [sr sQ]|r0 [rr rP]] := eqVneq r 0%R. + exists (- `|s|)%R; rewrite realN normr_real; split => // x xs; split. + by apply/rP/(le_trans xs); rewrite lee_fin ler_oppl oppr0. + apply/sQ/(le_trans xs); rewrite lee_fin ler_oppl -normrN. + by rewrite real_ler_normr ?realN ?lexx. + have [-> [_ sQ]|s0 [sr sQ]] := eqVneq s 0%R. + exists (- `|r|)%R; rewrite realN normr_real; split => // x rx; split. + apply/rP/(le_trans rx); rewrite lee_fin ler_oppl -normrN. by rewrite real_ler_normr ?realN // lexx. - by apply leMQ; rewrite (le_trans MPx) // lee_fin MQ0 ler_oppl oppr0. - have {}MP0 : (0 < `|MP|)%R by rewrite normr_gt0. - have {}MQ0 : (0 < `|MQ|)%R by rewrite normr_gt0. - exists (- (Num.max (PosNum MP0) (PosNum MQ0))%:num)%R. - rewrite realN realE /= ge0 /=; split => //. - case=> [r|//|]. + by apply/sQ/(le_trans rx); rewrite lee_fin ler_oppl oppr0. + have /andP[{}r0 {}s0]: ((0 < `|r|) && (0 < `|s|))%R by rewrite !normr_gt0 r0. + exists (- (Num.max (PosNum r0) (PosNum s0))%:num)%R. + rewrite realN realE /= ge0 /=; split => // -[t|//|_]. - rewrite lee_fin ler_oppr num_max num_le_maxl => /andP[]. - rewrite ler_oppr => MPx; rewrite ler_oppr => MQx; split. - apply/leMP; rewrite lee_fin (le_trans MPx) //= ler_oppl -normrN. - by rewrite real_ler_normr ?realN // lexx. - apply/leMQ; rewrite lee_fin (le_trans MQx) //= ler_oppl -normrN. - by rewrite real_ler_normr ?realN // lexx. - - by move=> _; split; [apply/leMP | apply/leMQ]. - * by exists M; split => // x /leM /sPQ. + rewrite ler_oppr => rx; rewrite ler_oppr => sx; split. + apply/rP; rewrite lee_fin (le_trans rx) //= ler_oppl -normrN. + by rewrite real_ler_normr ?realN ?lexx. + apply/sQ; rewrite lee_fin (le_trans sx) //= ler_oppl -normrN. + by rewrite real_ler_normr ?realN ?lexx. + - by split; [exact/rP|exact/sQ]. + * by exists r; split => // ? /rP /PQ. Qed. Typeclasses Opaque ereal_dnbhs. diff --git a/theories/topology.v b/theories/topology.v index 470bdd66b0..06bfc7d33e 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -714,7 +714,7 @@ Local Notation "{ 'all3' P }" := (forall x y z, P x y z: Prop) (at level 0). Local Notation ph := (phantom _). Definition prop_near1 {X} {fX : filteredType X} (x : fX) - P (phP : ph {all1 P}) := nbhs x P. + P (phP : ph {all1 P}) := nbhs x P. Definition prop_near2 {X X'} {fX : filteredType X} {fX' : filteredType X'} (x : fX) (x' : fX') := fun P of ph {all2 P} => @@ -761,7 +761,7 @@ Proof. exact. Qed. #[global] Hint Resolve cvg_refl : core. Lemma cvg_trans T (G F H : set (set T)) : - (F `=>` G) -> (G `=>` H) -> (F `=>` H). + F `=>` G -> G `=>` H -> F `=>` H. Proof. by move=> FG GH P /GH /FG. Qed. Notation "F --> G" := (cvg_to [filter of F] [filter of G]) : classical_set_scope.