From 5d39745d9f68fbf32fa2353ec2ac07cdbf5b3dc5 Mon Sep 17 00:00:00 2001 From: Reynald Affeldt Date: Sun, 28 Aug 2022 12:36:10 +0900 Subject: [PATCH] cumulative function with HB Co-authored-by: brun@itu.dk Co-authored-by: Takafumi Saikawa --- theories/lebesgue_stieltjes_measure.v | 154 ++++++++++++++------------ 1 file changed, 81 insertions(+), 73 deletions(-) diff --git a/theories/lebesgue_stieltjes_measure.v b/theories/lebesgue_stieltjes_measure.v index 1b71827aae..665d527f5d 100644 --- a/theories/lebesgue_stieltjes_measure.v +++ b/theories/lebesgue_stieltjes_measure.v @@ -29,21 +29,50 @@ Local Open Scope ring_scope. Notation right_continuous f := (forall x, f%function @ at_right x --> f%function x). -Lemma nondecreasing_right_continuousP (R : realType) (a : R) (e : R) - (f : R -> R) (ndf : {homo f : x y / x <= y}) (rcf : (right_continuous f)) : +Lemma right_continuousW (R : numFieldType) (f : R -> R) : + continuous f -> right_continuous f. +Proof. by move=> cf x; apply: cvg_within_filter; exact/cf. Qed. + +HB.mixin Record isCumulative (R : numFieldType) (f : R -> R) := { + cumulative_is_nondecreasing : {homo f : x y / x <= y} ; + cumulative_is_right_continuous : right_continuous f }. + +#[short(type=cumulative)] +HB.structure Definition Cumulative (R : numFieldType) := + { f of isCumulative R f }. + +Arguments cumulative_is_nondecreasing {R} _. +Arguments cumulative_is_right_continuous {R} _. + +Lemma nondecreasing_right_continuousP (R : numFieldType) (a : R) (e : R) + (f : cumulative R) : e > 0 -> exists d : {posnum R}, f (a + d%:num) <= f a + e. Proof. -move=> e0; move: rcf => /(_ a)/(@cvg_dist _ [normedModType R of R^o]). +move=> e0; move: (cumulative_is_right_continuous f). +move=> /(_ a)/(@cvg_dist _ [normedModType R of R^o]). move=> /(_ _ e0)[] _ /posnumP[d] => h. exists (PosNum [gt0 of (d%:num / 2)]) => //=. move: h => /(_ (a + d%:num / 2)) /=. rewrite opprD addrA subrr distrC subr0 ger0_norm //. rewrite ltr_pdivr_mulr// ltr_pmulr// ltr1n => /(_ erefl). rewrite ltr_addl divr_gt0// => /(_ erefl). -rewrite ler0_norm; last by rewrite subr_le0 ndf// ler_addl. +rewrite ler0_norm; last first. + by rewrite subr_le0 (cumulative_is_nondecreasing f)// ler_addl. by rewrite opprB ltr_subl_addl => fa; exact: ltW. Qed. +Section id_is_cumulative. +Variable R : realType. + +Let id_nd : {homo @idfun R : x y / x <= y}. +Proof. by []. Qed. + +Let id_rc : right_continuous (@idfun R). +Proof. by apply/right_continuousW => x; exact: cvg_id. Qed. + +HB.instance Definition _ := isCumulative.Build R idfun id_nd id_rc. +End id_is_cumulative. + (* TODO: move and use in lebesgue_measure.v? *) Lemma le_inf (R : realType) (S1 S2 : set R) : -%R @` S2 `<=` down (-%R @` S1) -> nonempty S2 -> has_inf S1 @@ -66,8 +95,6 @@ Qed. Section hlength. Local Open Scope ereal_scope. Variables (R : realType) (f : R -> R). -Hypothesis ndf : {homo f : x y / (x <= y)%R}. - Let g : \bar R -> \bar R := EFinf f. Implicit Types i j : interval R. @@ -149,7 +176,7 @@ rewrite hlength_itv; case: i => -[ba a|[]] [bb b|[]] //= => [|_|_|]. - by right. Qed. -Lemma hlength_ge0 i : 0 <= hlength [set` i]. +Lemma hlength_ge0 (ndf : {homo f : x y / (x <= y)%R}) i : 0 <= hlength [set` i]. Proof. rewrite hlength_itv; case: ifPn => //; case: (i.1 : \bar _) => [r| |]. - by rewrite suber_ge0// => /ltW /(nondecreasing_EFinf ndf). @@ -161,7 +188,7 @@ Local Hint Extern 0 (0%:E <= hlength _) => solve[apply: hlength_ge0] : core. Lemma hlength_Rhull (A : set R) : hlength [set` Rhull A] = hlength A. Proof. by rewrite /hlength Rhull_involutive. Qed. -Lemma le_hlength_itv i j : +Lemma le_hlength_itv (ndf : {homo f : x y / (x <= y)%R}) i j : {subset i <= j} -> hlength [set` i] <= hlength [set` j]. Proof. set I := [set` i]; set J := [set` j]. @@ -183,9 +210,10 @@ move=> r [r' Ir' <-{r}]; exists (- r')%R. by split => //; exists r' => //; apply: ij. Qed. -Lemma le_hlength : {homo hlength : A B / A `<=` B >-> A <= B}. +Lemma le_hlength (ndf : {homo f : x y / (x <= y)%R}) : + {homo hlength : A B / A `<=` B >-> A <= B}. Proof. -move=> a b /le_Rhull /le_hlength_itv. +move=> a b /le_Rhull /(le_hlength_itv ndf). by rewrite (hlength_Rhull a) (hlength_Rhull b). Qed. @@ -208,7 +236,8 @@ Lemma ocitv0 : ocitv set0. Proof. by exists (1, 0); rewrite //= set_itv_ge ?bnd_simp//= ltr10. Qed. Hint Resolve ocitv0 : core. -Lemma ocitvP X : ocitv X <-> X = set0 \/ exists2 x, x.1 < x.2 & X = `]x.1, x.2]%classic. +Lemma ocitvP X : + ocitv X <-> X = set0 \/ exists2 x, x.1 < x.2 & X = `]x.1, x.2]%classic. Proof. split=> [[x _ <-]|[->//|[x xlt ->]]]//. case: (boolP (x.1 < x.2)) => x12; first by right; exists x. @@ -252,14 +281,13 @@ Qed. Variable d : measure_display. -HB.instance Definition _ := - @isSemiRingOfSets.Build d ocitv_type (Pointed.class R) ocitv ocitv0 ocitvI ocitvD. +HB.instance Definition _ := @isSemiRingOfSets.Build d ocitv_type + (Pointed.class R) ocitv ocitv0 ocitvI ocitvD. Definition itvs_semiRingOfSets := [the semiRingOfSetsType d of ocitv_type]. -Variable f : R -> R. - -Lemma hlength_semi_additive : semi_additive (hlength f : set ocitv_type -> _). +Lemma hlength_semi_additive (f : R -> R) : + semi_additive (hlength f : set ocitv_type -> _). Proof. move=> /= I n /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym-/funext {I}->. move=> Itriv [[/= a1 a2] _] /esym /[dup] + ->. @@ -326,7 +354,8 @@ Qed. Hint Extern 0 (measurable _) => solve [apply: is_ocitv] : core. -Lemma hlength_sigma_finite : sigma_finite [set: ocitv_type] (hlength f). +Lemma hlength_sigma_finite (f : R -> R) : + sigma_finite [set: ocitv_type] (hlength f). Proof. exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic). apply/esym; rewrite -subTset => /= x _ /=. @@ -336,26 +365,30 @@ exists (fun k : nat => `] (- k%:R)%R, k%:R]%classic). rewrite [ltRHS]ger0_norm//. by rewrite (le_lt_trans _ (lt_succ_Rfloor _))// ?ler_norm. by rewrite addr_ge0// -Rfloor0 le_Rfloor. -by move=> k; split => //; rewrite hlength_itv /= -EFinB; case: ifP; rewrite ltey. +move=> k; split => //; rewrite hlength_itv /= -EFinB. +by case: ifP; rewrite ltey. Qed. -Hypothesis ndf : {homo f : x y / (x <= y)%R}. - -Lemma hlength_ge0' (I : set ocitv_type) : (0 <= hlength f I)%E. -Proof. by rewrite -(hlength0 f) le_hlength. Qed. +Lemma hlength_ge0' (f : cumulative R) (I : set ocitv_type) : + (0 <= hlength f I)%E. +Proof. +by rewrite -(hlength0 f) le_hlength//; exact: cumulative_is_nondecreasing. +Qed. -HB.instance Definition _ := +HB.instance Definition _ (f : cumulative R) := isAdditiveMeasure.Build _ R _ (hlength f : set ocitv_type -> _) - hlength_ge0' hlength_semi_additive. + (hlength_ge0' f) (hlength_semi_additive f). -Lemma hlength_content_sub_fsum (D : {fset nat}) a0 b0 +Lemma hlength_content_sub_fsum (f : cumulative R) (D : {fset nat}) a0 b0 (a b : nat -> R) : (forall i, i \in D -> a i <= b i) -> `]a0, b0] `<=` \big[setU/set0]_(i <- D) `] a i, b i]%classic -> f b0 - f a0 <= \sum_(i <- D) (f (b i) - f (a i)). Proof. move=> Dab h; have [ab|ab] := leP a0 b0; last first. - apply (@le_trans _ _ 0); first by rewrite subr_le0 ndf// ltW. - by rewrite big_seq sumr_ge0// => i iD; rewrite subr_ge0 ndf// Dab. + apply (@le_trans _ _ 0). + by rewrite subr_le0 cumulative_is_nondecreasing// ltW. + rewrite big_seq sumr_ge0// => i iD. + by rewrite subr_ge0 cumulative_is_nondecreasing// Dab. have mab k : [set` D] k -> @measurable d itvs_semiRingOfSets `]a k, b k]%classic by []. move: h; rewrite -bigcup_fset. @@ -368,7 +401,7 @@ rewrite -sumEFin fsbig_finite//= set_fsetK// big_seq [in X in (_ <= X)%E]big_seq by apply: lee_sum => i iD; rewrite hlength_itv_bnd// Dab. Qed. -Lemma hlength_sigma_sub_additive (rcf : right_continuous f) : +Lemma hlength_sigma_sub_additive (f : cumulative R) : sigma_sub_additive (hlength f : set ocitv_type -> _). Proof. move=> I A /(_ _)/cid2-/all_sig[b]/all_and2[_]/(_ _)/esym AE. @@ -381,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_eseries _ (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'). @@ -395,7 +428,7 @@ wlog wlogh : b A AE lebig / forall n, (b n).1 <= (b n).2. apply: lee_adde => e. rewrite [e%:num]splitr [in leRHS]EFinD addeA -lee_subl_addr//. apply: le_trans (epsilon_trick _ _ _) => //=. -have [c ce] := nondecreasing_right_continuousP a.1 ndf rcf [gt0 of e%:num / 2]. +have [c ce] := nondecreasing_right_continuousP a.1 f [gt0 of e%:num / 2]. have [D De] : exists D : nat -> {posnum R}, forall i, f ((b i).2 + (D i)%:num) <= f ((b i).2) + (e%:num / 2) / 2 ^ i.+1. suff : forall i, exists di : {posnum R}, @@ -403,7 +436,8 @@ have [D De] : exists D : nat -> {posnum R}, forall i, by move/choice => -[g hg]; exists g. move=> k; apply nondecreasing_right_continuousP => //. by rewrite divr_gt0 // exprn_gt0. -have acbd : `[ a.1 + c%:num / 2, a.2] `<=` \bigcup_i `](b i).1, (b i).2 + (D i)%:num[%classic. +have acbd : `[ a.1 + c%:num / 2, a.2] `<=` + \bigcup_i `](b i).1, (b i).2 + (D i)%:num[%classic. apply (@subset_trans _ `]a.1, a.2]). move=> r; rewrite /= !in_itv/= => /andP [+ ->]. by rewrite andbT; apply: lt_le_trans; rewrite ltr_addl. @@ -417,11 +451,13 @@ move=> /(_ _ _ _ obd acbd){obd acbd}. case=> X _ acXbd. rewrite -EFinD. apply: (@le_trans _ _ (\sum_(i <- X) (hlength f `](b i).1, (b i).2]%classic) + - \sum_(i <- X) (f ((b i).2 + (D i)%:num)%R - f (b i).2)%:E)%E). + \sum_(i <- X) (f ((b i).2 + (D i)%:num)%R - f (b i).2)%:E)%E). apply: (@le_trans _ _ (f a.2 - f (a.1 + c%:num / 2))%:E). - rewrite lee_fin -addrA -opprD ler_sub// (le_trans _ ce)// ndf//. + rewrite lee_fin -addrA -opprD ler_sub// (le_trans _ ce)//. + rewrite cumulative_is_nondecreasing//. by rewrite ler_add2l ler_pdivr_mulr// ler_pmulr// ler1n. - apply: (@le_trans _ _ (\sum_(i <- X) (f ((b i).2 + (D i)%:num) - f (b i).1)%:E)%E). + apply: (@le_trans _ _ + (\sum_(i <- X) (f ((b i).2 + (D i)%:num) - f (b i).1)%:E)%E). rewrite sumEFin lee_fin hlength_content_sub_fsum//. by move=> k kX; rewrite (@le_trans _ _ (b k).2)// ler_addl. apply: subset_trans. @@ -432,64 +468,36 @@ apply: (@le_trans _ _ (\sum_(i <- X) (hlength f `](b i).1, (b i).2]%classic) + by rewrite !(EFinB, hlength_itv_bnd)// addeA subeK. rewrite -big_split/= nneseries_esum//; last first. by move=> k _; rewrite adde_ge0// hlength_ge0'. -rewrite esum_ge//; exists X => //. +rewrite esum_ge//; exists [set` X] => //; rewrite fsbig_finite//= set_fsetK. rewrite big_seq [in X in (_ <= X)%E]big_seq; apply: lee_sum => k kX. by rewrite AE lee_add2l// lee_fin ler_subl_addl natrX De. Qed. Let gitvs := [the measurableType _ of salgebraType ocitv]. -Definition lebesgue_stieltjes_measure := +Definition lebesgue_stieltjes_measure (f : cumulative R) := Hahn_ext [the additive_measure _ _ of hlength f : set ocitv_type -> _ ]. End itv_semiRingOfSets. Arguments lebesgue_stieltjes_measure {R}. Section lebesgue_stieltjes_measure_itv. -Variables (d : measure_display) (R : realType) (f : R -> R). -Hypotheses (ndf : {homo f : x y / x <= y}) (rcf : right_continuous f). +Variables (d : measure_display) (R : realType) (f : cumulative R). -Let m := lebesgue_stieltjes_measure d f ndf. +Let m := lebesgue_stieltjes_measure d f. Let g : \bar R -> \bar R := EFinf f. Let lebesgue_stieltjes_measure_itvoc (a b : R) : (m `]a, b] = hlength f `]a, b])%classic. Proof. -rewrite /m /lebesgue_stieltjes_measure /= /Hahn_ext measurable_mu_extE//; last first. - by exists (a, b). -exact: hlength_sigma_sub_additive. +rewrite /m /lebesgue_stieltjes_measure /= /Hahn_ext measurable_mu_extE//. + exact: hlength_sigma_sub_additive. +by exists (a, b). Qed. -Lemma set1Ebigcap (x : R) : [set x] = \bigcap_k `](x - k.+1%:R^-1)%R, x]%classic. -Proof. -apply/seteqP; split => [_ -> k _ /=|]. - by rewrite in_itv/= lexx andbT ltr_subl_addl ltr_addr invr_gt0. -move=> y h; apply/eqP/negPn/negP => yx. -red in h. -simpl in h. -Admitted. - -Let lebesgue_stieltjes_measure_set1 (a : R) : - m [set a] = ((f a)%:E - (lim (f @ at_left a))%:E)%E. -Proof. -rewrite (set1Ebigcap a). -Admitted. - -Let lebesgue_stieltjes_measure_itvoo (a b : R) : a <= b -> - m `]a, b[%classic = ((lim (f @ at_left b))%:E - (f a)%:E)%E. -Proof. -Admitted. - -Let lebesgue_stieltjes_measure_itvcc (a b : R) : a <= b -> - m `[a, b]%classic = ((f b)%:E - (lim (f @ at_left a))%:E)%E. -Proof. -Admitted. - -Let lebesgue_stieltjes_measure_itvco (a b : R) : a <= b -> - m `[a, b[%classic = ((lim (f @ at_left b))%:E - (lim (f @ at_left a))%:E)%E. -Proof. -Admitted. - - End lebesgue_stieltjes_measure_itv. + +Example lebesgue_measure d (R : realType) + : set [the measurableType (d.-measurable).-sigma of salgebraType (d.-measurable)] -> \bar R := + lebesgue_stieltjes_measure _ [the cumulative _ of @idfun R].