diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1d842d6fdb..c392db50d4 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -88,6 +88,28 @@ + new lemmas `weak_sep_cvg`, `weak_sep_nbhsE`, `weak_sep_openE`, `join_product_continuous`, `join_product_open`, `join_product_inj`, and `join_product_weak`. +- in `measure.v`: + + structure `FiniteMeasure`, notation `{finite_measure set _ -> \bar _}` + +- in `measure.v`: + + definition `sfinite_measure_def` + + mixin `Measure_isSFinite_subdef`, structure `SFiniteMeasure`, + notation `{sfinite_measure set _ -> \bar _}` + + mixin `SigmaFinite_isFinite` with field `fin_num_measure`, structure `FiniteMeasure`, + notation `{finite_measure set _ -> \bar _}` + + lemmas `sfinite_measure_sigma_finite`, `sfinite_mzero`, `sigma_finite_mzero`, `finite_mzero` + + factory `Measure_isFinite`, `Measure_isSFinite` + + lemma `sfinite_measure` + + mixin `FiniteMeasure_isSubProbability`, structure `SubProbability`, + notation `subprobability` + + factory `Measure_isSubProbability` + + factory `FiniteMeasure_isSubProbability` + + factory `Measure_isSigmaFinite` + + lemmas `fin_num_fun_finite_measure`, `finite_measure_fin_num_fun` + + definition `fin_num_fun` + + structure `FinNumFun` + + definition `finite_measure2` + + lemmas `finite_measure2_finite_measure`, `finite_measure_finite_measure2` ### Changed @@ -107,6 +129,11 @@ + lemma `max_fimfun_subproof` + mixin `IsNonNegFun`, structure `NonNegFun`, notation `{nnfun _ >-> _}` +- in `measure.v`: + + `finite_measure` is now a lemma that applies to a finite measure + + order of arguments of `isContent`, `Content`, `measure0`, `isMeasure0`, + `Measure`, `isSigmaFinite`, `SigmaFiniteContent`, `SigmaFiniteMeasure` + ### Renamed - in `measurable.v`: @@ -148,6 +175,9 @@ + `xsection_preimage_snd`, `ysection_preimage_fst` - in `constructive_ereal.v`: + `oppeD`, `oppeB` +- in `measure.v`: + + `sigma_finite` generalized from `numFieldType` to `numDomainType` + + `finite_measure_sigma_finite` generalized from `measurableType` to `algebraOfSetsType` ### Deprecated diff --git a/_CoqProject b/_CoqProject index 1a9dd0cdc9..92fccdda5b 100644 --- a/_CoqProject +++ b/_CoqProject @@ -38,6 +38,8 @@ theories/numfun.v theories/lebesgue_integral.v theories/summability.v theories/signed.v +theories/charge.v +theories/radon_nikodym.v theories/altreals/xfinmap.v theories/altreals/discrete.v theories/altreals/realseq.v diff --git a/theories/charge.v b/theories/charge.v new file mode 100644 index 0000000000..142adf7d4c --- /dev/null +++ b/theories/charge.v @@ -0,0 +1,761 @@ +(* -*- company-coq-local-symbols: (("`&`" . ?∩) ("`|`" . ?∪) ("set0" . ?∅)); -*- *) +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +From mathcomp Require Import finmap fingroup perm rat. +Require Import boolp reals ereal classical_sets signed topology numfun. +Require Import mathcomp_extra functions normedtype. +From HB Require Import structures. +Require Import sequences esum measure fsbigop cardinality set_interval. +Require Import realfun. +Require Import lebesgue_measure lebesgue_integral. + +(******************************************************************************) +(* This file contains a formalization of charges and a proof of the Hahn *) +(* decomposition theorem. *) +(* *) +(* charge (a.k.a. signed measure): *) +(* isAdditiveCharge == mixin for additive charges *) +(* {additive_charge set T -> \bar R} == additive charge over T, a semiring *) +(* of sets *) +(* isCharge == mixin for charges *) +(* {charge set T -> \bar R} == charge over T, a semiring of sets *) +(* crestr D mu == restriction of the charge mu to the domain D *) +(* czero == zero charge *) +(* cscale == scaled charge *) +(* positive_set nu P == P is a positive set *) +(* negative_set nu N == N is a negative set *) +(* *) +(******************************************************************************) + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +(* NB: in the next releases of Coq, dependent_choice should be + generalized from Set to Type making the following lemma redundant *) +Section dependent_choice_Type. +Context X (R : X -> X -> Prop). + +Lemma dependent_choice_Type : (forall x, {y | R x y}) -> + forall x0, {f | f 0 = x0 /\ forall n, R (f n) (f n.+1)}. +Proof. +move=> h x0. +set (f := fix f n := if n is n'.+1 then proj1_sig (h (f n')) else x0). +exists f; split => //. +intro n; induction n; simpl; apply proj2_sig. +Qed. +End dependent_choice_Type. + +Local Open Scope ring_scope. +Local Open Scope classical_set_scope. +Local Open Scope ereal_scope. + +(* TODO: PR? *) +Lemma lt_trivIset T (F : nat -> set T) : + (forall n m, (m < n)%N -> F m `&` F n = set0) -> trivIset setT F. +Proof. +move=> h; apply/trivIsetP => m n _ _; rewrite neq_lt => /orP[|]; first exact: h. +by rewrite setIC; exact: h. +Qed. + +(* TODO: PR? *) +Lemma subsetC_trivIset T (F : nat -> set T) : + (forall n, F n.+1 `<=` ~` \big[setU/set0]_(i < n.+1) F i) -> trivIset setT F. +Proof. +move=> ACU; apply: lt_trivIset => n m mn; rewrite setIC; apply/disjoints_subset. +case: n mn => // n mn. +by apply: (subset_trans (ACU n)); exact/subsetC/bigsetU_sup. +Qed. + +(* TODO: PR? *) +Lemma fin_num_ltey (R : realDomainType) (x : \bar R) : x \is a fin_num -> x < +oo. +Proof. by move: x => [r| |]// _; rewrite ltey. Qed. + +(* TODO: PR? *) +Lemma gt0_fin_numE {R : realDomainType} [x : \bar R] : 0 < x -> (x \is a fin_num) = (x < +oo). +Proof. by move=> /ltW; exact: ge0_fin_numE. Qed. + +(* TODO: PR? *) +Lemma seqDUIE X (S : set X) (F : (set X)^nat) : + seqDU (fun n => S `&` F n) = (fun n => S `&` F n `\` \bigcup_(i < n) F i). +Proof. +apply/funext => n; rewrite -setIDA; apply/seteqP; split. + by rewrite /seqDU -setIDA bigcup_mkord -big_distrr/= setDIr setIUr setDIK set0U. +move=> x [Sx [Fnx UFx]]; split=> //; apply: contra_not UFx => /=. +by rewrite bigcup_mkord -big_distrr/= => -[]. +Qed. + +HB.mixin Record isAdditiveCharge d (T : semiRingOfSetsType d) (R : numFieldType) + (mu : set T -> \bar R) := { + charge_semi_additive : semi_additive mu }. + +#[short(type=additive_charge)] +HB.structure Definition AdditiveCharge d (T : semiRingOfSetsType d) + (R : numFieldType) := + { mu of isAdditiveCharge d T R mu & FinNumFun d mu }. + +Notation "{ 'additive_charge' 'set' T '->' '\bar' R }" := + (additive_charge T R) (at level 36, T, R at next level, + format "{ 'additive_charge' 'set' T '->' '\bar' R }") : ring_scope. + +#[export] Hint Resolve charge_semi_additive : core. + +HB.mixin Record isCharge d (T : semiRingOfSetsType d) (R : numFieldType) + (mu : set T -> \bar R) := { + charge_semi_sigma_additive : semi_sigma_additive mu }. + +#[short(type=charge)] +HB.structure Definition Charge d (T : algebraOfSetsType d) (R : realFieldType) := + { mu of isCharge d T R mu & AdditiveCharge d mu }. + +Notation "{ 'charge' 'set' T '->' '\bar' R }" := (charge T R) + (at level 36, T, R at next level, + format "{ 'charge' 'set' T '->' '\bar' R }") : ring_scope. + +Section charge_prop. +Context d (T : measurableType d) (R : realType). +Implicit Type mu : {charge set T -> \bar R}. + +Lemma charge0 mu : mu set0 = 0. +Proof. +have /[!big_ord0] ->// := @charge_semi_additive _ _ _ mu (fun=> set0) 0%N. +exact: trivIset_set0. +Qed. + +Hint Resolve charge0 : core. + +Lemma charge_semi_additiveW mu : mu set0 = 0 -> semi_additive mu -> semi_additive2 mu. +Proof. +move=> mu0 amx A B mA mB + AB; rewrite -bigcup2inE bigcup_mkord. +move=> /(amx (bigcup2 A B)) ->. +- by rewrite !(big_ord_recl, big_ord0)/= adde0. +- by move=> [|[|[]]]//=. +- move=> [|[|i]] [|[|j]]/= _ _ //. + + by rewrite AB => -[]. + + by rewrite setI0 => -[]. + + by rewrite setIC AB => -[]. + + by rewrite setI0 => -[]. + + by rewrite set0I => -[]. + + by rewrite set0I => -[]. + + by rewrite setI0 => -[]. +Qed. + +Lemma charge_semi_additive2E mu : semi_additive2 mu = additive2 mu. +Proof. +rewrite propeqE; split=> [amu A B ? ? ?|amu A B ? ? _ ?]; last by rewrite amu. +by rewrite amu //; exact: measurableU. +Qed. + +Lemma charge_semi_additive2 mu : semi_additive2 mu. +Proof. exact: charge_semi_additiveW. Qed. + +Hint Resolve charge_semi_additive2 : core. + +Lemma chargeU mu : additive2 mu. Proof. by rewrite -charge_semi_additive2E. Qed. + +Lemma chargeDI mu (A B : set T) : measurable A -> measurable B -> + mu A = mu (A `\` B) + mu (A `&` B). +Proof. +move=> mA mB; rewrite -charge_semi_additive2. +- by rewrite -setDDr setDv setD0. +- exact: measurableD. +- exact: measurableI. +- by apply: measurableU; [exact: measurableD |exact: measurableI]. +- by rewrite setDE setIACA setICl setI0. +Qed. + +Lemma chargeD mu (A B : set T) : measurable A -> measurable B -> + mu (A `\` B) = mu A - mu (A `&` B). +Proof. +move=> mA mB. +rewrite (chargeDI mu mA mB) addeK// fin_numE 1?gt_eqF 1?lt_eqF//. +- by rewrite ltey_eq fin_num_measure//; exact:measurableI. +- by rewrite ltNye_eq fin_num_measure//; exact:measurableI. +Qed. + +Lemma charge_partition mu S P N : + measurable S -> measurable P -> measurable N -> + P `|` N = setT -> P `&` N = set0 -> + mu S = mu (S `&` P) + mu (S `&` N). +Proof. +move=> mS mP mN PNT PN0; rewrite -{1}(setIT S) -PNT setIUr chargeU//. +- exact: measurableI. +- exact: measurableI. +- by rewrite setICA -(setIA S P N) PN0 setIA setI0. +Qed. + +End charge_prop. +#[export] Hint Resolve charge0 : core. +#[export] Hint Resolve charge_semi_additive2 : core. + +Definition crestr d (T : measurableType d) (R : realFieldType) (D : set T) + (f : set T -> \bar R) (mD : measurable D) := fun X => f (X `&` D). + +Section charge_restriction. +Context d (T : measurableType d) (R : realFieldType). +Variables (mu : {charge set T -> \bar R}) (D : set T) (mD : measurable D). + +Local Notation restr := (crestr mu mD). + +Let crestr_finite_measure_function U : measurable U -> restr U \is a fin_num. +Proof. +move=> mU. +by have /(@fin_num_measure _ _ _ mu) : measurable (U `&` D) by exact: measurableI. +Qed. + +HB.instance Definition _ := SigmaFinite_isFinite.Build _ _ _ + restr crestr_finite_measure_function. + +Let crestr_semi_additive : semi_additive restr. +Proof. +move=> F n mF tF mU; pose FD i := F i `&` D. +have mFD i : measurable (FD i) by exact: measurableI. +have tFD : trivIset setT FD. + apply/trivIsetP => i j _ _ ij. + move/trivIsetP : tF => /(_ i j Logic.I Logic.I ij). + by rewrite /FD setIACA => ->; rewrite set0I. +rewrite -(charge_semi_additive _ _ mFD)//; last exact: bigsetU_measurable. +by rewrite /crestr /FD big_distrl. +Qed. + +HB.instance Definition _ := + isAdditiveCharge.Build _ _ _ restr crestr_semi_additive. + +Let crestr_semi_sigma_additive : semi_sigma_additive restr. +Proof. +move=> F mF tF mU; pose FD i := F i `&` D. +have mFD i : measurable (FD i) by exact: measurableI. +have tFD : trivIset setT FD. + apply/trivIsetP => i j _ _ ij. + move/trivIsetP : tF => /(_ i j Logic.I Logic.I ij). + by rewrite /FD setIACA => ->; rewrite set0I. +rewrite /restr setI_bigcupl; apply: charge_semi_sigma_additive => //. +by apply: bigcup_measurable => k _; exact: measurableI. +Qed. + +HB.instance Definition _ := + isCharge.Build _ _ _ restr crestr_semi_sigma_additive. + +End charge_restriction. + +Section charge_zero. +Context d (T : measurableType d) (R : realFieldType). +Local Open Scope ereal_scope. + +Definition czero (A : set T) : \bar R := 0. + +Let czero0 : czero set0 = 0. Proof. by []. Qed. + +Let czero_finite_measure_function B : measurable B -> czero B \is a fin_num. +Proof. by []. Qed. + +HB.instance Definition _ := SigmaFinite_isFinite.Build _ _ _ + czero czero_finite_measure_function. + +Let czero_semi_additive : semi_additive czero. +Proof. by move=> F n mF tF mUF; rewrite /czero big1. Qed. + +HB.instance Definition _ := + isAdditiveCharge.Build _ _ _ czero czero_semi_additive. + +Let czero_sigma_additive : semi_sigma_additive czero. +Proof. +move=> F mF tF mUF; rewrite [X in X --> _](_ : _ = cst 0); first exact: cvg_cst. +by apply/funext => n; rewrite big1. +Qed. + +HB.instance Definition _ := isCharge.Build _ _ _ czero czero_sigma_additive. + +End charge_zero. +Arguments czero {d T R}. + +Section charge_scale. +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType). (* R : realFieldType? *) +Variables (r : R) (m : {charge set T -> \bar R}). + +Definition cscale (A : set T) : \bar R := r%:E * m A. + +Let cscale0 : cscale set0 = 0. Proof. by rewrite /cscale charge0 mule0. Qed. + +Let cscale_finite_measure_function U : measurable U -> cscale U \is a fin_num. +Proof. by move=> mU; apply: fin_numM => //; exact: fin_num_measure. Qed. + +HB.instance Definition _ := SigmaFinite_isFinite.Build _ _ _ + cscale cscale_finite_measure_function. + +Let cscale_semi_additive : semi_additive cscale. +Proof. +move=> F n mF tF mU; rewrite /cscale charge_semi_additive//. +rewrite fin_num_sume_distrr// => i j _ _. +by rewrite fin_num_adde_defl// fin_num_measure. +Qed. + +HB.instance Definition _ := + isAdditiveCharge.Build _ _ _ cscale cscale_semi_additive. + +Let cscale_sigma_additive : semi_sigma_additive cscale. +Proof. +move=> F mF tF mUF; rewrite /cscale; rewrite [X in X --> _](_ : _ = + (fun n => r%:E * \sum_(0 <= i < n) m (F i))); last first. + apply/funext => k; rewrite fin_num_sume_distrr// => i j _ _. + by rewrite fin_num_adde_defl// fin_num_measure. +rewrite /mscale; have [->|r0] := eqVneq r 0%R. + rewrite mul0e [X in X --> _](_ : _ = (fun=> 0)); first exact: cvg_cst. + by under eq_fun do rewrite mul0e. +by apply: cvgeMl => //; apply: charge_semi_sigma_additive. +Qed. + +HB.instance Definition _ := isCharge.Build _ _ _ cscale + cscale_sigma_additive. + +End charge_scale. + +Section positive_negative_set. +Context d (R : realType) (T : measurableType d). +Implicit Types nu : set T -> \bar R. + +Definition positive_set nu (P : set T) := + measurable P /\ forall E, measurable E -> E `<=` P -> nu E >= 0. + +Definition negative_set nu (N : set T) := + measurable N /\ forall E, measurable E -> E `<=` N -> nu E <= 0. + +End positive_negative_set. + +Section positive_negative_set_prop. +Context d (T : measurableType d) (R : realType). +Implicit Types nu : {charge set T -> \bar R}. + +Lemma negative_set_charge_le0 nu N : negative_set nu N -> nu N <= 0. +Proof. by move=> [mN]; exact. Qed. + +Lemma negative_set0 nu : negative_set nu set0. +Proof. by split => // E _; rewrite subset0 => ->; rewrite charge0. Qed. + +Lemma bigcup_negative_set nu (F : (set T)^nat) : + (forall i, negative_set nu (F i)) -> + negative_set nu (\bigcup_i F i). +Proof. +move=> hF; have mUF : measurable (\bigcup_k F k). + by apply: bigcup_measurable => n _; have [] := hF n. +split=> [//|S mS SUF]. +pose SF n := (S `&` F n) `\` \bigcup_(k < n) F k. +have SSF : S = \bigcup_i SF i. + transitivity (\bigcup_k seqDU (fun n => S `&` F n) k); last first. + by apply: eq_bigcup => // n _; rewrite seqDUIE. + by rewrite -seqDU_bigcup_eq -setI_bigcupr setIidl. +have mSF n : measurable (SF n). + apply: measurableD; first by apply: measurableI => //; have [] := hF n. + by apply: bigcup_measurable => // k _; have [] := hF k. +have SFS : (fun n => \sum_(0 <= i < n) nu (SF i)) --> nu S. + by rewrite SSF; apply: charge_semi_sigma_additive => //; + [by rewrite /SF -seqDUIE; exact: trivIset_seqDU|exact: bigcup_measurable]. +have nuS_ n : nu (SF n) <= 0 by have [_] := hF n; apply => // x -[[]]. +move/cvg_lim : (SFS) => <-//; apply: lime_le. + by apply/cvg_ex => /=; first eexists; exact: SFS. +by apply: nearW => n; exact: sume_le0. +Qed. + +Lemma negative_setU nu N M : + negative_set nu N -> negative_set nu M -> negative_set nu (N `|` M). +Proof. +move=> nN nM; rewrite -bigcup2E; apply: bigcup_negative_set => -[//|[//|/= _]]. +exact: negative_set0. +Qed. + +Lemma positive_negative0 nu P N : positive_set nu P -> negative_set nu N -> + forall S, measurable S -> nu (S `&` P `&` N) = 0. +Proof. +move=> [mP posP] [mN negN] S mS; apply/eqP; rewrite eq_le; apply/andP; split. + apply negN; first by apply measurableI => //; exact: measurableI. + by apply setIidPl; rewrite -setIA setIid. +rewrite -setIAC. +apply posP; first by apply measurableI => //; exact: measurableI. +by apply setIidPl; rewrite -setIA setIid. +Qed. + +End positive_negative_set_prop. + +Section hahn_decomp_lemma. +Context d (T : measurableType d) (R : realType). +Variable nu : {charge set T -> \bar R}. + +Variable D : set T. + +Let elt_prop (x : set T * \bar R) := [/\ measurable x.1, + 0 <= x.2, + x.1 `<=` D & + nu x.1 >= mine (x.2 * 2^-1%:E) 1]. + +Let elt_type := {x : set T * \bar R * set T | elt_prop x.1}. + +Let A_ (x : elt_type) := (proj1_sig x).1.1. +Let d_ (x : elt_type) := (proj1_sig x).1.2. +Let U_ (x : elt_type) := (proj1_sig x).2. + +Let elt_mA x : measurable (A_ x). +Proof. by move: x => [[[? ?] ?]] []. Qed. + +Let elt_A_ge0 x : 0 <= nu (A_ x). +Proof. +move: x => [[[? ?] ?]] [/= mA d_ge0 Ad]; apply: le_trans. +by rewrite /mine; case: ifPn => // _; rewrite mule_ge0. +Qed. + +Let elt_d_ge0 x : 0 <= d_ x. +Proof. by move: x => [[[? ?] ?]] []. Qed. + +Let elt_mine x : nu (A_ x) >= mine (d_ x * 2^-1%:E) 1. +Proof. by move: x => [[[? ?] ?]] []. Qed. + +Let elt_D x : A_ x `<=` D. +Proof. by move: x => [[[? ?] ?]] []. Qed. + +Let set_mE A := + [set mE | exists E, [/\ mE = nu E, measurable E & E `<=` D `\` A] ]. + +Let dd A := ereal_sup (set_mE A). + +Let seq_sup i j := [/\ d_ j = dd (U_ i), + A_ j `<=` D `\` U_ i & U_ j = U_ i `|` A_ j ]. + +Let next_elt A : 0 <= dd A -> { B | [/\ measurable B, + nu B >= 0, B `<=` D `\` A & nu B >= mine (dd A * 2^-1%:E) 1] }. +Proof. +move=> d_ge0; pose m := mine (dd A * 2^-1%R%:E) 1%E; apply/cid. +move: d_ge0; rewrite le_eqVlt => /predU1P[<-|d_gt0]. + by exists set0; split => //; rewrite charge0. +have m_gt0 : 0 < m by rewrite /m lt_minr lte01 andbT mule_gt0. +have : m < dd A. + rewrite /m; have [->|dn1oo] := eqVneq (dd A) +oo. + by rewrite min_r// ?ltey// gt0_mulye// leey. + rewrite -(@fineK _ (dd A)); last first. + by rewrite ge0_fin_numE// ?(ltW d_gt0)// lt_neqAle dn1oo leey. + rewrite -EFinM minEFin lte_fin lt_minl; apply/orP; left. + rewrite ltr_pdivr_mulr// ltr_pmulr// ?ltr1n// fine_gt0// d_gt0/=. + by rewrite lt_neqAle dn1oo/= leey. +move=> /ereal_sup_gt/cid2[x/= /cid[B [-> mB BDA mmuB]]]. +exists B; split => //. +by rewrite ltW// (lt_trans _ mmuB)//. +by rewrite (le_trans _ (ltW mmuB)). +Qed. + +Lemma hahn_decomp_lemma : measurable D -> nu D <= 0 -> + {A | [/\ A `<=` D, measurable A, negative_set nu A & nu A <= nu D]}. +Proof. +move=> mD nuD_ge0. +have d0_ge0 : 0 <= dd set0. + by apply: ereal_sup_ub => /=; exists set0; split => //; rewrite charge0. +have [A0 [mA0 nuA0 + A0d0]] := next_elt d0_ge0. +rewrite setD0 => A0D. +have [v [v0 Pv]] : {v : nat -> elt_type | + v 0%N = exist _ (A0, dd set0, A0) (And4 mA0 d0_ge0 A0D A0d0) /\ + forall n, seq_sup (v n) (v n.+1)}. + apply dependent_choice_Type => -[[[A' ?] U] [/= mA' mA'0]]. + have d1_ge0 : 0 <= dd U. + by apply: ereal_sup_ub => /=; exists set0; split => //; rewrite charge0. + have [A1 [mA1 muA10 A1DU A1d1] ] := next_elt d1_ge0. + have A1D : A1 `<=` D by apply: (subset_trans A1DU); apply: subDsetl. + by exists (exist _ (A1, dd U, U `|` A1) (And4 mA1 d1_ge0 A1D A1d1)). +set Aoo := \bigcup_k A_ (v k). +have mA_ k : d.-measurable (A_ (v k)) by exact: elt_mA. +have mAoo : measurable Aoo by exact: bigcup_measurable. +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. +exists (D `\` Aoo). +have cvg_nuA : (fun n => \sum_(0 <= i < n) nu (A_ (v i))) --> nu Aoo. + exact: charge_semi_sigma_additive. +have nuAoo : 0 <= nu Aoo. + move/cvg_lim : cvg_nuA => <-//=; apply: nneseries_ge0 => n _. + exact: elt_A_ge0. +have A_cvg_0 : (fun n => nu (A_ (v n))) --> 0. + rewrite [X in X --> _](_ : _ = EFin \o (fun n => fine (nu (A_ (v n))))); last first. + by apply/funext => n/=; rewrite fineK// fin_num_measure. + apply: continuous_cvg => //. + apply/(@cvg_series_cvg_0 _ [normedModType R of R^o]). + move: cvg_nuA. + rewrite -(@fineK _ (nu Aoo)) ?fin_num_measure//. + move/fine_cvgP => [_ ?]. + 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. + by apply/cvg_ex; exists (fine (nu Aoo)). +have mine_cvg_0 : (fun n => mine (d_ (v n) * 2^-1%:E) 1) --> 0. + apply: (@squeeze_cvge _ _ _ _ (cst 0) _ (fun n => nu (A_ (v n)))); + [|exact: cvg_cst|by []]. + apply: nearW => n /=. + by rewrite elt_mine andbT le_minr lee01 andbT mule_ge0. +have d_cvg_0 : d_ \o v --> 0. + move/fine_cvgP : A_cvg_0 => -[_]. + move=> /(@cvgrPdist_lt _ [normedModType R of R^o])/(_ _ ltr01)[N _ hN]. + have d_v_fin_num : \forall x \near \oo, d_ (v x) \is a fin_num. + near=> n. + have /hN : (N <= n)%N by near: n; exists N. + rewrite sub0r normrN /= ger0_norm ?fine_ge0//. + have := elt_mine (v n). + rewrite /mine; case: ifPn => [+ _ _|]. + rewrite lte_pdivr_mulr// mul1e => d2. + by rewrite ge0_fin_numE// (lt_le_trans d2)// leey. + move=> _ /[swap]; rewrite ltNge => -/[swap]. + by move/fine_le => -> //; rewrite fin_num_measure. + apply/fine_cvgP; split => //. + apply/(@cvgrPdist_lt _ [normedModType R of R^o]) => e e0. + move/fine_cvgP : mine_cvg_0 => -[_]. + move/(@cvgrPdist_lt _ [normedModType R of R^o]). + have : (0 < minr (e / 2) 1)%R by rewrite lt_minr// ltr01 andbT divr_gt0. + move=> /[swap] /[apply] -[M _ hM]. + near=> n. + rewrite sub0r normrN. + have /hM : (M <= n)%N by near: n; exists M. + rewrite sub0r normrN /mine/=; case: ifPn => [_|]. + rewrite fineM//=; last by near: n; exact: d_v_fin_num. + rewrite normrM (@gtr0_norm _ 2^-1%R); last by rewrite invr_gt0. + rewrite ltr_pdivr_mulr// => /lt_le_trans; apply. + rewrite /minr; case: ifPn. + by rewrite -mulrA mulVr// ?mulr1// unitfE. + by rewrite -leNgt -ler_pdivl_mulr. + rewrite -leNgt /minr; case: ifPn. + by rewrite ger0_norm//= => /ltW e21 _; rewrite ltNge e21. + by rewrite ger0_norm//= ltxx. +have nuDAoo : nu D >= nu (D `\` Aoo). + rewrite -[in leRHS](@setDUK _ Aoo D); last first. + by apply: bigcup_sub => i _; exact: elt_D. + by rewrite chargeU// ?lee_addr// ?setDIK//; exact: measurableD. +split; [by []|exact: measurableD| | by []]. +split; first exact: measurableD. +move=> E mE EDAoo. +pose H n := set_mE (\big[setU/set0]_(i < n) A_ (v i)). +have EH n : [set nu E] `<=` H n. + have : nu E \in set_mE Aoo by rewrite inE; exists E. + rewrite -sub1set => /subset_trans; apply. + move=> x/= [F [? ? FB]]. + exists F; split => //. + by apply: (subset_trans FB); apply: setDS; exact: bigsetU_bigcup. +have nudelta n : nu E <= d_ (v n). + move: n => [|n]. + rewrite v0/=. + apply: ereal_sup_ub => /=; exists E; split => //. + by apply: (subset_trans EDAoo); exact: setDS. + suff : nu E <= dd (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' [? ? A'D]]. + exists A'; split => //. + by apply: (subset_trans A'D); apply: setDS; rewrite Ubig. +apply: (@closed_cvg _ _ _ _ _ (fun v => nu E <= v) _ _ _ d_cvg_0) => //. + exact: closed_ereal_le_ereal. +exact: nearW. +Unshelve. all: by end_near. Qed. + +End hahn_decomp_lemma. + +Definition hahn_decomp d (T : measurableType d) (R : realType) + (nu : {charge set T -> \bar R}) P N := + [/\ positive_set nu P, negative_set nu N, P `|` N = setT & P `&` N = set0]. + +Section hahn_decomposition_theorem. +Context d (T : measurableType d) (R : realType). +Variable nu : {charge set T -> \bar R}. + +Let elt_prop (x : set T * \bar R) := [/\ x.2 <= 0, + negative_set nu x.1 & + nu x.1 <= maxe (x.2 * 2^-1%:E) (- 1%E) ]. + +Let elt_type := {AsU : set T * \bar R * set T | elt_prop AsU.1}. + +Let A_ (x : elt_type) := (proj1_sig x).1.1. +Let s_ (x : elt_type) := (proj1_sig x).1.2. +Let U_ (x : elt_type) := (proj1_sig x).2. + +Let elt_mA x : measurable (A_ x). +Proof. by move: x => [[[? ?] ?] [/= ? []]]. Qed. + +Let elt_nuA x : nu (A_ x) <= 0. +Proof. +by move: x => [[[? ?] ?]] [/= ? h ?]; exact: negative_set_charge_le0. +Qed. + +Let elt_s x : s_ x <= 0. +Proof. by move: x => [[[? ?] ?]] -[]. Qed. + +Let elt_neg_set x : negative_set nu (A_ x). +Proof. by move: x => [[[? ?] ?]] -[]. Qed. + +Let elt_maxe x : nu (A_ x) <= maxe (s_ x * 2^-1%:E) (- ( 1)). +Proof. by move: x => [[[? ?] ?]] -[]. Qed. + +Let set_mE A := + [set mE | exists E, [/\ mE = nu E, measurable E & E `<=` setT `\` A] ]. + +Let ss A := ereal_inf (set_mE A). + +Let seq_inf i j := [/\ s_ j = ss (U_ i), + A_ j `<=` setT `\` U_ i & + U_ j = U_ i `|` A_ j]. + +Let next_elt U : ss U <= 0 -> { A | [/\ A `<=` setT `\` U, + negative_set nu A & + nu A <= maxe (ss U * 2^-1%R%:E) (- 1%E)] }. +Proof. +move=> s_le0; pose m := maxe (ss U * 2^-1%R%:E) (- 1%E); apply/cid. +move: s_le0; rewrite le_eqVlt => /predU1P[->|s_lt0]. + by exists set0; split => //; rewrite ?charge0//; exact: negative_set0. +have m0_lt0 : m < 0 by rewrite /m lt_maxl lteN10 andbT nmule_rlt0. +have : ss U < m. + rewrite /m; have [->|s0oo] := eqVneq (ss U) -oo. + by rewrite max_r ?ltNye// gt0_mulNye// leNye. + rewrite -(@fineK _ (ss U)); last first. + by rewrite le0_fin_numE// ?(ltW s_lt0)// lt_neqAle leNye eq_sym s0oo. + rewrite -EFinM maxEFin lte_fin lt_maxr; apply/orP; left. + rewrite ltr_pdivl_mulr// gtr_nmulr ?ltr1n// fine_lt0// s_lt0/=. + by rewrite lt_neqAle s0oo/= leNye. +move=> /ereal_inf_lt/cid2[_/= /cid[B [-> mB BU nuBm]]]. +have nuB_le0 : nu B <= 0. + by rewrite (le_trans (ltW nuBm))// ltW. +have [C [CB mN1 neg_set_C nuCnuB]] := hahn_decomp_lemma mB nuB_le0. +exists C; split => //. +- exact: (subset_trans CB). +- by rewrite (le_trans nuCnuB)// (le_trans (ltW nuBm)). +Qed. + +Theorem Hahn_decomposition : exists P N, hahn_decomp nu P N. +Proof. +have ss0 : ss set0 <= 0. + by apply: ereal_inf_lb => /=; exists set0; split => //; rewrite charge0. +have [A0 [_ negA0 A0s0]] := next_elt ss0. +have [v [v0 Pv]] : {v | + v 0%N = exist _ (A0, ss set0, A0) (And3 ss0 negA0 A0s0) /\ + forall n, seq_inf (v n) (v n.+1)}. + apply: dependent_choice_Type => -[[[A s] U] [/= s_le0 negA]]. + pose s' := ss U. + have s'_le0 : s' <= 0. + by apply: ereal_inf_lb => /=; exists set0; split => //; rewrite charge0. + have [A' [? negA' A's'] ] := next_elt s'_le0. + by exists (exist _ (A', s', U `|` A') (And3 s'_le0 negA' A's')). +set N := \bigcup_k (A_ (v k)). +have mN : measurable N by exact: bigcup_measurable. +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. + rewrite -setTD; apply: setDSS => //. + by rewrite Ubig big_ord_recr. +have neg_set_N : negative_set nu N. + by apply: bigcup_negative_set => i; exact: elt_neg_set. +pose P := setT `\` N. +have mP : measurable P by exact: measurableD. +exists P, N; split; first last. + by rewrite /P setTD setICl. + by rewrite /P setTD setvU. + exact: neg_set_N. +split=> // D mD DP; rewrite leNgt; apply/negP => nuD0. +have snuD n : s_ (v n) <= nu D. + move: n => [|n]. + by rewrite v0 /=; apply: ereal_inf_lb => /=; exists D; rewrite setD0. + have [-> _ _] := Pv n. + apply: ereal_inf_lb => /=; exists D; split => //. + by apply: (subset_trans DP); apply: setDS; rewrite Ubig; exact: bigsetU_bigcup. +have max_le0 n : maxe (s_ (v n) * 2^-1%:E) (- (1)) <= 0. + rewrite /maxe; case: ifPn => // _. + by rewrite pmule_lle0// (le_trans (snuD _))// ltW. +have not_s_cvg_0 : ~ s_ \o v --> 0. + move/fine_cvgP => -[sfin]. + move/(@cvgrPdist_lt _ [normedModType R of R^o]). + 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//; last by rewrite fine_le0. + rewrite ltr0_norm//; last by rewrite fine_lt0// nuD0 andbT ltNye_eq fin_num_measure. + rewrite ltr_opp2; apply/negP; rewrite -leNgt; apply: fine_le. + - near: n; exact. + - by rewrite fin_num_measure. + - exact: snuD. +have nuN : nu N = \sum_(n //. + apply: charge_semi_sigma_additive; [by []|exact: tA|]. + exact: bigcup_measurable. +have sum_A_maxe : \sum_(n \sum_(0 <= k < n) maxe (s_ (v k) * 2^-1%:E) (- (1))). + 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. + rewrite leeNy_eq => /eqP nuNoo. + have := @fin_num_measure _ _ _ nu N mN. + by rewrite fin_numE => /andP[+ _] => /eqP; apply. + - move/cvg_lim => limoo. + have := @npeseries_le0 _ (fun n => maxe (s_ (v n) * 2^-1%:E) (- (1))) xpredT. + rewrite limoo// leNgt. + by move=> /(_ (fun n _ => max_le0 n))/negP; apply. +move/fine_cvgP => [Hfin cvgl]. +have : cvg (series (fun n => fine (maxe (s_ (v n) * 2^-1%:E) (- (1))))). + apply/cvg_ex; exists l. + move: cvgl. + rewrite (_ : _ \o _ = (fun n => + \sum_(0 <= k < n) fine (maxe (s_ (v k) * 2^-1%:E)%E (- (1))%E))%R) //. + apply/funext => n/=; rewrite sum_fine// => m _. + rewrite le0_fin_numE. + by rewrite (lt_le_trans _ (elt_maxe _))// -le0_fin_numE// ?fin_num_measure. + by rewrite /maxe; case: ifPn => // _; rewrite mule_le0_ge0. +move/(@cvg_series_cvg_0 _ [normedModType R of R^o]) => maxe_cvg_0. +apply: not_s_cvg_0. +rewrite (_ : _ \o _ = (fun n => s_ (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 => maxe_lt1; rewrite fin_numE; apply/andP; split. + apply/negP => /eqP h. + by rewrite h max_r// ?leNye//= normrN normr1 ltxx in maxe_lt1. + by rewrite lt_eqF// (@le_lt_trans _ _ 0)// mule_le0_ge0. +apply/(@cvgrPdist_lt _ [normedModType R of R^o]) => e e0. +have : (0 < minr e 1)%R by rewrite lt_minr// e0 ltr01. +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 => [_|]. + rewrite normrN normr1 /minr. + by case: ifPn; rewrite ?ltxx// ltNge => /[swap] /ltW ->. +rewrite -leNgt => ? /lt_le_trans; apply. +by rewrite /minr; case: ifPn => //; rewrite -leNgt. +Unshelve. all: by end_near. Qed. + +Lemma Hahn_decomposition_uniq P1 N1 P2 N2 : + hahn_decomp nu P1 N1 -> hahn_decomp nu P2 N2 -> + forall S, measurable S -> + nu (S `&` P1) = nu (S `&` P2) /\ nu (S `&` N1) = nu (S `&` N2). +Proof. +move=> [posP1 negN1 PN1T PN10] [posP2 negN2 PN2T PN20] S mS. +move: (posP1) (negN1) (posP2) (negN2) => [mP1 _] [mN1 _] [mP2 _] [mN2 _]. +split. + transitivity (nu (S `&` P1 `&` P2)). + rewrite (charge_partition _ _ mP2 mN2)//; last exact: measurableI. + by rewrite (positive_negative0 posP1 negN2 mS) adde0. + rewrite [RHS](charge_partition _ _ mP1 mN1)//; last exact: measurableI. + by rewrite (positive_negative0 posP2 negN1 mS) adde0 setIAC. +transitivity (nu (S `&` N1 `&` N2)). + rewrite (charge_partition nu _ mP2 mN2)//; last exact: measurableI. + have := positive_negative0 posP2 negN1 mS. + by rewrite setIAC => ->; rewrite add0e. +rewrite [RHS](charge_partition nu _ mP1 mN1)//; last exact: measurableI. +by rewrite (setIAC _ _ P1) (positive_negative0 posP1 negN2 mS) add0e setIAC. +Qed. + +End hahn_decomposition_theorem. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 1e123ee155..44f1fd8659 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -331,7 +331,7 @@ apply/andP; split=> //; apply: contraTneq xbj => ->. by rewrite in_itv/= le_gtF// (itvP xabi). Qed. -HB.instance Definition _ := isContent.Build _ R _ +HB.instance Definition _ := isContent.Build _ _ R (hlength : set ocitv_type -> _) (@hlength_ge0') hlength_semi_additive. Hint Extern 0 ((_ .-ocitv).-measurable _) => solve [apply: is_ocitv] : core. diff --git a/theories/measure.v b/theories/measure.v index 4ea7535333..10c0113d99 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -87,12 +87,6 @@ From HB Require Import structures. (* that it is semi_sigma_additive *) (* isMeasure == factory corresponding to the type of measures *) (* Measure == structure corresponding to measures *) -(* finite_measure mu == the measure mu is finite *) -(* {sigma_finite_content set T -> \bar R} == contents that are also sigma *) -(* finite *) -(* {sigma_finite_measure set T -> \bar R} == *) -(* measures that are also sigma finite *) -(* isSigmaFinite == factory corresponding to sigma finiteness *) (* *) (* pushforward mf m == pushforward/image measure of m by f, where mf is a *) (* proof that f is measurable *) @@ -110,8 +104,39 @@ From HB Require Import structures. (* proof that D is measurable *) (* counting T R == counting measure *) (* *) -(* sigma_finite A f == the measure f is sigma-finite on A : set T with *) -(* T : ringOfSetsType. *) +(* * Hierarchy of s-finite, sigma-finite, finite measures: *) +(* sfinite_measure_def == predicate for s-finite measure functions *) +(* Measure_isSFinite_subdef == mixin for s-finite measures *) +(* SFiniteMeasure == structure of s-finite measures *) +(* {sfinite_measure set T -> \bar R} == type of s-finite measures *) +(* Measure_isSFinite == factory for s-finite measures *) +(* *) +(* sigma_finite A f == the measure function f is sigma-finite on *) +(* A : set T with T : semiRingOfSetsType *) +(* isSigmaFinite == mixin corresponding to sigma finiteness *) +(* {sigma_finite_content set T -> \bar R} == contents that are also sigma *) +(* finite *) +(* {sigma_finite_measure set T -> \bar R} == measures that are also sigma *) +(* finite *) +(* *) +(* fin_num_fun == predicate for finite function over measurable sets *) +(* finite_measure == predicate for finite measure function *) +(* SigmaFinite_isFinite == mixin for finite measures *) +(* FiniteMeasure == structure of finite measures *) +(* Measure_isFinite == factory for finite measures *) +(* *) +(* FiniteMeasure_isSubProbability = mixin corresponding to subprobability *) +(* SubProbability = structure of subprobability *) +(* subprobability T R == subprobability measure over the measurableType T *) +(* with value in R : realType *) +(* Measure_isSubProbability == factory for subprobability measures *) +(* *) +(* isProbability == mixin corresponding to probability measures *) +(* Probability == structure of probability measures *) +(* probability T R == probability measure over the measurableType T with *) +(* value in R : realType *) +(* Measure_isProbability == factor for probability measures *) +(* *) (* mu.-negligible A == A is mu negligible *) (* {ae mu, forall x, P x} == P holds almost everywhere for the measure mu *) (* *) @@ -156,8 +181,6 @@ From HB Require Import structures. (* generated from T1 x T2, with T1 and T2 *) (* measurableType's with resp. display d1 and d2 *) (* *) -(* probability T R == probability measure over the measurableType T with *) -(* value in R : realType *) (******************************************************************************) Set Implicit Arguments. @@ -1238,10 +1261,6 @@ Definition sigma_sub_additive := forall (A : set T) (F : nat -> set T), A `<=` \bigcup_n F n -> mu A <= \sum_(n \bar R) := - exists2 F : (set T)^nat, A = \bigcup_(i : nat) F i & - forall i, measurable (F i) /\ mu (F i) < +oo. - Lemma semi_additiveW : mu set0 = 0 -> semi_additive -> semi_additive2. Proof. move=> mu0 amx A B mA mB + AB; rewrite -bigcup2inE bigcup_mkord. @@ -1282,7 +1301,7 @@ End ring_additivity. Lemma semi_sigma_additive_is_additive d (R : realFieldType (*TODO: numFieldType if possible?*)) - (X : semiRingOfSetsType d) (mu : set X -> \bar R) : + (T : semiRingOfSetsType d) (mu : set T -> \bar R) : mu set0 = 0 -> semi_sigma_additive mu -> semi_additive mu. Proof. move=> mu0 samu A n Am Atriv UAm. @@ -1303,7 +1322,7 @@ by rewrite [X in _ + X]big1 ?adde0// => ?; rewrite -ltn_subRL subnn. Unshelve. all: by end_near. Qed. Lemma semi_sigma_additiveE - (R : numFieldType) d (X : measurableType d) (mu : set X -> \bar R) : + (R : numFieldType) d (T : measurableType d) (mu : set T -> \bar R) : semi_sigma_additive mu = sigma_additive mu. Proof. rewrite propeqE; split=> [amu A mA tA|amu A mA tA mbigcupA]; last exact: amu. @@ -1311,7 +1330,7 @@ by apply: amu => //; exact: bigcupT_measurable. Qed. Lemma sigma_additive_is_additive - (R : realFieldType) d (X : measurableType d) (mu : set X -> \bar R) : + (R : realFieldType) d (T : measurableType d) (mu : set T -> \bar R) : mu set0 = 0 -> sigma_additive mu -> additive mu. Proof. move=> mu0; rewrite -semi_sigma_additiveE -semi_additiveE. @@ -1319,23 +1338,23 @@ exact: semi_sigma_additive_is_additive. Qed. HB.mixin Record isContent d - (R : numFieldType) (T : semiRingOfSetsType d) (mu : set T -> \bar R) := { + (T : semiRingOfSetsType d) (R : numFieldType) (mu : set T -> \bar R) := { measure_ge0 : forall x, 0 <= mu x ; measure_semi_additive : semi_additive mu }. HB.structure Definition Content d - (R : numFieldType) (T : semiRingOfSetsType d) := { - mu & isContent d R T mu }. + (T : semiRingOfSetsType d) (R : numFieldType) := { + mu & isContent d T R mu }. Notation content := Content.type. Notation "{ 'content' 'set' T '->' '\bar' R }" := - (content R T) (at level 36, T, R at next level, + (content T R) (at level 36, T, R at next level, format "{ 'content' 'set' T '->' '\bar' R }") : ring_scope. -Arguments measure_ge0 {d R T} _. +Arguments measure_ge0 {d T R} _. Section content_signed. -Context d (R : numFieldType) (T : semiRingOfSetsType d). +Context d (T : semiRingOfSetsType d) (R : numFieldType). Variable mu : {content set T -> \bar R}. @@ -1347,7 +1366,7 @@ Canonical content_snum S := Signed.mk (content_snum_subproof S). End content_signed. Section content_on_semiring_of_sets. -Context d (R : numFieldType) (T : semiRingOfSetsType d) +Context d (T : semiRingOfSetsType d) (R : numFieldType) (mu : {content set T -> \bar R}). Lemma measure0 : mu set0 = 0. @@ -1412,7 +1431,7 @@ Proof. exact/semi_additiveW. Qed. Hint Resolve measure_semi_additive2 : core. End content_on_semiring_of_sets. -Arguments measure0 {d R T} _. +Arguments measure0 {d T R} _. #[global] Hint Extern 0 (is_true (0 <= (_ : {content set _ -> \bar _}) _)%E) => @@ -1471,17 +1490,16 @@ End content_on_ring_of_sets. #[global] Hint Resolve measureU measure_bigsetU : core. -HB.mixin Record isMeasure0 d - (R : numFieldType) (T : semiRingOfSetsType d) - mu of isContent d R T mu := { +HB.mixin Record isMeasure0 d (T : semiRingOfSetsType d) (R : numFieldType) + mu of isContent d T R mu := { measure_semi_sigma_additive : semi_sigma_additive mu }. #[short(type=measure)] -HB.structure Definition Measure d - (R : numFieldType) (T : semiRingOfSetsType d) := - {mu of isMeasure0 d R T mu & Content d mu}. +HB.structure Definition Measure d (T : semiRingOfSetsType d) + (R : numFieldType) := + {mu of isMeasure0 d T R mu & Content d mu}. -Notation "{ 'measure' 'set' T '->' '\bar' R }" := (measure R T) +Notation "{ 'measure' 'set' T '->' '\bar' R }" := (measure T R) (at level 36, T, R at next level, format "{ 'measure' 'set' T '->' '\bar' R }") : ring_scope. @@ -1513,9 +1531,9 @@ apply: semi_sigma_additive_is_additive. - exact: measure_semi_sigma_additive. Qed. -HB.instance Definition _ := isContent.Build d R T mu +HB.instance Definition _ := isContent.Build d T R mu measure_ge0 semi_additive_mu. -HB.instance Definition _ := isMeasure0.Build d R T mu measure_semi_sigma_additive. +HB.instance Definition _ := isMeasure0.Build d T R mu measure_semi_sigma_additive. HB.end. Lemma eq_measure d (T : measurableType d) (R : realType) @@ -1567,47 +1585,6 @@ Arguments measure_bigcup {d R T} _ _. #[global] Hint Extern 0 (sigma_additive _) => solve [apply: measure_sigma_additive] : core. -Definition finite_measure d (T : measurableType d) (R : numDomainType) - (mu : set T -> \bar R) := - mu setT < +oo. - -Lemma finite_measure_sigma_finite d (T : measurableType d) (R : realFieldType) - (mu : {measure set T -> \bar R}) : - finite_measure mu -> sigma_finite setT mu. -Proof. -exists (fun i => if i \in [set 0%N] then setT else set0). - by rewrite -bigcup_mkcondr setTI bigcup_const//; exists 0%N. -move=> n; split; first by case: ifPn. -by case: ifPn => // _; rewrite ?measure0//; exact: finite_measure. -Qed. - -HB.mixin Record isSigmaFinite d (R : numFieldType) (T : semiRingOfSetsType d) - (mu : set T -> \bar R) := { - sigma_finiteT : sigma_finite setT mu -}. - -#[short(type="sigma_finite_content")] -HB.structure Definition SigmaFiniteContent d R T := - {mu of isSigmaFinite d R T mu & @Content d R T mu}. -Arguments sigma_finiteT {d R T} s. - -Notation "{ 'sigma_finite_content' 'set' T '->' '\bar' R }" := - (sigma_finite_content R T) - (at level 36, T, R at next level, - format "{ 'sigma_finite_content' 'set' T '->' '\bar' R }") - : ring_scope. - -#[global] -Hint Resolve sigma_finiteT : core. - -#[short(type="sigma_finite_measure")] -HB.structure Definition SigmaFiniteMeasure d R T := - {mu of isSigmaFinite d R T mu & @Measure d R T mu}. - -Notation "{ 'sigma_finite_measure' 'set' T '->' '\bar' R }" := (sigma_finite_measure R T) - (at level 36, T, R at next level, - format "{ 'sigma_finite_measure' 'set' T '->' '\bar' R }") : ring_scope. - Section pushforward_measure. Local Open Scope ereal_scope. Context d d' (T1 : measurableType d) (T2 : measurableType d') (f : T1 -> T2). @@ -1950,15 +1927,6 @@ HB.instance Definition _ := isMeasure.Build _ _ _ counting End measure_count. -Lemma sigma_finite_counting (R : realType) : - sigma_finite [set: nat] (counting R). -Proof. -exists (fun n => `I_n.+1); first by apply/seteqP; split=> //x _; exists x => /=. -by move=> k; split => //; rewrite /counting/= asboolT// ltry. -Qed. -HB.instance Definition _ R := - @isSigmaFinite.Build _ _ _ (counting R) (sigma_finite_counting R). - Lemma big_trivIset (I : choiceType) D T (R : Type) (idx : R) (op : Monoid.com_law idx) (A : I -> set T) (F : set T -> R) : finite_set D -> trivIset D A -> F set0 = idx -> @@ -2567,6 +2535,327 @@ HB.instance Definition _ := isMeasure0.Build _ _ _ Rmu End ring_sigma_content. +Definition finite_measure d (T : semiRingOfSetsType d) (R : numDomainType) + (mu : set T -> \bar R) := mu setT < +oo. + +Definition sfinite_measure_def d (T : measurableType d) (R : realType) + (mu : set T -> \bar R) := + exists2 s : {measure set T -> \bar R}^nat, + forall n, finite_measure (s n) & + forall U, measurable U -> mu U = mseries s 0 U. + +Definition sigma_finite d (T : semiRingOfSetsType d) (R : numDomainType) + (A : set T) (mu : set T -> \bar R) := + exists2 F : (set T)^nat, A = \bigcup_(i : nat) F i & + forall i, measurable (F i) /\ mu (F i) < +oo. + +Lemma finite_measure_sigma_finite d (T : algebraOfSetsType d) + (R : realFieldType) (mu : set T -> \bar R) : mu set0 < +oo -> + finite_measure mu -> sigma_finite setT mu. +Proof. +move=> muoo; exists (fun i => if i \in [set 0%N] then setT else set0). + by rewrite -bigcup_mkcondr setTI bigcup_const//; exists 0%N. +by move=> n; split; case: ifPn. +Qed. + +Lemma sfinite_measure_sigma_finite d (T : measurableType d) + (R : realType) (mu : {measure set T -> \bar R}) : + sigma_finite setT mu -> sfinite_measure_def mu. +Proof. +move=> [F UF mF]; rewrite /sfinite_measure_def. +have mDF k : measurable (seqDU F k). + apply: measurableD; first exact: (mF k).1. + by apply: bigsetU_measurable => i _; exact: (mF i).1. +exists (fun k => [the measure _ _ of mrestr mu (mDF k)]) => [n|U mU]. +- rewrite /finite_measure/= /mrestr setTI (@le_lt_trans _ _ (mu (F n)))//. + + apply: le_measure; last exact: subDsetl. + * rewrite inE; apply: measurableD; first exact: (mF n).1. + by apply: bigsetU_measurable => i _; exact: (mF i).1. + * by rewrite inE; exact: (mF n).1. + + exact: (mF n).2. +rewrite /mseries/= /mrestr/=; apply/esym/cvg_lim => //. +rewrite -[X in _ --> mu X]setIT UF seqDU_bigcup_eq setI_bigcupr. +apply: (@measure_sigma_additive _ _ _ mu (fun k => U `&` seqDU F k)). + by move=> i; exact: measurableI. +exact/trivIset_setIl/trivIset_seqDU. +Qed. + +HB.mixin Record Measure_isSFinite_subdef d (T : measurableType d) + (R : realType) (mu : set T -> \bar R) := { + sfinite_measure_subdef : sfinite_measure_def mu }. + +HB.structure Definition SFiniteMeasure + d (T : measurableType d) (R : realType) := + {mu of @Measure _ T R mu & Measure_isSFinite_subdef _ T R mu }. +Arguments sfinite_measure_subdef {d T R} _. + +Notation "{ 'sfinite_measure' 'set' T '->' '\bar' R }" := + (SFiniteMeasure.type T R) (at level 36, T, R at next level, + format "{ 'sfinite_measure' 'set' T '->' '\bar' R }") : ring_scope. + +HB.mixin Record isSigmaFinite d (T : semiRingOfSetsType d) (R : numFieldType) + (mu : set T -> \bar R) := { sigma_finiteT : sigma_finite setT mu }. + +#[short(type="sigma_finite_content")] +HB.structure Definition SigmaFiniteContent d T R := + { mu of isSigmaFinite d T R mu & @Content d T R mu }. + +Arguments sigma_finiteT {d T R} s. +#[global] Hint Resolve sigma_finiteT : core. + +Notation "{ 'sigma_finite_content' 'set' T '->' '\bar' R }" := + (sigma_finite_content T R) (at level 36, T, R at next level, + format "{ 'sigma_finite_content' 'set' T '->' '\bar' R }") + : ring_scope. + +#[short(type="sigma_finite_measure")] +HB.structure Definition SigmaFiniteMeasure d T R := + { mu of @SFiniteMeasure d T R mu & isSigmaFinite d T R mu }. + +Notation "{ 'sigma_finite_measure' 'set' T '->' '\bar' R }" := + (sigma_finite_measure T R) (at level 36, T, R at next level, + format "{ 'sigma_finite_measure' 'set' T '->' '\bar' R }") + : ring_scope. + +HB.factory Record Measure_isSigmaFinite d (T : measurableType d) (R : realType) + (mu : set T -> \bar R) of isMeasure _ _ _ mu := + { sigma_finiteT : sigma_finite setT mu }. + +HB.builders Context d (T : measurableType d) (R : realType) + mu of @Measure_isSigmaFinite d T R mu. + +Lemma sfinite : sfinite_measure_def mu. +Proof. +apply: sfinite_measure_sigma_finite. +exact: sigma_finiteT. +Qed. + +HB.instance Definition _ := @Measure_isSFinite_subdef.Build _ _ _ mu sfinite. + +HB.instance Definition _ := @isSigmaFinite.Build _ _ _ mu sigma_finiteT. + +HB.end. + +Lemma finite_mzero d (T : measurableType d) (R : realType) : + finite_measure (@mzero d T R). +Proof. by rewrite /finite_measure /mzero ltey. Qed. + +Lemma sigma_finite_mzero d (T : measurableType d) + (R : realType) : sigma_finite setT (@mzero d T R). +Proof. +by apply: finite_measure_sigma_finite; [rewrite measure0|exact: finite_mzero]. +Qed. + +HB.instance Definition _ d (T : measurableType d) (R : realType) := + @isSigmaFinite.Build d T R mzero (@sigma_finite_mzero d T R). + +Lemma sfinite_mzero d (T : measurableType d) + (R : realType) : sfinite_measure_def (@mzero d T R). +Proof. +apply: sfinite_measure_sigma_finite. +exact: sigma_finite_mzero. +Qed. + +HB.instance Definition _ d (T : measurableType d) (R : realType) := + @Measure_isSFinite_subdef.Build d T R mzero (@sfinite_mzero d T R). + +Definition fin_num_fun d (T : semiRingOfSetsType d) (R : numDomainType) + (mu : set T -> \bar R) := forall U, measurable U -> mu U \is a fin_num. + +HB.mixin Record SigmaFinite_isFinite d (T : semiRingOfSetsType d) + (R : numDomainType) (k : set T -> \bar R) := + { fin_num_measure : fin_num_fun k }. + +HB.structure Definition FinNumFun d (T : semiRingOfSetsType d) + (R : numFieldType) := { k of SigmaFinite_isFinite _ T R k }. + +HB.structure Definition FiniteMeasure d (T : measurableType d) (R : realType) := + { k of @SigmaFiniteMeasure _ _ _ k & SigmaFinite_isFinite _ T R k }. +Arguments fin_num_measure {d T R} _. + +Notation "{ 'finite_measure' 'set' T '->' '\bar' R }" := + (FiniteMeasure.type T R) (at level 36, T, R at next level, + format "{ 'finite_measure' 'set' T '->' '\bar' R }") : ring_scope. + +HB.factory Record Measure_isFinite d (T : measurableType d) + (R : realType) (k : set T -> \bar R) + of isMeasure _ _ _ k := { fin_num_measure : fin_num_fun k }. + +Lemma fin_num_fun_finite_measure d (T : measurableType d) (R : realType) + (mu : set T -> \bar R) : fin_num_fun mu -> finite_measure mu. +Proof. by move=> h; rewrite /finite_measure ltey_eq h. Qed. + +Lemma finite_measure_fin_num_fun d (T : measurableType d) + (R : realType) (mu : {measure set T -> \bar R}) : + finite_measure mu -> fin_num_fun mu. +Proof. +move=> h U mU; rewrite fin_real// (lt_le_trans _ (measure_ge0 mu U))//=. +by rewrite (le_lt_trans _ h)//= le_measure// inE. +Qed. + +HB.builders Context d (T : measurableType d) (R : realType) k + of Measure_isFinite d T R k. + +Let sfinite : sfinite_measure_def k. +Proof. +apply: sfinite_measure_sigma_finite. +apply: finite_measure_sigma_finite; first by rewrite measure0. +by apply: fin_num_fun_finite_measure; exact: fin_num_measure. +Qed. + +HB.instance Definition _ := @Measure_isSFinite_subdef.Build d T R k sfinite. + +Let sigma_finite : sigma_finite setT k. +Proof. +apply: finite_measure_sigma_finite; first by rewrite measure0. +by apply: fin_num_fun_finite_measure; exact: fin_num_measure. +Qed. + +HB.instance Definition _ := @isSigmaFinite.Build d T R k sigma_finite. + +Let finite : fin_num_fun k. Proof. exact: fin_num_measure. Qed. + +HB.instance Definition _ := @SigmaFinite_isFinite.Build d T R k finite. + +HB.end. + +HB.factory Record Measure_isSFinite d (T : measurableType d) + (R : realType) (k : set T -> \bar R) of isMeasure _ _ _ k := { + sfinite_measure_subdef : exists s : {finite_measure set T -> \bar R}^nat, + forall U, measurable U -> k U = mseries s 0 U }. + +HB.builders Context d (T : measurableType d) (R : realType) + k of Measure_isSFinite d T R k. + +Let sfinite : sfinite_measure_def k. +Proof. +have [s sE] := sfinite_measure_subdef; exists s => //. +by move=> n; apply: fin_num_fun_finite_measure; exact: fin_num_measure. +Qed. + +HB.instance Definition _ := @Measure_isSFinite_subdef.Build d T R k + sfinite. + +HB.end. + +Section sfinite_measure. +Context d (T : measurableType d) (R : realType) + (mu : {sfinite_measure set T -> \bar R}). + +Let s : (set T -> \bar R)^nat := + let: exist2 x _ _ := cid2 (sfinite_measure_subdef mu) in x. + +Let s0 n : s n set0 = 0. +Proof. by rewrite /s; case: cid2. Qed. + +Let s_ge0 n x : 0 <= s n x. +Proof. by rewrite /s; case: cid2. Qed. + +Let s_semi_sigma_additive n : semi_sigma_additive (s n). +Proof. +rewrite /s; case: cid2 => s' s'1 s'2. +exact: measure_semi_sigma_additive. +Qed. + +HB.instance Definition _ n := @isMeasure.Build _ _ _ (s n) (s0 n) (s_ge0 n) + (@s_semi_sigma_additive n). + +Let s_fin n : fin_num_fun (s n). +Proof. +by rewrite /s; case: cid2 => F finF muE; exact: finite_measure_fin_num_fun. +Qed. + +HB.instance Definition _ n := + @Measure_isFinite.Build d T R (s n) (s_fin n). + +Lemma sfinite_measure : exists s : {finite_measure set T -> \bar R}^nat, + forall U, measurable U -> mu U = mseries s O U. +Proof. +exists (fun n => [the {finite_measure set T -> \bar R} of s n]) => U mU. +by rewrite /mseries /= /s; case: cid2 => // x xfin ->//. +Qed. + +End sfinite_measure. + +HB.mixin Record FiniteMeasure_isSubProbability d (T : measurableType d) + (R : realType) (P : set T -> \bar R) := + { sprobability_setT : P setT <= 1%E }. + +#[short(type=subprobability)] +HB.structure Definition SubProbability d (T : measurableType d) (R : realType) + := {mu of @FiniteMeasure d T R mu & FiniteMeasure_isSubProbability d T R mu }. + +HB.factory Record Measure_isSubProbability d (T : measurableType d) + (R : realType) (P : set T -> \bar R) of isMeasure _ _ _ P := + { sprobability_setT : P setT <= 1%E }. + +HB.builders Context d (T : measurableType d) (R : realType) + P of Measure_isSubProbability d T R P. + +Let finite : @Measure_isFinite d T R P. +Proof. +split; apply: finite_measure_fin_num_fun. +by rewrite /finite_measure (le_lt_trans (@sprobability_setT))// ltey. +Qed. + +HB.instance Definition _ := finite. + +HB.instance Definition _ := + @FiniteMeasure_isSubProbability.Build _ _ _ P sprobability_setT. + +HB.end. + +HB.mixin Record isProbability d (T : measurableType d) (R : realType) + (P : set T -> \bar R) := { probability_setT : P setT = 1%E }. + +#[short(type=probability)] +HB.structure Definition Probability d (T : measurableType d) (R : realType) := + {P of @SubProbability d T R P & isProbability d T R P }. + +Section probability_lemmas. +Context d (T : measurableType d) (R : realType) (P : probability T R). + +Lemma probability_le1 (A : set T) : measurable A -> (P A <= 1)%E. +Proof. +move=> mA; rewrite -(@probability_setT _ _ _ P). +by apply: le_measure => //; rewrite ?in_setE. +Qed. + +End probability_lemmas. + +HB.factory Record Measure_isProbability d (T : measurableType d) + (R : realType) (P : set T -> \bar R) of isMeasure _ _ _ P := + { probability_setT : P setT = 1%E }. + +HB.builders Context d (T : measurableType d) (R : realType) + P of Measure_isProbability d T R P. + +Let subprobability : @Measure_isSubProbability d T R P. +Proof. by split; rewrite probability_setT. Qed. + +HB.instance Definition _ := subprobability. + +HB.instance Definition _ := @isProbability.Build _ _ _ P probability_setT. + +HB.end. + +Section pdirac. +Context d (T : measurableType d) (R : realType). + +HB.instance Definition _ x := + Measure_isProbability.Build _ _ _ (@dirac _ T x R) (diracT R x). + +End pdirac. + +Lemma sigma_finite_counting (R : realType) : + sigma_finite [set: nat] (counting R). +Proof. +exists (fun n => `I_n.+1); first by apply/seteqP; split=> //x _; exists x => /=. +by move=> k; split => //; rewrite /counting/= asboolT// ltry. +Qed. +HB.instance Definition _ R := + @isSigmaFinite.Build _ _ _ (counting R) (sigma_finite_counting R). + Lemma measureIl d (R : realFieldType) (T : semiRingOfSetsType d) (mu : {content set T -> \bar R}) (A B : set T) : measurable A -> measurable B -> (mu (A `&` B) <= mu A)%E. @@ -3532,7 +3821,7 @@ Qed. HB.instance Definition _ := isMeasure.Build _ _ _ Hahn_ext Hahn_ext0 Hahn_ext_ge0 Hahn_ext_sigma_additive. -Lemma Hahn_ext_sigma_finite : @sigma_finite _ _ T setT mu -> +Lemma Hahn_ext_sigma_finite : @sigma_finite _ T _ setT mu -> @sigma_finite _ _ _ setT Hahn_ext. Proof. move=> -[S setTS mS]; exists S => //; move=> i; split. @@ -3775,22 +4064,3 @@ exact: (measurable_fun_comp _ _ mf). Qed. End partial_measurable_fun. - -HB.mixin Record isProbability d (T : measurableType d) - (R : realType) (P : set T -> \bar R) of isMeasure d R T P := - { probability_setT : P setT = 1%E }. - -#[short(type=probability)] -HB.structure Definition Probability d (T : measurableType d) (R : realType) := - {P of isProbability d T R P & isMeasure d R T P }. - -Section probability_lemmas. -Context d (T : measurableType d) (R : realType) (P : probability T R). - -Lemma probability_le1 (A : set T) : measurable A -> (P A <= 1)%E. -Proof. -move=> mA; rewrite -(@probability_setT _ _ _ P). -by apply: le_measure => //; rewrite ?in_setE. -Qed. - -End probability_lemmas. diff --git a/theories/radon_nikodym.v b/theories/radon_nikodym.v new file mode 100644 index 0000000000..86389421b7 --- /dev/null +++ b/theories/radon_nikodym.v @@ -0,0 +1,1159 @@ +(* -*- company-coq-local-symbols: (("`&`" . ?∩) ("`|`" . ?∪) ("set0" . ?∅)); -*- *) +(* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) +From mathcomp Require Import all_ssreflect ssralg ssrnum ssrint interval. +From mathcomp Require Import finmap fingroup perm rat. +Require Import boolp reals ereal classical_sets signed topology numfun. +Require Import mathcomp_extra functions normedtype. +From HB Require Import structures. +Require Import sequences esum measure fsbigop cardinality set_interval. +Require Import realfun. +Require Import lebesgue_measure lebesgue_integral charge. + +(******************************************************************************) +(* tentative proof of the Radon-Nikodym Theorem *) +(* *) +(* m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or m2 dominates m1 *) +(* *) +(******************************************************************************) + +Reserved Notation "m1 `<< m2" (at level 51). + +Set Implicit Arguments. +Unset Strict Implicit. +Unset Printing Implicit Defensive. +Import Order.TTheory GRing.Theory Num.Def Num.Theory. +Import numFieldTopology.Exports. + +Local Open Scope classical_set_scope. +Local Open Scope ring_scope. + +(******************************************************************************) +(* lemmas to be moved to other files *) +(******************************************************************************) + +Lemma lteNy {R : realDomainType} (x : \bar R) : (x < -oo = false)%E. +Proof. by move: x => []. Qed. + +Lemma ltye {R : realDomainType} (x : \bar R) : (+oo < x = false)%E. +Proof. by move: x => []. Qed. + +(* TODO: move to classical_sets? *) +Section preimage_bool. +Context d (T : measurableType d). +Implicit Type D : set T. + +Lemma preimage_mem_true D : mem D @^-1` [set true] = D. +Proof. by apply/seteqP; split => [x/= /set_mem//|x /mem_set]. Qed. + +Lemma preimage_mem_false D : mem D @^-1` [set false] = ~` D. +Proof. +apply/seteqP; split => [x/=|x/=]; last exact: memNset. +by apply: contraFnot; exact/mem_set. +Qed. + +End preimage_bool. + +Lemma set_neg_setC T (f : T -> bool) : [set x | ~~ f x] = ~` [set x | f x]. +Proof. by apply/seteqP; split => [x/= /negP//|x/= /negP]. Qed. + +Lemma set_eq_leq_lt d (X : porderType d) T (f g : T -> X) : + [set x | f x = g x] = [set x | (f x <= g x)%O] `\` [set x | (f x < g x)%O]. +Proof. +apply/seteqP; split => [x/= ->|x []/=]; first by split => //; rewrite ltxx. +by rewrite le_eqVlt => /orP[/eqP ->|]. +Qed. + +Lemma set_neq_lt d (X : orderType d) T (f g : T -> X) : + [set x | f x != g x ] = [set x | (f x > g x)%O] `|` [set x | (f x < g x)%O]. +Proof. +apply/seteqP; split => [x/=|]; first by rewrite neq_lt => /orP; tauto. +by move=> x/= /orP; rewrite -neq_lt eq_sym. +Qed. + +Section set_lt. +Context (R : realType) T (f g : T -> R). + +Let E j := [set x | f x - g x >= j.+1%:R^-1]. + +Lemma set_lt_bigcup : + [set x | f x > g x] = \bigcup_j E j. +Proof. +apply/seteqP; split => [x/=|x [n _]]; last first. + by rewrite /E/= -subr_gt0; apply: lt_le_trans; rewrite invr_gt0. +rewrite -subr_gt0 => fgx; exists `|floor (f x - g x)^-1%R|%N => //. +rewrite /E/= -natr1 natr_absz. +rewrite ger0_norm ?floor_ge0 ?invr_ge0; last exact/ltW. +rewrite -[leRHS]invrK lef_pinv//. +- by apply/ltW; rewrite lt_succ_floor. +- by rewrite posrE// ltr_spaddr// ler0z floor_ge0 invr_ge0 ltW. +- by rewrite posrE invr_gt0. +Qed. + +End set_lt. + +Section eset_lt. +Context (R : realType) T (f g : T -> \bar R). +Local Open Scope ereal_scope. + +Let E j := [set x | f x - g x >= j.+1%:R^-1%:E]. + +Lemma eset_lt_bigcup : [set x | f x > g x] = \bigcup_j E j. +Proof. +apply/seteqP; split => [x/=|x [n _]]; last first. + rewrite /E/= -sube_gt0; apply: lt_le_trans. + by rewrite lte_fin invr_gt0. +move Hgx : (g x) => gx. +case: gx Hgx => [gx| |gxoo fxoo]. +- move Hfx : (f x) => fx. + case: fx Hfx => [fx Hfx Hgx|fxoo Hgx _|]. + + rewrite lte_fin -subr_gt0 => fgx. + exists `|floor (fx - gx)^-1%R|%N => //. + rewrite /E/= -natr1 natr_absz. + rewrite ger0_norm ?floor_ge0 ?invr_ge0; last exact/ltW. + rewrite Hfx Hgx lee_fin -[leRHS]invrK lef_pinv//. + - by apply/ltW; rewrite lt_succ_floor. + - by rewrite posrE// ltr_spaddr// ler0z floor_ge0 invr_ge0 ltW. + - by rewrite posrE invr_gt0. + + by exists 0%N => //; rewrite /E/= fxoo Hgx// addye// leey. + + by rewrite lteNy. +- by rewrite ltye. +- by exists 0%N => //; rewrite /E/= gxoo addey// ?leey// -ltNye. +Qed. + +End eset_lt. + +Section move_to_measure. +Local Open Scope ereal_scope. +Context d (X : measurableType d) (R : realType). + +Lemma measurable_lt_fun (f g : X -> \bar R) : + measurable_fun setT f -> measurable_fun setT g -> + measurable [set x | f x < g x]. +Proof. +move=> mf mg; under eq_set do rewrite -sube_gt0; rewrite -[X in measurable X]setTI. +by apply : emeasurable_fun_o_infty => //; exact: emeasurable_funB. +Qed. + +Lemma measurable_le_fun (f g : X -> \bar R) : + measurable_fun setT f -> measurable_fun setT g -> measurable [set x | f x <= g x]. +Proof. +move=> mf mg; under eq_set do rewrite leNgt. +by rewrite set_neg_setC; apply measurableC; exact : measurable_lt_fun. +Qed. + +Lemma measurable_eq_fun (f g : X -> \bar R) : + measurable_fun setT f -> measurable_fun setT g -> measurable [set x | f x = g x]. +Proof. +move=> mf mg; rewrite set_eq_leq_lt. +by apply measurableD; [exact : measurable_le_fun|exact : measurable_lt_fun]. +Qed. + +Lemma measurable_neq_fun (f g : X -> \bar R) : + measurable_fun setT f -> measurable_fun setT g -> measurable [set x | f x != g x]. +Proof. +by move=> mf mg; rewrite set_neq_lt; apply: measurableU; apply: measurable_lt_fun. +Qed. + +Lemma measurable_fun_bigcup (n : nat) (E : (set X)^nat) + (mu : {measure set X -> \bar R}) (f : X -> \bar R) : + (forall i, measurable (E i) /\ measurable_fun (E i) f) -> + measurable_fun (\bigcup_i E i) f. +Proof. +move=> mfE mE /= Y mY; rewrite setI_bigcupl; apply: bigcup_measurable => i _. +by apply mfE => //; apply mfE. +Qed. + +End move_to_measure. + +(* NB: PR in progress *) +Lemma integrable_abse d (T : measurableType d) (R : realType) D + (f : T -> \bar R) (mu : {measure set T -> \bar R}) : + mu.-integrable D f -> mu.-integrable D (abse \o f). +Proof. +move=> [mf foo]; split; first exact: measurable_funT_comp. +by under eq_integral do rewrite abse_id. +Qed. + +Local Open Scope ereal_scope. + +Lemma positive_set_measurable d (T : measurableType d) (R : realType) + (nu : {charge set T -> \bar R}) (P : set T) : + positive_set nu P -> measurable P. +Proof. by case. Qed. + +Lemma negative_set_measurable d (T : measurableType d) (R : realType) + (nu : {charge set T -> \bar R}) (P : set T) : + negative_set nu P -> measurable P. +Proof. by case. Qed. + +(******************************************************************************) +(* /lemmas to be moved to other files *) +(******************************************************************************) + +(******************************************************************************) +(* Radon-Nikodym starts here *) +(******************************************************************************) + +(* NB: specialized to positive set *) + +Definition measure_of_charge d (T : measurableType d) (R : realType) + (nu : set T -> \bar R) of (forall E, 0 <= nu E) := nu. + +Section measure_of_charge. +Context d (T : measurableType d) (R : realType). +Variable nu : {charge set T -> \bar R}. +Hypothesis nupos : forall E, 0 <= nu E. + +Local Notation mu := (measure_of_charge nupos). + +Let mu0 : mu set0 = 0. Proof. exact: charge0. Qed. + +Let mu_ge0 S : 0 <= mu S. +Proof. by rewrite nupos. Qed. + +Let mu_sigma_additive : semi_sigma_additive mu. +Proof. exact: charge_semi_sigma_additive. Qed. + +HB.instance Definition _ := isMeasure.Build d R T (measure_of_charge nupos) + mu0 mu_ge0 mu_sigma_additive. + +Lemma measure_of_chargeE S : mu S = nu S. Proof. by []. Qed. + +End measure_of_charge. +Arguments measure_of_charge {d T R}. + +(* TODO: move to measure.v? *) +Section absolute_continuity. +Context d (T : measurableType d) (R : realType). +Implicit Types m : set T -> \bar R. + +Definition dominates m1 m2 := + forall A, measurable A -> m2 A = 0 -> m1 A = 0. + +Local Notation "m1 `<< m2" := (dominates m1 m2). + +Lemma dominates_trans m1 m2 m3 : m1 `<< m2 -> m2 `<< m3 -> m1 `<< m3. +Proof. by move=> m12 m23 A mA /m23-/(_ mA) /m12; exact. Qed. + +End absolute_continuity. +Notation "m1 `<< m2" := (dominates m1 m2). + +Definition crestr0 d (T : measurableType d) (R : realFieldType) (D : set T) + (f : set T -> \bar R) (mD : measurable D) := + fun X => if X \in measurable then f (X `&` D) else 0. + +Section charge_restriction0. +Context d (T : measurableType d) (R : realFieldType). +Variables (mu : {charge set T -> \bar R}) (D : set T) (mD : measurable D). + +Local Notation restr := (crestr0 mu mD). + +Check fin_num_fun. + +Let crestr0_fin_num_fun : fin_num_fun restr. +Proof. +move=> U mU; rewrite /crestr0 mem_set//. +suff : measurable (U `&` D) by move/(@fin_num_measure _ _ _ mu). +exact: measurableI. +Qed. + +HB.instance Definition _ := SigmaFinite_isFinite.Build _ _ _ + restr crestr0_fin_num_fun. + +Let crestr0_additive : semi_additive restr. +Proof. +move=> F n mF tF mU; pose FD i := F i `&` D. +have mFD i : measurable (FD i) by exact: measurableI. +have tFD : trivIset setT FD. + apply/trivIsetP => i j _ _ ij. + move/trivIsetP : tF => /(_ i j Logic.I Logic.I ij). + by rewrite /FD setIACA => ->; rewrite set0I. +rewrite /crestr0 mem_set//. +under [RHS]eq_bigr do rewrite mem_set//. +rewrite -(charge_semi_additive _ _ mFD)//; last exact: bigsetU_measurable. +by rewrite big_distrl. +Qed. + +HB.instance Definition _ := isAdditiveCharge.Build _ _ _ restr crestr0_additive. + +Let crestr0_sigma_additive : semi_sigma_additive restr. +Proof. +move=> F mF tF mU; pose FD i := F i `&` D. +have mFD i : measurable (FD i) by exact: measurableI. +have tFD : trivIset setT FD. + apply/trivIsetP => i j _ _ ij. + move/trivIsetP : tF => /(_ i j Logic.I Logic.I ij). + by rewrite /FD setIACA => ->; rewrite set0I. +rewrite /crestr0 setI_bigcupl ifT ?inE//. +under [X in X --> _]eq_fun do under eq_bigr do rewrite mem_set//. +apply: charge_semi_sigma_additive => //. +by apply: bigcup_measurable => k _; exact: measurableI. +Qed. + +HB.instance Definition _ := isCharge.Build _ _ _ restr crestr0_sigma_additive. + +End charge_restriction0. + +(* NB: move with Hahn decomposition? *) +Section jordan_decomposition. +Context d (X : measurableType d) (R : realType). +Variable nu : {charge set X -> \bar R}. +Variables P N : set X. +Hypothesis nuPN : hahn_decomp nu P N. + +Let mP : measurable P. Proof. by have [[mP _] _ _ _] := nuPN. Qed. + +Let mN : measurable N. Proof. by have [_ [mN _] _ _] := nuPN. Qed. + +Definition cjordan_pos : {charge set X -> \bar R} := + [the charge _ _ of crestr0 nu mP]. + +Let positive_set_cjordan_pos E : 0 <= cjordan_pos E. +Proof. +have [posP _ _ _] := nuPN. +rewrite /cjordan_pos/= /crestr0/=; case: ifPn => // /[1!inE] mE. +by apply posP; [apply: measurableI|apply: subIsetr]. +Qed. + +Definition jordan_pos := measure_of_charge _ positive_set_cjordan_pos. + +HB.instance Definition _ := Measure.on jordan_pos. + +Let finite_jordan_pos : fin_num_fun jordan_pos. +Proof. by move=> U mU; rewrite fin_num_measure. Qed. + +HB.instance Definition _ := @Measure_isFinite.Build _ _ _ + jordan_pos finite_jordan_pos. + +Definition cjordan_neg : {charge set X -> \bar R} := + [the charge _ _ of cscale (-1) [the charge _ _ of crestr0 nu mN]]. + +Let positive_set_cjordan_neg E : 0 <= cjordan_neg E. +Proof. +rewrite /cjordan_neg/= /cscale/= /crestr0/= muleC mule_le0//. +case: ifPn => // /[1!inE] mE. +by move: nuPN => [_ [_ +] _ _] => -> //; exact: measurableI. +Qed. + +Definition jordan_neg := measure_of_charge _ positive_set_cjordan_neg. + +HB.instance Definition _ := Measure.on jordan_neg. + +Let finite_jordan_neg : fin_num_fun jordan_neg. +Proof. by move=> U mU; rewrite fin_num_measure. Qed. + +HB.instance Definition _ := @Measure_isFinite.Build _ _ _ + jordan_neg finite_jordan_neg. + +Lemma jordan_decomp A : measurable A -> + nu A = jordan_pos A - jordan_neg A. +Proof. +move=> mA; rewrite /jordan_pos /jordan_neg/= /measure_of_charge/= /cscale/= /crestr0/=. +rewrite mem_set// -[in LHS](setIT A). +case: nuPN => _ _ <- PN0; rewrite setIUr chargeU//; last 3 first. + exact: measurableI. + exact: measurableI. + by rewrite setIACA PN0 setI0. +by rewrite EFinN mulN1e oppeK. +Qed. + +Lemma jordan_pos_dominates (mu : {measure set X -> \bar R}) : + nu `<< mu -> jordan_pos `<< mu. +Proof. +move=> nu_mu A mA muA0; have := nu_mu A mA muA0. +rewrite jordan_decomp// /jordan_pos /jordan_neg /measure_of_charge/=. +rewrite /cscale/= /crestr0/= mem_set//. +rewrite EFinN mulN1e oppeK. +have mAP : measurable (A `&` P). + by apply: measurableI => //; exact: positive_set_measurable posP. +suff : mu (A `&` P) = 0 by move=> /(nu_mu _ mAP) ->. +by apply/eqP; rewrite eq_le measure_ge0// andbT -muA0 le_measure// inE. +Qed. + +Lemma jordan_neg_dominates (mu : {measure set X -> \bar R}) : + nu `<< mu -> jordan_neg `<< mu. +Proof. +move=> nu_mu A mA muA0; have := nu_mu A mA muA0. +rewrite jordan_decomp// /jordan_pos /jordan_neg /measure_of_charge/=. +rewrite /cscale/= /crestr0/= mem_set//. +have mAN : measurable (A `&` N). + by apply: measurableI => //; exact: negative_set_measurable negN. +suff : mu (A `&` N) = 0 by move=> /(nu_mu _ mAN) ->; rewrite mule0. +by apply/eqP; rewrite eq_le measure_ge0// andbT -muA0 le_measure// inE. +Qed. + +End jordan_decomposition. + +(* uniqueness of RN derivative up-to almost-everywhere equality *) +Section integral_ae_eq. +Context d (T : measurableType d) (R : realType) (mu : {measure set T -> \bar R}). + +Let integral_measure_lt (g f : T -> \bar R) : + mu.-integrable setT f -> mu.-integrable setT g -> + (forall E, measurable E -> \int[mu]_(x in E) f x = \int[mu]_(x in E) g x) -> + mu [set x | g x < f x] = 0. +Proof. +move=> mf mg fg. +pose E j := [set x | f x - g x >= j.+1%:R^-1%:E]. +have mE j : measurable (E j). + rewrite /E -[X in measurable X]setTI. + apply: emeasurable_fun_c_infty => //. + apply: emeasurable_funD => //; first by case: mf. + by apply: emeasurable_funN => //; case: mg. +have muE j : mu (E j) = 0. + apply/eqP; rewrite eq_le measure_ge0// andbT. + have fg0 : \int[mu]_(x in E j) (f \- g) x = 0. + rewrite integralB//; last 2 first. + exact: integrableS mf. + exact: integrableS mg. + rewrite fg// subee// fin_num_abs (le_lt_trans (le_abse_integral _ _ _))//. + exact: measurable_funS mg.1. + case: mg => mg; apply: le_lt_trans. + by apply: subset_integral => //; exact/measurable_funT_comp. + have : mu (E j) <= j.+1%:R%:E * \int[mu]_(x in E j) (f \- g) x. + apply: (@le_trans _ _ ((j.+1%:R)%:E * \int[mu]_(x in E j) j.+1%:R^-1%:E)). + by rewrite integral_cst// muleA -EFinM divrr ?unitfE// mul1e. + rewrite lee_pmul//; first exact: integral_ge0. + apply: ge0_le_integral => //. + - exact: measurable_fun_cst. + - by move=> x; rewrite /E/=; apply: le_trans. + - by apply: emeasurable_funB; [case: mf => + _|case: mg => + _]; + exact: measurable_funS. + by rewrite fg0 mule0. +have nd_E : {homo E : n0 m / (n0 <= m)%N >-> (n0 <= m)%O}. + move=> i j ij; apply/subsetPset => x; rewrite /E/=; apply: le_trans. + by rewrite lee_fin lef_pinv// ?posrE// ler_nat. +rewrite eset_lt_bigcup. +suff: mu (\bigcup_j E j) = 0 by []. +have /cvg_lim h1 : mu \o E --> 0. + by apply: cvg_near_cst; apply: nearW. +have := @nondecreasing_cvg_mu _ _ _ mu E mE (bigcupT_measurable E mE) nd_E. +move/cvg_lim => h2. +by rewrite -h2// h1. +Qed. + +Lemma integral_ae_eq (g f : T -> \bar R) : + mu.-integrable setT f -> mu.-integrable setT g -> + (forall E, measurable E -> \int[mu]_(x in E) f x = \int[mu]_(x in E) g x) -> + ae_eq mu setT f g. +Proof. +move=> mf mg fg. +have mugf : mu [set x | g x < f x] = 0. + by apply: integral_measure_lt. +have mufg : mu [set x | f x < g x] = 0. + by apply: integral_measure_lt => // E mE; rewrite fg. +have h : ~` [set x | [set: T] x -> f x = g x] = [set x | f x != g x]. + by apply/seteqP; split => [x/= ?|x/= /eqP]; [apply/eqP; tauto|tauto]. +apply/negligibleP. + by rewrite h; apply: measurable_neq_fun; [case: mf|case: mg]. +rewrite h; rewrite set_neq_lt measureU//; last 3 first. + by apply: measurable_lt_fun; [case: mg|case: mf]. + by apply: measurable_lt_fun; [case: mf|case: mg]. + by apply/seteqP; split => x//=[/lt_trans] => /[apply]; rewrite ltxx. +by rewrite [X in X + _]mugf add0e [LHS]mufg. +Qed. + +End integral_ae_eq. + +(* preparation of the elements of the proof of Radon-Nikodym *) +Section approxRN_measure. +Context d (X : measurableType d) (R : realType). +Variable mu : {measure set X -> \bar R}. +Variable nu : {measure set X -> \bar R}. + +Definition approxRN := [set g : X -> \bar R | [/\ + forall x, 0 <= g x, mu.-integrable setT g & + forall E, measurable E -> \int[mu]_(x in E) g x <= nu E] ]. + +Let approxRN_neq0 : approxRN !=set0. +Proof. +exists (cst 0); split => //; first exact: integrable0. +by move=> E mE; rewrite integral0 measure_ge0. +Qed. + +Definition int_approxRN := [set \int[mu]_x g x | g in approxRN]. + +Definition sup_int_approxRN := ereal_sup int_approxRN. + +Local Notation M := sup_int_approxRN. + +Definition sup_int_approxRN_ge0 : 0 <= M. +Proof. +rewrite -(ereal_sup1 0) (@le_ereal_sup _ [set 0] int_approxRN)// sub1set inE. +exists (fun=> 0); last exact: integral0. +split => //; first exact : integrable0. +by move=> E; rewrite integral0 => mE; rewrite measure_ge0. +Qed. + +End approxRN_measure. + +Section approxRN_finite_measure. +Context d (X : measurableType d) (R : realType). +Variable mu : {measure set X -> \bar R}. +Variable nu : {finite_measure set X -> \bar R}. + +Local Notation approxRN := (approxRN mu nu). +Local Notation int_approxRN := (int_approxRN mu nu). +Local Notation M := (sup_int_approxRN mu nu). + +Let int_approxRN_ub : + exists M, forall x, x \in int_approxRN -> x <= M%:E. +Proof. +exists (fine (nu setT)) => x. +rewrite inE => -[g [g0 g1 g2] <-{x}]. +by rewrite fineK ?fin_num_measure// (le_trans (g2 setT _))// inE. +Qed. + +Definition sup_int_approxRN_lty : M < +oo. +Proof. +rewrite /sup_int_approxRN; have [m hm] := int_approxRN_ub. +rewrite (@le_lt_trans _ _ m%:E)// ?ltey// ub_ereal_sup// => x IGx. +by apply: hm; rewrite inE. +Qed. + +Definition sup_int_approxRN_fin_num : + M \is a fin_num. +Proof. +rewrite ge0_fin_numE//; first exact: sup_int_approxRN_lty. +exact: sup_int_approxRN_ge0. +Qed. + +Lemma approxRN_seq_ex : + { g : (X -> \bar R)^nat | + forall k, g k \in approxRN /\ \int[mu]_x g k x > M - k.+1%:R^-1%:E }. +Proof. +pose P m g := g \in approxRN /\ M - m.+1%:R^-1%:E < \int[mu]_x g x. +suff : { g : (X -> \bar R) ^nat & forall m, P m (g m)} by case => g ?; exists g. +apply: (@choice _ _ P) => m. +rewrite /P. +have /(@ub_ereal_sup_adherent _ int_approxRN) : (0 < m.+1%:R^-1 :> R)%R. + by rewrite invr_gt0. +move/(_ sup_int_approxRN_fin_num) => [_ [h Gh <-]]. +by exists h; rewrite inE; split => //; rewrite -/M in q. +Qed. + +Definition approxRN_seq : (X -> \bar R)^nat := sval approxRN_seq_ex. + +Local Notation g_ := approxRN_seq. + +Lemma approxRN_seq_prop : forall m, + g_ m \in approxRN /\ \int[mu]_x (g_ m x) > M - m.+1%:R^-1%:E. +Proof. exact: (projT2 approxRN_seq_ex). Qed. + +Lemma approxRN_seq_ge0 x n : 0 <= g_ n x. +Proof. by have [+ _]:= approxRN_seq_prop n; rewrite inE /= => -[]. Qed. + +Lemma measurable_approxRN_seq n : measurable_fun setT (g_ n). +Proof. by have := approxRN_seq_prop n; rewrite inE /= => -[[_ []]]. Qed. + +Definition max_approxRN_seq n x := + \big[maxe/-oo]_(j < n.+1) g_ j x. + +Local Notation F_ := max_approxRN_seq. + +Lemma measurable_max_approxRN_seq n : measurable_fun setT (F_ n). +Proof. +elim: n => [|n ih]. + rewrite /max_approxRN_seq. + under eq_fun do rewrite big_ord_recr/=; rewrite -/(measurable_fun _ _). + under eq_fun do rewrite big_ord0; rewrite -/(measurable_fun _ _). + under eq_fun do rewrite maxNye; rewrite -/(measurable_fun _ _). + have [+ _] := approxRN_seq_prop 0%N. + by rewrite inE /= => -[]// _ _ _; exact: measurable_approxRN_seq. +rewrite /max_approxRN_seq => m. +under eq_fun do rewrite big_ord_recr. +by apply : emeasurable_fun_max => //; exact: measurable_approxRN_seq. +Qed. + +Lemma max_approxRN_seq_ge0 n x : 0 <= F_ n x. +Proof. +by apply/bigmax_geP; right => /=; exists ord0 => //; exact: approxRN_seq_ge0. +Qed. + +Lemma max_approxRN_seq_ge n x : F_ n x >= g_ n x. +Proof. by apply/bigmax_geP; right => /=; exists ord_max. Qed. + +Lemma max_approxRN_seq_nd x : nondecreasing_seq (F_ ^~ x). +Proof. by move=> a b ab; rewrite (le_bigmax_ord xpredT (g_ ^~ x)). Qed. + +Lemma is_cvg_max_approxRN_seq n : cvg (F_ ^~ n). +Proof. by apply: ereal_nondecreasing_is_cvg; exact: max_approxRN_seq_nd. Qed. + +Lemma is_cvg_int_max_approxRN_seq A : + measurable A -> cvg (fun n => \int[mu]_(x in A) F_ n x). +Proof. +move=> mA; apply: ereal_nondecreasing_is_cvg => a b ab. +apply ge0_le_integral => //. +- by move=> ? ?; exact: max_approxRN_seq_ge0. +- by apply: measurable_funS (measurable_max_approxRN_seq a). +- by move=> ? ?; exact: max_approxRN_seq_ge0. +- exact: measurable_funS (measurable_max_approxRN_seq b). +- by move=> x _; exact: max_approxRN_seq_nd. +Qed. + +Definition is_max_approxRN m j := + [set x | F_ m x = g_ j x /\ forall k, (k < j)%N -> g_ k x < g_ j x]. + +Local Notation E := is_max_approxRN. + +Lemma is_max_approxRNE m j : + E m j = [set x| F_ m x = g_ j x] `&` + [set x |forall k, (k < j)%nat -> g_ k x < g_ j x]. +Proof. by apply/seteqP; split. Qed. + +Lemma trivIset_is_max_approxRN n : trivIset setT (E n). +Proof. +apply/trivIsetP => /= i j _ _ ij. +apply/seteqP; split => // x []; rewrite /E/= => -[+ + [+ +]]. +wlog : i j ij / (i < j)%N. + move=> h Fmgi iFm Fmgj jFm. + have := ij; rewrite neq_lt => /orP[ji|ji]; first exact: (h i j). + by apply: (h j i) => //; rewrite eq_sym. +by move=> {}ij Fmgi h Fmgj => /(_ _ ij); rewrite -Fmgi -Fmgj ltxx. +Qed. + +Lemma bigsetU_is_max_approx_RN m : \big[setU/set0]_(j < m.+1) E m j = [set: X]. +Proof. +apply/seteqP; split => // x _; rewrite -bigcup_mkord. +pose j := [arg max_(j > @ord0 m) g_ j x]%O. +have j0_proof : exists k, (k < m.+1)%N && (g_ k x == g_ j x). + by exists j => //; rewrite eqxx andbT. +pose j0 := ex_minn j0_proof. +have j0m : (j0 < m.+1)%N by rewrite /j0; case: ex_minnP => // ? /andP[]. +have j0max k : (k < j0)%N -> g_ k x < g_ j0 x. + rewrite /j0; case: ex_minnP => //= j' /andP[j'm j'j] h kj'. + rewrite lt_neqAle; apply/andP; split; last first. + rewrite (eqP j'j) /j; case: arg_maxP => //= i _. + by move/(_ (Ordinal (ltn_trans kj' j'm))); exact. + apply/negP => /eqP gkj'. + have := h k; rewrite -(eqP j'j) -gkj' eqxx andbT (ltn_trans kj' j'm). + by move=> /(_ erefl); rewrite leqNgt kj'. +exists j0 => //; split. + rewrite /F_ /max_approxRN_seq (bigmax_eq_arg _ ord0)//; last first. + by move=> ? _; rewrite leNye. + rewrite /j0/=; case: ex_minnP => //= j' /andP[j'm /eqP]. + by rewrite /g_ => -> h. +by move=> k kj; exact: j0max. +Qed. + +Lemma measurable_is_max_approx_RN m j : measurable (E m j). +Proof. +rewrite is_max_approxRNE; apply measurableI => /=. + by apply: measurable_eq_fun; [exact: measurable_max_approxRN_seq| + exact: measurable_approxRN_seq]. +(* TODO : want to use \bigcap_(k < j) [set x | g k x < g j x]) *) +rewrite [T in measurable T](_ : _ = \bigcap_(k in `I_j) [set x | g_ k x < g_ j x]). + apply bigcap_measurable => k _; apply : measurable_lt_fun => //; + exact: measurable_approxRN_seq. +by apply/seteqP; split. +Qed. + +End approxRN_finite_measure. + +(* main lemma for Radon-Nikodym *) +Section radon_nikodym_finite_ge0. +Context d (X : measurableType d) (R : realType). +Variables mu nu : {finite_measure set X -> \bar R}. + +Let G := approxRN mu nu. +Let M := sup_int_approxRN mu nu. +Let g := approxRN_seq mu nu. +Let F := max_approxRN_seq mu nu. +Let f := fun x => lim (F ^~ x). + +Let mf : measurable_fun setT f. +Proof. +rewrite (_ : f = fun x => lim_esup (F ^~ x)). + by apply: measurable_fun_lim_esup => // n; exact: measurable_max_approxRN_seq. +by apply/funext=> n; rewrite is_cvg_lim_esupE//; exact: is_cvg_max_approxRN_seq. +Qed. + +Let f_ge0 x : 0 <= f x. +Proof. +apply: lime_ge => //; first exact: is_cvg_max_approxRN_seq. +by apply: nearW => ?; exact: max_approxRN_seq_ge0. +Qed. + +Let int_fE A : measurable A -> + \int[mu]_(x in A) f x = lim (fun n => \int[mu]_(x in A) F n x). +Proof. +move=> mA; rewrite monotone_convergence// => n. +- exact: measurable_funS (measurable_max_approxRN_seq mu nu n). +- by move=> ? ?; exact: max_approxRN_seq_ge0. +- by move=> ?; exact: max_approxRN_seq_nd. +Qed. + +Let E m j := is_max_approxRN mu nu m j. + +Let int_F_nu m A (mA : measurable A) : \int[mu]_(x in A) F m x <= nu A. +Proof. +rewrite [leLHS](_ : _ = \sum_(j < m.+1) \int[mu]_(x in (A `&` E m j)) F m x); + last first. + rewrite -[in LHS](setIT A) -(bigsetU_is_max_approx_RN mu nu m) big_distrr/=. + rewrite (@ge0_integral_bigsetU _ _ _ _ (fun n => A `&` E m n))//. + - by move=> n; apply: measurableI => //; exact: measurable_is_max_approx_RN. + - apply: (@measurable_funS _ _ _ _ setT) => //. + exact: measurable_max_approxRN_seq. + - by move=> ? ?; exact: max_approxRN_seq_ge0. + - apply: trivIset_setIl; apply: (@sub_trivIset _ _ _ setT (E m)) => //. + exact: trivIset_is_max_approxRN. +rewrite [leLHS](_ : _ = \sum_(j < m.+1) (\int[mu]_(x in (A `&` (E m j))) g j x)); + last first. + apply eq_bigr => i _; apply eq_integral => x; rewrite inE => -[?] [] Fmgi h. + by apply/eqP; rewrite eq_le; rewrite /F Fmgi lexx. +rewrite [leRHS](_ : _ = \sum_(j < m.+1) (nu (A `&` E m j))); last first. + rewrite -(@measure_semi_additive _ _ _ nu (fun i => A `&` E m i))//. + - by rewrite -big_distrr/= bigsetU_is_max_approx_RN// setIT. + - by move=> k; apply: measurableI => //; exact: measurable_is_max_approx_RN. + - by apply: trivIset_setIl => //; exact: trivIset_is_max_approxRN. + - apply: bigsetU_measurable => /= i _; apply: measurableI => //. + exact: measurable_is_max_approx_RN. +apply: lee_sum => //= i _. +have [+ _] := approxRN_seq_prop mu nu i. +rewrite inE /G/= => -[_ _]; apply. +by apply: measurableI => //; exact: measurable_is_max_approx_RN. +Qed. + +Let F_G m : F m \in G. +Proof. +rewrite inE /G/=; split => //. +- by move=> ?; exact: max_approxRN_seq_ge0. +- split; first exact: measurable_max_approxRN_seq. + under eq_integral. + by move=> x _; rewrite gee0_abs; last exact: max_approxRN_seq_ge0; over. + have /le_lt_trans := int_F_nu m measurableT; apply. + apply: fin_num_fun_finite_measure. + exact: fin_num_measure. +- by move=> A; exact: int_F_nu. +Qed. + +Let M_g_F m : M - m.+1%:R^-1%:E < \int[mu]_x g m x /\ + \int[mu]_x g m x <= \int[mu]_x F m x <= M. +Proof. +split; first by have [] := approxRN_seq_prop mu nu m. +apply/andP; split; last first. + by apply: ereal_sup_ub; exists (F m) => //; have := F_G m; rewrite inE. +apply: ge0_le_integral => //. +- by move=> x _; exact: approxRN_seq_ge0. +- exact: measurable_approxRN_seq. +- by move=> ? *; exact: max_approxRN_seq_ge0. +- exact: measurable_max_approxRN_seq. +- by move=> ? _; exact: max_approxRN_seq_ge. +Qed. + +Let int_foo : \int[mu]_x `|f x| < +oo. +Proof. +rewrite (@le_lt_trans _ _ M)//; last exact: sup_int_approxRN_lty. +under eq_integral. + by move=> x _; rewrite gee0_abs; last exact: f_ge0; over. +rewrite int_fE// lime_le//; first exact: is_cvg_int_max_approxRN_seq. +by apply: nearW => n; have [_ /andP[_ ]] := M_g_F n. +Qed. + +Let int_f_nu A : measurable A -> \int[mu]_(x in A) f x <= nu A. +Proof. +move=> mA; rewrite int_fE// lime_le //; first exact: is_cvg_int_max_approxRN_seq. +by apply: nearW => n; exact: int_F_nu. +Qed. + +Let int_f_M : \int[mu]_x f x = M. +Proof. +apply/eqP; rewrite eq_le; apply/andP; split. + rewrite int_fE// lime_le //; first exact: is_cvg_int_max_approxRN_seq. + by apply: nearW => n; have [_ /andP[_]] := M_g_F n. +rewrite int_fE//. +have cvgM : (fun m => M - m.+1%:R^-1%:E) --> M. + rewrite -[X in _ --> X]sube0; apply: cvgeB. + + by rewrite fin_num_adde_defl. + + exact: cvg_cst. + + apply/fine_cvgP; split; first exact: nearW. + rewrite [X in X @ _ --> _](_ : _ = (fun x => x.+1%:R^-1))//. + apply/gtr0_cvgV0; first exact: nearW. + apply/cvgrnyP. + rewrite [X in X @ _](_ : _ = fun n => n + 1)%N; first exact: cvg_addnr. + by apply/funext => n; rewrite addn1. +apply: (@le_trans _ _ (lim (fun m => M - m.+1%:R^-1%:E))). + by move/cvg_lim : cvgM => ->. +apply: lee_lim; [by apply/cvg_ex; exists M|exact: is_cvg_int_max_approxRN_seq|]. +apply: nearW => m. +by have [/[swap] /andP[? _] /ltW/le_trans] := M_g_F m; exact. +Qed. + +Section ab_absurdo. +Context A (mA : measurable A) (h : \int[mu]_(x in A) f x < nu A). + +Lemma epsRN_ex : + {eps : {posnum R} | \int[mu]_(x in A) (f x + eps%:num%:E) < nu A}. +Proof. +have [muA0|] := eqVneq (mu A) 0. + exists (PosNum ltr01). + under eq_integral. + move=> x _; rewrite -(@gee0_abs _ (_ + _)); last by rewrite adde_ge0. + over. + rewrite (@integral_abs_eq0 _ _ _ _ setT)//. + by rewrite (le_lt_trans _ h)// integral_ge0. + by apply: emeasurable_funD => //; exact: measurable_fun_cst. +rewrite neq_lt ltNge measure_ge0//= => muA_gt0. +pose mid := ((fine (nu A) - fine (\int[mu]_(x in A) f x)) / 2)%R. +pose e := (mid / fine (mu A))%R. +have ? : \int[mu]_(x in A) f x \is a fin_num. + by rewrite ge0_fin_numE// ?(lt_le_trans h)// ?leey// integral_ge0. +have e_gt0 : (0 < e)%R. + rewrite /e divr_gt0//; last by rewrite fine_gt0// fin_num_ltey ?fin_num_measure// andbT. + by rewrite divr_gt0// subr_gt0// fine_lt// fin_num_measure. +exists (PosNum e_gt0); rewrite ge0_integralD//; last 2 first. + exact: measurable_funS mf. + exact: measurable_fun_cst. +rewrite integral_cst// -lte_subr_addr//; last first. + by rewrite fin_numM// fin_num_measure. +rewrite -[X in _ * X](@fineK _ (mu A)) ?fin_num_measure//. +rewrite -EFinM -mulrA mulVr ?mulr1; last first. + by rewrite unitfE gt_eqF// fine_gt0// muA_gt0// fin_num_ltey// fin_num_measure. +rewrite lte_subr_addl// addeC -lte_subr_addl//; last first. +rewrite -(@fineK _ (nu A))// ?fin_num_measure// -[X in _ - X](@fineK _)// -EFinB lte_fin. +by rewrite /mid ltr_pdivr_mulr// ltr_pmulr// ?ltr1n// subr_gt0 fine_lt// fin_num_measure. +Qed. + +Definition epsRN := sval epsRN_ex. + +Definition sigmaRN B := nu B - \int[mu]_(x in B) (f x + epsRN%:num%:E). + +Let fin_num_int_f_eps B : measurable B -> + \int[mu]_(x in B) (f x + epsRN%:num%:E) \is a fin_num. +Proof. +move=> mB; rewrite ge0_integralD//; last 2 first. + exact: measurable_funS mf. + exact/EFin_measurable_fun/measurable_fun_cst. +rewrite fin_numD integral_cst// fin_numM ?fin_num_measure// andbT. +rewrite ge0_fin_numE ?measure_ge0//; last exact: integral_ge0. +rewrite (le_lt_trans _ int_foo)//. +under [in leRHS]eq_integral do rewrite gee0_abs//. +exact: subset_integral. +Qed. + +Let fin_num_sigmaRN B : measurable B -> sigmaRN B \is a fin_num. +Proof. +move=> mB; rewrite /sigmaRN fin_numB fin_num_measure//=. +exact: fin_num_int_f_eps. +Qed. + +HB.instance Definition _ := + @SigmaFinite_isFinite.Build _ _ _ sigmaRN fin_num_sigmaRN. + +Let sigmaRN_semi_additive : semi_additive sigmaRN. +Proof. +move=> H n mH tH mUH. +rewrite /sigmaRN measure_semi_additive// big_split/= fin_num_sumeN; last first. + by move=> i _; rewrite fin_num_int_f_eps. +congr (_ - _); rewrite ge0_integral_bigsetU//. +- rewrite -bigcup_mkord. + have : measurable_fun setT (fun x => f x + epsRN%:num%:E). + apply: emeasurable_funD => //. + exact/EFin_measurable_fun/measurable_fun_cst. + exact: measurable_funS. +- by move=> x _; rewrite adde_ge0. +- exact: sub_trivIset tH. +Qed. + +HB.instance Definition _ := + @isAdditiveCharge.Build _ _ _ sigmaRN sigmaRN_semi_additive. + +Let sigmaRN_semi_sigma_additive : semi_sigma_additive sigmaRN. +Proof. +move=> H mH tH mUH. +rewrite [X in X --> _](_ : _ = (fun n => \sum_(0 <= i < n) nu (H i) - + \sum_(0 <= i < n) \int[mu]_(x in H i) (f x + epsRN%:num%:E))); last first. + apply/funext => n; rewrite big_split/= fin_num_sumeN// => i _. + by rewrite fin_num_int_f_eps. +apply: cvgeB. +- by rewrite adde_defC fin_num_adde_defl// fin_num_measure. +- exact: measure_semi_sigma_additive. +- rewrite (ge0_integral_bigcup mH _ _ tH). + + have /cvg_ex[/= l hl] : cvg (fun x => + \sum_(0 <= i < x) \int[mu]_(y in H i) (f y + epsRN%:num%:E)). + apply: is_cvg_ereal_nneg_natsum => n _. + by apply: integral_ge0 => x _; rewrite adde_ge0. + by rewrite (@cvg_lim _ _ _ _ _ _ l). + + split. + suff: measurable_fun setT (fun x => f x + epsRN%:num%:E). + exact: measurable_funS. + apply: emeasurable_funD => //. + exact/EFin_measurable_fun/measurable_fun_cst. + apply: (@le_lt_trans _ _ (\int[mu]_(x in \bigcup_k H k) `|f x| + + \int[mu]_(x in \bigcup_k H k)`| epsRN%:num%:E |)). + rewrite -(integralD mUH); last 2 first. + * apply: integrable_abse; split; first exact: measurable_funS mf. + rewrite (le_lt_trans _ int_foo)// subset_integral//. + exact: measurable_funT_comp. + * apply: integrable_abse. + split; first exact/EFin_measurable_fun/measurable_fun_cst. + by rewrite integral_cst//= lte_mul_pinfty// fin_num_ltey// fin_num_measure. + apply: ge0_le_integral => //. + * apply: measurable_funT_comp => //. + apply: emeasurable_funD => //; first exact: measurable_funS mf. + exact/EFin_measurable_fun/measurable_fun_cst. + * apply: emeasurable_funD => //. + apply: measurable_funT_comp => //; first exact: measurable_funS mf. + apply: measurable_funT_comp => //. + exact/EFin_measurable_fun/measurable_fun_cst. + * by move=> x _; exact: lee_abs_add. + apply: lte_add_pinfty. + rewrite (le_lt_trans _ int_foo)// subset_integral//. + exact: measurable_funT_comp. + by rewrite integral_cst//= lte_mul_pinfty// fin_num_ltey// fin_num_measure. + + by move=> x _; rewrite adde_ge0. +Qed. + +HB.instance Definition _ := @isCharge.Build _ _ _ sigmaRN + sigmaRN_semi_sigma_additive. + +End ab_absurdo. + +Lemma radon_nikodym_finite_ge0 : nu `<< mu -> exists f : X -> \bar R, + [/\ forall x, f x >= 0, mu.-integrable setT f & + forall E, measurable E -> nu E = \int[mu]_(x in E) f x]. +Proof. +move=> nu_mu; exists f; split => // A mA. +apply/eqP; rewrite eq_le int_f_nu// andbT leNgt; apply/negP => abs. +pose sigma : {charge set X -> \bar R} := + [the {charge set X -> \bar R} of sigmaRN mA abs]. +have [P [N [[mP posP] [mN negN] PNX PN0]]] := Hahn_decomposition sigma. +pose AP := A `&` P. +have mAP : measurable AP by exact: measurableI. +have muAP_gt0 : 0 < mu AP. + rewrite lt_neqAle measure_ge0// andbT eq_sym. + apply/eqP/(contra_not (nu_mu _ mAP))/eqP; rewrite gt_eqF //. + rewrite (@lt_le_trans _ _ (sigma AP))//. + rewrite (@lt_le_trans _ _ (sigma A))//; last first. + rewrite (charge_partition _ _ mP mN)// gee_addl//. + by apply: negN => //; exact: measurableI. + by rewrite sube_gt0// (proj2_sig (epsRN_ex mA abs)). + rewrite /sigma/= /sigmaRN lee_subel_addl ?fin_num_measure//. + by rewrite lee_paddl// integral_ge0// => x _; rewrite adde_ge0. +pose h x := if x \in AP then f x + (epsRN mA abs)%:num%:E else f x. +have mh : measurable_fun setT h. + apply: (@measurable_fun_if _ _ _ _ _ _ _ _ (mem AP))=> //. + apply: (@emeasurable_fun_bool _ _ _ _ true). + by rewrite preimage_mem_true. + apply: measurable_funTS; apply: emeasurable_funD => //. + exact: measurable_fun_cst. + exact: measurable_funTS. +have hge0 x : 0 <= h x by rewrite /h; case: ifPn => // _; rewrite adde_ge0. +have hnuP S : measurable S -> S `<=` AP -> \int[mu]_(x in S) h x <= nu S. + move=> mS SAP. + have : 0 <= sigma S. + apply: posP => //. + by apply: (subset_trans SAP); exact: subIsetr. + rewrite sube_ge0; last by rewrite fin_num_measure// orbT. + apply: le_trans; rewrite le_eqVlt; apply/orP; left; apply/eqP. + rewrite -{1}(setIid S) integral_mkcondr; apply/eq_integral => x /[!inE] Sx. + by rewrite /restrict /h !ifT// inE//; exact: SAP. +have hnuN S : measurable S -> S `<=` ~` AP -> \int[mu]_(x in S) h x <= nu S. + move=> mS ScAP; rewrite /h; under eq_integral. + move=> x xS; rewrite ifF; last first. + by apply/negbTE; rewrite notin_set; apply: ScAP; apply: set_mem. + over. + exact: int_f_nu. +have hnu S : measurable S -> \int[mu]_(x in S) h x <= nu S. + move=> mS. + rewrite -(setD0 S) -(setDv AP) setDDr. + have mSIAP : measurable (S `&` AP) by exact: measurableI. + have mSDAP : measurable (S `\` AP) by exact: measurableD. + rewrite integral_setU //; last 2 first. + - exact: (measurable_funS measurableT). + - by rewrite disj_set2E setDE setIACA setICl setI0. + rewrite measureU//. + by apply: lee_add; [exact: hnuN|exact: hnuP]. + by rewrite setDE setIACA setICl setI0. +have int_h_M : \int[mu]_x h x > M. + have mCAP := measurableC mAP. + have disj_AP : [disjoint AP & ~` AP] by exact/disj_set2P/setICr. + rewrite -(setUv AP) integral_setU ?setUv// /h. + under eq_integral do rewrite ifT//. + under [X in _ < _ + X]eq_integral. + by move=> x; rewrite inE /= => xE0p; rewrite memNset//; over. + rewrite ge0_integralD//; last 2 first. + - exact: measurable_funTS. + - exact: measurable_fun_cst. + rewrite integral_cst // addeAC -integral_setU ?setUv//. + rewrite int_f_M -lte_subel_addl; last first. + by rewrite ge0_fin_numE// ?sup_int_approxRN_lty// sup_int_approxRN_ge0. + by rewrite /M subee ?mule_gt0// sup_int_approxRN_fin_num. +have Gh : G h. + split=> //; split => //. + under eq_integral do rewrite gee0_abs//. + by rewrite (le_lt_trans (hnu _ measurableT))// fin_num_ltey// fin_num_measure. +have : \int[mu]_x h x <= M. + rewrite -(ereal_sup1 (\int[mu]_x h x)). + rewrite (@le_ereal_sup _ [set \int[mu]_x h x] (int_approxRN mu nu))//. + by rewrite sub1set inE; exists h. +by rewrite leNgt int_h_M. +Qed. + +End radon_nikodym_finite_ge0. + +(* TODO: move *) +Lemma eq_eseriesl (R : realFieldType) (P Q : pred nat) (f : (\bar R)^nat) : + P =1 Q -> \sum_(i efg; congr (lim _); apply/funext => n; exact: eq_bigl. Qed. +Arguments eq_eseriesl {R P} Q. + +Definition mfrestr d (T : measurableType d) (R : realFieldType) (D : set T) + (f : set T -> \bar R) (mD : measurable D) (moo : f D < +oo) := + fun X => f (X `&` D). + +Section measure_frestr. +Context d (T : measurableType d) (R : realType). +Variables (mu : {measure set T -> \bar R}) (D : set T) (mD : measurable D). +Hypothesis moo : mu D < +oo. + +Local Notation restr := (mfrestr mD moo). + +Let restr0 : restr set0 = 0%E. +Proof. by rewrite /restr set0I measure0. Qed. + +Let restr_ge0 (A : set _) : (0 <= restr A)%E. +Proof. +by rewrite /restr; apply: measure_ge0; apply: measurableI. +Qed. + +Let restr_sigma_additive : semi_sigma_additive restr. +Proof. +move=> F mF tF mU; pose FD i := F i `&` D. +have mFD i : measurable (FD i) by exact: measurableI. +have tFD : trivIset setT FD. + apply/trivIsetP => i j _ _ ij. + move/trivIsetP : tF => /(_ i j Logic.I Logic.I ij). + by rewrite /FD setIACA => ->; rewrite set0I. +by rewrite /restr setI_bigcupl; exact: measure_sigma_additive. +Qed. + +HB.instance Definition _ := isMeasure.Build _ _ _ restr + restr0 restr_ge0 restr_sigma_additive. + +Let restr_fin : fin_num_fun restr. +Proof. +move=> U mU; rewrite /restr ge0_fin_numE ?measure_ge0//. +by rewrite (le_lt_trans _ moo)// le_measure// ?inE//; exact: measurableI. +Qed. + +HB.instance Definition _ := Measure_isFinite.Build _ _ _ restr + restr_fin. + +End measure_frestr. + +Section radon_nikodym. +Context d (X : measurableType d) (R : realType). + +Let radon_nikodym_sigma_finite_ge0 + (mu : {sigma_finite_measure set X -> \bar R}) + (nu : {finite_measure set X -> \bar R}) : + nu `<< mu -> + exists2 f : X -> \bar R, mu.-integrable setT f & + forall E, E \in measurable -> nu E = integral mu E f. +Proof. +move=> nu_mu. +have [F TF mFAFfin] := sigma_finiteT mu. +have {mFAFfin}[mF Ffin] := all_and2 mFAFfin. +pose E := seqDU F. +have mE k : measurable (E k). + by apply: measurableD => //; exact: bigsetU_measurable. +have Efin k : mu (E k) < +oo. + by rewrite (le_lt_trans _ (Ffin k))// le_measure ?inE//; exact: subDsetl. +have bigcupE : \bigcup_i E i = setT by rewrite TF [RHS]seqDU_bigcup_eq. +have tE := @trivIset_seqDU _ F. +pose mu_ j : {finite_measure set X -> \bar R} := + [the {finite_measure set _ -> \bar _} of @mfrestr _ _ _ _ mu (mE j) (Efin j)]. +have H1 i : nu (E i) < +oo by rewrite fin_num_ltey// fin_num_measure. +pose nu_ j : {finite_measure set X -> \bar R} := + [the {finite_measure set _ -> \bar _} of @mfrestr _ _ _ _ nu (mE j) (H1 j)]. +have nu_mu_ k : nu_ k `<< mu_ k. + by move=> S mS mu_kS0; apply: nu_mu => //; exact: measurableI. +have [g Hg] := choice (fun j => radon_nikodym_finite_ge0 (nu_mu_ j)). +have [g_ge0 integrable_g int_gE {Hg}] := all_and3 Hg. +pose f_ j x := if x \in E j then g j x else 0. +have f_ge0 k x : 0 <= f_ k x by rewrite /f_; case: ifP. +have mf_ k : measurable_fun setT (f_ k). + apply: (@measurable_fun_if _ _ _ _ _ _ _ _ (mem (E k))) => //. + by apply: (@emeasurable_fun_bool _ _ _ _ true); rewrite preimage_mem_true. + rewrite preimage_mem_true. + by apply: (measurable_funS measurableT) => //; apply (integrable_g k). + rewrite preimage_mem_false. + by apply: (measurable_funS measurableT) => //; exact: measurable_fun_cst. +have int_f_T k : integrable mu setT (f_ k). + split=> //. + under eq_integral do rewrite gee0_abs//. + rewrite -(setUv (E k)) integral_setU //; last 3 first. + - exact: measurableC. + - by rewrite setUv. + - exact/disj_set2P/subsets_disjoint. + rewrite /f_; under eq_integral do rewrite ifT//. + rewrite (@eq_measure_integral _ _ _ (E k) (mu_ k)); last first. + by move=> A mA AEj; rewrite /mu_ /= /mfrestr setIidl. + rewrite -int_gE ?inE//. + under eq_integral. + move=> x /[!inE] /= Ekx; rewrite ifF; last by rewrite memNset. + over. + by rewrite integral0 ?adde0 fin_num_ltey// fin_num_measure. +have int_f_E j S : measurable S -> \int[mu]_(x in S) f_ j x = nu (S `&` E j). + move=> mS. + have mSIEj := measurableI _ _ mS (mE j). + have mSDEj := measurableD mS (mE j). + rewrite -{1}(setUIDK S (E j)) (integral_setU _ mSIEj mSDEj)//; last 2 first. + - by rewrite setUIDK; exact: (measurable_funS measurableT). + - by apply/disj_set2P; rewrite setDE setIACA setICr setI0. + rewrite /f_ -(eq_integral _ (g j)); last first. + by move=> x /[!inE] SIEjx; rewrite /f_ ifT// inE; exact: (@subIsetr _ S). + rewrite (@eq_measure_integral _ _ _ (S `&` E j) (mu_ j)); last first. + by move=> A mA; rewrite subsetI => -[_ ?]; rewrite /mu_ /= /mfrestr setIidl. + rewrite -int_gE; last exact: measurableI. + under eq_integral. + move=> x; rewrite inE setDE /= => -[_ Ejx]. + rewrite ifF; last by rewrite memNset. + over. + by rewrite integral0 adde0 /nu_/= /mfrestr -setIA setIid. +pose f x : \bar R := \sum_(j i _; rewrite int_f_E// setTI. + rewrite -bigcupE measure_bigcup//. + by apply: eq_eseriesl => // x; rewrite in_setT. +exists f. + split; first exact: ge0_emeasurable_fun_sum. + under eq_integral do (rewrite gee0_abs; last exact: nneseries_ge0). + by rewrite int_f_nu fin_num_ltey// fin_num_measure. +move=> A /[!inE] mA; rewrite integral_nneseries//; last first. + by move=> n; exact: (measurable_funS measurableT). +rewrite nneseries_esum; last by move=> m _; rewrite integral_ge0. +under eq_esum do rewrite int_f_E//. +rewrite -nneseries_esum; last first. + by move=> n; rewrite measure_ge0//; exact: measurableI. +rewrite (eq_eseriesl (fun x => x \in [set: nat])); last by move=> x; rewrite in_setT. +rewrite -measure_bigcup//. +- by rewrite -setI_bigcupr bigcupE setIT. +- by move=> i _; exact: measurableI. +- exact: trivIset_setIl. +Qed. + +Theorem Radon_Nikodym (mu : {sigma_finite_measure set X -> \bar R}) + (nu : {charge set X -> \bar R}) : + nu `<< mu -> + exists2 f : X -> \bar R, mu.-integrable setT f & + forall E, measurable E -> nu E = \int[mu]_(x in E) f x. +Proof. +move=> nu_mu; have [P [N nuPN]] := Hahn_decomposition nu. +have [f_p intf_p f_pE] := @radon_nikodym_sigma_finite_ge0 mu + [the {finite_measure set _ -> \bar _} of (jordan_pos nuPN)] + (jordan_pos_dominates nuPN nu_mu). +have [f_n intf_n f_nE] := @radon_nikodym_sigma_finite_ge0 mu + [the {finite_measure set _ -> \bar _} of (jordan_neg nuPN)] + (jordan_neg_dominates nuPN nu_mu). +exists (f_p \- f_n); first exact: integrableB. +move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//. +- by rewrite -f_pE ?inE// -f_nE ?inE. +- exact: (integrableS measurableT). +- exact: (integrableS measurableT). +Qed. + +End radon_nikodym.