diff --git a/CHANGELOG_UNRELEASED.md b/CHANGELOG_UNRELEASED.md index 108f2dda4..43180e3eb 100644 --- a/CHANGELOG_UNRELEASED.md +++ b/CHANGELOG_UNRELEASED.md @@ -6,6 +6,17 @@ - in `kernel.v`: + `kseries` is now an instance of `Kernel_isSFinite_subdef` +- in `classical_sets.v`: + + lemma `setU_id2r` +- in `lebesgue_measure.v`: + + lemma `compact_measurable` + +- in `measure.v`: + + lemmas `outer_measure_subadditive`, `outer_measureU2` + +- in `lebesgue_measure.v`: + + declare `lebesgue_measure` as a `SigmaFinite` instance + + lemma `lebesgue_regularity_inner_sup` ### Changed diff --git a/classical/classical_sets.v b/classical/classical_sets.v index 428a11998..0506e91e3 100644 --- a/classical/classical_sets.v +++ b/classical/classical_sets.v @@ -651,6 +651,14 @@ Proof. by rewrite setUA !(setUAC _ C) -(setUA _ C) setUid. Qed. Lemma setUUr A B C : A `|` (B `|` C) = (A `|` B) `|` (A `|` C). Proof. by rewrite !(setUC A) setUUl. Qed. +Lemma setU_id2r C A B : + (forall x, (~` B) x -> A x = C x) -> (A `|` B) = (C `|` B). +Proof. +move=> h; apply/seteqP; split => [x [Ax|Bx]|x [Cx|Bx]]; [|by right| |by right]. +- by have [|/h {}h] := pselect (B x); [by right|left; rewrite -h]. +- by have [|/h {}h] := pselect (B x); [by right|left; rewrite h]. +Qed. + Lemma setDE A B : A `\` B = A `&` ~` B. Proof. by []. Qed. Lemma setDUK A B : A `<=` B -> A `|` (B `\` A) = B. @@ -1029,6 +1037,7 @@ Hint Resolve subsetUl subsetUr subIsetl subIsetr subDsetl subDsetr : core. Notation setvI := setICl. #[deprecated(since="mathcomp-analysis 0.6", note="Use setICr instead.")] Notation setIv := setICr. +Arguments setU_id2r {T} C {A B}. Section set_order. Import Order.TTheory. diff --git a/theories/lebesgue_measure.v b/theories/lebesgue_measure.v index 740f4d4c2..023ac065e 100644 --- a/theories/lebesgue_measure.v +++ b/theories/lebesgue_measure.v @@ -390,6 +390,14 @@ Qed. Definition lebesgue_measure := measure_extension hlength. HB.instance Definition _ := Measure.on lebesgue_measure. +(* TODO: this ought to be turned into a Let but older version of mathcomp/coq + does not seem to allow, try to change asap *) +Local Lemma sigmaT_finite_lebesgue_measure : sigma_finite setT lebesgue_measure. +Proof. exact/measure_extension_sigma_finite/hlength_sigma_finite. Qed. + +HB.instance Definition _ := @isSigmaFinite.Build _ _ _ + lebesgue_measure sigmaT_finite_lebesgue_measure. + End itv_semiRingOfSets. Arguments hlength {R}. #[global] Hint Extern 0 (is_true (0%R <= hlength _)) => @@ -1429,9 +1437,11 @@ by apply: measurableI => //; exact: open_measurable. Qed. Lemma closed_measurable (U : set R) : closed U -> measurable U. +Proof. by move/closed_openC/open_measurable/measurableC; rewrite setCK. Qed. + +Lemma compact_measurable (A : set R) : compact A -> measurable A. Proof. -move/closed_openC=> ?; rewrite -[U]setCK; apply: measurableC. -exact: open_measurable. +by move/compact_closed => /(_ (@Rhausdorff R)); exact: closed_measurable. Qed. Lemma subspace_continuous_measurable_fun (D : set R) (f : subspace D -> R) : @@ -1439,7 +1449,7 @@ Lemma subspace_continuous_measurable_fun (D : set R) (f : subspace D -> R) : Proof. move=> mD /continuousP cf; apply: (measurability (RGenOpens.measurableE R)). move=> _ [_ [a [b ->] <-]]; apply: open_measurable_subspace => //. -by exact/cf/interval_open. +exact/cf/interval_open. Qed. Corollary open_continuous_measurable_fun (D : set R) (f : R -> R) : @@ -1977,9 +1987,9 @@ wlog : eps epspos D mD finD / exists ab : R * R, D `<=` `[ab.1, ab.2]%classic. by apply: compact_closed => //; exact: Rhausdorff. exact: interval_closed. - by move=> ? [/VDab []]. - have -> : D `\` (V `&` `[a, b]) = (D `&` `[a, b]) `\` V `|` D `\` `[a, b]. - by rewrite setDIr eqEsubset; split => z /=; case: (z \in `[a, b]); - (try tauto); try (by case; case; left); try (by case; case; right). + rewrite setDIr (setU_id2r ((D `&` `[a, b]) `\` V)); last first. + move=> z ; rewrite setDE setCI setCK => -[?|?]; + by apply/propext; split => [[]|[[]]]. have mV : measurable V. by apply: closed_measurable; apply: compact_closed => //; exact: Rhausdorff. rewrite [eps]splitr EFinD (measureU mu) // ?lte_add //. @@ -2001,10 +2011,53 @@ exists (`[a, b] `&` ~` U); split. rewrite [_ `&` ~` _ ](iffRL (disjoints_subset _ _)) ?setCK // set0U. move: mDeps; rewrite /D' ?setDE setCI setIUr setCK [U `&` D]setIC. move => /(le_lt_trans _); apply; apply: le_measure; last by move => ?; right. - by rewrite inE; apply: measurableI => //; apply: open_measurable. + by rewrite inE; apply: measurableI => //; exact: open_measurable. rewrite inE; apply: measurableU. - by (apply: measurableI; first exact: open_measurable); exact: measurableC. - by apply: measurableI => //; apply: open_measurable. + by apply: measurableI; [exact: open_measurable|exact: measurableC]. + by apply: measurableI => //; exact: open_measurable. +Qed. + +Let lebesgue_regularity_innerE_bounded (A : set R) : measurable A -> + mu A < +oo -> + mu A = ereal_sup [set mu K | K in [set K | compact K /\ K `<=` A]]. +Proof. +move=> mA muA; apply/eqP; rewrite eq_le; apply/andP; split; last first. + by apply: ub_ereal_sup => /= x [B /= [cB BA <-{x}]]; exact: le_outer_measure. +apply/lee_addgt0Pr => e e0. +have [B [cB BA /= ABe]] := lebesgue_regularity_inner mA muA e0. +rewrite -{1}(setDKU BA) (@le_trans _ _ (mu B + mu (A `\` B)))//. + by rewrite setUC outer_measureU2. +by rewrite lee_add//; [apply: ereal_sup_ub => /=; exists B|exact/ltW]. +Qed. + +Lemma lebesgue_regularity_inner_sup (D : set R) (eps : R) : measurable D -> + mu D = ereal_sup [set mu K | K in [set K | compact K /\ K `<=` D]]. +Proof. +move=> mD; have [?|] := ltP (mu D) +oo. + exact: lebesgue_regularity_innerE_bounded. +have /sigma_finiteP [/= F RFU [Fsub ffin]] := sigmaT_finite_lebesgue_measure R (*TODO: sigma_finiteT mu should be enough but does not seem to work with holder version of mathcomp/coq *). +rewrite leye_eq => /eqP /[dup] + ->. +have {1}-> : D = \bigcup_n (F n `&` D) by rewrite -setI_bigcupl -RFU setTI. +move=> FDp; apply/esym/eq_infty => M. +have : (fun n => mu (F n `&` D)) @ \oo --> +oo. + rewrite -FDp; apply: nondecreasing_cvg_mu. + - by move=> i; apply: measurableI => //; exact: (ffin i).1. + - by apply: bigcup_measurable => i _; exact: (measurableI _ _ (ffin i).1). + - by move=> n m nm; apply/subsetPset; apply: setSI; exact/subsetPset/Fsub. +move/cvgey_ge => /(_ (M + 1)%R) [N _ /(_ _ (lexx N))]. +have [mFN FNoo] := ffin N. +have [] := @lebesgue_regularity_inner (F N `&` D) _ _ _ ltr01. +- exact: measurableI. +- by rewrite (le_lt_trans _ (ffin N).2)// measureIl. +move=> V [/[dup] /compact_measurable mV cptV VFND] FDV1 M1FD. +rewrite (@le_trans _ _ (mu V))//; last first. + apply: ereal_sup_ub; exists V => //=; split => //. + exact: (subset_trans VFND (@subIsetr _ _ _)). +rewrite -(@lee_add2lE _ 1)// {1}addeC -EFinD (le_trans M1FD)//. +rewrite /mu (@measureDI _ _ _ _ (F N `&` D) _ _ mV)/=; last exact: measurableI. +rewrite ltW// lte_le_add // ?ge0_fin_numE //; last first. + by rewrite measureIr//; apply: measurableI. +by rewrite -setIA (le_lt_trans _ (ffin N).2)// measureIl//; exact: measurableI. Qed. End lebesgue_regularity. diff --git a/theories/measure.v b/theories/measure.v index d2584687e..eb27c0542 100644 --- a/theories/measure.v +++ b/theories/measure.v @@ -3330,6 +3330,37 @@ Arguments outer_measure_ge0 {R T} _. Arguments le_outer_measure {R T} _. Arguments outer_measure_sigma_subadditive {R T} _. +Section outer_measureU. +Context d (T : semiRingOfSetsType d) (R : realType). +Variable mu : {outer_measure set T -> \bar R}. +Local Open Scope ereal_scope. + +Lemma outer_measure_subadditive (F : nat -> set T) n : + mu (\big[setU/set0]_(i < n) F i) <= \sum_(i < n) mu (F i). +Proof. +pose F' := fun k => if (k < n)%N then F k else set0. +rewrite -(big_mkord xpredT F) big_nat (eq_bigr F')//; last first. + by move=> k /= kn; rewrite /F' kn. +rewrite -big_nat big_mkord. +have := outer_measure_sigma_subadditive mu F'. +rewrite (bigcup_splitn n) (_ : bigcup _ _ = set0) ?setU0; last first. + by rewrite bigcup0 // => k _; rewrite /F' /= ltnNge leq_addr. +move/le_trans; apply. +rewrite (nneseries_split n); last by move=> ?; exact: outer_measure_ge0. +rewrite [X in _ + X](_ : _ = 0) ?adde0//; last first. + rewrite eseries_cond/= eseries_mkcond eseries0//. + by move=> k _; case: ifPn => //; rewrite /F' leqNgt => /negbTE ->. +by apply: lee_sum => i _; rewrite /F' ltn_ord. +Qed. + +Lemma outer_measureU2 A B : mu (A `|` B) <= mu A + mu B. +Proof. +have := outer_measure_subadditive (bigcup2 A B) 2. +by rewrite !big_ord_recl/= !big_ord0 setU0 adde0. +Qed. + +End outer_measureU. + Lemma le_outer_measureIC (R : realFieldType) T (mu : {outer_measure set T -> \bar R}) (A X : set T) : mu X <= mu (X `&` A) + mu (X `&` ~` A). @@ -3555,7 +3586,7 @@ Notation "mu .-cara.-measurable" := Section caratheodory_measure. Variables (R : realType) (T : pointedType). -Variable (mu : {outer_measure set T -> \bar R}). +Variable mu : {outer_measure set T -> \bar R}. Let U := caratheodory_type mu. Lemma caratheodory_measure0 : mu (set0 : set U) = 0.