Library mathcomp.analysis.measure
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import ssrnat eqtype choice seq fintype order bigop.
From mathcomp Require Import ssralg ssrnum finmap.
Require Import boolp classical_sets reals ereal posnum nngnum topology.
Require Import normedtype sequences cardinality csum.
From HB Require Import structures.
From Coq Require Import ssreflect ssrfun ssrbool.
From mathcomp Require Import ssrnat eqtype choice seq fintype order bigop.
From mathcomp Require Import ssralg ssrnum finmap.
Require Import boolp classical_sets reals ereal posnum nngnum topology.
Require Import normedtype sequences cardinality csum.
From HB Require Import structures.
Measure Theory
semiRingOfSetsType == the type of semirings of sets
ringOfSetsType == the type of rings of sets
algebraOfSetsType == the type of algebras of sets
measurableType == the type of sigma-algebras
sigma_finite A f == the measure f is sigma-finite on A : set T with
T : ringOfSetsType.
{additive_measure set T -> {ereal R}} == type of a function over sets of
elements of type T where R is expected to be a
numFieldType such that this function maps set0 to 0, is
non-negative over measurable sets, and is semi-additive
{measure set T -> {ereal R}} == type of a function over sets of elements
of type T where R is expected to be a numFieldType such
that this function maps set0 to 0, is non-negative over
measurable sets and is semi-sigma-additive
seqDU F == the sequence F_0, F_1 \ F_0, F_2 \ (F_0 U F_1),...
seqD F == the sequence F_0, F_1 \ F_0, F_2 \ F_1,...
Theorems: Boole_inequality, generalized_Boole_inequality
mu.-negligible A == A is mu negligible
{ae mu, forall x, P x} == P holds almost everywhere for the measure mu
{outer_measure set T -> {ereal R}} == type of an outer measure over sets
of elements of type T where R is expected
to be a numFieldType
mu.-measurable X == X is Caratheodory measurable for the outer measure
mu, i.e.,
forall Y, mu X = mu (X `&` Y) + mu (X `&` ~` Y)
measure_is_complete mu == the measure mu is complete
measurable_fun D f == the function f with domain D is measurable
Caratheodory theorem:
caratheodory_type mu := T, where mu : {outer_measure set T -> {ereal R}}
it is a canonical mesurableType copy of T.
caratheodory_measure mu == the restriction of the outer measure mu to the
sigma algebra of Caratheodory measurable sets is a
measure
Remark: sets that are negligible for
caratheodory_measure are Caratheodory measurable
Extension theorem:
measurable_cover X == the set of sequences F such that
- forall i, F i is measurable
- X `<=` \bigcup_i (F i)
Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Reserved Notation "mu .-negligible" (at level 2, format "mu .-negligible").
Reserved Notation "{ 'ae' m , P }" (at level 0, format "{ 'ae' m , P }").
Reserved Notation "mu .-measurable" (at level 2, format "mu .-measurable").
Local Open Scope classical_set_scope.
Local Open Scope ring_scope.
TODO: remove when available in all the Coq versions supported by the CI
(as of today, only in Coq 8.13)
Definition uncurry {A B C : Type} (f : A → B → C)
(p : A × B) : C := match p with (x, y) ⇒ f x y end.
Definition bigcup2 T (A B : set T) : nat → set T :=
fun i ⇒ if i == 0%N then A else if i == 1%N then B else set0.
Lemma bigcup2E T (A B : set T) : \bigcup_i (bigcup2 A B) i = A `|` B.
Notation semiRingOfSetsType := SemiRingOfSets.type.
Notation ringOfSetsType := RingOfSets.type.
Notation algebraOfSetsType := AlgebraOfSets.type.
Notation measurableType := Measurable.type.
Lemma semiRingOfSets_measurableI (A B : set T) :
measurable A → measurable B → measurable (A `&` B).
Definition diff_fsets := (fun A B : set T ⇒ ([fset (A `&` ~` B)%classic])%fset).
Lemma semiRingOfSets_measurableD (A B C : set T) :
measurable A → measurable B → C \in diff_fsets A B → measurable C.
Lemma semiRingOfSets_diff_fsetsE A B :
A `\` B = \big[setU/set0]_(X <- enum_fset (diff_fsets A B)) X.
Lemma semiRingOfSets_diff_fsets_disjoint A B C D : C != D →
C \in diff_fsets A B → D \in diff_fsets A B → C `&` D = set0.
Lemma measurableT : measurable (@setT T).
Obligation Tactic := idtac.
Lemma algebraOfSets_measurableU (A B : set T) :
measurable A → measurable B → measurable (A `|` B).
Lemma algebraOfSets_measurableC (A : set T) : measurable A → measurable (~` A).
Hint Extern 0 (measurable set0) ⇒ solve [apply: measurable0] : core.
Hint Extern 0 (measurable setT) ⇒ solve [apply: measurableT] : core.
Section ringofsets_lemmas.
Variables T : ringOfSetsType.
Implicit Types A B : set T.
Lemma bigsetU_measurable I r (P : pred I) (F : I → set T) :
(∀ i, P i → measurable (F i)) →
measurable (\big[setU/set0]_(i <- r | P i) F i).
Lemma measurableD A B : measurable A → measurable B → measurable (A `\` B).
End ringofsets_lemmas.
Section algebraofsets_lemmas.
Variables T : algebraOfSetsType.
Implicit Types A B : set T.
Lemma measurableC A : measurable A → measurable (~` A).
Lemma bigsetI_measurable I r (P : pred I) (F : I → set T) :
(∀ i, P i → measurable (F i)) →
measurable (\big[setI/setT]_(i <- r | P i) F i).
End algebraofsets_lemmas.
Section measurable_lemmas.
Variables T : measurableType.
Implicit Types A B : set T.
Lemma bigcup_measurable (F : (set T)^nat) (P : set nat) :
(∀ k, P k → measurable (F k)) → measurable (\bigcup_(i in P) F i).
Lemma bigcap_measurable (F : (set T)^nat) (P : set nat) :
(∀ k, P k → measurable (F k)) → measurable (\bigcap_(i in P) F i).
Lemma measurable_bigcap (F : (set T)^nat) :
(∀ i, measurable (F i)) → measurable (\bigcap_i (F i)).
End measurable_lemmas.
Local Open Scope ereal_scope.
Definition sigma_finite (R : numDomainType) (T : ringOfSetsType) (A : set T)
(mu : set T → \bar R) :=
exists2 F : (set T)^nat,
A = \bigcup_(i : nat) F i &
∀ i, measurable (F i) ∧ mu (F i) < +oo.
Section semi_additivity.
Variables (R : numFieldType) (T : semiRingOfSetsType) (mu : set T → \bar R).
Definition semi_additive2 := ∀ A B, measurable A → measurable B →
measurable (A `|` B) →
A `&` B = set0 → mu (A `|` B) = mu A + mu B.
Definition semi_additive :=
∀ A, (∀ i : nat, measurable (A i)) → trivIset setT A →
(∀ n, measurable (\big[setU/set0]_(i < n) A i)) →
∀ n, mu (\big[setU/set0]_(i < n) A i) = \sum_(i < n) mu (A i).
Definition semi_sigma_additive :=
∀ A, (∀ i : nat, measurable (A i)) → trivIset setT A →
measurable (\bigcup_n A n) →
(fun n ⇒ \sum_(i < n) mu (A i)) --> mu (\bigcup_n A n).
Definition additive2 := ∀ A B, measurable A → measurable B →
A `&` B = set0 → mu (A `|` B) = mu A + mu B.
Definition additive :=
∀ A, (∀ i : nat, measurable (A i)) → trivIset setT A →
∀ n, mu (\big[setU/set0]_(i < n) A i) = \sum_(i < n) mu (A i).
Definition sigma_additive :=
∀ A, (∀ i : nat, measurable (A i)) → trivIset setT A →
(fun n ⇒ \sum_(i < n) mu (A i)) --> mu (\bigcup_n A n).
Lemma semi_additive2P : mu set0 = 0 → semi_additive ↔ semi_additive2.
End semi_additivity.
Section additivity.
Variables (R : numFieldType) (T : ringOfSetsType) (mu : set T → \bar R).
Lemma semi_additiveE : semi_additive mu = additive mu.
Lemma semi_additive2E : semi_additive2 mu = additive2 mu.
Lemma additive2P : mu set0 = 0 → additive mu ↔ additive2 mu.
End additivity.
Lemma semi_sigma_additive_is_additive
(R : realFieldType (*TODO: numFieldType if possible?*))
(X : semiRingOfSetsType) (mu : set X → \bar R) :
mu set0 = 0 → semi_sigma_additive mu → semi_additive mu.
Lemma semi_sigma_additiveE
(R : numFieldType) (X : measurableType) (mu : set X → \bar R) :
semi_sigma_additive mu = sigma_additive mu.
Lemma sigma_additive_is_additive
(R : realFieldType) (X : measurableType) (mu : set X → \bar R) :
mu set0 = 0 → sigma_additive mu → additive mu.
Module AdditiveMeasure.
Section ClassDef.
Variables (R : numFieldType) (T : semiRingOfSetsType).
Record axioms (mu : set T → \bar R) := Axioms {
_ : mu set0 = 0 ;
_ : ∀ x, measurable x → 0 ≤ mu x ;
_ : semi_additive2 mu }.
Structure map (phUV : phant (set T → \bar R)) :=
Pack {apply : set T → \bar R ; _ : axioms apply}.
Variables (phUV : phant (set T → \bar R)) (f g : set T → \bar R).
Variable (cF : map phUV).
Definition class := let: Pack _ c as cF' := cF return axioms cF' in c.
Definition clone fA of phant_id g (apply cF) & phant_id fA class :=
@Pack phUV f fA.
End ClassDef.
Module Exports.
Notation additive_measure f := (axioms f).
Coercion apply : map >-> Funclass.
Notation AdditiveMeasure fA := (Pack (Phant _) fA).
Notation "{ 'additive_measure' fUV }" := (map (Phant fUV))
(at level 0, format "{ 'additive_measure' fUV }") : ring_scope.
Notation "[ 'additive_measure' 'of' f 'as' g ]" := (@clone _ _ _ f g _ _ idfun id)
(at level 0, format "[ 'additive_measure' 'of' f 'as' g ]") : form_scope.
Notation "[ 'additive_measure' 'of' f ]" := (@clone _ _ _ f f _ _ id id)
(at level 0, format "[ 'additive_measure' 'of' f ]") : form_scope.
End Exports.
End AdditiveMeasure.
Include AdditiveMeasure.Exports.
Section additive_measure_on_semiring_of_sets.
Variables (R : realFieldType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}).
Lemma measure0 : mu set0 = 0.
Hint Resolve measure0 : core.
Lemma measure_ge0 : ∀ x, measurable x → 0 ≤ mu x.
Hint Resolve measure_ge0 : core.
Lemma measure_semi_additive2 : semi_additive2 mu.
Hint Resolve measure_semi_additive2 : core.
Lemma measure_semi_additive : semi_additive mu.
End additive_measure_on_semiring_of_sets.
Hint Resolve measure0 measure_ge0 measure_semi_additive2
measure_semi_additive : core.
Section additive_measure_on_ring_of_sets.
Variables (R : realFieldType) (T : ringOfSetsType)
(mu : {additive_measure set T → \bar R}).
Lemma measureU : additive2 mu.
Lemma measure_bigsetU : additive mu.
End additive_measure_on_ring_of_sets.
Hint Resolve measureU measure_bigsetU : core.
Module Measure.
Section ClassDef.
Variables (R : numFieldType) (T : semiRingOfSetsType).
Record axioms (mu : set T → \bar R) := Axioms {
_ : mu set0 = 0 ;
_ : ∀ x, measurable x → 0 ≤ mu x ;
_ : semi_sigma_additive mu }.
Structure map (phUV : phant (set T → \bar R)) :=
Pack {apply : set T → \bar R ; _ : axioms apply}.
Variables (phUV : phant (set T → \bar R)) (f g : set T → \bar R).
Variable (cF : map phUV).
Definition class := let: Pack _ c as cF' := cF return axioms cF' in c.
Definition clone fA of phant_id g (apply cF) & phant_id fA class :=
@Pack phUV f fA.
End ClassDef.
Module Exports.
Notation is_measure f := (axioms f).
Coercion apply : map >-> Funclass.
Notation Measure fA := (Pack (Phant _) fA).
Notation "{ 'measure' fUV }" := (map (Phant fUV))
(at level 0, format "{ 'measure' fUV }") : ring_scope.
Notation "[ 'measure' 'of' f 'as' g ]" := (@clone _ _ _ f g _ _ idfun id)
(at level 0, format "[ 'measure' 'of' f 'as' g ]") : form_scope.
Notation "[ 'measure' 'of' f ]" := (@clone _ _ _ f f _ _ id id)
(at level 0, format "[ 'measure' 'of' f ]") : form_scope.
End Exports.
End Measure.
Include Measure.Exports.
Section measure_lemmas.
Variables (R : numFieldType) (T : semiRingOfSetsType).
Variable mu : {measure set T → \bar R}.
Lemma measure_semi_sigma_additive : semi_sigma_additive mu.
End measure_lemmas.
Section measure_lemmas.
Variables (R : numFieldType) (T : measurableType).
Variable mu : {measure set T → \bar R}.
Lemma measure_sigma_additive : sigma_additive mu.
End measure_lemmas.
Hint Extern 0 (_ set0 = 0) ⇒ solve [apply: measure0] : core.
Hint Extern 0 (sigma_additive _) ⇒
solve [apply: measure_sigma_additive] : core.
Section measure_is_additive_measure.
Variables (R : realFieldType) (T : semiRingOfSetsType)
(mu : {measure set T → \bar R}).
Lemma measure_is_additive_measure : additive_measure mu.
Canonical measure_additive_measure :=
AdditiveMeasure measure_is_additive_measure.
End measure_is_additive_measure.
Coercion measure_additive_measure : Measure.map >-> AdditiveMeasure.map.
(p : A × B) : C := match p with (x, y) ⇒ f x y end.
Definition bigcup2 T (A B : set T) : nat → set T :=
fun i ⇒ if i == 0%N then A else if i == 1%N then B else set0.
Lemma bigcup2E T (A B : set T) : \bigcup_i (bigcup2 A B) i = A `|` B.
Notation semiRingOfSetsType := SemiRingOfSets.type.
Notation ringOfSetsType := RingOfSets.type.
Notation algebraOfSetsType := AlgebraOfSets.type.
Notation measurableType := Measurable.type.
Lemma semiRingOfSets_measurableI (A B : set T) :
measurable A → measurable B → measurable (A `&` B).
Definition diff_fsets := (fun A B : set T ⇒ ([fset (A `&` ~` B)%classic])%fset).
Lemma semiRingOfSets_measurableD (A B C : set T) :
measurable A → measurable B → C \in diff_fsets A B → measurable C.
Lemma semiRingOfSets_diff_fsetsE A B :
A `\` B = \big[setU/set0]_(X <- enum_fset (diff_fsets A B)) X.
Lemma semiRingOfSets_diff_fsets_disjoint A B C D : C != D →
C \in diff_fsets A B → D \in diff_fsets A B → C `&` D = set0.
Lemma measurableT : measurable (@setT T).
Obligation Tactic := idtac.
Lemma algebraOfSets_measurableU (A B : set T) :
measurable A → measurable B → measurable (A `|` B).
Lemma algebraOfSets_measurableC (A : set T) : measurable A → measurable (~` A).
Hint Extern 0 (measurable set0) ⇒ solve [apply: measurable0] : core.
Hint Extern 0 (measurable setT) ⇒ solve [apply: measurableT] : core.
Section ringofsets_lemmas.
Variables T : ringOfSetsType.
Implicit Types A B : set T.
Lemma bigsetU_measurable I r (P : pred I) (F : I → set T) :
(∀ i, P i → measurable (F i)) →
measurable (\big[setU/set0]_(i <- r | P i) F i).
Lemma measurableD A B : measurable A → measurable B → measurable (A `\` B).
End ringofsets_lemmas.
Section algebraofsets_lemmas.
Variables T : algebraOfSetsType.
Implicit Types A B : set T.
Lemma measurableC A : measurable A → measurable (~` A).
Lemma bigsetI_measurable I r (P : pred I) (F : I → set T) :
(∀ i, P i → measurable (F i)) →
measurable (\big[setI/setT]_(i <- r | P i) F i).
End algebraofsets_lemmas.
Section measurable_lemmas.
Variables T : measurableType.
Implicit Types A B : set T.
Lemma bigcup_measurable (F : (set T)^nat) (P : set nat) :
(∀ k, P k → measurable (F k)) → measurable (\bigcup_(i in P) F i).
Lemma bigcap_measurable (F : (set T)^nat) (P : set nat) :
(∀ k, P k → measurable (F k)) → measurable (\bigcap_(i in P) F i).
Lemma measurable_bigcap (F : (set T)^nat) :
(∀ i, measurable (F i)) → measurable (\bigcap_i (F i)).
End measurable_lemmas.
Local Open Scope ereal_scope.
Definition sigma_finite (R : numDomainType) (T : ringOfSetsType) (A : set T)
(mu : set T → \bar R) :=
exists2 F : (set T)^nat,
A = \bigcup_(i : nat) F i &
∀ i, measurable (F i) ∧ mu (F i) < +oo.
Section semi_additivity.
Variables (R : numFieldType) (T : semiRingOfSetsType) (mu : set T → \bar R).
Definition semi_additive2 := ∀ A B, measurable A → measurable B →
measurable (A `|` B) →
A `&` B = set0 → mu (A `|` B) = mu A + mu B.
Definition semi_additive :=
∀ A, (∀ i : nat, measurable (A i)) → trivIset setT A →
(∀ n, measurable (\big[setU/set0]_(i < n) A i)) →
∀ n, mu (\big[setU/set0]_(i < n) A i) = \sum_(i < n) mu (A i).
Definition semi_sigma_additive :=
∀ A, (∀ i : nat, measurable (A i)) → trivIset setT A →
measurable (\bigcup_n A n) →
(fun n ⇒ \sum_(i < n) mu (A i)) --> mu (\bigcup_n A n).
Definition additive2 := ∀ A B, measurable A → measurable B →
A `&` B = set0 → mu (A `|` B) = mu A + mu B.
Definition additive :=
∀ A, (∀ i : nat, measurable (A i)) → trivIset setT A →
∀ n, mu (\big[setU/set0]_(i < n) A i) = \sum_(i < n) mu (A i).
Definition sigma_additive :=
∀ A, (∀ i : nat, measurable (A i)) → trivIset setT A →
(fun n ⇒ \sum_(i < n) mu (A i)) --> mu (\bigcup_n A n).
Lemma semi_additive2P : mu set0 = 0 → semi_additive ↔ semi_additive2.
End semi_additivity.
Section additivity.
Variables (R : numFieldType) (T : ringOfSetsType) (mu : set T → \bar R).
Lemma semi_additiveE : semi_additive mu = additive mu.
Lemma semi_additive2E : semi_additive2 mu = additive2 mu.
Lemma additive2P : mu set0 = 0 → additive mu ↔ additive2 mu.
End additivity.
Lemma semi_sigma_additive_is_additive
(R : realFieldType (*TODO: numFieldType if possible?*))
(X : semiRingOfSetsType) (mu : set X → \bar R) :
mu set0 = 0 → semi_sigma_additive mu → semi_additive mu.
Lemma semi_sigma_additiveE
(R : numFieldType) (X : measurableType) (mu : set X → \bar R) :
semi_sigma_additive mu = sigma_additive mu.
Lemma sigma_additive_is_additive
(R : realFieldType) (X : measurableType) (mu : set X → \bar R) :
mu set0 = 0 → sigma_additive mu → additive mu.
Module AdditiveMeasure.
Section ClassDef.
Variables (R : numFieldType) (T : semiRingOfSetsType).
Record axioms (mu : set T → \bar R) := Axioms {
_ : mu set0 = 0 ;
_ : ∀ x, measurable x → 0 ≤ mu x ;
_ : semi_additive2 mu }.
Structure map (phUV : phant (set T → \bar R)) :=
Pack {apply : set T → \bar R ; _ : axioms apply}.
Variables (phUV : phant (set T → \bar R)) (f g : set T → \bar R).
Variable (cF : map phUV).
Definition class := let: Pack _ c as cF' := cF return axioms cF' in c.
Definition clone fA of phant_id g (apply cF) & phant_id fA class :=
@Pack phUV f fA.
End ClassDef.
Module Exports.
Notation additive_measure f := (axioms f).
Coercion apply : map >-> Funclass.
Notation AdditiveMeasure fA := (Pack (Phant _) fA).
Notation "{ 'additive_measure' fUV }" := (map (Phant fUV))
(at level 0, format "{ 'additive_measure' fUV }") : ring_scope.
Notation "[ 'additive_measure' 'of' f 'as' g ]" := (@clone _ _ _ f g _ _ idfun id)
(at level 0, format "[ 'additive_measure' 'of' f 'as' g ]") : form_scope.
Notation "[ 'additive_measure' 'of' f ]" := (@clone _ _ _ f f _ _ id id)
(at level 0, format "[ 'additive_measure' 'of' f ]") : form_scope.
End Exports.
End AdditiveMeasure.
Include AdditiveMeasure.Exports.
Section additive_measure_on_semiring_of_sets.
Variables (R : realFieldType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}).
Lemma measure0 : mu set0 = 0.
Hint Resolve measure0 : core.
Lemma measure_ge0 : ∀ x, measurable x → 0 ≤ mu x.
Hint Resolve measure_ge0 : core.
Lemma measure_semi_additive2 : semi_additive2 mu.
Hint Resolve measure_semi_additive2 : core.
Lemma measure_semi_additive : semi_additive mu.
End additive_measure_on_semiring_of_sets.
Hint Resolve measure0 measure_ge0 measure_semi_additive2
measure_semi_additive : core.
Section additive_measure_on_ring_of_sets.
Variables (R : realFieldType) (T : ringOfSetsType)
(mu : {additive_measure set T → \bar R}).
Lemma measureU : additive2 mu.
Lemma measure_bigsetU : additive mu.
End additive_measure_on_ring_of_sets.
Hint Resolve measureU measure_bigsetU : core.
Module Measure.
Section ClassDef.
Variables (R : numFieldType) (T : semiRingOfSetsType).
Record axioms (mu : set T → \bar R) := Axioms {
_ : mu set0 = 0 ;
_ : ∀ x, measurable x → 0 ≤ mu x ;
_ : semi_sigma_additive mu }.
Structure map (phUV : phant (set T → \bar R)) :=
Pack {apply : set T → \bar R ; _ : axioms apply}.
Variables (phUV : phant (set T → \bar R)) (f g : set T → \bar R).
Variable (cF : map phUV).
Definition class := let: Pack _ c as cF' := cF return axioms cF' in c.
Definition clone fA of phant_id g (apply cF) & phant_id fA class :=
@Pack phUV f fA.
End ClassDef.
Module Exports.
Notation is_measure f := (axioms f).
Coercion apply : map >-> Funclass.
Notation Measure fA := (Pack (Phant _) fA).
Notation "{ 'measure' fUV }" := (map (Phant fUV))
(at level 0, format "{ 'measure' fUV }") : ring_scope.
Notation "[ 'measure' 'of' f 'as' g ]" := (@clone _ _ _ f g _ _ idfun id)
(at level 0, format "[ 'measure' 'of' f 'as' g ]") : form_scope.
Notation "[ 'measure' 'of' f ]" := (@clone _ _ _ f f _ _ id id)
(at level 0, format "[ 'measure' 'of' f ]") : form_scope.
End Exports.
End Measure.
Include Measure.Exports.
Section measure_lemmas.
Variables (R : numFieldType) (T : semiRingOfSetsType).
Variable mu : {measure set T → \bar R}.
Lemma measure_semi_sigma_additive : semi_sigma_additive mu.
End measure_lemmas.
Section measure_lemmas.
Variables (R : numFieldType) (T : measurableType).
Variable mu : {measure set T → \bar R}.
Lemma measure_sigma_additive : sigma_additive mu.
End measure_lemmas.
Hint Extern 0 (_ set0 = 0) ⇒ solve [apply: measure0] : core.
Hint Extern 0 (sigma_additive _) ⇒
solve [apply: measure_sigma_additive] : core.
Section measure_is_additive_measure.
Variables (R : realFieldType) (T : semiRingOfSetsType)
(mu : {measure set T → \bar R}).
Lemma measure_is_additive_measure : additive_measure mu.
Canonical measure_additive_measure :=
AdditiveMeasure measure_is_additive_measure.
End measure_is_additive_measure.
Coercion measure_additive_measure : Measure.map >-> AdditiveMeasure.map.
measure is monotone
Lemma le_measure (R : realFieldType) (T : ringOfSetsType)
(mu : {additive_measure set T → \bar R}) :
{in [set x | measurable x] &, {homo mu : A B / A `<=` B >-> A ≤ B}}.
Section measureD.
Variables (R : realFieldType) (T : ringOfSetsType).
Variable mu : {measure set T → \bar R}.
Lemma measureDI A B : measurable A → measurable B →
mu A = mu (A `\` B) + mu (A `&` B).
Lemma measureD A B : measurable A → measurable B →
mu A < +oo → mu (A `\` B) = mu A - mu (A `&` B).
End measureD.
Section seqDU.
Variables (T : Type).
Implicit Types F : (set T)^nat.
Definition seqDU F n := F n `\` \big[setU/set0]_(k < n) F k.
Lemma trivIset_seqDU F : trivIset setT (seqDU F).
Lemma bigsetU_seqDU F n :
\big[setU/set0]_(k < n) F k = \big[setU/set0]_(k < n) seqDU F k.
Lemma seqDU_bigcup_eq F : \bigcup_k F k = \bigcup_k seqDU F k.
End seqDU.
Section seqD.
Variable T : Type.
Implicit Types F : (set T) ^nat.
Definition seqD F := fun n ⇒ if n isn't n'.+1 then F O else F n `\` F n'.
Lemma seqDUE F : nondecreasing_seq F → seqDU F = seqD F.
Lemma trivIset_seqD F : nondecreasing_seq F → trivIset setT (seqD F).
Lemma bigsetU_seqD F n :
\big[setU/set0]_(i < n) F i = \big[setU/set0]_(i < n) seqD F i.
Lemma setU_seqD F : nondecreasing_seq F →
∀ n, F n.+1 = F n `|` seqD F n.+1.
Lemma eq_bigsetU_seqD F n : nondecreasing_seq F →
F n = \big[setU/set0]_(i < n.+1) seqD F i.
Lemma eq_bigcup_seqD F : \bigcup_n F n = \bigcup_n seqD F n.
Lemma eq_bigcup_seqD_bigsetU F :
\bigcup_n (seqD (fun n ⇒ \big[setU/set0]_(i < n.+1) F i) n) = \bigcup_n F n.
End seqD.
(mu : {additive_measure set T → \bar R}) :
{in [set x | measurable x] &, {homo mu : A B / A `<=` B >-> A ≤ B}}.
Section measureD.
Variables (R : realFieldType) (T : ringOfSetsType).
Variable mu : {measure set T → \bar R}.
Lemma measureDI A B : measurable A → measurable B →
mu A = mu (A `\` B) + mu (A `&` B).
Lemma measureD A B : measurable A → measurable B →
mu A < +oo → mu (A `\` B) = mu A - mu (A `&` B).
End measureD.
Section seqDU.
Variables (T : Type).
Implicit Types F : (set T)^nat.
Definition seqDU F n := F n `\` \big[setU/set0]_(k < n) F k.
Lemma trivIset_seqDU F : trivIset setT (seqDU F).
Lemma bigsetU_seqDU F n :
\big[setU/set0]_(k < n) F k = \big[setU/set0]_(k < n) seqDU F k.
Lemma seqDU_bigcup_eq F : \bigcup_k F k = \bigcup_k seqDU F k.
End seqDU.
Section seqD.
Variable T : Type.
Implicit Types F : (set T) ^nat.
Definition seqD F := fun n ⇒ if n isn't n'.+1 then F O else F n `\` F n'.
Lemma seqDUE F : nondecreasing_seq F → seqDU F = seqD F.
Lemma trivIset_seqD F : nondecreasing_seq F → trivIset setT (seqD F).
Lemma bigsetU_seqD F n :
\big[setU/set0]_(i < n) F i = \big[setU/set0]_(i < n) seqD F i.
Lemma setU_seqD F : nondecreasing_seq F →
∀ n, F n.+1 = F n `|` seqD F n.+1.
Lemma eq_bigsetU_seqD F n : nondecreasing_seq F →
F n = \big[setU/set0]_(i < n.+1) seqD F i.
Lemma eq_bigcup_seqD F : \bigcup_n F n = \bigcup_n seqD F n.
Lemma eq_bigcup_seqD_bigsetU F :
\bigcup_n (seqD (fun n ⇒ \big[setU/set0]_(i < n.+1) F i) n) = \bigcup_n F n.
End seqD.
401,p.43 measure is continuous from below
Lemma cvg_mu_inc (R : realFieldType) (T : ringOfSetsType)
(mu : {measure set T → \bar R}) (F : (set T) ^nat) :
(∀ i, measurable (F i)) → measurable (\bigcup_n F n) →
nondecreasing_seq F →
mu \o F --> mu (\bigcup_n F n).
Section boole_inequality.
Variables (R : realFieldType) (T : ringOfSetsType).
Variables (mu : {additive_measure set T → \bar R}).
Theorem Boole_inequality (A : (set T) ^nat) : (∀ i, measurable (A i)) →
∀ n, mu (\big[setU/set0]_(i < n) A i) ≤ \sum_(i < n) mu (A i).
End boole_inequality.
Notation le_mu_bigsetU := Boole_inequality.
Section sigma_finite_lemma.
Variables (R : realFieldType) (T : ringOfSetsType) (A : set T)
(mu : {additive_measure set T → \bar R}).
Lemma sigma_finiteP : sigma_finite A mu →
exists2 F, A = \bigcup_i F i &
nondecreasing_seq F ∧ ∀ i, measurable (F i) ∧ mu (F i) < +oo.
End sigma_finite_lemma.
Section generalized_boole_inequality.
Variables (R : realType) (T : ringOfSetsType).
Variable (mu : {measure set T → \bar R}).
(mu : {measure set T → \bar R}) (F : (set T) ^nat) :
(∀ i, measurable (F i)) → measurable (\bigcup_n F n) →
nondecreasing_seq F →
mu \o F --> mu (\bigcup_n F n).
Section boole_inequality.
Variables (R : realFieldType) (T : ringOfSetsType).
Variables (mu : {additive_measure set T → \bar R}).
Theorem Boole_inequality (A : (set T) ^nat) : (∀ i, measurable (A i)) →
∀ n, mu (\big[setU/set0]_(i < n) A i) ≤ \sum_(i < n) mu (A i).
End boole_inequality.
Notation le_mu_bigsetU := Boole_inequality.
Section sigma_finite_lemma.
Variables (R : realFieldType) (T : ringOfSetsType) (A : set T)
(mu : {additive_measure set T → \bar R}).
Lemma sigma_finiteP : sigma_finite A mu →
exists2 F, A = \bigcup_i F i &
nondecreasing_seq F ∧ ∀ i, measurable (F i) ∧ mu (F i) < +oo.
End sigma_finite_lemma.
Section generalized_boole_inequality.
Variables (R : realType) (T : ringOfSetsType).
Variable (mu : {measure set T → \bar R}).
404,p.44 measure satisfies generalized Boole's inequality
Theorem generalized_Boole_inequality (A : (set T) ^nat) :
(∀ i, measurable (A i)) → measurable (\bigcup_n A n) →
mu (\bigcup_n A n) ≤ \sum_(i <oo) mu (A i).
End generalized_boole_inequality.
Notation le_mu_bigcup := generalized_Boole_inequality.
Section negligible.
Variables (R : realFieldType) (T : ringOfSetsType).
Definition negligible (mu : set T → \bar R) (N : set T) :=
∃ A : set T, [/\ measurable A, mu A = 0 & N `<=` A].
Lemma negligibleP (mu : {measure _ → _}) A :
measurable A → mu.-negligible A ↔ mu A = 0.
Lemma negligible_set0 (mu : {measure _ → _}) : mu.-negligible set0.
Definition almost_everywhere (mu : set T → \bar R) (P : T → Prop)
& (phantom Prop (∀ x, P x)) :=
mu.-negligible (~` [set x | P x]).
Lemma aeW (mu : {measure _ → _}) (P : T → Prop) :
(∀ x, P x) → {ae mu, ∀ x, P x}.
End negligible.
Notation "mu .-negligible" := (negligible mu) : type_scope.
Notation "{ 'ae' m , P }" := (almost_everywhere m (inPhantom P)) : type_scope.
Definition sigma_subadditive (R : numFieldType) (T : Type)
(mu : set T → \bar R) := ∀ (A : (set T) ^nat),
mu (\bigcup_n (A n)) ≤ \sum_(i <oo) mu (A i).
Module OuterMeasure.
Section ClassDef.
Variables (R : numFieldType) (T : Type).
Record axioms (mu : set T → \bar R) := Axioms {
_ : mu set0 = 0 ;
_ : ∀ x, 0 ≤ mu x ;
_ : {homo mu : A B / A `<=` B >-> A ≤ B} ;
_ : sigma_subadditive mu }.
Structure map (phUV : phant (set T → \bar R)) :=
Pack {apply : set T → \bar R ; _ : axioms apply}.
Variables (phUV : phant (set T → \bar R)) (f g : set T → \bar R).
Variable (cF : map phUV).
Definition class := let: Pack _ c as cF' := cF return axioms cF' in c.
Definition clone fA of phant_id g (apply cF) & phant_id fA class :=
@Pack phUV f fA.
End ClassDef.
Module Exports.
Notation outer_measure f := (axioms f).
Coercion apply : map >-> Funclass.
Notation OuterMeasure fA := (Pack (Phant _) fA).
Notation "{ 'outer_measure' fUV }" := (map (Phant fUV))
(at level 0, format "{ 'outer_measure' fUV }") : ring_scope.
Notation "[ 'outer_measure' 'of' f 'as' g ]" := (@clone _ _ _ f g _ _ idfun id)
(at level 0, format "[ 'outer_measure' 'of' f 'as' g ]") : form_scope.
Notation "[ 'outer_measure' 'of' f ]" := (@clone _ _ _ f f _ _ id id)
(at level 0, format "[ 'outer_measure' 'of' f ]") : form_scope.
End Exports.
End OuterMeasure.
Include OuterMeasure.Exports.
Section outer_measure_lemmas.
Variables (R : numFieldType) (T : Type).
Variable mu : {outer_measure set T → \bar R}.
Lemma outer_measure0 : mu set0 = 0.
Lemma outer_measure_ge0 : ∀ x, 0 ≤ mu x.
Lemma le_outer_measure : {homo mu : A B / A `<=` B >-> A ≤ B}.
Lemma outer_measure_sigma_subadditive : sigma_subadditive mu.
End outer_measure_lemmas.
Hint Extern 0 (_ set0 = 0) ⇒ solve [apply: outer_measure0] : core.
Hint Extern 0 (sigma_subadditive _) ⇒
solve [apply: outer_measure_sigma_subadditive] : core.
Lemma le_outer_measureIC (R : realFieldType) T
(mu : {outer_measure set T → \bar R}) (A X : set T) :
mu X ≤ mu (X `&` A) + mu (X `&` ~` A).
Definition caratheodory_measurable (R : realType) (T : Type)
(mu : {outer_measure set T → \bar R}) (A : set T) := ∀ X,
mu X = mu (X `&` A) + mu (X `&` ~` A).
Notation "mu .-measurable" := (caratheodory_measurable mu)
(at level 2, format "mu .-measurable") : type_scope.
Lemma le_caratheodory_measurable (R : realType) T
(mu : {outer_measure set T → \bar R}) (A : set T) :
(∀ X, mu (X `&` A) + mu (X `&` ~` A) ≤ mu X) →
mu.-measurable A.
Section caratheodory_theorem_sigma_algebra.
Variables (R : realType) (T : Type) (mu : {outer_measure set T → \bar R}).
Lemma outer_measure_bigcup_lim (A : (set T) ^nat) X :
mu (X `&` \bigcup_k A k) ≤ \sum_(k <oo) mu (X `&` A k).
Let M := mu.-measurable.
Lemma caratheodory_measurable_set0 : M set0.
Lemma caratheodory_measurable_setC A : M A → M (~` A).
Lemma caratheodory_measurable_setU_le (X A B : set T) :
mu.-measurable A → mu.-measurable B →
mu (X `&` (A `|` B)) + mu (X `&` ~` (A `|` B)) ≤ mu X.
Lemma caratheodory_measurable_setU A B : M A → M B → M (A `|` B).
Lemma caratheodory_measurable_bigsetU (A : (set T) ^nat) : (∀ n, M (A n)) →
∀ n, M (\big[setU/set0]_(i < n) A i).
Lemma caratheodory_measurable_setI A B : M A → M B → M (A `&` B).
Lemma caratheodory_measurable_setD A B : M A → M B → M (A `\` B).
Section additive_ext_lemmas.
Variable A B : set T.
Hypothesis (mA : M A) (mB : M B).
Let caratheodory_decomp X :
mu X = mu (X `&` A `&` B) + mu (X `&` A `&` ~` B) +
mu (X `&` ~` A `&` B) + mu (X `&` ~` A `&` ~` B).
Let caratheorody_decompIU X : mu (X `&` (A `|` B)) =
mu (X `&` A `&` B) + mu (X `&` ~` A `&` B) + mu (X `&` A `&` ~` B).
Lemma disjoint_caratheodoryIU X : [disjoint A & B] →
mu (X `&` (A `|` B)) = mu (X `&` A) + mu (X `&` B).
End additive_ext_lemmas.
Lemma caratheodory_additive (A : (set T) ^nat) : (∀ n, M (A n)) →
trivIset setT A → ∀ n X,
mu (X `&` \big[setU/set0]_(i < n) A i) = \sum_(i < n) mu (X `&` A i).
Lemma caratheodory_lim_lee (A : (set T) ^nat) : (∀ n, M (A n)) →
trivIset setT A → ∀ X,
\sum_(k <oo) mu (X `&` A k) + mu (X `&` ~` \bigcup_k A k) ≤ mu X.
Lemma caratheodory_measurable_trivIset_bigcup (A : (set T) ^nat) :
(∀ n, M (A n)) → trivIset setT A → M (\bigcup_k (A k)).
Lemma caratheodory_measurable_bigcup (A : (set T) ^nat) : (∀ n, M (A n)) →
M (\bigcup_k (A k)).
End caratheodory_theorem_sigma_algebra.
Definition caratheodory_type (R : realType) (T : Type)
(mu : {outer_measure set T → \bar R}) := T.
Section caratheodory_sigma_algebra.
Variables (R : realType) (T : Type) (mu : {outer_measure set T → \bar R}).
End caratheodory_sigma_algebra.
Definition measure_is_complete (R : realType) (T : measurableType)
(mu : set T → \bar R) :=
∀ X, mu.-negligible X → measurable X.
Definition measurable_fun (T U : measurableType) (D : set T) (f : T → U) :=
∀ Y, measurable Y → measurable ((f @^-1` Y) `&` D).
Section caratheodory_measure.
Variables (R : realType) (T : Type) (mu : {outer_measure set T → \bar R}).
Lemma caratheodory_measure0 : mu (set0 : set U) = 0.
Lemma caratheodory_measure_ge0 (A : set U) : measurable A → 0 ≤ mu A.
Lemma caratheodory_measure_sigma_additive : semi_sigma_additive (mu : set U → _).
Definition caratheodory_measure_mixin := Measure.Axioms caratheodory_measure0
caratheodory_measure_ge0 caratheodory_measure_sigma_additive.
Definition caratheodory_measure : {measure set U → \bar R} :=
Measure caratheodory_measure_mixin.
Lemma measure_is_complete_caratheodory : measure_is_complete caratheodory_measure.
End caratheodory_measure.
(∀ i, measurable (A i)) → measurable (\bigcup_n A n) →
mu (\bigcup_n A n) ≤ \sum_(i <oo) mu (A i).
End generalized_boole_inequality.
Notation le_mu_bigcup := generalized_Boole_inequality.
Section negligible.
Variables (R : realFieldType) (T : ringOfSetsType).
Definition negligible (mu : set T → \bar R) (N : set T) :=
∃ A : set T, [/\ measurable A, mu A = 0 & N `<=` A].
Lemma negligibleP (mu : {measure _ → _}) A :
measurable A → mu.-negligible A ↔ mu A = 0.
Lemma negligible_set0 (mu : {measure _ → _}) : mu.-negligible set0.
Definition almost_everywhere (mu : set T → \bar R) (P : T → Prop)
& (phantom Prop (∀ x, P x)) :=
mu.-negligible (~` [set x | P x]).
Lemma aeW (mu : {measure _ → _}) (P : T → Prop) :
(∀ x, P x) → {ae mu, ∀ x, P x}.
End negligible.
Notation "mu .-negligible" := (negligible mu) : type_scope.
Notation "{ 'ae' m , P }" := (almost_everywhere m (inPhantom P)) : type_scope.
Definition sigma_subadditive (R : numFieldType) (T : Type)
(mu : set T → \bar R) := ∀ (A : (set T) ^nat),
mu (\bigcup_n (A n)) ≤ \sum_(i <oo) mu (A i).
Module OuterMeasure.
Section ClassDef.
Variables (R : numFieldType) (T : Type).
Record axioms (mu : set T → \bar R) := Axioms {
_ : mu set0 = 0 ;
_ : ∀ x, 0 ≤ mu x ;
_ : {homo mu : A B / A `<=` B >-> A ≤ B} ;
_ : sigma_subadditive mu }.
Structure map (phUV : phant (set T → \bar R)) :=
Pack {apply : set T → \bar R ; _ : axioms apply}.
Variables (phUV : phant (set T → \bar R)) (f g : set T → \bar R).
Variable (cF : map phUV).
Definition class := let: Pack _ c as cF' := cF return axioms cF' in c.
Definition clone fA of phant_id g (apply cF) & phant_id fA class :=
@Pack phUV f fA.
End ClassDef.
Module Exports.
Notation outer_measure f := (axioms f).
Coercion apply : map >-> Funclass.
Notation OuterMeasure fA := (Pack (Phant _) fA).
Notation "{ 'outer_measure' fUV }" := (map (Phant fUV))
(at level 0, format "{ 'outer_measure' fUV }") : ring_scope.
Notation "[ 'outer_measure' 'of' f 'as' g ]" := (@clone _ _ _ f g _ _ idfun id)
(at level 0, format "[ 'outer_measure' 'of' f 'as' g ]") : form_scope.
Notation "[ 'outer_measure' 'of' f ]" := (@clone _ _ _ f f _ _ id id)
(at level 0, format "[ 'outer_measure' 'of' f ]") : form_scope.
End Exports.
End OuterMeasure.
Include OuterMeasure.Exports.
Section outer_measure_lemmas.
Variables (R : numFieldType) (T : Type).
Variable mu : {outer_measure set T → \bar R}.
Lemma outer_measure0 : mu set0 = 0.
Lemma outer_measure_ge0 : ∀ x, 0 ≤ mu x.
Lemma le_outer_measure : {homo mu : A B / A `<=` B >-> A ≤ B}.
Lemma outer_measure_sigma_subadditive : sigma_subadditive mu.
End outer_measure_lemmas.
Hint Extern 0 (_ set0 = 0) ⇒ solve [apply: outer_measure0] : core.
Hint Extern 0 (sigma_subadditive _) ⇒
solve [apply: outer_measure_sigma_subadditive] : core.
Lemma le_outer_measureIC (R : realFieldType) T
(mu : {outer_measure set T → \bar R}) (A X : set T) :
mu X ≤ mu (X `&` A) + mu (X `&` ~` A).
Definition caratheodory_measurable (R : realType) (T : Type)
(mu : {outer_measure set T → \bar R}) (A : set T) := ∀ X,
mu X = mu (X `&` A) + mu (X `&` ~` A).
Notation "mu .-measurable" := (caratheodory_measurable mu)
(at level 2, format "mu .-measurable") : type_scope.
Lemma le_caratheodory_measurable (R : realType) T
(mu : {outer_measure set T → \bar R}) (A : set T) :
(∀ X, mu (X `&` A) + mu (X `&` ~` A) ≤ mu X) →
mu.-measurable A.
Section caratheodory_theorem_sigma_algebra.
Variables (R : realType) (T : Type) (mu : {outer_measure set T → \bar R}).
Lemma outer_measure_bigcup_lim (A : (set T) ^nat) X :
mu (X `&` \bigcup_k A k) ≤ \sum_(k <oo) mu (X `&` A k).
Let M := mu.-measurable.
Lemma caratheodory_measurable_set0 : M set0.
Lemma caratheodory_measurable_setC A : M A → M (~` A).
Lemma caratheodory_measurable_setU_le (X A B : set T) :
mu.-measurable A → mu.-measurable B →
mu (X `&` (A `|` B)) + mu (X `&` ~` (A `|` B)) ≤ mu X.
Lemma caratheodory_measurable_setU A B : M A → M B → M (A `|` B).
Lemma caratheodory_measurable_bigsetU (A : (set T) ^nat) : (∀ n, M (A n)) →
∀ n, M (\big[setU/set0]_(i < n) A i).
Lemma caratheodory_measurable_setI A B : M A → M B → M (A `&` B).
Lemma caratheodory_measurable_setD A B : M A → M B → M (A `\` B).
Section additive_ext_lemmas.
Variable A B : set T.
Hypothesis (mA : M A) (mB : M B).
Let caratheodory_decomp X :
mu X = mu (X `&` A `&` B) + mu (X `&` A `&` ~` B) +
mu (X `&` ~` A `&` B) + mu (X `&` ~` A `&` ~` B).
Let caratheorody_decompIU X : mu (X `&` (A `|` B)) =
mu (X `&` A `&` B) + mu (X `&` ~` A `&` B) + mu (X `&` A `&` ~` B).
Lemma disjoint_caratheodoryIU X : [disjoint A & B] →
mu (X `&` (A `|` B)) = mu (X `&` A) + mu (X `&` B).
End additive_ext_lemmas.
Lemma caratheodory_additive (A : (set T) ^nat) : (∀ n, M (A n)) →
trivIset setT A → ∀ n X,
mu (X `&` \big[setU/set0]_(i < n) A i) = \sum_(i < n) mu (X `&` A i).
Lemma caratheodory_lim_lee (A : (set T) ^nat) : (∀ n, M (A n)) →
trivIset setT A → ∀ X,
\sum_(k <oo) mu (X `&` A k) + mu (X `&` ~` \bigcup_k A k) ≤ mu X.
Lemma caratheodory_measurable_trivIset_bigcup (A : (set T) ^nat) :
(∀ n, M (A n)) → trivIset setT A → M (\bigcup_k (A k)).
Lemma caratheodory_measurable_bigcup (A : (set T) ^nat) : (∀ n, M (A n)) →
M (\bigcup_k (A k)).
End caratheodory_theorem_sigma_algebra.
Definition caratheodory_type (R : realType) (T : Type)
(mu : {outer_measure set T → \bar R}) := T.
Section caratheodory_sigma_algebra.
Variables (R : realType) (T : Type) (mu : {outer_measure set T → \bar R}).
End caratheodory_sigma_algebra.
Definition measure_is_complete (R : realType) (T : measurableType)
(mu : set T → \bar R) :=
∀ X, mu.-negligible X → measurable X.
Definition measurable_fun (T U : measurableType) (D : set T) (f : T → U) :=
∀ Y, measurable Y → measurable ((f @^-1` Y) `&` D).
Section caratheodory_measure.
Variables (R : realType) (T : Type) (mu : {outer_measure set T → \bar R}).
Lemma caratheodory_measure0 : mu (set0 : set U) = 0.
Lemma caratheodory_measure_ge0 (A : set U) : measurable A → 0 ≤ mu A.
Lemma caratheodory_measure_sigma_additive : semi_sigma_additive (mu : set U → _).
Definition caratheodory_measure_mixin := Measure.Axioms caratheodory_measure0
caratheodory_measure_ge0 caratheodory_measure_sigma_additive.
Definition caratheodory_measure : {measure set U → \bar R} :=
Measure caratheodory_measure_mixin.
Lemma measure_is_complete_caratheodory : measure_is_complete caratheodory_measure.
End caratheodory_measure.
TODO: move?
Lemma cvg_geometric_series_half (R : archiFieldType) (r : R) n :
series (fun k ⇒ r / (2 ^ (k + n.+1))%:R : R^o) --> (r / 2 ^+ n : R^o).
Arguments cvg_geometric_series_half {R} _ _.
Lemma epsilon_trick (R : realType) (A : (\bar R)^nat) (e : {nonneg R})
(P : pred nat) : (∀ n, 0 ≤ A n) →
\sum_(i <oo | P i) (A i + (e%:nngnum / (2 ^ i.+1)%:R)%:E) ≤
\sum_(i <oo | P i) A i + e%:nngnum%:E.
Section measurable_cover.
Variable T : ringOfSetsType.
Implicit Types (X : set T) (F : (set T)^nat).
Definition measurable_cover X := [set F : (set T)^nat |
(∀ i, measurable (F i)) ∧ X `<=` \bigcup_k (F k)].
Lemma cover_measurable X F : measurable_cover X F → ∀ k, measurable (F k).
Lemma cover_subset X F : measurable_cover X F → X `<=` \bigcup_k (F k).
End measurable_cover.
Section measure_extension.
Variables (R : realType) (T : ringOfSetsType) (mu : {measure set T → \bar R}).
Definition mu_ext (X : set T) : \bar R :=
ereal_inf [set \sum_(i <oo) mu (A i) | A in measurable_cover X].
Lemma le_mu_ext : {homo mu_ext : A B / A `<=` B >-> A ≤ B}.
Lemma mu_ext_ge0 A : 0 ≤ mu_ext A.
Lemma mu_ext0 : mu_ext set0 = 0.
Lemma measurable_uncurry (G : ((set T)^nat)^nat) (x : nat × nat) :
measurable (G x.1 x.2) → measurable (uncurry G x).
Lemma mu_ext_sigma_subadditive : sigma_subadditive mu_ext.
End measure_extension.
Canonical outer_measure_of_measure (R : realType) (T : ringOfSetsType)
(mu : {measure set T → \bar R}) : {outer_measure set T → \bar R} :=
OuterMeasure (OuterMeasure.Axioms (mu_ext0 mu) (mu_ext_ge0 mu)
(le_mu_ext mu) (mu_ext_sigma_subadditive mu)).
series (fun k ⇒ r / (2 ^ (k + n.+1))%:R : R^o) --> (r / 2 ^+ n : R^o).
Arguments cvg_geometric_series_half {R} _ _.
Lemma epsilon_trick (R : realType) (A : (\bar R)^nat) (e : {nonneg R})
(P : pred nat) : (∀ n, 0 ≤ A n) →
\sum_(i <oo | P i) (A i + (e%:nngnum / (2 ^ i.+1)%:R)%:E) ≤
\sum_(i <oo | P i) A i + e%:nngnum%:E.
Section measurable_cover.
Variable T : ringOfSetsType.
Implicit Types (X : set T) (F : (set T)^nat).
Definition measurable_cover X := [set F : (set T)^nat |
(∀ i, measurable (F i)) ∧ X `<=` \bigcup_k (F k)].
Lemma cover_measurable X F : measurable_cover X F → ∀ k, measurable (F k).
Lemma cover_subset X F : measurable_cover X F → X `<=` \bigcup_k (F k).
End measurable_cover.
Section measure_extension.
Variables (R : realType) (T : ringOfSetsType) (mu : {measure set T → \bar R}).
Definition mu_ext (X : set T) : \bar R :=
ereal_inf [set \sum_(i <oo) mu (A i) | A in measurable_cover X].
Lemma le_mu_ext : {homo mu_ext : A B / A `<=` B >-> A ≤ B}.
Lemma mu_ext_ge0 A : 0 ≤ mu_ext A.
Lemma mu_ext0 : mu_ext set0 = 0.
Lemma measurable_uncurry (G : ((set T)^nat)^nat) (x : nat × nat) :
measurable (G x.1 x.2) → measurable (uncurry G x).
Lemma mu_ext_sigma_subadditive : sigma_subadditive mu_ext.
End measure_extension.
Canonical outer_measure_of_measure (R : realType) (T : ringOfSetsType)
(mu : {measure set T → \bar R}) : {outer_measure set T → \bar R} :=
OuterMeasure (OuterMeasure.Axioms (mu_ext0 mu) (mu_ext_ge0 mu)
(le_mu_ext mu) (mu_ext_sigma_subadditive mu)).