separating_filter

_CoqProject

@@ -18,6 +18,7 @@ classical/functions.v
 classical/cardinality.v
 classical/fsbigop.v
 classical/set_interval.v
+classical/filter.v
 theories/all_analysis.v
 theories/constructive_ereal.v
 theories/ereal.v

classical/Make

@@ -16,4 +16,5 @@ functions.v
 cardinality.v
 fsbigop.v
 set_interval.v
+filter.v
 all_classical.v

classical/all_classical.v

@@ -6,3 +6,4 @@ From mathcomp Require Export functions.
 From mathcomp Require Export cardinality.
 From mathcomp Require Export fsbigop.
 From mathcomp Require Export set_interval.
+From mathcomp Require Export filter.

classical/mathcomp_extra.v

@@ -471,3 +471,11 @@ End floor_ceil.
 
 #[deprecated(since="mathcomp-analysis 1.3.0", note="renamed to `ceil_gt_int`")]
 Notation ceil_lt_int := ceil_gt_int (only parsing).
+
+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.

classical/set_interval.v

@@ -822,3 +822,68 @@ Lemma itv_setI {d} {T : orderType d} (i j : interval T) :
 Proof.
 by rewrite eqEsubset; split => z; rewrite /in_mem/= /pred_of_itv/= lexI=> /andP.
 Qed.
+
+Section bigmaxmin.
+Local Notation max := Order.max.
+Local Notation min := Order.min.
+Local Open Scope order_scope.
+Variables (d : Order.disp_t) (T : orderType d).
+Variables (x : T) (I : finType) (P : pred I) (m : T) (F : I -> T).
+
+Lemma bigmax_geP : reflect (m <= x \/ exists2 i, P i & m <= F i)
+                           (m <= \big[max/x]_(i | P i) F i).
+Proof.
+apply: (iffP idP) => [|[mx|[i Pi mFi]]].
+- rewrite leNgt => /bigmax_ltP /not_andP[/negP|]; first by rewrite -leNgt; left.
+  by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -leNgt; right; exists i.
+- by rewrite bigmax_idl le_max mx.
+- by rewrite (bigmaxD1 i)// le_max mFi.
+Qed.
+
+Lemma bigmax_gtP : reflect (m < x \/ exists2 i, P i & m < F i)
+                           (m < \big[max/x]_(i | P i) F i).
+Proof.
+apply: (iffP idP) => [|[mx|[i Pi mFi]]].
+- rewrite ltNge => /bigmax_leP /not_andP[/negP|]; first by rewrite -ltNge; left.
+  by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -ltNge; right; exists i.
+- by rewrite bigmax_idl lt_max mx.
+- by rewrite (bigmaxD1 i)// lt_max mFi.
+Qed.
+
+Lemma bigmin_leP : reflect (x <= m \/ exists2 i, P i & F i <= m)
+                           (\big[min/x]_(i | P i) F i <= m).
+Proof.
+apply: (iffP idP) => [|[xm|[i Pi Fim]]].
+- rewrite leNgt => /bigmin_gtP /not_andP[/negP|]; first by rewrite -leNgt; left.
+  by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -leNgt; right; exists i.
+- by rewrite bigmin_idl ge_min xm.
+- by rewrite (bigminD1 i)// ge_min Fim.
+Qed.
+
+Lemma bigmin_ltP : reflect (x < m \/ exists2 i, P i & F i < m)
+                           (\big[min/x]_(i | P i) F i < m).
+Proof.
+apply: (iffP idP) => [|[xm|[i Pi Fim]]].
+- rewrite ltNge => /bigmin_geP /not_andP[/negP|]; first by rewrite -ltNge; left.
+  by move=> /existsNP[i /not_implyP[Pi /negP]]; rewrite -ltNge; right; exists i.
+- by rewrite bigmin_idl gt_min xm.
+- by rewrite (bigminD1 _ _ _ Pi) gt_min Fim.
+Qed.
+
+End bigmaxmin.
+
+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.