Module mathcomp.reals_stdlib.Rstruct

From Stdlib Require Import ZArith Rdefinitions Raxioms RIneq Rbasic_fun Zwf.
From Stdlib Require Import Epsilon FunctionalExtensionality Ranalysis1 Rsqrt_def.
From Stdlib Require Import Rtrigo1 Reals.
From HB Require Import structures.
From mathcomp Require Import boot order ssralg poly ssrnum archimedean.

# Compatibility with the real numbers of Stdlib This essentially builds an instance of realType for the R type from the Stdlib library. This enables specializing all proofs on realType (that is, many things in the Analysis library) to Stdlib's real numbers. To this end, one can use tactics like `apply: RleP` or `rewrite !RealsE` (see below for more compatibility lemmas).

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Theory.

Local Open Scope R_scope.

Lemma ( : R) : {r1 = r2} + {r1 <> r2}.

Proof.

case: (total_order_T r1 r2) => [[r1Lr2 | <-] | r1Gr2].
- by right=> r1Er2; case: (Rlt_irrefl r1); rewrite {2}r1Er2.
- by left.
by right=> r1Er2; case: (Rlt_irrefl r1); rewrite {1}r1Er2.
Qed.

Definition ( : R) : bool :=
if Req_EM_T r1 r2 is left _ then true else false.

Lemma : Equality.axiom eqr.

Proof.

by move=> r1 r2; rewrite /eqr; case: Req_EM_T=> H; apply: (iffP idP).
Qed.

..Build R eqrP.

Fact : inhabited R.

Proof.

exact: (inhabits 0). Qed.

Definition ( : pred R) ( : nat) :=
let := epsilon inhR P in if P x then Some x else None.

Fact : pickR P n = Some x -> P x.

Proof.

by rewrite /pickR; case: (boolP (P _)) => // Px [<-]. Qed.

Fact ( : pred R) :
(exists : R, P x) -> exists , pickR P n.

Proof.

by rewrite /pickR; move=> /(epsilon_spec inhR)->; exists 0%N. Qed.

Fact ( : pred R) : P =1 Q -> pickR P =1 pickR Q.

Proof.

move=> PEQ n; rewrite /pickR; set u := epsilon _ _; set v := epsilon _ _.
suff->: u = v by rewrite PEQ.
by congr epsilon; apply: functional_extensionality=> x; rewrite PEQ.
Qed.

..Build R pickR_some pickR_ex pickR_ext.

Fact : associative (Rplus).

Proof.

by move=> *; rewrite Rplus_assoc. Qed.

..isZmodule.Build R
RplusA Rplus_comm Rplus_0_l Rplus_opp_l.

Fact : associative Rmult.

Proof.

by move=> *; rewrite Rmult_assoc. Qed.

Fact : R1 != R0.

Proof.

by apply/eqP/R1_neq_R0. Qed.

..Zmodule_isNzRing.Build R
  RmultA Rmult_1_l Rmult_1_r Rmult_plus_distr_r Rmult_plus_distr_l R1_neq_0.

..SemiRing_hasCommutativeMul.Build R Rmult_comm.

Import Monoid.

..Build R 0 Rplus
  RplusA Rplus_comm Rplus_0_l.

..Build R 1 Rmult
  RmultA Rmult_comm Rmult_1_l.

..Build R 0 Rmult Rmult_0_l Rmult_0_r.
..Build R Rmult Rplus
  Rmult_plus_distr_r Rmult_plus_distr_l.

Definition := r != 0.

Lemma : y * x = 1 /\ x * y = 1 -> unit_R x.

Proof.

move=> [yx_eq1 _]; apply: contra_eqN yx_eq1 => /eqP->.
by rewrite Rmult_0_r eq_sym R1_neq_0.
Qed.

Section Rinvx.

Let := if r != 0 then / r else r.

Let : x != 0 -> Rinv x = Rinvx x.

Proof.

by move=> x_neq0; rewrite -[RHS]/(if _ then _ else _) x_neq0. Qed.

Let : Rinv x = Rinvx x.

Proof.

have [->| ] := eqVneq x R0; last exact: neq0_RinvxE.
rewrite /GRing.inv /GRing.mul /= /Rinvx eqxx /=.
rewrite RinvImpl.Rinv_def; case: Req_appart_dec => //.
by move=> /[dup] -[] /Rlt_irrefl.
Qed.

Lemma : {in unit_R, left_inverse 1 Rinv Rmult}.

Proof.

move=> r; rewrite RinvxE -topredE /unit_R /Rinvx => /= rNZ /=.
by rewrite rNZ Rinv_l //; apply/eqP.
Qed.

Lemma : {in unit_R, right_inverse 1 Rinv Rmult}.

Proof.

move=> r; rewrite RinvxE -topredE /unit_R /Rinvx => /= rNZ /=.
by rewrite rNZ Rinv_r //; apply/eqP.
Qed.

Lemma : {in predC unit_R, Rinv =1 id}.

Proof.

by move=> x; rewrite inE/= RinvxE /Rinvx -if_neg => ->. Qed.

End Rinvx.

#[deprecated(since="mathcomp-analysis 1.9.0", note="To be removed. Use GRing.inv instead.")]
Definition := Rinv.

..NzRing_hasMulInverse.Build R
RmultRinv RinvRmult intro_unit_R Rinv_out.

Lemma : x * y = 0 -> (x == 0) || (y == 0).

Proof.

by move=> /Rmult_integral []->; rewrite eqxx ?orbT. Qed.

..ComUnitRing_isIntegral.Build R
R_idomainMixin.

Lemma : GRing.field_axiom R

Proof.

by []. Qed.

..UnitRing_isField.Build R R_fieldMixin.

Reflect the order on the reals to bool

Definition := if Rle_dec r1 r2 is left _ then true else false.
Definition := Rleb r1 r2 && (r1 != r2).
Definition := Rleb r2 r1.
Definition := Rltb r2 r1.

Lemma : reflect (r1 <= r2) (Rleb r1 r2).

Proof.

by rewrite /Rleb; apply: (iffP idP); case: Rle_dec. Qed.

Lemma : reflect (r1 < r2) (Rltb r1 r2).

Proof.

rewrite /Rltb /Rleb; apply: (iffP idP); case: Rle_dec=> //=.
- by case=> // r1Er2 /eqP[].
- by move=> _ r1Lr2; apply/eqP/Rlt_not_eq.
by move=> Nr1Lr2 r1Lr2; case: Nr1Lr2; left.
Qed.

Section ssreal_struct.

Local Open Scope R_scope.

Lemma : Rleb (Rabs (x + y)) (Rabs x + Rabs y).

Proof.

by apply/RlebP/Rabs_triang. Qed.

Lemma : Rltb 0 x -> Rltb 0 y -> Rltb 0 (x + y).

Proof.

by move/RltbP=> Hx /RltbP Hy; apply/RltbP/Rplus_lt_0_compat. Qed.

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

Proof.

by move=> H; case: (x == 0) /eqP=> // /Rabs_no_R0. Qed.

Lemma : Rleb 0 x -> Rleb 0 y -> (Rleb x y) || (Rleb y x).

Proof.

move/RlebP=> Hx /RlebP Hy; case: (Rlt_le_dec x y).
by move/Rlt_le/RlebP=> ->.
by move/RlebP=> ->; rewrite orbT.
Qed.

Lemma : {morph Rabs : / x * y}.

Proof.

exact: Rabs_mult. Qed.

Lemma : (Rleb x y) = (Rabs (y - x) == y - x).

Proof.

apply/(sameP (RlebP x y))/(iffP idP)=> [/eqP H| /Rle_minus H].
  apply: Rminus_le; rewrite -Ropp_minus_distr.
  apply/Rge_le/Ropp_0_le_ge_contravar.
  by rewrite -H; apply: Rabs_pos.
apply/eqP/Rabs_pos_eq.
rewrite -Ropp_minus_distr.
by apply/Ropp_0_ge_le_contravar/Rle_ge.
Qed.

Lemma : (Rltb x y) = (y != x) && (Rleb x y).

Proof.

apply/(sameP (RltbP x y))/(iffP idP).
  case/andP=> /eqP H /RlebP/Rle_not_gt H2.
  by case: (Rtotal_order x y)=> // [][] // /esym.
move=> H; apply/andP; split; [apply/eqP|apply/RlebP].
  exact: Rgt_not_eq.
exact: Rlt_le.
Qed.

..IntegralDomain_isNumRing.Build R
Rleb_norm_add addr_Rgtb0 Rnorm0_eq0 Rleb_leVge RnormM Rleb_def Rltb_def.

Lemma : forall , reflect (Rle x y) (x <= y)%R.

Proof.

exact: RlebP. Qed.

Lemma : forall , reflect (Rlt x y) (x < y)%R.

Proof.

exact: RltbP. Qed.

Lemma ( : R) : (0 <= x)%R || (x <= 0)%R.

Proof.

case: (Rle_dec 0 x)=> [/RleP ->|] //.
by move/Rnot_le_lt/Rlt_le/RleP=> ->; rewrite orbT.
Qed.

Lemma : total (<=%O : rel R).

Proof.

move=> x y; case: (Rle_lt_dec x y) => [/RleP -> //|/Rlt_le/RleP ->];
by rewrite orbT.
Qed.

..POrder_isTotal.Build _ R R_total.

Lemma : Num.archimedean_axiom R.

Proof.

move=> x; exists (Z.abs_nat (up x) + 2)%N.
have [Hx1 Hx2] := archimed x.
have Hz ( : Z) : z = (z - 1 + 1)%Z by rewrite Zplus_comm Zplus_minus.
have Zabs_nat_Zopp z : Z.abs_nat (- z)%Z = Z.abs_nat z by case: z.
apply/RltbP/Rabs_def1.
  apply: (Rlt_trans _ ((Z.abs_nat (up x))%:R)%R); last first.
    rewrite -[((Z.abs_nat _)%:R)%R]Rplus_0_r mulrnDr.
    by apply/Rplus_lt_compat_l/Rlt_0_2.
  apply: (Rlt_le_trans _ (IZR (up x)))=> //.
  elim/(well_founded_ind (Zwf_well_founded 0)): (up x) => z IHz.
  case: (Z_lt_le_dec 0 z) => [zp | zn].
    rewrite [z]Hz plus_IZR Zabs_nat_Zplus //; first exact: Zlt_0_le_0_pred.
    rewrite plusE mulrnDr.
    apply/Rplus_le_compat_r/IHz; split; first exact: Zlt_le_weak.
    exact: Zlt_pred.
  apply: (Rle_trans _ (IZR 0)); first exact: IZR_le.
  by apply/RlebP/(ler0n R (Z.abs_nat z)).
apply: (Rlt_le_trans _ (IZR (up x) - 1)).
  apply: Ropp_lt_cancel; rewrite Ropp_involutive.
  rewrite Ropp_minus_distr /Rminus -opp_IZR -{2}(Z.opp_involutive (up x)).
  elim/(well_founded_ind (Zwf_well_founded 0)): (- up x)%Z => z IHz .
  case: (Z_lt_le_dec 0 z) => [zp | zn].
  rewrite [z]Hz Zabs_nat_Zopp plus_IZR.
  rewrite Zabs_nat_Zplus //; first exact: Zlt_0_le_0_pred.
    rewrite plusE -Rplus_assoc -addnA [(_ + 2)%N]addnC addnA mulrnDr.
    apply: Rplus_lt_compat_r; rewrite -Zabs_nat_Zopp.
    apply: IHz; split; first exact: Zlt_le_weak.
    exact: Zlt_pred.
  apply: (Rle_lt_trans _ 1).
    rewrite -{2}[1]Rplus_0_r; apply: Rplus_le_compat_l.
    by rewrite -/(IZR 0); apply: IZR_le.
  rewrite mulrnDr; apply: (Rlt_le_trans _ 2).
    by rewrite -{1}[1]Rplus_0_r; apply/Rplus_lt_compat_l/Rlt_0_1.
  rewrite -[2]Rplus_0_l; apply: Rplus_le_compat_r.
  by apply/RlebP/(ler0n R (Z.abs_nat _)).
apply: Rminus_le.
rewrite /Rminus Rplus_assoc [- _ + _]Rplus_comm -Rplus_assoc -!/(Rminus _ _).
exact: Rle_minus.
Qed.

..NumDomain_bounded_isArchimedean.Build R
Rarchimedean_axiom.

Here are the lemmas that we will use to prove that R has the rcfType structure.

Lemma : f =1 g -> continuity f -> continuity g.

Proof.

move=> Hfg Hf x eps Heps.
have [y [Hy1 Hy2]]:= Hf x eps Heps.
by exists y; split=> // z; rewrite -!Hfg; exact: Hy2.
Qed.

Lemma ( : finType) ( : pred I) :
(forall , P i -> continuity (F i)) ->
continuity (fun => (\sum_( | P i) ((F i) x)))%R.

Proof.

move=> H; elim: (index_enum I)=> [|a l IHl].
  set f:= fun _ => _.
  have Hf: (fun => 0) =1 f by move=> x; rewrite /f big_nil.
  by apply: (continuity_eq Hf); exact: continuity_const.
set f := fun _ => _.
case Hpa: (P a).
  have Hf: (fun => F a x + \sum_( <- l | P i) F i x)%R =1 f.
    by move=> x; rewrite /f big_cons Hpa.
  apply: (continuity_eq Hf); apply: continuity_plus=> //.
  exact: H.
have Hf: (fun => \sum_( <- l | P i) F i x)%R =1 f.
  by move=> x; rewrite /f big_cons Hpa.
exact: (continuity_eq Hf).
Qed.

Lemma : continuity f -> continuity (fun => (f x)^+ n)%R.

Proof.

move=> Hf; elim: n=> [|n IHn]; first exact: continuity_const.
set g:= fun _ => _.
have Hg: (fun => f x * f x ^+ n)%R =1 g.
by move=> x; rewrite /g exprS.
by apply: (continuity_eq Hg); exact: continuity_mult.
Qed.

Lemma : Num.real_closed_axiom R.

Proof.

move=> p a b; rewrite !le_eqVlt.
case Hpa: ((p.[a])%R == 0%R).
  by move=> ? _ ; exists a=> //; rewrite lexx le_eqVlt.
case Hpb: ((p.[b])%R == 0%R).
  by move=> ? _; exists b=> //; rewrite lexx le_eqVlt andbT.
have [->|Hab] := eqVneq a b.
  by move=> _; rewrite eq_sym Hpb (ltNge 0) /=; case/andP=> /ltW ->.
rewrite eq_sym Hpb /=; clear=> /RltbP Hab /andP[/RltbP Hpa /RltbP Hpb].
suff Hcp : continuity (fun => (p.[x])%R).
  have [z [[Hza Hzb] /eqP Hz2]]:= IVT _ a b Hcp Hab Hpa Hpb.
  by exists z=> //; apply/andP; split; apply/RlebP.
rewrite -[p]coefK poly_def.
set f := fun _ => _.
have Hf: (fun : R => \sum_( < size p) (p`_i * x^+i))%R =1 f.
  move=> x; rewrite /f horner_sum.
  by apply: eq_bigr=> i _; rewrite hornerZ hornerXn.
apply: (continuity_eq Hf); apply: continuity_sum=> i _.
apply:continuity_scal; apply: continuity_exp=> x esp Hesp.
by exists esp; split=> // y [].
Qed.

..RealField_isClosed.Build R Rreal_closed_axiom.

End ssreal_struct.
Arguments RleP {x y}.
Arguments RltP {x y}.

Local Open Scope ring_scope.
From mathcomp Require Import boolp classical_sets.
From mathcomp Require Import reals.

Section ssreal_struct_contd.
Implicit Type E : set R.

Lemma : is_upper_bound E x = (ubound E) x.

Proof.

rewrite propeqE; split; [move=> h|move=> /ubP h y Ey; exact/RleP/h].
by apply/ubP => y Ey; apply/RleP/h.
Qed.

Lemma : bound E = has_ubound E.

Proof.

by apply/eq_exists=> x; rewrite is_upper_boundE. Qed.

Lemma : has_sup E -> { | isLub E m}.

Proof.

move=> [E0 uE]; have := completeness E; rewrite boundE => /(_ uE E0)[x [E1 E2]].
exists x; split; first by rewrite -is_upper_boundE; apply: E1.
by move=> y; rewrite -is_upper_boundE => /E2/RleP.
Qed.

Lemma : has_sup E -> (supremums E !=set0)%classic.

Proof.

by move=> /Rcondcomplete[x [? ?]]; exists x. Qed.

Lemma : has_sup E -> isLub E (supremum x0 E).

Proof.

have [-> [/set0P]|E0 hsE] := eqVneq E set0; first by rewrite eqxx.
have [s [Es sE]] := Rcondcomplete hsE.
split => x Ex; first by apply/ge_supremum_Nmem=> //; exact: Rsupremums_neq0.
rewrite /supremum (negbTE E0); case: xgetP => /=.
by move=> _ -> [_ EsE]; apply/EsE.
by have [y Ey /(_ y)] := Rsupremums_neq0 hsE.
Qed.

Lemma ( : R) : 0 < eps ->
has_sup E -> exists2 , E e & (supremum x0 E - eps) < e.

Proof.

move=> eps_gt0 supE; set m := _ - eps; apply: contrapT=> mNsmall.
have : (ubound E) m.
apply/ubP => y Ey.
by have /negP := mNsmall (ex_intro2 _ _ y Ey _); rewrite -leNgt.
have [_ /(_ m)] := Rsup_isLub x0 supE.
move => m_big /m_big.
by rewrite -subr_ge0 addrC addKr oppr_ge0 leNgt eps_gt0.
Qed.

Lemma : has_sup E -> (ubound E) (supremum x0 E).

Proof.

by move=> supE x Ex; apply/ge_supremum_Nmem => //; exact: Rsupremums_neq0.
Qed.

..Build R
(@Rsup_ub (0 : R)) (real_sup_adherent 0).

Implicit Types (x y : R) (m n : nat).

Lemma : exp (0 : R) = 1.

Proof.

by rewrite exp_0. Qed.

Lemma : exp x * exp y = exp (x + y).

Proof.

by rewrite exp_plus. Qed.

Lemma : exp x ^+ n = exp (x *+ n).

Proof.

elim: n => [|n Ihn]; first by rewrite expr0 mulr0n exp_0.
by rewrite exprS Ihn mulrS expRD.
Qed.

Lemma : sin (x + y) = sin x * cos y + cos x * sin y.

Proof.

by rewrite sin_plus. Qed.

Lemma : cos (x + y) = (cos x * cos y - sin x * sin y).

Proof.

by rewrite cos_plus. Qed.

Lemma : Rplus x y = x + y

Proof.

by []. Qed.

Lemma : Rminus x y = x - y

Proof.

by []. Qed.

Lemma : Rmult x y = x * y

Proof.

by []. Qed.

Lemma : Ropp x = - x

Proof.

by []. Qed.

Lemma : Rinv x = x^-1

Proof.

by []. Qed.

Lemma : Rdiv x y = x / y

Proof.

by rewrite /Rdiv. Qed.

Lemma : INR n = n%:R.

Proof.

elim: n => // n IH; by rewrite S_INR IH RplusE -addn1 natrD. Qed.

Lemma : Pos.to_nat p = nat_of_pos p.

Proof.

by elim: p => //= p <-;
rewrite ?(Pnat.Pos2Nat.inj_xI,Pnat.Pos2Nat.inj_xO) NatTrec.doubleE -mul2n.
Qed.

Lemma : IZR 0 = 0%R

Proof.

by []. Qed.

Lemma : IZR 1 = 1%R

Proof.

by []. Qed.

Note that rewrites using the following lemma `IZRposE` are systematically followed by a rewrite using the lemma `INRE`.

Lemma ( : positive) : IZR (Z.pos p) = INR (nat_of_pos p).

Proof.

by rewrite -Pos_to_natE INR_IPR. Qed.

Let : 0 <= x -> sqrt x = Num.sqrt x.

Proof.

move => x0; apply/eqP; have [t1 t2] := conj (sqrtr_ge0 x) (sqrt_pos x).
rewrite eq_sym -(eqrXn2 (_: 0 < 2)%N t1) //; first exact/RleP.
by rewrite sqr_sqrtr // !exprS expr0 mulr1 -RmultE ?sqrt_sqrt //; exact/RleP.
Qed.

Lemma : sqrt x = Num.sqrt x.

Proof.

set Rx := Rbasic_fun.Rcase_abs x.
have RxE : Rx = Rbasic_fun.Rcase_abs x by [].
rewrite /R_sqrt.sqrt -RxE.
move: RxE; case: Rbasic_fun.Rcase_abs => x0 RxE.
by rewrite RxE ler0_sqrtr//; exact/ltW/RltP.
by rewrite /Rx -/(R_sqrt.sqrt _) ge0_RsqrtE //; exact/RleP/Rge_le.
Qed.

Lemma : pow x n = x ^+ n.

Proof.

by elim: n => [ | n In] //=; rewrite exprS In RmultE. Qed.

Lemma : Rmax x y = Num.max x y.

Proof.

case: (lerP x y) => H; first by rewrite Rmax_right //; apply: RlebP.
by rewrite ?ltW // Rmax_left //; apply/RlebP; move/ltW : H.
Qed.

Lemma : Rmin x y = Num.min x y.

Proof.

case: (lerP x y) => H; first by rewrite Rmin_left //; apply: RlebP.
by rewrite ?ltW // Rmin_right //; apply/RlebP; move/ltW : H.
Qed.

Lemma : Rabs x = `|x|.

Proof.

by rewrite /Rabs; case: Rcase_abs => [/RltP x0|/Rge_le/RleP x0];
[rewrite ltr0_norm|rewrite ger0_norm].
Qed.

Lemma : Rdist x y = `|x - y|.

Proof.

by rewrite /Rdist RabsE RminusE. Qed.

Lemma : sum_f_R0 f n = \sum_(0 <= < n.+1) f k.

Proof.

elim: n => [|n ih/=]; first by rewrite big_nat1.
by rewrite RplusE big_nat_recr//= ih.
Qed.

Lemma : fact n = n`!.

Proof.

by elim: n => //= n ih; rewrite factS mulSn ih. Qed.

Definition := (RplusE, RminusE, RmultE, RoppE, RinvE, RdivE,
INRE, R0E, R1E, Pos_to_natE, IZRposE, RsqrtE, RpowE, RmaxE, RminE,
RabsE, RdistE, sum_f_R0E, factE).

Section bigmaxr.
Context { : realDomainType}.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
Definition ( : R) := \big[Num.max/head r s]_( <- s) i.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : R) : bigmaxr x0 [::] = x0.

Proof.

#[warning="-deprecated"] by rewrite /bigmaxr /= big_nil.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : R) : bigmaxr x0 [:: x] = x.

Proof.

#[warning="-deprecated"] by rewrite /bigmaxr /= big_cons big_nil maxxx.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : R) : bigmaxr r s = foldr Num.max (head r s) (behead s).

Proof.

#[warning="-deprecated"]
rewrite (_ : bigmaxr _ _ = if s isn't h :: t then r else \big[Num.max/h]_( <- s) i).
#[warning="-deprecated"]
by case: s => //=; rewrite /bigmaxr big_nil.
#[warning="-deprecated"]
case: s => // ? t; rewrite big_cons /bigmaxr.
by elim: t => //= [|? ? <-]; [rewrite big_nil maxxx | rewrite big_cons maxCA].
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
Lemma ( : R) : Num.max x (\big[Num.max/x]_( <- y :: s) j) =
Num.max x (\big[Num.max/y]_( <- y :: s) i).

Proof.

elim: s => /= [|h t IH] in x y *.
by rewrite !big_cons !big_nil maxxx maxCA maxxx maxC.
by rewrite big_cons maxCA IH maxCA [in RHS]big_cons IH.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : R) :
bigmaxr x0 (x :: y :: lr) = Num.max x (bigmaxr x0 (y :: lr)).

Proof.

#[warning="-deprecated"]
by rewrite [y :: lr]lock /bigmaxr /= -lock big_cons bigrmax_dflt.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : R) :
(i < size s)%N -> (nth x0 s i) <= (bigmaxr x0 s).

Proof.

#[warning="-deprecated"]
rewrite /bigmaxr; elim: s i => // h t IH [_|i] /=.
by rewrite big_cons /= le_max lexx.
rewrite ltnS => ti; case: t => [|h' t] // in IH ti *.
#[warning="-deprecated"]
by rewrite big_cons bigrmax_dflt le_max orbC IH.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : R) ( : R) :
bigmaxr (x0 + x) (map (fun : R => y + x) lr) = (bigmaxr x0 lr) + x.

Proof.

#[warning="-deprecated"]
rewrite /bigmaxr; case: lr => [|h t]; first by rewrite !big_nil.
elim: t h => /= [|h' t IH] h; first by rewrite ?(big_cons,big_nil) -addr_maxl.
#[warning="-deprecated"]
by rewrite [in RHS]big_cons bigrmax_dflt addr_maxl -IH big_cons bigrmax_dflt.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : R) : (0 < size lr)%N -> bigmaxr x0 lr \in lr.

Proof.

#[warning="-deprecated"]
rewrite /bigmaxr; case: lr => // h t _.
elim: t => //= [|h' t IH] in h *; first by rewrite big_cons big_nil inE maxxx.
#[warning="-deprecated"]
rewrite big_cons bigrmax_dflt inE eq_le; case: lerP => /=.
- by rewrite le_max lexx.
- by rewrite lt_max ltxx => ?; rewrite max_r ?IH // ltW.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : finType) ( : seq A) ( : R) ( : A -> R) :
0 <= k -> bigmaxr 0 (map (fun => k * x i) s) = k * bigmaxr 0 (map x s).

Proof.

move=> k0; elim: s => /= [|h [/=|h' t ih]].
#[warning="-deprecated"]
by rewrite bigmaxr_nil mulr0.
#[warning="-deprecated"]
by rewrite !bigmaxr_un.
#[warning="-deprecated"]
by rewrite bigmaxr_cons {}ih bigmaxr_cons maxr_pMr.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : R) :
(0 < size lr)%N -> (index (bigmaxr x0 lr) lr < size lr)%N.

Proof.

#[warning="-deprecated"]
rewrite /bigmaxr; case: lr => //= h t _; case: ifPn => // /negbTE H.
#[warning="-deprecated"]
move: (@bigmaxr_mem x0 (h :: t) isT).
by rewrite ltnS index_mem inE /= eq_sym H.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : R) ( : R) :
(0 < size lr)%N ->
reflect (forall , (i < size lr)%N -> (nth x0 lr i) <= x) ((bigmaxr x0 lr) <= x).

Proof.

move=> lr_size; apply: (iffP idP) => [le_x i i_size | H].
#[warning="-deprecated"]
by apply: (le_trans _ le_x); apply: bigmaxr_ler.
#[warning="-deprecated"]
by move/(nthP x0): (bigmaxr_mem x0 lr_size) => [i i_size <-]; apply: H.
Qed.

Proof.

move=> lr_size; apply: (iffP idP) => [lt_x i i_size | H].
#[warning="-deprecated"]
by apply: le_lt_trans lt_x; apply: bigmaxr_ler.
#[warning="-deprecated"]
by move/(nthP x0): (bigmaxr_mem x0 lr_size) => [i i_size <-]; apply: H.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : R) ( : R) :
(x \in lr /\ forall , (i < size lr) %N -> (nth x0 lr i) <= x) -> (bigmaxr x0 lr = x).

Proof.

move=> [] /(nthP x0) [] j j_size j_nth x_ler; apply: le_anti; apply/andP; split.
#[warning="-deprecated"]
by apply/bigmaxr_lerP => //; apply: (leq_trans _ j_size).
#[warning="-deprecated"]
by rewrite -j_nth (bigmaxr_ler _ j_size).
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : R) :
uniq lr -> forall , (i < size lr)%N ->
(nth x0 lr i) <= (bigmaxr x0 lr) ?= iff (i == index (bigmaxr x0 lr) lr).

Proof.

#[warning="-deprecated"]
move=> lr_uniq i i_size; rewrite /Num.leif (bigmaxr_ler _ i_size).
#[warning="-deprecated"]
rewrite -(nth_uniq x0 i_size (bigmaxr_index _ (leq_trans _ i_size)) lr_uniq) //.
rewrite nth_index //.
#[warning="-deprecated"]
by apply: bigmaxr_mem; apply: (leq_trans _ i_size).
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Definition ( : {ffun 'I_n.+1 -> R}) :=
bigmaxr (f ord0) (codom f).

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : {ffun 'I_n.+1 -> R}) :
(f i) <= (bmaxrf f).

Proof.

#[warning="-deprecated"]
move: (@bigmaxr_ler (f ord0) (codom f) (nat_of_ord i)).
#[warning="-deprecated"]
rewrite /bmaxrf size_codom card_ord => H; move: (ltn_ord i); move/H.
suff -> : nth (f ord0) (codom f) i = f i; first by [].
by rewrite /codom (nth_map ord0) ?size_enum_ord // nth_ord_enum.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : {ffun 'I_n.+1 -> R}) :
(index (bmaxrf f) (codom f) < n.+1)%N.

Proof.

#[warning="-deprecated"]
rewrite /bmaxrf.
rewrite [in X in (_ < X)%N](_ : n.+1 = size (codom f)).
by rewrite size_codom card_ord.
#[warning="-deprecated"]
by apply: bigmaxr_index; rewrite size_codom card_ord.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Definition := Ordinal (@bmaxrf_index n f).

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
Lemma ( : (i < n)%N) : i = Ordinal ord_i :> nat.

Proof.

by []. Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : {ffun 'I_n.+1 -> R}) :
f (index_bmaxrf f) = bmaxrf f.

Proof.

#[warning="-deprecated"]
move: (bmaxrf_index f).
rewrite -[X in _ (_ < X)%N]card_ord -(size_codom f) index_mem.
move/(nth_index (f ord0)) => <-; rewrite (nth_map ord0).
#[warning="-deprecated"]
by rewrite size_enum_ord; apply: bmaxrf_index.
#[warning="-deprecated"]
by rewrite (ordnat (bmaxrf_index _)) /index_bmaxrf nth_ord_enum.
Qed.

#[deprecated(note="To be removed. Use order.v's bigmax/min lemmas instead.")]
#[warning="-deprecated"]
Lemma ( : {ffun 'I_n.+1 -> R}) :
injective f -> forall ,
(f i) <= (bmaxrf f) ?= iff (i == index_bmaxrf f).

Proof.

#[warning="-deprecated"]
by move=> inj_f i; rewrite /Num.leif bmaxrf_ler -(inj_eq inj_f) eq_index_bmaxrf.
Qed.

End bigmaxr.

End ssreal_struct_contd.

Files

Module mathcomp.reals_stdlib.Rstruct