Module mathcomp.classical.unstable

From HB Require Import structures.
From mathcomp Require Import boot order finmap ssralg ssrnum ssrint.
From mathcomp Require Import vector archimedean interval matrix.

# Unstable This files contains lemmas that should eventually be backported to mathcomp. These lemmas may change before being backported to mathcomp, don't use anything in this file outside of Analysis. For this same reason, nothing in this file should be mentioned in the changelog. Once a result is backported to mathcomp, please move it to mathcomp_extra.v and mention it in the changelog. ``` clamp x := max (min x max) min swap x := (x.2, x.1) map_pair f x := (f x.1, f x.2) nondecreasing_fun f == the function f is non-decreasing nonincreasing_fun f == the function f is non-increasing increasing_fun f == the function f is (strictly) increasing decreasing_fun f == the function f is (strictly) decreasing nondecreasing_seq u == the sequence u is non-decreasing nonincreasing_seq u == the sequence u is non-increasing monotonic A f := {in A &, {homo f : x y / x <= y}} \/ {in A &, {homo f : x y /~ x <= y}} strict_monotonic A f := {in A &, {homo f : x y / x < y}} \/ {in A &, {homo f : x y /~ x < y}} sigT_fun f := lifts a family of functions f into a function on the dependent sum prodA x := sends (X * Y) * Z to X * (Y * Z) prodAr x := sends X * (Y * Z) to (X * Y) * Z isSemiNorm f == f : K -> L is a seminorm K is a numDomainType. L is a lmodType K. The HB class is SemiNorm. isNorm f == f : K -> L is a norm K is a numDomainType. L is a lmodType K. The HB class is Norm. Module MaxNngComLaw == contains on instance of Monoid.isComLaw on (@maxr {nonneg _}) to be used with caution ``` In module `EndlessDense`: ``` is_endless {d} T == forall x, (exists y, y < x) /\ (exists y, x < y) is_dense {d} T == forall x y, x < y -> exists z, x < z < y ``` The implementation of this module is likely to change following the review of https://github.com/math-comp/math-comp/pull/1597.

Attributes warn(note="The unstable.v file should only be used inside analysis.",
cats="internal-analysis").

Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.

Import Order.TTheory GRing.Theory Num.Theory.
Local Open Scope ring_scope.

Section Clamp.
Context { : realDomainType} ( : R).
Hypothesis : min <= max.

Definition ( : R) := Num.max (Num.min x max) min.

Lemma : min <= clamp x.

Proof.

by rewrite le_max lexx orbT. Qed.

Lemma : clamp x <= max.

Proof.

by rewrite ge_max ge_min lexx minmax orbT. Qed.

Definition := (clamp_gemin, clamp_lemax).

Lemma : min <= x <= max -> clamp x = x.

Proof.

by case/andP => minx xmax; rewrite /clamp min_l ?max_l. Qed.

Lemma : clamp (clamp x) = clamp x.

Proof.

by rewrite minmax_clamp// !clamp_gele. Qed.

Lemma : clamp min = min.

Proof.

by rewrite minmax_clamp// lexx minmax. Qed.

Lemma : clamp max = max.

Proof.

by rewrite minmax_clamp// lexx minmax. Qed.

End Clamp.

Module .
Import Order.
Definition : disp_t.

Proof.

exact: Disp tt tt. Defined.

End Order.

Definition {} { : I -> Type} ( : forall , T i) := f i.

Section DFunWith.
Variables ( : eqType) ( : I' -> Type) ( : forall , T i).

Lemma ( : T i) : cancel (@dfwith _ _ f i) (proj i).

Proof.

by move=> z; rewrite /proj dfwith_in. Qed.

End DFunWith.

Lemma { : zmodType} ( : 'M[V]_(m, n1)) ( : 'M[V]_(m, n2))
( : 'M[V]_(m, n1)) ( : 'M[V]_(m, n2)) :
row_mx A1 A2 - row_mx B1 B2 = row_mx (A1 - B1) (A2 - B2).

Proof.

by rewrite opp_row_mx add_row_mx. Qed.

Section IntervalNumDomain.
Variable : numDomainType.
Implicit Types x : R.

Lemma ( : R) :
(- x \in Interval (BInfty _ ba) (BSide bb xb)) =
(x \in Interval (BSide (~~ bb) (- xb)) (BInfty _ (~~ ba))).

Proof.

by rewrite !itv_boundlr /<=%O /= !implybF if_neg lteifNl andbC.
Qed.

Lemma ( : R) :
(- x \in Interval (BSide ba xa) (BInfty _ bb)) =
(x \in Interval (BInfty _ (~~ bb)) (BSide (~~ ba) (- xa))).

Proof.

by rewrite !itv_boundlr /<=%O /= !implybF if_neg lteifNr negbK andbC.
Qed.

End IntervalNumDomain.

Lemma ( : Type) ( : seq I) ( : {pred I}) ( : I -> nat) ( : I)
    ( : seq I) :
  all (coprime (F a)) [seq F i | <- [seq <- l | P i]] ->
  coprime (F a) (\prod_( <- l | P j) F j).

Proof.

elim: l => /= [_|h t ih]; first by rewrite big_nil coprimen1.
rewrite big_cons; case: ifPn => // Ph.
rewrite map_cons => /= /andP[FaFh FatP].
by rewrite coprimeMr FaFh/= ih.
Qed.

Lemma ( : eqType) ( : seq I) ( : {pred I}) ( : I -> nat)
    ( : nat) :
  pairwise coprime [seq F i | <- [seq <- r | P i]] ->
  reflect (forall , i \in r -> P i -> F i %| n)
          (\prod_( <- r | P i) F i %| n).

Proof.

elim: r => /= [_|a l HI].
  by rewrite big_nil dvd1n; apply: ReflectT => i; rewrite in_nil.
rewrite big_cons; case: ifP => [Pa|nPa]; last first.
  move/HI/equivP; apply; split=> [Fidvdn i|Fidvdn i il].
    by rewrite in_cons => /predU1P[->|]; [rewrite nPa|exact: Fidvdn].
  by apply: Fidvdn; rewrite in_cons il orbT.
rewrite map_cons pairwise_cons => /andP[allcoprimea pairwisecoprime].
rewrite Gauss_dvd; first exact: coprime_prodr.
apply: (equivP (andPP idP (HI pairwisecoprime))).
split=> [[Fadvdn Fidvdn] i|Fidvdn].
  by rewrite in_cons => /predU1P[->//|]; exact: Fidvdn.
split=> [|i il].
  by apply: Fidvdn => //; exact: mem_head.
by apply: Fidvdn; rewrite in_cons il orbT.
Qed.

Lemma ( : eqType) ( : seq I) ( : {pred I}) ( : I -> nat)
( : nat) :
((\prod_( <- r | P i) F i) ^ n = \prod_( <- r | P i) (F i) ^ n)%N.

Proof.

elim: r => [|a l]; first by rewrite !big_nil exp1n.
by rewrite !big_cons; case: ifPn => // Pa <-; rewrite expnMn.
Qed.

Lemma ( : nat) : (n <= x)%N -> (m <= y)%N ->
(\prod_(m <= < y) i * \prod_(n <= < x) i <= \prod_(n + m <= < x + y) i)%N.

Proof.

move=> nx my; rewrite big_addn -addnBA//.
rewrite [in leqRHS]/index_iota -addnBAC// iotaD big_cat/=.
rewrite mulnC leq_mul//.
by apply: leq_prod; move=> i _; rewrite leq_addr.
rewrite subnKC//.
rewrite -[in leqLHS](add0n m) big_addn.
rewrite [in leqRHS](_ : y - m = ((y - m + x) - x))%N.
by rewrite -addnBA// subnn addn0.
rewrite -[X in iota X _](add0n x) big_addn -addnBA// subnn addn0.
by apply: leq_prod => i _; rewrite leq_add2r leq_addr.
Qed.

Lemma ( : nat) : (n <= x) %N -> (m <= y)%N ->
(x`! * y`! * ((n + m).+1)`! <= n`! * m`! * ((x + y).+1)`!)%N.

Proof.

move=> nx my.
rewrite (fact_split nx) -!mulnA leq_mul2l; apply/orP; right.
rewrite (fact_split my) mulnCA -!mulnA leq_mul2l; apply/orP; right.
rewrite [leqRHS](_ : _ =
(n + m).+1`! * \prod_((n + m).+2 <= < (x + y).+2) i)%N.
by rewrite -fact_split// ltnS leq_add.
rewrite mulnA mulnC leq_mul2l; apply/orP; right.
do 2 rewrite -addSn -addnS.
exact: leq_Mprod_prodD.
Qed.

Notation := (ltac:(done)).

Lemma : exists , (2 ^ n <= m.+1 < 2 ^ n.+1)%N.

Proof.

elim: m => [|m [n /andP[h1 h2]]]; first by exists O.
have [m2n|nm2] := ltnP m.+2 (2 ^ n.+1)%N.
by exists n; rewrite m2n andbT (leq_trans h1).
exists n.+1; rewrite nm2/= -addn1.
rewrite -[X in (_ <= X)%N]prednK ?expn_gt0// -[X in (_ <= X)%N]addn1 leq_add2r.
by rewrite (leq_trans h2)// -subn1 leq_subRL ?expn_gt0// add1n ltn_exp2l.
Qed.

Notation := ({homo f : / (n <= m)%O >-> (n <= m)%O})
  (at level 10).
Notation := ({homo f : / (n <= m)%O >-> (n >= m)%O})
  (at level 10).
Notation := ({mono f : / (n <= m)%O >-> (n <= m)%O})
  (at level 10).
Notation := ({mono f : / (n <= m)%O >-> (n >= m)%O})
  (at level 10).
Notation := ({homo f : / (n <= m)%nat >-> (n <= m)%O})
  (at level 10).
Notation := ({homo f : / (n <= m)%nat >-> (n >= m)%O})
  (at level 10).

Definition ( : porderType d) ( : porderType d')
    ( : predType T) ( : pT) ( : T -> T') :=
  {in A &, nondecreasing f} \/ {in A &, {homo f : /~ (x <= y)%O}}.

Definition ( : porderType d) ( : porderType d')
    ( : predType T) ( : pT) ( : T -> T') :=
  {in A &, {homo f : / (x < y)%O}} \/ {in A &, {homo f : /~ (x < y)%O}}.

Lemma ( : orderType d) ( : porderType d')
    ( : predType T) ( : pT) ( : T -> T') :
  strict_monotonic A f -> monotonic A f.

Proof.

by move=> [/le_mono_in/monoW_in|/le_nmono_in/monoW_in]; [left|right].
Qed.

Lemma : {mono f : / (m <= n)%N} -> forall , (n <= f n)%N.

Proof.

move=> fincr; elim=> [//| n HR]; rewrite (leq_ltn_trans HR)//.
by rewrite ltn_neqAle fincr (inj_eq (incn_inj fincr)) -ltn_neqAle.
Qed.

Section path_lt.
Context { : orderType d}.
Implicit Types (a b c : T) (s : seq T).

Lemma ( : pred T) :
P a -> P (last a [seq <- s | P x]).

Proof.

by elim: s a => //= t1 t2 ih a Pa; case: ifPn => //= Pt1; exact: ih.
Qed.

Lemma : path <%O a s -> [seq <- s | (x < a)%O] = [::].

Proof.

move=> /lt_path_min/allP sa; rewrite -(filter_pred0 s).
apply: eq_in_filter => x xs.
by apply/negbTE; have := sa _ xs; rewrite ltNge; apply: contra => /ltW.
Qed.

Lemma : path <%O a s -> [seq <- s | (a < x)%O] = s.

Proof.

move=> /lt_path_min/allP sa; rewrite -[RHS](filter_predT s).
by apply: eq_in_filter => x xs; exact: sa.
Qed.

Lemma : (a < b)%O -> path <%O b s -> path <%O a s.

Proof.

by elim: s b => // h t ih b /= ab /andP[bh ->]; rewrite andbT (lt_trans ab).
Qed.

Lemma :
(a < c)%O -> (c < b)%O -> path <%O a s -> last a s = b ->
last c [seq <- s | (c < x)%O] = b.

Proof.

elim/last_ind : s a b c => /= [|h t ih a b c ac cb].
move=> a b c ac cb _ ab.
by apply/eqP; rewrite eq_le (ltW cb) -ab (ltW ac).
rewrite rcons_path => /andP[ah ht]; rewrite last_rcons => tb.
by rewrite filter_rcons tb cb last_rcons.
Qed.

Lemma : path <%O a s -> (a <= last a s)%O.

Proof.

elim: s a => // a [_ c /andP[/ltW//]|b t ih i/= /and3P[ia ab bt]] /=.
have /= := ih a; rewrite ab bt => /(_ erefl).
by apply: le_trans; exact/ltW.
Qed.

End path_lt.
Arguments last_filterP {d T a} P s.

Inductive := of T.

Reserved Notation "`1- r" (format "`1- r", at level 2).
Reserved Notation "f \^-1" (at level 1, format "f \^-1").

Lemma ( : choiceType) ( : {fset X})
( : X -> nat) : A != fset0 ->
(exists , i \in A /\ forall , j \in A -> f j <= f i)%nat.

Proof.

move=> /fset0Pn[x Ax].
have [/= y _ /(_ _ isT) mf] := @arg_maxnP _ [` Ax]%fset xpredT (f \o val) isT.
exists (val y); split; first exact: valP.
by move=> z Az; have := mf [` Az]%fset.
Qed.

Lemma ( : nat -> nat) :
(exists , i <= n /\ forall , j <= n -> f j <= f i)%N.

Proof.

have [i _ /(_ _ isT) mf] := @arg_maxnP _ (@ord0 n) xpredT f isT.
by exists i; split; rewrite ?leq_ord// => j jn; have := mf (@Ordinal n.+1 j jn).
Qed.

Arguments big_rmcond {R idx op I r} P.
Arguments big_rmcond_in {R idx op I r} P.

Reserved Notation "`1- x" (format "`1- x", at level 2).

Lemma ( : Type) ( : finType) ( : seq I) ( : {pred I})
( : I -> {set T}) :
(#|\bigcup_( <- r | P i) F i| <= \sum_( <- r | P i) #|F i|)%N.

Proof.

elim/big_ind2 : _ => // [|m A n B Am Bn]; first by rewrite cards0.
by rewrite (leq_trans (leq_card_setU _ _))// leq_add.
Qed.

Definition { : pzRingType} ( : R) : R := 1 - r.
#[deprecated(since="mathcomp-analysis 1.15.0")]
Notation := (onem r) : ring_scope.

Reserved Notation "p '.~'" (format "p .~", at level 1).
Notation := (onem p) : ring_scope.

Section onem_ring.
Context { : pzRingType}.
Implicit Type r : R.

Lemma : 0.~ = 1 :> R

Proof.

by rewrite /onem subr0. Qed.

Lemma : 1.~ = 0 :> R

Proof.

by rewrite /onem subrr. Qed.

Lemma : (r.~).~ = r

Proof.

exact: subKr. Qed.

Lemma : r + r.~ = 1

Proof.

by rewrite /onem addrC subrK. Qed.

Lemma : (r + s).~ = r.~ - s.

Proof.

by rewrite /onem opprD addrA. Qed.

Lemma : s * r.~ = s - s * r.

Proof.

by rewrite /onem mulrBr mulr1. Qed.

Lemma : (r * s).~ = r.~ + s.~ - r.~ * s.~.

Proof.

by rewrite /onem mulrBl 2!mulrBr !mul1r mulr1 addrKA opprK subrKA. Qed.

End onem_ring.

Section onem_order.
Variable : numDomainType.
Implicit Types r : R.

Lemma : r < 1 -> 0 < r.~

Proof.

by rewrite subr_gt0. Qed.

Lemma : r <= 1 -> 0 <= r.~.

Proof.

by rewrite le_eqVlt => /predU1P[->|/onem_gt0/ltW]; rewrite ?onem1. Qed.

Lemma : 0 <= r -> r.~ <= 1.

Proof.

by rewrite lerBlDr lerDl. Qed.

Lemma : 0 < r -> r.~ < 1.

Proof.

by rewrite ltrBlDr ltrDl. Qed.

Lemma : 0 <= r -> r <= 1 -> 0 <= (r ^+ n).~.

Proof.

by move=> ? ?; rewrite subr_ge0 exprn_ile1. Qed.

Lemma : 0 < r -> (r ^+ n).~ < 1.

Proof.

by move=> ?; rewrite onem_lt1// exprn_gt0. Qed.

End onem_order.

Lemma { : realDomainType} ( : R) :
(0 <= x <= 1 -> `| x.~ | <= 1)%R.

Proof.

move=> /andP[x0 x1]; rewrite ler_norml; apply/andP; split.
by rewrite lerBrDl lerBlDr (le_trans x1)// lerDl.
by rewrite lerBlDr lerDl.
Qed.

Lemma ( : numFieldType) ( : F) : x != 0 -> x^-1.~ = (x - 1) / x.

Proof.

by move=> ?; rewrite mulrDl divff// mulN1r. Qed.

Lemma ( : realFieldType) ( : R) ( : 0 < s) ( : 0 < t) :
(s / (s + t)).~ = t / (s + t).

Proof.

rewrite /onem.
by rewrite -(@divff _ (s + t)) ?gt_eqF ?addr_gt0// -mulrBl (addrC s) addrK.
Qed.

Lemma ( : int) : 0 <= a -> a <= b -> (`|a| <= `|b|)%N.

Proof.

by case: a => //= n _; case: b. Qed.

Lemma ( : numFieldType) ( : R) :
reflect (forall , z > y -> x <= z) (x <= y).

Proof.

apply: (equivP (ler_addgt0Pr _ _)); split=> [xy z|xz e e_gt0].
by rewrite -subr_gt0 => /xy; rewrite addrC addrNK.
by apply: xz; rewrite -[ltLHS]addr0 ler_ltD.
Qed.

Lemma ( : numFieldType) ( : R) :
reflect (forall , z < x -> z <= y) (x <= y).

Proof.

apply: (equivP (ler_addgt0Pr _ _)); split=> [xy z|xz e e_gt0].
by rewrite -subr_gt0 => /xy; rewrite addrCA -[leLHS]addr0 lerD2l subr_ge0.
by rewrite -lerBlDr xz// -[ltRHS]subr0 ler_ltB.
Qed.

Definition ( : unitRingType) ( : T -> R) := (f x)^-1%R.
Notation := (inv_fun f) : ring_scope.
Arguments inv_fun {T R} _ _ /.

Definition ( : porderType d) ( : bool) ( : itv_bound T) :=
if x is BSide c' _ then c == c' else false.

Lemma [ : numDomainType] [ : R] ( : R) :
x - y \is Num.real -> (`|x - y| < e) = (x - e < y < x + e).

Proof.

by move=> ?; rewrite distrC real_ltr_distl// -rpredN opprB. Qed.

Definition { : Type} ( : T1 * T2) := (x.2, x.1).

Section reassociate_products.
Context { : Type}.

Definition ( : (X * Y) * Z) : X * (Y * Z) :=
(xyz.1.1, (xyz.1.2, xyz.2)).

Definition ( : X * (Y * Z)) : (X * Y) * Z :=
((xyz.1, xyz.2.1), xyz.2.2).

Lemma : cancel prodA prodAr.

Proof.

by case; case. Qed.

Lemma : cancel prodAr prodA.

Proof.

by case => ? []. Qed.

End reassociate_products.

Lemma { : Type} : cancel (@swap T1 T2) (@swap T2 T1).

Proof.

by case=> ? ?. Qed.

Definition { : Type} ( : S -> U) ( : S * S) : (U * U) :=
(f x.1, f x.2).

Section order_min.
Variables ( : Order.disp_t) ( : orderType d).

Lemma ( : T) : (Order.min x z < Order.min y z)%O -> (x < y)%O.

Proof.

rewrite /Order.min/=; case: ifPn => xz; case: ifPn => yz; rewrite ?ltxx//.
- by move=> /lt_le_trans; apply; rewrite leNgt.
- by rewrite ltNge (ltW yz).
Qed.

End order_min.

Section bijection_forall.

Lemma ( : A -> B) ( : B -> Prop) :
bijective f -> (forall , P y) <-> (forall , P (f x)).

Proof.

by case; rewrite /cancel => g _ cangf; split => // => ? y; rewrite -(cangf y).
Qed.

End bijection_forall.

Lemma ( : Type) ( : mem_pred T) ( : T -> Prop) :
{in p, forall , P x /\ Q x} <->
{in p, forall , P x} /\ {in p, forall , 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 ( : porderType d) ( : T) ( : T -> T) :
{in `[a, b] &, {mono f : / (x <= y)%O}} ->
{homo f : / 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 ( : porderType d) ( : T) ( : T -> T) :
{in `[a, b] &, {mono f : /~ (x <= y)%O}} ->
{homo f : / 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 { : Type} { : I -> Type} { : Type}
  ( : forall , X i -> T) ( : { & X i}) : T :=
  (f (projT1 x) (projT2 x)).

Section FsetPartitions.
Variables : 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 ( : Type) ( : R) ( : Monoid.com_law idx).
Let :=
  (\big[op/idx]_( <- P) \big[op/idx]_( <- A | K x) E x)%fset.
Let := (\big[op/idx]_( <- P) \big[op/idx]_( <- A) E x)%fset.

Lemma ( : T -> R) ( : I -> {fset T})
  ( : {fset I}) :
  (forall , i \in K -> j \in K -> i != j -> [disjoint F i & F j])%fset ->
  \big[op/idx]_( <- \big[fsetU/fset0]_( <- K) (F x)) f i =
  \big[op/idx]_( <- K) (\big[op/idx]_( <- F k) f i).

Proof.

move=> disjF; pose P := [fset F 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_( <- 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|] /=.
  move: iK; rewrite !inE/= => /andP[iK Fi0].
  by apply: contraNeq (disjF _ _ iK jK) _; rewrite -fsetI_eq0 eqFij fsetIid.
rewrite big_filter big_mkcond; apply eq_bigr => i _.
by case: ifPn => // /negPn /eqP ->;  rewrite big_seq_fset0.
Qed.

End FsetPartitions.

Lemma { : realDomainType} ( : seq R) :
(forall , x \in s -> 0 <= x <= 1)%R -> (\prod_( <- 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.

Lemma ( : seq T) : (size (filter P r) > 0)%N = (has P r).

Proof.

by elim: r => //= x r; case: ifP. Qed.

Lemma [ : numDomainType] [ : Type] ( : seq I)
    [ : pred I] [ : I -> R] :
  has P r ->
  (forall : I, P i -> F i < G i) ->
  \sum_( <- r | P i) F i < \sum_( <- 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 [ : numDomainType] [ : nat] [ : nat -> R] :
(m < n)%N -> (forall : nat, (m <= i < n)%N -> F i < G i) ->
\sum_(m <= < n) F i < \sum_(m <= < 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 ( : Type) ( : A -> Prop) :
(forall , P x <-> P' x) ->
(exists2 , P x & Q x) <-> (exists2 , P' x & Q x).

Proof.

by move=> eqQ; split=> -[x p q]; exists x; move: p q; rewrite ?eqQ.
Qed.

Lemma ( : Type) ( : A -> Prop) :
(forall , Q x <-> Q' x) ->
(exists2 , P x & Q x) <-> (exists2 , 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 .

Notation := (@respectful _ _ (R%signature) (R'%signature))
  (right associativity, at level 55) : signature_scope.

Notation := (@respectful _ _ (R%signature) (R'%signature))
  (right associativity, at level 55) : signature_scope.

Notation := (@respectful _ _ (Program.Basics.flip (R%signature)) (R'%signature))
  (right associativity, at level 55) : signature_scope.

Export -(notations) Morphisms.
End ProperNotations.

Lemma { : rcfType} : {in Num.nneg, cancel (@Num.sqrt K) (fun => x ^+ 2)}.

Proof.

by move=> r r0; rewrite sqr_sqrtr. Qed.

Lemma { : archiNumDomainType} ( : R) : `|x| < (Num.bound x)%:R.

Proof.

by rewrite /Num.bound -[in ltRHS]normr_id archi_boundP. Qed.

Lemma { : archiNumDomainType} ( : R) :
x \is Num.real -> x < (Num.bound x)%:R.

Proof.

by move=> /real_ler_norm /le_lt_trans -> //; apply: ltr_norm_bound. Qed.

Lemma { : archiNumDomainType} ( : R) :
x \is Num.real -> - x < (Num.bound x)%:R.

Proof.

by rewrite /Num.bound -realN -normrN; exact: real_ltr_bound. Qed.

Lemma { : archiRealDomainType} ( : R) : x < (Num.bound x)%:R.

Proof.

exact: real_ltr_bound. Qed.

Lemma { : archiRealDomainType} ( : R) : - x < (Num.bound x)%:R.

Proof.

exact: real_ltrNbound. Qed.

Module .

. () (L : lmodType K) (norm : L -> K) := {
  norm0 : norm 0 = 0 ;
  norm_ge0 : forall , 0 <= norm x ;
  ler_normD : forall , norm (x + y) <= norm x + norm y ;
  normZ : forall , norm (r *: x) = `|r| * norm x
}.

. of @isSemiNorm K L norm }.

. () (L : lmodType K)
  (norm : L -> K) := { norm0_eq0 : forall , norm x = 0 -> x = 0 }.

.
  { of @SemiNorm_isNorm K L norm & @SemiNorm K L norm }.

Module Import .
Section Theory.
Variables ( : numDomainType) ( : lmodType K) ( : SemiNorm.type L).

Lemma : norm (x *+ n) = norm x *+ n.

Proof.

by rewrite -scaler_nat normZ normr_nat mulr_natl. Qed.

Lemma : norm (- x) = norm x.

Proof.

by rewrite -scaleN1r normZ normrN1 mul1r. Qed.

Lemma ( : Type) ( : seq I) ( : I -> L) :
norm (\sum_( <- r) F i) <= \sum_( <- r) norm (F i).

Proof.

by elim/big_ind2 : _ => *; rewrite ?norm0// (le_trans (ler_normD _ _))// lerD.
Qed.

End Theory.

Section realTheory.
Variables ( : realDomainType) ( : lmodType K) ( : SemiNorm.type L).

Lemma : `|norm x - norm y| <= norm (x - y).

Proof.

have [pxy | pyx] := leP (norm x) (norm y).
  rewrite ler0_norm ?subr_le0 // opprB.
  rewrite lerBlDl; rewrite  -(@normN _ _ norm (x-y)) opprB.
  by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK.
rewrite gtr0_norm ?subr_gt0 // lerBlDl.
by rewrite (le_trans _ (ler_normD _ _ )) // addrC subrK.
Qed.

End realTheory.
End Theory.

Module Import . HB.reexport. End Exports.
End Norm.
Export Norm.Exports.

From mathcomp Require Import interval_inference.
Module .
Section max_nng_comlaw.
Import Num.Def.
Context { : realFieldType}.

Let : left_id ((0 : K)%:nng) (@maxr {nonneg K}).

Proof.

move=> x; rewrite /maxr; case: ifPn => //.
rewrite -leNgt => x0.
apply/eqP; rewrite eq_le x0 andbT.
(* NB: the goal is `widen_itv 0%:itv <= x`, which does not match the syntax to
trigger the hint for `ge0` as can be seen at
https://github.com/math-comp/math-comp/blob/900e37912dbecbd3c04d3c1b320efe721d3f56dd/algebra/interval_inference.v#L770 *)
by rewrite -num_le/=.
Qed.

.
Monoid.isComLaw.Build {nonneg K} 0%:nng maxr maxA maxC nng_max0r.

End max_nng_comlaw.
End MaxNngComLaw.

Module .
Section ProdNormedZmodule.
Context { : numDomainType} { : normedZmodType R}.

Definition ( : U * V) : R := Num.max `|x.1| `|x.2|.

Lemma : norm (x + y) <= norm x + norm y.

Proof.

rewrite /norm num_ge_max !(le_trans (ler_normD _ _)) ?lerD//;
by rewrite comparable_le_max ?lexx ?orbT// real_comparable.
Qed.

Lemma : norm x = 0 -> x = 0.

Proof.

case: x => x1 x2 /eqP; rewrite eq_le num_ge_max 2!normr_le0 -andbA/=.
by case/and3P => /eqP -> /eqP ->.
Qed.

Lemma : norm (x *+ n) = (norm x) *+ n.

Proof.

by rewrite /norm pairMnE -mulr_natl maxr_pMr ?mulr_natl ?normrMn. Qed.

Lemma : norm (- x) = norm x.

Proof.

by rewrite /norm/= !normrN. Qed.

..Zmodule_isNormed.Build R (U * V)%type
normD norm_eq0 normMn normrN.

Lemma ( : U * V) : `|x| = Num.max `|x.1| `|x.2|.

Proof.

by []. Qed.

End ProdNormedZmodule.

Module .
HB.reexport.
Definition := @prod_normE.
End Exports.

End ProdNormedZmodule.
Export ProdNormedZmodule.Exports.

Section interval.
Local Open Scope order_scope.
Context {} { : porderType disp}.
Implicit Types (x : T) (bl br : itv_bound T).

Lemma : x \in Interval bl br -> bl < br.

Proof.

rewrite itv_boundlr => /andP[] lx.
by apply/lt_le_trans/(le_lt_trans lx); rewrite bnd_simp.
Qed.

End interval.

Module .
Local Open Scope order_scope.

Definition {} ( : porderType d) :=
  forall : T, (exists , y < x) /\ (exists , x < y).

Definition {} ( : porderType d) :=
  forall : T, x < y -> exists , x < z < y.

Section endless_dense_porderType.
Context {} { : porderType d}.
Implicit Type i j : itv_bound T.

Let ( : T) :
  is_dense T ->
  BSide bl L < BSide br R ->
  exists , BSide bl L <= BLeft y < BSide br R.

Proof.

move=> T_dense.
case: bl; case: br; rewrite !bnd_simp.
- by exists L; rewrite !bnd_simp.
- by exists R; rewrite !bnd_simp andbT.
- by case/T_dense => y ?; exists y; rewrite !bnd_simp.
- by exists R; rewrite !bnd_simp andbT.
Qed.

Let ( : T) :
  is_endless T ->
  BInfty _ bl < j ->
  exists , BInfty _ bl <= BLeft y < j.

Proof.

move=> T_endless.
case: bl; case: j => [[] J | []//]; rewrite !bnd_simp//.
- by have [[y ?] _] := T_endless J; exists y; rewrite !bnd_simp.
- by exists J; rewrite !bnd_simp.
- by exists x; rewrite !bnd_simp.
Qed.

Let ( : T) :
  is_endless T ->
  i < BInfty _ br ->
  exists , i <= BLeft y < BInfty _ br.

Proof.

move=> T_endless.
case: br; case: i => [[] I | []//]; rewrite !bnd_simp//.
- by exists I; rewrite !bnd_simp.
- by have [_ [y ?]] := T_endless I; exists y; rewrite !bnd_simp andbT.
- by exists x; rewrite !bnd_simp.
Qed.

Lemma ( : T) :
  is_endless T ->
  is_dense T ->
  i < j -> exists , i <= BLeft y < j.

Proof.

move=> T_endless T_dense.
case: i => [? ? | ?]; case j => [? ? | ?].
- exact: fin_itv_bound_half_dense.
- exact: rinfty_itv_bound_half_dense.
- exact: linfty_itv_bound_half_dense.
- exact: linfty_itv_bound_half_dense.
Qed.

End endless_dense_porderType.

Local Lemma {} { : orderType d} ( : interval T) :
  is_endless T ->
  is_dense T ->
  x \in i -> {subset i <= j} -> j.1 <= i.1.

Proof.

case: i => il ir; case: j => jl jr /=.
move=> T_endless T_dense xi isubj.
have := xi; rewrite itv_boundlr => /andP[] _ xir.
have := isubj _ xi; rewrite itv_boundlr => /andP[] jlx _.
rewrite leNgt; apply/negP => /itv_bound_half_dense [] // y /andP[ily yjl].
suff/isubj : y \in Interval il ir by rewrite itv_boundlr leNgt yjl.
rewrite itv_boundlr ily/= (le_trans _ xir)// ltW//.
by have:= lt_le_trans yjl jlx; rewrite !bnd_simp.
Qed.

Definition {} { : porderType d} ( : itv_bound T) :
  itv_bound T^d :=
  match ib with
  | BInfty b => BInfty _ (~~ b)
  | BSide b x => BSide (~~ b) x
  end.

Definition {} { : porderType d} ( : interval T) : interval T^d :=
  @Interval T^d (dual_itv_bound i.2) (dual_itv_bound i.1).

Section dual_porderType.
Context {} { : porderType d}.
Implicit Types i j : interval T.

Lemma : dual_itv i =i i.

Proof.

case: i => l r; move=> p; rewrite /dual_itv /dual_itv_bound.
case: l => [[] x | []]; case: r => [[] y | []]//=.
all: rewrite /= !in_itv/= !(@in_itv d T)/= ?ltEdual ?leEdual.
all: by rewrite ?andbT// ?andbF// andbC.
Qed.

Lemma :
{subset i <= j} <-> {subset dual_itv i <= dual_itv j}.

Proof.

by split => + x => /(_ x); rewrite !dual_itvE. Qed.

Lemma : is_dense T -> is_dense T^d.

Proof.

move=> + x y xy /= => /(_ y x xy) [] z yzx.
by exists z; rewrite !ltEdual andbC.
Qed.

Lemma : is_endless T -> is_endless T^d.

Proof.

move=> + x => /(_ x) [[y yx] [z xz]]; split.
by exists z; rewrite ltEdual.
by exists y; rewrite ltEdual.
Qed.

Lemma ( : itv_bound T) :
dual_itv_bound (dual_itv_bound ib) = ib.

Proof.

by case: ib => [[]?|[]]. Qed.

Lemma ( : itv_bound T) :
(dual_itv_bound l < dual_itv_bound r) = (r < l).

Proof.

by case: l => [[]?|[]]; case: r => [[]?|[]]. Qed.

Lemma ( : itv_bound T) :
(dual_itv_bound l <= dual_itv_bound r) = (r <= l).

Proof.

by case: l => [[]?|[]]; case: r => [[]?|[]]. Qed.

End dual_porderType.

Section endless_dense_orderType.
Context {} { : orderType d}.

Let ( : interval T) :
  is_endless T ->
  is_dense T ->
  x \in i -> {subset i <= j} -> i.2 <= j.2.

Proof.

case: i => il ir; case: j => jl jr.
move=> /dual_is_endless T_endless /dual_is_dense T_dense.
rewrite -dual_itvE => xi /dual_itv_sub_memP isubj.
have := @subitvP_half1 _ T^d.
move/(_ (dual_itv (Interval il ir)) (dual_itv (Interval jl jr)) x).
move/(_ T_endless T_dense xi isubj).
by rewrite dual_itv_bound_le.
Qed.

Lemma ( : interval T) :
  is_endless T ->
  is_dense T ->
  x \in i ->
  i <= j <-> {subset i <= j}.

Proof.

case: i => ? ?; case: j => ? ?.
move=> *; split; first exact: subitvP.
move=> isubj; apply/andP; split.
- by move/(@subitvP_half1 _ _ _ _ x): isubj; exact.
- by move/(@subitvP_half2 _ _ x): isubj; exact.
Qed.

End endless_dense_orderType.

Section num.
Local Open Scope ring_scope.

Lemma ( : numDomainType) : is_endless R.

Proof.

move=> x; split.
- by exists (x - 1); rewrite gtrBl.
- by exists (x + 1); rewrite ltrDl.
Qed.

Lemma ( : numFieldType) : is_dense R.

Proof.

move=> x y xy; exists (2^-1 * (x + y)).
rewrite -(@ltr_pM2l _ 2)// -[X in _ && X](@ltr_pM2l _ 2)//.
rewrite mulrA divff ?lt0r_neq0// mul1r !mulr_natl !mulr2n.
by rewrite ltrD2l ltrD2r xy.
Qed.

End num.

End EndlessDense.

Section interval_realFieldType.
Context { : realFieldType}.
Local Open Scope order_scope.

Lemma ( : interval R) : x \in i -> i <= j <-> {subset i <= j}.

Proof.

apply: EndlessDense.subitvP.
- exact: EndlessDense.numDomain_is_endless.
- exact: EndlessDense.numField_is_dense.
Qed.

End interval_realFieldType.

Files

Module mathcomp.classical.unstable