From accc2f508c2ea2bfef83e5c7a88c9da26946e5e0 Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 4 Dec 2023 15:16:51 -0500 Subject: [PATCH 01/22] total variation proofs underway --- theories/lebesgue_measure.v | 25 +++++ theories/realfun.v | 203 ++++++++++++++++++++++++++++++++++++ 2 files changed, 228 insertions(+) diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 0de7bf9e0..cd23c4318 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2155,6 +2155,31 @@ Qed. End egorov. +Section absolute_continuity. +Context {R : realType}. +Notation mu := (@lebesgue_measure R). + +Definition absolutely_continuous a b (f : R -> R) := + [/\ {within `[a,b], continuous f }, + bounded_variation a b f & + forall E, E `<=` `[a,b] -> mu E = 0%:E -> mu (f @` E) = 0%:E + ]. + +Local Notation TV := (@total_variation R). + +Lemma absolute_continuity_cumulative a b (f : R -> R) : + absolutely_continuous a b f -> exists g h, + [/\ absolutely_continuous a b g, + absolutely_continuous a b h, + {in `[a,b] &, {homo g : x y / x <= y}}, + {in `[a,b] &, {homo h : x y / x <= y}} & + f = g \- h + ]. +Proof. +case => ctsf bdf f0. + +End absolute_continuity. + Definition vitali_cover {R : realType} (E : set R) I (B : I -> set R) (D : set I) := (forall i, is_ball (B i)) /\ diff --git a/theories/realfun.v b/theories/realfun.v index eda6e41a4..8277d3f2e 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1518,3 +1518,206 @@ End is_derive_inverse. #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) => (eapply is_deriveV; first by []) : typeclass_instances. + +Section bounded_variation. + +Context {R : realType}. + +Fixpoint partition (a b : R) l := + match l with + | nil => False + | p :: nil => p = a /\ p = b + | p :: ((q :: l) as rest) => p = a /\ p <= q /\ partition q b rest + end. + +Lemma partition_head (a b x : R) l : partition a b (x :: l) -> a = x. +Proof. by case: l => [[]|? ? [->]]. Qed. + +Lemma partitionrr (a b : R) l : partition a b (a :: a :: l) -> partition a b (a :: l). +Proof. by elim: l a => [ ? [_ [//]]| ?] l IH a /= [_ [_ ]]. Qed. + +Lemma partition_cons (a b : R) l : partition a b l -> partition a b (a :: l). +Proof. by case: l => //= ? [[-> -> //]|] ? ? [-> [? ?]]. Qed. + +Lemma partition_le (a b : R) l : partition a b l -> a <= b. +Proof. +by elim: l a => //= a [_ ? [->->] //| ] x l IH ? [<- [ + /IH]]; exact: le_trans. +Qed. + +Lemma partition_eq a l x : partition a a l -> x \in l -> x = a. +Proof. +elim: l x a => //= x [_ ? ? [-> _ /[!inE]/eqP//]|] a l IH ? ? [<- []] xa. +move=> /[dup]/partition_le ax; have -> : x = a by apply/le_anti/andP; split. +by move/IH => P; rewrite in_cons => /orP [/eqP //|]; apply: P. +Qed. + +Lemma partition2 a b : a <= b -> partition a b (a :: b :: nil). +Proof. by split; rewrite //= andbT. Qed. + +Lemma partition_concat a b c l1 l2: + partition a b l1 -> + partition b c l2 -> + partition a c (l1 ++ l2). +Proof. +elim: l1 a b l2 => // x [_ ? ? ? [-> ->]|]; first exact: partition_cons. +move=> a l1 IH p b l2 pbxa1 pb2. +rewrite ?cat_cons -(partition_head pbxa1); split => //. +split; first by case: pbxa1 => -> []. +apply: IH; last exact: pb2. +by case: l1 pbxa1=> [[-> [_ [_ -> //]]]|] ? ? /= [_ [_]]. +Qed. + +Lemma partition_concat_tl a b c l1 l2: + partition a b l1 -> + partition b c l2 -> + partition a c (l1 ++ List.tl l2). +Proof. +elim: l1 a b l2 => // x [? ? ? l2 [-> ->]|]. + by case: l2 => //= ? [[-> -> //]| ? ? [-> [? ?]]]; split => //. +move=> a l1 IH p b l2 pbxa1 pb2. +rewrite ?cat_cons -(partition_head pbxa1); split => //. +split; first by case: pbxa1 => -> []. +apply: IH; last exact: pb2. +by case: l1 pbxa1=> [[-> [_ [_ -> //]]]|] ? ? /= [_ [_]]. +Qed. + +Definition pvar part (f : R -> R) := + \sum_(xy <- zip part (List.tl part)) `|f xy.2 - f xy.1|. + +Definition variations a b f := [set pvar l f | l in partition a b]. +Definition total_variation a b (f : R -> R) := ereal_sup [set x%:E | x in (variations a b f)]. +Local Notation TV := total_variation. + +Lemma variations_n0 a b f : a <= b -> variations a b f !=set0. +Proof. +move=> ?; exists (pvar (a :: b :: nil) f), (a::b::nil) => //. +Qed. + +Lemma partition_TV f a b l : + partition a b l -> + a <= b -> + ((pvar l f)%:E <= TV a b f)%E. +Proof. +move=> pl alb; rewrite /total_variation/sup/supremum. +rewrite /ereal_sup/supremum. +case E: (_ == _). + have /set0P := (@variations_n0 _ _ f alb); move/eqP/image_set0_set0:E ->. + by move/eqP. +rewrite /has_ubound; case: xgetP. + move=> w wE [] /(_ (pvar l f)%:E) + _; apply; exists (pvar l f) => //. + by exists l. +have [w Qw] := @ereal_supremums_neq0 R [set x%:E | x in variations a b f]. +by move => /(_ w). +Qed. + +Lemma partition_TV2 a b f: a <= b -> (`|f b - f a|%:E <= TV a b f)%E. +Proof. +move=> ?; suff -> : `|f b - f a| = pvar (a :: b :: nil) f. + by apply: partition_TV => //; apply: partition2. +by rewrite /pvar /= big_seq1. +Qed. + +Lemma total_variation_ge0 a b f: a <= b -> (0 <= TV a b f)%E. +Proof. by move=> ab; apply: le_trans; last exact: partition_TV2. Qed. + +Definition bounded_variation a b (f : R -> R) := + has_ubound (variations a b f). + +Lemma hasNrub_ereal_sup (A : set R) : ~ has_ubound A -> + A !=set0 -> ereal_sup [set x%:E | x in A] = +oo%E. +Proof. +move=> hasNubA /[dup] [][a Aa] A0. +apply/eqP; rewrite eq_le leey /= leNgt; apply: contra_notN hasNubA => Aoo. +exists (sup A); apply: sup_ub. +exists (fine (ereal_sup [set x%:E | x in A])) => w Aw. +have -> : w = fine (ereal_sup [set x%:E | x in [set w]]). + by rewrite ereal_sup_EFin /= ?sup1 //; exists w => // ? ->. +rewrite fine_le //. + by rewrite ereal_sup_EFin //=; exists w => // ? ->. + apply/fin_real/andP; split => //. + rewrite ltNge leeNy_eq; apply/negP => /eqP/ereal_sup_ninfty/(_ (w%:E)). + apply/not_implyP; split => //; by exists w. +by apply: le_ereal_sup => ? [? -> <-]; exists w. +Qed. + +Lemma bounded_variationP a b f : a <= b -> + bounded_variation a b f <-> TV a b f \is a fin_num. +Proof. +split; first by move=> ?; rewrite /TV ereal_sup_EFin //; exact: variations_n0. +rewrite ge0_fin_numE ?total_variation_ge0 //; apply: contraPP => Nbdf. +suff -> : (TV a b f = +oo)%E by []. +apply: hasNrub_ereal_sup => //; exact: variations_n0. +Qed. + +Lemma total_variation_neg a b f : TV a b f = TV a b (\- f). +Proof. +rewrite /TV; suff -> : variations a b f = variations a b (\- f) by []. +rewrite /variations; suff -> : pvar^~ f = pvar ^~ (\- f) by []. +rewrite /pvar /= funeqE => x /=. +by under eq_bigr => i _ do rewrite -normrN -mulN1r mulrBr ?mulN1r. +Qed. + +Lemma bounded_variation_le a b p q f : + bounded_variation a b f -> p <= q -> a <= p -> q <= b -> + bounded_variation p q f. +Proof. +move=> + pq ap qb; have ab : a <= b by exact/(le_trans ap)/(le_trans pq). +case=> M ubdM; exists M => ? [l pql <-]. +apply: (@le_trans _ _ (pvar (a :: l ++ [:: b]) f)). + rewrite /pvar /=; case: l pql => //. + move=> ? l /[dup]/partition_head <- pql /=. + rewrite /= ?big_cons /=; apply ler_paddl => //. + elim: l p a pq {ab ubdM} ap pql => //. + move=> ?????; rewrite /= ?big_cons; apply ler_paddl => //. + move=> w l IH p a pq ap pql. + rewrite /= ?big_cons; rewrite ler_add //. + move: pql => [_ [?] pql]. apply: IH => //. + exact: (@partition_le w q (w::l)). +apply: ubdM; exists (a :: l ++ [::b]) => //. +rewrite -cat_cons (_ : [:: b] = List.tl (q :: b ::nil)); last by []. +apply: (@partition_concat_tl _ q) => //. +case: l pql => // ? ? /[dup] /partition_head <- Q /=; split => //. +Qed. + +Lemma total_variation_concat a b c f : + a <= b -> b <= c -> (TV a b f + TV b c f <= TV a c f)%E. +Proof. +move=> ab bc; have ac : a <= c by exact: (le_trans ab). +case : (pselect (bounded_variation a c f)); first last. + move=> nbdac; suff /eqP -> : TV a c f == +oo%E by rewrite leey. + have: (-oo < TV a c f)%E by apply: (lt_le_trans _ (total_variation_ge0 f ac)). + by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ ac). +move=> bdAC. +have bdf1 : bounded_variation a b f by exact: (bounded_variation_le bdAC). +have bdf2 : bounded_variation b c f by exact: (bounded_variation_le bdAC). +rewrite /total_variation ?ereal_sup_EFin => //; try exact: variations_n0. +rewrite -EFinD -sup_sumE /has_sup; try (by split => //; exact: variations_n0). +apply: le_sup. +- move=> ? [? [l1 pabl2 <-]] [? [l2 pbcl2 <-] <-]; exists (pvar (l1 ++ List.tl l2) f). + split; first by exists (l1 ++ List.tl l2)=> //=; apply: (partition_concat_tl pabl2). + rewrite /pvar -big_cat /=. + rewrite (_ : (zip l1 (List.tl l1) ++ zip l2 (List.tl l2)) = zip (l1 ++ List.tl l2) (List.tl (l1 ++ List.tl l2))) //. + elim: l1 a {bdf1 bdf2 bdAC ac ab} pabl2 pbcl2 => // x [/= _ ? [-> ->]|]. + by move=> bc2; congr (_ _ _); case: l2 bc2 => // ? ? /partition_head ->. + move=> z ? IH ? pabl1 pbcl2 /=; congr (_ _); apply: (IH z) => //. + by case: pabl1 => /= _ [_]. +- have [x0 vx0] := (variations_n0 f ab). + have [y0 vy0] := (variations_n0 f bc). + exists (x0 + y0); exists x0 => //; exists y0 => //. +- split => //; exact: variations_n0. +Qed. + +Definition neg_tv a f (x:R) := ((TV a x f - (f x)%:E)*2^-1%:E)%E. + +Lemma neg_TV_increasing a b (f : R -> R) : + {in `[a,b] &, {homo (neg_tv a f) : x y / x <= y >-> (x <= y)%E}}. +Proof. +move=> x y xab yab xy; have ax : a <= x. + by move: xab; rewrite in_itv //= => /andP []. +rewrite /neg_tv lee_pmul2r // lee_subr_addl // addeCA -EFinB. +apply: le_trans; last exact: (@total_variation_concat _ x). +apply: lee_add => //; apply: le_trans; last exact: partition_TV2. +by rewrite lee_fin ler_norm. +Qed. + +End bounded_variation. \ No newline at end of file From f984c7886668a560e277f7f1ddd8b17609d1c423 Mon Sep 17 00:00:00 2001 From: zstone Date: Mon, 4 Dec 2023 22:51:04 -0500 Subject: [PATCH 02/22] increasing implies BV --- theories/realfun.v | 86 +++++++++++++++++++++++++++++++++++++++++----- 1 file changed, 78 insertions(+), 8 deletions(-) diff --git a/theories/realfun.v b/theories/realfun.v index 8277d3f2e..c8a80203d 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1533,17 +1533,22 @@ Fixpoint partition (a b : R) l := Lemma partition_head (a b x : R) l : partition a b (x :: l) -> a = x. Proof. by case: l => [[]|? ? [->]]. Qed. +Lemma partition_le (a b : R) l : partition a b l -> a <= b. +Proof. +by elim: l a => //= a [_ ? [->->] //| ] x l IH ? [<- [ + /IH]]; exact: le_trans. +Qed. + +Lemma partition_tail (a b x y : R) l : + partition a b (x :: y :: l) -> partition y b (y :: l). +Proof. by case=> [-> [//]]. Qed. + + Lemma partitionrr (a b : R) l : partition a b (a :: a :: l) -> partition a b (a :: l). Proof. by elim: l a => [ ? [_ [//]]| ?] l IH a /= [_ [_ ]]. Qed. Lemma partition_cons (a b : R) l : partition a b l -> partition a b (a :: l). Proof. by case: l => //= ? [[-> -> //]|] ? ? [-> [? ?]]. Qed. -Lemma partition_le (a b : R) l : partition a b l -> a <= b. -Proof. -by elim: l a => //= a [_ ? [->->] //| ] x l IH ? [<- [ + /IH]]; exact: le_trans. -Qed. - Lemma partition_eq a l x : partition a a l -> x \in l -> x = a. Proof. elim: l x a => //= x [_ ? ? [-> _ /[!inE]/eqP//]|] a l IH ? ? [<- []] xa. @@ -1649,14 +1654,21 @@ suff -> : (TV a b f = +oo)%E by []. apply: hasNrub_ereal_sup => //; exact: variations_n0. Qed. -Lemma total_variation_neg a b f : TV a b f = TV a b (\- f). +Lemma variationN a b f : + variations a b (\- f) = variations a b f. Proof. -rewrite /TV; suff -> : variations a b f = variations a b (\- f) by []. rewrite /variations; suff -> : pvar^~ f = pvar ^~ (\- f) by []. rewrite /pvar /= funeqE => x /=. by under eq_bigr => i _ do rewrite -normrN -mulN1r mulrBr ?mulN1r. Qed. +Lemma total_variationN a b f : TV a b (\- f) = TV a b f. +Proof. by rewrite /TV; rewrite variationN. Qed. + +Lemma bounded_variationN a b f : + bounded_variation a b f -> bounded_variation a b (\- f). +Proof. by rewrite /bounded_variation variationN. Qed. + Lemma bounded_variation_le a b p q f : bounded_variation a b f -> p <= q -> a <= p -> q <= b -> bounded_variation p q f. @@ -1720,4 +1732,62 @@ apply: lee_add => //; apply: le_trans; last exact: partition_TV2. by rewrite lee_fin ler_norm. Qed. -End bounded_variation. \ No newline at end of file +Lemma total_variation_jordan_decompE a b f : + bounded_variation a b f -> + {in `[a,b], f =1 (fine \o neg_tv a (\- f)) \- (fine \o neg_tv a f)}. +Proof. +move=> bdabf x; rewrite in_itv /= => /andP [ax xb]. +have ffin: TV a x f \is a fin_num. + by apply/bounded_variationP => //; apply: (bounded_variation_le bdabf). +have Nffin : TV a x (\- f) \is a fin_num. + apply/bounded_variationP => //; apply/bounded_variationN. + exact: (bounded_variation_le bdabf). +rewrite /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //; first last. +- by rewrite fin_numM // fin_numD; apply/andP; split. +- by rewrite fin_numM // fin_numD; apply/andP; split. +- by apply: fin_num_adde_defl; rewrite fin_numN fin_numD; apply/andP; split. +- by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split. +rewrite addeAC oppeD //= ?fin_num_adde_defl //. +by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -splitr. +Qed. + +Lemma neg_TV_increasing_fin a b (f : R -> R) : + bounded_variation a b f -> + {in `[a,b] &, {homo (fine \o neg_tv a f) : x y / x <= y}}. +Proof. +move=> bdv p q pab qab pq /=. +move: (pab) (qab); rewrite ?in_itv /= => /andP [? ?] /andP [? ?]. +apply: fine_le; rewrite /neg_tv ?fin_numM // ?fin_numB /=. +- apply/andP; split => //; apply/bounded_variationP => //. + exact: (bounded_variation_le bdv). +- apply/andP; split => //; apply/bounded_variationP => //. + exact: (bounded_variation_le bdv). +by apply: (neg_TV_increasing _ pab). +Qed. + +Lemma increasing_bounded_variation a b (f : R -> R) : + {in `[a,b] &, {homo f : x y / x <= y}} -> + bounded_variation a b f. +Proof. +move=> incf; exists (f b - f a) => ? [l pabl <-]; rewrite le_eqVlt. +apply/orP; left; apply/eqP. +rewrite /pvar; elim: l a incf pabl => // ? []. + by move=> _ ? _ [-> ->]; rewrite /= big_nil subrr. +move=> w l IH a fi /[dup]/partition_le ab /[dup]/partition_tail/[dup] ?. +move=> /partition_le wb [] => [-> [aw _]]; rewrite /= big_cons /=. +rewrite (IH w) //; first last. + move=> p q; rewrite in_itv /= => /andP [? ?] /andP [? ?] pq. + by apply: fi; rewrite //in_itv; apply/andP; split => //; exact: (le_trans aw). +have -> : `|f w - f a| = f w - f a. + rewrite ger0_norm // subr_ge0; apply: fi => //; rewrite // in_itv /=. + by apply/andP; split => //. + by apply/andP; split => //. +by rewrite addrCA; congr (_ _); rewrite addrC addrA [-_ + _]addrC subrr add0r. +Qed. + +Lemma neg_TV_bounded_variation a b f : + bounded_variation a b f -> + bounded_variation a b (fine \o neg_tv a f). +Proof. +by move=> ?; apply increasing_bounded_variation; apply: neg_TV_increasing_fin. +Qed. \ No newline at end of file From ded0e6f84ddfec616b828f140c3c75e3a345b776 Mon Sep 17 00:00:00 2001 From: zstone Date: Tue, 5 Dec 2023 17:36:15 -0500 Subject: [PATCH 03/22] splitting partitions --- theories/realfun.v | 109 ++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 104 insertions(+), 5 deletions(-) diff --git a/theories/realfun.v b/theories/realfun.v index c8a80203d..8831ff16d 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1530,6 +1530,8 @@ Fixpoint partition (a b : R) l := | p :: ((q :: l) as rest) => p = a /\ p <= q /\ partition q b rest end. +Arguments partition _ _ : simpl never. + Lemma partition_head (a b x : R) l : partition a b (x :: l) -> a = x. Proof. by case: l => [[]|? ? [->]]. Qed. @@ -1542,6 +1544,14 @@ Lemma partition_tail (a b x y : R) l : partition a b (x :: y :: l) -> partition y b (y :: l). Proof. by case=> [-> [//]]. Qed. +Lemma partition_consP (a b x y : R) l : partition a b (x :: y :: l) <-> + [/\ a = x, a <= y, y <= b & partition y b (y :: l)]. +Proof. +split; last by case => ->. +move=> /[dup]; case => -> [-> ?] /partition_tail/partition_le ->. +by split. +Qed. + Lemma partitionrr (a b : R) l : partition a b (a :: a :: l) -> partition a b (a :: l). Proof. by elim: l a => [ ? [_ [//]]| ?] l IH a /= [_ [_ ]]. Qed. @@ -1551,8 +1561,8 @@ Proof. by case: l => //= ? [[-> -> //]|] ? ? [-> [? ?]]. Qed. Lemma partition_eq a l x : partition a a l -> x \in l -> x = a. Proof. -elim: l x a => //= x [_ ? ? [-> _ /[!inE]/eqP//]|] a l IH ? ? [<- []] xa. -move=> /[dup]/partition_le ax; have -> : x = a by apply/le_anti/andP; split. +elim: l x a => //= x [_ ? ? [-> _ /[!inE]/eqP//]|] a l IH ? ?. +move=> /partition_consP[-> ? ax]; have -> : x = a by apply/le_anti/andP; split. by move/IH => P; rewrite in_cons => /orP [/eqP //|]; apply: P. Qed. @@ -1590,7 +1600,10 @@ Definition pvar part (f : R -> R) := \sum_(xy <- zip part (List.tl part)) `|f xy.2 - f xy.1|. Definition variations a b f := [set pvar l f | l in partition a b]. -Definition total_variation a b (f : R -> R) := ereal_sup [set x%:E | x in (variations a b f)]. + +Definition total_variation a b (f : R -> R) := + ereal_sup [set x%:E | x in (variations a b f)]. + Local Notation TV := total_variation. Lemma variations_n0 a b f : a <= b -> variations a b f !=set0. @@ -1691,7 +1704,7 @@ apply: (@partition_concat_tl _ q) => //. case: l pql => // ? ? /[dup] /partition_head <- Q /=; split => //. Qed. -Lemma total_variation_concat a b c f : +Let total_variation_concat_le a b c f : a <= b -> b <= c -> (TV a b f + TV b c f <= TV a c f)%E. Proof. move=> ab bc; have ac : a <= c by exact: (le_trans ab). @@ -1719,6 +1732,80 @@ apply: le_sup. - split => //; exact: variations_n0. Qed. +Fixpoint part_split x (l : seq R) := + match l with + | [::] => ([::x], [::x]) + | y :: tl => if x < y then ([:: x], x :: y :: tl) else + let xy := part_split x tl + in (y :: xy.1, xy.2 ) + end. + +Lemma part_splitl a b x l : + a <= x -> x <= b -> partition a b l -> + partition a x (part_split x l).1. +Proof. +elim: l a => // a [/= _ ? ax bx|]. + move: ax => /[swap]; move: bx => /[swap] [[-> ->]] ? ?. + have -> : x = b by apply/ le_anti/andP; split. + by rewrite lt_irreflexive /=; repeat split. +move=> w l IH ? + xb /partition_consP => /[swap] [[->]] aw wb wbl ax /=. +rewrite ltNge ax /= /=; case Nxw: (x < w) => //=. +have wx : w <= x by rewrite leNgt Nxw. +apply/partition_consP; split => //. +by have /= := IH w wx xb wbl; rewrite Nxw. +Qed. + +Lemma part_splitr a b x l : + a <= x -> x <= b -> partition a b l -> + partition x b (part_split x l).2. +Proof. +elim: l a => // a [/= _ ? ax bx|]. + case=> -> ->; move: (bx); rewrite le_eqVlt => /orP. + by case=> [/eqP ->|->]; rewrite ?lt_irreflexive //=. +move=> w l IH ? + xb /partition_consP => /[swap] [[->]] aw wb wbl ax /=. +rewrite ltNge ax /= /=; case Nxw: (x < w) => //=. + by apply/partition_consP; split => //; apply: ltW. +have wx : w <= x by rewrite leNgt Nxw. +by have /= := IH w wx xb wbl; rewrite Nxw. +Qed. + +Lemma part_split_pvar a b x l f : + partition a b l -> + a <= x -> x <= b -> + pvar l f <= pvar (part_split x l).1 f + pvar (part_split x l).2 f. +Proof. +move=> + + xb; elim: l a => // a [_ w [<- -> bx]|]. + by rewrite /pvar [x in x <= _]/= big_nil addr_ge0 //; apply: sumr_ge0 => ?. +move=> w l IH ? /partition_consP [-> aw wb pwbl ax]. +rewrite /= ?[x < a]ltNge ?ax /=; case Nxw: (x < w) => /=. + rewrite /pvar /= ?big_cons /= ?big_nil addr0 addrA. + by rewrite ler_add2r [x in _ <= x]addrC ler_dist_add. +rewrite /pvar /= ?big_cons /= -?addrA ler_add2l. +have wx : w <= x by rewrite leNgt Nxw. +by have /= := IH w pwbl wx; rewrite Nxw /=. +Qed. + +Let total_variation_concat_ge a b c f : + a <= b -> b <= c -> (TV a b f + TV b c f >= TV a c f)%E. +Proof. +move=> ab bc; have ac : a <= c by exact: (le_trans ab). +case : (pselect (bounded_variation a b f)); first last. + move=> nbdac; have /eqP -> : TV a b f == +oo%E. + have: (-oo < TV a b f)%E by apply: (lt_le_trans _ (total_variation_ge0 f ab)). + by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ ab). + by rewrite addye ?leey // -ltNye (@lt_le_trans _ _ 0)%E // ?total_variation_ge0 //. +case : (pselect (bounded_variation b c f)); first last. + move=> nbdac; have /eqP -> : TV b c f == +oo%E. + have: (-oo < TV b c f)%E by apply: (lt_le_trans _ (total_variation_ge0 f bc)). + by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ bc). + by rewrite addey ?leey // -ltNye (@lt_le_trans _ _ 0)%E // ?total_variation_ge0 //. +move=> bdAB bdAC. +rewrite /total_variation ?ereal_sup_EFin => //; try exact: variations_n0. +rewrite -EFinD -sup_sumE /has_sup; try (by split => //; exact: variations_n0). +apply: le_sup. +- move=> ? [l pacl <-]. + rewrite /down /=. + Definition neg_tv a f (x:R) := ((TV a x f - (f x)%:E)*2^-1%:E)%E. Lemma neg_TV_increasing a b (f : R -> R) : @@ -1790,4 +1877,16 @@ Lemma neg_TV_bounded_variation a b f : bounded_variation a b (fine \o neg_tv a f). Proof. by move=> ?; apply increasing_bounded_variation; apply: neg_TV_increasing_fin. -Qed. \ No newline at end of file +Qed. + +Lemma neg_TV_continuous a b (f : R -> R) : + {within `[a,b], continuous f} -> + {within `[a,b], continuous (TV a ^~ f)}. +Proof. +move=> ctsf. + +Qed. + + + + From 840c3640932e9b95a3f49d9a9220d227a2d1f512 Mon Sep 17 00:00:00 2001 From: zstone Date: Tue, 5 Dec 2023 19:07:32 -0500 Subject: [PATCH 04/22] halfway through right continuity proof --- theories/realfun.v | 75 +++++++++++++++++++++++++++++++++++++++------- 1 file changed, 65 insertions(+), 10 deletions(-) diff --git a/theories/realfun.v b/theories/realfun.v index 8831ff16d..40f0e6cdf 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1800,11 +1800,29 @@ case : (pselect (bounded_variation b c f)); first last. by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ bc). by rewrite addey ?leey // -ltNye (@lt_le_trans _ _ 0)%E // ?total_variation_ge0 //. move=> bdAB bdAC. -rewrite /total_variation ?ereal_sup_EFin => //; try exact: variations_n0. +rewrite /total_variation [x in (x + _)%E]ereal_sup_EFin => //; try exact: variations_n0. +rewrite [x in (_ + x)%E]ereal_sup_EFin => //; try exact: variations_n0. rewrite -EFinD -sup_sumE /has_sup; try (by split => //; exact: variations_n0). -apply: le_sup. -- move=> ? [l pacl <-]. - rewrite /down /=. +apply: ub_ereal_sup => ? [? [l pacl <- <-]]; rewrite lee_fin. +apply: le_trans; first exact: (@part_split_pvar a c b). +apply: sup_ub. + case: bdAB => M ubdM; case: bdAC => N ubdN; exists (N + M). + move=> q [?] [i pabi <-] [? [j pbcj <-]] <-. + by apply: ler_add; [apply: ubdN;exists i|apply:ubdM;exists j]. +exists (pvar (part_split b l).1 f). + by exists (part_split b l).1 => //; apply: (@part_splitl a c). +exists (pvar (part_split b l).2 f) => //. +by exists (part_split b l).2 => //; apply: (@part_splitr a c). +Qed. + +Lemma total_variation_concatE a b c f : + a <= b -> b <= c -> (TV a b f + TV b c f = TV a c f)%E. +Proof. +move=> ab bc; apply/le_anti/andP; split. + exact: total_variation_concat_le. +exact: total_variation_concat_ge. +Qed. + Definition neg_tv a f (x:R) := ((TV a x f - (f x)%:E)*2^-1%:E)%E. @@ -1814,7 +1832,7 @@ Proof. move=> x y xab yab xy; have ax : a <= x. by move: xab; rewrite in_itv //= => /andP []. rewrite /neg_tv lee_pmul2r // lee_subr_addl // addeCA -EFinB. -apply: le_trans; last exact: (@total_variation_concat _ x). +rewrite -[TV a y _](@total_variation_concatE _ x) //. apply: lee_add => //; apply: le_trans; last exact: partition_TV2. by rewrite lee_fin ler_norm. Qed. @@ -1879,11 +1897,48 @@ Proof. by move=> ?; apply increasing_bounded_variation; apply: neg_TV_increasing_fin. Qed. -Lemma neg_TV_continuous a b (f : R -> R) : - {within `[a,b], continuous f} -> - {within `[a,b], continuous (TV a ^~ f)}. -Proof. -move=> ctsf. +Lemma neg_TV_continuous a b x (f : R -> R) : + a <= x -> x < b -> + {for x, continuous f} -> + bounded_variation a b f -> + (fine \o TV a ^~ f @ at_right x --> fine (TV a x f)). +Proof. +move=> ax xb ctsf bvf; have ? : a <= b by apply:ltW; apply: (le_lt_trans ax). + apply/cvgrPdist_lt=> _/posnumP[eps]. +have ? : Filter (nbhs x^'+) by exact: at_right_proper_filter. +apply: filter_app (nbhs_right_ge _). +apply: filter_app (nbhs_right_le xb). +have abfin : TV a b f \is a fin_num by apply/bounded_variationP. +have [//|?] := @ub_ereal_sup_adherent R _ (eps%:num/2) _ abfin. +case=> ? [l pxl <- <-]; rewrite -/(total_variation a b f). +rewrite lte_subl_addr // -EFinD => tvp. +near=> t => tb xt; have ? : a <= t by exact: (le_trans ax). +have ? : x <= b by exact: (le_trans xt). +rewrite -fineB; first last. + by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). + by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). +rewrite -(total_variation_concatE _ ax xt). +rewrite oppeD ?fin_num_adde_defl //; first last. + by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). +have xtfin : TV x t f \is a fin_num. + by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). +rewrite addeA subee //; first last. + by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). +rewrite sub0e fineN normrN ger0_norm; first last. + rewrite fine_ge0 //; exact: total_variation_ge0. +apply: (@lt_trans _ _ (pvar l f + eps%:num / 2)). + by rewrite -lte_fin /= fineK. +rewrite {tvp} [x in _ < x]splitr ltr_add2r; move: l pxl. +near: t. + + rewrite + rewrite -[x in _ < x]fineK. +Search fine (Order.lt). + +near: t. +Search ereal_sup. + + Qed. From b9921ead1b3b5f7cd7397947f6a8c698eefc3ed8 Mon Sep 17 00:00:00 2001 From: zstone Date: Thu, 7 Dec 2023 17:02:57 -0500 Subject: [PATCH 05/22] right continuity of TV --- theories/realfun.v | 124 ++++++++++++++++++++++++++++++++++----------- 1 file changed, 95 insertions(+), 29 deletions(-) diff --git a/theories/realfun.v b/theories/realfun.v index 40f0e6cdf..ff6bc2b99 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1611,6 +1611,14 @@ Proof. move=> ?; exists (pvar (a :: b :: nil) f), (a::b::nil) => //. Qed. +Lemma pvar_cons0 f a l : + pvar (a :: a :: l) f = pvar (a :: l) f. +Proof. by rewrite /pvar /= big_cons /= subrr normr0 add0r. Qed. + +Lemma pvar_consE f a b l : + pvar (a :: b :: l) f = `|f b - f a| + pvar (b :: l) f. +Proof. by rewrite /pvar /= big_cons. Qed. + Lemma partition_TV f a b l : partition a b l -> a <= b -> @@ -1897,51 +1905,109 @@ Proof. by move=> ?; apply increasing_bounded_variation; apply: neg_TV_increasing_fin. Qed. +Fixpoint collapse_head (l : seq R) := + match l with + | nil => nil + | x :: nil => x :: nil + | x :: ((y :: _) as tl) => if x == y then collapse_head tl else x :: tl + end. + +Lemma collapse_head_consE x l : + collapse_head (x :: x :: l) = collapse_head (x :: l). +Proof. by rewrite /= eq_refl. Qed. + +Lemma collapse_head_consNE x y l : + x != y -> collapse_head (x :: y :: l) = x :: y :: l. +Proof. +move=> xy; case E: (x == y). + by move/eqP: E xy => ->; rewrite eq_refl. +by rewrite /= E. +Qed. + +Lemma collapse_head_partition a b l : + a <= b -> partition a b l -> partition a b (collapse_head l). +Proof. +elim: l a => // a [//| w l IH] ? /[swap] /partition_consP [-> + wb wbl ab]. +rewrite le_eqVlt => /orP [|]. + by move/eqP=> ->; rewrite collapse_head_consE; exact: IH. +move=> aw; rewrite collapse_head_consNE => //. + by apply/partition_consP; split => //; exact: ltW. +by apply/negP=> E; move /eqP: E aw => ->; rewrite lt_irreflexive. +Qed. + +Lemma collapse_head_pvar l f: + pvar l f = pvar (collapse_head l) f. +Proof. +elim: l => // w [//|] y l; case E: (w == y). + by move/eqP: E => ->; rewrite pvar_cons0 collapse_head_consE. +by rewrite collapse_head_consNE //; rewrite E. +Qed. + +Lemma collapse_head_neq l a b tl: + (collapse_head l) = a :: b :: tl -> a != b. +Proof. +elim: l a b tl => // w [//=|x l IH] a b tl. +case E: (w == x). + move/eqP: E => ->; rewrite collapse_head_consE; apply: IH. +rewrite collapse_head_consNE ?E //. +by case=> <- <- _; rewrite E. +Qed. + Lemma neg_TV_continuous a b x (f : R -> R) : a <= x -> x < b -> - {for x, continuous f} -> + (f @ at_right x --> f x) -> bounded_variation a b f -> (fine \o TV a ^~ f @ at_right x --> fine (TV a x f)). Proof. move=> ax xb ctsf bvf; have ? : a <= b by apply:ltW; apply: (le_lt_trans ax). - apply/cvgrPdist_lt=> _/posnumP[eps]. +apply/cvgrPdist_lt=> _/posnumP[eps]. have ? : Filter (nbhs x^'+) by exact: at_right_proper_filter. +have xbl := ltW xb. +have xbfin : TV x b f \is a fin_num. + by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). +have [//|?] := @ub_ereal_sup_adherent R _ (eps%:num/2) _ xbfin. +case=> ? [l + <- <-]; rewrite -/(total_variation x b f). +rewrite collapse_head_pvar => /(collapse_head_partition xbl). +case E : (collapse_head l) => //; move: E. +set i := (w in _ :: w); case: i => //. + by move=> _ []; move: xb => /[swap] -> /[swap] ->; rewrite lt_irreflexive. +move=> i j /collapse_head_neq /[swap] /[dup] /partition_consP [<-]; rewrite le_eqVlt. +move=> /orP [/eqP ->|]; rewrite ?eq_refl => // xi ib pibj pxij _ tv_eps. apply: filter_app (nbhs_right_ge _). -apply: filter_app (nbhs_right_le xb). -have abfin : TV a b f \is a fin_num by apply/bounded_variationP. -have [//|?] := @ub_ereal_sup_adherent R _ (eps%:num/2) _ abfin. -case=> ? [l pxl <- <-]; rewrite -/(total_variation a b f). -rewrite lte_subl_addr // -EFinD => tvp. -near=> t => tb xt; have ? : a <= t by exact: (le_trans ax). -have ? : x <= b by exact: (le_trans xt). +apply: filter_app (nbhs_right_lt xi). +have e20 : 0 < eps%:num/2 by []. +move/cvgrPdist_lt/(_ (eps%:num/2) e20):ctsf; apply: filter_app. +near=> t => fxt ti xt; have ? : a <= t by exact: (le_trans ax). +have ? : x <= b by apply: ltW; exact: (lt_le_trans xi). +have tb : t <= b by apply: ltW; exact: (lt_le_trans ti). rewrite -fineB; first last. - by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). + apply/bounded_variationP => //; apply: (bounded_variation_le bvf) => //. by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). rewrite -(total_variation_concatE _ ax xt). rewrite oppeD ?fin_num_adde_defl //; first last. by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). have xtfin : TV x t f \is a fin_num. by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). +have tbfin : TV t b f \is a fin_num. + by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). rewrite addeA subee //; first last. by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). rewrite sub0e fineN normrN ger0_norm; first last. rewrite fine_ge0 //; exact: total_variation_ge0. -apply: (@lt_trans _ _ (pvar l f + eps%:num / 2)). - by rewrite -lte_fin /= fineK. -rewrite {tvp} [x in _ < x]splitr ltr_add2r; move: l pxl. -near: t. - - rewrite - rewrite -[x in _ < x]fineK. -Search fine (Order.lt). - -near: t. -Search ereal_sup. - - - -Qed. - - - - +move: (tv_eps); rewrite -(total_variation_concatE f _ tb) //. +pose r := [:: x, i & j]. +have := part_split_pvar f pxij xt tb. +rewrite -lee_fin => /lt_le_trans /[apply]. +have -> : part_split t [:: x, i & j] = (x :: t :: nil, [:: t, i & j]). + by rewrite /part_split; rewrite ?ti ltNge xt /=. +rewrite /= -addeA -lte_subr_addr; first last. + by rewrite fin_numD; apply/andP; split => //. +rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA. +move/lt_trans; apply. +rewrite [x in (_ < x%:E)%E]splitr EFinD addeC lte_add2lE //. +rewrite -addeA; apply: (@le_lt_trans _ _ (pvar [::x;t] f)%:E). + rewrite gee_addl // sube_le0; apply: ereal_sup_ub. + exists (pvar [::t,i&j] f) => //; exists [::t,i&j] => //. + by apply/partition_consP; split => //; apply: ltW. + by rewrite /pvar /= big_seq1 /= distrC lte_fin. +Unshelve. all: by end_near. Qed. \ No newline at end of file From b953832dc71d8f4684c3ba86f827343be2fae348 Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 8 Dec 2023 07:43:05 -0500 Subject: [PATCH 06/22] bv functions done --- theories/realfun.v | 39 ++++++++++++++++++++++++++++++++++++--- 1 file changed, 36 insertions(+), 3 deletions(-) diff --git a/theories/realfun.v b/theories/realfun.v index ff6bc2b99..0573f2787 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1832,7 +1832,9 @@ exact: total_variation_concat_ge. Qed. -Definition neg_tv a f (x:R) := ((TV a x f - (f x)%:E)*2^-1%:E)%E. +Definition neg_tv a f (x:R) : \bar R := ((TV a x f - (f x)%:E)*2^-1%:E)%E. + +Definition pos_tv a f (x:R) : \bar R := neg_tv a (\- f) x. Lemma neg_TV_increasing a b (f : R -> R) : {in `[a,b] &, {homo (neg_tv a f) : x y / x <= y >-> (x <= y)%E}}. @@ -1953,7 +1955,7 @@ rewrite collapse_head_consNE ?E //. by case=> <- <- _; rewrite E. Qed. -Lemma neg_TV_continuous a b x (f : R -> R) : +Lemma TV_right_continuous a b x (f : R -> R) : a <= x -> x < b -> (f @ at_right x --> f x) -> bounded_variation a b f -> @@ -2010,4 +2012,35 @@ rewrite -addeA; apply: (@le_lt_trans _ _ (pvar [::x;t] f)%:E). exists (pvar [::t,i&j] f) => //; exists [::t,i&j] => //. by apply/partition_consP; split => //; apply: ltW. by rewrite /pvar /= big_seq1 /= distrC lte_fin. -Unshelve. all: by end_near. Qed. \ No newline at end of file +Unshelve. all: by end_near. Qed. + +Lemma neg_TV_right_continuous a x b (f : R -> R) : + a <= x -> x < b -> + bounded_variation a b f -> + (f @ at_right x --> f x) -> + (fine \o neg_tv a f @ at_right x --> fine (neg_tv a f x)). +Proof. +move=> ax ? bvf fcts; have xb : x <= b by exact: ltW. +have xbfin : TV a x f \is a fin_num. + by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). +apply: fine_cvg; rewrite /neg_tv fineM // ?fin_numB ?xbfin //= EFinM. +under eq_fun => i do rewrite EFinN. +apply: cvg_trans; first (apply: cvgeMr => //); last exact: cvg_id. +rewrite fineD // EFinB; apply: cvgeB => //. + apply/ fine_cvgP; split; first exists (b-x). + - by rewrite /= subr_gt0. + - move=> t /= xtbx xt; have ? : a <= t. + by apply: ltW; apply: (le_lt_trans ax). + apply/bounded_variationP => //; apply: (bounded_variation_le bvf) => //. + move: xtbx; rewrite distrC ger0_norm ?subr_ge0; last by exact: ltW. + by rewrite ltr_subr_addr -addrA [-_ + _]addrC subrr addr0 => /ltW. + by apply: TV_right_continuous => //; last exact: bvf => //. +apply: cvg_comp; first exact: fcts. +apply/ fine_cvgP; split; first by near=> t => //. +by have -> : (fine \o EFin = id) by move=> ?; rewrite funeqE => ? /=. +Unshelve. all: by end_near. Qed. + +Definition totally_bounded_variation (f : R -> R) := + forall a b, bounded_variation a b f. + +End bounded_variation. \ No newline at end of file From 6f2cadf0bf59bd016792c99e9df702967cce8efb Mon Sep 17 00:00:00 2001 From: zstone Date: Sat, 9 Dec 2023 09:36:28 -0500 Subject: [PATCH 07/22] cantor subspace --- theories/cantor.v | 36 +++++++++++++++++++++ theories/charge.v | 63 +++++++++++++++++++++++++++++++++++++ theories/lebesgue_measure.v | 25 --------------- 3 files changed, 99 insertions(+), 25 deletions(-) diff --git a/theories/cantor.v b/theories/cantor.v index 439c41e34..eb41507d0 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -548,3 +548,39 @@ by exists f; rewrite -cstf; exact: cst_continuous. Qed. End alexandroff_hausdorff. + +Section cantor_subspace. +Context {T : topologicalType} (A : set T) a (Aa : A a). +Let A' := PointedType (classicType_choiceType {x & A x}) (exist _ a Aa). +Let WA := @weak_topologicalType A' T (@projT1 _ A). +Lemma perfect_set_weak : + perfect_set A -> perfect_set [set: WA]. +Proof. +move=> pftA; apply/perfectTP; case=> t At /=. +rewrite /open/=/wopen/=; apply/forallPNP => E oE. +case: (pselect (E t)); first last. + apply: contra_not; rewrite eqEsubset; case=> _ /(_ (existT _ _ At)). + exact. +case: pftA => clA lpA Et; have : A t by done. +rewrite -[a in a _]lpA => /(_ E) []; first exact: open_nbhs_nbhs. +move=> e [+] Ae Ee; apply: contra_neq_not. +rewrite eqEsubset; case=> /(_ (existT _ _ Ae) Ee) /= + _. +exact: EqdepFacts.eq_sigT_fst. +Qed. + +Lemma compact_set_weak : + compact A -> compact [set: WA]. +Proof. +move=> /compact_near_coveringP cptA; apply/ compact_near_coveringP. +move=> ? F /= P FF cvr; pose Q i x := if pselect (A x) is left Ax + then P i (existT _ _ Ax) else True. +have := (@cptA _ F Q FF); have FQ : forall x, A x -> \near x & F, Q F x. + move=> x Ax; have := cvr (existT _ _ Ax) I. + case; case=> E j [/= [? [[V oV /= <- /= Vx VE FJ EJ]]]]. + exists (V, j); first by split => //; apply: open_nbhs_nbhs; split. + case=> /= z i [Vz ji]; rewrite /Q; case: (pselect _) => // Az. + by have := (EJ (existT _ _ Az, i)); apply; split => //; apply: VE. +move/(_ FQ); apply: filter_app; near=> z => + [r /= Ar _] => /(_ _ Ar). +by rewrite /Q; case (pselect _) => // Ar'; suff -> // : Ar = Ar'. +Unshelve. all: end_near. Qed. +End cantor_subspace. \ No newline at end of file diff --git a/theories/charge.v b/theories/charge.v index f2fb02d85..9a69cbc75 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -590,6 +590,69 @@ Qed. End positive_negative_set_realFieldType. +Section absolute_continuity. +Context {R : realType}. +Notation mu := (@lebesgue_measure R). + +Lemma interval_measure0 A : is_interval A -> mu A = 0 -> is_subset1 A. +Proof. +Admitted. + +Lemma measure0_disconnected A : + measurable A -> mu A = 0 -> totally_disconnected A. +Proof. +move=> mA A0 x Ax; rewrite eqEsubset; split; first last. + by move=> ? ->; exact: connected_component_refl. +move=> y [U /= [Ux UA /connected_intervalP ]] itvU. +have : mu U = 0. + apply/eqP; rewrite -measure_le0 //= -A0. + by apply: (le_measure); rewrite ?inE //; first exact: is_interval_measurable. +by move/(interval_measure0 itvU) => /[apply]; apply. +Qed. + + + + +Definition maps_null E (f : R -> R) := + forall A, A `<=` E -> mu A = 0%:E -> mu (f @` A) = 0%:E. + +Definition absolutely_continuous a b (f : R -> R) := + [/\ {within `[a,b], continuous f }, + bounded_variation a b f & + maps_null `[a,b] f + ]. + +Lemma maps_null_total_variation (a b : R) f : + (a <= b)%R -> + absolutely_continuous a b f -> + maps_null `[a, b] (fine \o neg_tv a f). +Proof. +move=> ab [ctsf bdf] f0 A AE A0. + +\int[pushforward mu mphi]_(y in (phi @` U)) f y + = \int[mu]_(x in phi^-1 (phi @` U)) (f \o phi) x. + +0 = \int_(f@`A) id + +integralD + +Search measure (0%:E). + +Local Notation TV := (@total_variation R). + +Lemma absolute_continuity_cumulative a b (f : R -> R) : + absolutely_continuous a b f -> exists g h, + [/\ absolutely_continuous a b g, + absolutely_continuous a b h, + {in `[a,b] &, {homo g : x y / x <= y}}, + {in `[a,b] &, {homo h : x y / x <= y}} & + f = g \- h + ]. +Proof. +case => ctsf bdf f0. + +End absolute_continuity. + Section hahn_decomposition_lemma. Context d (T : measurableType d) (R : realType). Variables (nu : {charge set T -> \bar R}) (D : set T). diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index cd23c4318..0de7bf9e0 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -2155,31 +2155,6 @@ Qed. End egorov. -Section absolute_continuity. -Context {R : realType}. -Notation mu := (@lebesgue_measure R). - -Definition absolutely_continuous a b (f : R -> R) := - [/\ {within `[a,b], continuous f }, - bounded_variation a b f & - forall E, E `<=` `[a,b] -> mu E = 0%:E -> mu (f @` E) = 0%:E - ]. - -Local Notation TV := (@total_variation R). - -Lemma absolute_continuity_cumulative a b (f : R -> R) : - absolutely_continuous a b f -> exists g h, - [/\ absolutely_continuous a b g, - absolutely_continuous a b h, - {in `[a,b] &, {homo g : x y / x <= y}}, - {in `[a,b] &, {homo h : x y / x <= y}} & - f = g \- h - ]. -Proof. -case => ctsf bdf f0. - -End absolute_continuity. - Definition vitali_cover {R : realType} (E : set R) I (B : I -> set R) (D : set I) := (forall i, is_ball (B i)) /\ From f33b0e88b247ce1eadad345092c3753cf0f96934 Mon Sep 17 00:00:00 2001 From: zstone Date: Tue, 12 Dec 2023 03:02:17 -0500 Subject: [PATCH 08/22] left continuity for BV --- theories/cantor.v | 74 ++++++++++++++++++++++++- theories/realfun.v | 130 +++++++++++++++++++++++++++++++++++++++++++- theories/topology.v | 8 +++ 3 files changed, 206 insertions(+), 6 deletions(-) diff --git a/theories/cantor.v b/theories/cantor.v index eb41507d0..49c3cb1ce 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -550,8 +550,17 @@ Qed. End alexandroff_hausdorff. Section cantor_subspace. -Context {T : topologicalType} (A : set T) a (Aa : A a). -Let A' := PointedType (classicType_choiceType {x & A x}) (exist _ a Aa). +Context {T : topologicalType} (A : set T). + +Definition cantor_like_subspace := + [/\ perfect_set A, + compact A, + hausdorff_space T & + totally_disconnected A]. + +Context a0 (Aa0 : A a0). + +Let A' := PointedType (classicType_choiceType {x & A x}) (exist _ _ Aa0). Let WA := @weak_topologicalType A' T (@projT1 _ A). Lemma perfect_set_weak : perfect_set A -> perfect_set [set: WA]. @@ -583,4 +592,63 @@ have := (@cptA _ F Q FF); have FQ : forall x, A x -> \near x & F, Q F x. move/(_ FQ); apply: filter_app; near=> z => + [r /= Ar _] => /(_ _ Ar). by rewrite /Q; case (pselect _) => // Ar'; suff -> // : Ar = Ar'. Unshelve. all: end_near. Qed. -End cantor_subspace. \ No newline at end of file + +Lemma totally_disconnected_weak : + totally_disconnected A -> totally_disconnected [set: WA]. +Proof. +move=> tdA [x Ax] _; rewrite eqEsubset; split; first last. + by move=> ? ->; exact: connected_component_refl. +move=> [y Ay] [U [Ux _ ctU Uy]] => /=. +apply/eq_existT_curried; last by move=> ?. +have := tdA _ Ax; rewrite eqEsubset; case=> + _; apply. +exists (@projT1 T _ @` U); last by exists (existT _ _ Ay). +split; first by exists (existT _ _ Ax). + by move=> ? [[? ? ? <-]]. +apply: connected_continuous_connected => //. +by apply: continuous_subspaceT; exact: weak_continuous. +Qed. + +Lemma hausdorff_weak : + hausdorff_space T -> hausdorff_space WA. +Proof. +move=> hsdfK [p Ap] [q Aq] /= clstr. +apply/eq_existT_curried; last by move=> ?. +apply: hsdfK; move: clstr; rewrite ?cluster_cvgE /= => -[G PG [GtoQ psubG]]. +exists (@projT1 T _ @ G); [exact: fmap_proper_filter|split]. + apply: cvg_trans; first (apply:cvg_app; exact: GtoQ). + exact: weak_continuous. +move/(cvg_app (@projT1 T _)): psubG => /cvg_trans; apply. +exact: weak_continuous. +Qed. + +Definition foo {R : realType} (P : set R) (P01 : P `<=` `[0%R,1%R]) : R -> R := + 0%R. + tvf@`P (wlog (tvf 1 = 1)) + + C --> [0,1] --> [0,1] + A A A + | | | + V | | + C <--> P ------> tvf @`P + + +mu (tvf @` P) = eps +mu (f @` P) = mu (((tvf + f)/2 - (tvf - f) /2) ) + +mu (f@` `[a,b]) = + + +Lemma cantor_like_subspaceP : + cantor_like_subspace -> cantor_like WA. +Proof. +case=> /perfect_set_weak ? /compact_set_weak ?. + +Search (existT _ _ _ = existT _ _ _). +pose f x := if pselect (A x) is left Ax then existT _ _ Ax else existT _ _ Aa0. +have -> : [set existT _ _ Ax] = f @` [set x]. + rewrite eqEsubset /f; split => z. + by move=> ->; exists x => //; case (pselect _) => // Ax';suff -> : Ax = Ax'. + by case => ? /= ->; case (pselect _) => // Ax'; suff -> : Ax = Ax'. + +apply: connected_component_max. +End cantor_subspace. diff --git a/theories/realfun.v b/theories/realfun.v index 0573f2787..41fa21cb1 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1649,6 +1649,9 @@ Proof. by move=> ab; apply: le_trans; last exact: partition_TV2. Qed. Definition bounded_variation a b (f : R -> R) := has_ubound (variations a b f). +Definition bounded_variationT (f : R -> R) := + forall a b, bounded_variation a b f. + Lemma hasNrub_ereal_sup (A : set R) : ~ has_ubound A -> A !=set0 -> ereal_sup [set x%:E | x in A] = +oo%E. Proof. @@ -2040,7 +2043,128 @@ apply/ fine_cvgP; split; first by near=> t => //. by have -> : (fine \o EFin = id) by move=> ?; rewrite funeqE => ? /=. Unshelve. all: by end_near. Qed. -Definition totally_bounded_variation (f : R -> R) := - forall a b, bounded_variation a b f. +Lemma pvarNE (l : seq R) f : + pvar l f = pvar (map (-%R) l) (f \o (-%R)). +Proof. +elim: l; first by rewrite /pvar /= !big_nil. +move=> a [|]; first by move=> _ /=; rewrite /pvar /= !big_nil. +by move=> w l IH; rewrite /= ?pvar_consE /= ?opprK; congr( _ + _). +Qed. + +Lemma pvarNE2 (l : seq R) f : + pvar (map (-%R) l) f = pvar l (f \o (-%R)). +Proof. +have NE : (-%R) \o (-%R) = @id R. + by apply: eq_fun => ?; rewrite opprK. +have compE g : g \o id = g by apply: eq_fun. +by rewrite (_ : f = f \o (-%R) \o (-%R)) -?pvarNE -compA NE compE. +Qed. + +Lemma partition_rev a b l : + partition a b l -> partition (-b) (-a) (rev (map (-%R) l)). +Proof. +elim: l a b => // => w []. + by move=> /= _ ? ? [] <- <-; split. +move=> y l; set j := y :: l => IH a b /partition_consP [<-] ay yb pyb. +have /(@partition_concat_tl _ _ _ _ (-y :: -a :: nil)) := IH _ _ pyb. +rewrite /= rev_cons -cats1 ?rev_cons -?cats1; apply. +by split => //; repeat split => //; rewrite ler_opp2. +Qed. + +Lemma pvar_cat a (l1 l2 : seq R) f : + pvar (l1 ++ a :: l2) f = pvar (l1 ++ [:: a]) f + pvar (a :: l2) f. +Proof. +elim: l1 a l2; first by move => ? ?; rewrite /= /pvar /= big_nil /= add0r. +move=> w []. + by move=> _ ? ? /=; rewrite ?pvar_consE /= /pvar /= big_nil /= -addrA add0r. +move=> y l1 IH a l2. +by rewrite ?cat_cons ?pvar_consE IH ?cat_cons addrA. +Qed. + +Lemma pvar_revE (l : seq R) f : + pvar l f = pvar (rev l) f. +Proof. +elim: l; first by rewrite /pvar /= !big_nil. +move=> a [|]; first by move=> _ /=; rewrite /pvar /= !big_nil. +move=> w l IH; rewrite pvar_consE; rewrite distrC IH. +rewrite ?rev_cons -?cats1 -catA [x in _ = x]pvar_cat addrC; congr (_ + _). +by rewrite pvar_consE /pvar big_nil addr0. +Qed. + +Lemma variation_revE a b f: + variations (-b) (-a) (f \o [eta -%R]) = variations a b f. +Proof. +rewrite eqEsubset; split => ?. + move=> [l] /partition_rev + <-; rewrite ?opprK => plrev. + by rewrite -pvarNE2 pvar_revE; exists (rev (map (-%R) l)) => //. +have fNE : f = (f \o -%R) \o -%R. + by apply: eq_fun => ?; rewrite /= opprK. +rewrite -{1}[a]opprK -{1}[b]opprK fNE. +move=> [l] /partition_rev + <-; rewrite ?opprK => plrev. +rewrite -pvarNE2 pvar_revE; exists (rev (map (-%R) l)) => //. +by rewrite -compA fNE; congr (_ _ ); apply: eq_fun => ?; rewrite /= ?opprK. +Qed. + +Lemma total_variation_revE a b f: + TV a b f = TV (-b) (-a) (f \o (-%R)). +Proof. by rewrite /total_variation -variation_revE. Qed. + +Lemma at_left_at_rightP {T: topologicalType} (f : R -> T) x (z:T): + f @ at_left x --> z <-> + f \o (-%R) @ at_right (-x) --> z. +Proof. + +suff -> : (- x)^'+ = (-%R) @ x^'-. + by rewrite -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK. +rewrite eqEsubset /=; split. + move=> E /= [r rpos xb]; exists r => //. + move=> t /= xtr tx; apply: xb. + by rewrite /= -opprB opprK normrN addrC. + by rewrite ltr_oppr opprK. +move=> E /= [r rpos xb]; exists r => //. +move=> t /= xtr tx; rewrite -[t]opprK; apply: xb. + by rewrite /= opprK -normrN opprD. +by rewrite ltr_oppl. +Qed. + +Lemma TV_left_continuous a b x (f : R -> R) : + a < x -> x <= b -> + (f @ at_left x --> f x) -> + bounded_variation a b f -> + (fine \o TV a ^~ f @ at_left x --> fine (TV a x f)). +Proof. +move=> ax xb fNcts bvf. +apply/at_left_at_rightP; rewrite total_variation_revE. +have bvNf : bounded_variation (-b) (-a) (f \o -%R). + by case:bvf=> M; rewrite -variation_revE => ?; exists M. +have bx : -b <= -x by rewrite ler_oppl opprK. +have xa : -x < -a by rewrite ltr_oppl opprK. +have ? : -x <= -a by apply: ltW. +have ? : Filter (nbhs (-x)^'+) by exact: at_right_proper_filter. +have -> : fine (TV (-x) (-a) (f \o -%R)) = + fine (TV (-b) (-a) (f \o -%R)) - fine (TV (-b) (-x) (f \o -%R)). + apply/eqP; rewrite -subr_eq opprK addrC. + rewrite -fineD ?total_variation_concatE //. + - by apply/bounded_variationP => //; apply: (bounded_variation_le bvNf). + - by apply/bounded_variationP => //; apply: (bounded_variation_le bvNf). +have /near_eq_cvg/cvg_trans : {near ((-x)^'+), + (fun t => fine (TV (-b) (-a) (f \o -%R)) - fine (TV (-b) t (f\o-%R))) =1 + (fine \o (TV a)^~ f) \o -%R }. + apply: filter_app (nbhs_right_lt xa). + apply: filter_app (nbhs_right_ge _). + near=> t => xt ta; have ? : -b <= t by exact: (le_trans bx). + have ? : t <= -a by exact: ltW. + apply/eqP; rewrite eq_sym -subr_eq opprK addrC. + rewrite /= [TV a _ f]total_variation_revE opprK -fineD ?total_variation_concatE //. + - by apply/bounded_variationP => //; apply: (bounded_variation_le bvNf) => //. + - by apply/bounded_variationP => //; apply: (bounded_variation_le bvNf). +apply. +apply: cvgB; first exact: cvg_cst. +apply: (TV_right_continuous _ _ _ bvNf). +- by rewrite ler_oppl opprK //. +- by rewrite ltr_oppl opprK //. +by apply/at_left_at_rightP; rewrite /= opprK. +Unshelve. all: by end_near. Qed. -End bounded_variation. \ No newline at end of file +End bounded_variation. +Unshelve. all: by end_near. Qed. \ No newline at end of file diff --git a/theories/topology.v b/theories/topology.v index 4e95029c6..42c290e4e 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -4248,6 +4248,14 @@ suff : R `&` U = R by move: Rx => /[swap] <- []. by apply: ctdR; [exists z|exists U|exists U]. Qed. +Lemma totally_disconnected_compact {T : topologicalType} : + hausdorff_space T -> + compact [set: T] -> + totally_disconnected [set: T] -> + zero_dimensional T. +Proof. +move=> hsdfT cmpT dctT x y xny. + Lemma totally_disconnected_cvg {T : topologicalType} (x : T) : hausdorff_space T -> zero_dimensional T -> compact [set: T] -> filter_from [set D : set T | D x /\ clopen D] id --> x. From 580b07cf1b92d7c0f1938db62474afdda85f1a4d Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 15 Dec 2023 18:30:04 -0500 Subject: [PATCH 09/22] continuity of TV with annoying admit --- theories/realfun.v | 142 ++++++++++++++++++++++++--------------------- 1 file changed, 75 insertions(+), 67 deletions(-) diff --git a/theories/realfun.v b/theories/realfun.v index 41fa21cb1..60f7674cf 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1532,14 +1532,14 @@ Fixpoint partition (a b : R) l := Arguments partition _ _ : simpl never. -Lemma partition_head (a b x : R) l : partition a b (x :: l) -> a = x. -Proof. by case: l => [[]|? ? [->]]. Qed. - Lemma partition_le (a b : R) l : partition a b l -> a <= b. Proof. by elim: l a => //= a [_ ? [->->] //| ] x l IH ? [<- [ + /IH]]; exact: le_trans. Qed. +Lemma partition_headE (a b x : R) l : partition a b (x :: l) -> a = x. +Proof. by case: l => [[]|? ? [->]]. Qed. + Lemma partition_tail (a b x y : R) l : partition a b (x :: y :: l) -> partition y b (y :: l). Proof. by case=> [-> [//]]. Qed. @@ -1552,51 +1552,28 @@ move=> /[dup]; case => -> [-> ?] /partition_tail/partition_le ->. by split. Qed. - -Lemma partitionrr (a b : R) l : partition a b (a :: a :: l) -> partition a b (a :: l). -Proof. by elim: l a => [ ? [_ [//]]| ?] l IH a /= [_ [_ ]]. Qed. - -Lemma partition_cons (a b : R) l : partition a b l -> partition a b (a :: l). -Proof. by case: l => //= ? [[-> -> //]|] ? ? [-> [? ?]]. Qed. - -Lemma partition_eq a l x : partition a a l -> x \in l -> x = a. -Proof. -elim: l x a => //= x [_ ? ? [-> _ /[!inE]/eqP//]|] a l IH ? ?. -move=> /partition_consP[-> ? ax]; have -> : x = a by apply/le_anti/andP; split. -by move/IH => P; rewrite in_cons => /orP [/eqP //|]; apply: P. -Qed. - Lemma partition2 a b : a <= b -> partition a b (a :: b :: nil). Proof. by split; rewrite //= andbT. Qed. -Lemma partition_concat a b c l1 l2: - partition a b l1 -> - partition b c l2 -> - partition a c (l1 ++ l2). +Lemma partition_concat a b c l1 l2: + partition a b l1 -> partition b c l2 -> partition a c (l1 ++ l2). Proof. -elim: l1 a b l2 => // x [_ ? ? ? [-> ->]|]; first exact: partition_cons. -move=> a l1 IH p b l2 pbxa1 pb2. -rewrite ?cat_cons -(partition_head pbxa1); split => //. -split; first by case: pbxa1 => -> []. -apply: IH; last exact: pb2. -by case: l1 pbxa1=> [[-> [_ [_ -> //]]]|] ? ? /= [_ [_]]. +elim: l1 a b l2 => // x [_ ? ? l [-> ->]|]. + by case: l => //= ? [[-> -> //]|] ? ? [-> [? ?]]. +move=> a l1 IH p b l2 /partition_consP [-> ? xa ab] pb2. +by rewrite cat_cons; do 2 (split => //); apply: IH; last exact: pb2. Qed. -Lemma partition_concat_tl a b c l1 l2: - partition a b l1 -> - partition b c l2 -> - partition a c (l1 ++ List.tl l2). +Lemma partition_concat_tl a b c l1 l2: + partition a b l1 -> partition b c l2 -> partition a c (l1 ++ List.tl l2). Proof. -elim: l1 a b l2 => // x [? ? ? l2 [-> ->]|]. - by case: l2 => //= ? [[-> -> //]| ? ? [-> [? ?]]]; split => //. -move=> a l1 IH p b l2 pbxa1 pb2. -rewrite ?cat_cons -(partition_head pbxa1); split => //. -split; first by case: pbxa1 => -> []. -apply: IH; last exact: pb2. -by case: l1 pbxa1=> [[-> [_ [_ -> //]]]|] ? ? /= [_ [_]]. +elim: l1 a b l2 => // x [? ? ? l2 [-> ->]|]. + by case: l2 => //= ? [[-> -> //]| ? ? [-> [? ?]]]. +move=> a l1 IH p b l2 /partition_consP [-> ? xa ab] pb2. +by rewrite cat_cons; do 2 (split => //); apply: IH; last exact: pb2. Qed. -Definition pvar part (f : R -> R) := +Definition pvar part (f : R -> R) := \sum_(xy <- zip part (List.tl part)) `|f xy.2 - f xy.1|. Definition variations a b f := [set pvar l f | l in partition a b]. @@ -1607,12 +1584,9 @@ Definition total_variation a b (f : R -> R) := Local Notation TV := total_variation. Lemma variations_n0 a b f : a <= b -> variations a b f !=set0. -Proof. -move=> ?; exists (pvar (a :: b :: nil) f), (a::b::nil) => //. -Qed. +Proof. by move=> ?; exists (pvar (a :: b :: nil) f), (a::b::nil). Qed. -Lemma pvar_cons0 f a l : - pvar (a :: a :: l) f = pvar (a :: l) f. +Lemma pvar_cons0 f a l : pvar (a :: a :: l) f = pvar (a :: l) f. Proof. by rewrite /pvar /= big_cons /= subrr normr0 add0r. Qed. Lemma pvar_consE f a b l : @@ -1620,12 +1594,10 @@ Lemma pvar_consE f a b l : Proof. by rewrite /pvar /= big_cons. Qed. Lemma partition_TV f a b l : - partition a b l -> - a <= b -> - ((pvar l f)%:E <= TV a b f)%E. + partition a b l -> ((pvar l f)%:E <= TV a b f)%E. Proof. -move=> pl alb; rewrite /total_variation/sup/supremum. -rewrite /ereal_sup/supremum. +move=> pl; rewrite /total_variation/sup/supremum/ereal_sup/supremum. +have alb := partition_le pl. case E: (_ == _). have /set0P := (@variations_n0 _ _ f alb); move/eqP/image_set0_set0:E ->. by move/eqP. @@ -1639,7 +1611,7 @@ Qed. Lemma partition_TV2 a b f: a <= b -> (`|f b - f a|%:E <= TV a b f)%E. Proof. move=> ?; suff -> : `|f b - f a| = pvar (a :: b :: nil) f. - by apply: partition_TV => //; apply: partition2. + by apply: partition_TV => //; exact: partition2. by rewrite /pvar /= big_seq1. Qed. @@ -1678,8 +1650,7 @@ suff -> : (TV a b f = +oo)%E by []. apply: hasNrub_ereal_sup => //; exact: variations_n0. Qed. -Lemma variationN a b f : - variations a b (\- f) = variations a b f. +Lemma variationN a b f : variations a b (\- f) = variations a b f. Proof. rewrite /variations; suff -> : pvar^~ f = pvar ^~ (\- f) by []. rewrite /pvar /= funeqE => x /=. @@ -1700,19 +1671,19 @@ Proof. move=> + pq ap qb; have ab : a <= b by exact/(le_trans ap)/(le_trans pq). case=> M ubdM; exists M => ? [l pql <-]. apply: (@le_trans _ _ (pvar (a :: l ++ [:: b]) f)). - rewrite /pvar /=; case: l pql => //. - move=> ? l /[dup]/partition_head <- pql /=. - rewrite /= ?big_cons /=; apply ler_paddl => //. - elim: l p a pq {ab ubdM} ap pql => //. - move=> ?????; rewrite /= ?big_cons; apply ler_paddl => //. - move=> w l IH p a pq ap pql. - rewrite /= ?big_cons; rewrite ler_add //. - move: pql => [_ [?] pql]. apply: IH => //. - exact: (@partition_le w q (w::l)). + elim: l a p pq {ab ubdM} ap pql => // ? []. + by move=> _ ?????; rewrite /pvar /= ?big_cons?big_nil addr0; exact: addr_ge0. + move=> w l IH a p => pq ap /partition_consP [ <- ? ? pwl]. + rewrite ?cat_cons pvar_consE pvar_consE pvar_consE. + rewrite [(`|f w - f p|)]distrC addrA [(`|_| + `|_|)]addrC. + rewrite -addrA ler_add // ler_paddl //. + apply: (le_trans (IH w w _ _ _)) => //; rewrite cat_cons pvar_consE subrr. + by rewrite normr0 add0r. apply: ubdM; exists (a :: l ++ [::b]) => //. rewrite -cat_cons (_ : [:: b] = List.tl (q :: b ::nil)); last by []. -apply: (@partition_concat_tl _ q) => //. -case: l pql => // ? ? /[dup] /partition_head <- Q /=; split => //. +apply: (@partition_concat_tl _ q) => //. +case: l pql => //?[[-> ->]|]; first by apply: partition2; apply: (le_trans ap). +by move=> ? ? /partition_consP [<- ? ? ?]; apply/partition_consP; split. Qed. Let total_variation_concat_le a b c f : @@ -1734,7 +1705,7 @@ apply: le_sup. rewrite /pvar -big_cat /=. rewrite (_ : (zip l1 (List.tl l1) ++ zip l2 (List.tl l2)) = zip (l1 ++ List.tl l2) (List.tl (l1 ++ List.tl l2))) //. elim: l1 a {bdf1 bdf2 bdAC ac ab} pabl2 pbcl2 => // x [/= _ ? [-> ->]|]. - by move=> bc2; congr (_ _ _); case: l2 bc2 => // ? ? /partition_head ->. + by move=> bc2; congr (_ _ _); case: l2 bc2 => // ? ? /partition_headE ->. move=> z ? IH ? pabl1 pbcl2 /=; congr (_ _); apply: (IH z) => //. by case: pabl1 => /= _ [_]. - have [x0 vx0] := (variations_n0 f ab). @@ -2113,7 +2084,6 @@ Lemma at_left_at_rightP {T: topologicalType} (f : R -> T) x (z:T): f @ at_left x --> z <-> f \o (-%R) @ at_right (-x) --> z. Proof. - suff -> : (- x)^'+ = (-%R) @ x^'-. by rewrite -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK. rewrite eqEsubset /=; split. @@ -2127,6 +2097,21 @@ move=> t /= xtr tx; rewrite -[t]opprK; apply: xb. by rewrite ltr_oppl. Qed. +Lemma left_right_continuousP {T: topologicalType} (f : R -> T) x: + (f @ at_left x --> f x /\ + f @ at_right x --> f x) <-> + f @ x --> f x. +Proof. +split; first last. + by move=> cts; split; exact: cvg_within_filter. +case => + + U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl. +rewrite ?near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf. +near=> t => xlt xgt; have := @real_leVge R x t; rewrite ?num_real. +move=> /(_ isT isT) /orP; rewrite ?le_eqVlt; case => /orP; case => //. + by move/eqP <-; apply: nbhs_singleton. +by move/eqP ->; apply: nbhs_singleton. +Unshelve. all: by end_near. Qed. + Lemma TV_left_continuous a b x (f : R -> R) : a < x -> x <= b -> (f @ at_left x --> f x) -> @@ -2166,5 +2151,28 @@ apply: (TV_right_continuous _ _ _ bvNf). by apply/at_left_at_rightP; rewrite /= opprK. Unshelve. all: by end_near. Qed. -End bounded_variation. -Unshelve. all: by end_near. Qed. \ No newline at end of file +Lemma continuous_within_itvP a b (f : R -> R) : + {within `[a,b], continuous f} <-> + {in `]a,b[, continuous f} /\ f @ a^'+ --> f a /\ f @b^'- --> f b. +Proof. +Admitted. + +Lemma TV_continuous a b (f : R -> R) : + a < b -> + {within `[a,b], continuous f} -> + bounded_variation a b f -> + {within `[a,b], continuous (fine \o TV a ^~ f)}. +Proof. +move=> ab /continuous_within_itvP [int [l r]] bdf. +apply/continuous_within_itvP; repeat split. +- move=> x /[dup] xab; rewrite in_itv /= => /andP [ax xb]. + apply/left_right_continuousP; split. + apply: (TV_left_continuous _ (ltW xb)) => //. + by have /left_right_continuousP [] := int x xab. + apply: (TV_right_continuous _ xb) => //; first exact: ltW. + by have /left_right_continuousP [] := int x xab. +- exact: (TV_right_continuous _ ab). +- exact: (TV_left_continuous ab). +Qed. + +End bounded_variation. \ No newline at end of file From 528ea58b4c7954c3d6e22d862e17175dc6da4405 Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 15 Dec 2023 18:31:12 -0500 Subject: [PATCH 10/22] resetting unused files --- theories/cantor.v | 104 -------------------------------------------- theories/charge.v | 63 --------------------------- theories/topology.v | 8 ---- 3 files changed, 175 deletions(-) diff --git a/theories/cantor.v b/theories/cantor.v index 49c3cb1ce..439c41e34 100644 --- a/theories/cantor.v +++ b/theories/cantor.v @@ -548,107 +548,3 @@ by exists f; rewrite -cstf; exact: cst_continuous. Qed. End alexandroff_hausdorff. - -Section cantor_subspace. -Context {T : topologicalType} (A : set T). - -Definition cantor_like_subspace := - [/\ perfect_set A, - compact A, - hausdorff_space T & - totally_disconnected A]. - -Context a0 (Aa0 : A a0). - -Let A' := PointedType (classicType_choiceType {x & A x}) (exist _ _ Aa0). -Let WA := @weak_topologicalType A' T (@projT1 _ A). -Lemma perfect_set_weak : - perfect_set A -> perfect_set [set: WA]. -Proof. -move=> pftA; apply/perfectTP; case=> t At /=. -rewrite /open/=/wopen/=; apply/forallPNP => E oE. -case: (pselect (E t)); first last. - apply: contra_not; rewrite eqEsubset; case=> _ /(_ (existT _ _ At)). - exact. -case: pftA => clA lpA Et; have : A t by done. -rewrite -[a in a _]lpA => /(_ E) []; first exact: open_nbhs_nbhs. -move=> e [+] Ae Ee; apply: contra_neq_not. -rewrite eqEsubset; case=> /(_ (existT _ _ Ae) Ee) /= + _. -exact: EqdepFacts.eq_sigT_fst. -Qed. - -Lemma compact_set_weak : - compact A -> compact [set: WA]. -Proof. -move=> /compact_near_coveringP cptA; apply/ compact_near_coveringP. -move=> ? F /= P FF cvr; pose Q i x := if pselect (A x) is left Ax - then P i (existT _ _ Ax) else True. -have := (@cptA _ F Q FF); have FQ : forall x, A x -> \near x & F, Q F x. - move=> x Ax; have := cvr (existT _ _ Ax) I. - case; case=> E j [/= [? [[V oV /= <- /= Vx VE FJ EJ]]]]. - exists (V, j); first by split => //; apply: open_nbhs_nbhs; split. - case=> /= z i [Vz ji]; rewrite /Q; case: (pselect _) => // Az. - by have := (EJ (existT _ _ Az, i)); apply; split => //; apply: VE. -move/(_ FQ); apply: filter_app; near=> z => + [r /= Ar _] => /(_ _ Ar). -by rewrite /Q; case (pselect _) => // Ar'; suff -> // : Ar = Ar'. -Unshelve. all: end_near. Qed. - -Lemma totally_disconnected_weak : - totally_disconnected A -> totally_disconnected [set: WA]. -Proof. -move=> tdA [x Ax] _; rewrite eqEsubset; split; first last. - by move=> ? ->; exact: connected_component_refl. -move=> [y Ay] [U [Ux _ ctU Uy]] => /=. -apply/eq_existT_curried; last by move=> ?. -have := tdA _ Ax; rewrite eqEsubset; case=> + _; apply. -exists (@projT1 T _ @` U); last by exists (existT _ _ Ay). -split; first by exists (existT _ _ Ax). - by move=> ? [[? ? ? <-]]. -apply: connected_continuous_connected => //. -by apply: continuous_subspaceT; exact: weak_continuous. -Qed. - -Lemma hausdorff_weak : - hausdorff_space T -> hausdorff_space WA. -Proof. -move=> hsdfK [p Ap] [q Aq] /= clstr. -apply/eq_existT_curried; last by move=> ?. -apply: hsdfK; move: clstr; rewrite ?cluster_cvgE /= => -[G PG [GtoQ psubG]]. -exists (@projT1 T _ @ G); [exact: fmap_proper_filter|split]. - apply: cvg_trans; first (apply:cvg_app; exact: GtoQ). - exact: weak_continuous. -move/(cvg_app (@projT1 T _)): psubG => /cvg_trans; apply. -exact: weak_continuous. -Qed. - -Definition foo {R : realType} (P : set R) (P01 : P `<=` `[0%R,1%R]) : R -> R := - 0%R. - tvf@`P (wlog (tvf 1 = 1)) - - C --> [0,1] --> [0,1] - A A A - | | | - V | | - C <--> P ------> tvf @`P - - -mu (tvf @` P) = eps -mu (f @` P) = mu (((tvf + f)/2 - (tvf - f) /2) ) - -mu (f@` `[a,b]) = - - -Lemma cantor_like_subspaceP : - cantor_like_subspace -> cantor_like WA. -Proof. -case=> /perfect_set_weak ? /compact_set_weak ?. - -Search (existT _ _ _ = existT _ _ _). -pose f x := if pselect (A x) is left Ax then existT _ _ Ax else existT _ _ Aa0. -have -> : [set existT _ _ Ax] = f @` [set x]. - rewrite eqEsubset /f; split => z. - by move=> ->; exists x => //; case (pselect _) => // Ax';suff -> : Ax = Ax'. - by case => ? /= ->; case (pselect _) => // Ax'; suff -> : Ax = Ax'. - -apply: connected_component_max. -End cantor_subspace. diff --git a/theories/charge.v b/theories/charge.v index 9a69cbc75..f2fb02d85 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -590,69 +590,6 @@ Qed. End positive_negative_set_realFieldType. -Section absolute_continuity. -Context {R : realType}. -Notation mu := (@lebesgue_measure R). - -Lemma interval_measure0 A : is_interval A -> mu A = 0 -> is_subset1 A. -Proof. -Admitted. - -Lemma measure0_disconnected A : - measurable A -> mu A = 0 -> totally_disconnected A. -Proof. -move=> mA A0 x Ax; rewrite eqEsubset; split; first last. - by move=> ? ->; exact: connected_component_refl. -move=> y [U /= [Ux UA /connected_intervalP ]] itvU. -have : mu U = 0. - apply/eqP; rewrite -measure_le0 //= -A0. - by apply: (le_measure); rewrite ?inE //; first exact: is_interval_measurable. -by move/(interval_measure0 itvU) => /[apply]; apply. -Qed. - - - - -Definition maps_null E (f : R -> R) := - forall A, A `<=` E -> mu A = 0%:E -> mu (f @` A) = 0%:E. - -Definition absolutely_continuous a b (f : R -> R) := - [/\ {within `[a,b], continuous f }, - bounded_variation a b f & - maps_null `[a,b] f - ]. - -Lemma maps_null_total_variation (a b : R) f : - (a <= b)%R -> - absolutely_continuous a b f -> - maps_null `[a, b] (fine \o neg_tv a f). -Proof. -move=> ab [ctsf bdf] f0 A AE A0. - -\int[pushforward mu mphi]_(y in (phi @` U)) f y - = \int[mu]_(x in phi^-1 (phi @` U)) (f \o phi) x. - -0 = \int_(f@`A) id - -integralD - -Search measure (0%:E). - -Local Notation TV := (@total_variation R). - -Lemma absolute_continuity_cumulative a b (f : R -> R) : - absolutely_continuous a b f -> exists g h, - [/\ absolutely_continuous a b g, - absolutely_continuous a b h, - {in `[a,b] &, {homo g : x y / x <= y}}, - {in `[a,b] &, {homo h : x y / x <= y}} & - f = g \- h - ]. -Proof. -case => ctsf bdf f0. - -End absolute_continuity. - Section hahn_decomposition_lemma. Context d (T : measurableType d) (R : realType). Variables (nu : {charge set T -> \bar R}) (D : set T). diff --git a/theories/topology.v b/theories/topology.v index 42c290e4e..4e95029c6 100644 --- a/theories/topology.v +++ b/theories/topology.v @@ -4248,14 +4248,6 @@ suff : R `&` U = R by move: Rx => /[swap] <- []. by apply: ctdR; [exists z|exists U|exists U]. Qed. -Lemma totally_disconnected_compact {T : topologicalType} : - hausdorff_space T -> - compact [set: T] -> - totally_disconnected [set: T] -> - zero_dimensional T. -Proof. -move=> hsdfT cmpT dctT x y xny. - Lemma totally_disconnected_cvg {T : topologicalType} (x : T) : hausdorff_space T -> zero_dimensional T -> compact [set: T] -> filter_from [set D : set T | D x /\ clopen D] id --> x. From 3abeb36cdb64e902abe4ee93e24902d1cb273fd3 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 18 Dec 2023 18:23:31 +0900 Subject: [PATCH 11/22] define variation with path --- theories/realfun.v | 1290 +++++++++++++++++++++++++++----------------- 1 file changed, 783 insertions(+), 507 deletions(-) diff --git a/theories/realfun.v b/theories/realfun.v index 60f7674cf..449d571ef 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1518,631 +1518,908 @@ End is_derive_inverse. #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) => (eapply is_deriveV; first by []) : typeclass_instances. - -Section bounded_variation. +From mathcomp Require Import path. +Require Import sequences. + +Notation "'nondecreasing_fun' f" := ({homo f : n m / (n <= m)%R >-> (n <= m)%R}) + (at level 10). +Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%R >-> (n >= m)%R}) + (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 ler_oppr opprK h. +by rewrite -(opprK (f n)) -ler_oppr 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; rewrite [in X in _ <-> X](_ : f = (\- (\- f))); last first. + by apply/funext => x /=; rewrite opprK. +exact: nondecreasing_funN. +Qed. + +Lemma has_ubound_ereal_sup {R : realType} T (A : set T) (f : T -> R) : + [set f x | x in A] !=set0 -> + has_ubound [set f x | x in A] -> (ereal_sup [set (f x)%:E | x in A] < +oo)%E. +Proof. by move=> A0 ubA; rewrite -image_comp ereal_sup_EFin// ltry. Qed. + +Lemma sup_le {R : realType} (S : set R) x : has_ubound S -> + (exists2 y, S y & x <= y) -> x <= sup S. +Proof. +by move=> uS [y Sy] /le_trans; apply; apply: sup_ub. +Qed. + +(* NB: already in master? *) +Lemma ereal_sup_le {R : realType} (S : set (\bar R)) x : + (exists2 y, S y & x <= y)%E -> (x <= ereal_sup S)%E. +Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ub. Qed. + +Lemma ereal_supy {R : realType} (A : set \bar R) : + A +oo%E -> ereal_sup A = +oo%E. +Proof. +by move=> Aoo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ub. +Qed. + +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 last_filter_lt d {T : porderType d} (h c : T) t : + (h < c)%O -> (last h [seq x <- t | x < c] < c)%O. +Proof. +elim: t h => //= t1 t2 ih h hc. +by case: ifPn => //= t1c; exact: ih. +Qed. + +Lemma 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_inv 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_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). -Fixpoint partition (a b : R) l := - match l with - | nil => False - | p :: nil => p = a /\ p = b - | p :: ((q :: l) as rest) => p = a /\ p <= q /\ partition q b rest - end. +(* a :: s is a of the interval [a, b] *) +Definition itv_partition a b s := [/\ path <%R a s & last a s == b]. -Arguments partition _ _ : simpl never. +Lemma itv_partition_nil a b : itv_partition a b [::] -> a = b. +Proof. by move=> [_ /eqP <-]. Qed. -Lemma partition_le (a b : R) l : partition a b l -> a <= b. -Proof. -by elim: l a => //= a [_ ? [->->] //| ] x l IH ? [<- [ + /IH]]; exact: le_trans. +Lemma itv_partition1 a b : a < b -> itv_partition a b [:: b]. +Proof. by rewrite /itv_partition /= => ->. Qed. + +Lemma itv_partition_cons 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 partition_headE (a b x : R) l : partition a b (x :: l) -> a = x. -Proof. by case: l => [[]|? ? [->]]. 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 partition_tail (a b x y : R) l : - partition a b (x :: y :: l) -> partition y b (y :: l). -Proof. by case=> [-> [//]]. 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_cons - /(_ _)/ltW]. +exact. +Qed. -Lemma partition_consP (a b x y : R) l : partition a b (x :: y :: l) <-> - [/\ a = x, a <= y, y <= b & partition y b (y :: l)]. -Proof. -split; last by case => ->. -move=> /[dup]; case => -> [-> ?] /partition_tail/partition_le ->. -by split. +Lemma itv_partition_tail a b x s : + itv_partition a b (x :: s) -> itv_partition x b s. +Proof. by rewrite /itv_partition/= => -[/andP[]]. 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 partition2 a b : a <= b -> partition a b (a :: b :: nil). -Proof. by split; rewrite //= andbT. 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_tail/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_tail 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)) ler_oppr. +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_filter_lt. +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/(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_inv ht. + by rewrite path_lt_filterT//; exact: path_inv 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 ltr_oppr 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 variationE 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. + +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_norm_add. +by rewrite /= addrACA addrA opprD addrA. +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 variationD a b c f s t : a <= c -> c <= b -> + itv_partition a c s -> itv_partition c b t -> + variation a c f s + variation c b f t = variation a b f (s ++ 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 RHS]/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 RHS](addnK (size s) (size t)). +rewrite -/(index_iota (size s) (size t + size s)). +rewrite -{1}[in RHS](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 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 !variationE//; 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. + rewrite !big_cons/= addrA ler_add// [leRHS]addrC. + by rewrite -[in leLHS](subrK (f c) (f _)) -addrA ler_norm_add. +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 ler_add//. +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 ler_add//= !big_cons !big_nil !addr0/= [leRHS]addrC. +by rewrite -[in leLHS](subrK (f c) (f B0)) -addrA ler_norm_add. +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 ler_add2r. +rewrite -[in leLHS](subrK (f x) (f h)) -addrA (le_trans (ler_norm_add _ _))//. +by rewrite distrC addrC. +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. + +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 partition_concat a b c l1 l2: - partition a b l1 -> partition b c l2 -> partition a c (l1 ++ l2). +Lemma variationsN a b f : variations a b (\- f) = variations a b f. Proof. -elim: l1 a b l2 => // x [_ ? ? l [-> ->]|]. - by case: l => //= ? [[-> -> //]|] ? ? [-> [? ?]]. -move=> a l1 IH p b l2 /partition_consP [-> ? xa ab] pb2. -by rewrite cat_cons; do 2 (split => //); apply: IH; last exact: pb2. +apply/seteqP; split => [_ [s abs] <-|r [s abs]]. + by rewrite variationN; exact: variations_variation. +by rewrite -variationN => <-; exact: variations_variation. Qed. -Lemma partition_concat_tl a b c l1 l2: - partition a b l1 -> partition b c l2 -> partition a c (l1 ++ List.tl l2). +Lemma variationsxx a f : variations a a f = [set 0]. Proof. -elim: l1 a b l2 => // x [? ? ? l2 [-> ->]|]. - by case: l2 => //= ? [[-> -> //]| ? ? [-> [? ?]]]. -move=> a l1 IH p b l2 /partition_consP [-> ? xa ab] pb2. -by rewrite cat_cons; do 2 (split => //); apply: IH; last exact: pb2. +apply/seteqP; split => [x [_ /itv_partitionxx ->]|x ->]. + by rewrite /variation big_nil => <-. +by exists [::] => //=; rewrite /variation /= big_nil. Qed. -Definition pvar part (f : R -> R) := - \sum_(xy <- zip part (List.tl part)) `|f xy.2 - f xy.1|. +Definition bounded_variation a b f := has_ubound (variations a b f). -Definition variations a b f := [set pvar l f | l in partition a b]. +Notation BV := bounded_variation. -Definition total_variation a b (f : R -> R) := - ereal_sup [set x%:E | x in (variations a b f)]. +Lemma bounded_variationxx a f : BV a a f. +Proof. by exists 0 => r; rewrite variationsxx => ->. Qed. -Local Notation TV := total_variation. +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 ler_add//. +- by apply: abfr; exact: variations_variation. +- by apply: abgs; exact: variations_variation. +Qed. -Lemma variations_n0 a b f : a <= b -> variations a b f !=set0. -Proof. by move=> ?; exists (pvar (a :: b :: nil) f), (a::b::nil). Qed. +Lemma bounded_variationN a b f : BV a b f -> BV a b (\- f). +Proof. by rewrite /bounded_variation variationsN. Qed. -Lemma pvar_cons0 f a l : pvar (a :: a :: l) f = pvar (a :: l) f. -Proof. by rewrite /pvar /= big_cons /= subrr normr0 add0r. 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//= ler_add//. +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 pvar_consE f a b l : - pvar (a :: b :: l) f = `|f b - f a| + pvar (b :: l) f. -Proof. by rewrite /pvar /= big_cons. 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//= ler_add. +Qed. -Lemma partition_TV f a b l : - partition a b l -> ((pvar l f)%:E <= TV a b f)%E. +Lemma variations_opp a b f : + variations (- b) (- a) (f \o -%R) = variations a b f. Proof. -move=> pl; rewrite /total_variation/sup/supremum/ereal_sup/supremum. -have alb := partition_le pl. -case E: (_ == _). - have /set0P := (@variations_n0 _ _ f alb); move/eqP/image_set0_set0:E ->. - by move/eqP. -rewrite /has_ubound; case: xgetP. - move=> w wE [] /(_ (pvar l f)%:E) + _; apply; exists (pvar l f) => //. - by exists l. -have [w Qw] := @ereal_supremums_neq0 R [set x%:E | x in variations a b f]. -by move => /(_ w). +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 partition_TV2 a b f: a <= b -> (`|f b - f a|%:E <= TV a b f)%E. +Lemma nondecreasing_bounded_variation a b f : + {in `[a, b] &, {homo f : x y / x <= y}} -> BV a b f. Proof. -move=> ?; suff -> : `|f b - f a| = pvar (a :: b :: nil) f. - by apply: partition_TV => //; exact: partition2. -by rewrite /pvar /= big_seq1. +move=> incf; exists (f b - f a) => ? [l pabl <-]; rewrite le_eqVlt. +by rewrite nondecreasing_variation// eqxx. Qed. -Lemma total_variation_ge0 a b f: a <= b -> (0 <= TV a b f)%E. -Proof. by move=> ab; apply: le_trans; last exact: partition_TV2. Qed. +End bounded_variation. + +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]. -Definition bounded_variation a b (f : R -> R) := - has_ubound (variations a b f). +Notation BV := bounded_variation. +Notation TV := total_variation. -Definition bounded_variationT (f : R -> R) := - forall a b, bounded_variation a b f. +Lemma total_variationxx a f : TV a a f = 0%E. +Proof. by rewrite /total_variation variationsxx image_set1 ereal_sup1. Qed. -Lemma hasNrub_ereal_sup (A : set R) : ~ has_ubound A -> - A !=set0 -> ereal_sup [set x%:E | x in A] = +oo%E. +Lemma total_variation_ge a b f : a <= b -> (`|f b - f a|%:E <= TV a b f)%E. Proof. -move=> hasNubA /[dup] [][a Aa] A0. -apply/eqP; rewrite eq_le leey /= leNgt; apply: contra_notN hasNubA => Aoo. -exists (sup A); apply: sup_ub. -exists (fine (ereal_sup [set x%:E | x in A])) => w Aw. -have -> : w = fine (ereal_sup [set x%:E | x in [set w]]). - by rewrite ereal_sup_EFin /= ?sup1 //; exists w => // ? ->. -rewrite fine_le //. - by rewrite ereal_sup_EFin //=; exists w => // ? ->. - apply/fin_real/andP; split => //. - rewrite ltNge leeNy_eq; apply/negP => /eqP/ereal_sup_ninfty/(_ (w%:E)). - apply/not_implyP; split => //; by exists w. -by apply: le_ereal_sup => ? [? -> <-]; exists w. +rewrite le_eqVlt => /predU1P[<-{b}|ab]. + by rewrite total_variationxx subrr normr0. +apply: ereal_sup_ub => /=; exists (variation a b f [:: b]). + exact/variations_variation/itv_partition1. +by rewrite /variation/= big_nat_recr//= big_nil add0r. Qed. -Lemma bounded_variationP a b f : a <= b -> - bounded_variation a b f <-> TV a b f \is a fin_num. +Lemma total_variation_ge0 a b f : a <= b -> (0 <= TV a b f)%E. +Proof. by move=> ab; rewrite (le_trans _ (total_variation_ge _ ab)). 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. -split; first by move=> ?; rewrite /TV ereal_sup_EFin //; exact: variations_n0. -rewrite ge0_fin_numE ?total_variation_ge0 //; apply: contraPP => Nbdf. -suff -> : (TV a b f = +oo)%E by []. -apply: hasNrub_ereal_sup => //; exact: variations_n0. +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 variationN a b f : variations a b (\- f) = variations a b f. +Lemma bounded_variationP a b f : a <= b -> BV a b f <-> TV a b f \is a fin_num. Proof. -rewrite /variations; suff -> : pvar^~ f = pvar ^~ (\- f) by []. -rewrite /pvar /= funeqE => x /=. -by under eq_bigr => i _ do rewrite -normrN -mulN1r mulrBr ?mulN1r. +rewrite le_eqVlt => /predU1P[<-{b}|ab]. + by rewrite total_variationxx; split => // ?; exact: bounded_variationxx. +rewrite ge0_fin_numE; last exact/total_variation_ge0/ltW. +split=> [abf|]. + apply: has_ubound_ereal_sup => //; rewrite image_id//. + exact: variations_neq0. +rewrite /total_variation /bounded_variation ltey => /eqP; apply: contra_notP. +by move/hasNub_ereal_sup; apply; exact: variations_neq0. Qed. Lemma total_variationN a b f : TV a b (\- f) = TV a b f. -Proof. by rewrite /TV; rewrite variationN. Qed. - -Lemma bounded_variationN a b f : - bounded_variation a b f -> bounded_variation a b (\- f). -Proof. by rewrite /bounded_variation variationN. Qed. - -Lemma bounded_variation_le a b p q f : - bounded_variation a b f -> p <= q -> a <= p -> q <= b -> - bounded_variation p q f. -Proof. -move=> + pq ap qb; have ab : a <= b by exact/(le_trans ap)/(le_trans pq). -case=> M ubdM; exists M => ? [l pql <-]. -apply: (@le_trans _ _ (pvar (a :: l ++ [:: b]) f)). - elim: l a p pq {ab ubdM} ap pql => // ? []. - by move=> _ ?????; rewrite /pvar /= ?big_cons?big_nil addr0; exact: addr_ge0. - move=> w l IH a p => pq ap /partition_consP [ <- ? ? pwl]. - rewrite ?cat_cons pvar_consE pvar_consE pvar_consE. - rewrite [(`|f w - f p|)]distrC addrA [(`|_| + `|_|)]addrC. - rewrite -addrA ler_add // ler_paddl //. - apply: (le_trans (IH w w _ _ _)) => //; rewrite cat_cons pvar_consE subrr. - by rewrite normr0 add0r. -apply: ubdM; exists (a :: l ++ [::b]) => //. -rewrite -cat_cons (_ : [:: b] = List.tl (q :: b ::nil)); last by []. -apply: (@partition_concat_tl _ q) => //. -case: l pql => //?[[-> ->]|]; first by apply: partition2; apply: (le_trans ap). -by move=> ? ? /partition_consP [<- ? ? ?]; apply/partition_consP; split. -Qed. - -Let total_variation_concat_le a b c f : - a <= b -> b <= c -> (TV a b f + TV b c f <= TV a c f)%E. -Proof. -move=> ab bc; have ac : a <= c by exact: (le_trans ab). -case : (pselect (bounded_variation a c f)); first last. - move=> nbdac; suff /eqP -> : TV a c f == +oo%E by rewrite leey. - have: (-oo < TV a c f)%E by apply: (lt_le_trans _ (total_variation_ge0 f ac)). - by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ ac). -move=> bdAC. -have bdf1 : bounded_variation a b f by exact: (bounded_variation_le bdAC). -have bdf2 : bounded_variation b c f by exact: (bounded_variation_le bdAC). -rewrite /total_variation ?ereal_sup_EFin => //; try exact: variations_n0. -rewrite -EFinD -sup_sumE /has_sup; try (by split => //; exact: variations_n0). +Proof. by rewrite /TV; rewrite variationsN. Qed. + +Lemma total_variation_le a b f g : a <= b -> + (TV a b (f \+ g)%R <= TV a b f + TV a b g)%E. +Proof. +rewrite le_eqVlt => /predU1P[<-{b}|ab]. + by rewrite !total_variationxx adde0. +have [abf|abf] := pselect (BV a b f); last first. + rewrite {2}/total_variation hasNub_ereal_sup//; last first. + exact: variations_neq0. + rewrite addye ?leey// -ltNye (@lt_le_trans _ _ 0%E)//. + exact/total_variation_ge0/ltW. +have [abg|abg] := pselect (BV a b g); last first. + rewrite {3}/total_variation hasNub_ereal_sup//; last first. + exact: variations_neq0. + rewrite addey ?leey// -ltNye (@lt_le_trans _ _ 0%E)//. + exact/total_variation_ge0/ltW. +move: abf abg => [r abfr] [s abgs]. +have BVabfg : BV a b (f \+ g). + by apply: bounded_variationD => //; [exists r|exists s]. +apply: ub_ereal_sup => y /= [r' [s' abs <-{r'} <-{y}]]. +apply: (@le_trans _ _ (variation a b f s' + variation a b g s')%:E). + exact: variation_le. +by rewrite EFinD lee_add// ereal_sup_le//; + (eexists; last exact: lexx); (eexists; last reflexivity); + exact: variations_variation. +Qed. + +Let total_variationD1 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. +have [abf|abf] := pselect (BV a b f); last first. + rewrite {3}/total_variation hasNub_ereal_sup ?leey//. + by apply: variations_neq0 => //; rewrite (lt_trans ac). +have H s t : itv_partition a c s -> itv_partition c b t -> + (TV a b f >= (variation a c f s)%:E + (variation c b f t)%:E)%E. + move=> acs cbt; rewrite -EFinD; apply: ereal_sup_le. + exists (variation a b f (s ++ t))%:E. + eexists; last reflexivity. + by exists (s ++ t) => //; exact: itv_partition_cat acs cbt. + by rewrite variationD// ltW. +rewrite [leRHS]ereal_sup_EFin//; last first. + by apply: variations_neq0; rewrite (lt_trans ac). +have acf : BV a c f := bounded_variationl (ltW ac) (ltW cb) abf. +have cbf : BV c b f := bounded_variationr (ltW ac) (ltW cb) abf. +rewrite {1 2}/total_variation ereal_sup_EFin//; last exact: variations_neq0. +rewrite ereal_sup_EFin//; last exact: variations_neq0. +rewrite -EFinD -sup_sumE; last 2 first. + by split => //; exact: variations_neq0. + by split => //; exact: variations_neq0. apply: le_sup. -- move=> ? [? [l1 pabl2 <-]] [? [l2 pbcl2 <-] <-]; exists (pvar (l1 ++ List.tl l2) f). - split; first by exists (l1 ++ List.tl l2)=> //=; apply: (partition_concat_tl pabl2). - rewrite /pvar -big_cat /=. - rewrite (_ : (zip l1 (List.tl l1) ++ zip l2 (List.tl l2)) = zip (l1 ++ List.tl l2) (List.tl (l1 ++ List.tl l2))) //. - elim: l1 a {bdf1 bdf2 bdAC ac ab} pabl2 pbcl2 => // x [/= _ ? [-> ->]|]. - by move=> bc2; congr (_ _ _); case: l2 bc2 => // ? ? /partition_headE ->. - move=> z ? IH ? pabl1 pbcl2 /=; congr (_ _); apply: (IH z) => //. - by case: pabl1 => /= _ [_]. -- have [x0 vx0] := (variations_n0 f ab). - have [y0 vy0] := (variations_n0 f bc). - exists (x0 + y0); exists x0 => //; exists y0 => //. -- split => //; exact: variations_n0. -Qed. - -Fixpoint part_split x (l : seq R) := - match l with - | [::] => ([::x], [::x]) - | y :: tl => if x < y then ([:: x], x :: y :: tl) else - let xy := part_split x tl - in (y :: xy.1, xy.2 ) - end. - -Lemma part_splitl a b x l : - a <= x -> x <= b -> partition a b l -> - partition a x (part_split x l).1. -Proof. -elim: l a => // a [/= _ ? ax bx|]. - move: ax => /[swap]; move: bx => /[swap] [[-> ->]] ? ?. - have -> : x = b by apply/ le_anti/andP; split. - by rewrite lt_irreflexive /=; repeat split. -move=> w l IH ? + xb /partition_consP => /[swap] [[->]] aw wb wbl ax /=. -rewrite ltNge ax /= /=; case Nxw: (x < w) => //=. -have wx : w <= x by rewrite leNgt Nxw. -apply/partition_consP; split => //. -by have /= := IH w wx xb wbl; rewrite Nxw. -Qed. - -Lemma part_splitr a b x l : - a <= x -> x <= b -> partition a b l -> - partition x b (part_split x l).2. -Proof. -elim: l a => // a [/= _ ? ax bx|]. - case=> -> ->; move: (bx); rewrite le_eqVlt => /orP. - by case=> [/eqP ->|->]; rewrite ?lt_irreflexive //=. -move=> w l IH ? + xb /partition_consP => /[swap] [[->]] aw wb wbl ax /=. -rewrite ltNge ax /= /=; case Nxw: (x < w) => //=. - by apply/partition_consP; split => //; apply: ltW. -have wx : w <= x by rewrite leNgt Nxw. -by have /= := IH w wx xb wbl; rewrite Nxw. -Qed. - -Lemma part_split_pvar a b x l f : - partition a b l -> - a <= x -> x <= b -> - pvar l f <= pvar (part_split x l).1 f + pvar (part_split x l).2 f. -Proof. -move=> + + xb; elim: l a => // a [_ w [<- -> bx]|]. - by rewrite /pvar [x in x <= _]/= big_nil addr_ge0 //; apply: sumr_ge0 => ?. -move=> w l IH ? /partition_consP [-> aw wb pwbl ax]. -rewrite /= ?[x < a]ltNge ?ax /=; case Nxw: (x < w) => /=. - rewrite /pvar /= ?big_cons /= ?big_nil addr0 addrA. - by rewrite ler_add2r [x in _ <= x]addrC ler_dist_add. -rewrite /pvar /= ?big_cons /= -?addrA ler_add2l. -have wx : w <= x by rewrite leNgt Nxw. -by have /= := IH w pwbl wx; rewrite Nxw /=. -Qed. - -Let total_variation_concat_ge a b c f : - a <= b -> b <= c -> (TV a b f + TV b c f >= TV a c f)%E. -Proof. -move=> ab bc; have ac : a <= c by exact: (le_trans ab). -case : (pselect (bounded_variation a b f)); first last. - move=> nbdac; have /eqP -> : TV a b f == +oo%E. - have: (-oo < TV a b f)%E by apply: (lt_le_trans _ (total_variation_ge0 f ab)). - by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ ab). - by rewrite addye ?leey // -ltNye (@lt_le_trans _ _ 0)%E // ?total_variation_ge0 //. -case : (pselect (bounded_variation b c f)); first last. - move=> nbdac; have /eqP -> : TV b c f == +oo%E. - have: (-oo < TV b c f)%E by apply: (lt_le_trans _ (total_variation_ge0 f bc)). - by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ bc). - by rewrite addey ?leey // -ltNye (@lt_le_trans _ _ 0)%E // ?total_variation_ge0 //. +- move=> r/= [s [l' acl' <-{s}]] [t [l cbl] <-{t} <-{r}]. + exists (variation a b f (l' ++ l)); split; last by rewrite variationD// ltW. + exact/variations_variation/(itv_partition_cat acl' cbl). +- have [r acfr] := variations_neq0 f ac. + have [s cbfs] := variations_neq0 f cb. + by exists (r + s); exists r => //; exists s. +- by split => //; apply: variations_neq0; rewrite (lt_trans ac). +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. +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))). + by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ (ltW ac)). + by rewrite addye ?leey // -ltNye (@lt_le_trans _ _ 0)%E // ?total_variation_ge0 // ltW. +case : (pselect (bounded_variation c b f)); first last. + move=> nbdac; have /eqP -> : TV c b f == +oo%E. + have: (-oo < TV c b f)%E. + exact: (lt_le_trans _ (total_variation_ge0 f (ltW cb))). + by rewrite ltNye_eq => /orP [] => // /bounded_variationP => /(_ (ltW cb)). + rewrite addey ?leey // -ltNye (@lt_le_trans _ _ 0%E)//. + exact/total_variation_ge0/ltW. move=> bdAB bdAC. -rewrite /total_variation [x in (x + _)%E]ereal_sup_EFin => //; try exact: variations_n0. -rewrite [x in (_ + x)%E]ereal_sup_EFin => //; try exact: variations_n0. -rewrite -EFinD -sup_sumE /has_sup; try (by split => //; exact: variations_n0). +rewrite /total_variation [x in (x + _)%E]ereal_sup_EFin //; last first. + exact: variations_neq0. +rewrite [x in (_ + x)%E]ereal_sup_EFin //; last exact: variations_neq0. +rewrite -EFinD -sup_sumE /has_sup; [|(by split => //; exact: variations_neq0)..]. apply: ub_ereal_sup => ? [? [l pacl <- <-]]; rewrite lee_fin. -apply: le_trans; first exact: (@part_split_pvar a c b). -apply: sup_ub. +apply: (le_trans (variation_itv_partitionLR _ ac _ _)) => //. +apply: sup_ub => /=. case: bdAB => M ubdM; case: bdAC => N ubdN; exists (N + M). move=> q [?] [i pabi <-] [? [j pbcj <-]] <-. - by apply: ler_add; [apply: ubdN;exists i|apply:ubdM;exists j]. -exists (pvar (part_split b l).1 f). - by exists (part_split b l).1 => //; apply: (@part_splitl a c). -exists (pvar (part_split b l).2 f) => //. -by exists (part_split b l).2 => //; apply: (@part_splitr a c). + by apply: ler_add; [apply: ubdN;exists i|apply:ubdM;exists j]. +exists (variation a c f (itv_partitionL l c)). + by apply: variations_variation; exact: itv_partitionLP pacl. +exists (variation c b f (itv_partitionR l c)). + by apply: variations_variation; exact: itv_partitionRP pacl. +by rewrite variationD// ?ltW//; + [exact: itv_partitionLP pacl|exact: itv_partitionRP pacl]. Qed. - -Lemma total_variation_concatE a b c f : - a <= b -> b <= c -> (TV a b f + TV b c f = TV a c f)%E. + +Lemma total_variationD a b c f : a <= c -> c <= b -> + (TV a b f = TV a c f + TV c b f)%E. Proof. -move=> ab bc; apply/le_anti/andP; split. - exact: total_variation_concat_le. -exact: total_variation_concat_ge. +by move=> ac cb; apply/eqP; rewrite eq_le; apply/andP; split; + [exact: total_variationD2|exact: total_variationD1]. Qed. +End total_variation. -Definition neg_tv a f (x:R) : \bar R := ((TV a x f - (f x)%:E)*2^-1%:E)%E. +Lemma at_left_at_rightP + {T : topologicalType} {R : realType} (f : R -> T) x (z : T) : + f @ x^'- --> z <-> f \o -%R @ (- x)^'+ --> z. +Proof. +suff -> : (- x)^'+ = (-%R) @ x^'-. + by rewrite -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK. +rewrite eqEsubset /=; split. + move=> E /= [r rpos xb]; exists r => //. + move=> t /= xtr tx; apply: xb. + by rewrite /= -opprB opprK normrN addrC. + by rewrite ltr_oppr opprK. +move=> E /= [r rpos xb]; exists r => //. +move=> t /= xtr tx; rewrite -[t]opprK; apply: xb. + by rewrite /= opprK -normrN opprD. +by rewrite ltr_oppl. +Qed. + +Lemma left_right_continuousP + {T: topologicalType} {R : realType} (f : R -> T) x : + (f @ x^'- --> f x /\ f @ x^'+ --> f x) <-> f @ x --> f x. +Proof. +split; first last. + by move=> cts; split; exact: cvg_within_filter. +case => + + U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl. +rewrite ?near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf. +near=> t => xlt xgt; have := @real_leVge R x t; rewrite ?num_real. +move=> /(_ isT isT) /orP; rewrite ?le_eqVlt; case => /orP; case => //. + by move/eqP <-; apply: nbhs_singleton. +by move/eqP ->; apply: nbhs_singleton. +Unshelve. all: by end_near. Qed. -Definition pos_tv a f (x:R) : \bar R := neg_tv a (\- f) x. +Section variation_continuity. +Context {R : realType}. +Implicit Type f : R -> R. -Lemma neg_TV_increasing a b (f : R -> R) : - {in `[a,b] &, {homo (neg_tv a f) : x y / x <= y >-> (x <= y)%E}}. +Notation BV := bounded_variation. +Notation TV := total_variation. + +Definition neg_tv a f (x : R) : \bar R := ((TV a x f - (f x)%:E) * 2^-1%:E)%E. + +Definition pos_tv a f (x : R) : \bar R := neg_tv a (\- f) x. + +Lemma neg_TV_increasing a b f : + {in `[a, b] &, {homo (neg_tv a f) : x y / x <= y >-> (x <= y)%E}}. Proof. move=> x y xab yab xy; have ax : a <= x. by move: xab; rewrite in_itv //= => /andP []. rewrite /neg_tv lee_pmul2r // lee_subr_addl // addeCA -EFinB. -rewrite -[TV a y _](@total_variation_concatE _ x) //. -apply: lee_add => //; apply: le_trans; last exact: partition_TV2. +rewrite [TV a y _](total_variationD _ ax xy) //. +apply: lee_add => //; apply: le_trans; last exact: total_variation_ge. by rewrite lee_fin ler_norm. Qed. -Lemma total_variation_jordan_decompE a b f : - bounded_variation a b f -> - {in `[a,b], f =1 (fine \o neg_tv a (\- f)) \- (fine \o neg_tv a f)}. +Lemma total_variation_jordan_decompE a b f : BV a b f -> + {in `[a, b], f =1 (fine \o neg_tv a (\- f)) \- (fine \o neg_tv a f)}. Proof. move=> bdabf x; rewrite in_itv /= => /andP [ax xb]. have ffin: TV a x f \is a fin_num. - by apply/bounded_variationP => //; apply: (bounded_variation_le bdabf). + apply/bounded_variationP => //. + exact: (bounded_variationl _ xb). have Nffin : TV a x (\- f) \is a fin_num. apply/bounded_variationP => //; apply/bounded_variationN. - exact: (bounded_variation_le bdabf). + exact: (bounded_variationl ax xb). rewrite /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //; first last. - by rewrite fin_numM // fin_numD; apply/andP; split. - by rewrite fin_numM // fin_numD; apply/andP; split. - by apply: fin_num_adde_defl; rewrite fin_numN fin_numD; apply/andP; split. - by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split. rewrite addeAC oppeD //= ?fin_num_adde_defl //. -by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -splitr. +by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -Num.Theory.splitr. Qed. -Lemma neg_TV_increasing_fin a b (f : R -> R) : - bounded_variation a b f -> +Lemma neg_TV_increasing_fin a b f : BV a b f -> {in `[a,b] &, {homo (fine \o neg_tv a f) : x y / x <= y}}. Proof. move=> bdv p q pab qab pq /=. -move: (pab) (qab); rewrite ?in_itv /= => /andP [? ?] /andP [? ?]. +move: (pab) (qab); rewrite ?in_itv /= => /andP[ap pb] /andP[aq qb]. apply: fine_le; rewrite /neg_tv ?fin_numM // ?fin_numB /=. - apply/andP; split => //; apply/bounded_variationP => //. - exact: (bounded_variation_le bdv). + exact: (bounded_variationl _ pb). - apply/andP; split => //; apply/bounded_variationP => //. - exact: (bounded_variation_le bdv). -by apply: (neg_TV_increasing _ pab). + exact: (bounded_variationl _ qb). +exact: (neg_TV_increasing _ pab). Qed. -Lemma increasing_bounded_variation a b (f : R -> R) : - {in `[a,b] &, {homo f : x y / x <= y}} -> - bounded_variation a b f. +Lemma neg_TV_bounded_variation a b f : BV a b f -> + BV a b (fine \o neg_tv a f). Proof. -move=> incf; exists (f b - f a) => ? [l pabl <-]; rewrite le_eqVlt. -apply/orP; left; apply/eqP. -rewrite /pvar; elim: l a incf pabl => // ? []. - by move=> _ ? _ [-> ->]; rewrite /= big_nil subrr. -move=> w l IH a fi /[dup]/partition_le ab /[dup]/partition_tail/[dup] ?. -move=> /partition_le wb [] => [-> [aw _]]; rewrite /= big_cons /=. -rewrite (IH w) //; first last. - move=> p q; rewrite in_itv /= => /andP [? ?] /andP [? ?] pq. - by apply: fi; rewrite //in_itv; apply/andP; split => //; exact: (le_trans aw). -have -> : `|f w - f a| = f w - f a. - rewrite ger0_norm // subr_ge0; apply: fi => //; rewrite // in_itv /=. - by apply/andP; split => //. - by apply/andP; split => //. -by rewrite addrCA; congr (_ _); rewrite addrC addrA [-_ + _]addrC subrr add0r. -Qed. - -Lemma neg_TV_bounded_variation a b f : - bounded_variation a b f -> - bounded_variation a b (fine \o neg_tv a f). -Proof. -by move=> ?; apply increasing_bounded_variation; apply: neg_TV_increasing_fin. -Qed. - -Fixpoint collapse_head (l : seq R) := - match l with - | nil => nil - | x :: nil => x :: nil - | x :: ((y :: _) as tl) => if x == y then collapse_head tl else x :: tl - end. - -Lemma collapse_head_consE x l : - collapse_head (x :: x :: l) = collapse_head (x :: l). -Proof. by rewrite /= eq_refl. Qed. - -Lemma collapse_head_consNE x y l : - x != y -> collapse_head (x :: y :: l) = x :: y :: l. -Proof. -move=> xy; case E: (x == y). - by move/eqP: E xy => ->; rewrite eq_refl. -by rewrite /= E. -Qed. - -Lemma collapse_head_partition a b l : - a <= b -> partition a b l -> partition a b (collapse_head l). -Proof. -elim: l a => // a [//| w l IH] ? /[swap] /partition_consP [-> + wb wbl ab]. -rewrite le_eqVlt => /orP [|]. - by move/eqP=> ->; rewrite collapse_head_consE; exact: IH. -move=> aw; rewrite collapse_head_consNE => //. - by apply/partition_consP; split => //; exact: ltW. -by apply/negP=> E; move /eqP: E aw => ->; rewrite lt_irreflexive. -Qed. - -Lemma collapse_head_pvar l f: - pvar l f = pvar (collapse_head l) f. -Proof. -elim: l => // w [//|] y l; case E: (w == y). - by move/eqP: E => ->; rewrite pvar_cons0 collapse_head_consE. -by rewrite collapse_head_consNE //; rewrite E. -Qed. - -Lemma collapse_head_neq l a b tl: - (collapse_head l) = a :: b :: tl -> a != b. -Proof. -elim: l a b tl => // w [//=|x l IH] a b tl. -case E: (w == x). - move/eqP: E => ->; rewrite collapse_head_consE; apply: IH. -rewrite collapse_head_consNE ?E //. -by case=> <- <- _; rewrite E. -Qed. - -Lemma TV_right_continuous a b x (f : R -> R) : - a <= x -> x < b -> - (f @ at_right x --> f x) -> - bounded_variation a b f -> - (fine \o TV a ^~ f @ at_right x --> fine (TV a x f)). +move=> ?; apply: nondecreasing_bounded_variation. +exact: neg_TV_increasing_fin. +Qed. + +Lemma TV_right_continuous a b x f : a <= x -> x < b -> + f @ at_right x --> f x -> + BV a b f -> + fine \o TV a ^~ f @ at_right x --> fine (TV a x f). Proof. move=> ax xb ctsf bvf; have ? : a <= b by apply:ltW; apply: (le_lt_trans ax). apply/cvgrPdist_lt=> _/posnumP[eps]. have ? : Filter (nbhs x^'+) by exact: at_right_proper_filter. have xbl := ltW xb. have xbfin : TV x b f \is a fin_num. - by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). -have [//|?] := @ub_ereal_sup_adherent R _ (eps%:num/2) _ xbfin. + by apply/bounded_variationP => //; exact: (bounded_variationr _ _ bvf). +have [//|?] := @ub_ereal_sup_adherent R _ (eps%:num / 2) _ xbfin. case=> ? [l + <- <-]; rewrite -/(total_variation x b f). -rewrite collapse_head_pvar => /(collapse_head_partition xbl). -case E : (collapse_head l) => //; move: E. -set i := (w in _ :: w); case: i => //. - by move=> _ []; move: xb => /[swap] -> /[swap] ->; rewrite lt_irreflexive. -move=> i j /collapse_head_neq /[swap] /[dup] /partition_consP [<-]; rewrite le_eqVlt. -move=> /orP [/eqP ->|]; rewrite ?eq_refl => // xi ib pibj pxij _ tv_eps. -apply: filter_app (nbhs_right_ge _). +move: l => [|i j]. + by move=> /itv_partition_nil /eqP; rewrite lt_eqF. +move=> [/= /andP[xi ij /eqP ijb]] tv_eps. +apply: filter_app (nbhs_right_ge _). apply: filter_app (nbhs_right_lt xi). -have e20 : 0 < eps%:num/2 by []. -move/cvgrPdist_lt/(_ (eps%:num/2) e20):ctsf; apply: filter_app. -near=> t => fxt ti xt; have ? : a <= t by exact: (le_trans ax). -have ? : x <= b by apply: ltW; exact: (lt_le_trans xi). -have tb : t <= b by apply: ltW; exact: (lt_le_trans ti). -rewrite -fineB; first last. - apply/bounded_variationP => //; apply: (bounded_variation_le bvf) => //. - by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). -rewrite -(total_variation_concatE _ ax xt). -rewrite oppeD ?fin_num_adde_defl //; first last. - by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). -have xtfin : TV x t f \is a fin_num. - by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). +have e20 : 0 < eps%:num / 2 by []. +move/cvgrPdist_lt/(_ (eps%:num/2) e20) : ctsf; apply: filter_app. +near=> t => fxt ti xt; have ta : a <= t by exact: (le_trans ax). +have tb : t <= b by rewrite (le_trans (ltW ti))// -ijb path_lt_le_last. +rewrite -fineB; last 2 first. + by apply/bounded_variationP => //; exact: bounded_variationl bvf. + by apply/bounded_variationP => //; exact: bounded_variationl bvf. +rewrite (total_variationD _ ax xt). have tbfin : TV t b f \is a fin_num. - by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). -rewrite addeA subee //; first last. - by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). -rewrite sub0e fineN normrN ger0_norm; first last. - rewrite fine_ge0 //; exact: total_variation_ge0. -move: (tv_eps); rewrite -(total_variation_concatE f _ tb) //. -pose r := [:: x, i & j]. -have := part_split_pvar f pxij xt tb. + by apply/bounded_variationP => //; exact: (@bounded_variationr _ a). +have xtfin : TV x t f \is a fin_num. + apply/bounded_variationP => //; apply: (@bounded_variationl _ _ _ b) => //. + exact: (@bounded_variationr _ a). +rewrite oppeD ?fin_num_adde_defl// addeA subee //; first last. + by apply/bounded_variationP => //; exact: (@bounded_variationl _ _ _ b). +rewrite sub0e fineN normrN ger0_norm; last first. + by rewrite fine_ge0// total_variation_ge0. +move: (tv_eps); rewrite (total_variationD f _ tb) //. +move: xt; rewrite le_eqVlt => /predU1P[->|xt]. + by rewrite total_variationxx/=. +have : variation x b f (i :: j) <= variation x t f (t :: nil) + + variation t b f (i :: j). + rewrite variationD//; last 2 first. + exact: itv_partition1. + by rewrite /itv_partition/= ti ij ijb. + exact: le_variation. rewrite -lee_fin => /lt_le_trans /[apply]. -have -> : part_split t [:: x, i & j] = (x :: t :: nil, [:: t, i & j]). - by rewrite /part_split; rewrite ?ti ltNge xt /=. -rewrite /= -addeA -lte_subr_addr; first last. - by rewrite fin_numD; apply/andP; split => //. -rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA. +rewrite {1}variationE; last exact: itv_partition1. +rewrite /= -addeA -lte_subr_addr; last by rewrite fin_numD; apply/andP. +rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA. move/lt_trans; apply. -rewrite [x in (_ < x%:E)%E]splitr EFinD addeC lte_add2lE //. -rewrite -addeA; apply: (@le_lt_trans _ _ (pvar [::x;t] f)%:E). - rewrite gee_addl // sube_le0; apply: ereal_sup_ub. - exists (pvar [::t,i&j] f) => //; exists [::t,i&j] => //. - by apply/partition_consP; split => //; apply: ltW. - by rewrite /pvar /= big_seq1 /= distrC lte_fin. +rewrite [x in (_ < x%:E)%E]Num.Theory.splitr EFinD addeC lte_add2lE //. +rewrite -addeA. +apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E). + rewrite [in leRHS]variationE; last exact: itv_partition1. + rewrite gee_addl // sube_le0; apply: ereal_sup_ub => /=. + exists (variation t b f (i :: j)) => //. + apply: variations_variation. + by rewrite /itv_partition/= ijb ij ti. +by rewrite /variation/= big_nat_recr//= big_nil add0r distrC lte_fin. Unshelve. all: by end_near. Qed. -Lemma neg_TV_right_continuous a x b (f : R -> R) : - a <= x -> x < b -> - bounded_variation a b f -> - (f @ at_right x --> f x) -> - (fine \o neg_tv a f @ at_right x --> fine (neg_tv a f x)). +Lemma neg_TV_right_continuous a x b f : a <= x -> x < b -> + BV a b f -> + f @ x^'+ --> f x -> + fine \o neg_tv a f @ x^'+ --> fine (neg_tv a f x). Proof. -move=> ax ? bvf fcts; have xb : x <= b by exact: ltW. +move=> ax ? bvf fcts; have xb : x <= b by exact: ltW. have xbfin : TV a x f \is a fin_num. - by apply/bounded_variationP => //; apply: (bounded_variation_le bvf). + by apply/bounded_variationP => //; exact: bounded_variationl bvf. apply: fine_cvg; rewrite /neg_tv fineM // ?fin_numB ?xbfin //= EFinM. under eq_fun => i do rewrite EFinN. -apply: cvg_trans; first (apply: cvgeMr => //); last exact: cvg_id. +apply: cvg_trans; first (apply: cvgeMr => //); last exact: cvg_id. rewrite fineD // EFinB; apply: cvgeB => //. apply/ fine_cvgP; split; first exists (b-x). - by rewrite /= subr_gt0. - move=> t /= xtbx xt; have ? : a <= t. by apply: ltW; apply: (le_lt_trans ax). - apply/bounded_variationP => //; apply: (bounded_variation_le bvf) => //. + apply/bounded_variationP => //. + apply: bounded_variationl bvf => //. move: xtbx; rewrite distrC ger0_norm ?subr_ge0; last by exact: ltW. by rewrite ltr_subr_addr -addrA [-_ + _]addrC subrr addr0 => /ltW. - by apply: TV_right_continuous => //; last exact: bvf => //. + by apply: TV_right_continuous => //; last exact: bvf. apply: cvg_comp; first exact: fcts. apply/ fine_cvgP; split; first by near=> t => //. -by have -> : (fine \o EFin = id) by move=> ?; rewrite funeqE => ? /=. +by have -> : fine \o EFin = id by move=> ?; rewrite funeqE => ? /=. Unshelve. all: by end_near. Qed. -Lemma pvarNE (l : seq R) f : - pvar l f = pvar (map (-%R) l) (f \o (-%R)). -Proof. -elim: l; first by rewrite /pvar /= !big_nil. -move=> a [|]; first by move=> _ /=; rewrite /pvar /= !big_nil. -by move=> w l IH; rewrite /= ?pvar_consE /= ?opprK; congr( _ + _). -Qed. - -Lemma pvarNE2 (l : seq R) f : - pvar (map (-%R) l) f = pvar l (f \o (-%R)). -Proof. -have NE : (-%R) \o (-%R) = @id R. - by apply: eq_fun => ?; rewrite opprK. -have compE g : g \o id = g by apply: eq_fun. -by rewrite (_ : f = f \o (-%R) \o (-%R)) -?pvarNE -compA NE compE. -Qed. - -Lemma partition_rev a b l : - partition a b l -> partition (-b) (-a) (rev (map (-%R) l)). -Proof. -elim: l a b => // => w []. - by move=> /= _ ? ? [] <- <-; split. -move=> y l; set j := y :: l => IH a b /partition_consP [<-] ay yb pyb. -have /(@partition_concat_tl _ _ _ _ (-y :: -a :: nil)) := IH _ _ pyb. -rewrite /= rev_cons -cats1 ?rev_cons -?cats1; apply. -by split => //; repeat split => //; rewrite ler_opp2. -Qed. - -Lemma pvar_cat a (l1 l2 : seq R) f : - pvar (l1 ++ a :: l2) f = pvar (l1 ++ [:: a]) f + pvar (a :: l2) f. -Proof. -elim: l1 a l2; first by move => ? ?; rewrite /= /pvar /= big_nil /= add0r. -move=> w []. - by move=> _ ? ? /=; rewrite ?pvar_consE /= /pvar /= big_nil /= -addrA add0r. -move=> y l1 IH a l2. -by rewrite ?cat_cons ?pvar_consE IH ?cat_cons addrA. -Qed. - -Lemma pvar_revE (l : seq R) f : - pvar l f = pvar (rev l) f. -Proof. -elim: l; first by rewrite /pvar /= !big_nil. -move=> a [|]; first by move=> _ /=; rewrite /pvar /= !big_nil. -move=> w l IH; rewrite pvar_consE; rewrite distrC IH. -rewrite ?rev_cons -?cats1 -catA [x in _ = x]pvar_cat addrC; congr (_ + _). -by rewrite pvar_consE /pvar big_nil addr0. -Qed. - -Lemma variation_revE a b f: - variations (-b) (-a) (f \o [eta -%R]) = variations a b f. -Proof. -rewrite eqEsubset; split => ?. - move=> [l] /partition_rev + <-; rewrite ?opprK => plrev. - by rewrite -pvarNE2 pvar_revE; exists (rev (map (-%R) l)) => //. -have fNE : f = (f \o -%R) \o -%R. - by apply: eq_fun => ?; rewrite /= opprK. -rewrite -{1}[a]opprK -{1}[b]opprK fNE. -move=> [l] /partition_rev + <-; rewrite ?opprK => plrev. -rewrite -pvarNE2 pvar_revE; exists (rev (map (-%R) l)) => //. -by rewrite -compA fNE; congr (_ _ ); apply: eq_fun => ?; rewrite /= ?opprK. -Qed. - -Lemma total_variation_revE a b f: - TV a b f = TV (-b) (-a) (f \o (-%R)). -Proof. by rewrite /total_variation -variation_revE. Qed. - -Lemma at_left_at_rightP {T: topologicalType} (f : R -> T) x (z:T): - f @ at_left x --> z <-> - f \o (-%R) @ at_right (-x) --> z. -Proof. -suff -> : (- x)^'+ = (-%R) @ x^'-. - by rewrite -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK. -rewrite eqEsubset /=; split. - move=> E /= [r rpos xb]; exists r => //. - move=> t /= xtr tx; apply: xb. - by rewrite /= -opprB opprK normrN addrC. - by rewrite ltr_oppr opprK. -move=> E /= [r rpos xb]; exists r => //. -move=> t /= xtr tx; rewrite -[t]opprK; apply: xb. - by rewrite /= opprK -normrN opprD. -by rewrite ltr_oppl. -Qed. - -Lemma left_right_continuousP {T: topologicalType} (f : R -> T) x: - (f @ at_left x --> f x /\ - f @ at_right x --> f x) <-> - f @ x --> f x. -Proof. -split; first last. - by move=> cts; split; exact: cvg_within_filter. -case => + + U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl. -rewrite ?near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf. -near=> t => xlt xgt; have := @real_leVge R x t; rewrite ?num_real. -move=> /(_ isT isT) /orP; rewrite ?le_eqVlt; case => /orP; case => //. - by move/eqP <-; apply: nbhs_singleton. -by move/eqP ->; apply: nbhs_singleton. -Unshelve. all: by end_near. Qed. +Lemma total_variation_opp a b f : TV a b f = TV (- b) (- a) (f \o -%R). +Proof. by rewrite /total_variation variations_opp. Qed. -Lemma TV_left_continuous a b x (f : R -> R) : - a < x -> x <= b -> - (f @ at_left x --> f x) -> - bounded_variation a b f -> - (fine \o TV a ^~ f @ at_left x --> fine (TV a x f)). +Lemma TV_left_continuous a b x f : a < x -> x <= b -> + f @ at_left x --> f x -> + BV a b f -> + fine \o TV a ^~ f @ x^'- --> fine (TV a x f). Proof. move=> ax xb fNcts bvf. -apply/at_left_at_rightP; rewrite total_variation_revE. -have bvNf : bounded_variation (-b) (-a) (f \o -%R). - by case:bvf=> M; rewrite -variation_revE => ?; exists M. -have bx : -b <= -x by rewrite ler_oppl opprK. -have xa : -x < -a by rewrite ltr_oppl opprK. -have ? : -x <= -a by apply: ltW. +apply/at_left_at_rightP; rewrite total_variation_opp. +have bvNf : BV (-b) (-a) (f \o -%R). + by case: bvf => M; rewrite -variations_opp => ?; exists M. +have bx : - b <= - x by rewrite ler_oppl opprK. +have xa : - x < - a by rewrite ltr_oppl opprK. +have ? : - x <= - a by exact: ltW. have ? : Filter (nbhs (-x)^'+) by exact: at_right_proper_filter. -have -> : fine (TV (-x) (-a) (f \o -%R)) = +have -> : fine (TV (-x) (-a) (f \o -%R)) = fine (TV (-b) (-a) (f \o -%R)) - fine (TV (-b) (-x) (f \o -%R)). apply/eqP; rewrite -subr_eq opprK addrC. - rewrite -fineD ?total_variation_concatE //. - - by apply/bounded_variationP => //; apply: (bounded_variation_le bvNf). - - by apply/bounded_variationP => //; apply: (bounded_variation_le bvNf). -have /near_eq_cvg/cvg_trans : {near ((-x)^'+), - (fun t => fine (TV (-b) (-a) (f \o -%R)) - fine (TV (-b) t (f\o-%R))) =1 - (fine \o (TV a)^~ f) \o -%R }. + rewrite -fineD; last 2 first. + by apply/bounded_variationP => //; exact: bounded_variationl bvNf. + by apply/bounded_variationP => //; exact: bounded_variationr bvNf. + by rewrite -total_variationD. +have /near_eq_cvg/cvg_trans : {near (- x)^'+, + (fun t => fine (TV (- b) (- a) (f \o -%R)) - fine (TV (- b) t (f \o -%R))) =1 + (fine \o (TV a)^~ f) \o -%R}. apply: filter_app (nbhs_right_lt xa). apply: filter_app (nbhs_right_ge _). near=> t => xt ta; have ? : -b <= t by exact: (le_trans bx). have ? : t <= -a by exact: ltW. apply/eqP; rewrite eq_sym -subr_eq opprK addrC. - rewrite /= [TV a _ f]total_variation_revE opprK -fineD ?total_variation_concatE //. - - by apply/bounded_variationP => //; apply: (bounded_variation_le bvNf) => //. - - by apply/bounded_variationP => //; apply: (bounded_variation_le bvNf). + rewrite /= [TV a _ f]total_variation_opp opprK -fineD; last first. + by apply/bounded_variationP => //; apply: bounded_variationr bvNf. + by apply/bounded_variationP => //; apply: bounded_variationl bvNf. + by rewrite -total_variationD. apply. apply: cvgB; first exact: cvg_cst. apply: (TV_right_continuous _ _ _ bvNf). @@ -2157,15 +2434,14 @@ Lemma continuous_within_itvP a b (f : R -> R) : Proof. Admitted. -Lemma TV_continuous a b (f : R -> R) : - a < b -> +Lemma TV_continuous a b (f : R -> R) : a < b -> {within `[a,b], continuous f} -> - bounded_variation a b f -> + BV a b f -> {within `[a,b], continuous (fine \o TV a ^~ f)}. Proof. -move=> ab /continuous_within_itvP [int [l r]] bdf. +move=> ab /continuous_within_itvP [int [l r]] bdf. apply/continuous_within_itvP; repeat split. -- move=> x /[dup] xab; rewrite in_itv /= => /andP [ax xb]. +- move=> x /[dup] xab; rewrite in_itv /= => /andP [ax xb]. apply/left_right_continuousP; split. apply: (TV_left_continuous _ (ltW xb)) => //. by have /left_right_continuousP [] := int x xab. @@ -2175,4 +2451,4 @@ apply/continuous_within_itvP; repeat split. - exact: (TV_left_continuous ab). Qed. -End bounded_variation. \ No newline at end of file +End variation_continuity. From 18378ee5bc84176e68f26b4c3cee14dad0c878cf Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 12 Jan 2024 13:39:09 -0500 Subject: [PATCH 12/22] filling in admits --- theories/normedtype.v | 48 +++++++++++++++++++++++++++++++++++++++++++ theories/realfun.v | 23 ++++----------------- 2 files changed, 52 insertions(+), 19 deletions(-) diff --git a/theories/normedtype.v b/theories/normedtype.v index 9fa6e6434..83238f791 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2914,6 +2914,54 @@ by apply: xe_A => //; rewrite eq_sym. Qed. Arguments cvg_at_leftE {R V} f x. +Lemma continuous_within_itvP {R : realType } a b (f : R -> R) : + a < b -> + {within `[a,b], continuous f} <-> + {in `]a,b[, continuous f} /\ f @ a^'+ --> f a /\ f @b^'- --> f b. +Proof. +move=> ab; split. +have [aab bab] : a \in `[a, b] /\ b \in `[a, b]. + by split; apply/andP; split => //; apply: ltW. +have [aabC babC] : `[a, b]%classic a /\ `[a, b]%classic b. + by rewrite ?inE /=; split. +move=> abf; split. + suff : {in `]a,b[%classic, continuous f}. + by move=> P ? W; by apply: P; move: W; rewrite inE /=. + rewrite -(@continuous_open_subspace); last exact: interval_open. + by move: abf; apply: continuous_subspaceW; apply: subset_itvW. + split; apply/cvgrPdist_lt => eps eps_gt0 /=; + [move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf a) + | move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf b)]; + rewrite /dnbhs /= ?near_withinE ?near_simpl /prop_near1/nbhs /=; + rewrite -nbhs_subspace_in // /within /= ?nbhs_simpl near_simpl; + apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac; + (apply => //; last by apply/eqP => CA; move: ac; rewrite CA ltxx); + apply/andP; split; apply: ltW => //; move: cba; rewrite /= ?[(`|a-c|)]distrC ger0_norm. + - by rewrite ltrBlDr -addrA [-_+_]addrC subrr addr0. + - by apply: ltW; rewrite subr_gt0. + - by rewrite ltrBlDr addrC addrA ltrBrDl -ltrBrDr -addrA subrr addr0. + - by apply: ltW; rewrite subr_gt0. +case=> ctsoo [ctsL ctsR]; apply/subspace_continuousP => x /andP []. +rewrite ?le_eqVlt => /orP + /orP; case => + []. +- by move=> /eqP [<-] /eqP [E]; move: ab; rewrite E ltxx. +- move=> /eqP [<-_]; apply/cvgrPdist_lt => eps eps_gt0 /=. + move/cvgrPdist_lt/(_ _ eps_gt0):ctsL; rewrite /at_right ?near_withinE. + apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac. + (have : a <= c by move: ac => /andP []); rewrite le_eqVlt => /orP []. + by move=> /eqP ->; rewrite subrr normr0. + by move=> ?; apply. +- move=> _ /eqP [->]; apply/cvgrPdist_lt => eps eps_gt0 /=. + move/cvgrPdist_lt/(_ _ eps_gt0):ctsR; rewrite /at_left ?near_withinE. + apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac. + (have : c <= b by move: ac => /andP []); rewrite le_eqVlt => /orP []. + by move=> /eqP ->; rewrite subrr normr0. + by move=> ?; apply. +- move=> ax xb; have aboox : x \in `]a,b[ by apply/andP; split. + rewrite within_interior; first exact: ctsoo. + suff : `]a,b[ `<=` interior `[a,b] by apply. + rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open]. +Qed. + (* TODO: generalize to R : numFieldType *) Section hausdorff. diff --git a/theories/realfun.v b/theories/realfun.v index 449d571ef..81cef9c16 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1210,6 +1210,7 @@ have : f a >= f b by rewrite (itvP xfafb). by case: ltrgtP xfafb => // ->. Qed. + Lemma segment_inc_surj_continuous a b f : {in `[a, b] &, {mono f : x y / x <= y}} -> set_surj `[a, b] `[f a, f b] f -> {within `[a, b], continuous f}. @@ -1520,12 +1521,7 @@ End is_derive_inverse. (eapply is_deriveV; first by []) : typeclass_instances. From mathcomp Require Import path. -Require Import sequences. -Notation "'nondecreasing_fun' f" := ({homo f : n m / (n <= m)%R >-> (n <= m)%R}) - (at level 10). -Notation "'nonincreasing_fun' f" := ({homo f : n m / (n <= m)%R >-> (n >= m)%R}) - (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)}. @@ -1553,11 +1549,6 @@ Proof. by move=> uS [y Sy] /le_trans; apply; apply: sup_ub. Qed. -(* NB: already in master? *) -Lemma ereal_sup_le {R : realType} (S : set (\bar R)) x : - (exists2 y, S y & x <= y)%E -> (x <= ereal_sup S)%E. -Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ub. Qed. - Lemma ereal_supy {R : realType} (A : set \bar R) : A +oo%E -> ereal_sup A = +oo%E. Proof. @@ -2389,7 +2380,7 @@ Lemma total_variation_opp a b f : TV a b f = TV (- b) (- a) (f \o -%R). Proof. by rewrite /total_variation variations_opp. Qed. Lemma TV_left_continuous a b x f : a < x -> x <= b -> - f @ at_left x --> f x -> + f @ x^'- --> f x -> BV a b f -> fine \o TV a ^~ f @ x^'- --> fine (TV a x f). Proof. @@ -2428,19 +2419,13 @@ apply: (TV_right_continuous _ _ _ bvNf). by apply/at_left_at_rightP; rewrite /= opprK. Unshelve. all: by end_near. Qed. -Lemma continuous_within_itvP a b (f : R -> R) : - {within `[a,b], continuous f} <-> - {in `]a,b[, continuous f} /\ f @ a^'+ --> f a /\ f @b^'- --> f b. -Proof. -Admitted. - Lemma TV_continuous a b (f : R -> R) : a < b -> {within `[a,b], continuous f} -> BV a b f -> {within `[a,b], continuous (fine \o TV a ^~ f)}. Proof. -move=> ab /continuous_within_itvP [int [l r]] bdf. -apply/continuous_within_itvP; repeat split. +move=> ab /(@continuous_within_itvP _ _ _ _ ab) [int [l r]] bdf. +apply/continuous_within_itvP; (repeat split) => //. - move=> x /[dup] xab; rewrite in_itv /= => /andP [ax xb]. apply/left_right_continuousP; split. apply: (TV_left_continuous _ (ltW xb)) => //. From abb83f8eb6a2251def8ff20e5e664f235449ef6b Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 12 Jan 2024 14:01:41 -0500 Subject: [PATCH 13/22] moving lemmas around --- theories/realfun.v | 29 ++++++++++++++--------------- 1 file changed, 14 insertions(+), 15 deletions(-) diff --git a/theories/realfun.v b/theories/realfun.v index 81cef9c16..6f475e046 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -87,6 +87,20 @@ apply: near_eq_cvg; near do rewrite subrK; exists M. by rewrite num_real. Unshelve. all: by end_near. Qed. +Lemma left_right_continuousP + {T: topologicalType} (f : R -> T) x : + (f @ x^'- --> f x /\ f @ x^'+ --> f x) <-> f @ x --> f x. +Proof. +split; first last. + by move=> cts; split; exact: cvg_within_filter. +case => + + U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl. +rewrite ?near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf. +near=> t => xlt xgt; have := @real_leVge R x t; rewrite ?num_real. +move=> /(_ isT isT) /orP; rewrite ?le_eqVlt; case => /orP; case => //. + by move/eqP <-; apply: nbhs_singleton. +by move/eqP ->; apply: nbhs_singleton. +Unshelve. all: by end_near. Qed. + Lemma cvg_at_right_left_dnbhs (f : R -> R) (p : R) (l : R) : f x @[x --> p^'+] --> l -> f x @[x --> p^'-] --> l -> f x @[x --> p^'] --> l. @@ -105,7 +119,6 @@ rewrite neq_lt => /orP[tp|pt]. move=> z/= + _ => /lt_le_trans; apply. by rewrite ler_pdivr_mulr// ler_pmulr// ler1n. Unshelve. all: by end_near. Qed. - End fun_cvg_realFieldType. Section cvgr_fun_cvg_seq. @@ -2215,20 +2228,6 @@ move=> t /= xtr tx; rewrite -[t]opprK; apply: xb. by rewrite ltr_oppl. Qed. -Lemma left_right_continuousP - {T: topologicalType} {R : realType} (f : R -> T) x : - (f @ x^'- --> f x /\ f @ x^'+ --> f x) <-> f @ x --> f x. -Proof. -split; first last. - by move=> cts; split; exact: cvg_within_filter. -case => + + U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl. -rewrite ?near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf. -near=> t => xlt xgt; have := @real_leVge R x t; rewrite ?num_real. -move=> /(_ isT isT) /orP; rewrite ?le_eqVlt; case => /orP; case => //. - by move/eqP <-; apply: nbhs_singleton. -by move/eqP ->; apply: nbhs_singleton. -Unshelve. all: by end_near. Qed. - Section variation_continuity. Context {R : realType}. Implicit Type f : R -> R. From 0f8feba42cd37a485405cb187ac56f48c1b81926 Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 12 Jan 2024 14:15:01 -0500 Subject: [PATCH 14/22] removing duplicate lemmas --- theories/realfun.v | 21 ++------------------- 1 file changed, 2 insertions(+), 19 deletions(-) diff --git a/theories/realfun.v b/theories/realfun.v index 6f475e046..d3d958e9c 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -2211,23 +2211,6 @@ Qed. End total_variation. -Lemma at_left_at_rightP - {T : topologicalType} {R : realType} (f : R -> T) x (z : T) : - f @ x^'- --> z <-> f \o -%R @ (- x)^'+ --> z. -Proof. -suff -> : (- x)^'+ = (-%R) @ x^'-. - by rewrite -?fmap_comp; under [_ \o _]eq_fun => ? do rewrite /= opprK. -rewrite eqEsubset /=; split. - move=> E /= [r rpos xb]; exists r => //. - move=> t /= xtr tx; apply: xb. - by rewrite /= -opprB opprK normrN addrC. - by rewrite ltr_oppr opprK. -move=> E /= [r rpos xb]; exists r => //. -move=> t /= xtr tx; rewrite -[t]opprK; apply: xb. - by rewrite /= opprK -normrN opprD. -by rewrite ltr_oppl. -Qed. - Section variation_continuity. Context {R : realType}. Implicit Type f : R -> R. @@ -2384,7 +2367,7 @@ Lemma TV_left_continuous a b x f : a < x -> x <= b -> fine \o TV a ^~ f @ x^'- --> fine (TV a x f). Proof. move=> ax xb fNcts bvf. -apply/at_left_at_rightP; rewrite total_variation_opp. +apply/cvg_at_leftNP; rewrite total_variation_opp. have bvNf : BV (-b) (-a) (f \o -%R). by case: bvf => M; rewrite -variations_opp => ?; exists M. have bx : - b <= - x by rewrite ler_oppl opprK. @@ -2415,7 +2398,7 @@ apply: cvgB; first exact: cvg_cst. apply: (TV_right_continuous _ _ _ bvNf). - by rewrite ler_oppl opprK //. - by rewrite ltr_oppl opprK //. -by apply/at_left_at_rightP; rewrite /= opprK. +by apply/cvg_at_leftNP; rewrite /= opprK. Unshelve. all: by end_near. Qed. Lemma TV_continuous a b (f : R -> R) : a < b -> From 2bf383fda8fa88df8a34907aecddf492295c5d81 Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 12 Jan 2024 14:25:30 -0500 Subject: [PATCH 15/22] docs and changelog --- CHANGELOG_UNRELEASED.md | 32 ++++++++++++++++++++++++++++++++ theories/realfun.v | 10 ++++++++++ 2 files changed, 42 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 6d418d4f8..08e2b062b 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -59,6 +59,38 @@ + lemma `continuous_uncurry` + lemma `curry_continuous` + lemma `uncurry_continuous` +- in file `normedtype.v`, + + new lemma `continuous_within_itvP`. + +- in file `realfun.v`, + + new definitions `itv_partition`, `itv_partitionL`, `itv_partitionR`, + `variation`, `variations`, `bounded_variation`, `total_variation`, + `neg_tv`, and `pos_tv`. + + + new lemmas `left_right_continuousP`, `nondecreasing_funN`, + `nonincreasing_funN`, `has_ubound_ereal_sup`, `sup_le`, `ereal_supy`, + `path_lt_filter0`, `path_lt_filterT`, `last_filter_lt`, `last_filter`, + `path_inv`, `path_lt_le_last`, `itv_partition_nil`, `itv_partition1`, + `itv_partition_cons`, `itv_partitionxx`, `itv_partition_le`, + `itv_partition_tail`, `itv_partition_cat`, `itv_partition_nth_size`, + `itv_partition_nth_ge`, `itv_partition_nth_le`, + `nondecreasing_fun_itv_partition`, `nonincreasing_fun_itv_partition`, + `itv_partitionLP`, `itv_partitionRP`, `in_itv_partition`, + `notin_itv_partition`, `itv_partition_rev`, `variationE`, `variation_nil`, + `variation_ge0`, `variationN`, `variation_le`, `nondecreasing_variation`, + `nonincreasing_variation`, `variationD`, `variation_itv_partitionLR`, + `le_variation`, `variation_opp_rev`, `variation_rev_opp`, + `variations_variation`, `variations_neq0`, `variationsN`, `variationsxx`, + `bounded_variationxx`, `bounded_variationD`, `bounded_variationN`, + `bounded_variationl`, `bounded_variationr`, `variations_opp`, + `nondecreasing_bounded_variation`, `total_variationxx`, + `total_variation_ge`, `total_variation_ge0`, + `nondecreasing_total_variation`, `bounded_variationP`, `total_variationN`, + `total_variation_le`, `total_variationD`, `neg_TV_increasing`, + `total_variation_jordan_decompE`, `neg_TV_increasing_fin`, + `neg_TV_bounded_variation`, `TV_right_continuous`, + `neg_TV_right_continuous`, `total_variation_opp`, `TV_left_continuous`, and + `TV_continuous`. ### Changed diff --git a/theories/realfun.v b/theories/realfun.v index d3d958e9c..e58fc9b40 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -24,6 +24,16 @@ From HB Require Import structures. (* *) (* derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and *) (* continuous up to the boundary *) +(* 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 variation 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 *) +(* *) (* ``` *) (* *) (******************************************************************************) From c2742fe5e5fcb1bf9be1515f1f2e5ddd279f66ad Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 13 Jan 2024 20:06:40 +0900 Subject: [PATCH 16/22] minor checks (wip) --- CHANGELOG_UNRELEASED.md | 46 ++++---- theories/ereal.v | 5 + theories/normedtype.v | 77 +++++++------- theories/realfun.v | 225 +++++++++++++++++++--------------------- 4 files changed, 174 insertions(+), 179 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 08e2b062b..d92cab284 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -62,35 +62,45 @@ - in file `normedtype.v`, + new lemma `continuous_within_itvP`. +- in `ereal.v`: + + lemma `ereal_supy` + - in file `realfun.v`, + new definitions `itv_partition`, `itv_partitionL`, `itv_partitionR`, `variation`, `variations`, `bounded_variation`, `total_variation`, `neg_tv`, and `pos_tv`. - + new lemmas `left_right_continuousP`, `nondecreasing_funN`, - `nonincreasing_funN`, `has_ubound_ereal_sup`, `sup_le`, `ereal_supy`, - `path_lt_filter0`, `path_lt_filterT`, `last_filter_lt`, `last_filter`, - `path_inv`, `path_lt_le_last`, `itv_partition_nil`, `itv_partition1`, - `itv_partition_cons`, `itv_partitionxx`, `itv_partition_le`, - `itv_partition_tail`, `itv_partition_cat`, `itv_partition_nth_size`, + + new lemmas `left_right_continuousP`, + `nondecreasing_funN`, `nonincreasing_funN`, `last_filterP`, + `path_lt_filter0`, `path_lt_filterT`, `path_lt_head`, `path_lt_last_filter`, + `path_lt_le_last` + + + new 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`, `nonincreasing_fun_itv_partition`, `itv_partitionLP`, `itv_partitionRP`, `in_itv_partition`, - `notin_itv_partition`, `itv_partition_rev`, `variationE`, `variation_nil`, + `notin_itv_partition`, `itv_partition_rev`, + + + new lemmas `variationE`, `variation_nil`, `variation_ge0`, `variationN`, `variation_le`, `nondecreasing_variation`, `nonincreasing_variation`, `variationD`, `variation_itv_partitionLR`, - `le_variation`, `variation_opp_rev`, `variation_rev_opp`, - `variations_variation`, `variations_neq0`, `variationsN`, `variationsxx`, - `bounded_variationxx`, `bounded_variationD`, `bounded_variationN`, + `le_variation`, `variation_opp_rev`, `variation_rev_opp` + + + new lemmas `variations_variation`, `variations_neq0`, `variationsN`, `variationsxx` + + + new lemmas `bounded_variationxx`, `bounded_variationD`, `bounded_variationN`, `bounded_variationl`, `bounded_variationr`, `variations_opp`, - `nondecreasing_bounded_variation`, `total_variationxx`, - `total_variation_ge`, `total_variation_ge0`, - `nondecreasing_total_variation`, `bounded_variationP`, `total_variationN`, - `total_variation_le`, `total_variationD`, `neg_TV_increasing`, - `total_variation_jordan_decompE`, `neg_TV_increasing_fin`, - `neg_TV_bounded_variation`, `TV_right_continuous`, - `neg_TV_right_continuous`, `total_variation_opp`, `TV_left_continuous`, and - `TV_continuous`. + `nondecreasing_bounded_variation` + + + new lemmas `total_variationxx`, `total_variation_ge`, `total_variation_ge0`, + `bounded_variationP`, `nondecreasing_total_variation`, `total_variationN`, + `total_variation_le`, `total_variationD`, `neg_tv_nondecreasing`, + `total_variation_jordan_decompE`, `fine_neg_tv_nondecreasing`, + `neg_tv_bounded_variation`, `total_variation_right_continuous`, + `neg_tv_right_continuous`, `total_variation_opp`, `total_variation_left_continuous`, + `total_variation_continuous` ### Changed diff --git a/theories/ereal.v b/theories/ereal.v index 9a0bcd033..198cb31ae 100644 --- a/theories/ereal.v +++ b/theories/ereal.v @@ -511,6 +511,11 @@ case: xgetP => /=; first by move=> _ -> -[] /ubP geS _; apply geS. by case: (ereal_supremums_neq0 S) => /= x0 Sx0; move/(_ x0). Qed. +Lemma ereal_supy S : S +oo -> ereal_sup S = +oo. +Proof. +by move=> Soo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ub. +Qed. + Lemma ereal_sup_le S x : (exists2 y, S y & x <= y) -> x <= ereal_sup S. Proof. by move=> [y Sy] /le_trans; apply; exact: ereal_sup_ub. Qed. diff --git a/theories/normedtype.v b/theories/normedtype.v index 83238f791..4ec620e77 100644 --- a/theories/normedtype.v +++ b/theories/normedtype.v @@ -2919,47 +2919,44 @@ Lemma continuous_within_itvP {R : realType } a b (f : R -> R) : {within `[a,b], continuous f} <-> {in `]a,b[, continuous f} /\ f @ a^'+ --> f a /\ f @b^'- --> f b. Proof. -move=> ab; split. -have [aab bab] : a \in `[a, b] /\ b \in `[a, b]. - by split; apply/andP; split => //; apply: ltW. -have [aabC babC] : `[a, b]%classic a /\ `[a, b]%classic b. - by rewrite ?inE /=; split. -move=> abf; split. - suff : {in `]a,b[%classic, continuous f}. - by move=> P ? W; by apply: P; move: W; rewrite inE /=. - rewrite -(@continuous_open_subspace); last exact: interval_open. - by move: abf; apply: continuous_subspaceW; apply: subset_itvW. - split; apply/cvgrPdist_lt => eps eps_gt0 /=; - [move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf a) - | move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf b)]; - rewrite /dnbhs /= ?near_withinE ?near_simpl /prop_near1/nbhs /=; - rewrite -nbhs_subspace_in // /within /= ?nbhs_simpl near_simpl; - apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac; - (apply => //; last by apply/eqP => CA; move: ac; rewrite CA ltxx); - apply/andP; split; apply: ltW => //; move: cba; rewrite /= ?[(`|a-c|)]distrC ger0_norm. - - by rewrite ltrBlDr -addrA [-_+_]addrC subrr addr0. - - by apply: ltW; rewrite subr_gt0. - - by rewrite ltrBlDr addrC addrA ltrBrDl -ltrBrDr -addrA subrr addr0. - - by apply: ltW; rewrite subr_gt0. -case=> ctsoo [ctsL ctsR]; apply/subspace_continuousP => x /andP []. -rewrite ?le_eqVlt => /orP + /orP; case => + []. -- by move=> /eqP [<-] /eqP [E]; move: ab; rewrite E ltxx. -- move=> /eqP [<-_]; apply/cvgrPdist_lt => eps eps_gt0 /=. - move/cvgrPdist_lt/(_ _ eps_gt0):ctsL; rewrite /at_right ?near_withinE. - apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac. - (have : a <= c by move: ac => /andP []); rewrite le_eqVlt => /orP []. - by move=> /eqP ->; rewrite subrr normr0. - by move=> ?; apply. -- move=> _ /eqP [->]; apply/cvgrPdist_lt => eps eps_gt0 /=. - move/cvgrPdist_lt/(_ _ eps_gt0):ctsR; rewrite /at_left ?near_withinE. - apply: filter_app; exists (b-a); rewrite /= ?subr_gt0 // => c cba + ac. - (have : c <= b by move: ac => /andP []); rewrite le_eqVlt => /orP []. - by move=> /eqP ->; rewrite subrr normr0. - by move=> ?; apply. -- move=> ax xb; have aboox : x \in `]a,b[ by apply/andP; split. +move=> ab; split=> [abf|]. + split. + suff : {in `]a, b[%classic, continuous f}. + by move=> P c W; apply: P; rewrite inE. + rewrite -continuous_open_subspace; last exact: interval_open. + by move: abf; exact/continuous_subspaceW/subset_itvW. + have [aab bab] : a \in `[a, b] /\ b \in `[a, b]. + by rewrite !in_itv/= !lexx (ltW ab). + split; apply/cvgrPdist_lt => eps eps_gt0 /=. + + move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf a). + rewrite /dnbhs/= near_withinE !near_simpl// /prop_near1 /nbhs/=. + rewrite -nbhs_subspace_in// /within/= near_simpl. + apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac. + apply=> //; rewrite ?gt_eqF// !in_itv/= (ltW ac)/=; move: cba => /=. + by rewrite ltr0_norm ?subr_lt0// opprB ltr_add2r => /ltW. + + move/continuous_withinNx/cvgrPdist_lt/(_ _ eps_gt0) : (abf b). + rewrite /dnbhs/= near_withinE !near_simpl /prop_near1 /nbhs/=. + rewrite -nbhs_subspace_in// /within/= near_simpl. + apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac. + apply=> //; rewrite ?lt_eqF// !in_itv/= (ltW ac)/= andbT; move: cba => /=. + by rewrite gtr0_norm ?subr_gt0// ltr_add2l ltr_oppr opprK => /ltW. +case=> ctsoo [ctsL ctsR]; apply/subspace_continuousP => x /andP[]. +rewrite !bnd_simp/= !le_eqVlt => /predU1P[<-{x}|ax] /predU1P[|]. +- by move/eqP; rewrite lt_eqF. +- move=> _; apply/cvgrPdist_lt => eps eps_gt0 /=. + move/cvgrPdist_lt/(_ _ eps_gt0): ctsL; rewrite /at_right !near_withinE. + apply: filter_app; exists (b - a); rewrite /= ?subr_gt0// => c cba + ac. + have : a <= c by move: ac => /andP[]. + by rewrite le_eqVlt => /predU1P[->|/[swap] /[apply]//]; rewrite subrr normr0. +- move=> ->; apply/cvgrPdist_lt => eps eps_gt0 /=. + move/cvgrPdist_lt/(_ _ eps_gt0): ctsR; rewrite /at_left !near_withinE. + apply: filter_app; exists (b - a); rewrite /= ?subr_gt0 // => c cba + ac. + have : c <= b by move: ac => /andP[]. + by rewrite le_eqVlt => /predU1P[->|/[swap] /[apply]//]; rewrite subrr normr0. +- move=> xb; have aboox : x \in `]a, b[ by rewrite !in_itv/= ax. rewrite within_interior; first exact: ctsoo. - suff : `]a,b[ `<=` interior `[a,b] by apply. - rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open]. + suff : `]a, b[ `<=` interior `[a, b] by exact. + by rewrite -open_subsetE; [exact: subset_itvW| exact: interval_open]. Qed. (* TODO: generalize to R : numFieldType *) diff --git a/theories/realfun.v b/theories/realfun.v index e58fc9b40..32132f6fa 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -14,28 +14,32 @@ From HB Require Import structures. (* numbers (e.g., the continuity of the inverse of a continuous function). *) (* *) (* ``` *) -(* 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 *) +(* 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 *) (* *) -(* lime_sup f a/lime_inf f a == limit sup/inferior of the extended *) -(* real-valued function f at point a *) +(* derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and *) +(* continuous up to the boundary *) (* *) -(* derivable_oo_continuous_bnd f x y == f is derivable on `]x, y[ and *) -(* continuous up to the boundary *) -(* 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 variation 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 *) +(* 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 *) (* *) (* ``` *) (* *) +(* * Limit superior and inferior for functions: *) +(* ``` *) +(* lime_sup f a/lime_inf f a == limit sup/inferior of the extended real- *) +(* valued function f at point a *) +(* ``` *) +(* *) (******************************************************************************) Set Implicit Arguments. @@ -59,6 +63,23 @@ Notation "'increasing_fun' f" := ({mono f : n m / (n <= m)%O >-> (n <= m)%O}) 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 ler_oppr opprK h. +by rewrite -(opprK (f n)) -ler_oppr 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. @@ -97,18 +118,16 @@ apply: near_eq_cvg; near do rewrite subrK; exists M. by rewrite num_real. Unshelve. all: by end_near. Qed. -Lemma left_right_continuousP - {T: topologicalType} (f : R -> T) x : - (f @ x^'- --> f x /\ f @ x^'+ --> f x) <-> f @ x --> f x. -Proof. -split; first last. - by move=> cts; split; exact: cvg_within_filter. -case => + + U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl. -rewrite ?near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf. -near=> t => xlt xgt; have := @real_leVge R x t; rewrite ?num_real. -move=> /(_ isT isT) /orP; rewrite ?le_eqVlt; case => /orP; case => //. - by move/eqP <-; apply: nbhs_singleton. -by move/eqP ->; apply: nbhs_singleton. +Lemma left_right_continuousP {T : topologicalType} (f : R -> T) x : + f @ x^'- --> f x /\ f @ x^'+ --> f x <-> f @ x --> f x. +Proof. +split; last by move=> cts; split; exact: cvg_within_filter. +move=> [+ +] U /= Uz => /(_ U Uz) + /(_ U Uz); near_simpl. +rewrite !near_withinE => lf rf; apply: filter_app lf; apply: filter_app rf. +near=> t => xlt xgt; have := @real_leVge R x t; rewrite !num_real. +move=> /(_ isT isT) /orP; rewrite !le_eqVlt => -[|] /predU1P[|//]. +- by move=> <-; exact: nbhs_singleton. +- by move=> ->; exact: nbhs_singleton. Unshelve. all: by end_near. Qed. Lemma cvg_at_right_left_dnbhs (f : R -> R) (p : R) (l : R) : @@ -1543,40 +1562,13 @@ End is_derive_inverse. #[global] Hint Extern 0 (is_derive _ _ (fun _ => (_ _)^-1) _) => (eapply is_deriveV; first by []) : typeclass_instances. -From mathcomp Require Import path. - - -Lemma nondecreasing_funN {R : realType} a b (f : R -> R) : - {in `[a, b] &, nondecreasing_fun f} <-> {in `[a, b] &, nonincreasing_fun (\- f)}. +Lemma last_filterP d {T : porderType d} (h : T) (P : pred T) t : + P h -> P (last h [seq x <- t | P x]). Proof. -split=> [h m n mab nab mn|h m n mab nab mn]; first by rewrite ler_oppr opprK h. -by rewrite -(opprK (f n)) -ler_oppr 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; rewrite [in X in _ <-> X](_ : f = (\- (\- f))); last first. - by apply/funext => x /=; rewrite opprK. -exact: nondecreasing_funN. -Qed. - -Lemma has_ubound_ereal_sup {R : realType} T (A : set T) (f : T -> R) : - [set f x | x in A] !=set0 -> - has_ubound [set f x | x in A] -> (ereal_sup [set (f x)%:E | x in A] < +oo)%E. -Proof. by move=> A0 ubA; rewrite -image_comp ereal_sup_EFin// ltry. Qed. - -Lemma sup_le {R : realType} (S : set R) x : has_ubound S -> - (exists2 y, S y & x <= y) -> x <= sup S. -Proof. -by move=> uS [y Sy] /le_trans; apply; apply: sup_ub. -Qed. - -Lemma ereal_supy {R : realType} (A : set \bar R) : - A +oo%E -> ereal_sup A = +oo%E. -Proof. -by move=> Aoo; apply/eqP; rewrite eq_le leey/=; exact: ereal_sup_ub. +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] = [::]. @@ -1593,14 +1585,13 @@ move=> /lt_path_min/allP sh; rewrite -[RHS](filter_predT s). by apply: eq_in_filter => x xs; exact: sh. Qed. -Lemma last_filter_lt d {T : porderType d} (h c : T) t : - (h < c)%O -> (last h [seq x <- t | x < c] < c)%O. +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. -elim: t h => //= t1 t2 ih h hc. -by case: ifPn => //= t1c; exact: ih. +by elim: s b => // h t ih b /= ab /andP[bh ->]; rewrite andbT (lt_trans ab). Qed. -Lemma last_filter d {T : porderType d} (a b c : T) (l : seq T) : +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. @@ -1613,12 +1604,6 @@ rewrite last_rcons => htb. by rewrite filter_rcons htb cb last_rcons. Qed. -Lemma path_inv 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_le_last d {T : porderType d} (i : T) (s : seq T) : path <%O i s -> (i <= last i s)%O. Proof. @@ -1632,16 +1617,21 @@ Section interval_partition. Context {R : realType}. Implicit Type (a b : R) (s : seq R). -(* a :: s is a of the interval [a, b] *) +(** 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_cons a b s : (size s > 0)%N -> itv_partition a b s -> a < b. +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 <-]. @@ -1659,14 +1649,10 @@ 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_cons - /(_ _)/ltW]. +case: s => [/itv_partition_nil ->//|h t /itv_partition_size_neq0 - /(_ _)/ltW]. exact. Qed. -Lemma itv_partition_tail a b x s : - itv_partition a b (x :: s) -> itv_partition x b s. -Proof. by rewrite /itv_partition/= => -[/andP[]]. 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. @@ -1677,7 +1663,7 @@ 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_tail/ih]. +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 -> @@ -1692,7 +1678,7 @@ 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_tail H. +by move=> [//|a h t /= nt] H; rewrite ih//; exact: itv_partition_cons H. Qed. Lemma nondecreasing_fun_itv_partition a b f s : @@ -1726,7 +1712,7 @@ move/nonincreasing_funN => ndNf abs F k ks; rewrite -(opprK (F k)) ler_oppr. exact: (nondecreasing_fun_itv_partition ndNf abs). Qed. -(* given a partition of [a,b] and c, returns a partition of [a,c] *) +(** 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 -> @@ -1735,11 +1721,11 @@ 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_filter_lt. + 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] *) +(** 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 -> @@ -1749,7 +1735,7 @@ 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/(last_filter ac). +exact/eqP/(path_lt_last_filter ac). Qed. Lemma in_itv_partition c s : sorted <%R s -> c \in s -> @@ -1773,8 +1759,8 @@ 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_inv ht. - by rewrite path_lt_filterT//; exact: path_inv ht. + 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. @@ -2087,6 +2073,17 @@ Qed. Lemma total_variation_ge0 a b f : a <= b -> (0 <= TV a b f)%E. Proof. by move=> ab; rewrite (le_trans _ (total_variation_ge _ ab)). Qed. +Lemma bounded_variationP a b f : a <= b -> BV a b f <-> TV a b f \is a fin_num. +Proof. +rewrite le_eqVlt => /predU1P[<-{b}|ab]. + by rewrite total_variationxx; split => // ?; exact: bounded_variationxx. +rewrite ge0_fin_numE; last exact/total_variation_ge0/ltW. +split=> [abf|]. + by rewrite /total_variation ereal_sup_EFin ?ltry//; exact: variations_neq0. +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. @@ -2101,18 +2098,6 @@ exists (variation a b f [:: b]) => //. by rewrite nondecreasing_variation//; exact: itv_partition1. Qed. -Lemma bounded_variationP a b f : a <= b -> BV a b f <-> TV a b f \is a fin_num. -Proof. -rewrite le_eqVlt => /predU1P[<-{b}|ab]. - by rewrite total_variationxx; split => // ?; exact: bounded_variationxx. -rewrite ge0_fin_numE; last exact/total_variation_ge0/ltW. -split=> [abf|]. - apply: has_ubound_ereal_sup => //; rewrite image_id//. - exact: variations_neq0. -rewrite /total_variation /bounded_variation ltey => /eqP; apply: contra_notP. -by move/hasNub_ereal_sup; apply; exact: variations_neq0. -Qed. - Lemma total_variationN a b f : TV a b (\- f) = TV a b f. Proof. by rewrite /TV; rewrite variationsN. Qed. @@ -2232,8 +2217,8 @@ Definition neg_tv a f (x : R) : \bar R := ((TV a x f - (f x)%:E) * 2^-1%:E)%E. Definition pos_tv a f (x : R) : \bar R := neg_tv a (\- f) x. -Lemma neg_TV_increasing a b f : - {in `[a, b] &, {homo (neg_tv a f) : x y / x <= y >-> (x <= y)%E}}. +Lemma neg_tv_nondecreasing a b f : + {in `[a, b] &, nondecreasing_fun (neg_tv a f)}. Proof. move=> x y xab yab xy; have ax : a <= x. by move: xab; rewrite in_itv //= => /andP []. @@ -2262,8 +2247,8 @@ rewrite addeAC oppeD //= ?fin_num_adde_defl //. by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -Num.Theory.splitr. Qed. -Lemma neg_TV_increasing_fin a b f : BV a b f -> - {in `[a,b] &, {homo (fine \o neg_tv a f) : x y / x <= y}}. +Lemma fine_neg_tv_nondecreasing a b f : BV a b f -> + {in `[a, b] &, nondecreasing_fun (fine \o neg_tv a f)}. Proof. move=> bdv p q pab qab pq /=. move: (pab) (qab); rewrite ?in_itv /= => /andP[ap pb] /andP[aq qb]. @@ -2272,20 +2257,19 @@ apply: fine_le; rewrite /neg_tv ?fin_numM // ?fin_numB /=. exact: (bounded_variationl _ pb). - apply/andP; split => //; apply/bounded_variationP => //. exact: (bounded_variationl _ qb). -exact: (neg_TV_increasing _ pab). +exact: (neg_tv_nondecreasing _ pab). Qed. -Lemma neg_TV_bounded_variation a b f : BV a b f -> - BV a b (fine \o neg_tv a f). +Lemma neg_tv_bounded_variation a b f : BV a b f -> BV a b (fine \o neg_tv a f). Proof. move=> ?; apply: nondecreasing_bounded_variation. -exact: neg_TV_increasing_fin. +exact: fine_neg_tv_nondecreasing. Qed. -Lemma TV_right_continuous a b x f : a <= x -> x < b -> - f @ at_right x --> f x -> +Lemma total_variation_right_continuous a b x f : a <= x -> x < b -> + f @ x^'+ --> f x -> BV a b f -> - fine \o TV a ^~ f @ at_right x --> fine (TV a x f). + fine \o TV a ^~ f @ x^'+ --> fine (TV a x f). Proof. move=> ax xb ctsf bvf; have ? : a <= b by apply:ltW; apply: (le_lt_trans ax). apply/cvgrPdist_lt=> _/posnumP[eps]. @@ -2336,13 +2320,12 @@ rewrite -addeA. apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E). rewrite [in leRHS]variationE; last exact: itv_partition1. rewrite gee_addl // sube_le0; apply: ereal_sup_ub => /=. - exists (variation t b f (i :: j)) => //. - apply: variations_variation. + exists (variation t b f (i :: j)) => //; apply: variations_variation. by rewrite /itv_partition/= ijb ij ti. by rewrite /variation/= big_nat_recr//= big_nil add0r distrC lte_fin. Unshelve. all: by end_near. Qed. -Lemma neg_TV_right_continuous a x b f : a <= x -> x < b -> +Lemma neg_tv_right_continuous a x b f : a <= x -> x < b -> BV a b f -> f @ x^'+ --> f x -> fine \o neg_tv a f @ x^'+ --> fine (neg_tv a f x). @@ -2362,7 +2345,7 @@ rewrite fineD // EFinB; apply: cvgeB => //. apply: bounded_variationl bvf => //. move: xtbx; rewrite distrC ger0_norm ?subr_ge0; last by exact: ltW. by rewrite ltr_subr_addr -addrA [-_ + _]addrC subrr addr0 => /ltW. - by apply: TV_right_continuous => //; last exact: bvf. + by apply: total_variation_right_continuous => //; last exact: bvf. apply: cvg_comp; first exact: fcts. apply/ fine_cvgP; split; first by near=> t => //. by have -> : fine \o EFin = id by move=> ?; rewrite funeqE => ? /=. @@ -2371,7 +2354,7 @@ Unshelve. all: by end_near. Qed. Lemma total_variation_opp a b f : TV a b f = TV (- b) (- a) (f \o -%R). Proof. by rewrite /total_variation variations_opp. Qed. -Lemma TV_left_continuous a b x f : a < x -> x <= b -> +Lemma total_variation_left_continuous a b x f : a < x -> x <= b -> f @ x^'- --> f x -> BV a b f -> fine \o TV a ^~ f @ x^'- --> fine (TV a x f). @@ -2405,13 +2388,13 @@ have /near_eq_cvg/cvg_trans : {near (- x)^'+, by rewrite -total_variationD. apply. apply: cvgB; first exact: cvg_cst. -apply: (TV_right_continuous _ _ _ bvNf). +apply: (total_variation_right_continuous _ _ _ bvNf). - by rewrite ler_oppl opprK //. - by rewrite ltr_oppl opprK //. by apply/cvg_at_leftNP; rewrite /= opprK. Unshelve. all: by end_near. Qed. -Lemma TV_continuous a b (f : R -> R) : a < b -> +Lemma total_variation_continuous a b (f : R -> R) : a < b -> {within `[a,b], continuous f} -> BV a b f -> {within `[a,b], continuous (fine \o TV a ^~ f)}. @@ -2420,12 +2403,12 @@ move=> ab /(@continuous_within_itvP _ _ _ _ ab) [int [l r]] bdf. apply/continuous_within_itvP; (repeat split) => //. - move=> x /[dup] xab; rewrite in_itv /= => /andP [ax xb]. apply/left_right_continuousP; split. - apply: (TV_left_continuous _ (ltW xb)) => //. + apply: (total_variation_left_continuous _ (ltW xb)) => //. by have /left_right_continuousP [] := int x xab. - apply: (TV_right_continuous _ xb) => //; first exact: ltW. + apply: (total_variation_right_continuous _ xb) => //; first exact: ltW. by have /left_right_continuousP [] := int x xab. -- exact: (TV_right_continuous _ ab). -- exact: (TV_left_continuous ab). +- exact: (total_variation_right_continuous _ ab). +- exact: (total_variation_left_continuous ab). Qed. End variation_continuity. From dabe6ef104ce169bdb8eb5665bf3a92b8563ffb9 Mon Sep 17 00:00:00 2001 From: zstone Date: Sat, 13 Jan 2024 11:07:44 -0500 Subject: [PATCH 17/22] adding monotone variation --- CHANGELOG_UNRELEASED.md | 18 +++++++++++++++--- theories/realfun.v | 26 ++++++++++++++++++++++++++ 2 files changed, 41 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d92cab284..953e1d8ad 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -96,11 +96,23 @@ + new lemmas `total_variationxx`, `total_variation_ge`, `total_variation_ge0`, `bounded_variationP`, `nondecreasing_total_variation`, `total_variationN`, - `total_variation_le`, `total_variationD`, `neg_tv_nondecreasing`, + `total_variation_le`, `total_variationD`, `neg_tv_nondecreasing`, `total_variation_jordan_decompE`, `fine_neg_tv_nondecreasing`, `neg_tv_bounded_variation`, `total_variation_right_continuous`, - `neg_tv_right_continuous`, `total_variation_opp`, `total_variation_left_continuous`, - `total_variation_continuous` + `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`, + `variationsN`, `variationsxx`, `bounded_variationxx`, `bounded_variationD`, + `bounded_variationN`, `bounded_variationl`, `bounded_variationr`, + `variations_opp`, `nondecreasing_bounded_variation`, `total_variationxx`, + `total_variation_ge`, `total_variation_ge0`, + `nondecreasing_total_variation`, `bounded_variationP`, `total_variationN`, + `total_variation_le`, `total_variationD`, `neg_TV_increasing`, + `total_variation_jordan_decompE`, `neg_TV_increasing_fin`, + `neg_TV_bounded_variation`, `TV_right_continuous`, + `neg_TV_right_continuous`, `total_variation_opp`, `TV_left_continuous`, and + `TV_continuous`. ### Changed diff --git a/theories/realfun.v b/theories/realfun.v index 32132f6fa..76a8f2a4a 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1952,6 +1952,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) : + 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. +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/andP; split => //; apply: (lt_trans wa). +rewrite variationD => //; last exact: itv_partition1. +apply: le_variation. +Qed. + End variation. Section bounded_variation. From adf2461a9b7d7113a29f722c30e259a31a2d8000 Mon Sep 17 00:00:00 2001 From: zstone Date: Sat, 13 Jan 2024 12:23:47 -0500 Subject: [PATCH 18/22] fixing names --- CHANGELOG_UNRELEASED.md | 2 +- theories/realfun.v | 21 ++++++++++----------- 2 files changed, 11 insertions(+), 12 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 953e1d8ad..04fcb2cb6 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -97,7 +97,7 @@ + new lemmas `total_variationxx`, `total_variation_ge`, `total_variation_ge0`, `bounded_variationP`, `nondecreasing_total_variation`, `total_variationN`, `total_variation_le`, `total_variationD`, `neg_tv_nondecreasing`, - `total_variation_jordan_decompE`, `fine_neg_tv_nondecreasing`, + `total_variation_pos_neg_tvE`, `fine_neg_tv_nondecreasing`, `neg_tv_bounded_variation`, `total_variation_right_continuous`, `neg_tv_right_continuous`, `total_variation_opp`, `total_variation_left_continuous`, `total_variation_continuous`, diff --git a/theories/realfun.v b/theories/realfun.v index 76a8f2a4a..fe8157c2e 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1973,11 +1973,10 @@ 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/andP; split => //; apply: (lt_trans wa). -rewrite variationD => //; last exact: itv_partition1. -apply: le_variation. + by split => //; apply/ (path_lt_head wa)/andP; split => //. +by rewrite variationD => //; [exact: le_variation | exact: itv_partition1]. Qed. - + End variation. Section bounded_variation. @@ -2254,8 +2253,8 @@ apply: lee_add => //; apply: le_trans; last exact: total_variation_ge. by rewrite lee_fin ler_norm. Qed. -Lemma total_variation_jordan_decompE a b f : BV a b f -> - {in `[a, b], f =1 (fine \o neg_tv a (\- f)) \- (fine \o neg_tv a f)}. +Lemma bounded_variation_pos_neg_tvE a b f : BV a b f -> + {in `[a, b], f =1 (fine \o pos_tv a f) \- (fine \o neg_tv a f)}. Proof. move=> bdabf x; rewrite in_itv /= => /andP [ax xb]. have ffin: TV a x f \is a fin_num. @@ -2264,13 +2263,13 @@ have ffin: TV a x f \is a fin_num. have Nffin : TV a x (\- f) \is a fin_num. apply/bounded_variationP => //; apply/bounded_variationN. exact: (bounded_variationl ax xb). -rewrite /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //; first last. +rewrite /pos_tv /neg_tv /= total_variationN -fineB -?muleBl // ?fineM //. +- rewrite addeAC oppeD //= ?fin_num_adde_defl //. + by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -Num.Theory.splitr. +- by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split. +- by apply: fin_num_adde_defl; rewrite fin_numN fin_numD; apply/andP; split. - by rewrite fin_numM // fin_numD; apply/andP; split. - by rewrite fin_numM // fin_numD; apply/andP; split. -- by apply: fin_num_adde_defl; rewrite fin_numN fin_numD; apply/andP; split. -- by rewrite fin_numB ?fin_numD ?ffin; apply/andP; split. -rewrite addeAC oppeD //= ?fin_num_adde_defl //. -by rewrite addeA subee // add0e -EFinD //= opprK mulrDl -Num.Theory.splitr. Qed. Lemma fine_neg_tv_nondecreasing a b f : BV a b f -> From 208c8e860d95dbe69d3251a4de2a0004f2b09698 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Mon, 15 Jan 2024 19:04:46 +0900 Subject: [PATCH 19/22] variation using prev and next --- CHANGELOG_UNRELEASED.md | 3 +++ theories/realfun.v | 35 +++++++++++++++++++++++++++++++++-- 2 files changed, 36 insertions(+), 2 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 04fcb2cb6..dc1490a23 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -114,6 +114,9 @@ `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/theories/realfun.v b/theories/realfun.v index fe8157c2e..7fec6f1a8 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -1795,6 +1795,37 @@ have /ih : itv_partition h b t by split => //; exact/eqP. by rewrite /variation => ->; rewrite !big_seq; apply/eq_bigr => r rt. Qed. +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. @@ -2336,14 +2367,14 @@ have : variation x b f (i :: j) <= variation x t f (t :: nil) + by rewrite /itv_partition/= ti ij ijb. exact: le_variation. rewrite -lee_fin => /lt_le_trans /[apply]. -rewrite {1}variationE; last exact: itv_partition1. +rewrite {1}variation_prev; last exact: itv_partition1. rewrite /= -addeA -lte_subr_addr; last by rewrite fin_numD; apply/andP. rewrite EFinD -lte_fin ?fineK // oppeD //= ?fin_num_adde_defl // opprK addeA. move/lt_trans; apply. rewrite [x in (_ < x%:E)%E]Num.Theory.splitr EFinD addeC lte_add2lE //. rewrite -addeA. apply: (@le_lt_trans _ _ (variation x t f (t :: nil))%:E). - rewrite [in leRHS]variationE; last exact: itv_partition1. + rewrite [in leRHS]variation_prev; last exact: itv_partition1. rewrite gee_addl // sube_le0; apply: ereal_sup_ub => /=. exists (variation t b f (i :: j)) => //; apply: variations_variation. by rewrite /itv_partition/= ijb ij ti. From 4e6aacd94447ca20a0bda8ec5cc27e5afc8000e9 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 17 Jan 2024 15:16:43 +0900 Subject: [PATCH 20/22] 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. From 48235eb9858a0d24ab002c4ed93799611f8031dc Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 19 Jan 2024 14:15:12 +0900 Subject: [PATCH 21/22] fix --- CHANGELOG_UNRELEASED.md | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index d2ddab391..4e62b78dd 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -65,15 +65,18 @@ - in `ereal.v`: + lemma `ereal_supy` +- in `mathcomp_extra.v`: + + lemmas `last_filterP`, + `path_lt_filter0`, `path_lt_filterT`, `path_lt_head`, `path_lt_last_filter`, + `path_lt_le_last` + - in file `realfun.v`, + new definitions `itv_partition`, `itv_partitionL`, `itv_partitionR`, `variation`, `variations`, `bounded_variation`, `total_variation`, `neg_tv`, and `pos_tv`. + new lemmas `left_right_continuousP`, - `nondecreasing_funN`, `nonincreasing_funN`, `last_filterP`, - `path_lt_filter0`, `path_lt_filterT`, `path_lt_head`, `path_lt_last_filter`, - `path_lt_le_last` + `nondecreasing_funN`, `nonincreasing_funN` + new lemmas `itv_partition_nil`, `itv_partition_cons`, `itv_partition1`, `itv_partition_size_neq0`, `itv_partitionxx`, `itv_partition_le`, From df8d6f02cb1e8652430e42e24c695aeb583dc77f Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 19 Jan 2024 14:36:29 +0900 Subject: [PATCH 22/22] fix --- CHANGELOG_UNRELEASED.md | 14 +------------- 1 file changed, 1 insertion(+), 13 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 4e62b78dd..06fa683ac 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -103,19 +103,7 @@ `total_variation_pos_neg_tvE`, `fine_neg_tv_nondecreasing`, `neg_tv_bounded_variation`, `total_variation_right_continuous`, `neg_tv_right_continuous`, `total_variation_opp`, - `total_variation_left_continuous`, `total_variation_continuous`, - `le_variation`, `variation_opp_rev`, `variation_rev_opp`, - `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`, - `total_variation_ge`, `total_variation_ge0`, - `nondecreasing_total_variation`, `bounded_variationP`, `total_variationN`, - `total_variation_le`, `total_variationD`, `neg_TV_increasing`, - `total_variation_jordan_decompE`, `neg_TV_increasing_fin`, - `neg_TV_bounded_variation`, `TV_right_continuous`, - `neg_TV_right_continuous`, `total_variation_opp`, `TV_left_continuous`, and - `TV_continuous`. + `total_variation_left_continuous`, `total_variation_continuous` ### Changed