proposition: Lemma nonincreasing_cvg_mu d (T : algebraOfSetsType d) (R : realFieldType) (mu : {measure set T -> \bar R}) (F : (set T) ^nat) : mu (F 0%N) < +oo -> (forall i, measurable (F i)) -> measurable (\bigcap_n F n) -> nonincreasing_seq F -> mu \o F @ \oo --> mu (\bigcap_n F n).
proof: Proof. move=> F0pos mF mbigcapF niF; pose G n := F O `\` F n. have ? : mu (F 0%N) \is a fin_num by rewrite ge0_fin_numE. have F0E r : mu (F 0%N) - (mu (F 0%N) - r) = r. by rewrite oppeB ?addeA ?subee ?add0e// fin_num_adde_defr. rewrite -[x in _ --> x] F0E. have -> : mu \o F = fun n => mu (F 0%N) - (mu (F 0%N) - mu (F n)). by apply:funext => n; rewrite F0E. apply: cvgeB; rewrite ?fin_num_adde_defr//; first exact: cvg_cst. have -> : \bigcap_n F n = F 0%N `&` \bigcap_n F n. by rewrite setIidr//; exact: bigcap_inf. rewrite -measureD // setDE setC_bigcap setI_bigcupr -[x in bigcup _ x]/G. have -> : (fun n => mu (F 0%N) - mu (F n)) = mu \o G. by apply: funext => n /=; rewrite measureD// setIidr//; exact/subsetPset/niF. apply: nondecreasing_cvg_mu. - by move=> ?; apply: measurableD; exact: mF. - rewrite -setI_bigcupr; apply: measurableI; first exact: mF. by rewrite -@setC_bigcap; exact: measurableC. - by move=> n m NM; apply/subsetPset; apply: setDS; apply/subsetPset/niF. 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)