From 5bcdf45520324c08857c21f84335e80717cdd05d Mon Sep 17 00:00:00 2001 From: zstone Date: Fri, 12 Jan 2024 14:25:30 -0500 Subject: [PATCH] docs and changelog --- CHANGELOG_UNRELEASED.md | 33 +++++++++++++++++++++++++++++++++ theories/realfun.v | 10 ++++++++++ 2 files changed, 43 insertions(+) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 15dd9a1e68..0020e71e4f 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -13,6 +13,39 @@ - in `lebesgue_integral.v`: + `sigma_finite_measure` instance on product measure `\x` +- 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 ### Renamed diff --git a/theories/realfun.v b/theories/realfun.v index dea77b14ba..bd21d1181f 100644 --- a/theories/realfun.v +++ b/theories/realfun.v @@ -21,6 +21,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 *) +(* *) (* ``` *) (* *) (* * Limit superior and inferior for functions: *)