proposition: Lemma hahn_decomposition_lemma : measurable D -> {A | [/\ A `<=` D, nu.-negative_set A & nu A <= nu D]}.
proof: Proof. move=> mD; have [A0 [mA0 + A0d0]] := next_elt set0. rewrite setD0 => A0D. have [v [v0 Pv]] : {v : nat -> elt_type | v 0%N = exist _ (A0, d_ set0, A0) (And4 mA0 A0D (d_ge0 set0) A0d0) /\ forall n, elt_rel (v n) (v n.+1)}. apply: dependent_choice_Type => -[[[A' ?] U] [/= mA' A'D]]. have [A1 [mA1 A1DU A1t1] ] := next_elt U. have A1D : A1 `<=` D by apply: (subset_trans A1DU); apply: subDsetl. by exists (exist _ (A1, d_ U, U `|` A1) (And4 mA1 A1D (d_ge0 U) A1t1)). 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 rewrite -setTD; apply: setDSS => //; rewrite Ubig big_ord_recr. set Aoo := \bigcup_k A_ (v k). have mAoo : measurable Aoo by exact: bigcup_measurable. exists (D `\` Aoo). have cvg_nuA : (\sum_(0 <= i < n) nu (A_ (v i))) @[n --> \oo]--> nu Aoo. exact: charge_semi_sigma_additive. have nuAoo : 0 <= nu Aoo. move/cvg_lim : cvg_nuA => <-//=; apply: nneseries_ge0 => n _. exact: nuA_ge0. have A_cvg_0 : nu (A_ (v n)) @[n --> \oo] --> 0. rewrite [X in X @ _ --> _](_ : _ = (fun n => (fine (nu (A_ (v n))))%:E)); last first. by apply/funext => n/=; rewrite fineK// fin_num_measure. apply: continuous_cvg => //; apply: cvg_series_cvg_0. rewrite (_ : series _ = fine \o (fun n => \sum_(0 <= i < n) nu (A_ (v i)))); last first. apply/funext => n /=. by rewrite /series/= sum_fine//= => i _; rewrite fin_num_measure. move: cvg_nuA; rewrite -(@fineK _ (nu Aoo)) ?fin_num_measure//. by move=> /fine_cvgP[_ ?]; apply/cvg_ex; exists (fine (nu Aoo)). have mine_cvg_0 : (mine (g_ (v n) * 2^-1%:E) 1) @[n --> \oo] --> 0. apply: (@squeeze_cvge _ _ _ _ _ _ (fun n => nu (A_ (v n)))); [|exact: cvg_cst|by []]. by apply: nearW => n /=; rewrite nuA_g_ andbT le_minr lee01 andbT mule_ge0. have g_cvg_0 : (g_ \o v) n @[n --> \oo] --> 0 by apply: mine2_cvg_0_cvg_0 => //=. have nuDAoo : nu D >= nu (D `\` Aoo). rewrite -[in leRHS](@setDUK _ Aoo D); last first. by apply: bigcup_sub => i _; exact: A_D. by rewrite chargeU// ?leeDr// ?setDIK//; exact: measurableD. split; [by []| |by []]; split; [exact: measurableD | move=> E mE EDAoo]. pose H n := subDD (\big[setU/set0]_(i < n) A_ (v i)). have EH n : [set nu E] `<=` H n. have : nu E \in subDD Aoo by rewrite inE; exists E. rewrite -sub1set => /subset_trans; apply => x/= [F [mF FDAoo ?]]. exists F => //; split => //. by apply: (subset_trans FDAoo); apply: setDS; exact: bigsetU_bigcup. have nudelta n : nu E <= g_ (v n). move: n => [|n]. rewrite v0/=; apply: ereal_sup_ub => /=; exists E; split => //. by apply: (subset_trans EDAoo); exact: setDS. suff : nu E <= d_ (U_ (v n)) by have [<- _] := Pv n. have /le_ereal_sup := EH n.+1; rewrite ereal_sup1 => /le_trans; apply. apply/le_ereal_sup => x/= [A' [mA' A'D ?]]. exists A' => //; split => //. by apply: (subset_trans A'D); apply: setDS; rewrite Ubig. apply: (@closed_cvg _ _ _ _ _ (fun v => nu E <= v) _ _ _ g_cvg_0) => //. exact: closed_ereal_le_ereal. exact: nearW. 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