On this page
Atoms of a finite measure
Imports 0 library modules and 20 external
External: HB.structures, mathcomp.classical.all_ssreflect_compat, mathcomp.algebra.algebraic_hierarchy.ssralg, mathcomp.algebra.numeric_hierarchy.ssrnum, mathcomp.finmap.finmap, mathcomp.classical.boolp, mathcomp.classical.classical_sets, mathcomp.classical.functions, mathcomp.classical.cardinality, mathcomp.reals.reals, mathcomp.analysis.ereal, mathcomp.analysis.topology_theory.topology, mathcomp.analysis.normedtype_theory.normedtype, mathcomp.analysis.sequences, mathcomp.analysis.esum, mathcomp.analysis.measure_theory.measure, mathcomp.analysis.lebesgue_measure, mathcomp.analysis.numfun, mathcomp.analysis.lebesgue_integral_theory.lebesgue_integral, mathcomp.analysis.probability_theory.probability
Required by 1 files of the paper proofs
On a measurable type whose singletons are measurable, the atoms of a measure P are the points of nonzero mass. A finite measure has countably many atoms, and a countable set without atoms is null. Hence a set of pairs whose vertical and horizontal sections are countable is charged by a product of two probabilities only above countably many points of the first factor, and not at all when the first factor has no atom.
atoms P | the set of the points x with P [set x] != 0 |
Main results:
- atoms_countable: the atoms of a finite measure form a countable set;
- countable_atomless_null: a countable set none of whose points is an atom is null;
- sections_charge_countable: for sets S x with S x countable for every x and [set x | S x y] countable for every y, the points x with P (S x) != 0 form a countable set, for a finite measure P;
- product_sections_null: for a measure P, a probability Q and a set A of pairs with countable vertical and horizontal sections, there is a countable set N with (P \x Q) (A `&` (~` N `*` setT)) = 0;
- atomless_product_null: if moreover P is a probability without atoms and A is measurable, then (P \x Q) A = 0.
Main results
| Results | Statement |
|---|---|
On a measurable type whose singletons are measurable, the atoms of a measure P are the points x with P [set x] != 0. A finite measure has countably many atoms, and a countable set without atoms is null. Hence, for sets S x such that every S x and every [set x | S x y] is countable, the points x with P (S x) != 0 form a countable set, for a finite measure P. | |
For a measure P, a probability Q and a set A of pairs whose vertical and horizontal sections are countable, there is a countable set N of first coordinates with (P \x Q) (A minus N x T2) = 0. If moreover P is a probability without atoms and A is measurable, then (P \x Q) A = 0. |
Declarations6 exported
Context d (T : measurableType d) (R : realType). Local Open Scope ereal_scope.
forall [d : measure_display] [T : measurableType d] [R : realType], (set T -> \bar R) -> set T
Definition atoms (P : set T -> \bar R) := [set x : T | P [set x] != 0].
The atoms of a set function on T: the points of nonzero mass.
On a measurable type whose singletons are measurable, the atoms of a measure P are the points x with P [set x] != 0. A finite measure has countably many atoms, and a countable set without atoms is null. Hence, for sets S x such that every S x and every [set x | S x y] is countable, the points x with P (S x) != 0 form a countable set, for a finite measure P.
Used by 2 declarations in 1 file
- this file: atoms_countable, sections_charge_countable
Hypothesis mT1 : forall x : T, measurable [set x].
forall [d : measure_display] [T : measurableType d] [R : realType], (forall x : T, d.-measurable [set x]) -> forall [P : measure T R] [C : set T], countable C -> (forall x : T, C x -> P [set x] = 0) -> P C = 0
A countable set none of whose points is an atom is null.
Stated in the README together with atoms.
Statement as written in the source
Lemma countable_atomless_null (P : {measure set T -> \bar R}) (C : set T) : countable C -> (forall x, C x -> P [set x] = 0) -> P C = 0.
Used by 2 declarations in 1 file
- this file: sections_charge_countable, atomless_product_null
Variable P : {finite_measure set T -> \bar R}.
forall [d : measure_display] [T : measurableType d] [R : realType], (forall x : T, d.-measurable [set x]) -> forall P : {finite_measure set T -> \bar R}, countable (atoms P)
The atoms of a finite measure: the points of mass > 1 / (k + 1) are at most (k + 1) P(T) for every k.
Stated in the README together with atoms.
Statement as written in the source
Lemma atoms_countable : countable (atoms P).
Used by 1 declaration in 1 file
- this file: sections_charge_countable
forall [d : measure_display] [T : measurableType d] [R : realType], (forall x : T, d.-measurable [set x]) -> forall (P : {finite_measure set T -> \bar R}) [X : Type] [S : X -> set T], (forall x : X, countable (S x)) -> (forall y : T, countable [set x | S x y]) -> countable [set x | P (S x) != 0]
The points x whose set S x has positive mass.
Stated in the README together with atoms.
Statement as written in the source
Lemma sections_charge_countable (X : Type) (S : X -> set T) : (forall x, countable (S x)) -> (forall y, countable [set x | S x y]) -> countable [set x | P (S x) != 0].
Used by 1 declaration in 1 file
- this file: product_sections_null
Context d1 d2 (T1 : measurableType d1) (T2 : measurableType d2). Context (R : realType). Local Open Scope ereal_scope. Hypothesis mT2 : forall y : T2, measurable [set y].
forall [d1 d2 : measure_display] [T1 : measurableType d1] [T2 : measurableType d2] [R : realType], (forall y : T2, d2.-measurable [set y]) -> forall (P : measure T1 R) (Q : probability T2 R) [A : set (T1 * T2)], (forall x : T1, countable (xsection A x)) -> (forall y : T2, countable (ysection A y)) -> exists N : set T1, countable N /\ (P \x Q)%E (A `&` ~` N `*` [set: T2]) = 0
A product charges a set of pairs with countable sections only above countably many points of the first factor.
For a measure P, a probability Q and a set A of pairs whose vertical and horizontal sections are countable, there is a countable set N of first coordinates with (P \x Q) (A minus N x T2) = 0. If moreover P is a probability without atoms and A is measurable, then (P \x Q) A = 0.
Statement as written in the source
Lemma product_sections_null (P : {measure set T1 -> \bar R}) (Q : probability T2 R) (A : set (T1 * T2)) : (forall x, countable (xsection A x)) -> (forall y, countable (ysection A y)) -> exists N : set T1, countable N /\ (P \x Q) (A `&` (~` N `*` setT)) = 0.
Used by 1 declaration in 1 file
- this file: atomless_product_null
forall [d1 d2 : measure_display] [T1 : measurableType d1] [T2 : measurableType d2] [R : realType], (forall y : T2, d2.-measurable [set y]) -> forall [P : probability T1 R] (Q : probability T2 R) [A : set (T1 * T2)], (forall x : T1, d1.-measurable [set x]) -> (forall x : T1, P [set x] = 0) -> ((d1, d2).-prod).-measurable A -> (forall x : T1, countable (xsection A x)) -> (forall y : T2, countable (ysection A y)) -> (P \x Q)%E A = 0
A product whose first factor has no atom does not charge a measurable set of pairs with countable sections.
Stated in the README together with product_sections_null.
Statement as written in the source
Lemma atomless_product_null (P : probability T1 R) (Q : probability T2 R) (A : set (T1 * T2)) : (forall x : T1, measurable [set x]) -> (forall x, P [set x] = 0) -> measurable A -> (forall x, countable (xsection A x)) -> (forall y, countable (ysection A y)) -> (P \x Q) A = 0.