diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d90a8985a4..84f327da8d 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -14,6 +14,11 @@ - in `uniform_structure.v`: + lemma `unif_continuous_continuous` +- in `unstable.v`: + + definitions `clamp`, `clamp_gele` + + lemmas `clamp_gemin`, `clamp_lemax`, `minmax_clamp`, + `clamp_id`, `clamp_min`, `clamp_max` + ### Changed - in `esum.v`: diff --git a/classical/unstable.v b/classical/unstable.v index 7e3c2827f8..3b00d8cfc2 100644 --- a/classical/unstable.v +++ b/classical/unstable.v @@ -14,6 +14,7 @@ From mathcomp Require Import vector archimedean interval matrix. (* 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 *) @@ -47,7 +48,6 @@ From mathcomp Require Import vector archimedean interval matrix. Attributes warn(note="The unstable.v file should only be used inside analysis.", cats="internal-analysis"). -Unset SsrOldRewriteGoalsOrder. (* remove the line when requiring MathComp >= 2.6 *) Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. @@ -55,6 +55,34 @@ Unset Printing Implicit Defensive. Import Order.TTheory GRing.Theory Num.Theory. Local Open Scope ring_scope. +Section Clamp. +Context {R : realDomainType} (min max : R). +Hypothesis minmax : min <= max. + +Definition clamp (x : R) := Num.max (Num.min x max) min. + +Lemma clamp_gemin x : min <= clamp x. +Proof. by rewrite le_max lexx orbT. Qed. + +Lemma clamp_lemax x : clamp x <= max. +Proof. by rewrite ge_max ge_min lexx minmax orbT. Qed. + +Definition clamp_gele := (clamp_gemin, clamp_lemax). + +Lemma minmax_clamp x : min <= x <= max -> clamp x = x. +Proof. by case/andP => minx xmax; rewrite /clamp min_l ?max_l. Qed. + +Lemma clamp_id x : clamp (clamp x) = clamp x. +Proof. by rewrite minmax_clamp// !clamp_gele. Qed. + +Lemma clamp_min : clamp min = min. +Proof. by rewrite minmax_clamp// lexx minmax. Qed. + +Lemma clamp_max : clamp max = max. +Proof. by rewrite minmax_clamp// lexx minmax. Qed. + +End Clamp. + Module Order. Import Order. Definition default_display : disp_t.