proposition: Lemma jordan_pos_dominates (mu : {measure set T -> \bar R}) : nu `<< mu -> jordan_pos `<< mu.
proof: Proof. move=> nu_mu A mA muA0; have := nu_mu A mA muA0. rewrite jordan_posE// cjordan_posE /crestr0 mem_set// /crestr/=. have mAP : measurable (A `&` P) by exact: measurableI. suff : mu (A `&` P) = 0 by move/(nu_mu _ mAP) => ->. by apply/eqP; rewrite eq_le measure_ge0// andbT -muA0 le_measure// inE. 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