proposition: Lemma measurable_mu_extE d (R : realType) (T : semiRingOfSetsType d) (mu : {measure set T -> \bar R}) X : measurable X -> mu^* X = mu X.
proof: Proof. move=> mX; apply/eqP; rewrite eq_le; apply/andP; split. apply: ereal_inf_lb; exists (fun n => if n is 0%N then X else set0). by split=> [[]// _|t Xt]; exists 0%N. apply/cvg_lim => //; rewrite -cvg_shiftS. rewrite (_ : [sequence _]_n = cst (mu X)); first exact: cvg_cst. by rewrite funeqE => n /=; rewrite big_nat_recl//= big1 ?adde0. apply/lb_ereal_inf => x [A [mA XA] <-{x}]. have XUA : X = \bigcup_n (X `&` A n). rewrite predeqE => t; split => [Xt|[i _ []//]]. by have [i _ Ait] := XA _ Xt; exists i. apply: (@le_trans _ _ (\sum_(i <oo) mu (X `&` A i))). by rewrite measure_sigma_sub_additive//= -?XUA => // i; apply: measurableI. apply: lee_lim; [exact: is_cvg_nneseries|exact: is_cvg_nneseries|]. by apply: nearW => n; apply: lee_sum => i _; exact: measureIr. Qed.
imports: mathcomp(all_ssreflect all_algebra finmap) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop ) reals ereal signed topology normedtype sequences esum numfun HB(structures)