diff options
Diffstat (limited to 'mathcomp/algebra/ssrnum.v')
| -rw-r--r-- | mathcomp/algebra/ssrnum.v | 622 |
1 files changed, 0 insertions, 622 deletions
diff --git a/mathcomp/algebra/ssrnum.v b/mathcomp/algebra/ssrnum.v index dce3ffd..cc04183 100644 --- a/mathcomp/algebra/ssrnum.v +++ b/mathcomp/algebra/ssrnum.v @@ -5395,625 +5395,3 @@ Export Num.NumMixin.Exports Num.RealMixin.Exports. Export Num.RealLeMixin.Exports Num.RealLtMixin.Exports. Notation ImaginaryMixin := Num.ClosedField.ImaginaryMixin. - -(* compatibility module *) -Module mc_1_10. -Module Num. -(* If you failed to process the next line in the PG or the CoqIDE, replace *) -(* all the "ssrnum.Num" with "Top.Num" in this module to process them, and *) -(* revert them in order to compile and commit. This problem will be solved *) -(* in Coq 8.10. See also: https://github.com/math-comp/math-comp/pull/270. *) -Export ssrnum.Num. - -Module Import Def. -Export ssrnum.Num.Def. -Definition minr {R : numDomainType} (x y : R) := if x <= y then x else y. -Definition maxr {R : numDomainType} (x y : R) := if x <= y then y else x. -End Def. - -Notation min := minr. -Notation max := maxr. - -Module Import Syntax. -Notation "`| x |" := - (@norm _ (@Num.NormedZmodule.numDomain_normedZmodType _) x) : ring_scope. -End Syntax. - -Module Import Theory. -Export ssrnum.Num.Theory. - -Section NumIntegralDomainTheory. -Variable R : numDomainType. -Implicit Types x y z : R. -Definition ltr_def x y : (x < y) = (y != x) && (x <= y) := lt_def x y. -Definition gerE x y : ge x y = (y <= x) := geE x y. -Definition gtrE x y : gt x y = (y < x) := gtE x y. -Definition lerr x : x <= x := lexx x. -Definition ltrr x : x < x = false := ltxx x. -Definition ltrW x y : x < y -> x <= y := @ltW _ _ x y. -Definition ltr_neqAle x y : (x < y) = (x != y) && (x <= y) := lt_neqAle x y. -Definition ler_eqVlt x y : (x <= y) = (x == y) || (x < y) := le_eqVlt x y. -Definition gtr_eqF x y : y < x -> x == y = false := @gt_eqF _ _ x y. -Definition ltr_eqF x y : x < y -> x == y = false := @lt_eqF _ _ x y. -Definition ler_asym : antisymmetric (@ler R) := le_anti. -Definition eqr_le x y : (x == y) = (x <= y <= x) := eq_le x y. -Definition ltr_trans : transitive (@ltr R) := lt_trans. -Definition ler_lt_trans y x z : x <= y -> y < z -> x < z := - @le_lt_trans _ _ y x z. -Definition ltr_le_trans y x z : x < y -> y <= z -> x < z := - @lt_le_trans _ _ y x z. -Definition ler_trans : transitive (@ler R) := le_trans. -Definition lterr := (lerr, ltrr). -Definition lerifP x y C : - reflect (x <= y ?= iff C) (if C then x == y else x < y) := leifP. -Definition ltr_asym x y : x < y < x = false := lt_asym x y. -Definition ler_anti : antisymmetric (@ler R) := le_anti. -Definition ltr_le_asym x y : x < y <= x = false := lt_le_asym x y. -Definition ler_lt_asym x y : x <= y < x = false := le_lt_asym x y. -Definition lter_anti := (=^~ eqr_le, ltr_asym, ltr_le_asym, ler_lt_asym). -Definition ltr_geF x y : x < y -> y <= x = false := @lt_geF _ _ x y. -Definition ler_gtF x y : x <= y -> y < x = false := @le_gtF _ _ x y. -Definition ltr_gtF x y : x < y -> y < x = false := @lt_gtF _ _ x y. -Definition normr0 : `|0| = 0 :> R := normr0 _. -Definition normrMn x n : `|x *+ n| = `|x| *+ n := normrMn x n. -Definition normr0P {x} : reflect (`|x| = 0) (x == 0) := normr0P. -Definition normr_eq0 x : (`|x| == 0) = (x == 0) := normr_eq0 x. -Definition normrN x : `|- x| = `|x| := normrN x. -Definition distrC x y : `|x - y| = `|y - x| := distrC x y. -Definition normr_id x : `| `|x| | = `|x| := normr_id x. -Definition normr_ge0 x : 0 <= `|x| := normr_ge0 x. -Definition normr_le0 x : (`|x| <= 0) = (x == 0) := normr_le0 x. -Definition normr_lt0 x : `|x| < 0 = false := normr_lt0 x. -Definition normr_gt0 x : (`|x| > 0) = (x != 0) := normr_gt0 x. -Definition normrE := (normr_id, normr0, @normr1 R, @normrN1 R, normr_ge0, - normr_eq0, normr_lt0, normr_le0, normr_gt0, normrN). -End NumIntegralDomainTheory. - -Section NumIntegralDomainMonotonyTheory. -Variables R R' : numDomainType. -Section AcrossTypes. -Variables (D D' : pred R) (f : R -> R'). -Definition ltrW_homo : {homo f : x y / x < y} -> {homo f : x y / x <= y} := - ltW_homo (f := f). -Definition ltrW_nhomo : {homo f : x y /~ x < y} -> {homo f : x y /~ x <= y} := - ltW_nhomo (f := f). -Definition inj_homo_ltr : - injective f -> {homo f : x y / x <= y} -> {homo f : x y / x < y} := - inj_homo_lt (f := f). -Definition inj_nhomo_ltr : - injective f -> {homo f : x y /~ x <= y} -> {homo f : x y /~ x < y} := - inj_nhomo_lt (f := f). -Definition incr_inj : {mono f : x y / x <= y} -> injective f := - inc_inj (f := f). -Definition decr_inj : {mono f : x y /~ x <= y} -> injective f := - dec_inj (f := f). -Definition lerW_mono : {mono f : x y / x <= y} -> {mono f : x y / x < y} := - leW_mono (f := f). -Definition lerW_nmono : {mono f : x y /~ x <= y} -> {mono f : x y /~ x < y} := - leW_nmono (f := f). -Definition ltrW_homo_in : - {in D & D', {homo f : x y / x < y}} -> {in D & D', {homo f : x y / x <= y}} := - ltW_homo_in (f := f). -Definition ltrW_nhomo_in : - {in D & D', {homo f : x y /~ x < y}} -> - {in D & D', {homo f : x y /~ x <= y}} := - ltW_nhomo_in (f := f). -Definition inj_homo_ltr_in : - {in D & D', injective f} -> {in D & D', {homo f : x y / x <= y}} -> - {in D & D', {homo f : x y / x < y}} := - inj_homo_lt_in (f := f). -Definition inj_nhomo_ltr_in : - {in D & D', injective f} -> {in D & D', {homo f : x y /~ x <= y}} -> - {in D & D', {homo f : x y /~ x < y}} := - inj_nhomo_lt_in (f := f). -Definition incr_inj_in : - {in D &, {mono f : x y / x <= y}} -> {in D &, injective f} := - inc_inj_in (f := f). -Definition decr_inj_in : - {in D &, {mono f : x y /~ x <= y}} -> {in D &, injective f} := - dec_inj_in (f := f). -Definition lerW_mono_in : - {in D &, {mono f : x y / x <= y}} -> {in D &, {mono f : x y / x < y}} := - leW_mono_in (f := f). -Definition lerW_nmono_in : - {in D &, {mono f : x y /~ x <= y}} -> {in D &, {mono f : x y /~ x < y}} := - leW_nmono_in (f := f). -End AcrossTypes. -Section NatToR. -Variables (D D' : pred nat) (f : nat -> R). -Definition ltnrW_homo : - {homo f : m n / (m < n)%N >-> m < n} -> - {homo f : m n / (m <= n)%N >-> m <= n} := - ltW_homo (f := f). -Definition ltnrW_nhomo : - {homo f : m n / (n < m)%N >-> m < n} -> - {homo f : m n / (n <= m)%N >-> m <= n} := - ltW_nhomo (f := f). -Definition inj_homo_ltnr : injective f -> - {homo f : m n / (m <= n)%N >-> m <= n} -> - {homo f : m n / (m < n)%N >-> m < n} := - inj_homo_lt (f := f). -Definition inj_nhomo_ltnr : injective f -> - {homo f : m n / (n <= m)%N >-> m <= n} -> - {homo f : m n / (n < m)%N >-> m < n} := - inj_nhomo_lt (f := f). -Definition incnr_inj : - {mono f : m n / (m <= n)%N >-> m <= n} -> injective f := - inc_inj (f := f). -Definition decnr_inj : - {mono f : m n / (n <= m)%N >-> m <= n} -> injective f := - dec_inj (f := f). -Definition decnr_inj_inj := decnr_inj. -Definition lenrW_mono : {mono f : m n / (m <= n)%N >-> m <= n} -> - {mono f : m n / (m < n)%N >-> m < n} := - leW_mono (f := f). -Definition lenrW_nmono : {mono f : m n / (n <= m)%N >-> m <= n} -> - {mono f : m n / (n < m)%N >-> m < n} := - leW_nmono (f := f). -Definition lenr_mono : {homo f : m n / (m < n)%N >-> m < n} -> - {mono f : m n / (m <= n)%N >-> m <= n} := - le_mono (f := f). -Definition lenr_nmono : - {homo f : m n / (n < m)%N >-> m < n} -> - {mono f : m n / (n <= m)%N >-> m <= n} := - le_nmono (f := f). -Definition ltnrW_homo_in : - {in D & D', {homo f : m n / (m < n)%N >-> m < n}} -> - {in D & D', {homo f : m n / (m <= n)%N >-> m <= n}} := - ltW_homo_in (f := f). -Definition ltnrW_nhomo_in : - {in D & D', {homo f : m n / (n < m)%N >-> m < n}} -> - {in D & D', {homo f : m n / (n <= m)%N >-> m <= n}} := - ltW_nhomo_in (f := f). -Definition inj_homo_ltnr_in : {in D & D', injective f} -> - {in D & D', {homo f : m n / (m <= n)%N >-> m <= n}} -> - {in D & D', {homo f : m n / (m < n)%N >-> m < n}} := - inj_homo_lt_in (f := f). -Definition inj_nhomo_ltnr_in : {in D & D', injective f} -> - {in D & D', {homo f : m n / (n <= m)%N >-> m <= n}} -> - {in D & D', {homo f : m n / (n < m)%N >-> m < n}} := - inj_nhomo_lt_in (f := f). -Definition incnr_inj_in : - {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} -> {in D &, injective f} := - inc_inj_in (f := f). -Definition decnr_inj_in : - {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} -> {in D &, injective f} := - dec_inj_in (f := f). -Definition decnr_inj_inj_in := decnr_inj_in. -Definition lenrW_mono_in : - {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} -> - {in D &, {mono f : m n / (m < n)%N >-> m < n}} := - leW_mono_in (f := f). -Definition lenrW_nmono_in : - {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} -> - {in D &, {mono f : m n / (n < m)%N >-> m < n}} := - leW_nmono_in (f := f). -Definition lenr_mono_in : - {in D &, {homo f : m n / (m < n)%N >-> m < n}} -> - {in D &, {mono f : m n / (m <= n)%N >-> m <= n}} := - le_mono_in (f := f). -Definition lenr_nmono_in : - {in D &, {homo f : m n / (n < m)%N >-> m < n}} -> - {in D &, {mono f : m n / (n <= m)%N >-> m <= n}} := - le_nmono_in (f := f). -End NatToR. -Section RToNat. -Variables (D D' : pred R) (f : R -> nat). -Definition ltrnW_homo : - {homo f : m n / m < n >-> (m < n)%N} -> - {homo f : m n / m <= n >-> (m <= n)%N} := - ltW_homo (f := f). -Definition ltrnW_nhomo : - {homo f : m n / n < m >-> (m < n)%N} -> - {homo f : m n / n <= m >-> (m <= n)%N} := - ltW_nhomo (f := f). -Definition inj_homo_ltrn : injective f -> - {homo f : m n / m <= n >-> (m <= n)%N} -> - {homo f : m n / m < n >-> (m < n)%N} := - inj_homo_lt (f := f). -Definition inj_nhomo_ltrn : injective f -> - {homo f : m n / n <= m >-> (m <= n)%N} -> - {homo f : m n / n < m >-> (m < n)%N} := - inj_nhomo_lt (f := f). -Definition incrn_inj : {mono f : m n / m <= n >-> (m <= n)%N} -> injective f := - inc_inj (f := f). -Definition decrn_inj : {mono f : m n / n <= m >-> (m <= n)%N} -> injective f := - dec_inj (f := f). -Definition lernW_mono : - {mono f : m n / m <= n >-> (m <= n)%N} -> - {mono f : m n / m < n >-> (m < n)%N} := - leW_mono (f := f). -Definition lernW_nmono : - {mono f : m n / n <= m >-> (m <= n)%N} -> - {mono f : m n / n < m >-> (m < n)%N} := - leW_nmono (f := f). -Definition ltrnW_homo_in : - {in D & D', {homo f : m n / m < n >-> (m < n)%N}} -> - {in D & D', {homo f : m n / m <= n >-> (m <= n)%N}} := - ltW_homo_in (f := f). -Definition ltrnW_nhomo_in : - {in D & D', {homo f : m n / n < m >-> (m < n)%N}} -> - {in D & D', {homo f : m n / n <= m >-> (m <= n)%N}} := - ltW_nhomo_in (f := f). -Definition inj_homo_ltrn_in : {in D & D', injective f} -> - {in D & D', {homo f : m n / m <= n >-> (m <= n)%N}} -> - {in D & D', {homo f : m n / m < n >-> (m < n)%N}} := - inj_homo_lt_in (f := f). -Definition inj_nhomo_ltrn_in : {in D & D', injective f} -> - {in D & D', {homo f : m n / n <= m >-> (m <= n)%N}} -> - {in D & D', {homo f : m n / n < m >-> (m < n)%N}} := - inj_nhomo_lt_in (f := f). -Definition incrn_inj_in : - {in D &, {mono f : m n / m <= n >-> (m <= n)%N}} -> {in D &, injective f} := - inc_inj_in (f := f). -Definition decrn_inj_in : - {in D &, {mono f : m n / n <= m >-> (m <= n)%N}} -> {in D &, injective f} := - dec_inj_in (f := f). -Definition lernW_mono_in : - {in D &, {mono f : m n / m <= n >-> (m <= n)%N}} -> - {in D &, {mono f : m n / m < n >-> (m < n)%N}} := - leW_mono_in (f := f). -Definition lernW_nmono_in : - {in D &, {mono f : m n / n <= m >-> (m <= n)%N}} -> - {in D &, {mono f : m n / n < m >-> (m < n)%N}} := - leW_nmono_in (f := f). -End RToNat. -End NumIntegralDomainMonotonyTheory. - -Section NumDomainOperationTheory. -Variable R : numDomainType. -Implicit Types x y z t : R. -Definition lerif_refl x C : reflect (x <= x ?= iff C) C := leif_refl. -Definition lerif_trans x1 x2 x3 C12 C23 : - x1 <= x2 ?= iff C12 -> x2 <= x3 ?= iff C23 -> x1 <= x3 ?= iff C12 && C23 := - @leif_trans _ _ x1 x2 x3 C12 C23. -Definition lerif_le x y : x <= y -> x <= y ?= iff (x >= y) := @leif_le _ _ x y. -Definition lerif_eq x y : x <= y -> x <= y ?= iff (x == y) := @leif_eq _ _ x y. -Definition ger_lerif x y C : x <= y ?= iff C -> (y <= x) = C := - @ge_leif _ _ x y C. -Definition ltr_lerif x y C : x <= y ?= iff C -> (x < y) = ~~ C := - @lt_leif _ _ x y C. -Definition normr_real x : `|x| \is real := normr_real x. -Definition ler_norm_sum I r (G : I -> R) (P : pred I): - `|\sum_(i <- r | P i) G i| <= \sum_(i <- r | P i) `|G i| := - ler_norm_sum r G P. -Definition ler_norm_sub x y : `|x - y| <= `|x| + `|y| := ler_norm_sub x y. -Definition ler_dist_add z x y : `|x - y| <= `|x - z| + `|z - y| := - ler_dist_add z x y. -Definition ler_sub_norm_add x y : `|x| - `|y| <= `|x + y| := - ler_sub_norm_add x y. -Definition ler_sub_dist x y : `|x| - `|y| <= `|x - y| := ler_sub_dist x y. -Definition ler_dist_dist x y : `| `|x| - `|y| | <= `|x - y| := - ler_dist_dist x y. -Definition ler_dist_norm_add x y : `| `|x| - `|y| | <= `|x + y| := - ler_dist_norm_add x y. -Definition ler_nnorml x y : y < 0 -> `|x| <= y = false := @ler_nnorml _ _ x y. -Definition ltr_nnorml x y : y <= 0 -> `|x| < y = false := @ltr_nnorml _ _ x y. -Definition lter_nnormr := (ler_nnorml, ltr_nnorml). -Definition mono_in_lerif (A : pred R) (f : R -> R) C : - {in A &, {mono f : x y / x <= y}} -> - {in A &, forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C)} := - @mono_in_leif _ _ A f C. -Definition mono_lerif (f : R -> R) C : - {mono f : x y / x <= y} -> - forall x y, (f x <= f y ?= iff C) = (x <= y ?= iff C) := - @mono_leif _ _ f C. -Definition nmono_in_lerif (A : pred R) (f : R -> R) C : - {in A &, {mono f : x y /~ x <= y}} -> - {in A &, forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C)} := - @nmono_in_leif _ _ A f C. -Definition nmono_lerif (f : R -> R) C : - {mono f : x y /~ x <= y} -> - forall x y, (f x <= f y ?= iff C) = (y <= x ?= iff C) := - @nmono_leif _ _ f C. -End NumDomainOperationTheory. - -Section RealDomainTheory. -Variable R : realDomainType. -Implicit Types x y z t : R. -Definition ler_total : total (@ler R) := le_total. -Definition ltr_total x y : x != y -> (x < y) || (y < x) := - @lt_total _ _ x y. -Definition wlog_ler P : - (forall a b, P b a -> P a b) -> (forall a b, a <= b -> P a b) -> - forall a b : R, P a b := - @wlog_le _ _ P. -Definition wlog_ltr P : - (forall a, P a a) -> - (forall a b, (P b a -> P a b)) -> (forall a b, a < b -> P a b) -> - forall a b : R, P a b := - @wlog_lt _ _ P. -Definition ltrNge x y : (x < y) = ~~ (y <= x) := @ltNge _ _ x y. -Definition lerNgt x y : (x <= y) = ~~ (y < x) := @leNgt _ _ x y. -Definition neqr_lt x y : (x != y) = (x < y) || (y < x) := @neq_lt _ _ x y. -Definition eqr_leLR x y z t : - (x <= y -> z <= t) -> (y < x -> t < z) -> (x <= y) = (z <= t) := - @eq_leLR _ _ x y z t. -Definition eqr_leRL x y z t : - (x <= y -> z <= t) -> (y < x -> t < z) -> (z <= t) = (x <= y) := - @eq_leRL _ _ x y z t. -Definition eqr_ltLR x y z t : - (x < y -> z < t) -> (y <= x -> t <= z) -> (x < y) = (z < t) := - @eq_ltLR _ _ x y z t. -Definition eqr_ltRL x y z t : - (x < y -> z < t) -> (y <= x -> t <= z) -> (z < t) = (x < y) := - @eq_ltRL _ _ x y z t. -End RealDomainTheory. - -Section RealDomainMonotony. -Variables (R : realDomainType) (R' : numDomainType) (D : pred R). -Variables (f : R -> R') (f' : R -> nat). -Definition ler_mono : {homo f : x y / x < y} -> {mono f : x y / x <= y} := - le_mono (f := f). -Definition homo_mono := ler_mono. -Definition ler_nmono : {homo f : x y /~ x < y} -> {mono f : x y /~ x <= y} := - le_nmono (f := f). -Definition nhomo_mono := ler_nmono. -Definition ler_mono_in : - {in D &, {homo f : x y / x < y}} -> {in D &, {mono f : x y / x <= y}} := - le_mono_in (f := f). -Definition homo_mono_in := ler_mono_in. -Definition ler_nmono_in : - {in D &, {homo f : x y /~ x < y}} -> {in D &, {mono f : x y /~ x <= y}} := - le_nmono_in (f := f). -Definition nhomo_mono_in := ler_nmono_in. -Definition lern_mono : - {homo f' : m n / m < n >-> (m < n)%N} -> - {mono f' : m n / m <= n >-> (m <= n)%N} := - le_mono (f := f'). -Definition lern_nmono : - {homo f' : m n / n < m >-> (m < n)%N} -> - {mono f' : m n / n <= m >-> (m <= n)%N} := - le_nmono (f := f'). -Definition lern_mono_in : - {in D &, {homo f' : m n / m < n >-> (m < n)%N}} -> - {in D &, {mono f' : m n / m <= n >-> (m <= n)%N}} := - le_mono_in (f := f'). -Definition lern_nmono_in : - {in D &, {homo f' : m n / n < m >-> (m < n)%N}} -> - {in D &, {mono f' : m n / n <= m >-> (m <= n)%N}} := - le_nmono_in (f := f'). -End RealDomainMonotony. - -Section RealDomainOperations. -Variable R : realDomainType. -Implicit Types x y z : R. -Section MinMax. - -Let mrE x y : ((min x y = Order.min x y) * (maxr x y = Order.max x y))%type. -Proof. by rewrite /minr /min /maxr /max; case: comparableP. Qed. -Ltac mapply x := do ?[rewrite !mrE|apply: x|move=> ?]. -Ltac mexact x := by mapply x. - -Lemma minrC : @commutative R R min. Proof. mexact @minC. Qed. -Lemma minrr : @idempotent R min. Proof. mexact @minxx. Qed. -Lemma minr_l x y : x <= y -> min x y = x. Proof. mexact @min_l. Qed. -Lemma minr_r x y : y <= x -> min x y = y. Proof. mexact @min_r. Qed. -Lemma maxrC : @commutative R R max. Proof. mexact @maxC. Qed. -Lemma maxrr : @idempotent R max. Proof. mexact @maxxx. Qed. -Lemma maxr_l x y : y <= x -> max x y = x. Proof. mexact @max_l. Qed. -Lemma maxr_r x y : x <= y -> max x y = y. Proof. mexact @max_r. Qed. - -Lemma minrA x y z : min x (min y z) = min (min x y) z. -Proof. mexact @minA. Qed. - -Lemma minrCA : @left_commutative R R min. Proof. mexact @minCA. Qed. -Lemma minrAC : @right_commutative R R min. Proof. mexact @minAC. Qed. -Lemma maxrA x y z : max x (max y z) = max (max x y) z. -Proof. mexact @maxA. Qed. - -Lemma maxrCA : @left_commutative R R max. Proof. mexact @maxCA. Qed. -Lemma maxrAC : @right_commutative R R max. Proof. mexact @maxAC. Qed. -Lemma eqr_minl x y : (min x y == x) = (x <= y). Proof. mexact @eq_minl. Qed. -Lemma eqr_minr x y : (min x y == y) = (y <= x). Proof. mexact @eq_minr. Qed. -Lemma eqr_maxl x y : (max x y == x) = (y <= x). Proof. mexact @eq_maxl. Qed. -Lemma eqr_maxr x y : (max x y == y) = (x <= y). Proof. mexact @eq_maxr. Qed. - -Lemma ler_minr x y z : (x <= min y z) = (x <= y) && (x <= z). -Proof. mexact @le_minr. Qed. - -Lemma ler_minl x y z : (min y z <= x) = (y <= x) || (z <= x). -Proof. mexact @le_minl. Qed. - -Lemma ler_maxr x y z : (x <= max y z) = (x <= y) || (x <= z). -Proof. mexact @le_maxr. Qed. - -Lemma ler_maxl x y z : (max y z <= x) = (y <= x) && (z <= x). -Proof. mexact @le_maxl. Qed. - -Lemma ltr_minr x y z : (x < min y z) = (x < y) && (x < z). -Proof. mexact @lt_minr. Qed. - -Lemma ltr_minl x y z : (min y z < x) = (y < x) || (z < x). -Proof. mexact @lt_minl. Qed. - -Lemma ltr_maxr x y z : (x < max y z) = (x < y) || (x < z). -Proof. mexact @lt_maxr. Qed. - -Lemma ltr_maxl x y z : (max y z < x) = (y < x) && (z < x). -Proof. mexact @lt_maxl. Qed. - -Definition lter_minr := (ler_minr, ltr_minr). -Definition lter_minl := (ler_minl, ltr_minl). -Definition lter_maxr := (ler_maxr, ltr_maxr). -Definition lter_maxl := (ler_maxl, ltr_maxl). - -Lemma minrK x y : max (min x y) x = x. Proof. rewrite minrC; mexact @minxK. Qed. -Lemma minKr x y : min y (max x y) = y. Proof. rewrite maxrC; mexact @maxKx. Qed. - -Lemma maxr_minl : @left_distributive R R max min. Proof. mexact @max_minl. Qed. -Lemma maxr_minr : @right_distributive R R max min. Proof. mexact @max_minr. Qed. -Lemma minr_maxl : @left_distributive R R min max. Proof. mexact @min_maxl. Qed. -Lemma minr_maxr : @right_distributive R R min max. Proof. mexact @min_maxr. Qed. - -Variant minr_spec x y : bool -> bool -> R -> Type := -| Minr_r of x <= y : minr_spec x y true false x -| Minr_l of y < x : minr_spec x y false true y. -Lemma minrP x y : minr_spec x y (x <= y) (y < x) (min x y). -Proof. by rewrite mrE; case: leP; constructor. Qed. - -Variant maxr_spec x y : bool -> bool -> R -> Type := -| Maxr_r of y <= x : maxr_spec x y true false x -| Maxr_l of x < y : maxr_spec x y false true y. -Lemma maxrP x y : maxr_spec x y (y <= x) (x < y) (max x y). -Proof. by rewrite mrE; case: (leP y); constructor. Qed. - -End MinMax. -End RealDomainOperations. - -Arguments lerifP {R x y C}. -Arguments lerif_refl {R x C}. -Arguments mono_in_lerif [R A f C]. -Arguments nmono_in_lerif [R A f C]. -Arguments mono_lerif [R f C]. -Arguments nmono_lerif [R f C]. - -Section RealDomainArgExtremum. - -Context {R : realDomainType} {I : finType} (i0 : I). -Context (P : pred I) (F : I -> R) (Pi0 : P i0). - -Definition arg_minr := extremum <=%R i0 P F. -Definition arg_maxr := extremum >=%R i0 P F. -Definition arg_minrP : extremum_spec <=%R P F arg_minr := arg_minP F Pi0. -Definition arg_maxrP : extremum_spec >=%R P F arg_maxr := arg_maxP F Pi0. - -End RealDomainArgExtremum. - -Notation "@ 'real_lerP'" := - (deprecate real_lerP real_leP) (at level 10, only parsing) : fun_scope. -Notation real_lerP := (@real_lerP _ _ _) (only parsing). -Notation "@ 'real_ltrP'" := - (deprecate real_ltrP real_ltP) (at level 10, only parsing) : fun_scope. -Notation real_ltrP := (@real_ltrP _ _ _) (only parsing). -Notation "@ 'real_ltrNge'" := - (deprecate real_ltrNge real_ltNge) (at level 10, only parsing) : fun_scope. -Notation real_ltrNge := (@real_ltrNge _ _ _) (only parsing). -Notation "@ 'real_lerNgt'" := - (deprecate real_lerNgt real_leNgt) (at level 10, only parsing) : fun_scope. -Notation real_lerNgt := (@real_lerNgt _ _ _) (only parsing). -Notation "@ 'real_ltrgtP'" := - (deprecate real_ltrgtP real_ltgtP) (at level 10, only parsing) : fun_scope. -Notation real_ltrgtP := (@real_ltrgtP _ _ _) (only parsing). -Notation "@ 'real_ger0P'" := - (deprecate real_ger0P real_ge0P) (at level 10, only parsing) : fun_scope. -Notation real_ger0P := (@real_ger0P _ _) (only parsing). -Notation "@ 'real_ltrgt0P'" := - (deprecate real_ltrgt0P real_ltgt0P) (at level 10, only parsing) : fun_scope. -Notation real_ltrgt0P := (@real_ltrgt0P _ _) (only parsing). -Notation lerif_nat := (deprecate lerif_nat leif_nat_r) (only parsing). -Notation "@ 'lerif_subLR'" := - (deprecate lerif_subLR leif_subLR) (at level 10, only parsing) : fun_scope. -Notation lerif_subLR := (@lerif_subLR _) (only parsing). -Notation "@ 'lerif_subRL'" := - (deprecate lerif_subRL leif_subRL) (at level 10, only parsing) : fun_scope. -Notation lerif_subRL := (@lerif_subRL _) (only parsing). -Notation "@ 'lerif_add'" := - (deprecate lerif_add leif_add) (at level 10, only parsing) : fun_scope. -Notation lerif_add := (@lerif_add _ _ _ _ _ _ _) (only parsing). -Notation "@ 'lerif_sum'" := - (deprecate lerif_sum leif_sum) (at level 10, only parsing) : fun_scope. -Notation lerif_sum := (@lerif_sum _ _ _ _ _ _) (only parsing). -Notation "@ 'lerif_0_sum'" := - (deprecate lerif_0_sum leif_0_sum) (at level 10, only parsing) : fun_scope. -Notation lerif_0_sum := (@lerif_0_sum _ _ _ _ _) (only parsing). -Notation "@ 'real_lerif_norm'" := - (deprecate real_lerif_norm real_leif_norm) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_norm := (@real_lerif_norm _ _) (only parsing). -Notation "@ 'lerif_pmul'" := - (deprecate lerif_pmul leif_pmul) (at level 10, only parsing) : fun_scope. -Notation lerif_pmul := (@lerif_pmul _ _ _ _ _ _ _) (only parsing). -Notation "@ 'lerif_nmul'" := - (deprecate lerif_nmul leif_nmul) (at level 10, only parsing) : fun_scope. -Notation lerif_nmul := (@lerif_nmul _ _ _ _ _ _ _) (only parsing). -Notation "@ 'lerif_pprod'" := - (deprecate lerif_pprod leif_pprod) (at level 10, only parsing) : fun_scope. -Notation lerif_pprod := (@lerif_pprod _ _ _ _ _ _) (only parsing). -Notation "@ 'real_lerif_mean_square_scaled'" := - (deprecate real_lerif_mean_square_scaled real_leif_mean_square_scaled) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_mean_square_scaled := - (@real_lerif_mean_square_scaled _ _ _ _ _ _) (only parsing). -Notation "@ 'real_lerif_AGM2_scaled'" := - (deprecate real_lerif_AGM2_scaled real_leif_AGM2_scaled) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_AGM2_scaled := - (@real_lerif_AGM2_scaled _ _ _) (only parsing). -Notation "@ 'lerif_AGM_scaled'" := - (deprecate lerif_AGM_scaled leif_AGM2_scaled) - (at level 10, only parsing) : fun_scope. -Notation lerif_AGM_scaled := (@lerif_AGM_scaled _ _ _ _) (only parsing). -Notation "@ 'real_lerif_mean_square'" := - (deprecate real_lerif_mean_square real_leif_mean_square) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_mean_square := - (@real_lerif_mean_square _ _ _) (only parsing). -Notation "@ 'real_lerif_AGM2'" := - (deprecate real_lerif_AGM2 real_leif_AGM2) - (at level 10, only parsing) : fun_scope. -Notation real_lerif_AGM2 := (@real_lerif_AGM2 _ _ _) (only parsing). -Notation "@ 'lerif_AGM'" := - (deprecate lerif_AGM leif_AGM) (at level 10, only parsing) : fun_scope. -Notation lerif_AGM := (@lerif_AGM _ _ _ _) (only parsing). -Notation "@ 'lerif_mean_square_scaled'" := - (deprecate lerif_mean_square_scaled leif_mean_square_scaled) - (at level 10, only parsing) : fun_scope. -Notation lerif_mean_square_scaled := - (@lerif_mean_square_scaled _) (only parsing). -Notation "@ 'lerif_AGM2_scaled'" := - (deprecate lerif_AGM2_scaled leif_AGM2_scaled) - (at level 10, only parsing) : fun_scope. -Notation lerif_AGM2_scaled := (@lerif_AGM2_scaled _) (only parsing). -Notation "@ 'lerif_mean_square'" := - (deprecate lerif_mean_square leif_mean_square) - (at level 10, only parsing) : fun_scope. -Notation lerif_mean_square := (@lerif_mean_square _) (only parsing). -Notation "@ 'lerif_AGM2'" := - (deprecate lerif_AGM2 leif_AGM2) (at level 10, only parsing) : fun_scope. -Notation lerif_AGM2 := (@lerif_AGM2 _) (only parsing). -Notation "@ 'lerif_normC_Re_Creal'" := - (deprecate lerif_normC_Re_Creal leif_normC_Re_Creal) - (at level 10, only parsing) : fun_scope. -Notation lerif_normC_Re_Creal := (@lerif_normC_Re_Creal _) (only parsing). -Notation "@ 'lerif_Re_Creal'" := - (deprecate lerif_Re_Creal leif_Re_Creal) - (at level 10, only parsing) : fun_scope. -Notation lerif_Re_Creal := (@lerif_Re_Creal _) (only parsing). -Notation "@ 'lerif_rootC_AGM'" := - (deprecate lerif_rootC_AGM leif_rootC_AGM) - (at level 10, only parsing) : fun_scope. -Notation lerif_rootC_AGM := (@lerif_rootC_AGM _ _ _ _) (only parsing). - -End Theory. - -Notation "[ 'arg' 'minr_' ( i < i0 | P ) F ]" := - (arg_minr i0 (fun i => P%B) (fun i => F)) - (at level 0, i, i0 at level 10, - format "[ 'arg' 'minr_' ( i < i0 | P ) F ]") : form_scope. - -Notation "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]" := - [arg minr_(i < i0 | i \in A) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'minr_' ( i < i0 'in' A ) F ]") : form_scope. - -Notation "[ 'arg' 'minr_' ( i < i0 ) F ]" := [arg minr_(i < i0 | true) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'minr_' ( i < i0 ) F ]") : form_scope. - -Notation "[ 'arg' 'maxr_' ( i > i0 | P ) F ]" := - (arg_maxr i0 (fun i => P%B) (fun i => F)) - (at level 0, i, i0 at level 10, - format "[ 'arg' 'maxr_' ( i > i0 | P ) F ]") : form_scope. - -Notation "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]" := - [arg maxr_(i > i0 | i \in A) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'maxr_' ( i > i0 'in' A ) F ]") : form_scope. - -Notation "[ 'arg' 'maxr_' ( i > i0 ) F ]" := [arg maxr_(i > i0 | true) F] - (at level 0, i, i0 at level 10, - format "[ 'arg' 'maxr_' ( i > i0 ) F ]") : form_scope. - -End Num. -End mc_1_10. |