Skip to content

Commit

Permalink
changelog for version 0.3.10
Browse files Browse the repository at this point in the history
  • Loading branch information
@affeldt-aist
affeldt-aist committed Aug 11, 2021
1 parent 6db5e90 commit ea16ab0
Show file tree
Hide file tree
Showing 2 changed files with 127 additions and 125 deletions.
128 changes: 127 additions & 1 deletion CHANGELOG.md
View file
Original file line number Diff line number Diff line change
@@ -1,6 +1,132 @@
# Changelog

Last releases: [[0.3.9] - 2021-06-12](#039---2021-06-12) and [[0.3.8] - 2021-06-01](#038---2021-06-01)
Last releases: [[0.3.10] - 2021-08-11](#0310---2021-08-11) and [[0.3.9] - 2021-06-12](#039---2021-06-12)

## [0.3.10] - 2021-08-11

### Added

- in `classical_sets.v`:
+ lemmas `bigcup_image`, `bigcup_of_set1`
+ lemmas `bigcupD1`, `bigcapD1`
- in `boolp.v`:
+ definitions `equality_mixin_of_Type`, `choice_of_Type`
- in `normedtype.v`:
+ lemma `cvg_bounded_real`
+ lemma `pseudoMetricNormedZModType_hausdorff`
- in `sequences.v`:
+ lemmas `seriesN`, `seriesD`, `seriesZ`, `is_cvg_seriesN`, `lim_seriesN`,
`is_cvg_seriesZ`, `lim_seriesZ`, `is_cvg_seriesD`, `lim_seriesD`,
`is_cvg_seriesB`, `lim_seriesB`, `lim_series_le`, `lim_series_norm`
- in `measure.v`:
+ HB.mixin `AlgebraOfSets_from_RingOfSets`
+ HB.structure `AlgebraOfSets` and notation `algebraOfSetsType`
+ HB.instance `T_isAlgebraOfSets` in HB.builders `isAlgebraOfSets`
+ lemma `bigcup_set_cond`
+ definition `measurable_fun`
+ lemma `adde_undef_nneg_series`
+ lemma `adde_def_nneg_series`
+ lemmas `cvg_geometric_series_half`, `epsilon_trick`
+ definition `measurable_cover`
+ lemmas `cover_measurable`, `cover_subset`
+ definition `mu_ext`
+ lemmas `le_mu_ext`, `mu_ext_ge0`, `mu_ext0`, `measurable_uncurry`,
`mu_ext_sigma_subadditive`
+ canonical `outer_measure_of_measure`

### Changed

- in `ereal.v`, definition `adde_undef` changed to `adde_def`
+ consequently, the following lemmas changed:
* in `ereal.v`, `adde_undefC` renamed to `adde_defC`,
`fin_num_adde_undef` renamed to `fin_num_adde_def`
* in `sequences.v`, `ereal_cvgD` and `ereal_limD` now use hypotheses with `adde_def`
- in `sequences.v`:
+ generalize `{in,de}creasing_seqP`, `non{in,de}creasing_seqP` from `numDomainType`
to `porderType`
- in `normedtype.v`:
+ generalized from `normedModType` to `pseudoMetricNormedZmodType`:
* `nbhs_le_nbhs_norm`
* `nbhs_norm_le_nbhs`
* `nbhs_nbhs_norm`
* `nbhs_normP`
* `filter_from_norm_nbhs`
* `nbhs_normE`
* `filter_from_normE`
* `near_nbhs_norm`
* `nbhs_norm_ball_norm`
* `nbhs_ball_norm`
* `ball_norm_dec`
* `ball_norm_sym`
* `ball_norm_le`
* `cvg_distP`
* `cvg_dist`
* `nbhs_norm_ball`
* `dominated_by`
* `strictly_dominated_by`
* `sub_dominatedl`
* `sub_dominatedr`
* `dominated_by1`
* `strictly_dominated_by1`
* `ex_dom_bound`
* `ex_strict_dom_bound`
* `bounded_near`
* `boundedE`
* `sub_boundedr`
* `sub_boundedl`
* `ex_bound`
* `ex_strict_bound`
* `ex_strict_bound_gt0`
* `norm_hausdorff`
* `norm_closeE`
* `norm_close_eq`
* `norm_cvg_unique`
* `norm_cvg_eq`
* `norm_lim_id`
* `norm_cvg_lim`
* `norm_lim_near_cst`
* `norm_lim_cst`
* `norm_cvgi_unique`
* `norm_cvgi_map_lim`
* `distm_lt_split`
* `distm_lt_splitr`
* `distm_lt_splitl`
* `normm_leW`
* `normm_lt_split`
* `cvg_distW`
* `continuous_cvg_dist`
* `add_continuous`
- in `measure.v`:
+ generalize lemma `eq_bigcupB_of`
+ HB.mixin `Measurable_from_ringOfSets` changed to `Measurable_from_algebraOfSets`
+ HB.instance `T_isRingOfSets` becomes `T_isAlgebraOfSets` in HB.builders `isMeasurable`
+ lemma `measurableC` now applies to `algebraOfSetsType` instead of `measureableType`
- moved from `normedtype.v` to `reals.v`:
+ lemmas `inf_lb_strict`, `sup_ub_strict`
- moved from `sequences.v` to `reals.v`:
+ lemma `has_ub_image_norm`

### Renamed

- in `classical_sets.v`:
+ `bigcup_mkset` -> `bigcup_set`
+ `bigsetU` -> `bigcup`
+ `bigsetI` -> `bigcap`
+ `trivIset_bigUI` -> `trivIset_bigsetUI`
- in `measure.v`:
+ `isRingOfSets` -> `isAlgebraOfSets`
+ `B_of` -> `seqD`
+ `trivIset_B_of` -> `trivIset_seqD`
+ `UB_of` -> `setU_seqD`
+ `bigUB_of` -> `bigsetU_seqD`
+ `eq_bigsetUB_of` -> `eq_bigsetU_seqD`
+ `eq_bigcupB_of` -> `eq_bigcup_seqD`
+ `eq_bigcupB_of_bigsetU` -> `eq_bigcup_seqD_bigsetU`

### Removed

- in `nngnum.v`:
+ lemma `filter_andb`

## [0.3.9] - 2021-06-12

Expand Down
124 changes: 0 additions & 124 deletions CHANGELOG_UNRELEASED.md
View file
Original file line number Diff line number Diff line change
Expand Up @@ -4,136 +4,12 @@

### Added

- in `sequences.v`:
+ lemmas `seriesN`, `seriesD`, `seriesZ`, `is_cvg_seriesN`, `lim_seriesN`,
`is_cvg_seriesZ`, `lim_seriesZ`, `is_cvg_seriesD`, `lim_seriesD`,
`is_cvg_seriesB`, `lim_seriesB`, `lim_series_le`, `lim_series_norm`
- in `classical_sets.v`:
+ lemmas `bigcup_image`, `bigcup_of_set1`
- in `boolp.v`:
+ definitions `equality_mixin_of_Type`, `choice_of_Type`
- in `measure.v`:
+ HB.mixin `AlgebraOfSets_from_RingOfSets`
+ HB.structure `AlgebraOfSets` and notation `algebraOfSetsType`
+ HB.instance `T_isAlgebraOfSets` in HB.builders `isAlgebraOfSets`
+ lemma `bigcup_set_cond`
- in `classical_sets.v`:
+ lemmas `bigcupD1`, `bigcapD1`
- in `measure.v`:
+ definition `measurable_fun`
+ lemma `adde_undef_nneg_series`
+ lemma `adde_def_nneg_series`
- in `measure.v`:
+ lemmas `cvg_geometric_series_half`, `epsilon_trick`
+ definition `measurable_cover`
+ lemmas `cover_measurable`, `cover_subset`
+ definition `mu_ext`
+ lemmas `le_mu_ext`, `mu_ext_ge0`, `mu_ext0`, `measurable_uncurry`,
`mu_ext_sigma_subadditive`
+ canonical `outer_measure_of_measure`

### Changed

- in `measure.v`:
+ generalize lemma `eq_bigcupB_of`
- in `ereal.v`, definition `adde_undef` changed to `adde_def`
+ consequently, the following lemmas changed:
* in `ereal.v`, `adde_undefC` renamed to `adde_defC`,
`fin_num_adde_undef` renamed to `fin_num_adde_def`
* in `sequences.v`, `ereal_cvgD` and `ereal_limD` now use hypotheses with `adde_def`
- in `sequences.v`:
+ generalize `{in,de}creasing_seqP`, `non{in,de}creasing_seqP` from `numDomainType`
to `porderType`
- in `measure.v`:
+ HB.mixin `Measurable_from_ringOfSets` changed to `Measurable_from_algebraOfSets`
+ HB.instance `T_isRingOfSets` becomes `T_isAlgebraOfSets` in HB.builders `isMeasurable`
+ lemma `measurableC` now applies to `algebraOfSetsType` instead of `measureableType`
- in `normedtype.v`:
+ lemma `cvg_bounded_real`
+ lemma `pseudoMetricNormedZModType_hausdorff`

### Changed

- in `normedtype.v`:
+ generalized from `normedModType` to `pseudoMetricNormedZmodType`:
* `nbhs_le_nbhs_norm`
* `nbhs_norm_le_nbhs`
* `nbhs_nbhs_norm`
* `nbhs_normP`
* `filter_from_norm_nbhs`
* `nbhs_normE`
* `filter_from_normE`
* `near_nbhs_norm`
* `nbhs_norm_ball_norm`
* `nbhs_ball_norm`
* `ball_norm_dec`
* `ball_norm_sym`
* `ball_norm_le`
* `cvg_distP`
* `cvg_dist`
* `nbhs_norm_ball`
* `dominated_by`
* `strictly_dominated_by`
* `sub_dominatedl`
* `sub_dominatedr`
* `dominated_by1`
* `strictly_dominated_by1`
* `ex_dom_bound`
* `ex_strict_dom_bound`
* `bounded_near`
* `boundedE`
* `sub_boundedr`
* `sub_boundedl`
* `ex_bound`
* `ex_strict_bound`
* `ex_strict_bound_gt0`
* `norm_hausdorff`
* `norm_closeE`
* `norm_close_eq`
* `norm_cvg_unique`
* `norm_cvg_eq`
* `norm_lim_id`
* `norm_cvg_lim`
* `norm_lim_near_cst`
* `norm_lim_cst`
* `norm_cvgi_unique`
* `norm_cvgi_map_lim`
* `distm_lt_split`
* `distm_lt_splitr`
* `distm_lt_splitl`
* `normm_leW`
* `normm_lt_split`
* `cvg_distW`
* `continuous_cvg_dist`
* `add_continuous`
- moved from `normedtype.v` to `reals.v`:
+ lemmas `inf_lb_strict`, `sup_ub_strict`
- moved from `sequences.v` to `reals.v`:
+ lemma `has_ub_image_norm`

### Renamed

- in `measure.v`:
+ `isRingOfSets` -> `isAlgebraOfSets`
- in `classical_sets.v`:
+ `bigcup_mkset` -> `bigcup_set`
+ `bigsetU` -> `bigcup`
+ `bigsetI` -> `bigcap`
+ `trivIset_bigUI` -> `trivIset_bigsetUI`
- in `measure.v`:
+ `B_of` -> `seqD`
+ `trivIset_B_of` -> `trivIset_seqD`
+ `UB_of` -> `setU_seqD`
+ `bigUB_of` -> `bigsetU_seqD`
+ `eq_bigsetUB_of` -> `eq_bigsetU_seqD`
+ `eq_bigcupB_of` -> `eq_bigcup_seqD`
+ `eq_bigcupB_of_bigsetU` -> `eq_bigcup_seqD_bigsetU`

### Removed

- in `nngnum.v`:
+ lemma `filter_andb`

### Infrastructure

### Misc

0 comments on commit ea16ab0

Please sign in to comment.