rebase

Author: affeldt-aist

theories/lebesgue_integral.v

@@ -5346,65 +5346,6 @@ Qed.
 End sfinite_fubini.
 Arguments sfinite_Fubini {d d' X Y R} m1 m2 f.
 
-(* PR in progress *)
-Lemma eseries_cond {R : numFieldType} (f : nat -> \bar R) P N :
-  (\sum_(N <= i <oo | P i) f i = \sum_(i <oo | P i && (N <= i)%N) f i)%E.
-Proof. by congr (lim _); apply: eq_fun => n /=; apply: big_nat_widenl. Qed.
-
-Lemma eseries_mkcondr {R : numFieldType} (f : nat -> \bar R) P Q :
-  (\sum_(i <oo | P i && Q i) f i = \sum_(i <oo | P i) if Q i then f i else 0)%E.
-Proof. by congr (lim _); apply/funext => n; rewrite big_mkcondr. Qed.
-
-Lemma lee_addgt0Pr {R : realType} (x y : \bar R) :
-  reflect (forall e, (0 < e)%R -> (x <= y + e%:E)%E) (x <= y)%E.
-Proof.
-apply/(iffP idP) => [|].
-- move: x y => [x| |] [y| |]//.
-  + rewrite lee_fin => xy e e0.
-    rewrite -EFinD lee_fin.
-    by rewrite ler_paddr// ltW.
-  + by move=> _ e e0; rewrite leNye.
-- move: x y => [x| |] [y| |]// xy.
-  + rewrite lee_fin; apply/ler_addgt0Pr => e e0.
-    by rewrite -lee_fin EFinD xy.
-  + by rewrite leey.
-  + by move: xy => /(_ 1 lte01).
-  + by move: xy => /(_ 1 lte01).
-  + by move: xy => /(_ 1 lte01).
-  + by rewrite leNye.
-Qed.
-(* /PR in progress *)
-
-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.
-set 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)// [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 ereal_sup_le {R : realType} (A : set (\bar R)) x :
   A !=set0 -> (forall y, A y -> x <= y)%E ->
   (x <= ereal_sup A)%E.
@@ -5447,24 +5388,6 @@ rewrite -(@ge0_integral_bigsetU _ _ _ _ (fun i => F (nth h (in_tuple (h :: t)) i
 exact/trivIset_nth.
 Qed.
 
-Lemma lebesgue_measure_inner_regular {R : realType} (A : set R) :
-  measurable A ->
-  let mu := @lebesgue_measure R in
-  (mu A < +oo)%E ->
-  mu A = ereal_sup [set mu K | K in [set K | compact K /\ K `<=` A]].
-Proof.
-move=> mA mu muA; apply/eqP; rewrite eq_le; apply/andP; split; last first.
-  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).
-rewrite (@le_trans _ _ (mu B + mu (A `\` B))%E)//.
-  by rewrite setUC outer_measureU2.
-rewrite lee_add//; last by rewrite ltW.
-by apply: ereal_sup_ub => /=; exists B.
-Qed.
-
 Section lower_semicontinuous.
 Local Open Scope ereal_scope.
 
@@ -5656,11 +5579,10 @@ have r_proof x : M f x > c%:E -> {r | (0 < r)%R &
     by rewrite lebesgue_measure_ball ?ltry// ltW.
   rewrite -lte_pdivl_mulr// 1?muleC// fine_gt0//.
   by rewrite lebesgue_measure_ball 1?ltW// ltry lte_fin mulrn_wgt0.
-rewrite lebesgue_measure_inner_regular//; last 2 first.
+rewrite lebesgue_regularity_inner_sup//; last 1 first.
   - rewrite -[X in measurable X]setTI; apply: emeasurable_fun_o_infty => //.
     apply: lower_semicontinuous_measurable.
     exact: lower_semicontinuous_HL_maximal.
-  - admit.
 apply: ub_ereal_sup => /= x /= [K [cK Kcmf <-{x}]].
 pose r_ x :=
   if pselect (M f x > c%:E) is left H then s2val (r_proof _ H) else 1%R.
@@ -5686,13 +5608,13 @@ have {ED}E'D : {subset E' <= D} by move=> x; rewrite mem_undup => /ED.
 have {tEB}tE'B : trivIset [set` E'] (scale_ball 1 \o B).
   by apply: sub_trivIset tEB => x/=; rewrite mem_undup.
 have {DE}DE' : cover [set` D] (scale_ball 1 \o B) `<=`
-               cover [set` E'] (scale_ball 3 \o B).
+               cover [set` E'] (scale_ball 3%:R \o B).
   by move=> x /DE [r/= rE] Brx; exists r => //=; rewrite mem_undup.
 have uniqE' : uniq E' by exact: undup_uniq.
 rewrite (@le_trans _ _ (3%:R%:E * \sum_(i <- E') mu (scale_ball 1 (B i))))//.
   have {}DE' := subset_trans KDB DE'.
-  apply: (le_trans (@content_sub_additive _ _ _ mu
-    K (fun i => scale_ball 3 (B (nth 0%R E' i))) (size E') _ _ _)) => //.
+  apply: (le_trans (@content_sub_additive _ _ _ [the measure _ _ of mu]
+    K (fun i => scale_ball 3%:R (B (nth 0%R E' i))) (size E') _ _ _)) => //.
   - by move=> k ?; exact: measurable_ball.
   - by apply: closed_measurable; apply: compact_closed => //; exact: Rhausdorff.
   - apply: (subset_trans DE'); rewrite /cover bigcup_set.
@@ -5715,6 +5637,6 @@ apply: subset_integral => //.
 - by apply: bigsetU_measurable => ? ?; exact: measurable_ball.
 - apply: measurableT_comp => //.
   by apply: measurableT_comp => //; case: locf.
-Admitted.
+Qed.
 
 End hardy_littlewood.