proposition: Lemma jordan_decomp (A : set T) : measurable A -> nu A = (cadd [the charge _ _ of jordan_pos] ([the charge _ _ of cscale (-1) [the charge _ _ of jordan_neg]])) A.
proof: Proof. move=> mA. rewrite /cadd cjordan_posE /= /cscale EFinN mulN1e cjordan_negE oppeK. rewrite /crestr0 mem_set// -[in LHS](setIT A). case: nuPN => _ _ <- PN0; rewrite setIUr chargeU//. - exact: measurableI. - exact: measurableI. - by rewrite setIACA PN0 setI0. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets cardinality) mathcomp(functions fsbigop set_interval) HB(structures) reals ereal signed topology numfun normedtype sequences esum measure realfun lebesgue_measure lebesgue_integral