fix, clean, doc, changelog

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -12,110 +12,22 @@
 - in `lebesgue_integral.v`:
   + lemma `sfinite_Fubini`
 - in `classical_sets.v`:
-  + canonical `unit_pointedType`
-- in `measure.v`:
-  + mixin `isProbability`, structure `Probability`, type `probability`
-  + lemma `probability_le1`
-  + definition `discrete_measurable_unit`
-  + structures `sigma_finite_additive_measure` and `sigma_finite_measure`
-
-- in file `topology.v`,
-  + new definition `perfect_set`.
-  + new lemmas `perfectTP`, `perfect_prod`, and `perfect_diagonal`.
-- in `constructive_ereal.v`:
-  + lemmas `EFin_sum_fine`, `sumeN`
-  + lemmas `adde_defDr`, `adde_def_sum`, `fin_num_sumeN`
-  + lemma `fin_num_adde_defr`, `adde_defN`
-
-- in `constructive_ereal.v`:
-  + lemma `oppe_inj`
-
-- in `mathcomp_extra.v`:
-  + lemma `add_onemK`
-  + function `swap`
-- in `classical_sets.v`:
-  + lemmas `setT0`, `set_unit`, `set_bool`
-  + lemmas `xsection_preimage_snd`, `ysection_preimage_fst`
-- in `exp.v`:
-  + lemma `expR_ge0`
-- in `measure.v`
-  + lemmas `measurable_curry`, `measurable_fun_fst`, `measurable_fun_snd`,
-    `measurable_fun_swap`, `measurable_fun_pair`, `measurable_fun_if_pair`
-  + lemmas `dirac0`, `diracT`
-  + lemma `fin_num_fun_sigma_finite`
-- in `lebesgue_measure.v`:
-  + lemma `measurable_fun_opp`
-- in `lebesgue_integral.v`
-  + lemmas `integral0_eq`, `fubini_tonelli`
-  + product measures now take `{measure _ -> _}` arguments and their
-    theory quantifies over a `{sigma_finite_measure _ -> _}`.
-
-- in `classical_sets.v`:
-  + lemma `trivIset_mkcond`
-- in `numfun.v`:
-  + lemmas `xsection_indic`, `ysection_indic`
-- in `classical_sets.v`:
-  + lemmas `xsectionI`, `ysectionI`
-- in `lebesgue_integral.v`:
-  + notations `\x`, `\x^` for `product_measure1` and `product_measure2`
-
-- in `constructive_ereal.v`:
-  + lemmas `expeS`, `fin_numX`
-
-- in `functions.v`:
-  + lemma `countable_bijP`
-  + lemma `patchE`
-
-- in file `topology.v`,
-  + new definitions `countable_uniformity`, `countable_uniformityT`, 
-    `sup_pseudoMetric_mixin`, `sup_pseudoMetricType`, and 
-    `product_pseudoMetricType`.
-  + new lemmas `countable_uniformityP`, `countable_sup_ent`, and 
-    `countable_uniformity_metric`.
-
-- in `constructive_ereal.v`:
-  + lemmas `adde_def_doppeD`, `adde_def_doppeB`
-  + lemma `fin_num_sume_distrr`
-- in `classical_sets.v`:
-  + lemma `coverE`
-
-- in file `topology.v`,
-  + new definitions `quotient_topology`, and `quotient_open`.
-  + new lemmas `pi_continuous`, `quotient_continuous`, and
-    `repr_comp_continuous`.
-
-- in file `boolp.v`,
-  + new lemma `forallp_asboolPn2`.
-- in file `classical_sets.v`,
-  + new lemma `preimage_range`.
-- in file `topology.v`,
-  + new definitions `hausdorff_accessible`, `separate_points_from_closed`, and 
-    `join_product`.
-  + new lemmas `weak_sep_cvg`, `weak_sep_nbhsE`, `weak_sep_openE`, 
-    `join_product_continuous`, `join_product_open`, `join_product_inj`, and 
-    `join_product_weak`. 
-- in `measure.v`:
-  + structure `FiniteMeasure`, notation `{finite_measure set _ -> \bar _}`
-
-- in `measure.v`:
-  + definition `sfinite_measure_def`
-  + mixin `Measure_isSFinite_subdef`, structure `SFiniteMeasure`,
-    notation `{sfinite_measure set _ -> \bar _}`
-  + mixin `SigmaFinite_isFinite` with field `fin_num_measure`, structure `FiniteMeasure`,
-    notation `{finite_measure set _ -> \bar _}`
-  + lemmas `sfinite_measure_sigma_finite`, `sfinite_mzero`, `sigma_finite_mzero`
-  + factory `Measure_isFinite`, `Measure_isSFinite`
-  + lemma `sfinite_measure`
-  + mixin `FiniteMeasure_isSubProbability`, structure `SubProbability`,
-    notation `subprobability`
-  + factory `Measure_isSubProbability`
-  + factory `FiniteMeasure_isSubProbability`
-  + factory `Measure_isSigmaFinite`
-  + lemmas `fin_num_fun_lty`, `finite_measure_fin_num_fun`
-  + definition `fin_num_fun`
-  + structure `FinNumFun`
-  + definition `finite_measure2`
-  + lemmas `finite_measure2_finite_measure`, `finite_measure_finite_measure2`
+  + lemmas `ltn_trivIset`, `subsetC_trivIset`
+- in `sequences.v`:
+  + lemma `seqDUIE`
+- file `charge.v`:
+  + mixin `isAdditiveCharge`, structure `AdditiveCharge`, notations
+    `additive_charge`, `{additive_charge set T -> \bar R}`
+  + mixin `isCharge`, structure `Charge`, notations `charge`,
+    `{charge set T -> \bar R}`
+  + lemmas `charge0`, `charge_semi_additiveW`, `charge_semi_additive2E`,
+    `charge_semi_additive2`, `chargeU`, `chargeDI`, `chargeD`,
+    `charge_partition`
+  + definitions `crestr`, `cszero`, `cscale`, `positive_set`, `negative_set`
+  + lemmas `negative_set_charge_le0`, `negative_set0`, `bigcup_negative_set`,
+    `negative_setU`, `positive_negative0`
+  + definition `hahn_decomposition`
+  + lemmas `hahn_decomposition_lemma`, `Hahn_decomposition`, `Hahn_decomposition_uniq`
 
 - file `itv.v`:
   + definition `wider_itv`

classical/classical_sets.v

@@ -2385,6 +2385,20 @@ Section partitions.
 Definition trivIset T I (D : set I) (F : I -> set T) :=
   forall i j : I, D i -> D j -> F i `&` F j !=set0 -> i = j.
 
+Lemma ltn_trivIset T (F : nat -> set T) :
+  (forall n m, (m < n)%N -> F m `&` F n = set0) -> trivIset setT F.
+Proof.
+move=> h m n _ _ [t [mt nt]]; apply/eqP/negPn/negP.
+by rewrite neq_ltn => /orP[] /h; apply/eqP/set0P; exists t.
+Qed.
+
+Lemma subsetC_trivIset T (F : nat -> set T) :
+  (forall n, F n.+1 `<=` ~` \big[setU/set0]_(i < n.+1) F i) -> trivIset setT F.
+Proof.
+move=> sF; apply: ltn_trivIset => n m h; rewrite setIC; apply/disjoints_subset.
+by case: n h => // n h; apply: (subset_trans (sF n)); exact/subsetC/bigsetU_sup.
+Qed.
+
 Lemma trivIset_mkcond T I (D : set I) (F : I -> set T) :
   trivIset D F <-> trivIset setT (fun i => if i \in D then F i else set0).
 Proof.