diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 14ded411a..784d7e425 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -120,6 +120,43 @@ - in `subspace_topology.v`: + notation `{within _, continuous _}` (now uses `from_subspace`) +- moved from `realfun.v` to `numfun.v`: + + notations `nondecreasing_fun`, `nonincreasing_fun`, `increasing_fun`, + `decreasing_fun` + + generalized from `realType` to `numDomainType`: + * lemmas `nondecreasing_funN`, `nonincreasing_funN` + + generalized from `realType` to `porderType` + * definitions `itv_partition`, `itv_partitionL`, `itv_partitionR` + * lemmas `itv_partition_nil`, `itv_partition_cons`, `itv_partition1`, + `itv_partition_size_neq0`, `itv_partitionxx`, `itv_partition_le`, + `itv_partition_cat`, `itv_partition_nth_size`, `itv_partition_nth_ge`, + `itv_partition_nth_le`, `nondecreasing_fun_itv_partition` + + generalized from `realType` to `orderType` + * lemmas `itv_partitionLP`, `itv_partitionRP`, `in_itv_partition`, + `notin_itv_partition` + + generalize from `realType` to `numDomainType`: + * lemmas `nonincreasing_fun_itv_partition`, `itv_partition_rev` + +- moved from `realfun.v` to `numfun.v`: + + generalize from `realType` to `numDomainType` + * definition `variation` + * lemmas `variation_zip`, `variation_prev`, `variation_next`, + `variation_nil`, `variation_ge0`, `variationN`, `variation_le`, + `nondecreasing_variation`, `nonincreasing_variation`, + `variation_cat` (order of parameters also changed), `le_variation`, + `variation_opp_rev`, `variation_rev_opp` + + generalize from `realType` to `realDomainType` + * lemmas `variation_itv_partitionLR`, `variation_subseq` + +- moved from `realfun.v` to `numfun.v`: + + generalize from `realType` to `numDomainType` + * definition `variations`, `bounded_variation` + * lemmas `variations_variation`, `variations_neq0`, `variationsN`, + `variationsxx` + * lemmas `bounded_variationxx`, `bounded_variationD`, + `bounded_variationN`, `bounded_variationl`, `bounded_variationr`, + `variations_opp`, `nondecreasing_bounded_variation` + ### Renamed - in `probability.v`: @@ -153,6 +190,12 @@ - in `lebesgue_integral_theory/lebesgue_integrable.v` + lemma `null_set_integral` +- in `realfun.v`: + + generalized from `realType` to `realFieldType`: + * definition `total_variation` + * lemmas `total_variationxx`, `nondecreasing_total_variation`, + `total_variationN` + ### Deprecated - in `topology_structure.v`: diff --git a/theories/numfun.v b/theories/numfun.v index 33e840c4d..0ce6da7b8 100644 --- a/theories/numfun.v +++ b/theories/numfun.v @@ -1,4 +1,4 @@ -(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +(* mathcomp analysis (c) 2025 Inria and AIST. License: CeCILL-C. *) From HB Require Import structures. From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval finmap. From mathcomp Require Import mathcomp_extra boolp classical_sets fsbigop. @@ -13,15 +13,25 @@ From mathcomp Require Import sequences function_spaces. (* theorems such as Tietze's extension theorem. *) (* *) (* ``` *) -(* {nnfun T >-> R} == type of non-negative functions *) -(* f ^\+ == the function formed by the non-negative outputs *) -(* of f (from a type to the type of extended real *) -(* numbers) and 0 otherwise *) -(* rendered as f ⁺ with company-coq (U+207A) *) -(* f ^\- == the function formed by the non-positive outputs *) -(* of f and 0 o.w. *) -(* rendered as f ⁻ with company-coq (U+207B) *) -(* \1_ A == indicator function 1_A *) +(* 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 *) +(* itv_partition a b s == s is a partition of the interval `[a, b] *) +(* itv_partitionL s c == the left side of splitting a partition at c *) +(* itv_partitionR s c == the right side of splitting a partition at c *) +(* variation a b f s == the sum of f at all points in the partition s *) +(* variations a b f == the set of all variations of f between a and b *) +(* bounded_variation a b f == all variations of f are bounded *) +(* {nnfun T >-> R} == type of non-negative functions *) +(* f ^\+ == the function formed by the non-negative outputs *) +(* of f (from a type to the type of extended real *) +(* numbers) and 0 otherwise *) +(* rendered as f ⁺ with company-coq (U+207A) *) +(* f ^\- == the function formed by the non-positive outputs *) +(* of f and 0 o.w. *) +(* rendered as f ⁻ with company-coq (U+207B) *) +(* \1_ A == indicator function 1_A *) (* ``` *) (* *) (******************************************************************************) @@ -40,6 +50,546 @@ Import numFieldTopology.Exports. Local Open Scope classical_set_scope. Local Open Scope ring_scope. +Notation "'nondecreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n <= m)%O}) + (at level 10). +Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n >= m)%O}) + (at level 10). +Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O}) + (at level 10). +Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O}) + (at level 10). + +Lemma nondecreasing_funN {R : numDomainType} a b (f : R -> R) : + {in `[a, b] &, nondecreasing_fun f} <-> + {in `[a, b] &, nonincreasing_fun (\- f)}. +Proof. +split=> [h m n mab nab mn|h m n mab nab mn]; first by rewrite lerNr opprK h. +by rewrite -(opprK (f n)) -lerNr h. +Qed. + +Lemma nonincreasing_funN {R : numDomainType} a b (f : R -> R) : + {in `[a, b] &, nonincreasing_fun f} <-> + {in `[a, b] &, nondecreasing_fun (\- f)}. +Proof. +apply: iff_sym; apply: (iff_trans (nondecreasing_funN a b (\- f))). +rewrite [in X in _ <-> X](_ : f = \- (\- f))//. +by apply/funext => x /=; rewrite opprK. +Qed. + +Section interval_partition_porderType. +Context {d} {T : porderType d}. +Implicit Type (a b : T) (s : seq T). + +(** a :: s is a partition of the interval [a, b] *) +Definition itv_partition a b s := [/\ path <%O a s & last a s == b]. + +Lemma itv_partition_nil a b : itv_partition a b [::] -> a = b. +Proof. by move=> [_ /eqP <-]. Qed. + +Lemma itv_partition_cons a b x s : + itv_partition a b (x :: s) -> itv_partition x b s. +Proof. by rewrite /itv_partition/= => -[/andP[]]. Qed. + +Lemma itv_partition1 a b : (a < b)%O -> itv_partition a b [:: b]. +Proof. by rewrite /itv_partition /= => ->. Qed. + +Lemma itv_partition_size_neq0 a b s : + (size s > 0)%N -> itv_partition a b s -> (a < b)%O. +Proof. +elim: s a => // x [_ a _|h t ih a _]; rewrite /itv_partition /=. + by rewrite andbT => -[ax /eqP <-]. +move=> [] /andP[ax /andP[xy] ht /eqP tb]. +by rewrite (lt_trans ax)// ih// /itv_partition /= xy/= tb. +Qed. + +Lemma itv_partitionxx a s : itv_partition a a s -> s = [::]. +Proof. +case: s => //= h t [/= /andP[ah /lt_path_min/allP ht] /eqP hta]. +suff : (h < a)%O by move/lt_trans => /(_ _ ah); rewrite ltxx. +apply/ht; rewrite -hta. +by have := mem_last h t; rewrite inE hta lt_eqF. +Qed. + +Lemma itv_partition_le a b s : itv_partition a b s -> (a <= b)%O. +Proof. +case: s => [/itv_partition_nil ->//|h t /itv_partition_size_neq0 - /(_ _)/ltW]. +exact. +Qed. + +Lemma itv_partition_cat a b c s t : + itv_partition a b s -> itv_partition b c t -> itv_partition a c (s ++ t). +Proof. +rewrite /itv_partition => -[sa /eqP asb] [bt btc]. +by rewrite cat_path// sa /= last_cat asb. +Qed. + +Lemma itv_partition_nth_size def a b s : itv_partition a b s -> + nth def (a :: s) (size s) = b. +Proof. +by elim: s a => [a/= /itv_partition_nil//|y t ih a /= /itv_partition_cons/ih]. +Qed. + +Lemma itv_partition_nth_ge a b s m : (m < (size s).+1)%N -> + itv_partition a b s -> (a <= nth b (a :: s) m)%O. +Proof. +elim: m s a b => [s a b _//|n ih [//|h t] a b]. +rewrite ltnS => nh [/= /andP[ah ht] lb]. +by rewrite (le_trans (ltW ah))// ih. +Qed. + +Lemma itv_partition_nth_le a b s m : (m < (size s).+1)%N -> + itv_partition a b s -> (nth b (a :: s) m <= b)%O. +Proof. +elim: m s a => [s a _|n ih]; first exact: itv_partition_le. +by move=> [//|a h t /= nt] H; rewrite ih//; exact: itv_partition_cons H. +Qed. + +Lemma nondecreasing_fun_itv_partition a b f s : + {in `[a, b] &, nondecreasing_fun f} -> itv_partition a b s -> + let F : nat -> T := f \o nth b (a :: s) in + forall k, (k < size s)%N -> (F k <= F k.+1)%O. +Proof. +move=> ndf abs F k ks. +have [_] := nondecreasing_seqP F; apply => m n mn; rewrite /F/=. +have [ms|ms] := ltnP m (size s).+1; last first. + rewrite nth_default//. + have [|ns] := ltnP n (size s).+1; last by rewrite nth_default. + by move=> /(leq_ltn_trans mn); rewrite ltnS leqNgt ms. +have [ns|ns] := ltnP n (size s).+1; last first. + rewrite [in leRHS]nth_default//=; apply/ndf/itv_partition_nth_le => //. + by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge. + by rewrite in_itv/= lexx andbT; exact: (itv_partition_le abs). +move: abs; rewrite /itv_partition => -[] sa sab. +move: mn; rewrite leq_eqVlt => /predU1P[->//|mn]. +apply/ndf/ltW/sorted_ltn_nth => //=; last exact: lt_trans. + by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge. +by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge. +Qed. + +(** given a partition of [a, b] and c, returns a partition of [a, c] *) +Definition itv_partitionL s c := rcons [seq x <- s | (x < c)%O] c. + +(** given a partition of [a, b] and c, returns a partition of [c, b] *) +Definition itv_partitionR s c := [seq x <- s | (c < x)%O]. + +End interval_partition_porderType. + +Section interval_partition_orderType. +Context {d} {T : orderType d}. +Implicit Type (a b : T) (s : seq T). + +Lemma itv_partitionLP a b c s : (a < c)%O -> (c < b)%O -> itv_partition a b s -> + itv_partition a c (itv_partitionL s c). +Proof. +move=> ac bc [] al /eqP htb; split. + rewrite /itv_partitionL rcons_path/=; apply/andP; split. + by apply: path_filter => //; exact: lt_trans. + exact: (last_filterP [pred x | (x < c)%O]). +by rewrite /itv_partitionL last_rcons. +Qed. + +Lemma itv_partitionRP a b c s : (a < c)%O -> (c < b)%O -> itv_partition a b s -> + itv_partition c b (itv_partitionR s c). +Proof. +move=> ac cb [] sa /eqP alb; rewrite /itv_partition; split. + move: sa; rewrite lt_path_sortedE => /andP[allas ss]. + rewrite lt_path_sortedE filter_all/=. + by apply: sorted_filter => //; exact: lt_trans. +exact/eqP/(path_lt_last_filter ac). +Qed. + +Lemma in_itv_partition c s : sorted <%O s -> c \in s -> + s = itv_partitionL s c ++ itv_partitionR s c. +Proof. +elim: s c => // h t ih c /= ht. +rewrite inE => /predU1P[->{c}/=|ct]. + rewrite ltxx /itv_partitionL /= ltxx /itv_partitionR/= path_lt_filter0//=. + by rewrite path_lt_filterT. +rewrite /itv_partitionL/=; case: ifPn => [hc|]. + by rewrite ltNge (ltW hc)/= /= [in LHS](ih _ _ ct)//; exact: path_sorted ht. +rewrite -leNgt le_eqVlt => /predU1P[ch|ch]. + by rewrite ch ltxx path_lt_filter0//= /itv_partitionR path_lt_filterT. +move: ht; rewrite lt_path_sortedE => /andP[/allP/(_ _ ct)]. +by move=> /lt_trans-/(_ _ ch); rewrite ltxx. +Qed. + +Lemma notin_itv_partition c s : sorted <%O s -> c \notin s -> + s = [seq x <- s | (x < c)%O] ++ itv_partitionR s c. +Proof. +elim: s c => // h t ih c /= ht. +rewrite inE negb_or => /andP[]; rewrite neq_lt => /orP[ch|ch] ct. + rewrite ch ltNge (ltW ch)/= path_lt_filter0/= /itv_partitionR; last first. + exact: path_lt_head ht. + by rewrite path_lt_filterT//; exact: path_lt_head ht. +by rewrite ch/= ltNge (ltW ch)/= -ih//; exact: path_sorted ht. +Qed. + +End interval_partition_orderType. + +Section interval_partition_numDomainType. +Context {R : numDomainType}. +Implicit Type (a b : R) (s : seq R). + +Lemma nonincreasing_fun_itv_partition a b f s : + {in `[a, b] &, nonincreasing_fun f} -> itv_partition a b s -> + let F : nat -> R := f \o nth b (a :: s) in + forall k, (k < size s)%N -> (F k.+1 <= F k)%O. +Proof. +move/nonincreasing_funN => ndNf abs F k ks; rewrite -(opprK (F k)) lerNr. +exact: (nondecreasing_fun_itv_partition ndNf abs). +Qed. + +Lemma itv_partition_rev a b s : itv_partition a b s -> + itv_partition (- b) (- a) (rev (belast (- a) (map -%R s))). +Proof. +move=> [sa /eqP alb]; split. + rewrite (_ : - b = last (- a) (map -%R s)); last by rewrite last_map alb. + rewrite rev_path// path_map. + by apply: sub_path sa => x y xy/=; rewrite ltrNr opprK. +case: s sa alb => [_ <-//|h t] /= /andP[ah ht] <-{b}. +by rewrite rev_cons last_rcons. +Qed. + +End interval_partition_numDomainType. + +Section variation_numDomainType. +Context {R : numDomainType}. +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 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]. + by rewrite /itv_partition /= => -[_ /eqP <-]; rewrite /variation/= !big_nil. +rewrite /itv_partition /variation => -[]/= /andP[ah ht] /eqP htb. +rewrite big_nat_recl//= big_cons/=; congr +%R. +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. +move=> [] sa /eqP asb; rewrite /variation [in LHS]/= (big_nth b) !big_nat. +apply: eq_bigr => i /andP[_ si]; congr (`| _ - f _ |). +rewrite -lock. +rewrite prev_nth inE gt_eqF; last first. + rewrite -[a]/(nth b (a :: s) 0) -[ltRHS]/(nth b (a :: s) i.+1). + exact: lt_sorted_ltn_nth. +rewrite orFb mem_nth// index_uniq//. + by apply: set_nth_default => /=; rewrite ltnS ltnW. +by apply: (sorted_uniq lt_trans) => //; apply: path_sorted sa. +Qed. + +Lemma variation_next a b f s : itv_partition a b s -> + variation a b f s = + \sum_(x <- belast a s) `|f (next (locked (a :: s)) x) - f x|. +Proof. +move=> [] sa /eqP asb; rewrite /variation [in LHS]/= (big_nth b) !big_nat. +rewrite size_belast; apply: eq_bigr => i /andP[_ si]. +congr (`| f _ - f _ |); last first. + by rewrite lastI -cats1 nth_cat size_belast// si. +rewrite -lock next_nth. +rewrite {1}lastI mem_rcons inE mem_nth ?size_belast// orbT. +rewrite lastI -cats1 index_cat mem_nth ?size_belast//. +rewrite index_uniq ?size_belast//. + exact: set_nth_default. +have /lt_sorted_uniq : sorted <%R (a :: s) by []. +by rewrite lastI rcons_uniq => /andP[]. +Qed. + +Lemma variation_nil a b f : variation a b f [::] = 0. +Proof. by rewrite /variation/= big_nil. Qed. + +Lemma variation_ge0 a b f s : 0 <= variation a b f s. +Proof. exact/sumr_ge0. Qed. + +Lemma variationN a b f s : variation a b (\- f) s = variation a b f s. +Proof. +by rewrite /variation; apply: eq_bigr => k _ /=; rewrite -opprD normrN. +Qed. + +Lemma variation_le a b f g s : + variation a b (f \+ g)%R s <= variation a b f s + variation a b g s. +Proof. +rewrite [in leRHS]/variation -big_split/=. +apply: ler_sum => k _; apply: le_trans; last exact: ler_normD. +by rewrite /= addrACA -opprD. +Qed. + +Lemma nondecreasing_variation a b f s : {in `[a, b] &, nondecreasing_fun f} -> + itv_partition a b s -> variation a b f s = f b - f a. +Proof. +move=> ndf abs; rewrite /variation; set F : nat -> R := f \o nth _ (a :: s). +transitivity (\sum_(0 <= n < size s) (F n.+1 - F n)). + rewrite !big_nat; apply: eq_bigr => k; rewrite leq0n/= => ks. + by rewrite ger0_norm// subr_ge0; exact: nondecreasing_fun_itv_partition. +by rewrite telescope_sumr// /F/= (itv_partition_nth_size _ abs). +Qed. + +Lemma nonincreasing_variation a b f s : {in `[a, b] &, nonincreasing_fun f} -> + itv_partition a b s -> variation a b f s = f a - f b. +Proof. +move=> /nonincreasing_funN ndNf abs; have := nondecreasing_variation ndNf abs. +by rewrite opprK addrC => <-; rewrite variationN. +Qed. + +Lemma variation_cat c a b f s t : a <= c -> c <= b -> + itv_partition a c s -> itv_partition c b t -> + variation a b f (s ++ t) = variation a c f s + variation c b f t. +Proof. +rewrite le_eqVlt => /predU1P[<-{c} cb|ac]. + by move=> /itv_partitionxx ->; rewrite variation_nil add0r. +rewrite le_eqVlt => /predU1P[<-{b}|cb]. + by move=> ? /itv_partitionxx ->; rewrite variation_nil addr0 cats0. +move=> acs cbt; rewrite /variation /= [in LHS]/index_iota subn0 size_cat. +rewrite iotaD add0n big_cat/= -[in X in X + _ = _](subn0 (size s)); congr +%R. + rewrite -/(index_iota 0 (size s)) 2!big_nat. + apply: eq_bigr => k /[!leq0n] /= ks. + rewrite nth_cat ks -cat_cons nth_cat /= ltnS (ltnW ks). + by rewrite !(set_nth_default b c)//= ltnS ltnW. +rewrite -[in LHS](addnK (size s) (size t)). +rewrite -/(index_iota (size s) (size t + size s)). +rewrite -{1}[in LHS](add0n (size s)) big_addn addnK 2!big_nat; apply: eq_bigr. +move=> k /[!leq0n]/= kt. +rewrite nth_cat {1}(addnC k) -ltn_subRL subnn ltn0 addnK. +case: k kt => [t0 /=|k kt]. + rewrite add0n -cat_cons nth_cat/= ltnS leqnn -last_nth. + by case: acs => _ /eqP ->. +rewrite addSnnS (addnC k) -cat_cons nth_cat/= -ltn_subRL subnn ltn0. +by rewrite -(addnC k) addnK. +Qed. + +Lemma le_variation a b f s x : variation a b f s <= variation a b f (x :: s). +Proof. +case: s => [|h t]. + by rewrite variation_nil /variation/= big_nat_recl//= big_nil addr0. +rewrite /variation/= !big_nat_recl//= addrA lerD2r. +by rewrite -(subrKA (f x)) addrC ler_normD. +Qed. + +Lemma variation_opp_rev a b f s : itv_partition a b s -> + variation a b f s = + variation (- b) (- a) (f \o -%R) (rev (belast (- a) (map -%R s))). +Proof. +move=> abl; rewrite belast_map /variation /= [LHS]big_nat_rev/= add0n. +rewrite size_rev size_map size_belast 2!big_nat. +apply: eq_bigr => k; rewrite leq0n /= => ks. +rewrite nth_rev ?size_map ?size_belast// [in RHS]distrC. +rewrite (nth_map a); last first. + by rewrite size_belast ltn_subLR// addSn ltnS leq_addl. +rewrite opprK -rev_rcons nth_rev ?size_rcons ?size_map ?size_belast 1?ltnW//. +rewrite subSn// -map_rcons (nth_map b) ?size_rcons ?size_belast; last first. + by rewrite ltnS ltn_subLR// addSn ltnS leq_addl. +rewrite opprK nth_rcons size_belast -subSn// subSS. +rewrite (ltn_subLR _ (ltnW ks)) if_same. +case: k => [|k] in ks *. + rewrite add0n ltnn subn1 (_ : nth b s _ = b); last first. + case: abl ks => _. + elim/last_ind : s => // h t _; rewrite last_rcons => /eqP -> _. + by rewrite nth_rcons size_rcons ltnn eqxx. + rewrite (_ : nth b (a :: s) _ = nth a (belast a s) (size s).-1)//. + case: abl ks => _. + elim/last_ind : s => // h t _; rewrite last_rcons => /eqP -> _. + rewrite belast_rcons size_rcons/= -rcons_cons nth_rcons/= ltnS leqnn. + exact: set_nth_default. +rewrite addSn ltnS leq_addl//; congr (`| f _ - f _ |). + elim/last_ind : s ks {abl} => // h t _; rewrite size_rcons ltnS => kh. + rewrite belast_rcons nth_rcons subSS ltn_subLR//. + by rewrite addSn ltnS leq_addl// subSn. +elim/last_ind : s ks {abl} => // h t _; rewrite size_rcons ltnS => kh. +rewrite belast_rcons subSS -rcons_cons nth_rcons /= ltn_subLR//. +rewrite addnS ltnS leq_addl; apply: set_nth_default => //. +by rewrite /= ltnS leq_subLR leq_addl. +Qed. + +Lemma variation_rev_opp a b f s : itv_partition (- b) (- a) s -> + variation a b f (rev (belast b (map -%R s))) = + variation (- b) (- a) (f \o -%R) s. +Proof. +move=> abs; rewrite [in RHS]variation_opp_rev ?opprK//. +suff: (f \o -%R) \o -%R = f by move=> ->. +by apply/funext=> ? /=; rewrite opprK. +Qed. + +End variation_numDomainType. +#[deprecated(since="mathcomp-analysis 1.12.0", note="use `variation_cat` instead")] +Notation variationD := variation_cat (only parsing). + +Section variation_realDomainType. +Context {R : realDomainType}. +Implicit Types (a b : R) (f g : R -> R). + +(* 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). +Proof. +move=> ac bc abs; have [cl|cl] := boolP (c \in s). + by rewrite -in_itv_partition//; case: abs => /path_sorted. +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 !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. + by apply: path_sorted; case: abs => + _; exact. +set L := [seq x <- s | x < c]. +rewrite -cats1 -catA. +move: L => L. +set B := itv_partitionR s c. +move: B => B. +elim/last_ind : L => [|L0 L1 _]. + rewrite !cat0s /=; case: B => [|B0 B1]. + by rewrite big_nil big_cons/= big_nil addr0. + by rewrite !big_cons/= addrA lerD// -(subrKA (f c)) [leRHS]addrC ler_normD. +rewrite -cats1. +rewrite (_ : a :: _ ++ B = (a :: L0) ++ [:: L1] ++ B)//; last first. + by rewrite -!catA -cat_cons. +rewrite zip_cat; last by rewrite cats1 size_rcons. +rewrite (_ : a :: _ ++ _ ++ B = (a :: L0) ++ [:: L1] ++ [:: c] ++ B); last first. + by rewrite -!catA -cat_cons. +rewrite zip_cat; last by rewrite cats1 size_rcons. +rewrite !big_cat lerD//. +case: B => [|B0 B1]. + by rewrite /= big_nil big_cons big_nil addr0. +rewrite -cat1s zip_cat// catA. +rewrite (_ : [:: L1] ++ _ ++ B1 = ([:: L1] ++ [:: c]) ++ [:: B0] ++ B1); last first. + by rewrite catA. +rewrite zip_cat// !big_cat lerD//= !big_cons !big_nil !addr0/= [leRHS]addrC. +by rewrite (le_trans _ (ler_normD _ _))// subrKA. +Qed. + +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 => [? ? ? /= _ /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 ?(@variation_cat _ a)//; [|exact: itv_partition1..]. + by rewrite lerD// IH. +move=> xts; rewrite -[_ :: s]cat1s (@variation_cat _ a) => //; last first. + exact: itv_partition1. +have [y [s' s'E]] : exists y s', s = y :: s'. + 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 -variation_cat//; [exact: le_variation | exact: itv_partition1]. +Qed. + +End variation_realDomainType. + +Section bounded_variation. +Context {R : numDomainType}. +Implicit Type (a b : R) (f : R -> R). + +Definition variations a b f := [set variation a b f l | l in itv_partition a b]. + +Lemma variations_variation a b f s : itv_partition a b s -> + variations a b f (variation a b f s). +Proof. by move=> abs; exists s. Qed. + +Lemma variations_neq0 a b f : a < b -> variations a b f !=set0. +Proof. +move=> ab; exists (variation a b f [:: b]); exists [:: b] => //. +exact: itv_partition1. +Qed. + +Lemma variationsN a b f : variations a b (\- f) = variations a b f. +Proof. +apply/seteqP; split => [_ [s abs] <-|r [s abs]]. + by rewrite variationN; exact: variations_variation. +by rewrite -variationN => <-; exact: variations_variation. +Qed. + +Lemma variationsxx a f : variations a a f = [set 0]. +Proof. +apply/seteqP; split => [x [_ /itv_partitionxx ->]|x ->]. + by rewrite /variation big_nil => <-. +by exists [::] => //=; rewrite /variation /= big_nil. +Qed. + +Definition bounded_variation a b f := has_ubound (variations a b f). + +Notation BV := bounded_variation. + +Lemma bounded_variationxx a f : BV a a f. +Proof. by exists 0 => r; rewrite variationsxx => ->. Qed. + +Lemma bounded_variationD a b f g : a < b -> + BV a b f -> BV a b g -> BV a b (f \+ g). +Proof. +move=> ab [r abfr] [s abgs]; exists (r + s) => _ [l abl] <-. +apply: le_trans; first exact: variation_le. +rewrite lerD//. +- by apply: abfr; exact: variations_variation. +- by apply: abgs; exact: variations_variation. +Qed. + +Lemma bounded_variationN a b f : BV a b f -> BV a b (\- f). +Proof. by rewrite /bounded_variation variationsN. Qed. + +Lemma bounded_variationl a c b f : a <= c -> c <= b -> BV a b f -> BV a c f. +Proof. +rewrite le_eqVlt => /predU1P[<-{c} ? ?|ac]; first exact: bounded_variationxx. +rewrite le_eqVlt => /predU1P[<-{b}//|cb]. +move=> [x Hx]; exists x => _ [s acs] <-. +rewrite (@le_trans _ _ (variation a b f (rcons s b)))//; last first. + apply/Hx/variations_variation; case: acs => sa /eqP asc. + by rewrite /itv_partition rcons_path last_rcons sa/= asc. +rewrite {2}/variation size_rcons -[leLHS]addr0 big_nat_recr//= lerD//. +rewrite /variation !big_nat ler_sum// => k; rewrite leq0n /= => ks. +rewrite nth_rcons// ks -cats1 -cat_cons nth_cat /= ltnS (ltnW ks). +by rewrite ![in leRHS](set_nth_default c)//= ltnS ltnW. +Qed. + +Lemma bounded_variationr a c b f : a <= c -> c <= b -> BV a b f -> BV c b f. +Proof. +rewrite le_eqVlt => /predU1P[<-{c}//|ac]. +rewrite le_eqVlt => /predU1P[<-{b} ?|cb]; first exact: bounded_variationxx. +move=> [x Hx]; exists x => _ [s cbs] <-. +rewrite (@le_trans _ _ (variation a b f (c :: s)))//; last first. + apply/Hx/variations_variation; case: cbs => cs csb. + by rewrite /itv_partition/= ac/= cs. +by rewrite {2}/variation/= -[leLHS]add0r big_nat_recl//= lerD. +Qed. + +Lemma variations_opp a b f : + variations (- b) (- a) (f \o -%R) = variations a b f. +Proof. +rewrite eqEsubset; split=> [_ [s bas <-]| _ [s abs <-]]. + eexists; last exact: variation_rev_opp. + by move/itv_partition_rev : bas; rewrite !opprK. +eexists; last by exact/esym/variation_opp_rev. +exact: itv_partition_rev abs. +Qed. + +Lemma nondecreasing_bounded_variation a b f : + {in `[a, b] &, {homo f : x y / x <= y}} -> BV a b f. +Proof. +move=> incf; exists (f b - f a) => ? [l pabl <-]; rewrite le_eqVlt. +by rewrite nondecreasing_variation// eqxx. +Qed. + +End bounded_variation. + HB.mixin Record isNonNegFun (aT : Type) (rT : numDomainType) (f : aT -> rT) := { fun_ge0 : forall x, (0 <= f x)%R }. diff --git a/theories/realfun.v b/theories/realfun.v index 5a15e7de4..c22658677 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -5,7 +5,7 @@ From mathcomp Require Import archimedean interval. From mathcomp Require Import mathcomp_extra boolp classical_sets functions. From mathcomp Require Import cardinality contra ereal reals interval_inference. From mathcomp Require Import topology prodnormedzmodule tvs normedtype derive. -From mathcomp Require Import sequences real_interval. +From mathcomp Require Import sequences real_interval numfun. (**md**************************************************************************) (* # Real-valued functions over reals *) @@ -15,10 +15,6 @@ From mathcomp Require Import sequences real_interval. (* L'Hopital's rule). *) (* *) (* ``` *) -(* 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 *) (* *) (* derivable_oo_LRcontinuous f x y == f is derivable in `]x, y[ and *) (* continuous up to the boundary, i.e., *) @@ -28,12 +24,6 @@ From mathcomp Require Import sequences real_interval. (* derivable_Nyo_Lcontinuous f x == f is derivable in `]-oo, x[ and *) (* f @ x^'- --> f x *) (* *) -(* itv_partition a b s == s is a partition of the interval `[a, b] *) -(* itv_partitionL s c == the left side of splitting a partition at c *) -(* itv_partitionR s c == the right side of splitting a partition at c *) -(* variation a b f s == the sum of f at all points in the partition s *) -(* variations a b f == the set of all variations of f between a and b *) -(* bounded_variation a b f == all variations of f are bounded *) (* total_variation a b f == the sup over all variations of f from a to b *) (* neg_tv a f x == the decreasing component of f *) (* pos_tv a f x == the increasing component of f *) @@ -62,32 +52,6 @@ Local Open Scope ring_scope. Import numFieldNormedType.Exports. -Notation "'nondecreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n <= m)%O}) - (at level 10). -Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%O >-> (n >= m)%O}) - (at level 10). -Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O}) - (at level 10). -Notation "'decreasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n >= m)%O}) - (at level 10). - -Lemma nondecreasing_funN {R : realType} a b (f : R -> R) : - {in `[a, b] &, nondecreasing_fun f} <-> - {in `[a, b] &, nonincreasing_fun (\- f)}. -Proof. -split=> [h m n mab nab mn|h m n mab nab mn]; first by rewrite lerNr opprK h. -by rewrite -(opprK (f n)) -lerNr h. -Qed. - -Lemma nonincreasing_funN {R : realType} a b (f : R -> R) : - {in `[a, b] &, nonincreasing_fun f} <-> - {in `[a, b] &, nondecreasing_fun (\- f)}. -Proof. -apply: iff_sym; apply: (iff_trans (nondecreasing_funN a b (\- f))). -rewrite [in X in _ <-> X](_ : f = \- (\- f))//. -by apply/funext => x /=; rewrite opprK. -Qed. - Section fun_cvg. Section fun_cvg_realFieldType. @@ -1919,515 +1883,44 @@ Unshelve. all: by end_near. Qed. #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) => (eapply is_deriveV; first by []) : typeclass_instances. -Section interval_partition. -Context {R : realType}. -Implicit Type (a b : R) (s : seq R). - -(** a :: s is a partition of the interval [a, b] *) -Definition itv_partition a b s := [/\ path <%R a s & last a s == b]. - -Lemma itv_partition_nil a b : itv_partition a b [::] -> a = b. -Proof. by move=> [_ /eqP <-]. Qed. - -Lemma itv_partition_cons a b x s : - itv_partition a b (x :: s) -> itv_partition x b s. -Proof. by rewrite /itv_partition/= => -[/andP[]]. Qed. - -Lemma itv_partition1 a b : a < b -> itv_partition a b [:: b]. -Proof. by rewrite /itv_partition /= => ->. Qed. - -Lemma itv_partition_size_neq0 a b s : - (size s > 0)%N -> itv_partition a b s -> a < b. -Proof. -elim: s a => // x [_ a _|h t ih a _]; rewrite /itv_partition /=. - by rewrite andbT => -[ax /eqP <-]. -move=> [] /andP[ax /andP[xy] ht /eqP tb]. -by rewrite (lt_trans ax)// ih// /itv_partition /= xy/= tb. -Qed. - -Lemma itv_partitionxx a s : itv_partition a a s -> s = [::]. -Proof. -case: s => //= h t [/= /andP[ah /lt_path_min/allP ht] /eqP hta]. -suff : h < a by move/lt_trans => /(_ _ ah); rewrite ltxx. -apply/ht; rewrite -hta. -by have := mem_last h t; rewrite inE hta lt_eqF. -Qed. - -Lemma itv_partition_le a b s : itv_partition a b s -> a <= b. -Proof. -case: s => [/itv_partition_nil ->//|h t /itv_partition_size_neq0 - /(_ _)/ltW]. -exact. -Qed. - -Lemma itv_partition_cat a b c s t : - itv_partition a b s -> itv_partition b c t -> itv_partition a c (s ++ t). -Proof. -rewrite /itv_partition => -[sa /eqP asb] [bt btc]. -by rewrite cat_path// sa /= last_cat asb. -Qed. - -Lemma itv_partition_nth_size def a b s : itv_partition a b s -> - nth def (a :: s) (size s) = b. -Proof. -by elim: s a => [a/= /itv_partition_nil//|y t ih a /= /itv_partition_cons/ih]. -Qed. - -Lemma itv_partition_nth_ge a b s m : (m < (size s).+1)%N -> - itv_partition a b s -> a <= nth b (a :: s) m. -Proof. -elim: m s a b => [s a b _//|n ih [//|h t] a b]. -rewrite ltnS => nh [/= /andP[ah ht] lb]. -by rewrite (le_trans (ltW ah))// ih. -Qed. - -Lemma itv_partition_nth_le a b s m : (m < (size s).+1)%N -> - itv_partition a b s -> nth b (a :: s) m <= b. -Proof. -elim: m s a => [s a _|n ih]; first exact: itv_partition_le. -by move=> [//|a h t /= nt] H; rewrite ih//; exact: itv_partition_cons H. -Qed. - -Lemma nondecreasing_fun_itv_partition a b f s : - {in `[a, b] &, nondecreasing_fun f} -> itv_partition a b s -> - let F : nat -> R := f \o nth b (a :: s) in - forall k, (k < size s)%N -> F k <= F k.+1. -Proof. -move=> ndf abs F k ks. -have [_] := nondecreasing_seqP F; apply => m n mn; rewrite /F/=. -have [ms|ms] := ltnP m (size s).+1; last first. - rewrite nth_default//. - have [|ns] := ltnP n (size s).+1; last by rewrite nth_default. - by move=> /(leq_ltn_trans mn); rewrite ltnS leqNgt ms. -have [ns|ns] := ltnP n (size s).+1; last first. - rewrite [in leRHS]nth_default//=; apply/ndf/itv_partition_nth_le => //. - by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge. - by rewrite in_itv/= lexx andbT; exact: (itv_partition_le abs). -move: abs; rewrite /itv_partition => -[] sa sab. -move: mn; rewrite leq_eqVlt => /predU1P[->//|mn]. -apply/ndf/ltW/sorted_ltn_nth => //=; last exact: lt_trans. - by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge. -by rewrite in_itv/= itv_partition_nth_le// andbT itv_partition_nth_ge. -Qed. - -Lemma nonincreasing_fun_itv_partition a b f s : - {in `[a, b] &, nonincreasing_fun f} -> itv_partition a b s -> - let F : nat -> R := f \o nth b (a :: s) in - forall k, (k < size s)%N -> F k.+1 <= F k. -Proof. -move/nonincreasing_funN => ndNf abs F k ks; rewrite -(opprK (F k)) lerNr. -exact: (nondecreasing_fun_itv_partition ndNf abs). -Qed. - -(** given a partition of [a, b] and c, returns a partition of [a, c] *) -Definition itv_partitionL s c := rcons [seq x <- s | x < c] c. - -Lemma itv_partitionLP a b c s : a < c -> c < b -> itv_partition a b s -> - itv_partition a c (itv_partitionL s c). -Proof. -move=> ac bc [] al /eqP htb; split. - rewrite /itv_partitionL rcons_path/=; apply/andP; split. - by apply: path_filter => //; exact: lt_trans. - exact: (last_filterP [pred x | x < c]). -by rewrite /itv_partitionL last_rcons. -Qed. - -(** given a partition of [a, b] and c, returns a partition of [c, b] *) -Definition itv_partitionR s c := [seq x <- s | c < x]. - -Lemma itv_partitionRP a b c s : a < c -> c < b -> itv_partition a b s -> - itv_partition c b (itv_partitionR s c). -Proof. -move=> ac cb [] sa /eqP alb; rewrite /itv_partition; split. - move: sa; rewrite lt_path_sortedE => /andP[allas ss]. - rewrite lt_path_sortedE filter_all/=. - by apply: sorted_filter => //; exact: lt_trans. -exact/eqP/(path_lt_last_filter ac). -Qed. - -Lemma in_itv_partition c s : sorted <%R s -> c \in s -> - s = itv_partitionL s c ++ itv_partitionR s c. -Proof. -elim: s c => // h t ih c /= ht. -rewrite inE => /predU1P[->{c}/=|ct]. - rewrite ltxx /itv_partitionL /= ltxx /itv_partitionR/= path_lt_filter0//=. - by rewrite path_lt_filterT. -rewrite /itv_partitionL/=; case: ifPn => [hc|]. - by rewrite ltNge (ltW hc)/= /= [in LHS](ih _ _ ct)//; exact: path_sorted ht. -rewrite -leNgt le_eqVlt => /predU1P[ch|ch]. - by rewrite ch ltxx path_lt_filter0//= /itv_partitionR path_lt_filterT. -move: ht; rewrite lt_path_sortedE => /andP[/allP/(_ _ ct)]. -by move=> /lt_trans-/(_ _ ch); rewrite ltxx. -Qed. - -Lemma notin_itv_partition c s : sorted <%R s -> c \notin s -> - s = [seq x <- s | x < c] ++ itv_partitionR s c. -Proof. -elim: s c => // h t ih c /= ht. -rewrite inE negb_or => /andP[]; rewrite neq_lt => /orP[ch|ch] ct. - rewrite ch ltNge (ltW ch)/= path_lt_filter0/= /itv_partitionR; last first. - exact: path_lt_head ht. - by rewrite path_lt_filterT//; exact: path_lt_head ht. -by rewrite ch/= ltNge (ltW ch)/= -ih//; exact: path_sorted ht. -Qed. - -Lemma itv_partition_rev a b s : itv_partition a b s -> - itv_partition (- b) (- a) (rev (belast (- a) (map -%R s))). -Proof. -move=> [sa /eqP alb]; split. - rewrite (_ : - b = last (- a) (map -%R s)); last by rewrite last_map alb. - rewrite rev_path// path_map. - by apply: sub_path sa => x y xy/=; rewrite ltrNr opprK. -case: s sa alb => [_ <-//|h t] /= /andP[ah ht] <-{b}. -by rewrite rev_cons last_rcons. -Qed. - -End interval_partition. - -Section variation. -Context {R : realType}. -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 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]. - by rewrite /itv_partition /= => -[_ /eqP <-]; rewrite /variation/= !big_nil. -rewrite /itv_partition /variation => -[]/= /andP[ah ht] /eqP htb. -rewrite big_nat_recl//= big_cons/=; congr +%R. -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. -move=> [] sa /eqP asb; rewrite /variation [in LHS]/= (big_nth b) !big_nat. -apply: eq_bigr => i /andP[_ si]; congr (`| _ - f _ |). -rewrite -lock. -rewrite prev_nth inE gt_eqF; last first. - rewrite -[a]/(nth b (a :: s) 0) -[ltRHS]/(nth b (a :: s) i.+1). - exact: lt_sorted_ltn_nth. -rewrite orFb mem_nth// index_uniq//. - by apply: set_nth_default => /=; rewrite ltnS ltnW. -by apply: (sorted_uniq lt_trans) => //; apply: path_sorted sa. -Qed. - -Lemma variation_next a b f s : itv_partition a b s -> - variation a b f s = - \sum_(x <- belast a s) `|f (next (locked (a :: s)) x) - f x|. -Proof. -move=> [] sa /eqP asb; rewrite /variation [in LHS]/= (big_nth b) !big_nat. -rewrite size_belast; apply: eq_bigr => i /andP[_ si]. -congr (`| f _ - f _ |); last first. - by rewrite lastI -cats1 nth_cat size_belast// si. -rewrite -lock next_nth. -rewrite {1}lastI mem_rcons inE mem_nth ?size_belast// orbT. -rewrite lastI -cats1 index_cat mem_nth ?size_belast//. -rewrite index_uniq ?size_belast//. - exact: set_nth_default. -have /lt_sorted_uniq : sorted <%R (a :: s) by []. -by rewrite lastI rcons_uniq => /andP[]. -Qed. - -Lemma variation_nil a b f : variation a b f [::] = 0. -Proof. by rewrite /variation/= big_nil. Qed. - -Lemma variation_ge0 a b f s : 0 <= variation a b f s. -Proof. exact/sumr_ge0. Qed. - -Lemma variationN a b f s : variation a b (\- f) s = variation a b f s. -Proof. -by rewrite /variation; apply: eq_bigr => k _ /=; rewrite -opprD normrN. -Qed. - -Lemma variation_le a b f g s : - variation a b (f \+ g)%R s <= variation a b f s + variation a b g s. -Proof. -rewrite [in leRHS]/variation -big_split/=. -apply: ler_sum => k _; apply: le_trans; last exact: ler_normD. -by rewrite /= addrACA -opprD. -Qed. - -Lemma nondecreasing_variation a b f s : {in `[a, b] &, nondecreasing_fun f} -> - itv_partition a b s -> variation a b f s = f b - f a. -Proof. -move=> ndf abs; rewrite /variation; set F : nat -> R := f \o nth _ (a :: s). -transitivity (\sum_(0 <= n < size s) (F n.+1 - F n)). - rewrite !big_nat; apply: eq_bigr => k; rewrite leq0n/= => ks. - by rewrite ger0_norm// subr_ge0; exact: nondecreasing_fun_itv_partition. -by rewrite telescope_sumr// /F/= (itv_partition_nth_size _ abs). -Qed. - -Lemma nonincreasing_variation a b f s : {in `[a, b] &, nonincreasing_fun f} -> - itv_partition a b s -> variation a b f s = f a - f b. -Proof. -move=> /nonincreasing_funN ndNf abs; have := nondecreasing_variation ndNf abs. -by rewrite opprK addrC => <-; rewrite variationN. -Qed. - -Lemma variation_cat a b c f s t : a <= c -> c <= b -> - itv_partition a c s -> itv_partition c b t -> - variation a b f (s ++ t) = variation a c f s + variation c b f t. -Proof. -rewrite le_eqVlt => /predU1P[<-{c} cb|ac]. - by move=> /itv_partitionxx ->; rewrite variation_nil add0r. -rewrite le_eqVlt => /predU1P[<-{b}|cb]. - by move=> ? /itv_partitionxx ->; rewrite variation_nil addr0 cats0. -move=> acs cbt; rewrite /variation /= [in LHS]/index_iota subn0 size_cat. -rewrite iotaD add0n big_cat/= -[in X in X + _ = _](subn0 (size s)); congr +%R. - rewrite -/(index_iota 0 (size s)) 2!big_nat. - apply: eq_bigr => k /[!leq0n] /= ks. - rewrite nth_cat ks -cat_cons nth_cat /= ltnS (ltnW ks). - by rewrite !(set_nth_default b c)//= ltnS ltnW. -rewrite -[in LHS](addnK (size s) (size t)). -rewrite -/(index_iota (size s) (size t + size s)). -rewrite -{1}[in LHS](add0n (size s)) big_addn addnK 2!big_nat; apply: eq_bigr. -move=> k /[!leq0n]/= kt. -rewrite nth_cat {1}(addnC k) -ltn_subRL subnn ltn0 addnK. -case: k kt => [t0 /=|k kt]. - rewrite add0n -cat_cons nth_cat/= ltnS leqnn -last_nth. - by case: acs => _ /eqP ->. -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). -Proof. -move=> ac bc abs; have [cl|cl] := boolP (c \in s). - by rewrite -in_itv_partition//; case: abs => /path_sorted. -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 !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. - by apply: path_sorted; case: abs => + _; exact. -set L := [seq x <- s | x < c]. -rewrite -cats1 -catA. -move: L => L. -set B := itv_partitionR s c. -move: B => B. -elim/last_ind : L => [|L0 L1 _]. - rewrite !cat0s /=; case: B => [|B0 B1]. - by rewrite big_nil big_cons/= big_nil addr0. - by rewrite !big_cons/= addrA lerD// -(subrKA (f c)) [leRHS]addrC ler_normD. -rewrite -cats1. -rewrite (_ : a :: _ ++ B = (a :: L0) ++ [:: L1] ++ B)//; last first. - by rewrite -!catA -cat_cons. -rewrite zip_cat; last by rewrite cats1 size_rcons. -rewrite (_ : a :: _ ++ _ ++ B = (a :: L0) ++ [:: L1] ++ [:: c] ++ B); last first. - by rewrite -!catA -cat_cons. -rewrite zip_cat; last by rewrite cats1 size_rcons. -rewrite !big_cat lerD//. -case: B => [|B0 B1]. - by rewrite /= big_nil big_cons big_nil addr0. -rewrite -cat1s zip_cat// catA. -rewrite (_ : [:: L1] ++ _ ++ B1 = ([:: L1] ++ [:: c]) ++ [:: B0] ++ B1); last first. - by rewrite catA. -rewrite zip_cat// !big_cat lerD//= !big_cons !big_nil !addr0/= [leRHS]addrC. -by rewrite (le_trans _ (ler_normD _ _))// subrKA. -Qed. - -Lemma le_variation a b f s x : variation a b f s <= variation a b f (x :: s). -Proof. -case: s => [|h t]. - by rewrite variation_nil /variation/= big_nat_recl//= big_nil addr0. -rewrite /variation/= !big_nat_recl//= addrA lerD2r. -by rewrite -(subrKA (f x)) addrC ler_normD. -Qed. - -Lemma variation_opp_rev a b f s : itv_partition a b s -> - variation a b f s = - variation (- b) (- a) (f \o -%R) (rev (belast (- a) (map -%R s))). -Proof. -move=> abl; rewrite belast_map /variation /= [LHS]big_nat_rev/= add0n. -rewrite size_rev size_map size_belast 2!big_nat. -apply: eq_bigr => k; rewrite leq0n /= => ks. -rewrite nth_rev ?size_map ?size_belast// [in RHS]distrC. -rewrite (nth_map a); last first. - by rewrite size_belast ltn_subLR// addSn ltnS leq_addl. -rewrite opprK -rev_rcons nth_rev ?size_rcons ?size_map ?size_belast 1?ltnW//. -rewrite subSn// -map_rcons (nth_map b) ?size_rcons ?size_belast; last first. - by rewrite ltnS ltn_subLR// addSn ltnS leq_addl. -rewrite opprK nth_rcons size_belast -subSn// subSS. -rewrite (ltn_subLR _ (ltnW ks)) if_same. -case: k => [|k] in ks *. - rewrite add0n ltnn subn1 (_ : nth b s _ = b); last first. - case: abl ks => _. - elim/last_ind : s => // h t _; rewrite last_rcons => /eqP -> _. - by rewrite nth_rcons size_rcons ltnn eqxx. - rewrite (_ : nth b (a :: s) _ = nth a (belast a s) (size s).-1)//. - case: abl ks => _. - elim/last_ind : s => // h t _; rewrite last_rcons => /eqP -> _. - rewrite belast_rcons size_rcons/= -rcons_cons nth_rcons/= ltnS leqnn. - exact: set_nth_default. -rewrite addSn ltnS leq_addl//; congr (`| f _ - f _ |). - elim/last_ind : s ks {abl} => // h t _; rewrite size_rcons ltnS => kh. - rewrite belast_rcons nth_rcons subSS ltn_subLR//. - by rewrite addSn ltnS leq_addl// subSn. -elim/last_ind : s ks {abl} => // h t _; rewrite size_rcons ltnS => kh. -rewrite belast_rcons subSS -rcons_cons nth_rcons /= ltn_subLR//. -rewrite addnS ltnS leq_addl; apply: set_nth_default => //. -by rewrite /= ltnS leq_subLR leq_addl. -Qed. - -Lemma variation_rev_opp a b f s : itv_partition (- b) (- a) s -> - variation a b f (rev (belast b (map -%R s))) = - variation (- b) (- a) (f \o -%R) s. -Proof. -move=> abs; rewrite [in RHS]variation_opp_rev ?opprK//. -suff: (f \o -%R) \o -%R = f by move=> ->. -by apply/funext=> ? /=; rewrite opprK. -Qed. - -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 => [? ? ? /= _ /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 ?(@variation_cat _ _ a)//; [|exact: itv_partition1..]. - by rewrite lerD// IH. -move=> xts; rewrite -[_ :: s]cat1s (@variation_cat _ _ a) => //; last first. - exact: itv_partition1. -have [y [s' s'E]] : exists y s', s = y :: s'. - 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 -variation_cat//; [exact: le_variation | exact: itv_partition1]. -Qed. - -End variation. -#[deprecated(since="mathcomp-analysis 1.12.0", note="use `variation_cat` instead")] -Notation variationD := variation_cat (only parsing). - -Section bounded_variation. -Context {R : realType}. -Implicit Type (a b : R) (f : R -> R). - -Definition variations a b f := [set variation a b f l | l in itv_partition a b]. - -Lemma variations_variation a b f s : itv_partition a b s -> - variations a b f (variation a b f s). -Proof. by move=> abs; exists s. Qed. - -Lemma variations_neq0 a b f : a < b -> variations a b f !=set0. -Proof. -move=> ab; exists (variation a b f [:: b]); exists [:: b] => //. -exact: itv_partition1. -Qed. - -Lemma variationsN a b f : variations a b (\- f) = variations a b f. -Proof. -apply/seteqP; split => [_ [s abs] <-|r [s abs]]. - by rewrite variationN; exact: variations_variation. -by rewrite -variationN => <-; exact: variations_variation. -Qed. - -Lemma variationsxx a f : variations a a f = [set 0]. -Proof. -apply/seteqP; split => [x [_ /itv_partitionxx ->]|x ->]. - by rewrite /variation big_nil => <-. -by exists [::] => //=; rewrite /variation /= big_nil. -Qed. - -Definition bounded_variation a b f := has_ubound (variations a b f). - -Notation BV := bounded_variation. - -Lemma bounded_variationxx a f : BV a a f. -Proof. by exists 0 => r; rewrite variationsxx => ->. Qed. - -Lemma bounded_variationD a b f g : a < b -> - BV a b f -> BV a b g -> BV a b (f \+ g). -Proof. -move=> ab [r abfr] [s abgs]; exists (r + s) => _ [l abl] <-. -apply: le_trans; first exact: variation_le. -rewrite lerD//. -- by apply: abfr; exact: variations_variation. -- by apply: abgs; exact: variations_variation. -Qed. +Section total_variation_realFieldType. +Context {R : realFieldType}. +Implicit Types (a b : R) (f : R -> R). -Lemma bounded_variationN a b f : BV a b f -> BV a b (\- f). -Proof. by rewrite /bounded_variation variationsN. Qed. +Definition total_variation a b f := + ereal_sup [set x%:E | x in variations a b f]. -Lemma bounded_variationl a c b f : a <= c -> c <= b -> BV a b f -> BV a c f. -Proof. -rewrite le_eqVlt => /predU1P[<-{c} ? ?|ac]; first exact: bounded_variationxx. -rewrite le_eqVlt => /predU1P[<-{b}//|cb]. -move=> [x Hx]; exists x => _ [s acs] <-. -rewrite (@le_trans _ _ (variation a b f (rcons s b)))//; last first. - apply/Hx/variations_variation; case: acs => sa /eqP asc. - by rewrite /itv_partition rcons_path last_rcons sa/= asc. -rewrite {2}/variation size_rcons -[leLHS]addr0 big_nat_recr//= lerD//. -rewrite /variation !big_nat ler_sum// => k; rewrite leq0n /= => ks. -rewrite nth_rcons// ks -cats1 -cat_cons nth_cat /= ltnS (ltnW ks). -by rewrite ![in leRHS](set_nth_default c)//= ltnS ltnW. -Qed. +Notation TV := total_variation. -Lemma bounded_variationr a c b f : a <= c -> c <= b -> BV a b f -> BV c b f. -Proof. -rewrite le_eqVlt => /predU1P[<-{c}//|ac]. -rewrite le_eqVlt => /predU1P[<-{b} ?|cb]; first exact: bounded_variationxx. -move=> [x Hx]; exists x => _ [s cbs] <-. -rewrite (@le_trans _ _ (variation a b f (c :: s)))//; last first. - apply/Hx/variations_variation; case: cbs => cs csb. - by rewrite /itv_partition/= ac/= cs. -by rewrite {2}/variation/= -[leLHS]add0r big_nat_recl//= lerD. -Qed. +Lemma total_variationxx a f : TV a a f = 0%E. +Proof. by rewrite /total_variation variationsxx image_set1 ereal_sup1. Qed. -Lemma variations_opp a b f : - variations (- b) (- a) (f \o -%R) = variations a b f. +Lemma nondecreasing_total_variation a b f : a <= b -> + {in `[a, b] &, nondecreasing_fun f} -> TV a b f = (f b - f a)%:E. Proof. -rewrite eqEsubset; split=> [_ [s bas <-]| _ [s abs <-]]. - eexists; last exact: variation_rev_opp. - by move/itv_partition_rev : bas; rewrite !opprK. -eexists; last by exact/esym/variation_opp_rev. -exact: itv_partition_rev abs. +rewrite le_eqVlt => /predU1P[<-{b} ?|ab ndf]. + by rewrite total_variationxx subrr. +rewrite /total_variation [X in ereal_sup X](_ : _ = [set (f b - f a)%:E]). + by rewrite ereal_sup1. +apply/seteqP; split => [x/= [s [t abt <-{s} <-{x}]]|x/= ->{x}]. + by rewrite nondecreasing_variation. +exists (variation a b f [:: b]) => //. + exact/variations_variation/itv_partition1. +by rewrite nondecreasing_variation//; exact: itv_partition1. Qed. -Lemma nondecreasing_bounded_variation a b f : - {in `[a, b] &, {homo f : x y / x <= y}} -> BV a b f. -Proof. -move=> incf; exists (f b - f a) => ? [l pabl <-]; rewrite le_eqVlt. -by rewrite nondecreasing_variation// eqxx. -Qed. +Lemma total_variationN a b f : TV a b (\- f) = TV a b f. +Proof. by rewrite /TV; rewrite variationsN. Qed. -End bounded_variation. +End total_variation_realFieldType. Section total_variation. Context {R : realType}. Implicit Types (a b : R) (f : R -> R). -Definition total_variation a b f := - ereal_sup [set x%:E | x in variations a b f]. - Notation BV := bounded_variation. Notation TV := total_variation. -Lemma total_variationxx a f : TV a a f = 0%E. -Proof. by rewrite /total_variation variationsxx image_set1 ereal_sup1. Qed. - Lemma total_variation_ge a b f : a <= b -> (`|f b - f a|%:E <= TV a b f)%E. Proof. rewrite le_eqVlt => /predU1P[<-{b}|ab]. @@ -2451,23 +1944,6 @@ rewrite /total_variation /bounded_variation ltey => /eqP; apply: contra_notP. by move/hasNub_ereal_sup; apply; exact: variations_neq0. Qed. -Lemma nondecreasing_total_variation a b f : a <= b -> - {in `[a, b] &, nondecreasing_fun f} -> TV a b f = (f b - f a)%:E. -Proof. -rewrite le_eqVlt => /predU1P[<-{b} ?|ab ndf]. - by rewrite total_variationxx subrr. -rewrite /total_variation [X in ereal_sup X](_ : _ = [set (f b - f a)%:E]). - by rewrite ereal_sup1. -apply/seteqP; split => [x/= [s [t abt <-{s} <-{x}]]|x/= ->{x}]. - by rewrite nondecreasing_variation. -exists (variation a b f [:: b]) => //. - exact/variations_variation/itv_partition1. -by rewrite nondecreasing_variation//; exact: itv_partition1. -Qed. - -Lemma total_variationN a b f : TV a b (\- f) = TV a b f. -Proof. by rewrite /TV; rewrite variationsN. Qed. - Lemma total_variation_le a b f g : a <= b -> (TV a b (f \+ g) <= TV a b f + TV a b g)%E. Proof. @@ -2531,13 +2007,15 @@ Qed. Let total_variationD2 a b c f : a <= c -> c <= b -> (TV a b f <= TV a c f + TV c b f)%E. Proof. -rewrite le_eqVlt => /predU1P[<-{c}|ac]; first by rewrite total_variationxx add0e. -rewrite le_eqVlt => /predU1P[<-{b}|cb]; first by rewrite total_variationxx adde0. +rewrite le_eqVlt => /predU1P[<-|ac]; first by rewrite total_variationxx add0e. +rewrite le_eqVlt => /predU1P[<-|cb]; first by rewrite total_variationxx adde0. case : (pselect (bounded_variation a c f)); first last. move=> nbdac; have /eqP -> : TV a c f == +oo%E. - have: (-oo < TV a c f)%E by apply: (lt_le_trans _ (total_variation_ge0 f (ltW ac))). + have : (-oo < TV a c f)%E + by apply: (lt_le_trans _ (total_variation_ge0 f (ltW ac))). by rewrite ltNye_eq => /orP[|//] => /bounded_variationP => /(_ (ltW ac)). - by rewrite addye ?leey // -ltNye (@lt_le_trans _ _ 0)%E // ?total_variation_ge0 // ltW. + rewrite addye ?leey // -ltNye (@lt_le_trans _ _ 0)%E//. + by rewrite total_variation_ge0 // ltW. have [|nbdac] := pselect (bounded_variation c b f); first last. have /eqP -> : TV c b f == +oo%E. have: (-oo < TV c b f)%E.