Module mathcomp.analysis.lebesgue_stieltjes_measure

From HB Require Import structures.
From mathcomp Require Import boot order finmap ssralg ssrnum ssrint interval.
From mathcomp Require Import archimedean.
#[warning="-warn-library-file-internal-analysis"]
From mathcomp Require Import unstable.
From mathcomp Require Import boolp classical_sets functions fsbigop cardinality.
From mathcomp Require Import reals ereal interval_inference topology numfun.
From mathcomp Require Import normedtype sequences esum real_interval measure.
From mathcomp Require Import realfun.

# Lebesgue Stieltjes Measure This file contains a formalization of the Lebesgue-Stieltjes measure using the Measure Extension theorem from `measure_theory`. References: - Achim Klenke. Probability Theory 2nd edition. 2014 - Y. Ishiguro, R. Affeldt. The Radon-Nikodym Theorem and the Lebesgue- Stieltjes measure in Coq. Computer Software 41(2).2024 ``` right_continuous f == the function f is right-continuous cumulative R == type of non-decreasing, right-continuous functions (with R : numFieldType) The HB class is Cumulative. instance: idfun cumulativeBounded R l r == type of cumulative functions f such that f @ -oo --> l and f @ +oo --> r The HB class is CumulativeBounded. ``` The modules RGenOInfty, RGenInftyO, RGenCInfty, RGenOpens, ROpenSets provide proofs of equivalence between the sigma-algebra generated by open-closed intervals and the sigma-algebras generated by open rays, closed rays, open intervals, and open sets. We distinguish in particular the sigma-algebras generated by ocitv and and open sets for which we introduce the following definitions/notations: ``` ocitv_type R == alias for R : realType ocitv == set of open-closed intervals ]x, y] where x and y are real numbers R.-ocitv == display for ocitv_type R R.-ocitv.-measurable == semiring of sets of open-closed intervals open_type R == alias for R : realType R.-open := sigma_display (@open R) R.-open.-measurable == sigma-algebra generated by open sets ``` The modules `MeasurableRocitv` and `MeasurableRopen` contains resp. the sigma-algebras generated from ocitv and open sets. They contain similar definitions: ``` measurableTypeR R == measurableType generated by R.-ocitv or R.-open @lebesgue_display R == (measure_)display for the sigma-algebra generated by R.-ocitv or R.-open @measurableR R == measurable sets generated by R.-ocitv or R.-open ``` The module `MeasurableR` contains the default sigma-algebra, which is `MeasurableRopen`. The latter contains in addition: ``` ocitv_measure mu == measure over the sigma-algebra generated by open sets built out of mu, the same measure over the sigma-algebra generated by ocitv ``` The last part of the file contains the construction of the Lebesgue- Stieltjes measure: ``` wlength f A := f b - f a with the hull of the set of real numbers A being delimited by a and b ocitv_lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f f is a cumulative function. The sigma algebra is generated from ocitv. lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f f is a cumulative function. The sigma algebra is generated from open sets. completed_lebesgue_stieltjes_measure f == the completed Lebesgue-Stieltjes measure ```

Unset SsrOldRewriteGoalsOrder.
Set Implicit Arguments.
Unset Strict Implicit.
Unset Printing Implicit Defensive.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Import numFieldTopology.Exports.

Local Open Scope classical_set_scope.
Local Open Scope ring_scope.

Reserved Notation "R .-ocitv" (at level 1, format "R .-ocitv").
Reserved Notation "R .-ocitv.-measurable"
(at level 2, format "R .-ocitv.-measurable").
Reserved Notation "R .-open" (at level 1, format "R .-open").
Reserved Notation "R .-open.-measurable"
(at level 2, format "R .-open.-measurable").

Notation f :=
(forall , f%function @ at_right x --> f%function x).

Lemma ( : numFieldType) {} ( : orderNbhsType d)
( : R -> U) : continuous f -> right_continuous f.

Proof.

by move=> cf x; apply: cvg_within_filter; exact/cf. Qed.

. () {d} (U : orderNbhsType d)
  (f : R -> U) := {
  cumulative_is_nondecreasing : nondecreasing f ;
  cumulative_is_right_continuous : right_continuous f }.

()
.
  () {d} (U : orderNbhsType d) := { of isCumulative R d U f }.

Arguments cumulative_is_nondecreasing {R d U} _.
Arguments cumulative_is_right_continuous {R d U} _.

Lemma ( : realFieldType) ( : R) ( : R)
    ( : cumulative R R) :
  e > 0 -> exists : {posnum R}, f (a + d%:num) <= f a + e.

Proof.

move=> e0; move: (cumulative_is_right_continuous f).
move=> /(_ a) /(@cvgr_dist_lt _ R^o) /(_ _ e0)[] _ /posnumP[d] => h.
exists (PosNum [gt0 of (d%:num / 2)]) => //=.
move: h => /(_ (a + d%:num / 2)) /=.
rewrite opprD addNKr normrN ger0_norm// ltr_pdivrMr// ltr_pMr// 2!ltrDl.
rewrite ltr01 divr_gt0// => /(_ erefl erefl).
rewrite ler0_norm.
by rewrite subr_le0 (cumulative_is_nondecreasing f)// lerDl.
by rewrite opprB ltrBlDl; exact: ltW.
Qed.

Section id_is_cumulative.
Context { : realFieldType}.

Let : {homo @idfun R : / x <= y}.

Proof.

by []. Qed.

Let : right_continuous (@idfun R).

Proof.

by apply/right_continuousW => x; exact: cvg_id. Qed.

..Build R _ R idfun id_nd id_rc.
End id_is_cumulative.

. () (l r : R) (f : R -> R) := {
  cumulativeNy : f @ -oo --> l ;
  cumulativey : f @ +oo --> r }.

()
. () (l r : R) :=
  { of isCumulativeBounded R l r f & Cumulative R f}.

Arguments cumulativeNy {R l r} s.
Arguments cumulativey {R l r} s.

Section itv_semiRingOfSets.
Context ( : realType).
Implicit Types (I J K : set R).
Definition : Type := R.

Definition := [set `]x.1, x.2]%classic | in [set: R * R]].

Lemma : ocitv `]a, b]%classic.

Proof.

by exists (a, b); split => //=; rewrite in_itv/= andbT. Qed.

Hint Extern 0 (ocitv _) => solve [apply: is_ocitv] : core.

Lemma : ocitv set0.

Proof.

by exists (1, 0); rewrite //= set_itv_ge ?bnd_simp//= ltr10. Qed.

Hint Resolve ocitv0 : core.

Lemma : ocitv X <-> X = set0 \/ exists2 , x.1 < x.2 & X = `]x.1, x.2]%classic.

Proof.

split=> [[x _ <-]|[->//|[x xlt ->]]]//.
case: (boolP (x.1 < x.2)) => x12; first by right; exists x.
by left; rewrite set_itv_ge.
Qed.

Lemma : semi_setD_closed ocitv.

Proof.

move=> _ _ [a _ <-] /ocitvP[|[b ltb]] ->.
  rewrite setD0; exists [set `]a.1, a.2]%classic].
  by split=> [//|? ->//||? ? -> ->//]; rewrite bigcup_set1.
rewrite setDE setCitv/= setIUr -!set_itvI.
rewrite /Order.meet/= /Order.meet/= /Order.join/=
         ?(andbF, orbF)/= ?(meetEtotal, joinEtotal).
rewrite -negb_or le_total/=; set c := minr _ _; set d := maxr _ _.
have inside : a.1 < c -> d < a.2 -> `]a.1, c] `&` `]d, a.2] = set0.
  rewrite -subset0 lt_min gt_max => /andP[a12 ab1] /andP[_ ba2] x /= [].
  have b1a2 : b.1 <= a.2 by rewrite ltW// (lt_trans ltb).
  have a1b2 : a.1 <= b.2 by rewrite ltW// (lt_trans _ ltb).
  rewrite /c /d (min_idPr _)// (max_idPr _)// !in_itv /=.
  move=> /andP[a1x xb1] /andP[b2x xa2].
  by have := lt_le_trans b2x xb1; case: ltgtP ltb.
exists ((if a.1 < c then [set `]a.1, c]%classic] else set0) `|`
        (if d < a.2 then [set `]d, a.2]%classic] else set0)); split.
- by rewrite finite_setU; do! case: ifP.
- by move=> ? []; case: ifP => ? // ->//=.
- by rewrite bigcup_setU; congr (_ `|` _);
     case: ifPn => ?; rewrite ?bigcup_set1 ?bigcup_set0// set_itv_ge.
- move=> I J/=; case: ifP => //= ac; case: ifP => //= da [] // -> []// ->.
    by rewrite inside// => -[].
  by rewrite setIC inside// => -[].
Qed.

Lemma : setI_closed ocitv.

Proof.

move=> _ _ [a _ <-] [b _ <-]; rewrite -set_itvI/=.
rewrite /Order.meet/= /Order.meet /Order.join/=
?(andbF, orbF)/= ?(meetEtotal, joinEtotal).
by rewrite -negb_or le_total/=.
Qed.

Definition : Type -> measure_display

Proof.

exact. Qed.

..on ocitv_type.
.
  .Build (ocitv_display R)
    ocitv_type ocitv ocitv0 ocitvI ocitvD.

End itv_semiRingOfSets.

Notation := (ocitv_display R) : measure_display_scope.
Notation := (measurable : set_system (ocitv_type R)) :
  classical_set_scope.

Module .
Section measurableRocitv.
Context { : realType}.

Definition := g_sigma_algebraType (@ocitv R).

Definition : measure_display := (@ocitv R).-sigma.

Definition : set_system R := (@ocitv R).-sigma.-measurable.

. lebesgue_display measurableTypeR :=
   Measurable.on measurableTypeR.

..copy R measurableTypeR.

Lemma ( : R) : measurable [set r].

Proof.

rewrite set1_bigcap_oc; apply: bigcap_measurable => // k _.
by apply: sub_sigma_algebra; exact/is_ocitv.
Qed.

#[local] Hint Resolve measurable_set1 : core.

Lemma ( : interval R) : measurable [set` i].

Proof.

have moc ( : R) : measurable `]a, b].
  by apply: sub_sigma_algebra; apply: is_ocitv.
have mopoo ( : R) : measurable `]x, +oo[.
  by rewrite itv_bndy_bigcup_BRight; exact: bigcup_measurable.
have mnooc ( : R) : measurable `]-oo, x].
  by rewrite -setCitvr; exact/measurableC.
have ooE ( : R) : `]a, b[%classic = `]a, b] `\ b.
  by rewrite setDitv1r.
have moo ( : R) : measurable `]a, b[ by rewrite ooE; exact: measurableD.
have mcc ( : R) : measurable `[a, b].
  case: (boolP (a <= b)) => ab; last by rewrite set_itv_ge.
  by rewrite -setU_1itvob//; apply/measurableU.
have mco ( : R) : measurable `[a, b[.
  case: (boolP (a < b)) => ab; last by rewrite set_itv_ge.
  by rewrite -setU_1itvob//; apply/measurableU.
have oooE ( : R) : `]-oo, b[%classic = `]-oo, b] `\ b.
  by rewrite setDitv1r.
case: i => [[[] a|[]] [[] b|[]]] => //; do ?by rewrite set_itv_ge.
- by rewrite -setU_1itvob//; exact/measurableU.
- by rewrite oooE; exact/measurableD.
- by rewrite set_itvNyy.
Qed.

End measurableRocitv.
Arguments measurableTypeR : clear implicits.
#[global]
Hint Extern 0 (measurable (_ @^-1` [set _])) =>
solve [apply: measurable_funPTI; exact: measurable_set1] : core.
#[global]
Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core.
#[global]
Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core.
End MeasurableRocitv.

Module .
Section rgenoinfty.
Context ( : realType).
Implicit Types x y z : R.

Definition := [set | exists , A = `]x, +oo[%classic].

Lemma :
G.-sigma.-measurable [set` Interval (BSide b x) +oo%O].

Proof.

case: b; last by apply: sub_sigma_algebra; eexists; reflexivity.
rewrite itvcyEbigcap; apply: bigcapT_measurable => k.
by apply: sub_sigma_algebra; eexists; reflexivity.
Qed.

Lemma : a != +oo%O ->
G.-sigma.-measurable [set` Interval a (BSide b x)].

Proof.

case: a => [a r _|[_|//]].
by rewrite set_itv_splitD; apply: measurableD => //;
exact: measurable_itv_bnd_infty.
by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty.
Qed.

Lemma : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable.

Proof.

rewrite eqEsubset; split => A.
apply: smallest_sub; first exact: smallest_sigma_algebra.
by move=> I [x _ <-]; exact: measurable_itv_bounded.
by apply: smallest_sub; [exact: smallest_sigma_algebra|move=> A' /= [x ->]].
Qed.

End rgenoinfty.
End RGenOInfty.

Module .
Section rgeninftyo.
Context ( : realType).
Implicit Types x y z : R.

Definition := [set | exists , A = `]-oo, x[%classic].

Lemma :
G.-sigma.-measurable [set` Interval -oo%O (BSide b x)].

Proof.

case: b; first by apply sub_sigma_algebra; eexists; reflexivity.
rewrite -setCitvr itvoyEbigcup; apply/measurableC/bigcupT_measurable => n.
rewrite -setCitvl; apply: measurableC.
by apply: sub_sigma_algebra; eexists; reflexivity.
Qed.

Lemma : a != -oo%O ->
G.-sigma.-measurable [set` Interval (BSide b x) a].

Proof.

case: a => [a r _|[//|_]].
by rewrite set_itv_splitD; apply/measurableD => //;
rewrite -setCitvl; apply: measurableC; exact: measurable_itv_bnd_infty.
by rewrite -setCitvl; apply: measurableC; exact: measurable_itv_bnd_infty.
Qed.

Lemma : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable.

Proof.

End rgeninftyo.
End RGenInftyO.

Module .
Section rgencinfty.
Context ( : realType).
Implicit Types x y z : R.

Definition : set_system R := [set | exists , A = `[x, +oo[%classic].

Lemma :
G.-sigma.-measurable [set` Interval (BSide b x) +oo%O].

Proof.

case: b; first by apply: sub_sigma_algebra; exists x; rewrite set_itvcy.
rewrite itvoyEbigcup; apply: bigcupT_measurable => k.
by apply: sub_sigma_algebra; eexists; reflexivity.
Qed.

Lemma : a != +oo%O ->
G.-sigma.-measurable [set` Interval a (BSide b y)].

Proof.

case: a => [a r _|[_|//]].
rewrite set_itv_splitD.
by apply: measurableD; exact: measurable_itv_bnd_infty.
by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty.
Qed.

Lemma : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable.

Proof.

End rgencinfty.
End RGenCInfty.

Module .
Section rgenopens.
Context ( : realType).
Implicit Types x y z : R.

Definition := [set | exists , A = `]x, y[%classic].

Local Lemma : G.-sigma.-measurable `]x, y[%classic.

Proof.

by apply sub_sigma_algebra; eexists; eexists; reflexivity. Qed.

Local Lemma : G.-sigma.-measurable `]x, +oo[%classic.

Proof.

rewrite itvbndyEbigcup; apply: bigcupT_measurable => i.
exact: measurable_itvoo.
Qed.

Lemma :
G.-sigma.-measurable [set` Interval (BSide b x) +oo%O].

Proof.

case: b; last exact: measurable_itv_o_infty.
rewrite itvcyEbigcap; apply: bigcapT_measurable => k.
exact: measurable_itv_o_infty.
Qed.

Lemma :
G.-sigma.-measurable [set` Interval -oo%O (BSide b x)].

Proof.

by rewrite -setCitvr; apply: measurableC; exact: measurable_itv_bnd_infty.
Qed.

Lemma :
G.-sigma.-measurable [set` Interval (BSide a x) (BSide b y)].

Proof.

move: a b => [] []; rewrite -[X in measurable X]setCK setCitv;
apply: measurableC; apply: measurableU; try solve[
exact: measurable_itv_infty_bnd|exact: measurable_itv_bnd_infty].
Qed.

Lemma : (@ocitv R).-sigma.-measurable = G.-sigma.-measurable.

Proof.

End rgenopens.
End RGenOpens.

Module .
Section rgenopensets.
Context ( : realType).
Implicit Types a b : R.
Import MeasurableRocitv.

Lemma : (@ocitv R).-sigma.-measurable = open.-sigma.-measurable.

Proof.

rewrite eqEsubset; split; [rewrite RGenOpens.measurableE|];
  apply: sigma_algebra_subl=> U.
- by rewrite /RGenOpens.G/= => -[a [b ->]]; exact: sub_sigma_algebra.
- move=> oU; rewrite (open_disjoint_itv_bigcup oU).
  apply: sigma_algebra_bigcup => k.
  have /is_intervalP -> := @open_disjoint_itv_is_interval _ U oU k.
  exact: measurable_itv.
Qed.

End rgenopensets.
End RGenOpenSets.

Section open.
Context { : realType}.

Definition : Type := R.

..on open_type.

Let : set_system R := @measurable _ (g_sigma_algebraType (@open R)).

Let : measurable set0

Proof.

exact: measurable0. Qed.

Let : measurable A -> measurable (~` A).

Proof.

by move=> /measurableC. Qed.

Let ( : (set R)^nat) : (forall , measurable (F i)) ->
measurable (\bigcup_ (F i)).

Proof.

move=> mF; exact: bigcupT_measurable. Qed.

.
  .Build (sigma_display (@open R))
    open_type measurable measurable0 measurableC measurable_bigcup.

End open.

Notation := (sigma_display (@open R)) : measure_display_scope.
Notation := (measurable : set_system (@open_type R)) :
  classical_set_scope.

Module .
Section measurableRopen.
Context { : realType}.

Definition := g_sigma_algebraType (@open R).

Definition : measure_display := R.-open.

Definition : set_system R := R.-open.-measurable.

. lebesgue_display measurableTypeR :=
   Measurable.on measurableTypeR.

..copy R measurableTypeR.

Lemma ( : R) : measurable [set r].

Proof.

rewrite set1_bigcap_oo; apply: bigcap_measurable => // k _.
exact: sub_sigma_algebra.
Qed.

#[local] Hint Resolve measurable_set1 : core.

Lemma ( : interval R) : measurable [set` i].

Proof.

have := MeasurableRocitv.measurable_itv i.
rewrite /MeasurableRocitv.lebesgue_display.
by rewrite RGenOpenSets.measurableE.
Qed.

End measurableRopen.
Arguments measurableTypeR : clear implicits.
#[global]
Hint Extern 0 (measurable (_ @^-1` [set _])) =>
  solve [apply: measurable_funPTI; exact: measurable_set1] : core.
#[global]
Hint Extern 0 (measurable [set _]) => solve [apply: measurable_set1] : core.
#[global]
Hint Extern 0 (measurable [set` _] ) => exact: measurable_itv : core.

Lemma {} { : measurableType d} { : realType}
   ( : {mfun aT >-> rT}) ( : rT) :
  measurable D -> measurable (D `&` f @^-1` [set y]).

Proof.

by move=> /(measurable_funP f); exact. Qed.

#[deprecated(since="mathcomp-analysis 1.13.0", use=measurable_funP1)]
Notation := measurable_funP1 (only parsing).
#[global] Hint Extern 0 (measurable (_ `&` _ @^-1` [set _])) =>
solve [apply: measurable_funP1; assumption] : core.

Section ocitv_measure.
Context { : realType} ( : measure (measurableTypeR R) R).

Definition : set (MeasurableRocitv.measurableTypeR R) -> \bar R :=
mu.

Let : ocitv_measure set0 = 0.

Proof.

by rewrite /ocitv_measure measure0. Qed.

Let : (0 <= ocitv_measure x)%E.

Proof.

by rewrite /ocitv_measure measure_ge0. Qed.

Let : semi_sigma_additive ocitv_measure.

Proof.

move=> F H1 H2 H3; apply: measure_semi_sigma_additive => //.
- move=> i; apply: H1; split => //=; first exact: sigma_algebra_measurable.
by rewrite -RGenOpenSets.measurableE; exact: sub_sigma_algebra.
- by rewrite -RGenOpenSets.measurableE.
Qed.

..Build _ _ _ ocitv_measure
measure0 measure_ge0 measure_semi_sigma_additive.

Lemma : ocitv_measure A = mu A

Proof.

by []. Qed.

End ocitv_measure.

End MeasurableRopen.

Module .
Export MeasurableRopen.
End MeasurableR.

The construction of the Lebesgue-Stieltjes measure actually starts here.

Section wlength.
Context { : realType} ( : R -> R).
Import MeasurableR.
Local Open Scope ereal_scope.
Implicit Types i j : interval R.

Let : \bar R -> \bar R := er_map f.

Definition ( : set (ocitv_type R)) : \bar R :=
let := Rhull A in g i.2 - g i.1.

Lemma : wlength (set0 : set R) = 0.

Proof.

by rewrite /wlength Rhull0 /= subee. Qed.

Lemma ( : R) : wlength `[r, r] = 0.

Proof.

rewrite /wlength /= asboolT// sup_itvcc//= asboolT//.
by rewrite asboolT inf_itvcc//= ?subee// inE.
Qed.

Lemma : wlength setT = +oo%E :> \bar R.

Proof.

by rewrite /wlength RhullT. Qed.

Lemma : wlength [set` i] = if i.2 > i.1 then g i.2 - g i.1 else 0.

Proof.

case: ltP => [/lt_ereal_bnd/neitvP i12|]; first by rewrite /wlength set_itvK.
rewrite le_eqVlt => /orP[|/lt_ereal_bnd i12]; last first.
  rewrite -wlength0; congr (wlength _).
  by apply/eqP/negPn; rewrite -/(neitv _) neitvE -leNgt (ltW i12).
case: i => -[ba a|[|]] [bb b|[|]] //=.
- rewrite /= => /eqP[->{b}]; move: ba bb => -[] []; try
    by rewrite set_itvE wlength0.
  by rewrite wlength_singleton.
- by move=> _; rewrite set_itvE wlength0.
- by move=> _; rewrite set_itvE wlength0.
Qed.

Lemma : neitv i -> wlength [set` i] < +oo ->
((i.1 : \bar R) \is a fin_num) /\ ((i.2 : \bar R) \is a fin_num).

Proof.

move: i => [[ba a|[]] [bb b|[]]] /neitvP //=; do ?by rewrite ?set_itvE ?eqxx.
by move=> _; rewrite wlength_itv /= ltry.
by move=> _; rewrite wlength_itv /= ltNye.
by move=> _; rewrite wlength_itv.
Qed.

Lemma : neitv i -> wlength [set` i] < +oo ->
wlength [set` i] = (fine (g i.2))%:E - (fine (g i.1))%:E.

Proof.

move=> i0 ioo; have [i1f i2f] := wlength_finite_fin_num i0 ioo.
rewrite fineK.
  by rewrite /g; move: i2f; case: (ereal_of_itv_bound i.2).
rewrite fineK.
  by rewrite /g; move: i1f; case: (ereal_of_itv_bound i.1).
rewrite wlength_itv; case: ifPn => //; rewrite -leNgt le_eqVlt => /predU1P[->|].
  by rewrite subee// /g; move: i1f; case: (ereal_of_itv_bound i.1).
by move/lt_ereal_bnd/ltW; rewrite leNgt; move: i0 => /neitvP => ->.
Qed.

Lemma ( : R) ( : bool) : (a <= b)%R ->
wlength [set` Interval (BSide x a) (BSide y b)] = (f b - f a)%:E.

Proof.

move=> ab; rewrite wlength_itv/= lte_fin lt_neqAle ab andbT.
by have [-> /=|/= ab'] := eqVneq a b; rewrite ?subrr// EFinN EFinB.
Qed.

Lemma :
wlength [set` Interval -oo%O (BSide b r)] = +oo :> \bar R.

Proof.

by rewrite wlength_itv /= ltNye. Qed.

Lemma :
wlength [set` Interval (BSide b r) +oo%O] = +oo :> \bar R.

Proof.

by rewrite wlength_itv /= ltey. Qed.

Lemma : wlength [set` i] = +oo ->
(exists , i = Interval -oo%O (BSide s r) \/ i = Interval (BSide s r) +oo%O)
\/ i = `]-oo, +oo[.

Proof.

rewrite wlength_itv; case: i => -[ba a|[]] [bb b|[]] //= => [|_|_|].
- by case: ifPn.
- by left; exists ba, a; right.
- by left; exists bb, b; left.
- by right.
Qed.

Lemma ( : {homo f : / (x <= y)%R}) :
0 <= wlength [set` i].

Proof.

rewrite wlength_itv; case: ifPn => //; case: (i.1 : \bar _) => [r| |].
- by rewrite suber_ge0// => /ltW /(le_er_map ndf).
- by rewrite ltNge leey.
- case: (i.2 : \bar _) => //=; last by rewrite leey.
by move=> r _; rewrite leey.
Qed.

Lemma ( : set R) : wlength [set` Rhull A] = wlength A.

Proof.

by rewrite /wlength Rhull_involutive. Qed.

Lemma ( : {homo f : / (x <= y)%R}) :
{subset i <= j} -> wlength [set` i] <= wlength [set` j].

Proof.

set I := [set` i]; set J := [set` j].
have [->|/set0P I0] := eqVneq I set0; first by rewrite wlength0 wlength_itv_ge0.
have [J0|/set0P J0] := eqVneq J set0.
  by move/subset_itvP; rewrite -/J J0 subset0 -/I => ->.
move=> /subset_itvP ij; apply: leeB => /=.
  have [ui|ui] := asboolP (has_ubound I).
    have [uj /=|uj] := asboolP (has_ubound J); last by rewrite leey.
    by rewrite lee_fin ndf// supS.
  have [uj /=|//] := asboolP (has_ubound J).
  by move: ui; have := subset_has_ubound ij uj.
have [lj /=|lj] := asboolP (has_lbound J); last by rewrite leNye.
have [li /=|li] := asboolP (has_lbound I); last first.
  by move: li; have := subset_has_lbound ij lj.
by rewrite lee_fin; exact/ndf/infS.
Qed.

Lemma ( : {homo f : / (x <= y)%R}) :
{homo wlength : / A `<=` B >-> A <= B}.

Proof.

move=> a b /le_Rhull /(le_wlength_itv ndf).
by rewrite (wlength_Rhull a) (wlength_Rhull b).
Qed.

End wlength.

Section wlength_extension.
Context { : realType}.

Lemma ( : R -> R) :
measure_function.semi_additive (wlength f).

Proof.

move=> /= I n /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym-/funext {I}->.
move=> Itriv [[/= a1 a2] _] /esym /[dup] + ->.
rewrite wlength_itv ?lte_fin/= -EFinB.
case: ifPn => a12; last first.
  pose I := `](b i).1, (b i).2]%classic.
  rewrite set_itv_ge//= -(bigcup_mkord _ I) /I => /bigcup0P I0.
  by under eq_bigr => i _ do rewrite I0//= wlength0; rewrite big1.
set A := `]a1, a2]%classic.
rewrite -bigcup_pred; set P := xpredT; rewrite (eq_bigl P)//.
move: P => P; have [p] := ubnP #|P|; elim: p => // p IHp in P a2 a12 A *.
rewrite ltnS => cP /esym AE.
have : A a2 by rewrite /A /= in_itv/= lexx andbT.
rewrite AE/= => -[i /= Pi] a2bi.
case: (boolP ((b i).1 < (b i).2)) => bi; last by rewrite itv_ge in a2bi.
have {}a2bi : a2 = (b i).2.
  apply/eqP; rewrite eq_le (itvP a2bi)/=.
  suff: A (b i).2 by move=> /itvP->.
  by rewrite AE; exists i=> //=; rewrite in_itv/= lexx andbT.
rewrite {a2}a2bi in a12 A AE *.
rewrite (bigD1 i)//= wlength_itv ?lte_fin/= bi !EFinD -addeA.
congr (_ + _)%E; apply/eqP; rewrite addeC -sube_eq// 1?adde_defC//.
rewrite ?EFinN oppeK addeC; apply/eqP.
have [a1bi|a1bi] := eqVneq a1 (b i).1.
  rewrite {a1}a1bi in a12 A AE {IHp} *; rewrite subee ?big1// => j.
  move=> /andP[Pj Nji]; rewrite wlength_itv ?lte_fin/=; case: ifPn => bj//.
  exfalso; have /trivIsetP/(_ j i I I Nji) := Itriv.
  pose m := ((b j).1 + (b j).2) / 2%:R.
  have mbj : `](b j).1, (b j).2]%classic m.
     by rewrite /= !in_itv/= ?(midf_lt, midf_le)//= ltW.
  rewrite -subset0 => /(_ m); apply; split=> //.
  by suff: A m by []; rewrite AE; exists j.
have a1b2 j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).2.
  move=> Pj bj; suff /itvP-> : A (b j).2 by [].
  by rewrite AE; exists j => //=; rewrite ?in_itv/= bj/=.
have a1b j : P j -> (b j).1 < (b j).2 -> a1 <= (b j).1.
  move=> Pj bj; case: ltP=> // bj1a.
  suff : A a1 by rewrite /A/= in_itv/= ltxx.
  by rewrite AE; exists j; rewrite //= in_itv/= bj1a//= a1b2.
have bbi2 j : P j -> (b j).1 < (b j).2 -> (b j).2 <= (b i).2.
  move=> Pj bj; suff /itvP-> : A (b j).2 by [].
  by rewrite AE; exists j => //=; rewrite ?in_itv/= bj/=.
apply/IHp.
- by rewrite lt_neqAle a1bi/= a1b.
- rewrite (leq_trans _ cP)// -(cardID (pred1 i) P).
  rewrite [X in (_ < X + _)%N](@eq_card _ _ (pred1 i)).
    by move=> j; rewrite !inE andbC; case: eqVneq => // ->.
  rewrite ?card1 ?ltnS// subset_leq_card//.
  by apply/fintype.subsetP => j; rewrite -topredE/= !inE andbC.
apply/seteqP; split=> /= [x [j/= /andP[Pj Nji]]|x/= xabi].
  case: (boolP ((b j).1 < (b j).2)) => bj; last by rewrite itv_ge.
  apply: subitvP; rewrite subitvE ?bnd_simp a1b//= leNgt.
  have /trivIsetP/(_ j i I I Nji) := Itriv.
  rewrite -subset0 => /(_ (b j).2); apply: contra_notN => /= bi1j2.
  by rewrite !in_itv/= bj !lexx bi1j2 bbi2.
have: A x.
  rewrite /A/= in_itv/= (itvP xabi)/= ltW//.
  by rewrite (le_lt_trans _ bi) ?(itvP xabi).
rewrite AE => -[j /= Pj xbj].
exists j => //=.
apply/andP; split=> //; apply: contraTneq xbj => ->.
by rewrite in_itv/= le_gtF// (itvP xabi).
Qed.

Lemma ( : cumulative R R) ( : set (ocitv_type R)) :
(0 <= wlength f I)%E.

Proof.

by rewrite -(wlength0 f) le_wlength//; exact: cumulative_is_nondecreasing.
Qed.

#[local] Hint Extern 0 (0%:E <= wlength _ _) => solve[apply: wlength_ge0] : core.

. ( R R) :=
  isContent.Build _ _ R (wlength f)
    (wlength_ge0 f)
    (wlength_semi_additive f).

Hint Extern 0 (measurable _) => solve [apply: is_ocitv] : core.

Lemma ( : cumulative R R) ( : {fset nat})
    ( : nat -> R) : (forall , i \in D -> a i <= b i) ->
    `]a0, b0] `<=` \big[setU/set0]_( <- D) `]a i, b i]%classic ->
  f b0 - f a0 <= \sum_( <- D) (f (b i) - f (a i)).

Proof.

move=> Dab h; have [ab|ab] := leP a0 b0; last first.
  apply (@le_trans _ _ 0).
    by rewrite subr_le0 cumulative_is_nondecreasing// ltW.
  rewrite big_seq sumr_ge0// => i iD.
  by rewrite subr_ge0 cumulative_is_nondecreasing// Dab.
have mab k : [set` D] k -> R.-ocitv.-measurable `]a k, b k]%classic by [].
move: h; rewrite -bigcup_fset.
move/(content_sub_fsum (wlength f) (finite_fset D) mab (is_ocitv a0 b0)) => /=.
rewrite wlength_itv_bnd// -lee_fin => /le_trans; apply.
rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in leRHS]big_seq.
by apply: lee_sum => i iD; rewrite wlength_itv_bnd// Dab.
Qed.

Lemma ( : cumulative R R) :
measurable_subset_sigma_subadditive (wlength f).

Proof.

move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE => -[a _ <-].
rewrite /subset_sigma_subadditive wlength_itv ?lte_fin/= -EFinB => lebig.
case: ifPn => a12; last by rewrite nneseries_esum ?esum_ge0.
wlog wlogh : b A AE lebig / forall , (b n).1 <= (b n).2.
  move=> /= h.
  set A' := fun => if (b n).1 >= (b n).2 then set0 else A n.
  set b' := fun => if (b n).1 >= (b n).2 then (0, 0) else b n.
  rewrite [leRHS](_ : _ = \sum_( <oo) wlength f (A' n))%E.
    apply: (@eq_eseriesr _ (wlength f \o A) (wlength f \o A')) => k.
    rewrite /= /A' AE; case: ifPn => // bn.
    by rewrite set_itv_ge//= bnd_simp -leNgt.
  apply: (h b').
  - move=> k; rewrite /A'; case: ifPn => // bk.
    by rewrite set_itv_ge//= bnd_simp -leNgt /b' bk.
  - by rewrite AE /b' (negbTE bk).
  - apply: (subset_trans lebig); apply subset_bigcup => k _.
    rewrite /A' AE; case: ifPn => bk //.
    by rewrite subset0 set_itv_ge//= bnd_simp -leNgt.
  - by move=> k; rewrite /b'; case: ifPn => //; rewrite -ltNge => /ltW.
apply/lee_addgt0Pr => _/posnumP[e].
rewrite [e%:num]splitr [in leRHS]EFinD addeA -leeBlDr//.
apply: le_trans (epsilon_trick _ _ _) => //=.
have [c ce] := nondecreasing_right_continuousP a.1 f [gt0 of e%:num / 2].
have [D De] : exists : nat -> {posnum R}, forall ,
    f ((b i).2 + (D i)%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1.
  suff : forall , exists : {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.
  by move=> k; apply nondecreasing_right_continuousP.
have acbd : `[ a.1 + c%:num / 2, a.2] `<=`
            \bigcup_ `](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 ltrDl.
  apply: (subset_trans lebig) => r [n _ Anr]; exists n => //.
  move: Anr; rewrite AE /= !in_itv/= => /andP [->]/= /le_lt_trans.
  by apply; rewrite ltrDl.
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.
  by move=> _; exact: interval_open.
move=> /(_ _ _ _ obd acbd){obd acbd}.
case=> X _ acXbd.
rewrite /cover in acXbd.
rewrite -EFinD.
apply: (@le_trans _ _ (\sum_( <- X) (wlength f `](b i).1, (b i).2]%classic) +
    \sum_( <- 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 lerB// (le_trans _ ce)//.
    rewrite cumulative_is_nondecreasing//.
    by rewrite lerD2l ler_pdivrMr// ler_pMr// ler1n.
  apply: (@le_trans _ _
      (\sum_( <- X) (f ((b i).2 + (D i)%:num) - f (b i).1)%:E)%E).
    rewrite sumEFin lee_fin cumulative_content_sub_fsum//.
      by move=> k kX; rewrite (@le_trans _ _ (b k).2)// lerDl.
    apply: subset_trans.
      exact/(subset_trans _ acXbd)/subset_itv_oc_cc.
    move=> x [k kX] kx; rewrite -bigcup_fset; exists k => //.
    by move: x kx; exact: subset_itv_oo_oc.
  rewrite addeC -big_split/=; apply: lee_sum => k _.
  by rewrite !(EFinB, wlength_itv_bnd)// addeA subeK.
rewrite -big_split/= nneseries_esum//; first by move=> k _; rewrite adde_ge0.
rewrite esum_ge//=; first by move=> n _; rewrite adde_ge0.
exists [set` X] => //; rewrite fsbig_finite//= set_fsetK.
rewrite big_seq [in X in (_ <= X)%E]big_seq; apply: lee_sum => k kX.
by rewrite AE leeD2l// lee_fin lerBlDl natrX De.
Qed.

. ( R R) :=
  Content_SigmaSubAdditive_isMeasure.Build _ _ _
    (wlength f) (wlength_sigma_subadditive f).

Lemma ( : R -> R) :
  sigma_finite [set: (ocitv_type R)] (wlength f).

Proof.

exists (fun => `](- k%:R), k%:R]%classic).
apply/esym; rewrite -subTset => /= x _ /=.
by exists (Num.bound x); rewrite //= in_itv/= ltrNl ltrNbound ltW// ltr_bound.
move=> k; split => //; rewrite wlength_itv /= -EFinB.
by case: ifP; rewrite ltey.
Qed.

Definition ( : cumulative R R) :=
  measure_extension (wlength f).
. ( R R) :=
  Measure.on (ocitv_lebesgue_stieltjes_measure f).

Let ( : cumulative R R) :
  sigma_finite setT (ocitv_lebesgue_stieltjes_measure f).

Proof.

have := measure_extension_sigma_finite (wlength_sigma_finite f).
by move=> [X bX fX]; exists X.
Qed.

. ( R R) :=
  @Measure_isSigmaFinite.Build _ _ _ (ocitv_lebesgue_stieltjes_measure f)
    (ocitv_sigmaT_finite_lebesgue_stieltjes_measure f).

Definition ( : cumulative R R) :
  set (g_sigma_algebraType (@open R)) -> \bar R :=
  measure_extension (wlength f).

Let ( : cumulative R R) : lebesgue_stieltjes_measure f set0 = 0.

Proof.

by []. Qed.

Let ( : cumulative R R) : (0 <= lebesgue_stieltjes_measure f x)%E.

Proof.

by []. Qed.

Let ( : cumulative R R) :
semi_sigma_additive (lebesgue_stieltjes_measure f).

Proof.

by move=> /= F mF tF mbF; apply: measure_semi_sigma_additive=>//;
rewrite RGenOpenSets.measurableE//=.
Qed.

. ( R R) :=
  isMeasure.Build _ _ _ (lebesgue_stieltjes_measure f)
    (lsm0 f) (lsm_ge0 f) (@lsm_semi_sigma_additive f).

Let ( : cumulative R R) :
  sigma_finite setT (lebesgue_stieltjes_measure f).

Proof.

have := measure_extension_sigma_finite (wlength_sigma_finite f).
by move=> [X bX fX]; exists X=>// i; rewrite -RGenOpenSets.measurableE.
Qed.

. ( R R) :=
  @Measure_isSigmaFinite.Build _ _ _ (lebesgue_stieltjes_measure f)
    (sigmaT_finite_lebesgue_stieltjes_measure f).

End wlength_extension.
Arguments lebesgue_stieltjes_measure {R}.

Section lebesgue_stieltjes_measure_unique.
Context { : realType} ( : cumulative R R).
Import MeasurableR.

Let
    ( : {measure set (MeasurableRocitv.measurableTypeR R) -> \bar R}) :
    (forall , ocitv X -> lebesgue_stieltjes_measure f X = mu X) ->
  forall : set R, measurable A -> lebesgue_stieltjes_measure f A = mu A.

Proof.

move=> muE A mA.
apply: measure_extension_unique => //=.
- exact: wlength_sigma_finite.
- by move=> X mX; rewrite -muE// -measurable_mu_extE.
- by rewrite RGenOpenSets.measurableE.
Qed.

Lemma
    ( : {measure set (MeasurableRopen.measurableTypeR R) -> \bar R}) :
    (forall , ocitv X -> lebesgue_stieltjes_measure f X = mu X) ->
  forall : set R, measurable A -> lebesgue_stieltjes_measure f A = mu A.

Proof.

move=> muE A mA; rewrite -ocitv_measure_ext.
exact: ocitv_lebesgue_stieltjes_measure_unique.
Qed.

End lebesgue_stieltjes_measure_unique.

Section completed_lebesgue_stieltjes_measure.
Context { : realType}.

Definition ( : cumulative R R) :=
  @completed_measure_extension _ _ _ (wlength f).

. ( R R) :=
  Measure.on (@completed_lebesgue_stieltjes_measure f).

Let ( : cumulative R R) :
  sigma_finite setT (@completed_lebesgue_stieltjes_measure f).

Proof.

exact/completed_measure_extension_sigma_finite/wlength_sigma_finite. Qed.

. ( R R) :=
  @Measure_isSigmaFinite.Build _ _ _
    (@completed_lebesgue_stieltjes_measure f)
    (sigmaT_finite_completed_lebesgue_stieltjes_measure f).

End completed_lebesgue_stieltjes_measure.
Arguments completed_lebesgue_stieltjes_measure {R}.

Section probability_measure_of_lebesgue_stieltjes_mesure.
Context { : realType} ( : cumulativeBounded (0:R) (1:R)).
Local Open Scope measure_display_scope.

Let := lebesgue_stieltjes_measure f.

Let : lsf setT = 1%E.

Proof.

rewrite -(bigcup_itvT false false).
pose I : set R := `]- (n%:R), n%:R]%classic.
have : (lsf \o I) n @[ --> \oo] --> 1%E.
  have -> : lsf \o I = (fun => (f n%:R)%:E - (f (- n%:R))%:E)%E.
    apply/funext=> n; rewrite /= /lsf/= /lebesgue_stieltjes_measure.
    rewrite /measure_extension measurable_mu_extE/=; first exact: is_ocitv.
    by rewrite wlength_itv_bnd// ge0_cp.
  rewrite -(sube0 1); apply: cvgeB => //.
  - by apply/cvg_EFin; [near=> F
                       |exact/(cvg_comp _ _ (@cvgr_idn R))/cumulativey].
  - apply/cvg_EFin; [by near=> F|apply: (cvg_ninftyP _ _).1 => //].
      exact: cumulativeNy.
    by apply: (cvg_comp _ _ (@cvgr_idn R)); rewrite ninfty.
have : (lsf \o I) n @[ --> \oo] --> lsf (\bigcup_ I n).
  apply: nondecreasing_cvg_measure; rewrite /I//; first exact: bigcup_measurable.
  by move=> *; apply/subsetPset/subset_itv; rewrite leBSide/= ?lerN2 ler_nat.
exact: cvg_unique.
Unshelve. all: end_near. Qed.

..Build _ _ _
(lebesgue_stieltjes_measure f) lebesgue_stieltjes_setT.

End probability_measure_of_lebesgue_stieltjes_mesure.

Files

Module mathcomp.analysis.lebesgue_stieltjes_measure