tentative proof of Hahn decomposition theorem (#777)

- introduces signed measures/charges

Co-authored-by: IshiguroYoshihiro

CHANGELOG_UNRELEASED.md

@@ -11,6 +11,23 @@
   + lemma `emeasurable_itv`
 - in `lebesgue_integral.v`:
   + lemma `sfinite_Fubini`
+- in `classical_sets.v`:
+  + 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`
@@ -148,6 +165,10 @@
     `_ <| _ |> _`
   + lemmas `conv1`, `second_derivative_convex`
 
+- in `mathcomp_extra.v`:
+  + lemma `lt_min_lt`
+- in `constructive_ereal.v`:
+  + lemmas `EFin_min`, `EFin_max`
 
 ### Changed
 
@@ -178,6 +199,10 @@
   + weaken condition of `exp_fun_mulrn` and rename to `power_pos_mulrn`
   + the notation ``` `^ ``` has now scope `real_scope`
   + weaken condition of `riemannR_gt0` and `dvg_riemannR`
+- in `constructive_ereal.v`:
+  + `maxEFin` changed to `fine_max`
+  + `minEFin` changed to `fine_min`
+
 
 ### Renamed
 

_CoqProject

@@ -41,6 +41,7 @@ theories/summability.v
 theories/signed.v
 theories/itv.v
 theories/convex.v
+theories/charge.v
 theories/altreals/xfinmap.v
 theories/altreals/discrete.v
 theories/altreals/realseq.v

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.

classical/mathcomp_extra.v

@@ -1134,3 +1134,17 @@ have [b_gt0 _|//|<- _] := ltgtP; last first.
 have [a_le0|a_gt0] := ler0P a; last by rewrite ler_psqrt.
 by rewrite ler0_sqrtr // sqrtr_ge0 (le_trans a_le0) ?ltW.
 Qed.
+
+Section order_min.
+Variables (d : unit) (T : orderType d).
+Import Order.
+Local Open Scope order_scope.
+
+Lemma lt_min_lt (x y z : T) : (min x z < min y z)%O -> (x < y)%O.
+Proof.
+rewrite /Order.min/=; case: ifPn => xz; case: ifPn => yz; rewrite ?ltxx//.
+- by move=> /lt_le_trans; apply; rewrite leNgt.
+- by rewrite ltNge (ltW yz).
+Qed.
+
+End order_min.

theories/Make

@@ -32,6 +32,7 @@ summability.v
 signed.v
 itv.v
 convex.v
+charge.v
 altreals/xfinmap.v
 altreals/discrete.v
 altreals/realseq.v