tentative proof of Radon-Nikodym

CHANGELOG_UNRELEASED.md

@@ -64,6 +64,21 @@
   + lemma `integrable_sum`
 - in `probability.v`
   + lemma `cantelli`
+- in `classical_sets.v`:
+  + lemmas `preimage_mem_true`, `preimage_mem_false`
+- in `measure.v`:
+  + definition `measure_dominates`, notation `` `<< ``
+  + lemma `measure_dominates_trans`
+- in `measure.v`:
+  + defintion `mfrestr`
+- in `charge.v`:
+  + definition `measure_of_charge`
+  + definition `crestr0`
+  + definitions `jordan_neg`, `jordan_pos`
+  + lemmas `jordan_decomp`, `jordan_pos_dominates`, `jordan_neg_dominates`
+  + lemma `radon_nikodym_finite`
+  + definition `Radon_Nikodym`, notation `'d nu '/d mu`
+  + theorems `Radon_Nikodym_integrable`, `Radon_Nikodym_integral`
 
 - in `measure.v`:
   + lemmas `measurable_pair1`, `measurable_pair2`

classical/classical_sets.v

@@ -1387,6 +1387,15 @@ Qed.
 Lemma preimage10 {T R} {f : T -> R} {x} : ~ range f x -> f @^-1` [set x] = set0.
 Proof. by move/preimage10P. Qed.
 
+Lemma preimage_mem_true {T} (A : set T) : mem A @^-1` [set true] = A.
+Proof. by apply/seteqP; split => [x/= /set_mem//|x /mem_set]. Qed.
+
+Lemma preimage_mem_false {T} (A : set T) : mem A @^-1` [set false] = ~` A.
+Proof.
+apply/seteqP; split => [x/=|x/=]; last exact: memNset.
+by apply: contraFnot; exact/mem_set.
+Qed.
+
 End image_lemmas.
 Arguments sub_image_setI {aT rT f A B} t _.