gen cont under int

Author: affeldt-aist

theories/lang_syntax_noisy.v

@@ -317,16 +317,15 @@ set MS12 := (S1 * S2)%R.
 set C := ((((y * s1 ^+ 2)%R + (m1 * s2 ^+ 2)%R)%E - m2 * s1 ^+ 2) / DS12)%R.
 under eq_integral do rewrite expRD EFinM.
 rewrite ge0_integralZr//=; last first.
- apply/measurable_EFinP.
- apply: measurableT_comp => //.
- apply: measurable_funM => //.
- apply: measurableT_comp => //.
- apply: (@measurableT_comp _ _ _ _ _ _ (fun t : R => t ^+ 2)%R) => //.
- exact: measurable_funD.
+  apply/measurable_EFinP.
+  apply: measurableT_comp => //.
+  apply: measurable_funM => //.
+  apply: measurableT_comp => //.
+  apply: (@measurableT_comp _ _ _ _ _ _ (fun t : R => t ^+ 2)%R) => //.
+  exact: measurable_funD.
 rewrite /normal_peak /normal_fun.
 rewrite [in RHS]EFinM.
-rewrite [in RHS]sqr_sqrtr//; last first.
-  by rewrite addr_ge0// sqr_ge0.
+rewrite [in RHS]sqr_sqrtr//; last by rewrite addr_ge0// sqr_ge0.
 rewrite muleA; congr *%E; last by rewrite -mulNr.
 (* gauss integral *)
 have MS12DS12_gt0 : (0 < MS12 / DS12)%R.
@@ -339,14 +338,11 @@ transitivity (((Num.sqrt S1 * Num.sqrt S2 * pi *+ 2)^-1)%:E
   congr *%E.
   apply: eq_integral => x _.
   rewrite -EFinM; congr EFin.
-  rewrite normal_pdfE; last first.
-    apply: lt0r_neq0.
-    by rewrite sqrtr_gt0.
+  rewrite normal_pdfE; last by rewrite lt0r_neq0// sqrtr_gt0.
   rewrite mulrA mulVf// ?mul1r//.
   rewrite lt0r_neq0// invr_gt0 sqrtr_gt0 pmulrn_lgt0// mulr_gt0// ?pi_gt0//.
-  rewrite exprn_even_gt0//=.
-  by rewrite lt0r_neq0// sqrtr_gt0.
-rewrite ge0_integralZl//; last 3 first.
+  by rewrite exprn_even_gt0//= lt0r_neq0// sqrtr_gt0.
+rewrite ge0_integralZl//=; last 3 first.
   apply/measurable_EFinP.
   exact: measurable_normal_pdf.
   move=> x _.

theories/lebesgue_integral_theory/lebesgue_integral_under.v

@@ -41,12 +41,11 @@ Variable f : R -> Y -> R.
 Variable B : set Y.
 Hypothesis mB : measurable B.
 
-Variable a u v : R.
+Variable u v : R.
 Let I : set R := `]u, v[.
 
-Hypothesis Ia : I a.
 Hypothesis int_f : forall x, I x -> mu.-integrable B (EFin \o (f x)).
-Hypothesis cf : {ae mu, forall y, B y -> continuous (f ^~ y)}.
+Hypothesis cf : {ae mu, forall y, B y -> {in I, continuous (f ^~ y)}}.
 
 Variable g : Y -> R.
 
@@ -56,13 +55,14 @@ Hypothesis g_ub : forall x, I x -> {ae mu, forall y, B y -> `|f x y| <= g y}.
 Let F x := (\int[mu]_(y in B) f x y)%R.
 
 Lemma continuity_under_integral :
-  continuous_at a (fun l => \int[mu]_(x in B) f l x).
+  {in I, continuous (fun l => \int[mu]_(x in B) f l x)}.
 Proof.
+move=> a /set_mem Ia.
 have [Z [mZ Z0 /subsetCPl ncfZ]] := cf.
-have BZ_cf x : x \in B `\` Z -> continuous (f ^~ x).
+have BZ_cf x : x \in B `\` Z -> {in I, continuous (f ^~ x)}.
   by rewrite inE/= => -[Bx nZx]; exact: ncfZ.
 have [vu|uv] := lerP v u.
-  by move: Ia; rewrite /I set_itv_ge// -leNgt bnd_simp.
+  by move: (Ia); rewrite /I set_itv_ge// -leNgt bnd_simp.
 apply/cvg_nbhsP => w wa.
 have /near_in_itvoo[e /= e0 aeuv] : a \in `]u, v[ by rewrite inE.
 move/cvgrPdist_lt : (wa) => /(_ _ e0)[N _ aue].
@@ -114,7 +114,8 @@ apply: (@dominated_cvg _ _ _ mu _ _
   have : x \in B `\` Z.
     move: BZUUx; rewrite inE/= => -[Bx nZUUx]; rewrite inE/=; split => //.
     by apply: contra_not nZUUx; left.
-  by move/(BZ_cf x)/(_ a)/cvg_nbhsP; apply; rewrite (cvg_shiftn N).
+  move/(BZ_cf x)/(_ a); move/mem_set : Ia => /[swap] /[apply].
+  by move/cvg_nbhsP; apply; rewrite (cvg_shiftn N).
 - by apply: (integrableS mB) => //; exact: measurableD.
 - move=> n x [Bx ZUUx]; rewrite lee_fin.
   move/subsetCPl : (Ug_ub n); apply => //=.
@@ -125,7 +126,8 @@ End continuity_under_integral.
 
 Section differentiation_under_integral.
 
-Definition partial1of2 {R : realType} {T : Type} (f : R -> T -> R) : R -> T -> R := fun x y => (f ^~ y)^`() x.
+Definition partial1of2 {R : realType} {T : Type} (f : R -> T -> R) : R -> T -> R
+  := fun x y => (f ^~ y)^`() x.
 
 Local Notation "'d1 f" := (partial1of2 f).