Require Import Program.Basics.
Require Import Coquelicot.Coquelicot.
Require Import Coq.Reals.Rbase.
Require Import Coq.Reals.Rfunctions.
Require Import Coq.Reals.RiemannInt.
Require Import Reals.
Require Import Lra Lia.
Require Import List Permutation.
Require Import Morphisms EquivDec.
Require Import Equivalence.
Require Import Classical ClassicalFacts ClassicalChoice.
Require Ensembles.
Require Import Utils DVector.
Import ListNotations.
Require Export Event SigmaAlgebras ProbSpace.
Require Export RandomVariable VectorRandomVariable.
Require Import ClassicalDescription.
Set Bullet Behavior "
Strict Subproofs".
Local Open Scope prob.
Section measure.
Local Existing Instance Rbar_le_pre.
Local Existing Instance Rbar_le_part.
Context {
T:
Type}.
Context {σ:
SigmaAlgebra T}.
Class is_measure (μ:
event σ ->
Rbar)
:=
mk_measure {
measure_proper :>
Proper (
event_equiv ==>
eq) μ
;
measure_none : μ
event_none = 0%
R
;
measure_nneg a :
Rbar_le 0 (μ
a)
;
measure_countable_disjoint_union (
B:
nat->
event σ) :
collection_is_pairwise_disjoint B ->
μ (
union_of_collection B) = (
ELim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => μ (
B n))
i))
}.
Lemma measure_list_disjoint_union (μ:
event σ ->
Rbar) {μ
_meas:
is_measure μ} (
l:
list (
event σ)) :
ForallOrdPairs event_disjoint l ->
μ (
list_union l) =
list_Rbar_sum (
map μ
l).
Proof.
Lemma measure_disjoint_union (μ:
event σ ->
Rbar) {μ
_meas:
is_measure μ} (
a b:
event σ) :
event_disjoint a b ->
μ (
a ∪
b) =
Rbar_plus (μ
a) (μ
b).
Proof.
Global Instance measure_monotone (μ:
event σ ->
Rbar) {μ
_meas:
is_measure μ} :
Proper (
event_sub ==>
Rbar_le) μ.
Proof.
Lemma measure_countable_sub_union (μ:
event σ ->
Rbar) {μ
_meas:
is_measure μ} (
B:
nat->
event σ) :
Rbar_le (μ (
union_of_collection B)) (
ELim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => μ (
B n))
i)).
Proof.
Lemma measure_all_one_ps_le1 (μ:
event σ ->
Rbar) {μ
_meas:
is_measure μ}
(
measure_all:μ Ω =
R1)
A :
Rbar_le (μ
A)
R1.
Proof.
Lemma measure_all_one_ps_fin (μ:
event σ ->
Rbar) {μ
_meas:
is_measure μ}
(
measure_all:μ Ω =
R1)
A :
is_finite (μ
A).
Proof.
Lemma is_measure_ex_Elim_seq
(μ:
event σ ->
Rbar) {μ
_meas:
is_measure μ} (
E:
nat->
event σ) :
ex_Elim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => μ (
E n))
i).
Proof.
Program Instance measure_all_one_ps (μ:
event σ ->
Rbar) {μ
_meas:
is_measure μ}
(
measure_all:μ Ω =
R1) :
ProbSpace σ
:= {|
ps_P x :=
real (μ
x)
|}.
Next Obligation.
intros ???.
now rewrite H.
Qed.
Next Obligation.
Next Obligation.
now rewrite measure_all.
Qed.
Next Obligation.
generalize (
measure_nneg A);
simpl.
match_destr;
simpl;
try tauto;
try lra.
Qed.
Lemma ps_measure (
ps:
ProbSpace σ) :
is_measure ps_P.
Proof.
Class is_complete_measure (μ:
event σ ->
Rbar) {μ
_meas:
is_measure μ}
:=
measure_is_complete :
forall a b,
pre_event_sub a (
event_pre b) -> μ
b = 0 ->
sa_sigma a.
End measure.
Global Instance is_measure_proper {
A} :
Proper (
sa_sub --> (
pre_event_equiv ==>
eq) ==>
impl) (@
is_measure A).
Proof.
Global Instance is_measure_proper_sub {
A}
(
sa1 sa2:
SigmaAlgebra A)
(
sub:
sa_sub sa1 sa2) μ {μ
_meas:
is_measure (σ:=
sa2) μ} :
is_measure (σ:=
sa1) (
fun x => μ (
event_sa_sub sub x)).
Proof.
Section outer_measure.
Context {
T:
Type}.
Local Existing Instance Rbar_le_pre.
Local Existing Instance Rbar_le_part.
Class is_outer_measure (μ:
pre_event T ->
Rbar)
:=
mk_outer_measure {
outer_measure_proper :>
Proper (
pre_event_equiv ==>
eq) μ
;
outer_measure_none : μ
pre_event_none = 0%
R
;
outer_measure_nneg a :
Rbar_le 0 (μ
a)
;
outer_measure_countable_subadditive (
A:
pre_event T) (
B:
nat->
pre_event T) :
pre_event_sub A (
pre_union_of_collection B) ->
Rbar_le (μ
A) (
ELim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => μ (
B n))
i))
}.
Class is_outer_measure_alt (μ:
pre_event T ->
Rbar)
:=
mk_outer_measure_alt {
outer_measure_alt_none : μ
pre_event_none = 0%
R
;
outer_measure_alt_nneg a :
Rbar_le 0 (μ
a)
;
outer_measure_alt_monotone :>
Proper (
pre_event_sub ==>
Rbar_le) μ
;
outer_measure_alt_countable_union (
B:
nat->
pre_event T) :
Rbar_le (μ (
pre_union_of_collection B)) (
ELim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => μ (
B n))
i))
}.
Hint Resolve outer_measure_nneg :
prob.
Hint Resolve Rbar_plus_nneg_compat :
prob.
Global Instance outer_measure_alt_proper (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure_alt μ}:
Proper (
pre_event_equiv ==>
eq) μ.
Proof.
Lemma is_outer_measure_ex_Elim_seq
(μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
E:
nat->
pre_event T) :
ex_Elim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => μ (
E n))
i).
Proof.
Lemma outer_measure_list_subadditive
(μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ}
(
A:
pre_event T) (
B:
list (
pre_event T)) :
pre_event_sub A (
pre_list_union B) ->
Rbar_le (μ
A) (
list_Rbar_sum (
map μ
B)).
Proof.
Global Instance is_outer_measure_is_alt
(μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} :
is_outer_measure_alt μ.
Proof.
Lemma is_outer_measure_alt_iff (μ:
pre_event T ->
Rbar) :
is_outer_measure μ <->
is_outer_measure_alt μ.
Proof.
Definition μ
_measurable (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
E:
pre_event T)
:=
forall (
A:
pre_event T), μ
A =
Rbar_plus (μ (
pre_event_inter A E)) (μ (
pre_event_diff A E)).
Global Instance μ
_measurable_proper (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} :
Proper (
pre_event_equiv ==>
iff) (μ
_measurable μ).
Proof.
unfold μ_measurable.
intros ???.
split; intros ??.
- now rewrite <- H.
- now rewrite H.
Qed.
Lemma μ
_measurable_simpl (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
E:
pre_event T)
: (
forall (
A:
pre_event T),
Rbar_le (
Rbar_plus (μ (
pre_event_inter A E))
(μ (
pre_event_diff A E)))
(μ
A)) -> μ
_measurable μ
E.
Proof.
Lemma μ
_measurable_complement (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
E:
pre_event T) :
μ
_measurable μ
E -> μ
_measurable μ (
pre_event_complement E).
Proof.
Lemma μ
_measurable_complement_b (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
E:
pre_event T) :
μ
_measurable μ (
pre_event_complement E) -> μ
_measurable μ
E.
Proof.
Hint Resolve ex_Rbar_plus_pos :
prob.
Lemma measure_ex_Rbar_plus (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ}
x y :
ex_Rbar_plus (μ
x) (μ
y).
Proof.
auto with prob.
Qed.
Hint Resolve measure_ex_Rbar_plus :
prob.
Lemma measure_fold_right_Rbar_plus_nneg
(μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ}
l :
Rbar_le 0 (
fold_right Rbar_plus 0 (
map μ
l)).
Proof.
Lemma list_Rbar_sum_measure_perm (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} {
l1 l2} :
Permutation l1 l2 ->
list_Rbar_sum (
map μ
l1) =
list_Rbar_sum (
map μ
l2).
Proof.
Lemma μ
_measurable_list_inter_disjoint_additivity
(μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
A:
pre_event T) (
l :
list (
pre_event T)) :
Forall (μ
_measurable μ)
l ->
ForallOrdPairs pre_event_disjoint l ->
μ (
pre_list_union (
map (
pre_event_inter A)
l)) =
list_Rbar_sum (
map μ (
map (
pre_event_inter A)
l)).
Proof.
Lemma μ
_measurable_list_disjoint_additivity
(μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
l :
list (
pre_event T)) :
Forall (μ
_measurable μ)
l ->
ForallOrdPairs pre_event_disjoint l ->
μ (
pre_list_union l) =
list_Rbar_sum (
map μ
l).
Proof.
Lemma μ
_measurable_list_inter_take_disjoint_additivity
(μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
A:
pre_event T) (
E:
nat ->
pre_event T) :
(
forall n, μ
_measurable μ (
E n)) ->
pre_collection_is_pairwise_disjoint E ->
forall n, μ (
pre_list_union (
map (
pre_event_inter A) (
collection_take E n))) =
sum_Rbar_n (
fun i :
nat => μ (
pre_event_inter A (
E i)))
n.
Proof.
Lemma μ
_measurable_list_take_disjoint_additivity
(μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
E:
nat ->
pre_event T) :
(
forall n, μ
_measurable μ (
E n)) ->
pre_collection_is_pairwise_disjoint E ->
forall n, μ (
pre_list_union (
collection_take E n)) =
sum_Rbar_n (
fun i :
nat => μ (
E i))
n.
Proof.
Theorem μ
_measurable_countable_inter_disjoint_additivity
(μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
A:
pre_event T) (
E:
nat ->
pre_event T) :
(
forall n, μ
_measurable μ (
E n)) ->
pre_collection_is_pairwise_disjoint E ->
μ (
pre_union_of_collection (
fun n =>
pre_event_inter A (
E n))) =
ELim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => μ (
pre_event_inter A (
E n)))
i).
Proof.
Theorem μ
_measurable_countable_disjoint_additivity
(μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
E:
nat ->
pre_event T) :
(
forall n, μ
_measurable μ (
E n)) ->
pre_collection_is_pairwise_disjoint E ->
(μ (
pre_union_of_collection E)) =
ELim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => μ (
E n))
i).
Proof.
Theorem μ
_measurable_0 (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
E:
pre_event T) :
μ
E = 0 -> μ
_measurable μ
E.
Proof.
Lemma μ
_measurable_none (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} :
μ
_measurable μ
pre_event_none.
Proof.
Hint Resolve μ
_measurable_none :
prob.
Lemma μ
_measurable_Ω (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} :
μ
_measurable μ
pre_Ω.
Proof.
rewrite <-
pre_event_not_none.
apply μ
_measurable_complement.
apply μ
_measurable_none.
Qed.
Hint Resolve μ
_measurable_Ω :
prob.
Lemma μ
_measurable_union (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
a b :
pre_event T) :
μ
_measurable μ
a ->
μ
_measurable μ
b ->
μ
_measurable μ (
pre_event_union a b).
Proof.
Hint Resolve μ
_measurable_union μ
_measurable_complement :
prob.
Corollary μ
_measurable_inter (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
a b :
pre_event T) :
μ
_measurable μ
a ->
μ
_measurable μ
b ->
μ
_measurable μ (
pre_event_inter a b).
Proof.
Hint Resolve μ
_measurable_inter :
prob.
Corollary μ
_measurable_diff (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
a b :
pre_event T) :
μ
_measurable μ
a ->
μ
_measurable μ
b ->
μ
_measurable μ (
pre_event_diff a b).
Proof.
Hint Resolve μ
_measurable_inter :
prob.
Lemma μ
_measurable_list_union (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
l:
list (
pre_event T)) :
Forall (μ
_measurable μ)
l ->
μ
_measurable μ (
pre_list_union l).
Proof.
Lemma μ
_measurable_disjoint_countable_union (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
E:
nat ->
pre_event T) :
(
forall n, μ
_measurable μ (
E n)) ->
pre_collection_is_pairwise_disjoint E ->
μ
_measurable μ (
pre_union_of_collection E).
Proof.
Lemma μ
_measurable_make_disjoint (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
E:
nat ->
pre_event T) :
(
forall n, μ
_measurable μ (
E n)) ->
forall n, μ
_measurable μ (
make_pre_collection_disjoint E n).
Proof.
Theorem μ
_measurable_countable_union (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} (
E:
nat ->
pre_event T) :
(
forall n, μ
_measurable μ (
E n)) -> μ
_measurable μ (
pre_union_of_collection E).
Proof.
Instance μ
_measurable_sa (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} :
SigmaAlgebra T
:= {|
sa_sigma E := μ
_measurable μ
E
;
sa_countable_union := μ
_measurable_countable_union μ
;
sa_complement := μ
_measurable_complement μ
;
sa_all := μ
_measurable_Ω μ
|}.
Global Instance μ
_measurable_sa_measure (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} :
is_measure (σ:=μ
_measurable_sa μ) μ.
Proof.
constructor.
-
intros ???.
red in H.
now rewrite H.
-
apply outer_measure_none.
-
intros.
apply outer_measure_nneg.
-
intros.
apply (μ
_measurable_countable_disjoint_additivity μ);
trivial.
intros.
now destruct (
B n);
simpl.
Qed.
Global Instance μ
_measurable_sa_complete_measure (μ:
pre_event T ->
Rbar) {μ
_outer:
is_outer_measure μ} :
is_complete_measure (σ:=μ
_measurable_sa μ) μ.
Proof.
End outer_measure.
Section algebra.
Class Algebra (
T:
Type) :=
{
alg_in :
pre_event T ->
Prop;
alg_in_list_union (
l:
list (
pre_event T)) :
Forall alg_in l ->
alg_in (
pre_list_union l);
alg_in_complement (
A:
pre_event T) :
alg_in A ->
alg_in (
pre_event_complement A) ;
alg_in_all :
alg_in pre_Ω
}.
Global Instance alg_proper {
T} (
s:
Algebra T) :
Proper (
pre_event_equiv ==>
iff)
alg_in.
Proof.
Lemma alg_in_none {
T} (
s:
Algebra T) :
alg_in pre_event_none.
Proof.
Lemma alg_in_list_inter {
T} {
alg:
Algebra T}
(
l:
list (
pre_event T)) :
Forall alg_in l ->
alg_in (
pre_list_inter l).
Proof.
Lemma alg_in_union {
T} {
alg:
Algebra T}
(
a b :
pre_event T) :
alg_in a ->
alg_in b ->
alg_in (
pre_event_union a b).
Proof.
Lemma alg_in_inter {
T} {
alg:
Algebra T}
(
a b :
pre_event T) :
alg_in a ->
alg_in b ->
alg_in (
pre_event_inter a b).
Proof.
Lemma alg_in_diff {
T} {
alg:
Algebra T}
(
a b :
pre_event T) :
alg_in a ->
alg_in b ->
alg_in (
pre_event_diff a b).
Proof.
Definition alg_set {
T} (
A:
Algebra T):
Type := {
x |
alg_in x}.
Definition alg_pre {
T} {
A:
Algebra T} :
alg_set A -> (
T->
Prop)
:=
fun e =>
proj1_sig e.
Lemma alg_set_in {
T} {
Alg:
Algebra T} (
a:
alg_set Alg) :
alg_in (
alg_pre a).
Proof.
now destruct a.
Qed.
Definition alg_sub {
T} {
Alg:
Algebra T} (
x y:
alg_set Alg) :=
pre_event_sub (
proj1_sig x) (
proj1_sig y).
Definition alg_equiv {
T} {
Alg:
Algebra T} (
x y:
alg_set Alg) :=
pre_event_equiv (
proj1_sig x) (
proj1_sig y).
Global Instance alg_equiv_equiv {
T} {
Alg:
Algebra T} :
Equivalence alg_equiv.
Proof.
firstorder.
Qed.
Global Instance alg_equiv_sub {
T} {
Alg:
Algebra T} :
subrelation alg_equiv alg_sub.
Proof.
firstorder.
Qed.
Global Instance alg_sub_pre {
T} {
Alg:
Algebra T} :
PreOrder alg_sub.
Proof.
firstorder.
Qed.
Global Instance alg_sub_part {
T} {
Alg:
Algebra T} :
PartialOrder alg_equiv alg_sub.
Proof.
firstorder.
Qed.
Coercion alg_pre :
alg_set >->
Funclass.
Definition alg_none {
T} {
Alg :
Algebra T} :
alg_set Alg
:=
exist _ _ (
alg_in_none _).
Definition alg_all {
T} {
Alg :
Algebra T} :
alg_set Alg
:=
exist _ _ alg_in_all.
Program Definition alg_list_union {
T} {
Alg:
Algebra T} (
l:
list (
alg_set Alg)) :
alg_set Alg
:=
exist _ (
pre_list_union (
map alg_pre l))
_.
Next Obligation.
Program Definition alg_list_inter {
T} {
Alg:
Algebra T} (
l:
list (
alg_set Alg)) :
alg_set Alg
:=
exist _ (
pre_list_inter (
map alg_pre l))
_.
Next Obligation.
Definition alg_union {
T} {
Alg:
Algebra T} (
a b :
alg_set Alg) :
alg_set Alg
:=
exist _ (
pre_event_union a b) (
alg_in_union _ _ (
alg_set_in a) (
alg_set_in b)).
Definition alg_inter {
T} {
Alg:
Algebra T} (
a b :
alg_set Alg) :
alg_set Alg
:=
exist _ (
pre_event_inter a b) (
alg_in_inter _ _ (
alg_set_in a) (
alg_set_in b)).
Definition alg_diff {
T} {
Alg:
Algebra T} (
a b :
alg_set Alg) :
alg_set Alg
:=
exist _ (
pre_event_diff a b) (
alg_in_diff _ _ (
alg_set_in a) (
alg_set_in b)).
Context {
T} {
Alg:
Algebra T}.
Global Instance alg_union_proper :
Proper (
alg_equiv ==>
alg_equiv ==>
alg_equiv)
alg_union.
Proof.
Global Instance alg_inter_proper :
Proper (
alg_equiv ==>
alg_equiv ==>
alg_equiv)
alg_inter.
Proof.
Global Instance alg_diff_proper :
Proper (
alg_equiv ==>
alg_equiv ==>
alg_equiv)
alg_diff.
Proof.
Lemma alg_sub_diff_union (
A B :
alg_set Alg) :
alg_sub B A ->
alg_equiv A (
alg_union (
alg_diff A B)
B).
Proof.
Lemma alg_list_union_nil :
alg_equiv (
alg_list_union [])
alg_none.
Proof.
firstorder.
Qed.
Lemma alg_list_union_cons (
x1 :
alg_set Alg) (
l:
list (
alg_set Alg)):
alg_equiv (
alg_list_union (
x1::
l)) (
alg_union x1 (
alg_list_union l)).
Proof.
Lemma alg_list_union_singleton (
En:
alg_set Alg) :
alg_equiv (
alg_list_union [
En])
En.
Proof.
End algebra.
Section premeasure.
Local Existing Instance Rbar_le_pre.
Local Existing Instance Rbar_le_part.
Context {
T:
Type}.
Context {
Alg:
Algebra T}.
Class is_premeasure (λ:
alg_set Alg ->
Rbar)
:=
mk_premeasure {
premeasure_proper :>
Proper (
alg_equiv ==>
eq) λ
;
premeasure_none : λ
alg_none = 0%
R
;
premeasure_nneg a :
Rbar_le 0 (λ
a)
;
premeasure_countable_disjoint_union (
B:
nat->
alg_set Alg) :
pre_collection_is_pairwise_disjoint (
fun x =>
B x) ->
forall (
pf:
alg_in (
pre_union_of_collection (
fun x =>
B x))),
λ (
exist _ _ pf) = (
ELim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => λ (
B n))
i))
}.
Section props.
Context (λ:
alg_set Alg ->
Rbar) {μ
_meas:
is_premeasure λ}.
Lemma premeasure_list_disjoint_union (
a:
list (
alg_set Alg)) :
ForallOrdPairs pre_event_disjoint (
map alg_pre a) ->
λ (
alg_list_union a) =
list_Rbar_sum (
map λ
a).
Proof.
Lemma premeasure_disjoint_union (
a b:
alg_set Alg) :
pre_event_disjoint a b ->
λ (
alg_union a b) =
Rbar_plus (λ
a) (λ
b).
Proof.
Global Instance premeasure_monotone :
Proper (
alg_sub ==>
Rbar_le) λ.
Proof.
Definition alg_make_collection_disjoint (
coll:
nat->
alg_set Alg) :
nat ->
alg_set Alg
:=
fun x =>
alg_diff (
coll x) (
alg_list_union
(
collection_take coll x)).
Lemma alg_make_collection_disjoint_sub (
En:
nat ->
alg_set Alg)
n :
alg_sub (
alg_make_collection_disjoint En n) (
En n).
Proof.
now intros x [??].
Qed.
Lemma alg_make_collection_disjoint_in (
coll:
nat->
alg_set Alg) (
x:
nat) (
e:
T) :
proj1_sig (
alg_make_collection_disjoint coll x)
e <->
(
proj1_sig (
coll x)
e /\
forall y, (
y <
x)%
nat -> ~
proj1_sig (
coll y)
e).
Proof.
Lemma alg_make_collection_disjoint_disjoint (
coll:
nat->
alg_set Alg) :
pre_collection_is_pairwise_disjoint (
alg_make_collection_disjoint coll).
Proof.
Lemma pre_alg_make_collection_disjoint_union (
coll:
nat->
alg_set Alg) :
pre_event_equiv (
pre_union_of_collection (
fun x :
nat =>
coll x))
(
pre_union_of_collection (
alg_make_collection_disjoint coll)).
Proof.
Lemma alg_make_collection_disjoint_union (
coll:
nat->
alg_set Alg)
(
pf1:
alg_in (
pre_union_of_collection (
fun x :
nat =>
coll x)))
(
pf2:
alg_in (
pre_union_of_collection (
alg_make_collection_disjoint coll))) :
alg_equiv (
exist _ _ pf1) (
exist _ _ pf2).
Proof.
Lemma alg_make_collection_disjoint_union_alg_in (
coll:
nat->
alg_set Alg)
(
pf1:
alg_in (
pre_union_of_collection (
fun x :
nat =>
coll x))) :
alg_in (
pre_union_of_collection (
alg_make_collection_disjoint coll)).
Proof.
Lemma alg_make_collection_disjoint_union' (
coll:
nat->
alg_set Alg)
(
pf1:
alg_in (
pre_union_of_collection (
fun x :
nat =>
coll x))) :
alg_equiv (
exist _ _ pf1) (
exist _ _ (
alg_make_collection_disjoint_union_alg_in _ pf1)).
Proof.
Lemma premeasure_countable_sub_union (
B:
nat->
alg_set Alg) :
forall (
pf:
alg_in (
pre_union_of_collection (
fun x =>
B x))),
Rbar_le (λ (
exist _ _ pf)) (
ELim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => λ (
B n))
i)).
Proof.
End props.
End premeasure.
Section omf.
Local Existing Instance Rbar_le_pre.
Local Existing Instance Rbar_le_part.
Context {
T:
Type}.
Context {
Alg:
Algebra T}.
Context (λ:
alg_set Alg ->
Rbar).
Context {λ
_meas:
is_premeasure λ}.
Definition outer_λ
_of_covers (
an:
nat->
alg_set Alg) :
Rbar :=
ELim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => λ (
an n))
i).
Definition outer_λ (
A:
pre_event T) :
Rbar
:=
Rbar_glb (
fun (
x :
Rbar) =>
exists (
an:
nat->
alg_set Alg),
pre_event_sub A (
pre_union_of_collection an) /\
x =
outer_λ
_of_covers an).
Lemma outer_λ
_nneg (
A:
pre_event T)
:
Rbar_le 0 (
outer_λ
A).
Proof.
Lemma outer_λ
_of_covers_nneg (
an:
nat->
alg_set Alg) :
Rbar_le 0 (
outer_λ
_of_covers an).
Proof.
Global Instance outer_λ
_of_covers_monotone :
Proper (
pointwise_relation _ alg_sub ==>
Rbar_le)
outer_λ
_of_covers.
Proof.
Global Instance outer_λ
_outer_measure :
is_outer_measure outer_λ.
Proof.
unfold outer_λ.
apply is_outer_measure_alt_iff.
constructor.
-
apply antisymmetry;
try apply outer_λ
_nneg.
unfold Rbar_glb,
proj1_sig;
match_destr;
destruct r as [
lb glb].
apply lb.
exists (
fun _ =>
alg_none).
split.
+
simpl.
rewrite pre_union_of_collection_const.
reflexivity.
+
rewrite <- (
ELim_seq_const 0).
apply ELim_seq_ext;
intros.
unfold sum_Rbar_n.
induction (
seq 0
n);
simpl;
trivial.
rewrite IHl,
premeasure_none;
simpl.
now rewrite Rbar_plus_0_l.
-
intros.
apply outer_λ
_nneg.
-
intros ???.
apply Rbar_glb_subset
;
intros ? [? [??]].
exists x1.
split;
trivial.
now rewrite H.
-
intros B.
assert (
lim_seq_nneg:
Rbar_le 0
(
ELim_seq
(
fun i :
nat =>
sum_Rbar_n
(
fun n :
nat =>
Rbar_glb
(
fun x :
Rbar =>
exists an :
nat ->
alg_set Alg,
pre_event_sub (
B n) (
pre_union_of_collection an) /\
x =
outer_λ
_of_covers an))
i))).
{
apply ELim_seq_nneg;
intros.
apply sum_Rbar_n_nneg_nneg;
intros k klt.
apply Rbar_glb_ge;
intros ? [?[??]];
subst.
apply outer_λ
_of_covers_nneg.
}
case_eq (
ELim_seq
(
fun i :
nat =>
sum_Rbar_n
(
fun n :
nat =>
Rbar_glb
(
fun x :
Rbar =>
exists an :
nat ->
alg_set Alg,
pre_event_sub (
B n) (
pre_union_of_collection an) /\
x =
outer_λ
_of_covers an))
i)).
+
intros ??.
assert (
isnneg :
forall n,
Rbar_le 0
(
Rbar_glb
(
fun x :
Rbar =>
exists an :
nat ->
alg_set Alg,
pre_event_sub (
B n) (
pre_union_of_collection an) /\
x =
outer_λ
_of_covers an))).
{
intros.
apply Rbar_glb_ge;
intros ? [?[??]];
subst.
apply outer_λ
_of_covers_nneg.
}
assert (
isfin :
forall n,
is_finite (
Rbar_glb
(
fun x :
Rbar =>
exists an :
nat ->
alg_set Alg,
pre_event_sub (
B n) (
pre_union_of_collection an) /\
x =
outer_λ
_of_covers an))).
{
apply (
Elim_seq_sum_pos_fin_n_fin _ _ isnneg H).
}
apply Rbar_le_forall_Rbar_le;
intros eps.
assert (
p:
forall n,
exists (
en:
nat ->
alg_set Alg),
pre_event_sub (
B n) (
pre_union_of_collection en) /\
Rbar_le (
outer_λ
_of_covers en)
(
Rbar_plus (
outer_λ (
B n))
(
eps/(
pow 2 (
S n))))).
{
intros n.
specialize (
isfin n).
unfold outer_λ,
Rbar_glb,
proj1_sig in *;
match_destr.
rewrite <-
isfin in r0.
assert (
posdiv: 0 < (
eps / 2 ^ (
S n))).
{
apply Rdiv_lt_0_compat.
-
apply cond_pos.
-
apply pow_lt;
lra.
}
destruct (
Rbar_is_glb_fin_close_classic (
mkposreal _ posdiv)
r0)
as [? [[?[??]] ?]];
subst.
exists x1.
simpl.
split;
trivial.
simpl in H2.
rewrite <-
isfin;
simpl.
trivial.
}
apply choice in p;
trivial.
destruct p as [
an HH].
rewrite <-
H.
assert (
le1:
Rbar_le
(
ELim_seq
(
fun i :
nat =>
sum_Rbar_n
(
fun x :
nat =>
outer_λ
_of_covers (
an x))
i))
(
ELim_seq
(
fun i :
nat =>
sum_Rbar_n
(
fun x :
nat => (
Rbar_plus (
outer_λ (
B x)) (
eps / 2 ^
S x)))
i))).
{
apply ELim_seq_le;
intros.
apply sum_Rbar_n_monotone;
trivial;
intros ?.
apply HH.
}
rewrite ELim_seq_sum_eps2n in le1;
trivial
;
try solve [
destruct eps;
simpl;
lra].
etransitivity
; [
etransitivity |]
; [ |
apply le1 | ].
*
unfold Rbar_glb,
proj1_sig;
match_destr.
apply r0.
exists (
fun n =>
let '(
a,
b) :=
iso_b (
Isomorphism:=
nat_pair_encoder)
n in an a b).
split.
--
intros ? [??].
destruct (
HH x1).
destruct (
H1 x0 H0).
exists (
iso_f (
Isomorphism:=
nat_pair_encoder) (
x1,
x2)).
now rewrite iso_b_f.
--
unfold outer_λ
_of_covers.
transitivity (
ELim_seq
(
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => (
let '(
a,
b) :=
iso_b n in λ (
an a b)))
i)).
++
apply ELim_seq_Elim_seq_pair;
intros.
apply premeasure_nneg.
++
apply ELim_seq_ext;
intros ?.
unfold sum_Rbar_n.
f_equal.
apply map_ext;
intros ?.
now destruct (
iso_b a).
*
reflexivity.
+
intros H.
unfold Rbar_le;
match_destr.
+
intros H.
rewrite H in lim_seq_nneg.
now simpl in lim_seq_nneg.
Qed.
Lemma outer_λ
_is_measurable (
A:
alg_set Alg) : μ
_measurable outer_λ
A.
Proof.
Lemma outer_λ
_λ (
A:
alg_set Alg) :
outer_λ
A = λ
A.
Proof.
End omf.
Section semi_algebra.
Class SemiAlgebra (
T:
Type) :=
{
salg_in :
pre_event T ->
Prop;
salg_nempty :
exists a,
salg_in a;
salg_in_inter (
a b:
pre_event T) :
salg_in a ->
salg_in b ->
salg_in (
pre_event_inter a b);
salg_in_complement (
a:
pre_event T) :
salg_in a ->
exists l,
pre_event_equiv (
pre_event_complement a) (
pre_list_union l) /\
ForallOrdPairs pre_event_disjoint l /\
Forall salg_in l
}.
Global Instance salg_proper {
T} (
s:
SemiAlgebra T) :
Proper (
pre_event_equiv ==>
iff)
salg_in.
Proof.
Lemma pre_list_disjoint_concat_from_parts {
A B} (
f:
A->
list (
pre_event B))
l:
Forall (
fun x =>
ForallOrdPairs pre_event_disjoint (
f x))
l ->
ForallOrdPairs pre_event_disjoint (
map pre_list_union (
map f l)) ->
ForallOrdPairs pre_event_disjoint (
concat (
map f l)).
Proof.
intros.
induction l;
simpl;
trivial.
invcs H;
invcs H0.
cut_to IHl;
trivial.
induction (
f a);
simpl;
trivial.
invcs H3.
cut_to IHl0;
trivial.
-
constructor;
trivial.
apply Forall_app;
trivial.
rewrite Forall_forall;
intros ??.
rewrite Forall_forall in H2.
apply in_concat in H.
destruct H as [?[??]].
apply in_map_iff in H.
destruct H as [?[??]];
subst.
specialize (
H2 (
pre_list_union (
f x1))).
cut_to H2.
+
intros b ??.
apply (
H2 b)
;
red;
simpl;
eauto.
+
apply in_map.
now apply in_map.
-
revert H2.
apply Forall_impl;
intros.
rewrite pre_list_union_cons in H.
intros ???.
eapply H;
try eapply H2.
red;
eauto.
Qed.
Definition salgebra_algebra_in {
T} (
s:
SemiAlgebra T) (
x:
pre_event T) :=
exists (
l:
list (
pre_event T)),
Forall salg_in l /\
ForallOrdPairs pre_event_disjoint l /\
pre_event_equiv x (
pre_list_union l).
Lemma salgebra_algebra_none {
T:
Type} (
s:
SemiAlgebra T) :
salgebra_algebra_in s pre_Ω.
Proof.
Lemma salgebra_algebra_simpl {
T:
Type} (
s:
SemiAlgebra T)
x :
(
exists (
l:
list (
pre_event T)),
Forall salg_in l /\
pre_event_equiv x (
pre_list_union l)) <->
(
exists (
l:
list (
pre_event T)),
Forall salg_in l /\
ForallOrdPairs pre_event_disjoint l /\
pre_event_equiv x (
pre_list_union l)).
Proof.
Program Instance SemiAlgebra_Algebra {
T:
Type} (
s:
SemiAlgebra T) :
Algebra T
:= {|
alg_in (
x:
pre_event T) :=
salgebra_algebra_in s x
|}.
Next Obligation.
Next Obligation.
Next Obligation.
Lemma SemiAlgebra_in_algebra {
T} (
s:
SemiAlgebra T):
pre_event_sub salg_in (
alg_in (
Algebra:=
SemiAlgebra_Algebra s)).
Proof.
Lemma SemiAlgebra_Algebra_generates_same {
T} (
s:
SemiAlgebra T):
sa_equiv (
generated_sa (
alg_in (
Algebra:=
SemiAlgebra_Algebra s)))
(
generated_sa salg_in).
Proof.
Definition salg_set {
T} (
A:
SemiAlgebra T):
Type := {
x |
salg_in x}.
Definition salg_pre {
T} {
A:
SemiAlgebra T} :
salg_set A -> (
T->
Prop)
:=
fun e =>
proj1_sig e.
Lemma salg_set_in {
T} {
SAlg:
SemiAlgebra T} (
a:
salg_set SAlg) :
salg_in (
salg_pre a).
Proof.
now destruct a.
Qed.
Definition salg_sub {
T} {
SAlg:
SemiAlgebra T} (
x y:
salg_set SAlg) :=
pre_event_sub (
proj1_sig x) (
proj1_sig y).
Definition salg_equiv {
T} {
SAlg:
SemiAlgebra T} (
x y:
salg_set SAlg) :=
pre_event_equiv (
proj1_sig x) (
proj1_sig y).
Global Instance salg_equiv_equiv {
T} {
SAlg:
SemiAlgebra T} :
Equivalence salg_equiv.
Proof.
firstorder.
Qed.
Global Instance salg_equiv_sub {
T} {
SAlg:
SemiAlgebra T} :
subrelation salg_equiv salg_sub.
Proof.
firstorder.
Qed.
Global Instance salg_sub_pre {
T} {
SAlg:
SemiAlgebra T} :
PreOrder salg_sub.
Proof.
firstorder.
Qed.
Global Instance salg_sub_part {
T} {
SAlg:
SemiAlgebra T} :
PartialOrder salg_equiv salg_sub.
Proof.
firstorder.
Qed.
Coercion salg_pre :
salg_set >->
Funclass.
Definition salg_inter {
T} {
SAlg:
SemiAlgebra T} (
a b :
salg_set SAlg) :
salg_set SAlg
:=
exist _ (
pre_event_inter a b) (
salg_in_inter _ _ (
salg_set_in a) (
salg_set_in b)).
Context {
T} {
SAlg:
SemiAlgebra T}.
Global Instance salg_inter_proper :
Proper (
salg_equiv ==>
salg_equiv ==>
salg_equiv)
salg_inter.
Proof.
End semi_algebra.
Section semi_premeasure.
Local Existing Instance Rbar_le_pre.
Local Existing Instance Rbar_le_part.
Context {
T:
Type}.
Context {
SAlg:
SemiAlgebra T}.
Class is_semipremeasure (λ:
salg_set SAlg ->
Rbar)
:=
mk_semipremeasure {
semipremeasure_proper :>
Proper (
salg_equiv ==>
eq) λ
;
semipremeasure_nneg a :
Rbar_le 0 (λ
a)
;
semipremeasure_list_disjoint_union (
B:
list (
salg_set SAlg)) :
ForallOrdPairs pre_event_disjoint (
map salg_pre B) ->
forall (
pf:
salg_in (
pre_list_union (
map salg_pre B))),
λ (
exist _ _ pf) =
list_Rbar_sum (
map λ
B)
;
semipremeasure_countable_disjoint_union (
B:
nat->
salg_set SAlg) :
pre_collection_is_pairwise_disjoint (
fun x =>
B x) ->
forall (
pf:
salg_in (
pre_union_of_collection (
fun x =>
B x))),
λ (
exist _ _ pf) = (
ELim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => λ (
B n))
i))
}.
Lemma semipremeasure_with_zero_simpl (λ:
salg_set SAlg ->
Rbar)
(
proper :
Proper (
salg_equiv ==>
eq) λ)
(
nneg :
forall a,
Rbar_le 0 (λ
a))
(
has_none :
salg_in pre_event_none)
(
none: λ (
exist _ _ has_none) = 0)
(
countable_disjoint_union :
forall (
B:
nat->
salg_set SAlg),
pre_collection_is_pairwise_disjoint (
fun x =>
B x) ->
forall (
pf:
salg_in (
pre_union_of_collection (
fun x =>
B x))),
λ (
exist _ _ pf) = (
ELim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => λ (
B n))
i))) :
is_semipremeasure λ.
Proof.
Lemma semipremeasure_disjoint_list_irrel (λ:
salg_set SAlg ->
Rbar) {
meas:
is_semipremeasure λ}
(
R S:
list (
salg_set SAlg)):
ForallOrdPairs pre_event_disjoint (
map salg_pre R) ->
ForallOrdPairs pre_event_disjoint (
map salg_pre S) ->
pre_event_equiv (
pre_list_union (
map salg_pre R)) (
pre_list_union (
map salg_pre S)) ->
list_Rbar_sum (
map λ
R) =
list_Rbar_sum (
map λ
S).
Proof.
Lemma semipremeasure_disjoint_list_countable_irrel (λ:
salg_set SAlg ->
Rbar) {
meas:
is_semipremeasure λ}
(
R:
list (
salg_set SAlg))
(
S:
nat ->
salg_set SAlg):
ForallOrdPairs pre_event_disjoint (
map salg_pre R) ->
pre_collection_is_pairwise_disjoint (
fun x =>
S x) ->
pre_event_equiv (
pre_list_union (
map salg_pre R)) (
pre_union_of_collection S) ->
list_Rbar_sum (
map λ
R) =
ELim_seq (
fun i :
nat =>
sum_Rbar_n (
fun n :
nat => λ (
S n))
i).
Proof.
Ltac nth_destr_in H
:=
match type of H with
|
context [
nth ?
a ?
b ?
c] =>
let HH :=
fresh "
ntheq"
in
destruct (
nth_in_or_default a b c)
as [
HH|
HH]
; [|
rewrite HH in H]
end.
Lemma semipremeasure_disjoint_list_countable_list_irrel_with_default
(λ:
salg_set SAlg ->
Rbar) {
meas:
is_semipremeasure λ}
(
has_none :
salg_in pre_event_none)
(
none: λ (
exist _ _ has_none) = 0)
(
R:
list (
salg_set SAlg))
(
S:
nat ->
list (
salg_set SAlg)):
ForallOrdPairs pre_event_disjoint (
map salg_pre R) ->
pre_collection_is_pairwise_disjoint (
fun x =>
pre_list_union (
map salg_pre (
S x))) ->
(
forall n,
ForallOrdPairs pre_event_disjoint (
map salg_pre (
S n))) ->
pre_event_equiv (
pre_list_union (
map salg_pre R)) (
pre_union_of_collection (
fun x => (
pre_list_union (
map salg_pre (
S x))))) ->
list_Rbar_sum (
map λ
R) =
ELim_seq (
sum_Rbar_n (
fun n :
nat => (
list_Rbar_sum (
map λ (
S n))))).
Proof.
Definition premeasure_of_semipremeasure (λ:
salg_set SAlg ->
Rbar) :
(
alg_set (
SemiAlgebra_Algebra SAlg) ->
Rbar).
Proof.
Global Instance premeasure_of_semipremeasure_proper (λ:
salg_set SAlg ->
Rbar) {
meas:
is_semipremeasure λ} :
Proper (
alg_equiv ==>
eq) (
premeasure_of_semipremeasure λ).
Proof.
Global Instance premeasure_of_semipremeasure_premeasure
(λ:
salg_set SAlg ->
Rbar) {
meas:
is_semipremeasure λ}
(
has_none :
salg_in pre_event_none)
(
none: λ (
exist _ _ has_none) = 0)
:
is_premeasure (
premeasure_of_semipremeasure λ).
Proof.
constructor.
-
now apply premeasure_of_semipremeasure_proper.
-
unfold premeasure_of_semipremeasure.
unfold alg_none.
repeat match_destr.
destruct a.
rewrite (
semipremeasure_disjoint_list_irrel _ _ nil).
+
now simpl.
+
unfold salg_pre,
salg_set;
simpl.
now rewrite list_dep_zip_map1.
+
simpl;
constructor.
+
unfold salg_pre,
salg_set;
simpl.
rewrite list_dep_zip_map1.
rewrite pre_list_union_nil.
now symmetry.
-
intros.
unfold premeasure_of_semipremeasure.
destruct a.
repeat match_destr.
apply list_Rbar_sum_nneg_nneg;
intros.
apply in_map_iff in H.
destruct H as [? [??]];
subst.
apply semipremeasure_nneg.
-
intros.
unfold premeasure_of_semipremeasure at 1.
repeat match_destr.
destruct a as [??].
assert (
forall i,
exists S,
ForallOrdPairs pre_event_disjoint S /\
pre_event_equiv (
B i) (
pre_list_union S) /\
exists (
F:
Forall salg_in S),
premeasure_of_semipremeasure λ (
B i) =
(
list_Rbar_sum (
map λ (
list_dep_zip _ F)))).
{
intros.
unfold premeasure_of_semipremeasure.
repeat match_destr.
destruct a0.
eauto.
}
apply choice in H2.
destruct H2 as [
l HH].
assert (
forall x,
exists F :
Forall salg_in (
l x),
premeasure_of_semipremeasure λ (
B x) =
list_Rbar_sum (
map λ (
list_dep_zip (
l x)
F))).
{
intros a.
destruct (
HH a);
tauto.
}
apply (
Coq.Logic.ChoiceFacts.non_dep_dep_functional_choice choice)
in H2.
destruct H2 as [??].
transitivity (
ELim_seq (
sum_Rbar_n (
fun n :
nat =>
list_Rbar_sum (
map λ (
list_dep_zip (
l n) (
x0 n)))))).
+
apply (
semipremeasure_disjoint_list_countable_list_irrel_with_default _ has_none none);
trivial.
*
unfold salg_pre,
salg_set;
simpl.
now rewrite list_dep_zip_map1.
*
unfold salg_pre,
salg_set;
simpl.
eapply pre_collection_is_pairwise_disjoint_pre_event_sub_proper
;
try eapply H.
intros ?.
rewrite list_dep_zip_map1.
destruct (
HH a)
as [?[??]].
rewrite H4.
reflexivity.
*
intros.
unfold salg_pre,
salg_set;
simpl.
rewrite list_dep_zip_map1.
now destruct (
HH n).
*
unfold salg_pre,
salg_set;
simpl.
repeat rewrite list_dep_zip_map1.
intros ?.
split.
--
intros HH2.
apply H1 in HH2.
destruct HH2 as [
n HH2].
exists n.
rewrite list_dep_zip_map1.
destruct (
HH n)
as [
_ [
HH3 _]].
now apply HH3.
--
intros [?[?[??]]].
rewrite list_dep_zip_map1 in H3.
destruct (
HH x2)
as [
_ [
HH3 _]].
apply H1.
exists x2.
apply HH3.
red;
eauto.
+
apply ELim_seq_ext;
intros.
unfold sum_Rbar_n;
f_equal.
apply map_ext;
intros.
auto.
Qed.
Lemma premeasure_of_semipremeasure_same
(λ :
salg_set SAlg ->
Rbar)
{
meas :
is_semipremeasure λ}
x
(
pf1 :
salg_in x)
(
pf2 :
alg_in (
Algebra:=(
SemiAlgebra_Algebra SAlg))
x) :
premeasure_of_semipremeasure λ (
exist _ x pf2) = λ (
exist _ x pf1).
Proof.
End semi_premeasure.
Section caratheodory_semi.
Local Existing Instance Rbar_le_pre.
Local Existing Instance Rbar_le_part.
Context {
T:
Type}.
Context {
SAlg:
SemiAlgebra T}.
Context (
has_none :
salg_in pre_event_none).
Context (λ:
salg_set SAlg ->
Rbar).
Context {
meas:
is_semipremeasure λ}.
Context (
none: λ (
exist _ _ has_none) = 0).
Instance semi_σ :
SigmaAlgebra T
:= μ
_measurable_sa (μ
_outer:=
outer_λ
_outer_measure _
(λ
_meas:=
premeasure_of_semipremeasure_premeasure
_ has_none none))
(
outer_λ (
premeasure_of_semipremeasure λ)).
Lemma semi_σ
_in :
pre_event_sub salg_in (
sa_sigma (
SigmaAlgebra:=
semi_σ)).
Proof.
Lemma semi_σ
_sa_sigma (
x:
salg_set SAlg) :
sa_sigma x.
Proof.
destruct x; simpl.
now apply semi_σ_in.
Qed.
Definition semi_as_semi_σ (
x:
salg_set SAlg) :
event semi_σ
:=
exist _ _ (
semi_σ
_sa_sigma x).
Definition semi_μ :
pre_event T ->
Rbar
:=
outer_λ ((
premeasure_of_semipremeasure λ)).
Instance semi_μ
_measurable :
is_measure (σ:=
semi_σ)
semi_μ.
Proof.
apply μ_measurable_sa_measure.
Qed.
Lemma semi_μ
_λ (
x:
salg_set SAlg) :
semi_μ
x = λ
x.
Proof.
End caratheodory_semi.