proposition: Theorem Hahn_decomposition : exists P N, hahn_decomposition nu P N.
proof: Proof. have [A0 [_ negA0 A0s0]] := next_elt set0. have [v [v0 Pv]] : {v | v 0%N = exist _ (A0, s_ set0, A0) (And3 (s_le0 set0) negA0 A0s0) /\ forall n, elt_rel (v n) (v n.+1)}. apply: dependent_choice_Type => -[[[A s] U] [/= s_le0' nsA]]. have [A' [? nsA' A's'] ] := next_elt U. by exists (exist _ (A', s_ U, U `|` A') (And3 (s_le0 U) nsA' A's')). have Ubig n : U_ (v n) = \big[setU/set0]_(i < n.+1) A_ (v i). elim: n => [|n ih]; first by rewrite v0/= big_ord_recr/= big_ord0 set0U v0. by have [_ _ ->] := Pv n; rewrite big_ord_recr/= -ih. have tA : trivIset setT (A_ \o v). apply: subsetC_trivIset => n. have [_ + _] := Pv n; move/subset_trans; apply. by apply: subsetC; rewrite Ubig big_ord_recr. set N := \bigcup_k (A_ (v k)). have mN : measurable N by exact: bigcup_measurable. have neg_set_N : negative_set nu N. by apply: bigcup_negative_set => i; exact: negative_set_A_. pose P := ~` N. have mP : measurable P by exact: measurableC. exists P, N; split; [|exact: neg_set_N|by rewrite /P setvU|by rewrite /P setICl]. split=> // D mD DP; rewrite leNgt; apply/negP => nuD0. have znuD n : z_ (v n) <= nu D. move: n => [|n]. by rewrite v0 /=; apply: ereal_inf_lb; exists D; split => //; rewrite setC0. have [-> _ _] := Pv n; apply: ereal_inf_lb => /=; exists D; split => //. apply: (subset_trans DP); apply: subsetC; rewrite Ubig. exact: bigsetU_bigcup. have max_le0 n : maxe (z_ (v n) * 2^-1%:E) (- 1%E) <= 0. by rewrite le_maxl leeN10 andbT pmule_lle0. have not_s_cvg_0 : ~ (z_ \o v) n @[n --> \oo] --> 0. move/fine_cvgP => -[zfin] /cvgrPdist_lt. have /[swap] /[apply] -[M _ hM] : (0 < `|fine (nu D)|)%R. by rewrite normr_gt0// fine_eq0// ?lt_eqF// fin_num_measure. near \oo => n. have /hM : (M <= n)%N by near: n; exists M. rewrite sub0r normrN /= ler0_norm ?fine_le0// ltr0_norm//; last first. by rewrite fine_lt0// nuD0 andbT ltNye_eq fin_num_measure. rewrite ltrN2; apply/negP; rewrite -leNgt fine_le ?fin_num_measure//. by near: n; exact. have nuN : nu N = \sum_(n <oo) nu (A_ (v n)). apply/esym/cvg_lim => //. by apply: charge_semi_sigma_additive; [|exact: tA|exact: bigcup_measurable]. have sum_A_maxe : \sum_(n <oo) nu (A_ (v n)) <= \sum_(n <oo) maxe (z_ (v n) * 2^-1%:E) (- 1%E) by exact: lee_npeseries. have : cvg (\sum_(0 <= k < n) maxe (z_ (v k) * 2^-1%:E) (- 1%E) @[n --> \oo]). by apply: is_cvg_ereal_npos_natsum_cond => n _ _; exact: max_le0. move=> /cvg_ex[[l| |]]; first last. - move/cvg_lim => limNoo. have : nu N <= -oo by rewrite -limNoo// nuN. by rewrite leNgt => /negP; apply; rewrite ltNye_eq fin_num_measure. - move/cvg_lim => limoo. have := @npeseries_le0 _ (fun n => maxe (z_ (v n) * 2^-1%:E) (- 1%E)) xpredT 0. by rewrite limoo// leNgt => /(_ (fun n _ => max_le0 n))/negP; apply. move/fine_cvgP => [Hfin cvgl]. have : cvg (series (fun n => fine (maxe (z_ (v n) * 2^-1%:E) (- 1%E))) n @[n --> \oo]). apply/cvg_ex; exists l; move: cvgl. rewrite (_ : _ \o _ = (fun n => \sum_(0 <= k < n) fine (maxe (z_ (v k) * 2^-1%:E)%E (- 1%E)%E))%R) //. apply/funext => n/=; rewrite sum_fine// => m _. rewrite le0_fin_numE; first by rewrite lt_maxr ltNyr orbT. by rewrite /maxe; case: ifPn => // _; rewrite mule_le0_ge0. move/cvg_series_cvg_0 => maxe_cvg_0. apply: not_s_cvg_0. rewrite (_ : _ \o _ = (fun n => z_ (v n) * 2^-1%:E) \* cst 2%:E); last first. by apply/funext => n/=; rewrite -muleA -EFinM mulVr ?mule1// unitfE. rewrite (_ : 0 = 0 * 2%:E); last by rewrite mul0e. apply: cvgeM; [by rewrite mule_def_fin| |exact: cvg_cst]. apply/fine_cvgP; split. move/cvgrPdist_lt : maxe_cvg_0 => /(_ _ ltr01)[M _ hM]; near=> n. have /hM : (M <= n)%N by near: n; exists M. rewrite sub0r normrN ltNge => maxe_lt1; rewrite fin_numE; apply/andP; split. by apply: contra maxe_lt1 => /eqP ->; rewrite max_r ?leNye//= normrN1 lexx. by rewrite lt_eqF// (@le_lt_trans _ _ 0)// mule_le0_ge0. apply/cvgrPdist_lt => _ /posnumP[e]. have : (0 < minr e%:num 1)%R by rewrite lt_minr// ltr01 andbT. move/cvgrPdist_lt : maxe_cvg_0 => /[apply] -[M _ hM]. near=> n; rewrite sub0r normrN. have /hM : (M <= n)%N by near: n; exists M. rewrite sub0r normrN /maxe/=; case: ifPn => [_|]. by rewrite normrN normr1 lt_minr ltxx andbF. by rewrite -leNgt => ? /lt_le_trans; apply; rewrite le_minl lexx. Unshelve. all: by end_near. 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