Library mathcomp.analysis.measure
(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *)
From mathcomp Require Import all_ssreflect all_algebra finmap.
Require Import boolp classical_sets mathcomp_extra reals ereal signed.
Require Import functions topology normedtype sequences cardinality esum fsbigop.
Require Import numfun.
From HB Require Import structures.
From mathcomp Require Import all_ssreflect all_algebra finmap.
Require Import boolp classical_sets mathcomp_extra reals ereal signed.
Require Import functions topology normedtype sequences cardinality esum fsbigop.
Require Import numfun.
From HB Require Import structures.
Measure Theory
This files provides a formalization of the basics of measure theory. This
includes the formalization of mathematical structures for measure theory
and of measures, as well as standard theorems such as the Boole
inequality, Caratheodory's theorem, the Hahn extension, etc.
Main references:
g_measurableType G == the measurableType corresponding to s
measurable_fun D f == the function f with domain D is measurable
preimage_class D f G == class generated by the preimages of G by f
image_class D f G == class generated by the images of G by f
{outer_measure set T -> \bar R} == type of an outer measure over sets
of elements of type T where R is expected to be a
numFieldType
mu.-measurable A == A is Caratheodory measurable for the outer measure
mu, i.e.,
forall B, mu A = mu (A `&` B) + mu (A `&` ~` B)
measure_is_complete mu == the measure mu is complete
- Daniel Li, Intégration et applications, 2016
- Achim Klenke, Probability Theory 2nd edition, 2014
setI_closed G == the set of sets G is closed under finite intersection setU_closed G == the set of sets G is closed under finite union setC_closed G == the set of sets G is closed under complement setD_closed G == the set of sets G is closed under difference ndseq_closed G == the set of sets G is closed under non-decreasing countable union trivIset_closed G == the set of sets G is closed under pairwise-disjoint countable unionsigma_algebra D G == the set of sets G forms a sigma algebra on D
s D, G== sigma-algebra generated by G on D := smallest (sigma_algebra D) Gs G:=s setT, Gmonotone_class D G == G is a monotone class of subsets of Dm D, G== monotone class generated by G on Dm G:=m setT, Gdynkin G == G is a set of sets that form a Dynkin (or a lambda) systemd G== Dynkin system generated by G, i.e., smallest dynkin G
Mathematical structures for 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-algebrasG
Measures:
{additive_measure set T -> \bar 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 -> \bar 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 pushforward f m == pushforward/image measure of m by f \d_a == Dirac measure msum mu n == the measure corresponding to the sum of the measures mu_0, ..., mu{n-1} @mzero T R == the zero measure measure_add m1 m2 == the measure corresponding to the sum of the measures m1 and m2 mseries mu n == the measure corresponding to the sum of the measures mu_n, mu{n+1}, ... sigma_finite A f == the measure f is sigma-finite on A : set T with T : ringOfSetsType. mu.-negligible A == A is mu negligible {ae mu, forall x, P x} == P holds almost everywhere for the measure muCaratheodory theorem (from an outer measure to a measure):
caratheodory_type mu := T, where mu : {outer_measure set T -> \bar 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 measurableCaratheodory theorem (from a premeasure to an outer measure):
measurable_cover X == the set of sequences F such that- forall k, F k is measurable
- X `<=` \bigcup_k (F k)
Hahn Extension:
Hahn_ext_measure mu == extension of the additive measure mu over a semiring of sets to a measure over the generated sigma algebra (requires a proof of sigma-sub-additivity)Product of measurable spaces:
preimage_classes f1 f2 :=s preimage_class setT f1 measurable `|`
preimage_class setT f2 measurable >>.
prod_measurableType == product of measurableType
Set Implicit Arguments.
Import Order.TTheory GRing.Theory Num.Def Num.Theory.
Reserved Notation "'s<|' D , G '|>'" (at level 40, G, D at next level).
Reserved Notation "'s<<' A '>>'".
Reserved Notation "'d<<' D '>>'".
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.
Section classes.
Context {T} (C : set (set T) → Prop) (D : set T) (G : set (set T)).
Definition setC_closed := ∀ A, G A → G (~` A).
Definition setI_closed := ∀ A B, G A → G B → G (A `&` B).
Definition setU_closed := ∀ A B, G A → G B → G (A `|` B).
Definition setD_closed := ∀ A B, B `<=` A → G A → G B → G (A `\` B).
Definition setDI_closed := ∀ A B, G A → G B → G (A `\` B).
Definition fin_bigcap_closed :=
∀ I (D : set I) A_, finite_set D → (∀ i, D i → G (A_ i)) →
G (\bigcap_(i in D) (A_ i)).
Definition finN0_bigcap_closed :=
∀ I (D : set I) A_, finite_set D → D !=set0 →
(∀ i, D i → G (A_ i)) →
G (\bigcap_(i in D) (A_ i)).
Definition fin_bigcup_closed :=
∀ I (D : set I) A_, finite_set D → (∀ i, D i → G (A_ i)) →
G (\bigcup_(i in D) (A_ i)).
Definition semi_setD_closed := ∀ A B, G A → G B → ∃ D,
[/\ finite_set D, D `<=` G, A `\` B = \bigcup_(X in D) X & trivIset D id].
Definition ndseq_closed :=
∀ F, nondecreasing_seq F → (∀ i, G (F i)) → G (\bigcup_i (F i)).
Definition trivIset_closed :=
∀ F : (set T)^nat, trivIset setT F → (∀ n, G (F n)) →
G (\bigcup_k F k).
Definition fin_trivIset_closed :=
∀ I (D : set I) (F : I → set T), finite_set D → trivIset D F →
(∀ i, D i → G (F i)) → G (\bigcup_(k in D) F k).
Definition setring := [/\ G set0, setU_closed & setDI_closed].
Definition sigma_algebra :=
[/\ G set0, (∀ A, G A → G (D `\` A)) &
(∀ A : (set T)^nat, (∀ n, G (A n)) → G (\bigcup_k A k))].
Definition dynkin := [/\ G setT, setC_closed & trivIset_closed].
Definition monotone_class :=
[/\ ∀ A, G A → A `<=` D, G D, setD_closed & ndseq_closed].
End classes.
Notation "'<<m' D , G '>>'" := (smallest (monotone_class D) G)
(at level 2, format "'<<m' D , G '>>'") : classical_set_scope.
Notation "'<<m' G '>>'" := (<<m setT, G>>)
(at level 2, format "'<<m' G '>>'") : classical_set_scope.
Notation "'<<s' D , G '>>'" := (smallest (sigma_algebra D) G)
(at level 2, format "'<<s' D , G '>>'") : classical_set_scope.
Notation "'<<s' G '>>'" := (<<s setT, G>>)
(at level 2, format "'<<s' G '>>'") : classical_set_scope.
Notation "'<<d' G '>>'" := (smallest dynkin G)
(at level 2, format "'<<d' G '>>'") : classical_set_scope.
Notation "'<<r' G '>>'" := (smallest setring G)
(at level 2, format "'<<r' G '>>'") : classical_set_scope.
Notation "'<<fu' G '>>'" := (smallest fin_trivIset_closed G)
(at level 2, format "'<<fu' G '>>'") : classical_set_scope.
Lemma fin_bigcup_closedP T (G : set (set T)) :
(G set0 ∧ setU_closed G) ↔ fin_bigcup_closed G.
Lemma finN0_bigcap_closedP T (G : set (set T)) :
setI_closed G ↔ finN0_bigcap_closed G.
Lemma sedDI_closedP T (G : set (set T)) :
setDI_closed G ↔ (setI_closed G ∧ setD_closed G).
Lemma sigma_algebra_bigcap T (I : choiceType) (D : set T)
(F : I → set (set T)) (J : set I) :
(∀ n, J n → sigma_algebra D (F n)) →
sigma_algebra D (\bigcap_(i in J) F i).
Lemma sigma_algebraP T U (C : set (set T)) :
(∀ X, C X → X `<=` U) →
sigma_algebra U C ↔
[/\ C U, setD_closed C, ndseq_closed C & setI_closed C].
Section generated_sigma_algebra.
Context {T : Type} (D : set T) (G : set (set T)).
Implicit Types (M : set (set T)).
Lemma smallest_sigma_algebra : sigma_algebra D <<s D, G >>.
Hint Resolve smallest_sigma_algebra : core.
Lemma sub_sigma_algebra2 M : M `<=` G → <<s D, M >> `<=` <<s D, G >>.
Lemma sigma_algebra_id : sigma_algebra D G → <<s D, G >> = G.
Lemma sub_sigma_algebra : G `<=` <<s D, G >>.
Lemma sigma_algebra0 : <<s D, G >> set0.
Lemma sigma_algebraD : ∀ A, <<s D, G >> A → <<s D, G >> (D `\` A).
Lemma sigma_algebra_bigcup (A : (set T)^nat) :
(∀ i, <<s D, G >> (A i)) → <<s D, G >> (\bigcup_i (A i)).
End generated_sigma_algebra.
#[global] Hint Resolve smallest_sigma_algebra : core.
Section generated_setring.
Context {T : Type} (G : set (set T)).
Implicit Types (M : set (set T)).
Lemma smallest_setring : setring <<r G >>.
Hint Resolve smallest_setring : core.
Lemma sub_setring2 M : M `<=` G → <<r M >> `<=` <<r G >>.
Lemma setring_id : setring G → <<r G >> = G.
Lemma sub_setring : G `<=` <<r G >>.
Lemma setring0 : <<r G >> set0.
Lemma setringDI : setDI_closed <<r G>>.
Lemma setringU : setU_closed <<r G>>.
Lemma setring_fin_bigcup : fin_bigcup_closed <<r G>>.
End generated_setring.
#[global] Hint Resolve smallest_setring setring0 : core.
Lemma monotone_class_g_salgebra T (G : set (set T)) (D : set T) :
(∀ X, <<s D, G >> X → X `<=` D) → G D →
monotone_class D (<<s D, G >>).
Section smallest_monotone_classE.
Variables (T : Type) (G : set (set T)) (setIG : setI_closed G).
Variables (D : set T) (GD : G D).
Variables (H : set (set T)) (monoH : monotone_class D H) (GH : G `<=` H).
Lemma smallest_monotone_classE : (∀ X, <<s D, G >> X → X `<=` D) →
(∀ E, monotone_class D E → G `<=` E → H `<=` E) →
H = <<s D, G >>.
End smallest_monotone_classE.
Section monotone_class_subset.
Variables (T : Type) (G : set (set T)) (setIG : setI_closed G).
Variables (D : set T) (GD : G D).
Variables (H : set (set T)) (monoH : monotone_class D H) (GH : G `<=` H).
Lemma monotone_class_subset : (∀ X, (<<s D, G >>) X → X `<=` D) →
<<s D, G >> `<=` H.
End monotone_class_subset.
Section dynkin.
Variable T : Type.
Implicit Types G D : set (set T).
Lemma dynkinT G : dynkin G → G setT.
Lemma dynkinC G : dynkin G → setC_closed G.
Lemma dynkinU G : dynkin G → (∀ F : (set T)^nat, trivIset setT F →
(∀ n, G (F n)) → G (\bigcup_k F k)).
End dynkin.
Section dynkin_lemmas.
Variable T : Type.
Implicit Types D G : set (set T).
Lemma dynkin_monotone G : dynkin G ↔ monotone_class setT G.
Lemma dynkin_g_dynkin G : dynkin (<<d G >>).
Lemma sigma_algebra_dynkin G : sigma_algebra setT G → dynkin G.
Lemma dynkin_setI_bigsetI G (F : (set T)^nat) : dynkin G → setI_closed G →
(∀ n, G (F n)) → ∀ n, G (\big[setI/setT]_(i < n) F i).
Lemma dynkin_setI_sigma_algebra G : dynkin G → setI_closed G →
sigma_algebra setT G.
Lemma setI_closed_gdynkin_salgebra G : setI_closed G → <<d G >> = <<s G >>.
End dynkin_lemmas.
Notation semiRingOfSetsType := SemiRingOfSets.type.
Canonical semiRingOfSets_eqType (T : semiRingOfSetsType) := EqType T ptclass.
Canonical semiRingOfSets_choiceType (T : semiRingOfSetsType) :=
ChoiceType T ptclass.
Canonical semiRingOfSets_ptType (T : semiRingOfSetsType) :=
PointedType T ptclass.
Notation ringOfSetsType := RingOfSets.type.
Canonical ringOfSets_eqType (T : ringOfSetsType) := EqType T ptclass.
Canonical ringOfSets_choiceType (T : ringOfSetsType) := ChoiceType T ptclass.
Canonical ringOfSets_ptType (T : ringOfSetsType) := PointedType T ptclass.
Notation algebraOfSetsType := AlgebraOfSets.type.
Canonical algebraOfSets_eqType (T : algebraOfSetsType) := EqType T ptclass.
Canonical algebraOfSets_choiceType (T : algebraOfSetsType) :=
ChoiceType T ptclass.
Canonical algebraOfSets_ptType (T : algebraOfSetsType) :=
PointedType T ptclass.
Notation measurableType := Measurable.type.
Canonical measurable_eqType (T : measurableType) := EqType T ptclass.
Canonical measurable_choiceType (T : measurableType) := ChoiceType T ptclass.
Canonical measurable_ptType (T : measurableType) := PointedType T ptclass.
Implicit Types (A B C D : set T).
Lemma mI : setI_closed measurable.
Lemma mD : semi_setD_closed measurable.
Lemma mD : setDI_closed measurable.
Lemma measurableT : measurable (@setT T).
Obligation Tactic := idtac.
Lemma mU : setU_closed measurable.
Lemma mC : setC_closed measurable.
#[global] Hint Extern 0 (measurable set0) ⇒ solve [apply: measurable0] : core.
#[global] 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 fin_bigcup_measurable I (D : set I) (F : I → set T) :
finite_set D →
(∀ i, D i → measurable (F i)) →
measurable (\bigcup_(i in D) F i).
Lemma measurableD : setDI_closed (@measurable T).
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).
Lemma fin_bigcap_measurable I (D : set I) (F : I → set T) :
finite_set D →
(∀ i, D i → measurable (F i)) →
measurable (\bigcap_(i in D) F i).
End algebraofsets_lemmas.
Section measurable_lemmas.
Variables T : measurableType.
Implicit Types (A B : set T) (F : (set T)^nat) (P : set nat).
Lemma sigma_algebra_measurable : sigma_algebra setT (@measurable T).
Lemma bigcup_measurable F P :
(∀ k, P k → measurable (F k)) → measurable (\bigcup_(i in P) F i).
Lemma bigcap_measurable F P :
(∀ k, P k → measurable (F k)) → measurable (\bigcap_(i in P) F i).
Lemma bigcapT_measurable F : (∀ i, measurable (F i)) →
measurable (\bigcap_i (F i)).
End measurable_lemmas.
Lemma bigcupT_measurable_rat (T : measurableType) (F : rat → set T) :
(∀ i, measurable (F i)) → measurable (\bigcup_i F i).
Definition g_measurable {T} (G : set (set T)) := T.
Section g_salgebra_instance.
Variables (T : pointedType) (G : set (set T)).
Lemma sigma_algebraC (A : set T) : <<s G >> A → <<s G >> (~` A).
Canonical g_measurable_eqType := EqType (g_measurable G) (Equality.class T).
Canonical g_measurable_choiceType :=
ChoiceType (g_measurable G) (Choice.class T).
Canonical g_measurable_ptType := PointedType (g_measurable G) (Pointed.class T).
Definition g_measurableType := [the measurableType of g_measurable G].
End g_salgebra_instance.
Lemma measurable_g_measurableTypeE (T : pointedType) (G : set (set T)) :
sigma_algebra setT G → @measurable (g_measurableType G) = G.
Definition measurable_fun (T U : measurableType) (D : set T) (f : T → U) :=
measurable D → ∀ Y, measurable Y → measurable (D `&` f @^-1` Y).
Section measurable_fun.
Implicit Types T : measurableType.
Lemma measurable_fun_id T (D : set T) : measurable_fun D id.
Lemma measurable_fun_comp T1 T2 T3 (f : T2 → T3) E (g : T1 → T2) :
measurable_fun setT f → measurable_fun E g → measurable_fun E (f \o g).
Lemma eq_measurable_fun T1 T2 (D : set T1) (f g : T1 → T2) :
{in D, f =1 g} → measurable_fun D f → measurable_fun D g.
Lemma measurable_fun_cst T1 T2 (D : set T1) (r : T2) :
measurable_fun D (cst r : T1 → _).
Lemma measurable_funU T1 T2 (D E : set T1) (f : T1 → T2) :
measurable D → measurable E →
measurable_fun (D `|` E) f ↔ measurable_fun D f ∧ measurable_fun E f.
Lemma measurable_funS T1 T2 (E D : set T1) (f : T1 → T2) :
measurable E → D `<=` E → measurable_fun E f →
measurable_fun D f.
Lemma measurable_fun_ext T1 T2 D (f g : T1 → T2) :
{in D, f =1 g} → measurable_fun D f → measurable_fun D g.
Lemma measurable_restrict {aT rT : measurableType} D E (f : aT → rT) :
measurable D → measurable E → D `<=` E →
measurable_fun D f ↔ measurable_fun E (f \_ D).
End measurable_fun.
Arguments measurable_fun_ext {T1 T2 D} f {g}.
Section measurability.
Definition preimage_class (aT rT : Type) (D : set aT) (f : aT → rT)
(G : set (set rT)) : set (set aT) :=
[set D `&` f @^-1` B | B in G].
f1 is measurable on the sigma-algebra generated by itself
Lemma preimage_class_measurable_fun (aT : pointedType) (rT : measurableType)
(D : set aT) (f : aT → rT) :
@measurable_fun (g_measurableType (preimage_class D f measurable))
rT D f.
Lemma sigma_algebra_preimage_class (aT rT : Type) (G : set (set rT))
(D : set aT) (f : aT → rT) :
sigma_algebra setT G → sigma_algebra D (preimage_class D f G).
Definition image_class (aT rT : Type) (D : set aT) (f : aT → rT)
(G : set (set aT)) : set (set rT) :=
[set B : set rT | G (D `&` f @^-1` B)].
Lemma sigma_algebra_image_class (aT rT : Type) (D : set aT) (f : aT → rT)
(G : set (set aT)) :
sigma_algebra D G → sigma_algebra setT (image_class D f G).
Lemma sigma_algebra_preimage_classE aT (rT : pointedType) (D : set aT)
(f : aT → rT) (G' : set (set rT)) :
<<s D, preimage_class D f G' >> =
preimage_class D f (@measurable (g_measurableType G')).
Lemma measurability (aT rT : measurableType) (D : set aT) (f : aT → rT)
(G' : set (set rT)) :
@measurable rT = <<s G' >> → preimage_class D f G' `<=` @measurable aT →
measurable_fun D f.
End measurability.
Local Open Scope ereal_scope.
Section 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 := ∀ F n,
(∀ k : nat, measurable (F k)) → trivIset setT F →
measurable (\big[setU/set0]_(k < n) F k) →
mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).
Definition semi_sigma_additive :=
∀ F, (∀ i : nat, measurable (F i)) → trivIset setT F →
measurable (\bigcup_n F n) →
(fun n ⇒ \sum_(0 ≤ i < n) mu (F i)) --> mu (\bigcup_n F n).
Definition additive2 := ∀ A B, measurable A → measurable B →
A `&` B = set0 → mu (A `|` B) = mu A + mu B.
Definition additive :=
∀ F, (∀ i : nat, measurable (F i)) → trivIset setT F →
∀ n, mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).
Definition sigma_additive :=
∀ F, (∀ i : nat, measurable (F i)) → trivIset setT F →
(fun n ⇒ \sum_(0 ≤ i < n) mu (F i)) --> mu (\bigcup_n F n).
Definition sub_additive := ∀ (A : set T) (F : nat → set T) n,
(∀ k, `I_n k → measurable (F k)) → measurable A →
A `<=` \big[setU/set0]_(k < n) F k →
mu A ≤ \sum_(k < n) mu (F k).
Definition sigma_sub_additive := ∀ (A : set T) (F : nat → set T),
(∀ n, measurable (F n)) → measurable A →
A `<=` \bigcup_n F n →
mu A ≤ \sum_(n <oo) mu (F n).
Definition sigma_finite (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.
Lemma semi_additiveW : mu set0 = 0 → semi_additive → semi_additive2.
End additivity.
Section ring_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 → semi_additive mu ↔ additive2 mu.
End ring_additivity.
(D : set aT) (f : aT → rT) :
@measurable_fun (g_measurableType (preimage_class D f measurable))
rT D f.
Lemma sigma_algebra_preimage_class (aT rT : Type) (G : set (set rT))
(D : set aT) (f : aT → rT) :
sigma_algebra setT G → sigma_algebra D (preimage_class D f G).
Definition image_class (aT rT : Type) (D : set aT) (f : aT → rT)
(G : set (set aT)) : set (set rT) :=
[set B : set rT | G (D `&` f @^-1` B)].
Lemma sigma_algebra_image_class (aT rT : Type) (D : set aT) (f : aT → rT)
(G : set (set aT)) :
sigma_algebra D G → sigma_algebra setT (image_class D f G).
Lemma sigma_algebra_preimage_classE aT (rT : pointedType) (D : set aT)
(f : aT → rT) (G' : set (set rT)) :
<<s D, preimage_class D f G' >> =
preimage_class D f (@measurable (g_measurableType G')).
Lemma measurability (aT rT : measurableType) (D : set aT) (f : aT → rT)
(G' : set (set rT)) :
@measurable rT = <<s G' >> → preimage_class D f G' `<=` @measurable aT →
measurable_fun D f.
End measurability.
Local Open Scope ereal_scope.
Section 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 := ∀ F n,
(∀ k : nat, measurable (F k)) → trivIset setT F →
measurable (\big[setU/set0]_(k < n) F k) →
mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).
Definition semi_sigma_additive :=
∀ F, (∀ i : nat, measurable (F i)) → trivIset setT F →
measurable (\bigcup_n F n) →
(fun n ⇒ \sum_(0 ≤ i < n) mu (F i)) --> mu (\bigcup_n F n).
Definition additive2 := ∀ A B, measurable A → measurable B →
A `&` B = set0 → mu (A `|` B) = mu A + mu B.
Definition additive :=
∀ F, (∀ i : nat, measurable (F i)) → trivIset setT F →
∀ n, mu (\big[setU/set0]_(i < n) F i) = \sum_(i < n) mu (F i).
Definition sigma_additive :=
∀ F, (∀ i : nat, measurable (F i)) → trivIset setT F →
(fun n ⇒ \sum_(0 ≤ i < n) mu (F i)) --> mu (\bigcup_n F n).
Definition sub_additive := ∀ (A : set T) (F : nat → set T) n,
(∀ k, `I_n k → measurable (F k)) → measurable A →
A `<=` \big[setU/set0]_(k < n) F k →
mu A ≤ \sum_(k < n) mu (F k).
Definition sigma_sub_additive := ∀ (A : set T) (F : nat → set T),
(∀ n, measurable (F n)) → measurable A →
A `<=` \bigcup_n F n →
mu A ≤ \sum_(n <oo) mu (F n).
Definition sigma_finite (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.
Lemma semi_additiveW : mu set0 = 0 → semi_additive → semi_additive2.
End additivity.
Section ring_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 → semi_additive mu ↔ additive2 mu.
End ring_additivity.
NB: generalize to numFieldType when Rhausdorff is generalized
Lemma semi_sigma_additive_is_additive (R : realFieldType)
(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.
Lemma fset_set_image (T1 T2 : choiceType) (D : set T1) (f : T1 → T2) :
finite_set D → fset_set (f @` D) = (f @` (fset_set D))%fset.
Module AdditiveMeasure.
Section ClassDef.
Variables (R : numFieldType) (T : semiRingOfSetsType).
Record axioms (mu : set T → \bar R) := Axioms {
_ : mu set0 = 0 ;
_ : ∀ x, 0 ≤ mu x ;
_ : semi_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 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, 0 ≤ mu x.
Hint Resolve measure_ge0 : core.
Lemma measure_semi_additive : semi_additive mu.
Hint Resolve measure_semi_additive : core.
Lemma content_fin_bigcup (I : choiceType) (D : set I) (F : I → set T) :
finite_set D →
trivIset D F →
(∀ i, D i → measurable (F i)) →
measurable (\bigcup_(i in D) F i) →
mu (\bigcup_(i in D) F i) = \sum_(i <- fset_set D) mu (F i).
Lemma measure_semi_additive2 : semi_additive2 mu.
Hint Resolve measure_semi_additive2 : core.
End additive_measure_on_semiring_of_sets.
#[global] Hint Extern 0
(is_true (0 ≤ (_ : {additive_measure set _ → \bar _}) _)%E) ⇒
solve [apply: measure_ge0] : core.
#[global]
Hint Resolve measure0 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.
Lemma measure_fin_bigcup (I : choiceType) (D : set I) (F : I → set T) :
finite_set D →
trivIset D F →
(∀ i, D i → measurable (F i)) →
mu (\bigcup_(i in D) F i) = \sum_(i <- fset_set D) mu (F i).
Lemma measure_bigsetU_ord_cond n (P : {pred 'I_n}) (F : 'I_n → set T) :
(∀ i : 'I_n, P i → measurable (F i)) → trivIset P F →
mu (\big[setU/set0]_(i < n | P i) F i) = (\sum_(i < n | P i) mu (F i))%E.
Lemma measure_bigsetU_ord n (P : {pred 'I_n}) (F : 'I_n → set T) :
(∀ i : 'I_n, measurable (F i)) → trivIset setT F →
mu (\big[setU/set0]_(i < n | P i) F i) = (\sum_(i < n | P i) mu (F i))%E.
Lemma measure_fbigsetU (I : choiceType) (A : {fset I}) (F : I → set T) :
(∀ i, i \in A → measurable (F i)) → trivIset [set` A] F →
mu (\big[setU/set0]_(i <- A) F i) = (\sum_(i <- A) mu (F i))%E.
End additive_measure_on_ring_of_sets.
#[global]
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, 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.
Lemma eq_measure (T : measurableType) (R : realType)
(m1 m2 : {measure set T → \bar R}) :
(m1 = m2 :> (set T → \bar R)) → m1 = m2.
Section measure_lemmas.
Variables (R : realFieldType) (T : semiRingOfSetsType).
Coercion measure_to_nadditive_measure (mu : set T → \bar R) :
is_measure mu → additive_measure mu.
Variable mu : {measure set T → \bar R}.
Lemma measure_semi_sigma_additive : semi_sigma_additive mu.
Lemma measure_semi_bigcup A :
(∀ i : nat, measurable (A i)) →
trivIset setT A →
measurable (\bigcup_n A n) →
mu (\bigcup_n A n) = \sum_(i <oo) mu (A i).
End measure_lemmas.
Section measure_lemmas.
Variables (R : realFieldType) (T : measurableType).
Variable mu : {measure set T → \bar R}.
Lemma measure_sigma_additive : sigma_additive mu.
Lemma measure_bigcup A : (∀ i : nat, measurable (A i)) →
trivIset setT A →
mu (\bigcup_n A n) = \sum_(i <oo) mu (A i).
End measure_lemmas.
Arguments measure_bigcup {R T} mu A.
#[global] Hint Extern 0 (_ set0 = 0) ⇒ solve [apply: measure0] : core.
#[global] Hint Extern 0 (sigma_additive _) ⇒
solve [apply: measure_sigma_additive] : core.
#[global] Hint Extern 0 (is_true (0 ≤ _)) ⇒ solve [apply: measure_ge0] : 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.
Section pushforward_measure.
Local Open Scope ereal_scope.
Variables (T1 T2 : measurableType) (f : T1 → T2).
Hypothesis mf : measurable_fun setT f.
Variables (R : realFieldType) (m : {measure set T1 → \bar R}).
Definition pushforward A := m (f @^-1` A).
Let pushforward0 : pushforward set0 = 0.
Let pushforward_ge0 A : 0 ≤ pushforward A.
Let pushforward_sigma_additive : semi_sigma_additive pushforward.
Canonical pushforward_measure : {measure set T2 → \bar R} :=
Measure.Pack _ (Measure.Axioms pushforward0 pushforward_ge0
pushforward_sigma_additive).
End pushforward_measure.
Section dirac_measure.
Local Open Scope ereal_scope.
Variables (T : measurableType) (a : T) (R : realFieldType).
Definition dirac (A : set T) : \bar R := (\1_A a)%:E.
Let dirac0 : dirac set0 = 0.
Let dirac_ge0 B : 0 ≤ dirac B.
Let dirac_sigma_additive : semi_sigma_additive dirac.
Canonical dirac_measure : {measure set T → \bar R} :=
Measure.Pack _ (Measure.Axioms dirac0 dirac_ge0 dirac_sigma_additive).
End dirac_measure.
Arguments dirac {T} _ {R}.
Arguments dirac_measure {T} _ {R}.
Notation "\d_ a" := (dirac_measure a) : ring_scope.
Section dirac_lemmas.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType).
Lemma finite_card_dirac (A : set T) : finite_set A →
\esum_(i in A) \d_ i A = (#|` fset_set A|%:R)%:E :> \bar R.
Lemma infinite_card_dirac (A : set T) : infinite_set A →
\esum_(i in A) \d_ i A = +oo :> \bar R.
End dirac_lemmas.
Section measure_sum.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType).
Variables (m : {measure set T → \bar R}^nat) (n : nat).
Definition msum (A : set T) : \bar R := \sum_(k < n) m k A.
Let msum0 : msum set0 = 0.
Let msum_ge0 B : 0 ≤ msum B.
Let msum_sigma_additive : semi_sigma_additive msum.
Canonical measure_sum : {measure set T → \bar R} :=
Measure.Pack _ (Measure.Axioms msum0 msum_ge0 msum_sigma_additive).
End measure_sum.
Arguments msum {T R}.
Arguments measure_sum {T R}.
Section measure_zero.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType).
Definition mzero (A : set T) : \bar R := 0.
Let mzero0 : mzero set0 = 0.
Let mzero_ge0 B : 0 ≤ mzero B.
Let mzero_sigma_additive : semi_sigma_additive mzero.
Canonical measure_zero : {measure set T → \bar R} :=
Measure.Pack _ (Measure.Axioms mzero0 mzero_ge0 mzero_sigma_additive).
End measure_zero.
Arguments mzero {T R}.
Arguments measure_zero {T R}.
Section measure_add.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType).
Variables (m1 m2 : {measure set T → \bar R}).
Definition measure_add := measure_sum (fun n ⇒ if n is 0%N then m1 else m2) 2.
Lemma measure_addE A : measure_add A = m1 A + m2 A.
End measure_add.
Section measure_series.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType).
Variables (m : {measure set T → \bar R}^nat) (n : nat).
Definition mseries (A : set T) : \bar R := \sum_(n ≤ k <oo) m k A.
Let mseries0 : mseries set0 = 0.
Let mseries_ge0 B : 0 ≤ mseries B.
Let mseries_sigma_additive : semi_sigma_additive mseries.
Canonical measure_series : {measure set T → \bar R} :=
Measure.Pack _ (Measure.Axioms mseries0 mseries_ge0 mseries_sigma_additive).
End measure_series.
Arguments mseries {T R}.
Arguments measure_series {T R}.
Section measure_restr.
Variables (T : measurableType) (R : realType) (mu : {measure set T → \bar R}).
Variables (D : set T) (mD : measurable D).
Let measure_restr' (X : set _) : \bar R := mu (X `&` D).
Let measure_restr'0 : measure_restr' set0 = 0%E.
Let measure_restr'_ge0 (A : set _) : (0 ≤ measure_restr' A)%E.
Let measure_restr'_sigma_additive : semi_sigma_additive measure_restr'.
Definition measure_restr : {measure set _ → \bar R} :=
Measure.Pack _ (Measure.Axioms
measure_restr'0 measure_restr'_ge0 measure_restr'_sigma_additive).
Lemma measure_restrE A : measure_restr A = mu (A `&` D).
End measure_restr.
Lemma big_trivIset (I : choiceType) D T (R : Type) (idx : R)
(op : Monoid.com_law idx) (A : I → set T) (F : set T → R) :
finite_set D → trivIset D A → F set0 = idx →
\big[op/idx]_(i <- fset_set D) F (A i) =
\big[op/idx]_(X <- (A @` fset_set D)%fset) F X.
Section covering.
Context {T : Type}.
Implicit Type (C : ∀ I, set (set I)).
Implicit Type (P : ∀ I, set I → set (I → set T)).
Definition covered_by C P :=
[set X : set T | ∃ I D A, [/\ C I D, P I D A & X = \bigcup_(i in D) A i]].
Lemma covered_bySr C P P' : (∀ I D A, P I D A → P' I D A) →
covered_by C P `<=` covered_by C P'.
Lemma covered_byP C P I D A : C I D → P I D A →
covered_by C P (\bigcup_(i in D) A i).
Lemma covered_by_finite P :
(∀ I (D : set I) A, (∀ i, D i → A i = set0) → P I D A) →
(∀ (I : pointedType) D A, finite_set D → P I D A →
P nat `I_#|` fset_set D| (A \o nth point (fset_set D))) →
covered_by (@finite_set) P =
[set X : set T | ∃ n A, [/\ P nat `I_n A & X = \bigcup_(i in `I_n) A i]].
Lemma covered_by_countable P :
(∀ I (D : set I) A, (∀ i, D i → A i = set0) → P I D A) →
(∀ (I : pointedType) (D : set I) (A : I → set T) (f : nat → I),
set_surj [set: nat] D f →
P I D A → P nat [set: nat] (A \o f)) →
covered_by (@countable) P =
[set X : set T | ∃ A, [/\ P nat [set: nat] A & X = \bigcup_i A i]].
End covering.
Module SetRing.
Definition type (T : Type) := T.
Section SetRing.
Context {T : semiRingOfSetsType}.
Notation rT := (type T).
Canonical ring_eqType := EqType rT ptclass.
Canonical ring_choiceType := ChoiceType rT ptclass.
Canonical ring_ptType := PointedType rT ptclass.
#[export]
HB.instance Definition _ := isRingOfSets.Build rT ptclass
(@setring0 T measurable) (@setringU T measurable) (@setringDI T measurable).
Definition ring := [the ringOfSetsType of rT].
Lemma ring_measurableE : @measurable ring = measurable_fin_trivIset.
Lemma ring_fsets (A : set rT) : measurable A → ∃ B : {fset set T},
[/\ all [pred X | X != set0] B,
trivIset [set` B] id,
(∀ X : set T, X \in B → measurable X) &
A = \bigcup_(X in [set` B]) X].
Definition decomp (A : set rT) : {fset set T} :=
if A == set0 then [fset set0]%fset else
if pselect (measurable A) is left mA then projT1 (cid (ring_fsets mA)) else [fset A]%fset.
Lemma decomp_triv (A : set rT) : trivIset [set` decomp A] id.
Hint Resolve decomp_triv : core.
Lemma all_decomp_neq0 (A : set rT) : A !=set0 → all [pred X | X != set0] (decomp A).
Lemma decomp_neq0 (A : set rT) X : A !=set0 → X \in decomp A → X !=set0.
Lemma decomp_measurable (A : set rT) (X : set T) :
measurable A → X \in decomp A → measurable X.
Lemma cover_decomp (A : set rT) : \bigcup_(X in [set` decomp A]) X = A.
Lemma decomp_sub (A : set rT) (X : set T) : X \in decomp A → X `<=` A.
Lemma decomp_set0 : decomp set0 = [fset set0]%fset.
Lemma decompN0 (A : set rT) : decomp A != fset0.
Definition measure (R : numDomainType) (mu : set T → \bar R)
(A : set rT) : \bar R := \sum_(X <- decomp A) mu X.
Section additive_measure.
Context {R : realFieldType} (mu : {additive_measure set T → \bar R}).
Arguments big_trivIset {I D T R idx op} A F.
Lemma Rmu_fin_bigcup (I : choiceType) (D : set I) (F : I → set T) :
finite_set D → trivIset D F → (∀ i, D i → measurable (F i)) →
Rmu (\bigcup_(i in D) F i) = \sum_(i <- fset_set D) mu (F i).
Lemma RmuE (A : set T) : measurable A → Rmu A = mu A.
Lemma Rmu0 : Rmu set0 = 0.
Lemma Rmu_ge0 A : Rmu A ≥ 0.
Lemma Rmu_additive : semi_additive Rmu.
Lemma Rmu_additive_measure : additive_measure Rmu.
Canonical measure_additive_measure :=
AdditiveMeasure Rmu_additive_measure.
End additive_measure.
End SetRing.
Module Exports.
Canonical ring_eqType.
Canonical ring_choiceType.
Canonical ring_ptType.
Canonical measure_additive_measure.
End Exports.
End SetRing.
Export SetRing.Exports.
Lemma le_measure (R : realFieldType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}) :
{in measurable &, {homo mu : A B / A `<=` B >-> (A ≤ B)%E}}.
Lemma measure_le0 (T : semiRingOfSetsType) (R : realFieldType)
(mu : {additive_measure set T → \bar R}) (A : set T) :
(mu A ≤ 0)%E = (mu A == 0)%E.
Section more_content_semiring_lemmas.
Variables (R : realFieldType) (T : semiRingOfSetsType).
Variable mu : {additive_measure set T → \bar R}.
Lemma content_sub_additive : sub_additive mu.
Lemma content_sub_fsum (I : choiceType) D (A : set T) (A_ : I → set T) :
finite_set D →
(∀ i, D i → measurable (A_ i)) →
measurable A →
A `<=` \bigcup_(i in D) A_ i → mu A ≤ \sum_(i \in D) mu (A_ i).
(* (* alternative proof *)
Theorem semi_Boole_inequality : sub_additive mu.
Proof.
move=> X A n Am Xm Xsub; rewrite -SetRing.RmuE//.
under eq_bigr => i do rewrite -SetRing.RmuE; do ?by apply: Am⇒ /=.
pose rT := SetRing.type T.
have {}Am i : `I_n i -> measurable (A i : set rT).
by move=> *; apply/SetRing.measurableW/Am => /=.
have {}Xm : measurable (X : set rT) by exact: SetRing.measurableW.
pose ammu := additive_measure of SetRing.measure mu.
rewrite (le_trans (le_measure ammu _ _ Xsub)) ?inE// {Xsub}.
by rewrite -bigcup_mkord; apply: fin_bigcup_measurable.
elim: n Am Xm => |n IHn Am Xm; first by rewrite !big_ord0 measure0.
have Anm : measurable (A n : set rT) by apply: Am => /=.
set B := \bigsetU/set0_(i < n) A i.
set C := \bigsetU/set0_(i < n.+1) A i.
have -> : C = B `|` (A n `\` B).
suff -> : A n `\` B = C `\` B by rewrite setDUK// /C big_ord_recr/=; left.
by rewrite /C big_ord_recr/= !setDE setIUl -!setDE setDv set0U.
have Bm : measurable (B : set rT).
by rewrite -Bbigcup_mkord; apply: fin_bigcup_measurable => //= i /ltnW/Am.
rewrite measureU // ?setDIK//; last exact: measurableD.
rewrite (@le_trans _ _ (ammu B + ammu (A n))) // ?lee_add2l //; last first.
by rewrite big_ord_recr /= lee_add2r// IHn// => i /ltnW/Am.
by rewrite le_measure // ?inE// ?setDE//; exact: measurableD.
Qed. *)
End more_content_semiring_lemmas.
Section content_ring_lemmas.
Variables (R : realType) (T : ringOfSetsType).
Variable mu : {additive_measure set T → \bar R}.
Lemma content_ring_sup_sigma_additive (A : nat → set T) :
(∀ i, measurable (A i)) → measurable (\bigcup_i A i) →
trivIset [set: nat] A → \sum_(i <oo) mu (A i) ≤ mu (\bigcup_i A i).
Lemma content_ring_sigma_additive : sigma_sub_additive mu → semi_sigma_additive mu.
End content_ring_lemmas.
Section ring_sigma_sub_additive_content.
Context (R : realType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}).
Import SetRing.
Lemma ring_sigma_sub_additive : sigma_sub_additive mu → sigma_sub_additive Rmu.
Lemma ring_sigma_additive : sigma_sub_additive mu → semi_sigma_additive Rmu.
End ring_sigma_sub_additive_content.
Section more_premeasure_ring_lemmas.
Variables (R : realType) (T : semiRingOfSetsType).
Variable mu : {measure set T → \bar R}.
Import SetRing.
Lemma measure_sigma_sub_additive : sigma_sub_additive mu.
End more_premeasure_ring_lemmas.
Section ring_sigma_additive_measure.
Context (R : realType) (T : semiRingOfSetsType)
(mu : {measure set T → \bar R}).
Import SetRing.
Canonical set_ring_measure : {measure set (SetRing.type T) → \bar R} :=
@Measure.Pack _ _ (Phant _) Rmu
(Measure.Axioms (measure0 _) (measure_ge0 _) ring_sigma_additive_measure).
End ring_sigma_additive_measure.
Lemma measureIl (R : realFieldType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}) (A B : set T) :
measurable A → measurable B → (mu (A `&` B) ≤ mu A)%E.
Lemma measureIr (R : realFieldType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}) (A B : set T) :
measurable A → measurable B → (mu (A `&` B) ≤ mu B)%E.
Lemma subset_measure0 (T : semiRingOfSetsType) (R : realType)
(mu : {additive_measure set T → \bar R}) (A B : set T) :
measurable A → measurable B → A `<=` B →
mu B = 0%E → mu A = 0%E.
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.
Lemma measureUfinr (T : ringOfSetsType) (R : realFieldType) (A B : set T)
(mu : {measure set T → \bar R}):
measurable A → measurable B → (mu B < +oo)%E →
mu (A `|` B) = (mu A + mu B - mu (A `&` B))%E.
Lemma measureUfinl (T : ringOfSetsType) (R : realFieldType) (A B : set T)
(mu : {measure set T → \bar R}):
measurable A → measurable B → (mu A < +oo)%E →
mu (A `|` B) = (mu A + mu B - mu (A `&` B))%E.
Lemma eq_measureU (T : ringOfSetsType) (R : realFieldType) (A B : set T)
(mu mu' : {measure set T → \bar R}):
measurable A → measurable B →
mu A = mu' A → mu B = mu' B → mu (A `&` B) = mu' (A `&` B) →
mu (A `|` B) = mu' (A `|` B).
Lemma null_set_setU (R : realFieldType) (T : ringOfSetsType)
(mu : {measure set T → \bar R}) (A B : set T) :
measurable A → measurable B → mu A = 0%E → mu B = 0%E → mu (A `|` B) = 0%E.
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) n :
(∀ i, `I_n i → measurable (A i)) →
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}).
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 : {additive_measure _ → _}) A :
measurable A → mu.-negligible A ↔ mu A = 0.
Lemma negligible_set0 (mu : {additive_measure _ → _}) : mu.-negligible set0.
Lemma measure_negligible (mu : {additive_measure set T → \bar R}) (A : set T) :
measurable A → mu.-negligible A → mu A = 0%E.
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) := ∀ (F : (set T) ^nat),
mu (\bigcup_n (F n)) ≤ \sum_(i <oo) mu (F 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.
#[global] Hint Extern 0 (_ set0 = 0) ⇒ solve [apply: outer_measure0] : core.
#[global] 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 : 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 : set T → \bar R) := T.
Section caratheodory_sigma_algebra.
Variables (R : realType) (T : pointedType) (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.
Section caratheodory_measure.
Variables (R : realType) (T : pointedType) (mu : {outer_measure set T → \bar R}).
Lemma caratheodory_measure0 : mu (set0 : set U) = 0.
Lemma caratheodory_measure_ge0 (A : set U) : 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.
Lemma epsilon_trick (R : realType) (A : (\bar R)^nat) e
(P : pred nat) : (∀ n, 0 ≤ A n) → (0 ≤ e)%R →
\sum_(i <oo | P i) (A i + (e / (2 ^ i.+1)%:R)%:E) ≤
\sum_(i <oo | P i) A i + e%:E.
Section measurable_cover.
Variable T : semiRingOfSetsType.
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 : semiRingOfSetsType).
Variable mu : set T → \bar R.
Hypothesis measure0 : mu set0 = 0.
Hypothesis measure_ge0 : ∀ X, mu X ≥ 0.
Hint Resolve measure_ge0 measure0 : core.
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.
Section measure_extension.
Variables (R : realType) (T : semiRingOfSetsType).
Variable mu : {additive_measure set T → \bar R}.
Canonical outer_measure_of_measure (R : realType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}) : {outer_measure set T → \bar R} :=
OuterMeasure (OuterMeasure.Axioms
(mu_ext0 (measure0 mu) (measure_ge0 mu))
(mu_ext_ge0 (measure_ge0 mu))
(le_mu_ext mu)
(mu_ext_sigma_subadditive (measure_ge0 mu))).
End measure_extension.
Section g_salgebra_measure_unique_trace.
Variables (R : realType) (T : measurableType) (G : set (set T)).
Variables (D : set T) (mD : measurable D).
Let H := [set X | G X ∧ X `<=` D] .
Hypotheses (Hm : H `<=` measurable) (setIH : setI_closed H) (HD : H D).
Variables m1 m2 : {measure set T → \bar R}.
Hypotheses (m1m2 : ∀ A, H A → m1 A = m2 A) (m1oo : (m1 D < +oo)%E).
Lemma g_salgebra_measure_unique_trace :
(∀ X, (<<s D, H >>) X → X `<=` D) → ∀ X, <<s D, H >> X →
m1 X = m2 X.
End g_salgebra_measure_unique_trace.
Section g_salgebra_measure_unique.
Variables (R : realType) (T : measurableType) (G : set (set T)).
Hypothesis Gm : G `<=` measurable.
Variable g : (set T)^nat.
Hypotheses (Gg : ∀ i, G (g i)).
Hypothesis g_cover : \bigcup_k (g k) = setT.
Variables m1 m2 : {measure set T → \bar R}.
Lemma g_salgebra_measure_unique_cover :
(∀ n A, <<s G >> A → m1 (g n `&` A) = m2 (g n `&` A)) →
∀ A, <<s G >> A → m1 A = m2 A.
Hypothesis setIG : setI_closed G.
Hypothesis m1m2 : ∀ A, G A → m1 A = m2 A.
Hypothesis m1goo : ∀ k, (m1 (g k) < +oo)%E.
Lemma g_salgebra_measure_unique : ∀ E, <<s G >> E → m1 E = m2 E.
End g_salgebra_measure_unique.
Section measure_unique.
Variables (R : realType) (T : measurableType) (G : set (set T)).
Variable g : (set T)^nat.
Hypotheses (mG : measurable = <<s G >>) (setIG : setI_closed G).
Hypothesis Gg : ∀ i, G (g i).
Hypothesis g_cover : \bigcup_k (g k) = setT.
Variables m1 m2 : {measure set T → \bar R}.
Hypothesis m1m2 : ∀ A, G A → m1 A = m2 A.
Hypothesis m1goo : ∀ k, (m1 (g k) < +oo)%E.
Lemma measure_unique A : measurable A → m1 A = m2 A.
End measure_unique.
Arguments measure_unique {R T} G g.
Lemma measurable_mu_extE (R : realType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}) X :
sigma_sub_additive mu →
measurable X → mu_ext mu X = mu X.
Section Rmu_ext.
Import SetRing.
Lemma Rmu_ext (R : realType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}) :
mu_ext (measure mu) = mu_ext mu.
End Rmu_ext.
Lemma measurable_Rmu_extE (R : realType) (T : semiRingOfSetsType)
(rT := @SetRing.ring T) (mu : {additive_measure set T → \bar R}) X :
sigma_sub_additive mu →
measurable (X : set rT) → mu_ext mu X = SetRing.measure mu X.
Section Hahn_extension.
Variables (R : realType) (T : semiRingOfSetsType).
Variable mu : {additive_measure set T → \bar R}.
Let M : measurableType := [the measurableType of caratheodory_type (mu_ext mu)].
Hypothesis mu_sub : sigma_sub_additive mu.
Let Rmu := SetRing.measure mu.
Lemma sub_caratheodory : <<s @measurable T >> `<=` @measurable M.
Let I : measurableType := g_measurableType (@measurable T).
Definition Hahn_ext : set I → \bar R := mu_ext mu.
Canonical Hahn_ext_measure : {measure set I → \bar R} :=
@Measure.Pack _ _ _ Hahn_ext (Measure.Axioms
Hahn_ext0 Hahn_ext_ge0 Hahn_ext_sigma_additive).
Lemma Hahn_ext_sigma_finite : @sigma_finite _ T setT mu →
@sigma_finite _ I setT Hahn_ext.
Lemma Hahn_ext_unique : @sigma_finite _ T setT mu →
∀ mu' : {measure set I → \bar R},
(∀ X, @measurable T X → mu X = mu' X) →
∀ X, @measurable I X → Hahn_ext X = mu' X.
End Hahn_extension.
Lemma caratheodory_measurable_mu_ext (R : realType) (T : measurableType)
(mu : {measure set T → \bar R}) A :
measurable A → (mu_ext mu).-measurable A.
Definition preimage_classes (T1 T2 : measurableType) (T : Type)
(f1 : T → T1) (f2 : T → T2) :=
<<s preimage_class setT f1 measurable `|`
preimage_class setT f2 measurable >>.
Section product_lemma.
Variables (T1 T2 : measurableType) (T : pointedType).
Variables (f1 : T → T1) (f2 : T → T2) (T3 : Type) (g : T3 → T).
Lemma preimage_classes_comp : preimage_classes (f1 \o g) (f2 \o g) =
preimage_class setT g (preimage_classes f1 f2).
End product_lemma.
Definition prod_measurable (T1 T2 : measurableType) := (T1 × T2)%type.
Section product_salgebra_instance.
Variables (T1 T2 : measurableType).
Let f1 := @fst T1 T2.
Let f2 := @snd T1 T2.
Let prod_salgebra_set0 : preimage_classes f1 f2 (set0 : set (T1 × T2)).
Let prod_salgebra_setC A : preimage_classes f1 f2 A →
preimage_classes f1 f2 (~` A).
Let prod_salgebra_bigcup (F : _^nat) : (∀ i, preimage_classes f1 f2 (F i))
→ preimage_classes f1 f2 (\bigcup_i (F i)).
Definition prod_measurableType := [the measurableType of prod_measurable T1 T2].
End product_salgebra_instance.
Lemma measurableM (T1 T2 : measurableType) (A : set T1) (B : set T2) :
measurable A → measurable B → measurable (A `*` B).
Section product_salgebra_measurableType.
Variables (T1 T2 : measurableType).
Let M1 := @measurable T1.
Let M2 := @measurable T2.
Let M1xM2 := [set A `*` B | A in M1 & B in M2].
Lemma measurable_prod_measurableType :
@measurable (prod_measurableType T1 T2) = <<s M1xM2 >>.
End product_salgebra_measurableType.
Section product_salgebra_g_measurableTypeR.
Variables (T1 : measurableType) (T2 : pointedType) (C2 : set (set T2)).
Hypothesis (setTC2 : setT `<=` C2).
(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.
Lemma fset_set_image (T1 T2 : choiceType) (D : set T1) (f : T1 → T2) :
finite_set D → fset_set (f @` D) = (f @` (fset_set D))%fset.
Module AdditiveMeasure.
Section ClassDef.
Variables (R : numFieldType) (T : semiRingOfSetsType).
Record axioms (mu : set T → \bar R) := Axioms {
_ : mu set0 = 0 ;
_ : ∀ x, 0 ≤ mu x ;
_ : semi_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 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, 0 ≤ mu x.
Hint Resolve measure_ge0 : core.
Lemma measure_semi_additive : semi_additive mu.
Hint Resolve measure_semi_additive : core.
Lemma content_fin_bigcup (I : choiceType) (D : set I) (F : I → set T) :
finite_set D →
trivIset D F →
(∀ i, D i → measurable (F i)) →
measurable (\bigcup_(i in D) F i) →
mu (\bigcup_(i in D) F i) = \sum_(i <- fset_set D) mu (F i).
Lemma measure_semi_additive2 : semi_additive2 mu.
Hint Resolve measure_semi_additive2 : core.
End additive_measure_on_semiring_of_sets.
#[global] Hint Extern 0
(is_true (0 ≤ (_ : {additive_measure set _ → \bar _}) _)%E) ⇒
solve [apply: measure_ge0] : core.
#[global]
Hint Resolve measure0 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.
Lemma measure_fin_bigcup (I : choiceType) (D : set I) (F : I → set T) :
finite_set D →
trivIset D F →
(∀ i, D i → measurable (F i)) →
mu (\bigcup_(i in D) F i) = \sum_(i <- fset_set D) mu (F i).
Lemma measure_bigsetU_ord_cond n (P : {pred 'I_n}) (F : 'I_n → set T) :
(∀ i : 'I_n, P i → measurable (F i)) → trivIset P F →
mu (\big[setU/set0]_(i < n | P i) F i) = (\sum_(i < n | P i) mu (F i))%E.
Lemma measure_bigsetU_ord n (P : {pred 'I_n}) (F : 'I_n → set T) :
(∀ i : 'I_n, measurable (F i)) → trivIset setT F →
mu (\big[setU/set0]_(i < n | P i) F i) = (\sum_(i < n | P i) mu (F i))%E.
Lemma measure_fbigsetU (I : choiceType) (A : {fset I}) (F : I → set T) :
(∀ i, i \in A → measurable (F i)) → trivIset [set` A] F →
mu (\big[setU/set0]_(i <- A) F i) = (\sum_(i <- A) mu (F i))%E.
End additive_measure_on_ring_of_sets.
#[global]
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, 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.
Lemma eq_measure (T : measurableType) (R : realType)
(m1 m2 : {measure set T → \bar R}) :
(m1 = m2 :> (set T → \bar R)) → m1 = m2.
Section measure_lemmas.
Variables (R : realFieldType) (T : semiRingOfSetsType).
Coercion measure_to_nadditive_measure (mu : set T → \bar R) :
is_measure mu → additive_measure mu.
Variable mu : {measure set T → \bar R}.
Lemma measure_semi_sigma_additive : semi_sigma_additive mu.
Lemma measure_semi_bigcup A :
(∀ i : nat, measurable (A i)) →
trivIset setT A →
measurable (\bigcup_n A n) →
mu (\bigcup_n A n) = \sum_(i <oo) mu (A i).
End measure_lemmas.
Section measure_lemmas.
Variables (R : realFieldType) (T : measurableType).
Variable mu : {measure set T → \bar R}.
Lemma measure_sigma_additive : sigma_additive mu.
Lemma measure_bigcup A : (∀ i : nat, measurable (A i)) →
trivIset setT A →
mu (\bigcup_n A n) = \sum_(i <oo) mu (A i).
End measure_lemmas.
Arguments measure_bigcup {R T} mu A.
#[global] Hint Extern 0 (_ set0 = 0) ⇒ solve [apply: measure0] : core.
#[global] Hint Extern 0 (sigma_additive _) ⇒
solve [apply: measure_sigma_additive] : core.
#[global] Hint Extern 0 (is_true (0 ≤ _)) ⇒ solve [apply: measure_ge0] : 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.
Section pushforward_measure.
Local Open Scope ereal_scope.
Variables (T1 T2 : measurableType) (f : T1 → T2).
Hypothesis mf : measurable_fun setT f.
Variables (R : realFieldType) (m : {measure set T1 → \bar R}).
Definition pushforward A := m (f @^-1` A).
Let pushforward0 : pushforward set0 = 0.
Let pushforward_ge0 A : 0 ≤ pushforward A.
Let pushforward_sigma_additive : semi_sigma_additive pushforward.
Canonical pushforward_measure : {measure set T2 → \bar R} :=
Measure.Pack _ (Measure.Axioms pushforward0 pushforward_ge0
pushforward_sigma_additive).
End pushforward_measure.
Section dirac_measure.
Local Open Scope ereal_scope.
Variables (T : measurableType) (a : T) (R : realFieldType).
Definition dirac (A : set T) : \bar R := (\1_A a)%:E.
Let dirac0 : dirac set0 = 0.
Let dirac_ge0 B : 0 ≤ dirac B.
Let dirac_sigma_additive : semi_sigma_additive dirac.
Canonical dirac_measure : {measure set T → \bar R} :=
Measure.Pack _ (Measure.Axioms dirac0 dirac_ge0 dirac_sigma_additive).
End dirac_measure.
Arguments dirac {T} _ {R}.
Arguments dirac_measure {T} _ {R}.
Notation "\d_ a" := (dirac_measure a) : ring_scope.
Section dirac_lemmas.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType).
Lemma finite_card_dirac (A : set T) : finite_set A →
\esum_(i in A) \d_ i A = (#|` fset_set A|%:R)%:E :> \bar R.
Lemma infinite_card_dirac (A : set T) : infinite_set A →
\esum_(i in A) \d_ i A = +oo :> \bar R.
End dirac_lemmas.
Section measure_sum.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType).
Variables (m : {measure set T → \bar R}^nat) (n : nat).
Definition msum (A : set T) : \bar R := \sum_(k < n) m k A.
Let msum0 : msum set0 = 0.
Let msum_ge0 B : 0 ≤ msum B.
Let msum_sigma_additive : semi_sigma_additive msum.
Canonical measure_sum : {measure set T → \bar R} :=
Measure.Pack _ (Measure.Axioms msum0 msum_ge0 msum_sigma_additive).
End measure_sum.
Arguments msum {T R}.
Arguments measure_sum {T R}.
Section measure_zero.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType).
Definition mzero (A : set T) : \bar R := 0.
Let mzero0 : mzero set0 = 0.
Let mzero_ge0 B : 0 ≤ mzero B.
Let mzero_sigma_additive : semi_sigma_additive mzero.
Canonical measure_zero : {measure set T → \bar R} :=
Measure.Pack _ (Measure.Axioms mzero0 mzero_ge0 mzero_sigma_additive).
End measure_zero.
Arguments mzero {T R}.
Arguments measure_zero {T R}.
Section measure_add.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType).
Variables (m1 m2 : {measure set T → \bar R}).
Definition measure_add := measure_sum (fun n ⇒ if n is 0%N then m1 else m2) 2.
Lemma measure_addE A : measure_add A = m1 A + m2 A.
End measure_add.
Section measure_series.
Local Open Scope ereal_scope.
Variables (T : measurableType) (R : realType).
Variables (m : {measure set T → \bar R}^nat) (n : nat).
Definition mseries (A : set T) : \bar R := \sum_(n ≤ k <oo) m k A.
Let mseries0 : mseries set0 = 0.
Let mseries_ge0 B : 0 ≤ mseries B.
Let mseries_sigma_additive : semi_sigma_additive mseries.
Canonical measure_series : {measure set T → \bar R} :=
Measure.Pack _ (Measure.Axioms mseries0 mseries_ge0 mseries_sigma_additive).
End measure_series.
Arguments mseries {T R}.
Arguments measure_series {T R}.
Section measure_restr.
Variables (T : measurableType) (R : realType) (mu : {measure set T → \bar R}).
Variables (D : set T) (mD : measurable D).
Let measure_restr' (X : set _) : \bar R := mu (X `&` D).
Let measure_restr'0 : measure_restr' set0 = 0%E.
Let measure_restr'_ge0 (A : set _) : (0 ≤ measure_restr' A)%E.
Let measure_restr'_sigma_additive : semi_sigma_additive measure_restr'.
Definition measure_restr : {measure set _ → \bar R} :=
Measure.Pack _ (Measure.Axioms
measure_restr'0 measure_restr'_ge0 measure_restr'_sigma_additive).
Lemma measure_restrE A : measure_restr A = mu (A `&` D).
End measure_restr.
Lemma big_trivIset (I : choiceType) D T (R : Type) (idx : R)
(op : Monoid.com_law idx) (A : I → set T) (F : set T → R) :
finite_set D → trivIset D A → F set0 = idx →
\big[op/idx]_(i <- fset_set D) F (A i) =
\big[op/idx]_(X <- (A @` fset_set D)%fset) F X.
Section covering.
Context {T : Type}.
Implicit Type (C : ∀ I, set (set I)).
Implicit Type (P : ∀ I, set I → set (I → set T)).
Definition covered_by C P :=
[set X : set T | ∃ I D A, [/\ C I D, P I D A & X = \bigcup_(i in D) A i]].
Lemma covered_bySr C P P' : (∀ I D A, P I D A → P' I D A) →
covered_by C P `<=` covered_by C P'.
Lemma covered_byP C P I D A : C I D → P I D A →
covered_by C P (\bigcup_(i in D) A i).
Lemma covered_by_finite P :
(∀ I (D : set I) A, (∀ i, D i → A i = set0) → P I D A) →
(∀ (I : pointedType) D A, finite_set D → P I D A →
P nat `I_#|` fset_set D| (A \o nth point (fset_set D))) →
covered_by (@finite_set) P =
[set X : set T | ∃ n A, [/\ P nat `I_n A & X = \bigcup_(i in `I_n) A i]].
Lemma covered_by_countable P :
(∀ I (D : set I) A, (∀ i, D i → A i = set0) → P I D A) →
(∀ (I : pointedType) (D : set I) (A : I → set T) (f : nat → I),
set_surj [set: nat] D f →
P I D A → P nat [set: nat] (A \o f)) →
covered_by (@countable) P =
[set X : set T | ∃ A, [/\ P nat [set: nat] A & X = \bigcup_i A i]].
End covering.
Module SetRing.
Definition type (T : Type) := T.
Section SetRing.
Context {T : semiRingOfSetsType}.
Notation rT := (type T).
Canonical ring_eqType := EqType rT ptclass.
Canonical ring_choiceType := ChoiceType rT ptclass.
Canonical ring_ptType := PointedType rT ptclass.
#[export]
HB.instance Definition _ := isRingOfSets.Build rT ptclass
(@setring0 T measurable) (@setringU T measurable) (@setringDI T measurable).
Definition ring := [the ringOfSetsType of rT].
Lemma ring_measurableE : @measurable ring = measurable_fin_trivIset.
Lemma ring_fsets (A : set rT) : measurable A → ∃ B : {fset set T},
[/\ all [pred X | X != set0] B,
trivIset [set` B] id,
(∀ X : set T, X \in B → measurable X) &
A = \bigcup_(X in [set` B]) X].
Definition decomp (A : set rT) : {fset set T} :=
if A == set0 then [fset set0]%fset else
if pselect (measurable A) is left mA then projT1 (cid (ring_fsets mA)) else [fset A]%fset.
Lemma decomp_triv (A : set rT) : trivIset [set` decomp A] id.
Hint Resolve decomp_triv : core.
Lemma all_decomp_neq0 (A : set rT) : A !=set0 → all [pred X | X != set0] (decomp A).
Lemma decomp_neq0 (A : set rT) X : A !=set0 → X \in decomp A → X !=set0.
Lemma decomp_measurable (A : set rT) (X : set T) :
measurable A → X \in decomp A → measurable X.
Lemma cover_decomp (A : set rT) : \bigcup_(X in [set` decomp A]) X = A.
Lemma decomp_sub (A : set rT) (X : set T) : X \in decomp A → X `<=` A.
Lemma decomp_set0 : decomp set0 = [fset set0]%fset.
Lemma decompN0 (A : set rT) : decomp A != fset0.
Definition measure (R : numDomainType) (mu : set T → \bar R)
(A : set rT) : \bar R := \sum_(X <- decomp A) mu X.
Section additive_measure.
Context {R : realFieldType} (mu : {additive_measure set T → \bar R}).
Arguments big_trivIset {I D T R idx op} A F.
Lemma Rmu_fin_bigcup (I : choiceType) (D : set I) (F : I → set T) :
finite_set D → trivIset D F → (∀ i, D i → measurable (F i)) →
Rmu (\bigcup_(i in D) F i) = \sum_(i <- fset_set D) mu (F i).
Lemma RmuE (A : set T) : measurable A → Rmu A = mu A.
Lemma Rmu0 : Rmu set0 = 0.
Lemma Rmu_ge0 A : Rmu A ≥ 0.
Lemma Rmu_additive : semi_additive Rmu.
Lemma Rmu_additive_measure : additive_measure Rmu.
Canonical measure_additive_measure :=
AdditiveMeasure Rmu_additive_measure.
End additive_measure.
End SetRing.
Module Exports.
Canonical ring_eqType.
Canonical ring_choiceType.
Canonical ring_ptType.
Canonical measure_additive_measure.
End Exports.
End SetRing.
Export SetRing.Exports.
Lemma le_measure (R : realFieldType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}) :
{in measurable &, {homo mu : A B / A `<=` B >-> (A ≤ B)%E}}.
Lemma measure_le0 (T : semiRingOfSetsType) (R : realFieldType)
(mu : {additive_measure set T → \bar R}) (A : set T) :
(mu A ≤ 0)%E = (mu A == 0)%E.
Section more_content_semiring_lemmas.
Variables (R : realFieldType) (T : semiRingOfSetsType).
Variable mu : {additive_measure set T → \bar R}.
Lemma content_sub_additive : sub_additive mu.
Lemma content_sub_fsum (I : choiceType) D (A : set T) (A_ : I → set T) :
finite_set D →
(∀ i, D i → measurable (A_ i)) →
measurable A →
A `<=` \bigcup_(i in D) A_ i → mu A ≤ \sum_(i \in D) mu (A_ i).
(* (* alternative proof *)
Theorem semi_Boole_inequality : sub_additive mu.
Proof.
move=> X A n Am Xm Xsub; rewrite -SetRing.RmuE//.
under eq_bigr => i do rewrite -SetRing.RmuE; do ?by apply: Am⇒ /=.
pose rT := SetRing.type T.
have {}Am i : `I_n i -> measurable (A i : set rT).
by move=> *; apply/SetRing.measurableW/Am => /=.
have {}Xm : measurable (X : set rT) by exact: SetRing.measurableW.
pose ammu := additive_measure of SetRing.measure mu.
rewrite (le_trans (le_measure ammu _ _ Xsub)) ?inE// {Xsub}.
by rewrite -bigcup_mkord; apply: fin_bigcup_measurable.
elim: n Am Xm => |n IHn Am Xm; first by rewrite !big_ord0 measure0.
have Anm : measurable (A n : set rT) by apply: Am => /=.
set B := \bigsetU/set0_(i < n) A i.
set C := \bigsetU/set0_(i < n.+1) A i.
have -> : C = B `|` (A n `\` B).
suff -> : A n `\` B = C `\` B by rewrite setDUK// /C big_ord_recr/=; left.
by rewrite /C big_ord_recr/= !setDE setIUl -!setDE setDv set0U.
have Bm : measurable (B : set rT).
by rewrite -Bbigcup_mkord; apply: fin_bigcup_measurable => //= i /ltnW/Am.
rewrite measureU // ?setDIK//; last exact: measurableD.
rewrite (@le_trans _ _ (ammu B + ammu (A n))) // ?lee_add2l //; last first.
by rewrite big_ord_recr /= lee_add2r// IHn// => i /ltnW/Am.
by rewrite le_measure // ?inE// ?setDE//; exact: measurableD.
Qed. *)
End more_content_semiring_lemmas.
Section content_ring_lemmas.
Variables (R : realType) (T : ringOfSetsType).
Variable mu : {additive_measure set T → \bar R}.
Lemma content_ring_sup_sigma_additive (A : nat → set T) :
(∀ i, measurable (A i)) → measurable (\bigcup_i A i) →
trivIset [set: nat] A → \sum_(i <oo) mu (A i) ≤ mu (\bigcup_i A i).
Lemma content_ring_sigma_additive : sigma_sub_additive mu → semi_sigma_additive mu.
End content_ring_lemmas.
Section ring_sigma_sub_additive_content.
Context (R : realType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}).
Import SetRing.
Lemma ring_sigma_sub_additive : sigma_sub_additive mu → sigma_sub_additive Rmu.
Lemma ring_sigma_additive : sigma_sub_additive mu → semi_sigma_additive Rmu.
End ring_sigma_sub_additive_content.
Section more_premeasure_ring_lemmas.
Variables (R : realType) (T : semiRingOfSetsType).
Variable mu : {measure set T → \bar R}.
Import SetRing.
Lemma measure_sigma_sub_additive : sigma_sub_additive mu.
End more_premeasure_ring_lemmas.
Section ring_sigma_additive_measure.
Context (R : realType) (T : semiRingOfSetsType)
(mu : {measure set T → \bar R}).
Import SetRing.
Canonical set_ring_measure : {measure set (SetRing.type T) → \bar R} :=
@Measure.Pack _ _ (Phant _) Rmu
(Measure.Axioms (measure0 _) (measure_ge0 _) ring_sigma_additive_measure).
End ring_sigma_additive_measure.
Lemma measureIl (R : realFieldType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}) (A B : set T) :
measurable A → measurable B → (mu (A `&` B) ≤ mu A)%E.
Lemma measureIr (R : realFieldType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}) (A B : set T) :
measurable A → measurable B → (mu (A `&` B) ≤ mu B)%E.
Lemma subset_measure0 (T : semiRingOfSetsType) (R : realType)
(mu : {additive_measure set T → \bar R}) (A B : set T) :
measurable A → measurable B → A `<=` B →
mu B = 0%E → mu A = 0%E.
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.
Lemma measureUfinr (T : ringOfSetsType) (R : realFieldType) (A B : set T)
(mu : {measure set T → \bar R}):
measurable A → measurable B → (mu B < +oo)%E →
mu (A `|` B) = (mu A + mu B - mu (A `&` B))%E.
Lemma measureUfinl (T : ringOfSetsType) (R : realFieldType) (A B : set T)
(mu : {measure set T → \bar R}):
measurable A → measurable B → (mu A < +oo)%E →
mu (A `|` B) = (mu A + mu B - mu (A `&` B))%E.
Lemma eq_measureU (T : ringOfSetsType) (R : realFieldType) (A B : set T)
(mu mu' : {measure set T → \bar R}):
measurable A → measurable B →
mu A = mu' A → mu B = mu' B → mu (A `&` B) = mu' (A `&` B) →
mu (A `|` B) = mu' (A `|` B).
Lemma null_set_setU (R : realFieldType) (T : ringOfSetsType)
(mu : {measure set T → \bar R}) (A B : set T) :
measurable A → measurable B → mu A = 0%E → mu B = 0%E → mu (A `|` B) = 0%E.
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) n :
(∀ i, `I_n i → measurable (A i)) →
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}).
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 : {additive_measure _ → _}) A :
measurable A → mu.-negligible A ↔ mu A = 0.
Lemma negligible_set0 (mu : {additive_measure _ → _}) : mu.-negligible set0.
Lemma measure_negligible (mu : {additive_measure set T → \bar R}) (A : set T) :
measurable A → mu.-negligible A → mu A = 0%E.
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) := ∀ (F : (set T) ^nat),
mu (\bigcup_n (F n)) ≤ \sum_(i <oo) mu (F 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.
#[global] Hint Extern 0 (_ set0 = 0) ⇒ solve [apply: outer_measure0] : core.
#[global] 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 : 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 : set T → \bar R) := T.
Section caratheodory_sigma_algebra.
Variables (R : realType) (T : pointedType) (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.
Section caratheodory_measure.
Variables (R : realType) (T : pointedType) (mu : {outer_measure set T → \bar R}).
Lemma caratheodory_measure0 : mu (set0 : set U) = 0.
Lemma caratheodory_measure_ge0 (A : set U) : 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.
Lemma epsilon_trick (R : realType) (A : (\bar R)^nat) e
(P : pred nat) : (∀ n, 0 ≤ A n) → (0 ≤ e)%R →
\sum_(i <oo | P i) (A i + (e / (2 ^ i.+1)%:R)%:E) ≤
\sum_(i <oo | P i) A i + e%:E.
Section measurable_cover.
Variable T : semiRingOfSetsType.
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 : semiRingOfSetsType).
Variable mu : set T → \bar R.
Hypothesis measure0 : mu set0 = 0.
Hypothesis measure_ge0 : ∀ X, mu X ≥ 0.
Hint Resolve measure_ge0 measure0 : core.
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.
Section measure_extension.
Variables (R : realType) (T : semiRingOfSetsType).
Variable mu : {additive_measure set T → \bar R}.
Canonical outer_measure_of_measure (R : realType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}) : {outer_measure set T → \bar R} :=
OuterMeasure (OuterMeasure.Axioms
(mu_ext0 (measure0 mu) (measure_ge0 mu))
(mu_ext_ge0 (measure_ge0 mu))
(le_mu_ext mu)
(mu_ext_sigma_subadditive (measure_ge0 mu))).
End measure_extension.
Section g_salgebra_measure_unique_trace.
Variables (R : realType) (T : measurableType) (G : set (set T)).
Variables (D : set T) (mD : measurable D).
Let H := [set X | G X ∧ X `<=` D] .
Hypotheses (Hm : H `<=` measurable) (setIH : setI_closed H) (HD : H D).
Variables m1 m2 : {measure set T → \bar R}.
Hypotheses (m1m2 : ∀ A, H A → m1 A = m2 A) (m1oo : (m1 D < +oo)%E).
Lemma g_salgebra_measure_unique_trace :
(∀ X, (<<s D, H >>) X → X `<=` D) → ∀ X, <<s D, H >> X →
m1 X = m2 X.
End g_salgebra_measure_unique_trace.
Section g_salgebra_measure_unique.
Variables (R : realType) (T : measurableType) (G : set (set T)).
Hypothesis Gm : G `<=` measurable.
Variable g : (set T)^nat.
Hypotheses (Gg : ∀ i, G (g i)).
Hypothesis g_cover : \bigcup_k (g k) = setT.
Variables m1 m2 : {measure set T → \bar R}.
Lemma g_salgebra_measure_unique_cover :
(∀ n A, <<s G >> A → m1 (g n `&` A) = m2 (g n `&` A)) →
∀ A, <<s G >> A → m1 A = m2 A.
Hypothesis setIG : setI_closed G.
Hypothesis m1m2 : ∀ A, G A → m1 A = m2 A.
Hypothesis m1goo : ∀ k, (m1 (g k) < +oo)%E.
Lemma g_salgebra_measure_unique : ∀ E, <<s G >> E → m1 E = m2 E.
End g_salgebra_measure_unique.
Section measure_unique.
Variables (R : realType) (T : measurableType) (G : set (set T)).
Variable g : (set T)^nat.
Hypotheses (mG : measurable = <<s G >>) (setIG : setI_closed G).
Hypothesis Gg : ∀ i, G (g i).
Hypothesis g_cover : \bigcup_k (g k) = setT.
Variables m1 m2 : {measure set T → \bar R}.
Hypothesis m1m2 : ∀ A, G A → m1 A = m2 A.
Hypothesis m1goo : ∀ k, (m1 (g k) < +oo)%E.
Lemma measure_unique A : measurable A → m1 A = m2 A.
End measure_unique.
Arguments measure_unique {R T} G g.
Lemma measurable_mu_extE (R : realType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}) X :
sigma_sub_additive mu →
measurable X → mu_ext mu X = mu X.
Section Rmu_ext.
Import SetRing.
Lemma Rmu_ext (R : realType) (T : semiRingOfSetsType)
(mu : {additive_measure set T → \bar R}) :
mu_ext (measure mu) = mu_ext mu.
End Rmu_ext.
Lemma measurable_Rmu_extE (R : realType) (T : semiRingOfSetsType)
(rT := @SetRing.ring T) (mu : {additive_measure set T → \bar R}) X :
sigma_sub_additive mu →
measurable (X : set rT) → mu_ext mu X = SetRing.measure mu X.
Section Hahn_extension.
Variables (R : realType) (T : semiRingOfSetsType).
Variable mu : {additive_measure set T → \bar R}.
Let M : measurableType := [the measurableType of caratheodory_type (mu_ext mu)].
Hypothesis mu_sub : sigma_sub_additive mu.
Let Rmu := SetRing.measure mu.
Lemma sub_caratheodory : <<s @measurable T >> `<=` @measurable M.
Let I : measurableType := g_measurableType (@measurable T).
Definition Hahn_ext : set I → \bar R := mu_ext mu.
Canonical Hahn_ext_measure : {measure set I → \bar R} :=
@Measure.Pack _ _ _ Hahn_ext (Measure.Axioms
Hahn_ext0 Hahn_ext_ge0 Hahn_ext_sigma_additive).
Lemma Hahn_ext_sigma_finite : @sigma_finite _ T setT mu →
@sigma_finite _ I setT Hahn_ext.
Lemma Hahn_ext_unique : @sigma_finite _ T setT mu →
∀ mu' : {measure set I → \bar R},
(∀ X, @measurable T X → mu X = mu' X) →
∀ X, @measurable I X → Hahn_ext X = mu' X.
End Hahn_extension.
Lemma caratheodory_measurable_mu_ext (R : realType) (T : measurableType)
(mu : {measure set T → \bar R}) A :
measurable A → (mu_ext mu).-measurable A.
Definition preimage_classes (T1 T2 : measurableType) (T : Type)
(f1 : T → T1) (f2 : T → T2) :=
<<s preimage_class setT f1 measurable `|`
preimage_class setT f2 measurable >>.
Section product_lemma.
Variables (T1 T2 : measurableType) (T : pointedType).
Variables (f1 : T → T1) (f2 : T → T2) (T3 : Type) (g : T3 → T).
Lemma preimage_classes_comp : preimage_classes (f1 \o g) (f2 \o g) =
preimage_class setT g (preimage_classes f1 f2).
End product_lemma.
Definition prod_measurable (T1 T2 : measurableType) := (T1 × T2)%type.
Section product_salgebra_instance.
Variables (T1 T2 : measurableType).
Let f1 := @fst T1 T2.
Let f2 := @snd T1 T2.
Let prod_salgebra_set0 : preimage_classes f1 f2 (set0 : set (T1 × T2)).
Let prod_salgebra_setC A : preimage_classes f1 f2 A →
preimage_classes f1 f2 (~` A).
Let prod_salgebra_bigcup (F : _^nat) : (∀ i, preimage_classes f1 f2 (F i))
→ preimage_classes f1 f2 (\bigcup_i (F i)).
Definition prod_measurableType := [the measurableType of prod_measurable T1 T2].
End product_salgebra_instance.
Lemma measurableM (T1 T2 : measurableType) (A : set T1) (B : set T2) :
measurable A → measurable B → measurable (A `*` B).
Section product_salgebra_measurableType.
Variables (T1 T2 : measurableType).
Let M1 := @measurable T1.
Let M2 := @measurable T2.
Let M1xM2 := [set A `*` B | A in M1 & B in M2].
Lemma measurable_prod_measurableType :
@measurable (prod_measurableType T1 T2) = <<s M1xM2 >>.
End product_salgebra_measurableType.
Section product_salgebra_g_measurableTypeR.
Variables (T1 : measurableType) (T2 : pointedType) (C2 : set (set T2)).
Hypothesis (setTC2 : setT `<=` C2).
NB: useful?
Lemma measurable_prod_g_measurableTypeR :
@measurable (prod_measurableType T1 (g_measurableType C2))
= <<s [set A `*` B | A in measurable & B in C2] >>.
End product_salgebra_g_measurableTypeR.
Section product_salgebra_g_measurableType.
Variables (T1 T2 : pointedType) (C1 : set (set T1)) (C2 : set (set T2)).
Hypotheses (setTC1 : setT `<=` C1) (setTC2 : setT `<=` C2).
Lemma measurable_prod_g_measurableType :
@measurable (prod_measurableType (g_measurableType C1) (g_measurableType C2))
= <<s [set A `*` B | A in C1 & B in C2] >>.
End product_salgebra_g_measurableType.
Section prod_measurable_fun.
Variables (T T1 T2 : measurableType) (f : T → prod_measurableType T1 T2).
Lemma prod_measurable_funP : measurable_fun setT f ↔
measurable_fun setT (fst \o f) ∧ measurable_fun setT (snd \o f).
End prod_measurable_fun.
Section partial_measurable_fun.
Variables (T T1 T2 : measurableType) (f : prod_measurableType T1 T2 → T).
Lemma measurable_fun_prod1 x :
measurable_fun setT f → measurable_fun setT (fun y ⇒ f (x, y)).
Lemma measurable_fun_prod2 y :
measurable_fun setT f → measurable_fun setT (fun x ⇒ f (x, y)).
End partial_measurable_fun.
@measurable (prod_measurableType T1 (g_measurableType C2))
= <<s [set A `*` B | A in measurable & B in C2] >>.
End product_salgebra_g_measurableTypeR.
Section product_salgebra_g_measurableType.
Variables (T1 T2 : pointedType) (C1 : set (set T1)) (C2 : set (set T2)).
Hypotheses (setTC1 : setT `<=` C1) (setTC2 : setT `<=` C2).
Lemma measurable_prod_g_measurableType :
@measurable (prod_measurableType (g_measurableType C1) (g_measurableType C2))
= <<s [set A `*` B | A in C1 & B in C2] >>.
End product_salgebra_g_measurableType.
Section prod_measurable_fun.
Variables (T T1 T2 : measurableType) (f : T → prod_measurableType T1 T2).
Lemma prod_measurable_funP : measurable_fun setT f ↔
measurable_fun setT (fst \o f) ∧ measurable_fun setT (snd \o f).
End prod_measurable_fun.
Section partial_measurable_fun.
Variables (T T1 T2 : measurableType) (f : prod_measurableType T1 T2 → T).
Lemma measurable_fun_prod1 x :
measurable_fun setT f → measurable_fun setT (fun y ⇒ f (x, y)).
Lemma measurable_fun_prod2 y :
measurable_fun setT f → measurable_fun setT (fun x ⇒ f (x, y)).
End partial_measurable_fun.