deprecate approximation and make its interface accessible (#1421)

CHANGELOG_UNRELEASED.md

@@ -12,21 +12,45 @@
 
 - in `mathcomp_extra.v`:
   + lemma `partition_disjoint_bigfcup`
+- in `lebesgue_measure.v`:
+  + lemma `measurable_indicP`
+
+- in `lebesgue_integral.v`:
+  + definition `dyadic_approx` (was `Let A`)
+  + definition `integer_approx` (was `Let B`)
+  + lemma `measurable_sum`
+  + lemma `integrable_indic`
 
 - in `constructive_ereal.v`:
   + notations `\prod` in scope ereal_scope
   + lemmas `prode_ge0`, `prode_fin_num`
 
 ### Changed
+
+- in `lebesgue_integrale.v`
+  + change implicits of `measurable_funP`
 
 ### Renamed
 
+- in `lebesgue_measure.v`:
+  + `measurable_fun_indic` -> `measurable_indic`
+  + `emeasurable_fun_sum` -> `emeasurable_sum`
+  + `emeasurable_fun_fsum` -> `emeasurable_fsum`
+  + `ge0_emeasurable_fun_sum` -> `ge0_emeasurable_sum`
+
 ### Generalized
 
 ### Deprecated
 
+- in file `lebesgue_integral.v`:
+  + lemma `approximation`
+
 ### Removed
 
+- in `lebesgue_integral.v`:
+  + lemma `measurable_indic` (was uselessly specializing `measurable_fun_indic` (now `measurable_indic`) from `lebesgue_measure.v`)
+  + notation `measurable_fun_indic` (deprecation since 0.6.3)
+
 ### Infrastructure
 
 ### Misc

theories/charge.v

@@ -1837,7 +1837,7 @@ have int_f_nuT : \int[mu]_x f x = nu setT.
     by apply: eq_eseriesr => i _; rewrite int_f_E// setTI.
   rewrite -UET measure_bigcup//.
   by apply: eq_eseriesl => // x; rewrite in_setT.
-have mf : measurable_fun setT f by exact: ge0_emeasurable_fun_sum.
+have mf : measurable_fun setT f by exact: ge0_emeasurable_sum.
 have fi : mu.-integrable setT f.
   apply/integrableP; split => //.
   under eq_integral do (rewrite gee0_abs; last exact: nneseries_ge0).
@@ -1921,29 +1921,29 @@ Lemma change_of_variables f E : (forall x, 0 <= f x) ->
   \int[mu]_(x in E) (f x * ('d nu '/d mu) x) = \int[nu]_(x in E) f x.
 Proof.
 move=> f0 mE mf; set g := 'd nu '/d mu.
-have [h [ndh hf]] := approximation mE mf (fun x _ => f0 x).
+pose h := nnsfun_approx mE mf.
 have -> : \int[nu]_(x in E) f x =
     lim (\int[nu]_(x in E) (EFin \o h n) x @[n --> \oo]).
   have fE x : E x -> f x = lim ((EFin \o h n) x @[n --> \oo]).
-    by move=> Ex; apply/esym/cvg_lim => //; exact: hf.
+    by move=> Ex; apply/esym/cvg_lim => //; exact: cvg_nnsfun_approx.
   under eq_integral => x /[!inE] /fE -> //.
   apply: monotone_convergence => //.
   - move=> n; apply/measurable_EFinP.
     by apply: (measurable_funS measurableT) => //; exact/measurable_funP.
   - by move=> n x Ex //=; rewrite lee_fin.
-  - by move=> x Ex a b /ndh /=; rewrite lee_fin => /lefP.
+  - by move=> x Ex a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 have -> : \int[mu]_(x in E) (f \* g) x =
     lim (\int[mu]_(x in E) ((EFin \o h n) \* g) x @[n --> \oo]).
   have fg x :E x -> f x * g x = lim (((EFin \o h n) \* g) x @[n --> \oo]).
     by move=> Ex; apply/esym/cvg_lim => //; apply: cvgeMr;
-      [exact: f_fin_num|exact: hf].
+      [exact: f_fin_num|exact: cvg_nnsfun_approx].
   under eq_integral => x /[!inE] /fg -> //.
   apply: monotone_convergence => [//| | |].
   - move=> n; apply/emeasurable_funM; apply/measurable_funTS.
       exact/measurable_EFinP.
     exact: measurable_int (f_integrable _).
   - by move=> n x Ex //=; rewrite mule_ge0 ?lee_fin//=; exact: f_ge0.
-  - by move=> x Ex a b /ndh /= /lefP hahb; rewrite lee_wpmul2r ?lee_fin// f_ge0.
+  - by move=> x Ex a b ab/=; rewrite lee_wpmul2r ?lee_fin ?f_ge0//; exact/lefP/nd_nnsfun_approx.
 suff suf n : \int[mu]_(x in E) ((EFin \o h n) x * g x) =
     \int[nu]_(x in E) (EFin \o h n) x.
   by under eq_fun do rewrite suf.
@@ -2005,18 +2005,16 @@ Local Notation "'d nu '/d mu" := (f nu mu).
 Lemma chain_rule E : nu `<< mu -> mu `<< la -> measurable E ->
   ae_eq la E ('d nu '/d la) ('d nu '/d mu \* 'd mu '/d la).
 Proof.
-move=> numu mula mE; have nula := measure_dominates_trans numu mula.
+move=> numu mula mE.
 have mf : measurable_fun E ('d nu '/d mu).
   exact/measurable_funTS/(measurable_int _ (f_integrable _)).
-have [h [ndh hf]] := approximation mE mf (fun x _ => f_ge0 numu x).
 apply: integral_ae_eq => //.
-- apply: (integrableS measurableT) => //.
-  apply: f_integrable.
-  exact: (measure_dominates_trans numu mula).
+- apply: (integrableS measurableT) => //; apply: f_integrable.
+  exact: measure_dominates_trans numu mula.
 - apply: emeasurable_funM => //.
   exact/measurable_funTS/(measurable_int _ (f_integrable _)).
 - move=> A AE mA; rewrite change_of_variables//.
-  + by rewrite -!f_integral.
+  + by rewrite -!f_integral//; exact: measure_dominates_trans numu mula.
   + exact: f_ge0.
   + exact: measurable_funS mf.
 Qed.

theories/kernel.v

@@ -131,8 +131,7 @@ Definition kseries : X -> {measure set Y -> \bar R} :=
 Lemma measurable_fun_kseries (U : set Y) :
   measurable U -> measurable_fun [set: X] (kseries ^~ U).
 Proof.
-move=> mU.
-by apply: ge0_emeasurable_fun_sum => // n _; exact/measurable_kernel.
+by move=> mU; apply: ge0_emeasurable_sum => // n _; exact/measurable_kernel.
 Qed.
 
 HB.instance Definition _ :=
@@ -546,7 +545,7 @@ rewrite [X in measurable_fun _ X](_ : _ = (fun x => \sum_(r \in range (k_ n))
     apply/measurable_EFinP/measurableT_comp => [//|].
     exact/measurableT_comp.
   - by move=> m y _; rewrite nnfun_muleindic_ge0.
-apply: emeasurable_fun_fsum => // r.
+apply: emeasurable_fsum => // r.
 rewrite [X in measurable_fun _ X](_ : _ = fun x => r%:E *
     \int[l x]_y (\1_(k_ n @^-1` [set r]) (x, y))%:E); last first.
   apply/funext => x; under eq_integral do rewrite EFinM.
@@ -571,24 +570,30 @@ Lemma measurable_fun_integral_finite_kernel (l : R.-fker X ~> Y)
     (k0 : forall z, 0 <= k z) (mk : measurable_fun [set: X * Y] k) :
   measurable_fun [set: X] (fun x => \int[l x]_y k (x, y)).
 Proof.
-have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x).
-apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r.
-have [l_ hl_] := measure_uub l.
-by apply: measurable_fun_xsection_finite_kernel => // /[!inE].
+pose k_ := nnsfun_approx measurableT mk.
+apply: (@measurable_fun_xsection_integral _ k_).
+- by move=> a b ab; exact/nd_nnsfun_approx.
+- by move=> z; exact/cvg_nnsfun_approx.
+- move => n r.
+  have [l_ hl_] := measure_uub l.
+  by apply: measurable_fun_xsection_finite_kernel => // /[!inE].
 Qed.
 
 Lemma measurable_fun_integral_sfinite_kernel (l : R.-sfker X ~> Y)
     (k0 : forall t, 0 <= k t) (mk : measurable_fun [set: X * Y] k) :
   measurable_fun [set: X] (fun x => \int[l x]_y k (x, y)).
 Proof.
-have [k_ [ndk_ k_k]] := approximation measurableT mk (fun xy _ => k0 xy).
-apply: (measurable_fun_xsection_integral ndk_ (k_k ^~ Logic.I)) => n r.
-have [l_ hl_] := sfinite_kernel l.
-rewrite (_ : (fun x => _) = (fun x =>
-    mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first.
-  by apply/funext => x; rewrite hl_//; exact/measurable_xsection.
-apply: ge0_emeasurable_fun_sum => // m _.
-by apply: measurable_fun_xsection_finite_kernel => // /[!inE].
+pose k_ := nnsfun_approx measurableT mk.
+apply: (@measurable_fun_xsection_integral _ k_).
+- by move=> a b ab; exact/nd_nnsfun_approx.
+- by move=> z; exact/cvg_nnsfun_approx.
+- move => n r.
+  have [l_ hl_] := sfinite_kernel l.
+  rewrite (_ : (fun x => _) = (fun x =>
+      mseries (l_ ^~ x) 0 (xsection (k_ n @^-1` [set r]) x))); last first.
+    by apply/funext => x; rewrite hl_//; exact/measurable_xsection.
+  apply: ge0_emeasurable_sum => // m _.
+  by apply: measurable_fun_xsection_finite_kernel => // /[!inE].
 Qed.
 
 End measurable_fun_integral_finite_sfinite.
@@ -1007,8 +1012,11 @@ Lemma measurable_fun_integral_kernel
     (k : Y -> \bar R) (k0 : forall z, 0 <= k z) (mk : measurable_fun [set: Y] k) :
   measurable_fun [set: X] (fun x => \int[l x]_y k y).
 Proof.
-have [k_ [ndk_ k_k]] := approximation measurableT mk (fun x _ => k0 x).
-by apply: (measurable_fun_preimage_integral ndk_ k_k) => n r; exact/ml.
+pose k_ := nnsfun_approx measurableT mk.
+apply: (@measurable_fun_preimage_integral _ _ _ _ _ _ k_) => //.
+- by move=> a b ab; exact/nd_nnsfun_approx.
+- by move=> z _; exact/cvg_nnsfun_approx.
+- by move=> n r; exact/ml.
 Qed.
 
 End measurable_fun_integral_kernel.
@@ -1077,13 +1085,13 @@ Lemma integral_kcomp x f : (forall z, 0 <= f z) -> measurable_fun [set: Z] f ->
   \int[kcomp l k x]_z f z = \int[l x]_y (\int[k (x, y)]_z f z).
 Proof.
 move=> f0 mf.
-have [f_ [ndf_ f_f]] := approximation measurableT mf (fun z _ => f0 z).
+pose f_ := nnsfun_approx measurableT mf.
 transitivity (\int[kcomp l k x]_z (lim ((f_ n z)%:E @[n --> \oo]))).
-  by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: f_f.
+  by apply/eq_integral => z _; apply/esym/cvg_lim => //=; exact: cvg_nnsfun_approx.
 rewrite monotone_convergence//; last 3 first.
   by move=> n; exact/measurable_EFinP.
   by move=> n z _; rewrite lee_fin.
-  by move=> z _ a b /ndf_ /lefP ab; rewrite lee_fin.
+  by move=> z _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 rewrite (_ : (fun _ => _) =
     (fun n => \int[l x]_y (\int[k (x, y)]_z (f_ n z)%:E)))//; last first.
   by apply/funext => n; rewrite integral_kcomp_nnsfun.
@@ -1099,12 +1107,12 @@ transitivity (\int[l x]_y lim ((\int[k (x, y)]_z (f_ n z)%:E) @[n --> \oo])).
     + exact/measurable_EFinP.
     + by move=> z _; rewrite lee_fin.
     + exact/measurable_EFinP.
-    + by move: ab => /ndf_ /lefP ab z _; rewrite lee_fin.
+    + by move=> z _; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
 apply: eq_integral => y _; rewrite -monotone_convergence//; last 3 first.
   - by move=> n; exact/measurable_EFinP.
   - by move=> n z _; rewrite lee_fin.
-  - by move=> z _ a b /ndf_ /lefP; rewrite lee_fin.
-by apply: eq_integral => z _; apply/cvg_lim => //; exact: f_f.
+  - by move=> z _ a b ab; rewrite lee_fin; exact/lefP/nd_nnsfun_approx.
+by apply: eq_integral => z _; apply/cvg_lim => //; exact: cvg_nnsfun_approx.
 Qed.
 
 End integral_kcomp.