Lusin (math-comp#966)

* lusin for simple functions

* main lusin theorem done

* full version of lusin

* linting

* changelog

* fixing build somehow

* fixing build

* prove measureU2 using content property

* nitpicking

* minor generalization

---------

Co-authored-by: Reynald Affeldt <[email protected]>

CHANGELOG_UNRELEASED.md

@@ -40,6 +40,13 @@
   + lemmas `set_predC`, `preimage_true`, `preimage_false`
 - in `lebesgue_measure.v`:
   + lemmas `measurable_fun_ltr`, `measurable_minr`
+- in file `lebesgue_integral.v`,
+  + new lemmas `lusin_simple`, and `measurable_almost_continuous`.
+- in file `measure.v`,
+  + new lemmas `finite_card_sum`, and `measureU2`.
+
+- in `topology.v`:
+  + lemma `bigsetU_compact`
 
 - in `exp.v`:
   + notation `` e `^?(r +? s) ``

theories/lebesgue_integral.v

@@ -1483,6 +1483,7 @@ Qed.
 
 End approximation.
 
+
 Section semi_linearity0.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType).
@@ -1617,6 +1618,128 @@ Qed.
 
 End approximation_sfun.
 
+Section lusin.
+Hint Extern 0  (hausdorff_space _) => (exact: Rhausdorff ) : core.
+Local Open Scope ereal_scope.
+Context (rT : realType) (A : set rT).
+Let mu := [the measure _ _ of @lebesgue_measure rT].
+Let R  := [the measurableType _ of measurableTypeR rT].
+Hypothesis mA : measurable A.
+Hypothesis finA : mu A < +oo.
+
+Let lusin_simple (f : {sfun R >-> rT}) (eps : rT) : (0 < eps)%R ->
+  exists K, [/\ compact K, K `<=` A, mu (A `\` K) < eps%:E &
+  {within K, continuous f}].
+Proof.
+move: eps=> _/posnumP[eps]; have [N /card_fset_set rfN] := @fimfunP _ _ f.
+pose Af x : set R := A `&` f @^-1` [set x].
+have mAf x : measurable (Af x) by exact: measurableI.
+have finAf x : mu (Af x) < +oo.
+  by rewrite (le_lt_trans _ finA)// le_measure// ?inE//; exact: subIsetl.
+have eNpos : (0 < eps%:num/N.+1%:R)%R by [].
+have dK' x := lebesgue_regularity_inner (mAf x) (finAf x) eNpos.
+pose dK x : set R := projT1 (cid (dK' x)); pose J i : set R := Af i `\` dK i.
+have dkP x := projT2 (cid (dK' x)).
+have mdK i : measurable (dK i).
+  by apply: closed_measurable; apply: compact_closed => //; case: (dkP i).
+have mJ i : measurable (J i) by apply: measurableD => //; exact: measurableI.
+have dKsub z : dK z `<=` f @^-1` [set z].
+  by case: (dkP z) => _ /subset_trans + _; apply => ? [].
+exists (\bigcup_(i in range f) dK i); split.
+- by rewrite -bigsetU_fset_set//; apply: bigsetU_compact=>// i _; case: (dkP i).
+- by move=> z [y _ dy]; have [_ /(_ _ dy) []] := dkP y.
+- have -> : A `\` \bigcup_(i in range f) dK i = \bigcup_(i in range f) J i.
+    rewrite -bigcupDr /= ?eqEsubset; last by exists (f point), point.
+    split => z; first by move=> /(_ (f z)) [//| ? ?]; exists (f z).
+    case => ? [? _ <-] [[zab /= <- nfz]] ? [r _ <-]; split => //.
+    by move: nfz; apply: contra_not => /[dup] /dKsub ->.
+  apply: (@le_lt_trans _ _ (\sum_(i \in range f) mu (J i))).
+    by apply: content_sub_fsum => //; exact: fin_bigcup_measurable.
+  apply: le_lt_trans.
+    apply: (@lee_fsum _ _ _ _ (fun=> (eps%:num / N.+1%:R)%:E * 1%:E)) => //.
+    by move=> i ?; rewrite mule1; apply: ltW; have [_ _] := dkP i.
+  rewrite /=-ge0_mule_fsumr // -esum_fset // finite_card_sum // -EFinM lte_fin.
+  by rewrite rfN -mulrA gtr_pmulr // mulrC ltr_pdivr_mulr // mul1r ltr_nat.
+- suff : closed (\bigcup_(i in range f) dK i) /\
+    {within \bigcup_(i in range f) dK i, continuous f} by case.
+  rewrite -bigsetU_fset_set //.
+  apply: (@big_ind _ (fun U => closed U /\ {within U, continuous f})).
+  + by split; [exact: closed0 | exact: continuous_subspace0].
+  + by move=> ? ? [? ?][? ?]; split; [exact: closedU|exact: withinU_continuous].
+  + move=> i _; split; first by apply: compact_closed; have [] := dkP i.
+    apply: (continuous_subspaceW (dKsub i)).
+    apply: (@subspace_eq_continuous _ _ _ (fun=> i)).
+      by move=> ? /set_mem ->.
+    by apply: continuous_subspaceT => ?; exact: cvg_cst.
+Qed.
+
+Let measurable_almost_continuous' (f : R -> R) (eps : rT) :
+  (0 < eps)%R -> measurable_fun A f -> exists K,
+  [/\ measurable K, K `<=` A, mu (A `\` K) < eps%:E &
+  {within K, continuous f}].
+Proof.
+move: eps=> _/posnumP[eps] mf; pose f' := EFin \o f.
+have mf' : measurable_fun A f' by exact/EFin_measurable_fun.
+have [/= g_ gf'] := @approximation_sfun _ R rT _ _ mA mf'.
+pose e2n n := (eps%:num / 2) / (2 ^ n.+1)%:R.
+have e2npos n : (0 < e2n n)%R by rewrite divr_gt0.
+have gK' n := @lusin_simple (g_ n) (e2n n) (e2npos n).
+pose gK n := projT1 (cid (gK' n)); have gKP n := projT2 (cid (gK' n)).
+pose K := \bigcap_i gK i; have mgK n : measurable (gK n).
+  by apply: closed_measurable; apply: compact_closed => //; have [] := gKP n.
+have mK : measurable K by exact: bigcap_measurable.
+have Kab : K `<=` A by move=> z /(_ O I); have [_ + _ _] := gKP O; apply.
+have []// := @pointwise_almost_uniform _ rT R mu g_ f K (eps%:num / 2).
+- by move=> n; exact: measurable_funTS.
+- exact: (measurable_funS _ Kab).
+- by rewrite (@le_lt_trans _ _ (mu A))// le_measure// ?inE.
+- by move=> z Kz; have /fine_fcvg := gf' z (Kab _ Kz); rewrite -fmap_comp compA.
+move=> D [/= mD Deps KDf]; exists (K `\` D); split => //.
+- exact: measurableD.
+- exact: subset_trans Kab.
+- rewrite setDDr; apply: le_lt_trans => /=.
+    by apply: measureU2 => //; apply: measurableI => //; apply: measurableC.
+  rewrite [_%:num]splitr EFinD; apply: lee_lt_add => //=; first 2 last.
+  + by rewrite (@le_lt_trans _ _ (mu D)) ?le_measure ?inE//; exact: measurableI.
+  + rewrite ge0_fin_numE// (@le_lt_trans _ _ (mu A))// le_measure// ?inE//.
+    exact: measurableD.
+  rewrite setDE setC_bigcap setI_bigcupr.
+  apply: (@le_trans _ _(\sum_(k <oo) mu (A `\` gK k))).
+    apply: measure_sigma_sub_additive => //; [|apply: bigcup_measurable => + _].
+      by move=> k /=; apply: measurableD => //; apply: mgK.
+    by move=> k /=; apply: measurableD => //; apply: mgK.
+  apply: (@le_trans _ _(\sum_(k <oo) (e2n k)%:E)); last exact: epsilon_trick0.
+  by apply: lee_nneseries => // k _; apply: ltW; have [] := gKP k.
+apply: (@uniform_limit_continuous_subspace _ _ _ (g_ @ \oo)) => //.
+near_simpl; apply: nearW => // n; apply: (@continuous_subspaceW _ _ _ (gK n)).
+  by move=> z [+ _]; apply.
+by have [] := projT2 (cid (gK' n)).
+Qed.
+
+Lemma measurable_almost_continuous (f : R -> R) (eps : rT) :
+  (0 < eps)%R -> measurable_fun A f -> exists K,
+  [/\ compact K, K `<=` A, mu (A `\` K) < eps%:E &
+  {within K, continuous f}].
+Proof.
+move: eps=> _/posnumP[eps] mf; have e2pos : (0 < eps%:num/2)%R by [].
+have [K [mK KA ? ?]] := measurable_almost_continuous' e2pos mf.
+have Kfin : mu K < +oo by rewrite (le_lt_trans _ finA)// le_measure ?inE.
+have [D /= [cD DK KDe]] := lebesgue_regularity_inner mK Kfin e2pos.
+exists D; split => //; last exact: (continuous_subspaceW DK).
+  exact: (subset_trans DK).
+have -> : A `\` D = (A `\` K) `|` (K `\` D).
+  rewrite eqEsubset; split => z.
+    by case: (pselect (K z)) => // ? [? ?]; [right | left].
+  case; case=> az nz; split => //; [by move: z nz {az}; apply/subsetC|].
+  exact: KA.
+apply: le_lt_trans.
+  apply: measureU2; apply: measurableD => //; apply: closed_measurable.
+  by apply: compact_closed; first exact: Rhausdorff.
+by rewrite [_ eps]splitr EFinD lte_add.
+Qed.
+
+End lusin.
+
 Section emeasurable_fun.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType).

theories/measure.v

@@ -1731,6 +1731,13 @@ Section dirac_lemmas.
 Local Open Scope ereal_scope.
 Context d (T : measurableType d) (R : realType).
 
+Lemma finite_card_sum (A : set T) : finite_set A ->
+  \esum_(i in A) 1 = (#|` fset_set A|%:R)%:E :> \bar R.
+Proof.
+move=> finA; rewrite esum_fset// (eq_fsbigr (cst 1))//.
+by rewrite card_fset_sum1// natr_sum -sumEFin fsbig_finite.
+Qed.
+
 Lemma finite_card_dirac (A : set T) : finite_set A ->
   \esum_(i in A) \d_ i A = (#|` fset_set A|%:R)%:E :> \bar R.
 Proof.
@@ -2968,8 +2975,8 @@ by apply: le_measure; rewrite ?inE.
 Qed.
 
 Section measureD.
-Context d (R : realFieldType) (T : ringOfSetsType d).
-Variable mu : {measure set T -> \bar R}.
+Context d (T : ringOfSetsType d) (R : realFieldType).
+Variable mu : {content set T -> \bar R}.
 
 Lemma measureDI A B : measurable A -> measurable B ->
   mu A = mu (A `\` B) + mu (A `&` B).
@@ -2993,24 +3000,41 @@ Qed.
 
 End measureD.
 
-Lemma measureUfinr d (T : ringOfSetsType d) (R : realFieldType) (A B : set T)
-   (mu : {measure set T -> \bar R}):
-    measurable A -> measurable B -> (mu B < +oo)%E ->
-  mu (A `|` B) = (mu A + mu B - mu (A `&` B))%E.
+Section measureU2.
+Context d (T : ringOfSetsType d) (R : realFieldType).
+Variable mu : {content set T -> \bar R}.
+
+Lemma measureU2 A B : measurable A -> measurable B ->
+  mu (A `|` B) <= mu A + mu B.
+Proof.
+move=> ? ?; rewrite -bigcup2inE bigcup_mkord.
+rewrite (le_trans (@content_sub_additive _ _ _ mu _ (bigcup2 A B) 2%N _ _ _))//.
+by move=> -[//|[//|[|]]].
+by apply: bigsetU_measurable => -[] [//|[//|[|]]].
+by rewrite big_ord_recr/= big_ord_recr/= big_ord0 add0e.
+Qed.
+
+End measureU2.
+
+Section measureU.
+Context d (T : ringOfSetsType d) (R : realFieldType).
+Variable mu : {measure set T -> \bar R}.
+
+Lemma measureUfinr A B : measurable A -> measurable B -> mu B < +oo ->
+  mu (A `|` B) = mu A + mu B - mu (A `&` B).
 Proof.
 move=> Am Bm mBfin; rewrite -[B in LHS](setDUK (@subIsetl _ _ A)) setUA.
 rewrite [A `|` _]setUidl; last exact: subIsetr.
-rewrite measureU//=; do ?by apply:measurableD; do ?apply: measurableI.
-  rewrite measureD//; do ?exact: measurableI.
-  by rewrite addeA setIA setIid setIC.
-by rewrite setDE setCI setIUr -!setDE setDv set0U setDIK.
+rewrite measureU//=; [|rewrite setDIr setDv set0U ?setDIK//..].
+- by rewrite measureD// ?setIA ?setIid 1?setIC ?addeA//; exact: measurableI.
+- exact: measurableD.
 Qed.
 
-Lemma measureUfinl d (T : ringOfSetsType d) (R : realFieldType) (A B : set T)
-   (mu : {measure set T -> \bar R}):
-    measurable A -> measurable B -> (mu A < +oo)%E ->
-  mu (A `|` B) = (mu A + mu B - mu (A `&` B))%E.
-Proof. by move=> *; rewrite setUC measureUfinr// setIC [(mu B + _)%E]addeC. Qed.
+Lemma measureUfinl A B : measurable A -> measurable B -> mu A < +oo ->
+  mu (A `|` B) = mu A + mu B - mu (A `&` B).
+Proof. by move=> *; rewrite setUC measureUfinr// setIC [mu B + _]addeC. Qed.
+
+End measureU.
 
 Lemma eq_measureU d (T : ringOfSetsType d) (R : realFieldType) (A B : set T)
    (mu mu' : {measure set T -> \bar R}):
@@ -3755,8 +3779,8 @@ have setDE : setD_closed E.
   move=> A B BA [mA m1m2A AD] [mB m1m2B BD]; split; first exact: measurableD.
   - rewrite measureD//; last first.
       by rewrite (le_lt_trans _ m1oo)//; apply: le_measure => // /[!inE].
-    rewrite setIidr// m1m2A m1m2B measureD// ?setIidr//.
-    by rewrite (le_lt_trans _ m1oo)// -m1m2A; apply: le_measure => // /[!inE].
+    rewrite setIidr//= m1m2A m1m2B measureD// ?setIidr//.
+    by rewrite (le_lt_trans _ m1oo)//= -m1m2A; apply: le_measure => // /[!inE].
   - by rewrite setDE; apply: subIset; left.
 have ndE : ndseq_closed E.
   move=> A ndA EA; split; have mA n : measurable (A n) by have [] := EA n.

theories/topology.v

@@ -3173,6 +3173,11 @@ have /cptB[x BFx] : F B by apply: filterS FBA; exact: subIsetr.
 by exists x; right.
 Qed.
 
+Lemma bigsetU_compact I (F : I -> set X) (s : seq I) (P : pred I) :
+    (forall i, P i -> compact (F i)) ->
+  compact (\big[setU/set0]_(i <- s | P i) F i).
+Proof. by move=> ?; elim/big_ind : _ =>//; [exact:compact0|exact:compactU]. Qed.
+
 (* The closed condition here is neccessary to make this definition work in a  *)
 (* non-hausdorff setting.                                                     *)
 Definition compact_near (F : set (set X)) :=