Library mathcomp.analysis.lebesgue_stieltjes_measure

(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval.
From mathcomp Require Import finmap fingroup perm rat.
From HB Require Import structures.
From mathcomp.classical Require Import mathcomp_extra boolp classical_sets.
From mathcomp.classical Require Import functions fsbigop cardinality.
Require Import reals ereal signed topology numfun normedtype sequences esum.
Require Import real_interval measure realfun.

Lebesgue Stieltjes Measure This file contains a formalization of the Lebesgue-Stieltjes measure using the Measure Extension theorem from measure.v. Reference:

Achim Klenke, Probability Theory 2nd edition, 2014 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 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 wlength f A := f b - f a with the hull of the set of real numbers A being delimited by a and b

lebesgue_stieltjes_measure f == Lebesgue-Stieltjes measure for f f is a cumulative function.

Set Implicit Arguments.
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").

TODO: move?

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

Lemma right_continuousW (R : numFieldType) (f : R → R) :
  continuous f → right_continuous f.

#[short(type=cumulative)]
HB.structure Definition Cumulative (R : numFieldType) :=
  { f of isCumulative R f }.

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

Lemma nondecreasing_right_continuousP (R : numFieldType) (a : R) (e : R)
    (f : cumulative R) :
  e > 0 → ∃ d : {posnum R }, f (a + d %:num) ≤ f a + e.

Section id_is_cumulative.
Variable R : realType.

Let id_nd : {homo @idfun R : x y / x ≤ y }.

Let id_rc : right_continuous (@idfun R).

End id_is_cumulative.

/TODO: move?

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

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

Lemma is_ocitv a b : ocitv `]a , b ]%classic.
Hint Extern 0 (ocitv _) ⇒ solve [apply: is_ocitv] : core.

Lemma ocitv0 : ocitv set0.
Hint Resolve ocitv0 : core.

Lemma ocitvP X : ocitv X ↔ X = set0 ∨ exists2 x , x .1 < x .2 & X = `]x .1 , x .2 ]%classic.

Lemma ocitvD : semi_setD_closed ocitv.

Lemma ocitvI : setI_closed ocitv.

Definition ocitv_display : Type → measure_display.

End itv_semiRingOfSets.

Notation "R .-ocitv" := (ocitv_display R) : measure_display_scope.
Notation "R .-ocitv.-measurable" := (measurable : set (set (ocitv_type R))) :
  classical_set_scope.

Local Open Scope measure_display_scope.

Section wlength.
Context {R : realType}.
Variable (f : R → R).
Local Open Scope ereal_scope.
Implicit Types i j : interval R.

Let g : \bar R → \bar R := er_map f.

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

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

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

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

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

Lemma wlength_finite_fin_num i : neitv i → wlength [set ` i ] < +oo →
  ((i .1 : \bar R ) \is a fin_num ) ∧ ((i .2 : \bar R ) \is a fin_num ).

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

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

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

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

Lemma pinfty_wlength_itv i : wlength [set ` i ] = +oo →
  (∃ s r , i = Interval -oo%O (BSide s r) ∨ i = Interval (BSide s r) +oo%O)
  ∨ i = `]-oo, +oo[.

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

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

Lemma le_wlength_itv (ndf : {homo f : x y / (x ≤ y)%R}) i j :
  {subset i ≤ j } → wlength [set ` i ] ≤ wlength [set ` j ].

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

End wlength.

Section wlength_extension.
Context {R : realType}.

Lemma wlength_semi_additive (f : R → R) : semi_additive (wlength f).

Lemma wlength_ge0 (f : cumulative R) (I : set (ocitv_type R)) :
  (0 ≤ wlength f I)%E.

#[local] Hint Extern 0 (0%:E ≤ wlength _ _) ⇒ solve[apply: wlength_ge0] : core.

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

Lemma cumulative_content_sub_fsum (f : cumulative R) (D : {fset nat}) a0 b0
    (a b : nat → R) : (∀ 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)).

Lemma wlength_sigma_sub_additive (f : cumulative R) :
  sigma_sub_additive (wlength f).

Lemma wlength_sigma_finite (f : R → R) :
  sigma_finite [set : (ocitv_type R )] (wlength f).

Definition lebesgue_stieltjes_measure (f : cumulative R) :=
  measure_extension [the measure _ _ of wlength f ].

TODO: this ought to be turned into a Let but older version of mathcomp/coq does not seem to allow, try to change asap