proposition: Lemma semi_sigma_additive_elebesgue_measure : semi_sigma_additive elebesgue_measure.
proof: Proof. move=> /= F mF tF mUF; rewrite /elebesgue_measure. rewrite [X in lebesgue_measure X](_ : _ = \bigcup_n (fine @` (F n `\` [set -oo; +oo]%E))); last first. rewrite predeqE => r; split. by move=> [x [[n _ Fnx xoo <-]]]; exists n => //; exists x. by move=> [n _ [x [Fnx xoo <-{r}]]]; exists x => //; split => //; exists n. apply: (@measure_semi_sigma_additive _ _ _ (@lebesgue_measure R) (fun n => fine @` (F n `\` [set -oo; +oo]%E))). - move=> n; have := mF n. move=> [X mX [X' mX']] XX'Fn. apply: measurable_image_fine. rewrite -XX'Fn. apply: measurableU; first exact: measurable_image_EFin. by case: mX' => //; exact: measurableU. - move=> i j _ _ [x [[a [Fia aoo ax] [b [Fjb boo] bx]]]]. move: tF => /(_ i j Logic.I Logic.I); apply. suff ab : a = b by exists a; split => //; rewrite ab. move: a b {Fia Fjb} aoo boo ax bx. move=> [a| |] [b| |] /=. + by move=> _ _ -> ->. + by move=> _; rewrite not_orP => -[_]/(_ erefl). + by move=> _; rewrite not_orP => -[]/(_ erefl). + by rewrite not_orP => -[_]/(_ erefl). + by rewrite not_orP => -[_]/(_ erefl). + by rewrite not_orP => -[_]/(_ erefl). + by rewrite not_orP => -[]/(_ erefl). + by rewrite not_orP => -[]/(_ erefl). + by rewrite not_orP => -[]/(_ erefl). - move: mUF. rewrite {1}/measurable /emeasurable /= => -[X mX [Y []]] {Y}. - rewrite setU0 => h. rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-{r}]]]. have : (\bigcup_n F n) x by exists n. by rewrite -h => -[x' Xx' <-]. have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; exists r. by exists n => //; exists r%:E => //; split => //; case. - move=> h. rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-]]]. have : (\bigcup_n F n) x by exists n. by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[]. have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. by exists n => //; exists r%:E => //; split => //; case. - move=> h. rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-]]]. have : (\bigcup_n F n) x by exists n. by rewrite -h => -[[x' Xx' <-//]|xoo']; move/not_orP : xoo => -[]. have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. by exists n => //; exists r%:E => //; split => //; case. - move=> h. rewrite [X in measurable X](_ : _ = X) // predeqE => r; split => [|Xr]. move=> -[n _ [x [Fnx xoo <-]]]. have : (\bigcup_n F n) x by exists n. by rewrite -h => -[[x' Xx' <-//]|]. have [n _ Fnr] : (\bigcup_n F n) r%:E by rewrite -h; left; exists r. by exists n => //; exists r%:E => //; split => //; case. Qed.
imports: mathcomp(all_ssreflect ssralg ssrnum ssrint interval) mathcomp(finmap fingroup perm rat) mathcomp(mathcomp_extra boolp classical_sets functions) mathcomp(cardinality fsbigop) reals ereal signed topology numfun normedtype HB(structures) sequences esum measure real_interval realfun exp lebesgue_stieltjes_measure