Lebesgue measure 20230807 (#1005)

* lebesgue inner regularity lemma

* fix for compatibility with earlier versions

Co-authored-by: zstone <[email protected]>

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
 

classical/classical_sets.v

@@ -650,6 +650,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.
@@ -1028,6 +1036,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.

theories/lebesgue_measure.v

@@ -387,6 +387,14 @@ Qed.
 Definition lebesgue_measure := measure_extension [the measure _ _ of 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 (0%:E <= hlength _) => solve[apply: hlength_ge0] : core.
@@ -1424,17 +1432,19 @@ 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) :
   measurable D -> continuous f -> measurable_fun D f.
 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) :
@@ -1975,9 +1985,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 //.
@@ -1999,10 +2009,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.

theories/measure.v

@@ -3352,6 +3352,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).
@@ -3576,7 +3607,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.