From 31bc05c8b6e27b559138e10f087653db5b6fd6de Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sat, 25 Feb 2023 18:32:52 +0900 Subject: [PATCH] upd --- theories/lebesgue_stieltjes_measure.v | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index a6315b5654..825cfcef27 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -376,7 +376,7 @@ by rewrite -(hlength0 f) le_hlength//; exact: cumulative_is_nondecreasing. Qed. HB.instance Definition _ (f : cumulative R) := - isAdditiveMeasure.Build _ R _ (hlength f : set ocitv_type -> _) + isContent.Build _ _ R (hlength f : set ocitv_type -> _) (hlength_ge0' f) (hlength_semi_additive f). Lemma hlength_content_sub_fsum (f : cumulative R) (D : {fset nat}) a0 b0 @@ -393,7 +393,7 @@ have mab k : [set` D] k -> @measurable d itvs_semiRingOfSets `]a k, b k]%classic by []. move: h; rewrite -bigcup_fset. move/(@content_sub_fsum d R _ - [the additive_measure _ _ of hlength f : set ocitv_type -> _] _ [set` D] + [the content _ _ of hlength f : set ocitv_type -> _] _ [set` D] `]a0, b0]%classic (fun x => `](a x), (b x)]%classic) (finite_fset D) mab (is_ocitv _ _)) => /=. rewrite hlength_itv_bnd// -lee_fin => /le_trans; apply. @@ -414,7 +414,7 @@ wlog wlogh : b A AE lebig / forall n, (b n).1 <= (b n).2. set A' := fun n => if (b n).1 >= (b n).2 then set0 else A n. set b' := fun n => if (b n).1 >= (b n).2 then (0, 0) else b n. rewrite [X in (_ <= X)%E](_ : _ = \sum_(n k. + apply: (@eq_eseriesr _ (hlength f \o A) (hlength f \o A')) => k. rewrite /= /A' AE; case: ifPn => // bn. by rewrite set_itv_ge//= bnd_simp -leNgt. apply (h b'). @@ -476,7 +476,7 @@ Qed. Let gitvs := [the measurableType _ of salgebraType ocitv]. Definition lebesgue_stieltjes_measure (f : cumulative R) := - Hahn_ext [the additive_measure _ _ of hlength f : set ocitv_type -> _ ]. + Hahn_ext [the content _ _ of hlength f : set ocitv_type -> _ ]. Let lebesgue_stieltjes_measure0 (f : cumulative R) : lebesgue_stieltjes_measure f set0 = 0%E.