Skip to content

Commit 9c311a9

Browse files
affeldt-aistaffeldt-aist
authored
changelog for version 1.2.0 (#1239)
* changelog for version 1.2.0
1 parent 8d95107 commit 9c311a9

9 files changed

+270
-285
lines changed

‎CHANGELOG.md‎

Lines changed: 265 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,270 @@
11
# Changelog
22

3-
Latest releases: [[1.1.0] - 2024-03-31](#110---2024-03-31) and [[1.0.0] - 2024-01-26](#100---2024-01-26)
3+
Latest releases: [[1.2.0] - 2024-06-06](#120---2024-06-06) and [[1.1.0] - 2024-03-31](#110---2024-03-31)
4+
5+
## [1.2.0] - 2024-06-06
6+
7+
### Added
8+
9+
- in file `mathcomp_extra.v`:
10+
+ module `Order`
11+
* definitions `disp_t`, `default_display`
12+
+ lemma `Pos_to_natE`
13+
14+
- in `classical_sets.v`:
15+
+ lemma `bigcup_recl`
16+
+ notations `\bigcup_(i >= n) F i` and `\bigcap_(i >= n) F i`
17+
+ lemmas `bigcup_addn`, `bigcap_addn`
18+
+ lemmas `setD_bigcup`, `nat_nonempty`
19+
+ hint `nat_nonempty`
20+
+ lemma `bigcup_bigsetU_bigcup`
21+
+ lemmas `setDUD`, `setIDAC`
22+
23+
- in `Rstruct.v`:
24+
+ lemma `IZRposE`
25+
26+
- in `signed.v`:
27+
+ lemma `onem_nonneg_proof`, definition `onem_nonneg`
28+
29+
- in `esum.v`:
30+
+ lemma `nneseries_sum_bigcup`
31+
32+
- in `normedtype.v`:
33+
+ lemma `not_near_at_leftP`
34+
35+
- in `sequences.v`:
36+
+ lemma `nneseries_recl`
37+
+ lemma `nneseries_addn`
38+
39+
- in `realfun.v`
40+
+ lemmas `total_variation_nondecreasing`, `total_variation_bounded_variation`
41+
42+
- in `measure.v`:
43+
+ definition `subset_sigma_subadditive`
44+
+ factory `isSubsetOuterMeasure`
45+
+ structure `SigmaRing`, notation `sigmaRingType`
46+
+ factory `isSigmaRing`
47+
+ lemma `bigcap_measurable` for `sigmaRingType`
48+
+ lemma `setDI_semi_setD_closed`
49+
+ lemmas `powerset_lambda_system`, `lambda_system_smallest`, `sigmaRingType_lambda_system`
50+
+ definitions `niseq_closed`, `sigma_ring` (notation `<<sr _ >>`),
51+
`monotone` (notation `<<M _ >>`)
52+
+ lemmas `smallest_sigma_ring`, `sigma_ring_monotone`, `g_sigma_ring_monotone`,
53+
`sub_g_sigma_ring`, `setring_monotone_sigma_ring`, `g_monotone_monotone`,
54+
`g_monotone_setring`, `g_monotone_g_sigma_ring`, `monotone_setring_sub_g_sigma_ring`
55+
+ lemmas `powerset_sigma_ring`, `g_sigma_ring_strace`, `setI_g_sigma_ring`,
56+
`subset_strace`
57+
+ lemma `measurable_and`
58+
+ lemma `measurableID`
59+
+ lemma `strace_sigma_ring`
60+
61+
- in `lebesgue_measure.v`:
62+
+ lemma `measurable_fun_ler`
63+
+ lemmas `measurable_natmul`, `measurable_fun_pow`
64+
65+
- in `lebesgue_integral.v`:
66+
+ lemmas `integrableMl`, `integrableMr`
67+
68+
- in `probability.v`:
69+
+ definition `bernoulli_pmf`
70+
+ lemmas `bernoulli_pmf_ge0`, `bernoulli_pmf1`, `measurable_bernoulli_pmf`
71+
+ definition `bernoulli` (equipped with the `probability` structure)
72+
+ lemmas `bernoulli_dirac`, `bernoulliE`, `integral_bernoulli`, `measurable_bernoulli`,
73+
`measurable_bernoulli2`
74+
+ definition `binomial_pmf`
75+
+ lemmas `binomial_pmf_ge0`, `measurable_binomial_pmf`
76+
+ definitions `binomial_prob` (equipped with the `probability` structure), `bin_prob`
77+
+ lemmas `bin_prob0`, `bin_prob1`, `binomial_msum`, `binomial_probE`, `integral_binomial`,
78+
`integral_binomial_prob`, `measurable_binomial_prob`
79+
+ definition `uniform_pdf`
80+
+ lemmas `measurable_uniform_pdf`, `integral_uniform_pdf`, `integral_uniform_pdf1`
81+
+ definition `uniform_prob` (equipped with the `probability` structure)
82+
+ lemmas `dominates_uniform_prob`, `integral_uniform`
83+
84+
- new file `theories/all_analysis.v`
85+
86+
### Changed
87+
88+
- in `forms.v`:
89+
+ notation ``` u ``_ _ ```
90+
91+
- in `sequences.v`:
92+
+ definition `expR` is now HB.locked
93+
+ equality reversed in lemma `eq_bigcup_seqD`
94+
+ `eq_bigsetU_seqD` renamed to `nondecreasing_bigsetU_seqD`
95+
and equality reversed
96+
97+
- in `trigo.v`:
98+
+ definitions `sin`, `cos`, `acos`, `asin`, `atan` are now HB.locked
99+
100+
- in `measure.v`:
101+
+ change the hypothesis of `measurable_fun_bool`
102+
+ mixin `AlgebraOfSets_isMeasurable` renamed to `hasMeasurableCountableUnion`
103+
and made to inherit from `SemiRingOfSets`
104+
+ rm hypo and variable in lemma `smallest_monotone_classE`
105+
and rename to `smallest_lambda_system`
106+
+ rm hypo in lemma `monotone_class_g_salgebra` and renamed
107+
to `g_salgebra_lambda_system`
108+
+ rm hypo in lemma `monotone_class_subset` and renamed to
109+
`lambda_system_subset`
110+
+ notation `<<m _, _>>` changed to `<<l _, _>>`,
111+
notation `<<m _>>` changed to `<<l _>>`
112+
113+
- moved from `lebesgue_measure.v` to `measure.v`:
114+
+ definition `strace`
115+
+ lemma `sigma_algebra_strace`
116+
117+
### Renamed
118+
119+
- in `classical_sets.v`:
120+
+ `notin_set` -> `notin_setE`
121+
122+
- in `constructive_ereal.v`:
123+
+ `gee_pmull` -> `gee_pMl`
124+
+ `gee_addl` -> `geeDl`
125+
+ `gee_addr` -> `geeDr`
126+
+ `gte_addl` -> `gteDl`
127+
+ `gte_addr` -> `gteDr`
128+
+ `lte_subl_addr` -> `lteBlDr`
129+
+ `lte_subl_addl` -> `lteBlDl`
130+
+ `lte_subr_addr` -> `lteBrDr`
131+
+ `lte_subr_addl` -> `lteBrDl`
132+
+ `lee_subl_addr` -> `leeBlDr`
133+
+ `lee_subl_addl` -> `leeBlDl`
134+
+ `lee_subr_addr` -> `leeBrDr`
135+
+ `lee_subr_addl` -> `leeBrDl`
136+
+ `num_lee_maxr` -> `num_lee_max`
137+
+ `num_lee_maxl` -> `num_gee_max`
138+
+ `num_lee_minr` -> `num_lee_min`
139+
+ `num_lee_minl` -> `num_gee_min`
140+
+ `num_lte_maxr` -> `num_lte_max`
141+
+ `num_lte_maxl` -> `num_gte_max`
142+
+ `num_lte_minr` -> `num_lte_min`
143+
+ `num_lte_minl` -> `num_gte_min`
144+
145+
- in `signed.v`:
146+
+ `num_le_maxr` -> `num_le_max`
147+
+ `num_le_maxl` -> `num_ge_max`
148+
+ `num_le_minr` -> `num_le_min`
149+
+ `num_le_minl` -> `num_ge_min`
150+
+ `num_lt_maxr` -> `num_lt_max`
151+
+ `num_lt_maxl` -> `num_gt_max`
152+
+ `num_lt_minr` -> `num_lt_min`
153+
+ `num_lt_minl` -> `num_gt_min`
154+
155+
- in `measure.v`:
156+
+ `sub_additive` -> `subadditive`
157+
+ `sigma_sub_additive` -> `measurable_subset_sigma_subadditive`
158+
+ `content_sub_additive` -> `content_subadditive`
159+
+ `ring_sigma_sub_additive` -> `ring_sigma_subadditive`
160+
+ `Content_SubSigmaAdditive_isMeasure` -> `Content_SigmaSubAdditive_isMeasure`
161+
+ `measure_sigma_sub_additive` -> `measure_sigma_subadditive`
162+
+ `measure_sigma_sub_additive_tail` -> `measure_sigma_subadditive_tail`
163+
+ `bigcap_measurable` -> `bigcap_measurableType`
164+
+ `monotone_class` -> `lambda_system`
165+
+ `monotone_class_g_salgebra` -> `g_sigma_algebra_lambda_system`
166+
+ `smallest_monotone_classE` -> `smallest_lambda_system`
167+
+ `dynkin_monotone` -> `dynkin_lambda_system`
168+
+ `dynkin_g_dynkin` -> `g_dynkin_dynkin`
169+
+ `salgebraType` -> `g_sigma_algebraType`
170+
+ `g_salgebra_measure_unique_trace` -> `g_sigma_algebra_measure_unique_trace`
171+
+ `g_salgebra_measure_unique_cover` -> `g_sigma_algebra_measure_unique_cover`
172+
+ `g_salgebra_measure_unique` -> `g_sigma_algebra_measure_unique`
173+
+ `setI_closed_gdynkin_salgebra` -> `setI_closed_g_dynkin_g_sigma_algebra`
174+
175+
- in `lebesgue_integral.v`:
176+
+ `integral_measure_add` -> `ge0_integral_measure_add`
177+
+ `integral_pushforward` -> `ge0_integral_pushforward`
178+
179+
### Generalized
180+
181+
- in `Rstruct.v`:
182+
+ lemmas `RinvE`, `RdivE`
183+
184+
- in `constructive_ereal.v`:
185+
+ `gee_pMl` (was `gee_pmull`)
186+
187+
- in `sequences.v`:
188+
+ lemmas `eseries0`, `nneseries_split`
189+
190+
- in `measure.v`:
191+
+ lemmas `outer_measure_subadditive`, `outer_measureU2` (from `semiRingOfSetType` to `Type`)
192+
+ lemmas `caratheodory_measurable_mu_ext`, `measurableM`, `measure_dominates_trans`, `ess_sup_ge0`
193+
definitions `preimage_classes`, `measure_dominates`, `ess_sup`
194+
(from `measurableType` to `semiRingOfSetsType`)
195+
+ lemmas ` measurable_prod_measurableType`, `measurable_prod_g_measurableTypeR` (from `measurableType` to `algebraOfSetsType`)
196+
+ from `measurableType` to `sigmaRingType`
197+
* lemmas `bigcup_measurable`, `bigcapT_measurable`
198+
* definition `measurable_fun`
199+
* lemmas `measurable_id`, `measurable_comp`, `eq_measurable_fun`, `measurable_cst`,
200+
`measurable_fun_bigcup`, `measurable_funU`, `measurable_funS`, `measurable_fun_if`
201+
* lemmas `semi_sigma_additiveE`, `sigma_additive_is_additive`, `measure_sigma_additive`
202+
* definitions `pushforward`, `dirac`
203+
* lemmas `diracE`, `dirac0`, `diracT`, `finite_card_sum`, `finite_card_dirac`, `infinite_card_dirac`
204+
* definitions `msum`, `measure_add`, `mscale`, `mseries`, `mrestr`
205+
* lemmas `msum_mzero`, `measure_addE`
206+
* definition `sfinite_measure`
207+
* mixin `isSFinite`, structure `SFiniteMeasure`
208+
* structure `FiniteMeasure`
209+
* factory `Measure_isSFinite`
210+
* lemma `negligible_bigcup`
211+
* definition `ae_eq`
212+
* lemmas `ae_eq0`, `ae_eq_comp`, `ae_eq_funeposneg`, `ae_eq_refl`, `ae_eq_sym`,
213+
`ae_eq_trans`, `ae_eq_sub`, `ae_eq_mul2r`, `ae_eq_mul2l`, `ae_eq_mul1l`,
214+
`ae_eq_abse`, `ae_eq_subset`
215+
+ from `measurableType` to `sigmaRingType` and from `realType` to `realFieldType`
216+
* definition `mzero`
217+
+ from `realType` to `realFieldType`:
218+
* lemma `sigma_finite_mzero`
219+
220+
- in `lebesgue_measure.v`:
221+
+ from `measurableType` to `sigmaRingType`
222+
* section `measurable_fun_measurable`
223+
224+
- in `lebesgue_integral.v`:
225+
+ lemma `ge0_integral_bigcup`
226+
+ lemma `ge0_emeasurable_fun_sum`
227+
+ from `measurableType` to `sigmaRingType`
228+
* mixin `isMeasurableFun`
229+
* structure `SimpleFun`
230+
* structure `NonNegSimpleFun`
231+
* sections `fimfun_bin`, `mfun_pred`, `sfun_pred`, `simple_bounded`
232+
* lemmas `nnfun_muleindic_ge0`, `mulemu_ge0`, `nnsfun_mulemu_ge0`
233+
* section `sintegral_lemmas`
234+
* lemma `eq_sintegral`
235+
* section `sintegralrM`
236+
237+
- in `probability.v`:
238+
+ lemma `markov`
239+
240+
### Deprecated
241+
242+
- in `classical_sets.v`:
243+
+ `notin_set` (use `notin_setE` instead)
244+
245+
### Removed
246+
247+
- in `forms.v`
248+
+ canonical `rev_mulmx`
249+
+ structure `revop`
250+
251+
- in `reals.v`
252+
+ lemma `inf_lower_bound` (use `inf_lb` instead)
253+
254+
- in `derive.v`:
255+
+ definition `mulr_rev`
256+
+ canonical `rev_mulr`
257+
+ lemmas `mulr_is_linear`, `mulr_rev_is_linear`
258+
259+
- in `measure.v`:
260+
+ lemmas `prod_salgebra_set0`, `prod_salgebra_setC`, `prod_salgebra_bigcup`
261+
(use `measurable0`, `measurableC`, `measurable_bigcup` instead)
262+
263+
- in `lebesgue_measure.v`:
264+
+ lemmas `stracexx`, `strace_measurable`
265+
266+
- in `lebesgue_integral.v`:
267+
+ `integrablerM`, `integrableMr` (were deprecated since version 0.6.4)
4268

5269
## [1.1.0] - 2024-03-31
6270

0 commit comments

Comments
 (0)