From 0133478bfdf04c93f41a8dde6ec5989e9b16ec02 Mon Sep 17 00:00:00 2001 From: IshiguroYoshihiro Date: Tue, 14 Nov 2023 16:40:50 +0900 Subject: [PATCH] fix --- theories/charge.v | 16 ++++++++++------ 1 file changed, 10 insertions(+), 6 deletions(-) diff --git a/theories/charge.v b/theories/charge.v index 983be76de0..c9d061df0f 100644 --- a/theories/charge.v +++ b/theories/charge.v @@ -479,10 +479,13 @@ HB.instance Definition _ := isCharge.Build _ _ _ End pushforward_charge. HB.builders Context d (T : measurableType d) (R : realType) - mu of Measure_isFinite d T R mu. + (mu : set T -> \bar R) of Measure_isFinite d T R mu. + +Let mu0 : mu set0 = 0. +Proof. by apply: measure0. Qed. HB.instance Definition _ := isCharge.Build _ _ _ - mu (measure0 mu) fin_num_measure measure_semi_sigma_additive. + mu mu0 fin_num_measure measure_semi_sigma_additive. HB.end. @@ -970,7 +973,8 @@ HB.instance Definition _ := @Measure_isFinite.Build _ _ _ jordan_neg finite_jordan_neg. Lemma jordan_decomp (A : set T) (mA : measurable A) : - nu A = (cadd jordan_pos (cscale (-1) jordan_neg)) A. + nu A = (cadd [the charge _ _ of jordan_pos] + ([the charge _ _ of cscale (-1) [the charge _ _ of jordan_neg]])) A. Proof. rewrite caddE cjordan_posE /= cscaleE EFinN mulN1e cjordan_negE oppeK. rewrite /crestr0 mem_set// -[in LHS](setIT A). @@ -1915,7 +1919,7 @@ Hypothesis numu : nu `<< mu. Lemma ae_eq_Radon_Nikodym_SigmaFinite E : measurable E -> ae_eq mu E (Radon_Nikodym_SigmaFinite.f nu mu) - ('d (charge_of_finite_measure nu) '/d mu). + ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu). Proof. move=> mE; apply: integral_ae_eq => //. - apply: (integrableS measurableT) => //. @@ -1936,7 +1940,7 @@ Implicit Types f : T -> \bar R. Lemma Radon_Nikodym_change_of_variables f E : measurable E -> nu.-integrable E f -> - \int[mu]_(x in E) (f x * ('d (charge_of_finite_measure nu) '/d mu) x) = + \int[mu]_(x in E) (f x * ('d [the charge _ _ of charge_of_finite_measure nu] '/d mu) x) = \int[nu]_(x in E) f x. Proof. move=> mE mf; rewrite [in RHS](funeposneg f) integralB //; last 2 first. @@ -2013,7 +2017,7 @@ Variables (nu : {charge set T -> \bar R}) Lemma Radon_Nikodym_chain_rule : nu `<< mu -> mu `<< la -> ae_eq la setT ('d nu '/d la) - ('d nu '/d mu \* 'd (charge_of_finite_measure mu) '/d la). + ('d nu '/d mu \* 'd [the charge _ _ of charge_of_finite_measure mu] '/d la). Proof. have [Pnu [Nnu nuPN]] := Hahn_decomposition nu. move=> numu mula; have nula := measure_dominates_trans numu mula.