From 4e6aacd94447ca20a0bda8ec5cc27e5afc8000e9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 17 Jan 2024 15:16:43 +0900 Subject: [PATCH] renamings, mv path lemmas to extra --- CHANGELOG_UNRELEASED.md | 7 +-- classical/mathcomp_extra.v | 51 ++++++++++++++++++++ theories/realfun.v | 96 ++++++++++---------------------------- 3 files changed, 78 insertions(+), 76 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index dc1490a23..d2ddab391 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -83,7 +83,7 @@ `itv_partitionLP`, `itv_partitionRP`, `in_itv_partition`, `notin_itv_partition`, `itv_partition_rev`, - + new lemmas `variationE`, `variation_nil`, + + new lemmas `variation_zip`, `variation_prev`, `variation_next`, `variation_nil`, `variation_ge0`, `variationN`, `variation_le`, `nondecreasing_variation`, `nonincreasing_variation`, `variationD`, `variation_itv_partitionLR`, `le_variation`, `variation_opp_rev`, `variation_rev_opp` @@ -102,7 +102,7 @@ `neg_tv_right_continuous`, `total_variation_opp`, `total_variation_left_continuous`, `total_variation_continuous`, `le_variation`, `variation_opp_rev`, `variation_rev_opp`, - `variation_monotone`, `variations_variation`, `variations_neq0`, + `variation_subseq`, `variations_variation`, `variations_neq0`, `variationsN`, `variationsxx`, `bounded_variationxx`, `bounded_variationD`, `bounded_variationN`, `bounded_variationl`, `bounded_variationr`, `variations_opp`, `nondecreasing_bounded_variation`, `total_variationxx`, @@ -114,9 +114,6 @@ `neg_TV_right_continuous`, `total_variation_opp`, `TV_left_continuous`, and `TV_continuous`. -- in `realfun.v`: - + lemmas `variation_prev`, `variation_next` - ### Changed - in `topology.v`: diff --git a/classical/mathcomp_extra.v b/classical/mathcomp_extra.v index 06e386232..6e9fc6b51 100644 --- a/classical/mathcomp_extra.v +++ b/classical/mathcomp_extra.v @@ -1476,3 +1476,54 @@ Qed. Definition monotonous d (T : porderType d) (pT : predType T) (A : pT) (f : T -> T) := {in A &, {mono f : x y / (x <= y)%O}} \/ {in A &, {mono f : x y /~ (x <= y)%O}}. + +(* NB: these lemmas have been introduced to develop the theory of bounded variation *) +Section path_lt. +Context d {T : orderType d}. +Implicit Types (a b c : T) (s : seq T). + +Lemma last_filterP a (P : pred T) s : + P a -> P (last a [seq x <- s | P x]). +Proof. +by elim: s a => //= t1 t2 ih a Pa; case: ifPn => //= Pt1; exact: ih. +Qed. + +Lemma path_lt_filter0 a s : path <%O a s -> [seq x <- 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_lt_filterT a s : path <%O a s -> [seq x <- 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 path_lt_head a b s : (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. + +(* TODO: this lemma feels a bit too technical, generalize? *) +Lemma path_lt_last_filter a b c s : + (a < c)%O -> (c < b)%O -> path <%O a s -> last a s = b -> + last c [seq x <- 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_lt_le_last a s : 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. diff --git a/theories/realfun.v b/theories/realfun.v index 7fec6f1a8..2330e55ed 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1562,57 +1562,6 @@ End is_derive_inverse. #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) => (eapply is_deriveV; first by []) : typeclass_instances. -Lemma last_filterP d {T : porderType d} (h : T) (P : pred T) t : - P h -> P (last h [seq x <- t | P x]). -Proof. -elim: t h => //= t1 t2 ih h hc. -by case: ifPn => //= t1c; exact: ih. -Qed. -Arguments last_filterP {d T h} P t. - -Lemma path_lt_filter0 d {T : orderType d} h (s : seq T) : - path <%O h s -> [seq x <- s | (x < h)%O] = [::]. -Proof. -move=> /lt_path_min/allP sh; rewrite -(filter_pred0 s). -apply: eq_in_filter => x xs. -by apply/negbTE; have := sh _ xs; rewrite ltNge; apply: contra => /ltW. -Qed. - -Lemma path_lt_filterT d {T : porderType d} h (s : seq T) : - path <%O h s -> [seq x <- s | (h < x)%O] = s. -Proof. -move=> /lt_path_min/allP sh; rewrite -[RHS](filter_predT s). -by apply: eq_in_filter => x xs; exact: sh. -Qed. - -Lemma path_lt_head d {T : porderType d} (a b : T) (s : seq T) : - (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 path_lt_last_filter d {T : porderType d} (a b c : T) (l : seq T) : - (a < c)%O -> (c < b)%O -> path <%O a l -> last a l = b -> - last c [seq x <- l | (c < x)%O] = b. -Proof. -elim/last_ind : l a b c => /= [|h t ih a b c ac cb]. - move=> a b c ac cb _ ?; subst b. - have := lt_trans ac cb. - by rewrite ltxx. -rewrite rcons_path => /andP[ah ht]. -rewrite last_rcons => htb. -by rewrite filter_rcons htb cb last_rcons. -Qed. - -Lemma path_lt_le_last d {T : porderType d} (i : T) (s : seq T) : - path <%O i s -> (i <= last i s)%O. -Proof. -elim: s i => // a [_ i /andP[/ltW//]|b t ih i/= /and3P[ia ab bt]] /=. -have /= := ih a. -rewrite ab bt => /(_ erefl). -by apply: le_trans; exact/ltW. -Qed. - Section interval_partition. Context {R : realType}. Implicit Type (a b : R) (s : seq R). @@ -1784,7 +1733,7 @@ Implicit Types (a b : R) (f g : R -> R). Definition variation a b f s := let F := f \o nth b (a :: s) in \sum_(0 <= n < size s) `|F n.+1 - F n|%R. -Lemma variationE a b f s : itv_partition a b s -> +Lemma variation_zip a b f s : itv_partition a b s -> variation a b f s = \sum_(x <- zip s (a :: s)) `|f x.1 - f x.2|. Proof. elim: s a b => // [a b|h t ih a b]. @@ -1795,6 +1744,7 @@ have /ih : itv_partition h b t by split => //; exact/eqP. by rewrite /variation => ->; rewrite !big_seq; apply/eq_bigr => r rt. Qed. +(* NB: not used yet but should allow for "term-by-term" comparisons *) Lemma variation_prev a b f s : itv_partition a b s -> variation a b f s = \sum_(x <- s) `|f x - f (prev (locked (a :: s)) x)|. Proof. @@ -1888,6 +1838,7 @@ rewrite addSnnS (addnC k) -cat_cons nth_cat/= -ltn_subRL subnn ltn0. by rewrite -(addnC k) addnK. Qed. +(* NB: this is the only lemma that uses variation_zip *) Lemma variation_itv_partitionLR a b c f s : a < c -> c < b -> itv_partition a b s -> variation a b f s <= variation a b f (itv_partitionL s c ++ itv_partitionR s c). @@ -1898,7 +1849,7 @@ rewrite /itv_partitionL [in leLHS](notin_itv_partition _ cl)//; last first. by apply: path_sorted; case: abs => + _; exact. rewrite -notin_itv_partition//; last first. by apply: path_sorted; case: abs => /= + _; exact. -rewrite !variationE//; last first. +rewrite !variation_zip//; last first. by apply: itv_partition_cat; [exact: (itv_partitionLP _ bc)|exact: (itv_partitionRP ac)]. rewrite [in leLHS](notin_itv_partition _ cl); last first. @@ -1983,29 +1934,32 @@ suff: (f \o -%R) \o -%R = f by move=> ->. by apply/funext=> ? /=; rewrite opprK. Qed. -Lemma variation_monotone a b f (s t : list R) : +Lemma variation_subseq a b f (s t : list R) : itv_partition a b s -> itv_partition a b t -> subseq s t -> variation a b f s <= variation a b f t. Proof. -elim: t s a; first by move=> ? ? ? [/=] _ /eqP -> /eqP ->. -move=> a s IH [] /= x; first by rewrite variation_nil // variation_ge0. -move=> t w /[dup] /itv_partition_cons itvxb /[dup] /itv_partition_le wb itvxt. -move=> /[dup] /itv_partition_cons itvas itvws. -have ? : a <= b by exact: (itv_partition_le itvas). -have wa : w < a by case: itvws => /= /andP []. -have waW : w <= a by exact: ltW. -case nXA: (x == a). - move/eqP:nXA itvxt itvxb => -> itvat itvt sub; rewrite -[_ :: t]cat1s -[_ :: s]cat1s. - by rewrite -?(@variationD _ _ a) // ?ler_add // ?(ltW wa) //; - [exact: IH | exact: itv_partition1 | exact: itv_partition1]. -move=> sub; rewrite -[_ :: s]cat1s -(@variationD _ _ a) => //; last exact: itv_partition1. +elim: t s a => [? ? ? /= _ /eqP ->//|a s IH [|x t] w]. + by rewrite variation_nil // variation_ge0. +move=> /[dup] /itv_partition_cons itvxb /[dup] /itv_partition_le wb itvxt. +move=> /[dup] /itv_partition_cons itvas itvws /=. +have ab : a <= b by exact: (itv_partition_le itvas). +have wa : w < a by case: itvws => /= /andP[]. +have waW : w <= a := ltW wa. +case: ifPn => [|] nXA. + move/eqP : nXA itvxt itvxb => -> itvat itvt /= ta. + rewrite -[_ :: t]cat1s -[_ :: s]cat1s. + rewrite -?(@variationD _ _ a)//; [|exact: itv_partition1..]. + by rewrite ler_add// IH. +move=> xts; rewrite -[_ :: s]cat1s -(@variationD _ _ a) => //; last first. + exact: itv_partition1. have [y [s' s'E]] : exists y s', s = y :: s'. - by case: {itvas itvws IH} s sub => // y s' ?; exists y, s'. -apply: le_trans; first apply IH => //. - case: itvws => /= /andP [_]; rewrite s'E /= => /andP [ay ys' lyb]. - by split => //; apply/ (path_lt_head wa)/andP; split => //. -by rewrite variationD => //; [exact: le_variation | exact: itv_partition1]. + by case: {itvas itvws IH} s xts => // y s' ?; exists y, s'. +apply: (@le_trans _ _ (variation w b f s)). + rewrite IH//. + case: itvws => /= /andP[_]; rewrite s'E /= => /andP[ay ys' lyb]. + by split => //; rewrite (path_lt_head wa)//= ys' andbT. +by rewrite variationD //; [exact: le_variation | exact: itv_partition1]. Qed. End variation.