Lnorm_ge0 and Lnorm_eq0_eq0 need not be specialized

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -53,27 +53,6 @@
 
 - in `pi_irrational`:
   + definition `rational`
-- new directory `lebesgue_integral_theory` with new files:
-  + `simple_functions.v`
-  + `lebesgue_integral_definition.v`
-  + `lebesgue_integral_approximation.v`
-  + `lebesgue_integral_monotone_convergence.v`
-  + `lebesgue_integral_nonneg.v`
-  + `lebesgue_integrable.v`
-  + `lebesgue_integral_dominated_convergence.v`
-  + `lebesgue_integral_under.v`
-  + `lebesgue_Rintegral.v`
-  + `lebesgue_integral_fubini.v`
-  + `lebesgue_integral_differentiation.v`
-  + `lebesgue_integral.v`
-- in `boolp.v`:
-  + lemmas `orW`, `or3W`, `or4W`
-
-- in `classical_sets.v`:
-  + lemma `image_nonempty`
-
-- in `mathcomp_extra.v`:
-  + lemmas `eq_exists2l`, `eq_exists2r`
 
 - in `ereal.v`:
   + lemmas `ereal_infEN`, `ereal_supN`, `ereal_infN`, `ereal_supEN`
@@ -122,9 +101,6 @@
 - in `lebesgue_integral.v`:
   + lemma `mfunMn`
 
-- in `classical_sets.v`:
-  + lemma `set_cst`
-
 - in `measurable_realfun.v`:
   + lemmas `ereal_inf_seq`, `ereal_sup_seq`,
     `ereal_sup_cst`, `ereal_inf_cst`, `ereal_sup_pZl`,
@@ -168,32 +144,6 @@
 - in `probability.v`:
   + lemma `lfun1_expectation_lty`
 
-### Changed
-
-- file `nsatz_realtype.v` moved from `reals` to `reals-stdlib` package
-- moved from `gauss_integral` to `trigo.v`:
-  + `oneDsqr`, `oneDsqr_ge1`, `oneDsqr_inum`, `oneDsqrV_le1`,
-    `continuous_oneDsqr`, `continuous_oneDsqr`
-- moved, generalized, and renamed from `gauss_integral` to `trigo.v`:
-  + `integral01_oneDsqr` -> `integral0_oneDsqr`
-
-- in `interval_inference.v`:
-  + definition `IntItv.exprn_le1_bound`
-  + lemmas `Instances.nat_spec_succ`, `Instances.num_spec_natmul`,
-    `Instances.num_spec_intmul`, `Instances.num_itv_bound_exprn_le1`
-  + canonical instance `Instances.succn_inum`
-
-- in `lebesgue_integral_properties.v`
-  (new file with contents moved from `lebesgue_integral.v`)
-  + `le_normr_integral` renamed to `le_normr_Rintegral`
-
-- moved to `lebesgue_measure.v` (from old `lebesgue_integral.v`)
-  + `compact_finite_measure`
-
-- moved from `ftc.v` to `lebesgue_integral_under.v` (new file)
-  + notation `'d1`, definition `partial1of2`, lemmas `partial1of2E`,
-    `cvg_differentiation_under_integral`, `differentiation_under_integral`,
-    `derivable_under_integral`
 - in `hoelder.v`:
   + lemmas `Lnorm_eq0_eq0`
 
@@ -229,18 +179,12 @@
 
 - in `normedtype.v`:
   + lemmas `gt0_cvgMlNy`, `gt0_cvgMly`
-- in `boolp.v`:
-  + `eq_fun2` -> `eq2_fun`
-  + `eq_fun3` -> `eq3_fun`
-  + `eq_forall2` -> `eq2_forall`
-  + `eq_forall3` -> `eq3_forall`
+
 - in `ereal.v`:
   + `ereal_sup_le` -> `ereal_sup_ge`
 
 - in `hoelder.v`:
   + `minkowski` -> `minkowski_EFin`
-  + `Lnorm_ge0` -> `Lnormr_ge0`
-  + `Lnorm_eq0_eq0` -> `Lnormr_eq0_eq0`
 
 ### Generalized
 
@@ -265,44 +209,6 @@
 
 ### Removed
 
-- file `mathcomp_extra.v`
-  + lemma `Pos_to_natE` (moved to `Rstruct.v`)
-  + lemma `deg_le2_ge0` (available as `deg_le2_poly_ge0` in `ssrnum.v`
-    since MathComp 2.1.0)
-  + definitions `monotonous`, `boxed`, `onem`, `inv_fun`,
-    `bound_side`, `swap`, `prodA`, `prodAr`, `map_pair`, `sigT_fun`
-    (moved to new file `unstable.v` that shouldn't be used outside of
-    Analysis)
-  + notations `` `1 - r ``, `f \^-1` (moved to new file `unstable.v`
-    that shouldn't be used outside of Analysis)
-  + lemmas `dependent_choice_Type`, `maxr_absE`, `minr_absE`,
-    `le_bigmax_seq`, `bigmax_sup_seq`, `leq_ltn_expn`, `last_filterP`,
-    `path_lt_filter0`, `path_lt_filterT`, `path_lt_head`,
-    `path_lt_last_filter`, `path_lt_le_last`, `sumr_le0`,
-    `fset_nat_maximum`, `image_nat_maximum`, `card_fset_sum1`,
-    `onem0`, `onem1`, `onemK`, `add_onemK`, `onem_gt0`, `onem_ge0`,
-    `onem_le1`, `onem_lt1`, `onemX_ge0`, `onemX_lt1`, `onemD`,
-    `onemMr`, `onemM`, `onemV`, `lez_abs2`, `ler_gtP`, `ler_ltP`,
-    `real_ltr_distlC`, `prodAK`, `prodArK`, `swapK`, `lt_min_lt`,
-    `intrD1`, `intr1D`, `floor_lt_int`, `floor_ge0`, `floor_le0`,
-    `floor_lt0`, `floor_eq`, `floor_neq0`, `ceil_gt_int`, `ceil_ge0`,
-    `ceil_gt0`, `ceil_le0`, `abs_ceil_ge`, `nat_int`, `bij_forall`,
-    `and_prop_in`, `mem_inc_segment`, `mem_dec_segment`,
-    `partition_disjoint_bigfcup`, `partition_disjoint_bigfcup`,
-    `prodr_ile1`, `size_filter_gt0`, `ltr_sum`, `ltr_sum_nat` (moved
-    to new file `unstable.v` that shouldn't be used outside of
-    Analysis)
-
-- in `reals.v`:
-  + lemmas `floor_le`, `le_floor` (deprecated since 1.3.0)
-
-- file `lebesgue_integral.v` (split in several files in the directory
-  `lebesgue_integral_theory`)
-
-- in `classical_sets.v`:
-  + notations `setvI`, `setIv`, `bigcup_set`, `bigcup_set_cond`, `bigcap_set`,
-    `bigcap_set_cond`
-
 - in `measure.v`:
   + definition `almost_everywhere_notation`
   + lemma `ess_sup_ge0`

classical/mathcomp_extra.v

@@ -470,148 +470,3 @@ Proof. by move=>  ? ? []. Qed.
 
 Lemma inl_inj {A B} : injective (@inl A B).
 Proof. by move=>  ? ? []. Qed.
-
-Section bijection_forall.
-
-Lemma bij_forall A B (f : A -> B) (P : B -> Prop) :
-  bijective f -> (forall y, P y) <-> (forall x, P (f x)).
-Proof.
-by case; rewrite /cancel => g _ cangf; split => // => ? y; rewrite -(cangf y).
-Qed.
-
-End bijection_forall.
-
-Lemma and_prop_in (T : Type) (p : mem_pred T) (P Q : T -> Prop) :
-  {in p, forall x, P x /\ Q x} <->
-  {in p, forall x, P x} /\ {in p, forall x, Q x}.
-Proof.
-split=> [cnd|[cnd1 cnd2] x xin]; first by split=> x xin; case: (cnd x xin).
-by split; [apply: cnd1 | apply: cnd2].
-Qed.
-
-Lemma mem_inc_segment d (T : porderType d) (a b : T) (f : T -> T) :
-    {in `[a, b] &, {mono f : x y / (x <= y)%O}} ->
-  {homo f : x / x \in `[a, b] >-> x \in `[f a, f b]}.
-Proof.
-move=> fle x xab; have leab : (a <= b)%O by rewrite (itvP xab).
-by rewrite in_itv/= !fle ?(itvP xab).
-Qed.
-
-Lemma mem_dec_segment d (T : porderType d) (a b : T) (f : T -> T) :
-    {in `[a, b] &, {mono f : x y /~ (x <= y)%O}} ->
-  {homo f : x / x \in `[a, b] >-> x \in `[f b, f a]}.
-Proof.
-move=> fge x xab; have leab : (a <= b)%O by rewrite (itvP xab).
-by rewrite in_itv/= !fge ?(itvP xab).
-Qed.
-
-Definition sigT_fun {I : Type} {X : I -> Type} {T : Type}
-  (f : forall i, X i -> T) (x : {i & X i}) : T :=
-  (f (projT1 x) (projT2 x)).
-
-(* PR 114 to finmap in progress *)
-Section FsetPartitions.
-Variables T I : choiceType.
-Implicit Types (x y z : T) (A B D X : {fset T}) (P Q : {fset {fset T}}).
-Implicit Types (J : pred I) (F : I -> {fset T}).
-
-Variables (R : Type) (idx : R) (op : Monoid.com_law idx).
-Let rhs_cond P K E :=
-  (\big[op/idx]_(A <- P) \big[op/idx]_(x <- A | K x) E x)%fset.
-Let rhs P E := (\big[op/idx]_(A <- P) \big[op/idx]_(x <- A) E x)%fset.
-
-Lemma partition_disjoint_bigfcup (f : T -> R) (F : I -> {fset T})
-  (K : {fset I}) :
-  (forall i j, i \in K -> j \in K -> i != j -> [disjoint F i & F j])%fset ->
-  \big[op/idx]_(i <- \big[fsetU/fset0]_(x <- K) (F x)) f i =
-  \big[op/idx]_(k <- K) (\big[op/idx]_(i <- F k) f i).
-Proof.
-move=> disjF; pose P := [fset F i | i in K & F i != fset0]%fset.
-have trivP : trivIfset P.
-  apply/trivIfsetP => _ _ /imfsetP[i iK ->] /imfsetP[j jK ->] neqFij.
-  move: iK; rewrite !inE/= => /andP[iK Fi0].
-  move: jK; rewrite !inE/= => /andP[jK Fj0].
-  by apply: (disjF _ _ iK jK); apply: contraNneq neqFij => ->.
-have -> : (\bigcup_(i <- K) F i)%fset = fcover P.
-  apply/esym; rewrite /P fcover_imfset big_mkcond /=; apply eq_bigr => i _.
-  by case: ifPn => // /negPn/eqP.
-rewrite big_trivIfset // /rhs big_imfset => [|i j iK /andP[jK notFj0] eqFij] /=.
-  rewrite big_filter big_mkcond; apply eq_bigr => i _.
-  by case: ifPn => // /negPn /eqP ->;  rewrite big_seq_fset0.
-move: iK; rewrite !inE/= => /andP[iK Fi0].
-by apply: contraNeq (disjF _ _ iK jK) _; rewrite -fsetI_eq0 eqFij fsetIid.
-Qed.
-
-End FsetPartitions.
-
-(* TODO: move to ssrnum *)
-Lemma prodr_ile1 {R : realDomainType} (s : seq R) :
-  (forall x, x \in s -> 0 <= x <= 1)%R -> (\prod_(j <- s) j <= 1)%R.
-Proof.
-elim: s => [_ | y s ih xs01]; rewrite ?big_nil// big_cons.
-have /andP[y0 y1] : (0 <= y <= 1)%R by rewrite xs01// mem_head.
-rewrite mulr_ile1 ?andbT//.
-  rewrite big_seq prodr_ge0// => x xs.
-  by have := xs01 x; rewrite inE xs orbT => /(_ _)/andP[].
-by rewrite ih// => e xs; rewrite xs01// in_cons xs orbT.
-Qed.
-
-(* TODO: move to ssrnum *)
-
-Lemma size_filter_gt0 T P (r : seq T) : (size (filter P r) > 0)%N = (has P r).
-Proof. by elim: r => //= x r; case: ifP. Qed.
-
-Lemma ltr_sum [R : numDomainType] [I : Type] (r : seq I)
-    [P : pred I] [F G : I -> R] :
-  has P r ->
-  (forall i : I, P i -> F i < G i) ->
-  \sum_(i <- r | P i) F i < \sum_(i <- r | P i) G i.
-Proof.
-rewrite -big_filter -[ltRHS]big_filter -size_filter_gt0.
-case: filter (filter_all P r) => //= x {}r /andP[Px Pr] _ ltFG.
-rewrite !big_cons ltr_leD// ?ltFG// -(all_filterP Pr) !big_filter.
-by rewrite ler_sum => // i Pi; rewrite ltW ?ltFG.
-Qed.
-
-Lemma ltr_sum_nat [R : numDomainType] [m n : nat] [F G : nat -> R] :
-  (m < n)%N -> (forall i : nat, (m <= i < n)%N -> F i < G i) ->
-  \sum_(m <= i < n) F i < \sum_(m <= i < n) G i.
-Proof.
-move=> lt_mn i; rewrite big_nat [ltRHS]big_nat ltr_sum//.
-by apply/hasP; exists m; rewrite ?mem_index_iota leqnn lt_mn.
-Qed.
-
-Lemma eq_exists2l (A : Type) (P P' Q : A -> Prop) :
-  (forall x, P x <-> P' x) ->
-  (exists2 x, P x & Q x) <-> (exists2 x, P' x & Q x).
-Proof.
-by move=> eqQ; split=> -[x p q]; exists x; move: p q; rewrite ?eqQ.
-Qed.
-
-Lemma eq_exists2r (A : Type) (P Q Q' : A -> Prop) :
-  (forall x, Q x <-> Q' x) ->
-  (exists2 x, P x & Q x) <-> (exists2 x, P x & Q' x).
-Proof.
-by move=> eqP; split=> -[x p q]; exists x; move: p q; rewrite ?eqP.
-Qed.
-
-Declare Scope signature_scope.
-Delimit Scope signature_scope with signature.
-
-Import -(notations) Morphisms.
-Arguments Proper {A}%_type R%_signature m.
-Arguments respectful {A B}%_type (R R')%_signature _ _.
-
-Module ProperNotations.
-
-Notation " R ++> R' " := (@respectful _ _ (R%signature) (R'%signature))
-  (right associativity, at level 55) : signature_scope.
-
-Notation " R ==> R' " := (@respectful _ _ (R%signature) (R'%signature))
-  (right associativity, at level 55) : signature_scope.
-
-Notation " R ~~> R' " := (@respectful _ _ (Program.Basics.flip (R%signature)) (R'%signature))
-  (right associativity, at level 55) : signature_scope.
-
-Export -(notations) Morphisms.
-End ProperNotations.