doc & changelog

Author: affeldt-aist

CHANGELOG_UNRELEASED.md

@@ -128,6 +128,9 @@
     * lemmas `zornS_ex`, `domain_extend`, `hahn_banach_witness`
   + theorems `hahn_banach_extension`, `hahn_banach_extension_normed`
 
+- in `lebesgue_stieltjes_measure.v`:
+  + definition `lebesgue_display`
+
 ### Changed
 
 - moved from `measurable_structure.v` to `classical_sets.v`:

theories/lebesgue_measure.v

@@ -338,7 +338,6 @@ End LebesgueMeasure.
 
 Definition lebesgue_measure {R : realType} : set R -> \bar R :=
   lebesgue_stieltjes_measure idfun.
-Check fun R : realType => lebesgue_stieltjes_measure idfun : Measure.type _ _.
 HB.instance Definition _ (R : realType) := Measure.on (@lebesgue_measure R).
 HB.instance Definition _ (R : realType) :=
   SigmaFiniteMeasure.on (@lebesgue_measure R).

theories/lebesgue_stieltjes_measure.v

@@ -33,6 +33,10 @@ From mathcomp Require Import realfun.
 (*         R.-ocitv.-measurable == semiring of sets of open-closed intervals  *)
 (*                  wlength f A := f b - f a with the hull of the set of real *)
 (*                                 numbers A being delimited by a and b       *)
+(*           @measurableTypeR R == measurableType generated by R.-ocitv       *)
+(*          @lebesgue_display R == (measure_)display for the sigma-algebra    *)
+(*                                 generated by R.-ocitv                      *)
+(*               @measurableR R == measurable sets generated by R.-ocitv      *)
 (* lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f           *)
 (*                                 f is a cumulative function.                *)
 (* completed_lebesgue_stieltjes_measure f == the completed Lebesgue-Stieltjes *)
@@ -522,7 +526,7 @@ Definition measurableR : set (set R) :=
 HB.instance Definition _ : Measurable lebesgue_display (measurableTypeR R) :=
    Measurable.on (measurableTypeR R).
 (* Presumably it is safe to use NFI here because morally R is unique
-   and nothing else can be used here*)
+   and nothing else can be used here *)
 #[non_forgetful_inheritance]
 HB.instance Definition _ := Measurable.copy R (measurableTypeR R).