From 0ad046bc2a490b43ce7f18f0bee01d95184c99f5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 17 Feb 2023 14:06:12 +0900 Subject: [PATCH 01/11] tentative proof of Radon-Nikodym Co-authored-by: IshiguroYoshihiro --- theories/radon_nikodym.v | 1138 ++++++++++++++++++++++++++++++++++++++ 1 file changed, 1138 insertions(+) create mode 100644 theories/radon_nikodym.v diff --git a/theories/radon_nikodym.v b/theories/radon_nikodym.v new file mode 100644 index 0000000000..e14fa6ce02 --- /dev/null +++ b/theories/radon_nikodym.v @@ -0,0 +1,1138 @@ +(* -*- 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. +From mathcomp.classical Require Import mathcomp_extra boolp classical_sets. +From mathcomp.classical Require Import functions fsbigop cardinality set_interval. +From HB Require Import structures. +Require Import reals ereal signed topology numfun normedtype sequences esum. +Require Import measure realfun 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. + +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 *) +(******************************************************************************) + +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). + +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_decomposition 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). +Variables mu 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// sub1set inE. +exists (fun=> 0); last exact: integral0. +by split => //; [exact: integrable0|move=> E; rewrite integral0]. +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 /[1!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. + by apply: fin_num_fun_lty; 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 first. + by rewrite fine_gt0// muA_gt0/= ltey_eq fin_num_measure. + 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/= ltey_eq 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// ltey_eq 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// ltey_eq 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: (@measurable_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))// ltey_eq 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. + +(* NB: PR in progress *) +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 ltey_eq 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: (@measurable_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 ltey_eq 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 ltey_eq 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 [fp intfp fpE] := @radon_nikodym_sigma_finite_ge0 mu + [the {finite_measure set _ -> \bar _} of jordan_pos nuPN] + (jordan_pos_dominates nuPN nu_mu). +have [fn intfn fnE] := @radon_nikodym_sigma_finite_ge0 mu + [the {finite_measure set _ -> \bar _} of (jordan_neg nuPN)] + (jordan_neg_dominates nuPN nu_mu). +exists (fp \- fn); first exact: integrableB. +move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//. +- by rewrite -fpE ?inE// -fnE ?inE. +- exact: (integrableS measurableT). +- exact: (integrableS measurableT). +Qed. + +End radon_nikodym. From a9d77c838d9e82555b606489d57936fcab5610ba Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Thu, 27 Apr 2023 16:08:34 +0900 Subject: [PATCH 02/11] clean, changelog --- CHANGELOG_UNRELEASED.md | 13 + classical/classical_sets.v | 9 + theories/charge.v | 873 +++++++++++++++++++++++++++ theories/itv.v | 2 +- theories/measure.v | 80 +++ theories/radon_nikodym.v | 1138 ------------------------------------ 6 files changed, 976 insertions(+), 1139 deletions(-) delete mode 100644 theories/radon_nikodym.v diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 172a6510ca..1da54bc246 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -64,6 +64,19 @@ + lemma `integrable_sum` - in `probability.v` + lemma `cantelli` +- in `classical_sets.v`: + + lemmas `preimage_mem_true`, `preimage_mem_false` +- in `measure.v`: + + definition `dominates`, notation `` `<< `` + + lemma `dominates_trans` +- in `measure.v`: + + defintion `mfrestr` +- in `charge.v`: + + definition `measure_of_charge` + + definition `crestr0` + + definitions `jordan_neg`, `jordan_pos` + + lemmas `jordan_decomp`, `jordan_pos_dominates`, `jordan_neg_dominates` + + lemma `radon_nikodym_finite`, theorem `Radon_Nikodym` - in `measure.v`: + lemmas `measurable_pair1`, `measurable_pair2` diff --git a/classical/classical_sets.v b/classical/classical_sets.v index f661c379bc..9fb02bde2b 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -1387,6 +1387,15 @@ Qed. Lemma preimage10 {T R} {f : T -> R} {x} : ~ range f x -> f @^-1` [set x] = set0. Proof. by move/preimage10P. Qed. +Lemma preimage_mem_true {T} (A : set T) : mem A @^-1` [set true] = A. +Proof. by apply/seteqP; split => [x/= /set_mem//|x /mem_set]. Qed. + +Lemma preimage_mem_false {T} (A : set T) : mem A @^-1` [set false] = ~` A. +Proof. +apply/seteqP; split => [x/=|x/=]; last exact: memNset. +by apply: contraFnot; exact/mem_set. +Qed. + End image_lemmas. Arguments sub_image_setI {aT rT f A B} t _. diff --git a/theories/charge.v b/theories/charge.v index fc12d8e072..4782eb2190 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -21,14 +21,24 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* Charge == structure of charges *) (* charge T R == type of charges *) (* {charge set T -> \bar R} == charge over T, a semiring of sets *) +(* measure_of_charge nu nu0 == measure corresponding to the charge nu, nu0 *) +(* is a proof that nu is non-negative *) (* crestr nu mD == restriction of the charge nu to the domain D *) (* where mD is a proof that D is measurable *) +(* crestr0 nu mD == csrestr nu mD that returns 0 for *) +(* non-measurable sets *) (* czero == zero charge *) (* cscale r nu == charge nu scaled by a factor r *) (* positive_set nu P == P is a positive set *) (* negative_set nu N == N is a negative set *) (* hahn_decomposition nu P N == the charge nu is decomposed into the positive *) (* set P and the negative set N *) +(* jordan_pos nu nuPN == the charge obtained by restricting the charge *) +(* nu to the positive set P of the Hahn *) +(* decomposition nuPN: hahn_decomposition nu P N *) +(* jordan_neg nu nuPN == the charge obtained by restricting the charge *) +(* nu to the positive set N of the Hahn *) +(* decomposition nuPN: hahn_decomposition nu P N *) (* *) (******************************************************************************) @@ -153,6 +163,28 @@ End charge_lemmas. #[export] Hint Resolve charge0 : core. #[export] Hint Resolve charge_semi_additive2 : core. +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). +Variables (nu : {charge set T -> \bar R}) (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. + +End measure_of_charge. +Arguments measure_of_charge {d T R}. + Section charge_lemmas_realFieldType. Context d (T : measurableType d) (R : realFieldType). Implicit Type nu : {charge set T -> \bar R}. @@ -218,6 +250,42 @@ HB.instance Definition _ := End charge_restriction. +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 crestr f mD X else 0. + +Section charge_restriction0. +Context d (T : measurableType d) (R : realFieldType). +Variables (nu : {charge set T -> \bar R}) (D : set T) (mD : measurable D). + +Local Notation restr := (crestr0 nu mD). + +Let crestr0_fin_num_fun : fin_num_fun restr. +Proof. by move=> U mU; rewrite /crestr0 mem_set// fin_num_measure. 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; rewrite /crestr0 mem_set// charge_semi_additive//=. +by apply: eq_bigr => i _; rewrite mem_set. +Qed. + +HB.instance Definition _ := isAdditiveCharge.Build _ _ _ restr crestr0_additive. + +Let crestr0_sigma_additive : semi_sigma_additive restr. +Proof. +move=> F mF tF mU; rewrite /crestr0 mem_set//. +rewrite [X in X --> _](_ : _ = (fun n => \sum_(0 <= i < n) crestr nu mD (F i))). + exact: charge_semi_sigma_additive. +by apply/funext => n; apply: eq_bigr => i _; rewrite mem_set. +Qed. + +HB.instance Definition _ := isCharge.Build _ _ _ restr crestr0_sigma_additive. + +End charge_restriction0. + Section charge_zero. Context d (T : measurableType d) (R : realFieldType). Local Open Scope ereal_scope. @@ -698,3 +766,808 @@ split. Qed. End hahn_decomposition_theorem. + +Section jordan_decomposition. +Context d (X : measurableType d) (R : realType). +Variable nu : {charge set X -> \bar R}. +Variables (P N : set X) (nuPN : hahn_decomposition nu P N). + +Let mP : measurable P. Proof. by have [[mP _] _ _ _] := nuPN. Qed. + +Let mN : measurable N. Proof. by have [_ [mN _] _ _] := nuPN. Qed. + +Let 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. + +Let 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/=. +rewrite /cscale/= /crestr0/= mem_set// -[in LHS](setIT A). +case: nuPN => _ _ <- PN0; rewrite setIUr chargeU//. +- by rewrite EFinN mulN1e oppeK. +- exact: measurableI. +- exact: measurableI. +- by rewrite setIACA PN0 setI0. +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// EFinN mulN1e oppeK. +have mAP : measurable (A `&` P) by exact: measurableI. +suff : mu (A `&` P) = 0 by move/(nu_mu _ mAP); rewrite /crestr => ->. +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 exact: measurableI. +suff : mu (A `&` N) = 0. + by move=> /(nu_mu _ mAN); rewrite /crestr => ->; rewrite mule0. +by apply/eqP; rewrite eq_le measure_ge0// andbT -muA0 le_measure// inE. +Qed. + +End jordan_decomposition. + +Section PR_in_progress. + +Lemma set_eq_le d (rT : porderType d) T (f g : T -> rT) : + [set x | f x = g x] = [set x | (f x <= g x)%O] `&` [set x | (f x >= g x)%O]. +Proof. by apply/seteqP; split => [x/= ->//|x /andP]; rewrite -eq_le =>/eqP. Qed. + +Local Open Scope ereal_scope. +Context d (T : measurableType d) (R : realType). + +Lemma emeasurable_fun_lt (D : set T) (mD : measurable D) (f g : T -> \bar R) : + measurable_fun D f -> measurable_fun D g -> + measurable (D `&` [set x | f x < g x]). +Proof. +move=> mf mg; under eq_set do rewrite -sube_gt0. +by apply: emeasurable_fun_o_infty => //; exact: emeasurable_funB. +Qed. + +Lemma emeasurable_fun_le (D : set T) (mD : measurable D) (f g : T -> \bar R) : + measurable_fun D f -> measurable_fun D g -> + measurable (D `&` [set x | f x <= g x]). +Proof. +move=> mf mg; under eq_set do rewrite -sube_le0. +by apply: emeasurable_fun_infty_c => //; exact: emeasurable_funB. +Qed. + +Lemma emeasurable_fun_eq (D : set T) (mD : measurable D) (f g : T -> \bar R) : + measurable_fun D f -> measurable_fun D g -> + measurable (D `&` [set x | f x = g x]). +Proof. +move=> mf mg; rewrite set_eq_le setIIr. +by apply: measurableI; apply: emeasurable_fun_le. +Qed. + +End PR_in_progress. + +(* We put definitions and lemmas used only in the proof of the Radon-Nikodym + theorem as Definition's and Lemma's in the following modules. See + https://staff.aist.go.jp/reynald.affeldt/documents/measure-ppl2023.pdf + for an overview. *) +Module approxRN. +Section approxRN. +Context d (X : measurableType d) (R : realType). +Variables mu 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. + +Lemma sup_int_approxRN_ge0 : 0 <= sup_int_approxRN. +Proof. +rewrite -(ereal_sup1 0) le_ereal_sup// sub1set inE. +exists (fun=> 0); last exact: integral0. +by split => //; [exact: integrable0|move=> E; rewrite integral0]. +Qed. + +End approxRN. +End approxRN. + +Module approxRN_seq. +Section approxRN_seq. +Context d (X : measurableType d) (R : realType). +Variable mu : {measure set X -> \bar R}. +Variable nu : {finite_measure set X -> \bar R}. + +Import approxRN. + +Let approxRN := approxRN mu nu. +Let int_approxRN := int_approxRN mu nu. +Let 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 /[1!inE] -[g [g0 g1 g2] <-{x}]. +by rewrite fineK ?fin_num_measure// (le_trans (g2 setT _))// inE. +Qed. + +Lemma 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. + +Lemma 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. + +Let 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 =>-[[_ /integrableP[]]]. Qed. + +Definition max_approxRN_seq n x := \big[maxe/-oo]_(j < n.+1) g_ j x. + +Let F_ := max_approxRN_seq. + +Lemma measurable_max_approxRN_seq n : measurable_fun setT (F_ n). +Proof. +elim: n => [|n ih]. + rewrite /F_ /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 /F_ /max_approxRN_seq => m. +under eq_fun do rewrite big_ord_recr. +by apply: measurable_maxe => //; 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]. + +Let 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_approxRN 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_approxRN m j : measurable (E m j). +Proof. +rewrite is_max_approxRNE; apply: measurableI => /=. + rewrite -[X in measurable X]setTI. + by apply: emeasurable_fun_eq => //; [exact: measurable_max_approxRN_seq| + exact: measurable_approxRN_seq]. +rewrite [T in measurable T](_ : _ = \bigcap_(k in `I_j) [set x | g_ k x < g_ j x])//. +apply: bigcap_measurable => k _. +rewrite -[X in measurable X]setTI; apply: emeasurable_fun_lt => //; +exact: measurable_approxRN_seq. +Qed. + +End approxRN_seq. +End approxRN_seq. + +Module lim_max_approxRN_seq. +Section lim_max_approxRN_seq. +Context d (X : measurableType d) (R : realType). +Variables mu nu : {finite_measure set X -> \bar R}. + +Import approxRN. + +Let G := approxRN mu nu. +Let M := sup_int_approxRN mu nu. + +Import approxRN_seq. + +Let g := approxRN_seq mu nu. +Let F := max_approxRN_seq mu nu. + +Definition fRN := fun x => lim (F ^~ x). + +Lemma measurable_fun_fRN : measurable_fun setT fRN. +Proof. +rewrite (_ : fRN = 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. + +Lemma fRN_ge0 x : 0 <= fRN x. +Proof. +apply: lime_ge => //; first exact: is_cvg_max_approxRN_seq. +by apply: nearW => ?; exact: max_approxRN_seq_ge0. +Qed. + +Let int_fRN_lim A : measurable A -> + \int[mu]_(x in A) fRN 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_approxRN mu nu m) big_distrr/=. + rewrite (@ge0_integral_bigsetU _ _ _ _ (fun n => A `&` E m n))//. + - by move=> n; apply: measurableI => //; exact: measurable_is_max_approxRN. + - by apply: measurable_funTS => //; 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_approxRN// setIT. + - by move=> k; apply: measurableI => //; exact: measurable_is_max_approxRN. + - by apply: trivIset_setIl => //; exact: trivIset_is_max_approxRN. + - apply: bigsetU_measurable => /= i _; apply: measurableI => //. + exact: measurable_is_max_approxRN. +apply: lee_sum => //= i _. +have [+ _] := approxRN_seq_prop mu nu i. +rewrite inE /G/= => -[_ _]; apply. +by apply: measurableI => //; exact: measurable_is_max_approxRN. +Qed. + +Let F_G m : F m \in G. +Proof. +rewrite inE /G/=; split => //. +- by move=> ?; exact: max_approxRN_seq_ge0. +- apply/integrableP; 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. + by apply: fin_num_fun_lty; 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. + +Lemma int_fRN_lty : \int[mu]_x `|fRN 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: fRN_ge0; over. +rewrite int_fRN_lim// lime_le//; first exact: is_cvg_int_max_approxRN_seq. +by apply: nearW => n; have [_ /andP[_ ]] := M_g_F n. +Qed. + +Lemma int_fRN_ub A : measurable A -> \int[mu]_(x in A) fRN x <= nu A. +Proof. +move=> mA; rewrite int_fRN_lim// lime_le //. + exact: is_cvg_int_max_approxRN_seq. +by apply: nearW => n; exact: int_F_nu. +Qed. + +Lemma int_fRNE : \int[mu]_x fRN x = M. +Proof. +apply/eqP; rewrite eq_le; apply/andP; split. + rewrite int_fRN_lim// lime_le//; first exact: is_cvg_int_max_approxRN_seq. + by apply: nearW => n; have [_ /andP[_]] := M_g_F n. +rewrite int_fRN_lim//. +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) fRN x < nu A). + +Lemma epsRN_ex : + {eps : {posnum R} | \int[mu]_(x in A) (fRN 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 first. + by rewrite adde_ge0// fRN_ge0. + over. + rewrite (@integral_abs_eq0 _ _ _ _ setT)//. + by rewrite (le_lt_trans _ h)// integral_ge0// => x Ax; exact: fRN_ge0. + by apply: emeasurable_funD => //; exact: measurable_fun_fRN. +rewrite neq_lt ltNge measure_ge0//= => muA_gt0. +pose mid := ((fine (nu A) - fine (\int[mu]_(x in A) fRN x)) / 2)%R. +pose e := (mid / fine (mu A))%R. +have ? : \int[mu]_(x in A) fRN x \is a fin_num. + rewrite ge0_fin_numE// ?(lt_le_trans h)// ?leey// integral_ge0//. + by move=> x Ax; exact: fRN_ge0. +have e_gt0 : (0 < e)%R. + rewrite /e divr_gt0//; last first. + by rewrite fine_gt0// muA_gt0/= ltey_eq fin_num_measure. + by rewrite divr_gt0// subr_gt0// fine_lt// fin_num_measure. +exists (PosNum e_gt0); rewrite ge0_integralD//; last 2 first. + by move=> x Ax; exact: fRN_ge0. + exact: measurable_funS measurable_fun_fRN. +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/= ltey_eq fin_num_measure. +rewrite lte_subr_addl// addeC -lte_subr_addl//; last first. +rewrite -(@fineK _ (nu A))// ?fin_num_measure// -[X in _ - X](@fineK _)//. +rewrite -EFinB lte_fin /mid ltr_pdivr_mulr// ltr_pmulr// ?ltr1n// subr_gt0. +by rewrite fine_lt// fin_num_measure. +Qed. + +Definition epsRN := sval epsRN_ex. + +Definition sigmaRN B := nu B - \int[mu]_(x in B) (fRN x + epsRN%:num%:E). + +Let fin_num_int_fRN_eps B : measurable B -> + \int[mu]_(x in B) (fRN x + epsRN%:num%:E) \is a fin_num. +Proof. +move=> mB; rewrite ge0_integralD//; last 2 first. + by move=> x Bx; exact: fRN_ge0. + exact: measurable_funS measurable_fun_fRN. +rewrite fin_numD integral_cst// fin_numM ?fin_num_measure// andbT. +rewrite ge0_fin_numE ?measure_ge0//; last first. + by apply: integral_ge0 => x Bx; exact: fRN_ge0. +rewrite (le_lt_trans _ int_fRN_lty)//. +under [in leRHS]eq_integral. + move=> x _; rewrite gee0_abs; last first. + exact: fRN_ge0. + over. +apply: subset_integral => //; first exact: measurable_fun_fRN. +by move=> x _; exact: fRN_ge0. +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_fRN_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_fRN_eps. +congr (_ - _); rewrite ge0_integral_bigsetU//. +- rewrite -bigcup_mkord. + have : measurable_fun setT (fun x => fRN x + epsRN%:num%:E). + by apply: emeasurable_funD => //; exact: measurable_fun_fRN. + exact: measurable_funS. +- by move=> x _; rewrite adde_ge0//; exact: fRN_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) (fRN x + epsRN%:num%:E))); last first. + apply/funext => n; rewrite big_split/= fin_num_sumeN// => i _. + by rewrite fin_num_int_fRN_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) (fRN y + epsRN%:num%:E)). + apply: is_cvg_ereal_nneg_natsum => n _. + by apply: integral_ge0 => x _; rewrite adde_ge0//; exact: fRN_ge0. + by rewrite (@cvg_lim _ _ _ _ _ _ l). + + apply/integrableP; split. + suff: measurable_fun setT (fun x => fRN x + epsRN%:num%:E). + exact: measurable_funS. + by apply: emeasurable_funD => //; exact: measurable_fun_fRN. + apply: (@le_lt_trans _ _ (\int[mu]_(x in \bigcup_k H k) `|fRN x| + + \int[mu]_(x in \bigcup_k H k)`| epsRN%:num%:E |)). + rewrite -(integralD mUH); last 2 first. + * apply/integrable_abse/integrableP; split. + exact: measurable_funS measurable_fun_fRN. + rewrite (le_lt_trans _ int_fRN_lty)// subset_integral//. + by apply: measurableT_comp => //; exact: measurable_fun_fRN. + * apply/integrable_abse/integrableP; split => //. + by rewrite integral_cst//= lte_mul_pinfty// ltey_eq fin_num_measure. + apply: ge0_le_integral => //. + * apply: measurableT_comp => //; apply: emeasurable_funD => //. + exact: measurable_funS measurable_fun_fRN. + * apply: emeasurable_funD => //; apply: measurableT_comp => //. + exact: measurable_funS measurable_fun_fRN. + * by move=> x _; exact: lee_abs_add. + apply: lte_add_pinfty. + rewrite (le_lt_trans _ int_fRN_lty)// subset_integral//. + by apply: measurableT_comp => //; exact: measurable_fun_fRN. + by rewrite integral_cst//= lte_mul_pinfty// ltey_eq fin_num_measure. + + by move=> x _; rewrite adde_ge0//; exact: fRN_ge0. +Qed. + +HB.instance Definition _ := @isCharge.Build _ _ _ sigmaRN + sigmaRN_semi_sigma_additive. + +End ab_absurdo. + +End lim_max_approxRN_seq. +End lim_max_approxRN_seq. + +Section radon_nikodym_finite. +Context d (X : measurableType d) (R : realType). +Variables mu nu : {finite_measure set X -> \bar R}. + +Import approxRN. + +Let G := approxRN mu nu. +Let M := sup_int_approxRN mu nu. + +Import lim_max_approxRN_seq. + +Let f := fRN mu nu. +Let mf := measurable_fun_fRN. +Let f_ge0 := fRN_ge0. + +Lemma radon_nikodym_finite : 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. + - by move=> x; exact: f_ge0. + - by apply/integrableP; split; [exact: mf|exact: int_fRN_lty]. +move=> // A mA. +apply/eqP; rewrite eq_le int_fRN_ub// 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//; exact: f_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 => //. + - by apply: (measurable_fun_bool true); rewrite preimage_mem_true. + - by apply: measurable_funTS; apply: emeasurable_funD => //; exact: mf. + - by apply: measurable_funTS; exact: mf. +have hge0 x : 0 <= h x. + rewrite /h; case: ifPn; last by move=> ?; exact: f_ge0. + by move=> _; rewrite adde_ge0//; exact: f_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_fRN_ub. +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 //. + - rewrite measureU//. + by apply: lee_add; [exact: hnuN|exact: hnuP]. + by rewrite setDE setIACA setICl setI0. + - exact: measurable_funTS. + - by rewrite disj_set2E 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. + - by move=> x _; exact: f_ge0. + - by apply: measurable_funTS; exact: mf. + rewrite integral_cst // addeAC -integral_setU//; last 2 first. + by rewrite setUv//; exact: mf. + by move=> x _; exact: f_ge0. + rewrite setUv int_fRNE -lte_subel_addl; last first. + rewrite ge0_fin_numE// ?sup_int_approxRN_lty//. + exact: approxRN_seq.sup_int_approxRN_lty. + exact: sup_int_approxRN_ge0. + by rewrite /M subee ?mule_gt0// approxRN_seq.sup_int_approxRN_fin_num. +have Gh : G h. + split=> //; apply/integrableP; split => //. + under eq_integral do rewrite gee0_abs//. + by rewrite (le_lt_trans (hnu _ measurableT))// ltey_eq 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. + +Section radon_nikodym. +Context d (X : measurableType d) (R : realType). + +Let radon_nikodym_sigma_finite + (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 (mE j) (Efin j)]. +have H1 i : nu (E i) < +oo by rewrite ltey_eq fin_num_measure. +pose nu_ j : {finite_measure set X -> \bar R} := + [the {finite_measure set _ -> \bar _} of mfrestr (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 (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 fRN_ge0 k x : 0 <= f_ k x by rewrite /f_; case: ifP. +have mf_ k : measurable_fun setT (f_ k). + apply: measurable_fun_if => //. + - by apply: (measurable_fun_bool true); rewrite preimage_mem_true. + - rewrite preimage_mem_true. + by apply: measurable_funTS => //; exact/(measurable_int (integrable_g k)). +have int_f_T k : integrable mu setT (f_ k). + apply/integrableP; 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 /mrestr setIidl. + rewrite -int_gE ?inE//. + under eq_integral. + move=> x /[!inE] /= Ekx; rewrite ifF; last by rewrite memNset. + over. + by rewrite integral0 ?adde0 ltey_eq 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. + move=> A mA; rewrite subsetI => -[_ ?]; rewrite /mu_ /=. + by rewrite /mfrestr /mrestr 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 /mrestr -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. + apply/integrableP; split; first exact: ge0_emeasurable_fun_sum. + under eq_integral do (rewrite gee0_abs; last exact: nneseries_ge0). + by rewrite int_f_nuT ltey_eq fin_num_measure. +move=> A /[!inE] mA; rewrite integral_nneseries//; last first. + by move=> n; exact: measurable_funTS. +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 [fp intfp fpE] := @radon_nikodym_sigma_finite mu + [the {finite_measure set _ -> \bar _} of jordan_pos nuPN] + (jordan_pos_dominates nuPN nu_mu). +have [fn intfn fnE] := @radon_nikodym_sigma_finite mu + [the {finite_measure set _ -> \bar _} of jordan_neg nuPN] + (jordan_neg_dominates nuPN nu_mu). +exists (fp \- fn); first exact: integrableB. +move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//. +- by rewrite -fpE ?inE// -fnE ?inE. +- exact: (integrableS measurableT). +- exact: (integrableS measurableT). +Qed. + +End radon_nikodym. diff --git a/theories/itv.v b/theories/itv.v index 73b3530e8c..2603bc6118 100644 --- a/theories/itv.v +++ b/theories/itv.v @@ -1,8 +1,8 @@ (* mathcomp analysis (c) 2017 Inria and AIST. License: CeCILL-C. *) From Coq Require Import ssreflect ssrfun ssrbool. From mathcomp Require Import ssrnat eqtype choice order ssralg ssrnum ssrint. -From mathcomp.classical Require Import boolp mathcomp_extra. From mathcomp Require Import interval. +From mathcomp.classical Require Import boolp mathcomp_extra. Require Import signed. (******************************************************************************) diff --git a/theories/measure.v b/theories/measure.v index 137b01b5fc..dc480802ea 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -140,6 +140,44 @@ From HB Require Import structures. (* trivIset_closed G == the set of sets G is closed under pairwise-disjoint *) (* countable union *) (* *) +(* * Hierarchy of s-finite, sigma-finite, finite measures: *) +(* sfinite_measure == 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 *) +(* sfinite_measure_seq mu == the sequence of finite measures of the *) +(* s-finite measure mu *) +(* *) +(* sigma_finite A f == the measure function f is sigma-finite on the set *) +(* 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 *) +(* SigmaFinite_isFinite == mixin for finite measures *) +(* FiniteMeasure == structure of finite measures *) +(* Measure_isFinite == factory for finite measures *) +(* *) +(* mfrestr mD muDoo == finite measure corresponding to the restriction of *) +(* the measure mu over D with mu D < +oo, *) +(* mD : measurable D, muDoo : mu D < +oo *) +(* *) +(* 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 *) +(* *) (* monotone_class D G == G is a monotone class of subsets of D *) (* <> == monotone class generated by G on D *) (* <> := <> *) @@ -188,6 +226,8 @@ From HB Require Import structures. (* generated from T1 x T2, with T1 and T2 *) (* measurableType's with resp. display d1 and d2 *) (* *) +(* m1 `<< m2 == m1 is absolutely continuous w.r.t. m2 or m2 dominates m1 *) +(* *) (******************************************************************************) Set Implicit Arguments. @@ -245,6 +285,7 @@ Reserved Notation "[ 'outer_measure' 'of' f ]" Reserved Notation "p .-prod" (at level 1, format "p .-prod"). Reserved Notation "p .-prod.-measurable" (at level 2, format "p .-prod.-measurable"). +Reserved Notation "m1 `<< m2" (at level 51). Inductive measure_display := default_measure_display. Declare Scope measure_display_scope. @@ -2804,6 +2845,30 @@ Qed. End sfinite_measure. +Definition mfrestr d (T : measurableType d) (R : realFieldType) (D : set T) + (f : set T -> \bar R) (mD : measurable D) of f D < +oo := + mrestr f mD. + +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). + +HB.instance Definition _ := Measure.on restr. + +Let restr_fin : fin_num_fun restr. +Proof. +move=> U mU; rewrite /restr /mrestr 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. + HB.mixin Record FiniteMeasure_isSubProbability d (T : measurableType d) (R : realType) (P : set T -> \bar R) := { sprobability_setT : P setT <= 1%E }. @@ -4146,3 +4211,18 @@ End partial_measurable_fun. solve [apply: measurable_pair1] : core. #[global] Hint Extern 0 (measurable_fun _ (pair^~ _)) => solve [apply: measurable_pair2] : core. + +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). diff --git a/theories/radon_nikodym.v b/theories/radon_nikodym.v deleted file mode 100644 index e14fa6ce02..0000000000 --- a/theories/radon_nikodym.v +++ /dev/null @@ -1,1138 +0,0 @@ -(* -*- 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. -From mathcomp.classical Require Import mathcomp_extra boolp classical_sets. -From mathcomp.classical Require Import functions fsbigop cardinality set_interval. -From HB Require Import structures. -Require Import reals ereal signed topology numfun normedtype sequences esum. -Require Import measure realfun 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. - -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 *) -(******************************************************************************) - -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). - -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_decomposition 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). -Variables mu 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// sub1set inE. -exists (fun=> 0); last exact: integral0. -by split => //; [exact: integrable0|move=> E; rewrite integral0]. -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 /[1!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. - by apply: fin_num_fun_lty; 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 first. - by rewrite fine_gt0// muA_gt0/= ltey_eq fin_num_measure. - 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/= ltey_eq 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// ltey_eq 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// ltey_eq 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: (@measurable_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))// ltey_eq 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. - -(* NB: PR in progress *) -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 ltey_eq 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: (@measurable_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 ltey_eq 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 ltey_eq 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 [fp intfp fpE] := @radon_nikodym_sigma_finite_ge0 mu - [the {finite_measure set _ -> \bar _} of jordan_pos nuPN] - (jordan_pos_dominates nuPN nu_mu). -have [fn intfn fnE] := @radon_nikodym_sigma_finite_ge0 mu - [the {finite_measure set _ -> \bar _} of (jordan_neg nuPN)] - (jordan_neg_dominates nuPN nu_mu). -exists (fp \- fn); first exact: integrableB. -move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//. -- by rewrite -fpE ?inE// -fnE ?inE. -- exact: (integrableS measurableT). -- exact: (integrableS measurableT). -Qed. - -End radon_nikodym. From efcd718aaa6047b73b50d2b006932138f103e2fc Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 28 Apr 2023 12:28:07 +0900 Subject: [PATCH 03/11] fix --- theories/charge.v | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/theories/charge.v b/theories/charge.v index 4782eb2190..38fd8ee57a 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1543,7 +1543,8 @@ 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 (@eq_eseriesl _ _ (fun x => x \in [set: nat])); last first. + by move=> x; rewrite in_setT. rewrite -measure_bigcup//. - by rewrite -setI_bigcupr bigcupE setIT. - by move=> i _; exact: measurableI. From 0b4b88488d0a8a1a513293d99730b930fefe1fd8 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 17 May 2023 13:34:08 +0900 Subject: [PATCH 04/11] fix --- theories/charge.v | 35 ----------------------------------- 1 file changed, 35 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index 38fd8ee57a..ee68269580 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -852,41 +852,6 @@ Qed. End jordan_decomposition. -Section PR_in_progress. - -Lemma set_eq_le d (rT : porderType d) T (f g : T -> rT) : - [set x | f x = g x] = [set x | (f x <= g x)%O] `&` [set x | (f x >= g x)%O]. -Proof. by apply/seteqP; split => [x/= ->//|x /andP]; rewrite -eq_le =>/eqP. Qed. - -Local Open Scope ereal_scope. -Context d (T : measurableType d) (R : realType). - -Lemma emeasurable_fun_lt (D : set T) (mD : measurable D) (f g : T -> \bar R) : - measurable_fun D f -> measurable_fun D g -> - measurable (D `&` [set x | f x < g x]). -Proof. -move=> mf mg; under eq_set do rewrite -sube_gt0. -by apply: emeasurable_fun_o_infty => //; exact: emeasurable_funB. -Qed. - -Lemma emeasurable_fun_le (D : set T) (mD : measurable D) (f g : T -> \bar R) : - measurable_fun D f -> measurable_fun D g -> - measurable (D `&` [set x | f x <= g x]). -Proof. -move=> mf mg; under eq_set do rewrite -sube_le0. -by apply: emeasurable_fun_infty_c => //; exact: emeasurable_funB. -Qed. - -Lemma emeasurable_fun_eq (D : set T) (mD : measurable D) (f g : T -> \bar R) : - measurable_fun D f -> measurable_fun D g -> - measurable (D `&` [set x | f x = g x]). -Proof. -move=> mf mg; rewrite set_eq_le setIIr. -by apply: measurableI; apply: emeasurable_fun_le. -Qed. - -End PR_in_progress. - (* We put definitions and lemmas used only in the proof of the Radon-Nikodym theorem as Definition's and Lemma's in the following modules. See https://staff.aist.go.jp/reynald.affeldt/documents/measure-ppl2023.pdf From c71aa74852cd8dc80105bbfc807350fa05e60c6c Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 20 May 2023 17:09:55 +0900 Subject: [PATCH 05/11] fix --- theories/charge.v | 82 +++++++++++++++++++++++------------------------ 1 file changed, 41 insertions(+), 41 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index ee68269580..51cfeae5e0 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -151,7 +151,7 @@ Qed. Lemma charge_partition nu S P N : measurable S -> measurable P -> measurable N -> - P `|` N = setT -> P `&` N = set0 -> nu S = nu (S `&` P) + nu (S `&` N). + P `|` N = [set: T] -> P `&` N = set0 -> nu S = nu (S `&` P) + nu (S `&` N). Proof. move=> mS mP mN PNT PN0; rewrite -{1}(setIT S) -PNT setIUr chargeU//. - exact: measurableI. @@ -601,7 +601,7 @@ End hahn_decomposition_lemma. Definition hahn_decomposition 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]. + [/\ positive_set nu P, negative_set nu N, P `|` N = [set: T] & P `&` N = set0]. Section hahn_decomposition_theorem. Context d (T : measurableType d) (R : realType). @@ -768,15 +768,15 @@ Qed. End hahn_decomposition_theorem. Section jordan_decomposition. -Context d (X : measurableType d) (R : realType). -Variable nu : {charge set X -> \bar R}. -Variables (P N : set X) (nuPN : hahn_decomposition nu P N). +Context d (T : measurableType d) (R : realType). +Variable nu : {charge set T -> \bar R}. +Variables (P N : set T) (nuPN : hahn_decomposition nu P N). Let mP : measurable P. Proof. by have [[mP _] _ _ _] := nuPN. Qed. Let mN : measurable N. Proof. by have [_ [mN _] _ _] := nuPN. Qed. -Let cjordan_pos : {charge set X -> \bar R} := +Let cjordan_pos : {charge set T -> \bar R} := [the charge _ _ of crestr0 nu mP]. Let positive_set_cjordan_pos E : 0 <= cjordan_pos E. @@ -796,7 +796,7 @@ Proof. by move=> U mU; rewrite fin_num_measure. Qed. HB.instance Definition _ := @Measure_isFinite.Build _ _ _ jordan_pos finite_jordan_pos. -Let cjordan_neg : {charge set X -> \bar R} := +Let cjordan_neg : {charge set T -> \bar R} := [the charge _ _ of cscale (-1) [the charge _ _ of crestr0 nu mN]]. Let positive_set_cjordan_neg E : 0 <= cjordan_neg E. @@ -827,7 +827,7 @@ case: nuPN => _ _ <- PN0; rewrite setIUr chargeU//. - by rewrite setIACA PN0 setI0. Qed. -Lemma jordan_pos_dominates (mu : {measure set X -> \bar R}) : +Lemma jordan_pos_dominates (mu : {measure set T -> \bar R}) : nu `<< mu -> jordan_pos `<< mu. Proof. move=> nu_mu A mA muA0; have := nu_mu A mA muA0. @@ -838,7 +838,7 @@ suff : mu (A `&` P) = 0 by move/(nu_mu _ mAP); rewrite /crestr => ->. by apply/eqP; rewrite eq_le measure_ge0// andbT -muA0 le_measure// inE. Qed. -Lemma jordan_neg_dominates (mu : {measure set X -> \bar R}) : +Lemma jordan_neg_dominates (mu : {measure set T -> \bar R}) : nu `<< mu -> jordan_neg `<< mu. Proof. move=> nu_mu A mA muA0; have := nu_mu A mA muA0. @@ -858,11 +858,11 @@ End jordan_decomposition. for an overview. *) Module approxRN. Section approxRN. -Context d (X : measurableType d) (R : realType). -Variables mu nu : {measure set X -> \bar R}. +Context d (T : measurableType d) (R : realType). +Variables mu nu : {measure set T -> \bar R}. -Definition approxRN := [set g : X -> \bar R | [/\ - forall x, 0 <= g x, mu.-integrable setT g & +Definition approxRN := [set g : T -> \bar R | [/\ + forall x, 0 <= g x, mu.-integrable [set: T] g & forall E, measurable E -> \int[mu]_(x in E) g x <= nu E] ]. Let approxRN_neq0 : approxRN !=set0. @@ -887,9 +887,9 @@ End approxRN. Module approxRN_seq. Section approxRN_seq. -Context d (X : measurableType d) (R : realType). -Variable mu : {measure set X -> \bar R}. -Variable nu : {finite_measure set X -> \bar R}. +Context d (T : measurableType d) (R : realType). +Variable mu : {measure set T -> \bar R}. +Variable nu : {finite_measure set T -> \bar R}. Import approxRN. @@ -916,11 +916,11 @@ 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 | +Lemma approxRN_seq_ex : { g : (T -> \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. +suff : { g : (T -> \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. @@ -929,7 +929,7 @@ 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. +Definition approxRN_seq : (T -> \bar R)^nat := sval approxRN_seq_ex. Let g_ := approxRN_seq. @@ -947,7 +947,7 @@ Definition max_approxRN_seq n x := \big[maxe/-oo]_(j < n.+1) g_ j x. Let F_ := max_approxRN_seq. -Lemma measurable_max_approxRN_seq n : measurable_fun setT (F_ n). +Lemma measurable_max_approxRN_seq n : measurable_fun [set: T] (F_ n). Proof. elim: n => [|n ih]. rewrite /F_ /max_approxRN_seq. @@ -996,7 +996,7 @@ 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). +Lemma trivIset_is_max_approxRN n : trivIset [set: nat] (E n). Proof. apply/trivIsetP => /= i j _ _ ij. apply/seteqP; split => // x []; rewrite /E/= => -[+ + [+ +]]. @@ -1007,7 +1007,7 @@ wlog : i j ij / (i < j)%N. by move=> {}ij Fmgi h Fmgj => /(_ _ ij); rewrite -Fmgi -Fmgj ltxx. Qed. -Lemma bigsetU_is_max_approxRN m : \big[setU/set0]_(j < m.+1) E m j = [set: X]. +Lemma bigsetU_is_max_approxRN m : \big[setU/set0]_(j < m.+1) E m j = [set: T]. Proof. apply/seteqP; split => // x _; rewrite -bigcup_mkord. pose j := [arg max_(j > @ord0 m) g_ j x]%O. @@ -1048,8 +1048,8 @@ End approxRN_seq. Module lim_max_approxRN_seq. Section lim_max_approxRN_seq. -Context d (X : measurableType d) (R : realType). -Variables mu nu : {finite_measure set X -> \bar R}. +Context d (T : measurableType d) (R : realType). +Variables mu nu : {finite_measure set T -> \bar R}. Import approxRN. @@ -1063,7 +1063,7 @@ Let F := max_approxRN_seq mu nu. Definition fRN := fun x => lim (F ^~ x). -Lemma measurable_fun_fRN : measurable_fun setT fRN. +Lemma measurable_fun_fRN : measurable_fun [set: T] fRN. Proof. rewrite (_ : fRN = fun x => lim_esup (F ^~ x)). by apply: measurable_fun_lim_esup => // n; exact: measurable_max_approxRN_seq. @@ -1318,8 +1318,8 @@ End lim_max_approxRN_seq. End lim_max_approxRN_seq. Section radon_nikodym_finite. -Context d (X : measurableType d) (R : realType). -Variables mu nu : {finite_measure set X -> \bar R}. +Context d (T : measurableType d) (R : realType). +Variables mu nu : {finite_measure set T -> \bar R}. Import approxRN. @@ -1332,8 +1332,8 @@ Let f := fRN mu nu. Let mf := measurable_fun_fRN. Let f_ge0 := fRN_ge0. -Lemma radon_nikodym_finite : nu `<< mu -> exists f : X -> \bar R, - [/\ forall x, f x >= 0, mu.-integrable setT f & +Lemma radon_nikodym_finite : nu `<< mu -> exists f : T -> \bar R, + [/\ forall x, f x >= 0, mu.-integrable [set: T] f & forall E, measurable E -> nu E = \int[mu]_(x in E) f x]. Proof. move=> nu_mu; exists f; split. @@ -1341,8 +1341,8 @@ move=> nu_mu; exists f; split. - by apply/integrableP; split; [exact: mf|exact: int_fRN_lty]. move=> // A mA. apply/eqP; rewrite eq_le int_fRN_ub// andbT leNgt; apply/negP => abs. -pose sigma : {charge set X -> \bar R} := - [the {charge set X -> \bar R} of sigmaRN mA abs]. +pose sigma : {charge set T -> \bar R} := + [the {charge set T -> \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. @@ -1423,13 +1423,13 @@ Qed. End radon_nikodym_finite. Section radon_nikodym. -Context d (X : measurableType d) (R : realType). +Context d (T : measurableType d) (R : realType). Let radon_nikodym_sigma_finite - (mu : {sigma_finite_measure set X -> \bar R}) - (nu : {finite_measure set X -> \bar R}) : + (mu : {sigma_finite_measure set T -> \bar R}) + (nu : {finite_measure set T -> \bar R}) : nu `<< mu -> - exists2 f : X -> \bar R, mu.-integrable setT f & + exists2 f : T -> \bar R, mu.-integrable [set: T] f & forall E, E \in measurable -> nu E = integral mu E f. Proof. move=> nu_mu. @@ -1442,10 +1442,10 @@ 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} := +pose mu_ j : {finite_measure set T -> \bar R} := [the {finite_measure set _ -> \bar _} of mfrestr (mE j) (Efin j)]. have H1 i : nu (E i) < +oo by rewrite ltey_eq fin_num_measure. -pose nu_ j : {finite_measure set X -> \bar R} := +pose nu_ j : {finite_measure set T -> \bar R} := [the {finite_measure set _ -> \bar _} of mfrestr (mE j) (H1 j)]. have nu_mu_ k : nu_ k `<< mu_ k. by move=> S mS mu_kS0; apply: nu_mu => //; exact: measurableI. @@ -1457,9 +1457,9 @@ have mf_ k : measurable_fun setT (f_ k). apply: measurable_fun_if => //. - by apply: (measurable_fun_bool true); rewrite preimage_mem_true. - rewrite preimage_mem_true. - by apply: measurable_funTS => //; exact/(measurable_int (integrable_g k)). + by apply: measurable_funTS => //; have /integrableP[] := integrable_g k. have int_f_T k : integrable mu setT (f_ k). - apply/integrableP; split=> //. + apply/integrableP; split => //. under eq_integral do rewrite gee0_abs//. rewrite -(setUv (E k)) integral_setU //; last 3 first. - exact: measurableC. @@ -1517,9 +1517,9 @@ rewrite -measure_bigcup//. Qed. Theorem Radon_Nikodym - (mu : {sigma_finite_measure set X -> \bar R}) (nu : {charge set X -> \bar R}) : + (mu : {sigma_finite_measure set T -> \bar R}) (nu : {charge set T -> \bar R}) : nu `<< mu -> - exists2 f : X -> \bar R, mu.-integrable setT f & + exists2 f : T -> \bar R, mu.-integrable [set: T] 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. From 520c047882b8afeeae12ed5ad15dea6b20101caf Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 21 May 2023 22:55:43 +0900 Subject: [PATCH 06/11] fix to compile with 8.14+1.14.0 --- theories/charge.v | 8 +++----- 1 file changed, 3 insertions(+), 5 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index 51cfeae5e0..a4c0fc8244 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1348,7 +1348,7 @@ 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 //. + 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//. @@ -1363,13 +1363,11 @@ have mh : measurable_fun setT h. - by apply: measurable_funTS; apply: emeasurable_funD => //; exact: mf. - by apply: measurable_funTS; exact: mf. have hge0 x : 0 <= h x. - rewrite /h; case: ifPn; last by move=> ?; exact: f_ge0. - by move=> _; rewrite adde_ge0//; exact: f_ge0. + by rewrite /h; case: ifPn => [_|?]; [rewrite adde_ge0// f_ge0|exact: f_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. + by apply: posP => //; 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. From 54ba33b0b75561a61328bcbae7ba85bf202c023b Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Fri, 2 Jun 2023 11:56:34 +0900 Subject: [PATCH 07/11] simplification by Zachary Co-authored-by: Zachary Stone --- theories/charge.v | 28 +++++----------------------- 1 file changed, 5 insertions(+), 23 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index a4c0fc8244..fbc0a5aaf8 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -1283,29 +1283,11 @@ apply: cvgeB. apply: is_cvg_ereal_nneg_natsum => n _. by apply: integral_ge0 => x _; rewrite adde_ge0//; exact: fRN_ge0. by rewrite (@cvg_lim _ _ _ _ _ _ l). - + apply/integrableP; split. - suff: measurable_fun setT (fun x => fRN x + epsRN%:num%:E). - exact: measurable_funS. - by apply: emeasurable_funD => //; exact: measurable_fun_fRN. - apply: (@le_lt_trans _ _ (\int[mu]_(x in \bigcup_k H k) `|fRN x| + - \int[mu]_(x in \bigcup_k H k)`| epsRN%:num%:E |)). - rewrite -(integralD mUH); last 2 first. - * apply/integrable_abse/integrableP; split. - exact: measurable_funS measurable_fun_fRN. - rewrite (le_lt_trans _ int_fRN_lty)// subset_integral//. - by apply: measurableT_comp => //; exact: measurable_fun_fRN. - * apply/integrable_abse/integrableP; split => //. - by rewrite integral_cst//= lte_mul_pinfty// ltey_eq fin_num_measure. - apply: ge0_le_integral => //. - * apply: measurableT_comp => //; apply: emeasurable_funD => //. - exact: measurable_funS measurable_fun_fRN. - * apply: emeasurable_funD => //; apply: measurableT_comp => //. - exact: measurable_funS measurable_fun_fRN. - * by move=> x _; exact: lee_abs_add. - apply: lte_add_pinfty. - rewrite (le_lt_trans _ int_fRN_lty)// subset_integral//. - by apply: measurableT_comp => //; exact: measurable_fun_fRN. - by rewrite integral_cst//= lte_mul_pinfty// ltey_eq fin_num_measure. + + apply: integrableD => //=. + * apply: (integrableS measurableT) => //. + by apply/integrableP; split; [exact: measurable_fun_fRN|exact: int_fRN_lty]. + * apply/integrableP; split => //. + by rewrite integral_cst// lte_mul_pinfty// ltey_eq fin_num_measure. + by move=> x _; rewrite adde_ge0//; exact: fRN_ge0. Qed. From 405fd3abed8d11ac37e2f0ee88a4f7810ecfd3f7 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 7 Jun 2023 17:19:58 +0900 Subject: [PATCH 08/11] add a definition of RN derivative - add notation Co-authored-by: IshiguroYoshihiro --- CHANGELOG_UNRELEASED.md | 4 +++- theories/charge.v | 43 ++++++++++++++++++++++++++++++++++++++--- 2 files changed, 43 insertions(+), 4 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 1da54bc246..78964a98ec 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -76,7 +76,9 @@ + definition `crestr0` + definitions `jordan_neg`, `jordan_pos` + lemmas `jordan_decomp`, `jordan_pos_dominates`, `jordan_neg_dominates` - + lemma `radon_nikodym_finite`, theorem `Radon_Nikodym` + + lemma `radon_nikodym_finite` + + definition `Radon_Nikodym`, notation `'d nu /d mu` + + theorems `Radon_Nikodym_integrable`, `Radon_Nikodym_integral` - in `measure.v`: + lemmas `measurable_pair1`, `measurable_pair2` diff --git a/theories/charge.v b/theories/charge.v index fbc0a5aaf8..c23094cdb5 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -39,6 +39,8 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* jordan_neg nu nuPN == the charge obtained by restricting the charge *) (* nu to the positive set N of the Hahn *) (* decomposition nuPN: hahn_decomposition nu P N *) +(* 'd nu /d mu == Radon-Nikodym derivative of nu w.r.t. mu *) +(* (the scope is charge_scope) *) (* *) (******************************************************************************) @@ -48,10 +50,14 @@ Reserved Notation "{ 'additive_charge' 'set' T '->' '\bar' R }" Reserved Notation "{ 'charge' 'set' T '->' '\bar' R }" (at level 36, T, R at next level, format "{ 'charge' 'set' T '->' '\bar' R }"). +Reserved Notation "'d nu /d mu" (at level 10, format "''d' nu /d mu"). + +Declare Scope charge_scope. Set Implicit Arguments. Unset Strict Implicit. Unset Printing Implicit Defensive. + Import Order.TTheory GRing.Theory Num.Def Num.Theory. Import numFieldTopology.Exports. @@ -82,7 +88,7 @@ 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) : ring_scope. + (additive_charge T R) : ring_scope. #[export] Hint Resolve charge_semi_additive : core. @@ -1496,11 +1502,11 @@ rewrite -measure_bigcup//. - exact: trivIset_setIl. Qed. -Theorem Radon_Nikodym +Let Radon_Nikodym0 (mu : {sigma_finite_measure set T -> \bar R}) (nu : {charge set T -> \bar R}) : nu `<< mu -> exists2 f : T -> \bar R, mu.-integrable [set: T] f & - forall E, measurable E -> nu E = \int[mu]_(x in E) f x. + forall A, measurable A -> nu A = \int[mu]_(x in A) f x. Proof. move=> nu_mu; have [P [N nuPN]] := Hahn_decomposition nu. have [fp intfp fpE] := @radon_nikodym_sigma_finite mu @@ -1516,4 +1522,35 @@ move=> E mE; rewrite [LHS](jordan_decomp nuPN mE)// integralB//. - exact: (integrableS measurableT). Qed. +Definition Radon_Nikodym + (mu : {sigma_finite_measure set T -> \bar R}) + (nu : {charge set T -> \bar R}) : T -> \bar R := + match pselect (nu `<< mu) with + | left nu_mu => sval (cid2 (Radon_Nikodym0 nu_mu)) + | right _ => cst -oo + end. + +Local Notation "'d nu /d mu" := (Radon_Nikodym mu nu). + +Theorem Radon_Nikodym_integrable + (mu : {sigma_finite_measure set T -> \bar R}) + (nu : {charge set T -> \bar R}) : + nu `<< mu -> + mu.-integrable [set: T] ('d nu /d mu). +Proof. +move=> numu; rewrite /Radon_Nikodym; case: pselect => // {}numu. +by case: cid2. +Qed. + +Theorem Radon_Nikodym_integral + (mu : {sigma_finite_measure set T -> \bar R}) + (nu : {charge set T -> \bar R}) : + nu `<< mu -> + forall A, measurable A -> nu A = \int[mu]_(x in A) ('d nu /d mu) x. +Proof. +move=> numu; rewrite /Radon_Nikodym; case: pselect => // {}numu. +by case: cid2. +Qed. + End radon_nikodym. +Notation "'d nu /d mu" := (Radon_Nikodym mu nu) : charge_scope. From c6dfc9a0a21a1b949bab07428af4e8c9e41c11b8 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 7 Jun 2023 17:42:11 +0900 Subject: [PATCH 09/11] fix format --- theories/charge.v | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/theories/charge.v b/theories/charge.v index c23094cdb5..46110fa110 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -50,7 +50,7 @@ Reserved Notation "{ 'additive_charge' 'set' T '->' '\bar' R }" Reserved Notation "{ 'charge' 'set' T '->' '\bar' R }" (at level 36, T, R at next level, format "{ 'charge' 'set' T '->' '\bar' R }"). -Reserved Notation "'d nu /d mu" (at level 10, format "''d' nu /d mu"). +Reserved Notation "'d nu /d mu" (at level 10, format "''d' nu /d mu"). Declare Scope charge_scope. From bdcce060bc3ca89a777e09eab1e86a1f334e7edb Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 7 Jun 2023 18:10:02 +0900 Subject: [PATCH 10/11] dominates -> measure_dominates --- CHANGELOG_UNRELEASED.md | 4 ++-- theories/measure.v | 8 ++++---- 2 files changed, 6 insertions(+), 6 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 78964a98ec..76bd876df2 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -67,8 +67,8 @@ - in `classical_sets.v`: + lemmas `preimage_mem_true`, `preimage_mem_false` - in `measure.v`: - + definition `dominates`, notation `` `<< `` - + lemma `dominates_trans` + + definition `measure_dominates`, notation `` `<< `` + + lemma `measure_dominates_trans` - in `measure.v`: + defintion `mfrestr` - in `charge.v`: diff --git a/theories/measure.v b/theories/measure.v index dc480802ea..c1cdd33af9 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -4216,13 +4216,13 @@ Section absolute_continuity. Context d (T : measurableType d) (R : realType). Implicit Types m : set T -> \bar R. -Definition dominates m1 m2 := +Definition measure_dominates m1 m2 := forall A, measurable A -> m2 A = 0 -> m1 A = 0. -Local Notation "m1 `<< m2" := (dominates m1 m2). +Local Notation "m1 `<< m2" := (measure_dominates m1 m2). -Lemma dominates_trans m1 m2 m3 : m1 `<< m2 -> m2 `<< m3 -> m1 `<< m3. +Lemma measure_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). +Notation "m1 `<< m2" := (measure_dominates m1 m2). From b4c611bc329a956acb362465e44121bc9f84a236 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Wed, 7 Jun 2023 20:57:47 +0900 Subject: [PATCH 11/11] for compilation with coq < 8.17 --- CHANGELOG_UNRELEASED.md | 2 +- theories/charge.v | 13 +++++++------ 2 files changed, 8 insertions(+), 7 deletions(-) diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 76bd876df2..611ce3f834 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -77,7 +77,7 @@ + definitions `jordan_neg`, `jordan_pos` + lemmas `jordan_decomp`, `jordan_pos_dominates`, `jordan_neg_dominates` + lemma `radon_nikodym_finite` - + definition `Radon_Nikodym`, notation `'d nu /d mu` + + definition `Radon_Nikodym`, notation `'d nu '/d mu` + theorems `Radon_Nikodym_integrable`, `Radon_Nikodym_integral` - in `measure.v`: diff --git a/theories/charge.v b/theories/charge.v index 46110fa110..701ccc14ba 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -39,7 +39,7 @@ Require Import esum measure realfun lebesgue_measure lebesgue_integral. (* jordan_neg nu nuPN == the charge obtained by restricting the charge *) (* nu to the positive set N of the Hahn *) (* decomposition nuPN: hahn_decomposition nu P N *) -(* 'd nu /d mu == Radon-Nikodym derivative of nu w.r.t. mu *) +(* 'd nu '/d mu == Radon-Nikodym derivative of nu w.r.t. mu *) (* (the scope is charge_scope) *) (* *) (******************************************************************************) @@ -50,7 +50,8 @@ Reserved Notation "{ 'additive_charge' 'set' T '->' '\bar' R }" Reserved Notation "{ 'charge' 'set' T '->' '\bar' R }" (at level 36, T, R at next level, format "{ 'charge' 'set' T '->' '\bar' R }"). -Reserved Notation "'d nu /d mu" (at level 10, format "''d' nu /d mu"). +Reserved Notation "'d nu '/d mu" (at level 10, nu, mu at next level, + format "''d' nu ''/d' mu"). Declare Scope charge_scope. @@ -1530,13 +1531,13 @@ Definition Radon_Nikodym | right _ => cst -oo end. -Local Notation "'d nu /d mu" := (Radon_Nikodym mu nu). +Local Notation "'d nu '/d mu" := (Radon_Nikodym mu nu). Theorem Radon_Nikodym_integrable (mu : {sigma_finite_measure set T -> \bar R}) (nu : {charge set T -> \bar R}) : nu `<< mu -> - mu.-integrable [set: T] ('d nu /d mu). + mu.-integrable [set: T] ('d nu '/d mu). Proof. move=> numu; rewrite /Radon_Nikodym; case: pselect => // {}numu. by case: cid2. @@ -1546,11 +1547,11 @@ Theorem Radon_Nikodym_integral (mu : {sigma_finite_measure set T -> \bar R}) (nu : {charge set T -> \bar R}) : nu `<< mu -> - forall A, measurable A -> nu A = \int[mu]_(x in A) ('d nu /d mu) x. + forall A, measurable A -> nu A = \int[mu]_(x in A) ('d nu '/d mu) x. Proof. move=> numu; rewrite /Radon_Nikodym; case: pselect => // {}numu. by case: cid2. Qed. End radon_nikodym. -Notation "'d nu /d mu" := (Radon_Nikodym mu nu) : charge_scope. +Notation "'d nu '/d mu" := (Radon_Nikodym mu nu) : charge_scope.