Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Total variation #1118

Merged
merged 22 commits into from
Jan 19, 2024
Merged
Changes from 1 commit
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
Prev Previous commit
Next Next commit
minor checks (wip)
affeldt-aist committed Jan 19, 2024
commit c2742fe5e5fcb1bf9be1515f1f2e5ddd279f66ad
46 changes: 28 additions & 18 deletions CHANGELOG_UNRELEASED.md
Original file line number Diff line number Diff line change
@@ -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

5 changes: 5 additions & 0 deletions theories/ereal.v
Original file line number Diff line number Diff line change
@@ -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.

77 changes: 37 additions & 40 deletions theories/normedtype.v
Original file line number Diff line number Diff line change
@@ -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 *)
Loading