rebase

theories/lebesgue_measure.v

@@ -555,7 +555,7 @@ Qed.
 End puncture_ereal_itv.
 
 Lemma set1_bigcap_oc (R : realType) (r : R) :
-   [set r] = \bigcap_i `]r - i.+1%:R^-1, r]%classic.
+  [set r] = \bigcap_i `]r - i.+1%:R^-1, r]%classic.
 Proof.
 apply/seteqP; split=> [x ->|].
   by move=> i _/=; rewrite in_itv/= lexx ltr_subl_addr ltr_addl invr_gt0 ltr0n.

theories/lebesgue_stieltjes_measure.v

@@ -73,7 +73,7 @@ Let g : \bar R -> \bar R := EFinf f.
 Implicit Types i j : interval R.
 Definition itvs : Type := R.
 
-Definition hlength (A : set itvs): \bar R := let i := Rhull A in g i.2 - g i.1.
+Definition hlength (A : set itvs) : \bar R := let i := Rhull A in g i.2 - g i.1.
 
 Lemma hlength0 : hlength (set0 : set R) = 0.
 Proof. by rewrite /hlength Rhull0 /= subee. Qed.
@@ -196,7 +196,7 @@ Arguments hlength {R}.
 Section itv_semiRingOfSets.
 Variable R : realType.
 Implicit Types (I J K : set R).
-Local Notation itvs := (itvs R).
+Definition ocitv_type : Type := R.
 
 Definition ocitv := [set `]x.1, x.2]%classic | x in [set: R * R]].
 
@@ -250,16 +250,16 @@ rewrite /Order.meet/= /Order.meet /Order.join/=
 by rewrite -negb_or le_total/=.
 Qed.
 
-HB.instance Definition _  : isSemiRingOfSets itvs :=
-  @isSemiRingOfSets.Build itvs (Pointed.class R) ocitv ocitv0 ocitvI ocitvD.
+Variable d : measure_display.
 
-Definition itvs_semiRingOfSets := [the semiRingOfSetsType of itvs].
+HB.instance Definition _ :=
+  @isSemiRingOfSets.Build d ocitv_type (Pointed.class R) ocitv ocitv0 ocitvI ocitvD.
 
-Lemma hlength_ge0' (f : R -> R) (ndf : {homo f : x y / (x <= y)%R})
-  (I : set itvs) : (0 <= hlength f I)%E.
-Proof. by rewrite -(hlength0 f) le_hlength. Qed.
+Definition itvs_semiRingOfSets := [the semiRingOfSetsType d of ocitv_type].
+
+Variable f : R -> R.
 
-Lemma hlength_semi_additive (f : R -> R) : semi_additive (hlength f).
+Lemma hlength_semi_additive : semi_additive (hlength f : set ocitv_type -> _).
 Proof.
 move=> /= I n /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym-/funext {I}->.
 move=> Itriv [[/= a1 a2] _] /esym /[dup] + ->.
@@ -324,36 +324,52 @@ apply/andP; split=> //; apply: contraTneq xbj => ->.
 by rewrite in_itv/= le_gtF// (itvP xabi).
 Qed.
 
-Canonical hlength_measure (f : R -> R) (f_monotone : {homo f : x y / (x <= y)%R}) :
- {additive_measure set itvs -> \bar R}
-  := AdditiveMeasure (AdditiveMeasure.Axioms (hlength0 f)
-     (hlength_ge0' f_monotone) (hlength_semi_additive f)).
-
 Hint Extern 0 (measurable _) => solve [apply: is_ocitv] : core.
 
-Lemma hlength_content_sub_fsum (f : R -> R) (D : {fset nat}) a0 b0
-    (a b : nat -> R) : {homo f : x y / x <= y} ->
-    (forall i, i \in D -> a i <= b i) ->
+Lemma hlength_sigma_finite : sigma_finite [set: ocitv_type] (hlength f).
+Proof.
+exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic).
+  apply/esym; rewrite -subTset => /= x _ /=.
+  exists `|(floor `|x|%R + 1)%R|%N; rewrite //= in_itv/=.
+  rewrite !natr_absz intr_norm intrD -RfloorE.
+  suff: `|x| < `|Rfloor `|x| + 1| by rewrite ltr_norml => /andP[-> /ltW->].
+  rewrite [ltRHS]ger0_norm//.
+    by rewrite (le_lt_trans _ (lt_succ_Rfloor _))// ?ler_norm.
+  by rewrite addr_ge0// -Rfloor0 le_Rfloor.
+by move=> k; split => //; rewrite hlength_itv /= -EFinB; case: ifP; rewrite ltey.
+Qed.
+
+Hypothesis ndf : {homo f : x y / (x <= y)%R}.
+
+Lemma hlength_ge0' (I : set ocitv_type) : (0 <= hlength f I)%E.
+Proof. by rewrite -(hlength0 f) le_hlength. Qed.
+
+HB.instance Definition _ :=
+  isAdditiveMeasure.Build _ R _ (hlength f : set ocitv_type -> _)
+    hlength_ge0' hlength_semi_additive.
+
+Lemma hlength_content_sub_fsum (D : {fset nat}) a0 b0
+    (a b : nat -> R) : (forall i, i \in D -> a i <= b i) ->
     `]a0, b0] `<=` \big[setU/set0]_(i <- D) `] a i, b i]%classic ->
   f b0 - f a0 <= \sum_(i <- D) (f (b i) - f (a i)).
 Proof.
-move=> ndf Dab h; have [ab|ab] := leP a0 b0; last first.
+move=> Dab h; have [ab|ab] := leP a0 b0; last first.
   apply (@le_trans _ _ 0); first by rewrite subr_le0 ndf// ltW.
   by rewrite big_seq sumr_ge0// => i iD; rewrite subr_ge0 ndf// Dab.
 have mab k :
-  [set` D] k -> @measurable itvs_semiRingOfSets `]a k, b k]%classic by [].
+  [set` D] k -> @measurable d itvs_semiRingOfSets `]a k, b k]%classic by [].
 move: h; rewrite -bigcup_fset.
-move/(@content_sub_fsum R _ (@hlength_measure f ndf) _ [set` D]
-  `]a0, b0]%classic (fun x => `](a x), (b x)]%classic) (finite_fset D) mab
+move/(@content_sub_fsum d R _
+    [the additive_measure _ _ of hlength f : set ocitv_type -> _] _ [set` D]
+    `]a0, b0]%classic (fun x => `](a x), (b x)]%classic) (finite_fset D) mab
   (is_ocitv _ _)) => /=.
 rewrite hlength_itv_bnd// -lee_fin => /le_trans; apply.
 rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in X in (_ <= X)%E]big_seq.
 by apply: lee_sum => i iD; rewrite hlength_itv_bnd// Dab.
 Qed.
 
-Lemma hlength_sigma_sub_additive (f : R -> R)
-    (ndf : {homo f : x y / (x <= y)%R}) (rcf : right_continuous f) :
-  sigma_sub_additive (hlength f).
+Lemma hlength_sigma_sub_additive (rcf : right_continuous f) :
+  sigma_sub_additive (hlength f : set ocitv_type -> _).
 Proof.
 move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE.
 move=> [a _ <-]; rewrite hlength_itv ?lte_fin/= -EFinB => lebig.
@@ -378,35 +394,34 @@ wlog wlogh : b A AE lebig / forall n, (b n).1 <= (b n).2.
   - by move=> k; rewrite /b'; case: ifPn => //; rewrite -ltNge => /ltW.
 apply: lee_adde => e.
 rewrite [e%:num]splitr [in leRHS]EFinD addeA -lee_subl_addr//.
-apply: le_trans (epsilon_trick _ _ _) => //=; last first.
-  by move=> ?; exact: hlength_ge0'.
+apply: le_trans (epsilon_trick _ _ _) => //=.
 have [c ce] := nondecreasing_right_continuousP a.1 ndf rcf [gt0 of e%:num / 2].
-have [d de] : exists d : nat -> {posnum R}, forall i,
-    f ((b i).2 + (d i)%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1.
+have [D De] : exists D : nat -> {posnum R}, forall i,
+    f ((b i).2 + (D i)%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1.
   suff : forall i, exists di : {posnum R},
       f ((b i).2 + di%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1.
     by move/choice => -[g hg]; exists g.
   move=> k; apply nondecreasing_right_continuousP => //.
   by rewrite divr_gt0 // exprn_gt0.
-have acbd : `[ a.1 + c%:num / 2, a.2] `<=` \bigcup_i `](b i).1, (b i).2 + (d i)%:num[%classic.
+have acbd : `[ a.1 + c%:num / 2, a.2] `<=` \bigcup_i `](b i).1, (b i).2 + (D i)%:num[%classic.
   apply (@subset_trans _ `]a.1, a.2]).
     move=> r; rewrite /= !in_itv/= => /andP [+ ->].
     by rewrite andbT; apply: lt_le_trans; rewrite ltr_addl.
   apply (subset_trans lebig) => r [n _ Anr]; exists n => //.
   move: Anr; rewrite AE /= !in_itv/= => /andP [->]/= /le_lt_trans.
   by apply; rewrite ltr_addl.
 have := @segment_compact _ (a.1 + c%:num / 2) a.2; rewrite compact_cover.
-have obd k : [set: nat] k-> open `](b k).1, ((b k).2 + (d k)%:num)[%classic.
+have obd k : [set: nat] k-> open `](b k).1, ((b k).2 + (D k)%:num)[%classic.
   by move=> _; exact: interval_open.
 move=> /(_ _ _ _ obd acbd){obd acbd}.
 case=> X _ acXbd.
 rewrite -EFinD.
 apply: (@le_trans _ _ (\sum_(i <- X) (hlength f `](b i).1, (b i).2]%classic) +
-                       \sum_(i <- X) (f ((b i).2 + (d i)%:num)%R - f (b i).2)%:E)%E).
+                       \sum_(i <- X) (f ((b i).2 + (D i)%:num)%R - f (b i).2)%:E)%E).
   apply: (@le_trans _ _ (f a.2 - f (a.1 + c%:num / 2))%:E).
     rewrite lee_fin -addrA -opprD ler_sub// (le_trans _ ce)// ndf//.
     by rewrite ler_add2l ler_pdivr_mulr// ler_pmulr// ler1n.
-  apply: (@le_trans _ _ (\sum_(i <- X) (f ((b i).2 + (d i)%:num) - f (b i).1)%:E)%E).
+  apply: (@le_trans _ _ (\sum_(i <- X) (f ((b i).2 + (D i)%:num) - f (b i).1)%:E)%E).
     rewrite sumEFin lee_fin hlength_content_sub_fsum//.
       by move=> k kX; rewrite (@le_trans _ _ (b k).2)// ler_addl.
     apply: subset_trans.
@@ -419,28 +434,62 @@ rewrite -big_split/= nneseries_esum//; last first.
   by move=> k _; rewrite adde_ge0// hlength_ge0'.
 rewrite esum_ge//; exists X => //.
 rewrite big_seq [in X in (_ <= X)%E]big_seq; apply: lee_sum => k kX.
-by rewrite AE lee_add2l// lee_fin ler_subl_addl natrX de.
+by rewrite AE lee_add2l// lee_fin ler_subl_addl natrX De.
 Qed.
 
-Lemma hlength_sigma_finite (f : R -> R) : sigma_finite [set: itvs] (hlength f).
+Let gitvs := [the measurableType _ of salgebraType ocitv].
+
+Definition lebesgue_stieltjes_measure :=
+  Hahn_ext [the additive_measure _ _ of hlength f : set ocitv_type -> _ ].
+
+End itv_semiRingOfSets.
+Arguments lebesgue_stieltjes_measure {R}.
+
+Section lebesgue_stieltjes_measure_itv.
+Variables (d : measure_display) (R : realType) (f : R -> R).
+Hypotheses (ndf : {homo f : x y / x <= y}) (rcf : right_continuous f).
+
+Let m := lebesgue_stieltjes_measure d f ndf.
+
+Let g : \bar R -> \bar R := EFinf f.
+
+Let lebesgue_stieltjes_measure_itvoc (a b : R) :
+  (m `]a, b] = hlength f `]a, b])%classic.
 Proof.
-exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic).
-  apply/esym; rewrite -subTset => /= x _ /=.
-  exists `|(floor `|x|%R + 1)%R|%N; rewrite //= in_itv/=.
-  rewrite !natr_absz intr_norm intrD -RfloorE.
-  suff: `|x| < `|Rfloor `|x| + 1| by rewrite ltr_norml => /andP[-> /ltW->].
-  rewrite [ltRHS]ger0_norm//.
-    by rewrite (le_lt_trans _ (lt_succ_Rfloor _))// ?ler_norm.
-  by rewrite addr_ge0// -Rfloor0 le_Rfloor.
-by move=> k; split => //; rewrite hlength_itv/= -EFinB; case: ifP; rewrite ltey.
+rewrite /m /lebesgue_stieltjes_measure /= /Hahn_ext measurable_mu_extE//; last first.
+  by exists (a, b).
+exact: hlength_sigma_sub_additive.
 Qed.
 
-Let gitvs := g_measurableType ocitv.
+Lemma set1Ebigcap (x : R) : [set x] = \bigcap_k `](x - k.+1%:R^-1)%R, x]%classic.
+Proof.
+apply/seteqP; split => [_ -> k _ /=|].
+  by rewrite in_itv/= lexx andbT ltr_subl_addl ltr_addr invr_gt0.
+move=> y h; apply/eqP/negPn/negP => yx.
+red in h.
+simpl in h.
+Admitted.
+
+Let lebesgue_stieltjes_measure_set1 (a : R) :
+  m [set a] = ((f a)%:E - (lim (f @ at_left a))%:E)%E.
+Proof.
+rewrite (set1Ebigcap a).
+Admitted.
 
-Definition lebesgue_stieltjes_measure (f : R -> R)
-    (ndf : {homo f : x y / x <= y}) (rcf : right_continuous f)
-  : {measure set gitvs -> \bar R} :=
-  @Hahn_ext_measure R _ (hlength_measure ndf) (hlength_sigma_sub_additive ndf rcf).
+Let lebesgue_stieltjes_measure_itvoo (a b : R) : a <= b ->
+  m `]a, b[%classic = ((lim (f @ at_left b))%:E - (f a)%:E)%E.
+Proof.
+Admitted.
 
-End itv_semiRingOfSets.
-Arguments lebesgue_stieltjes_measure {R}.
+Let lebesgue_stieltjes_measure_itvcc (a b : R) : a <= b ->
+  m `[a, b]%classic = ((f b)%:E - (lim (f @ at_left a))%:E)%E.
+Proof.
+Admitted.
+
+Let lebesgue_stieltjes_measure_itvco (a b : R) : a <= b ->
+  m `[a, b[%classic = ((lim (f @ at_left b))%:E - (lim (f @ at_left a))%:E)%E.
+Proof.
+Admitted.
+
+
+End lebesgue_stieltjes_measure_itv.