Generalize integration_by_parts

CHANGELOG_UNRELEASED.md

@@ -102,6 +102,12 @@
 - in `lebesgue_integral_nonneg.v`:
   + lemma `ge0_integral_ereal_sup` (was a `Let`)
 
+- in `ftc.v`:
+  + lemmas `integration_by_partsy_ge0_ge0`,
+           `integration_by_partsy_le0_ge0`,
+           `integration_by_partsy_le0_le0`,
+           `integration_by_partsy_ge0_le0`
+
 ### Changed
 
 - in `convex.v`:

theories/ftc.v

@@ -836,6 +836,326 @@ Qed.
 
 End integration_by_parts.
 
+(* PR#1656 *)
+Lemma derivable_oy_continuous_within_itvcy {R : numFieldType}
+  {V : normedModType R} (f : R -> V) (x : R) :
+  derivable_oy_continuous_bnd f x -> {within `[x, +oo[, continuous f}.
+Proof.
+Admitted.
+
+(* #PR1656 *)
+Lemma derivable_oy_continuous_bndW_oo {R : numFieldType} {V : normedModType R}
+    (a c d : R) (f : R -> V) :
+  (c < d) ->
+  (a <= c) ->
+  derivable_oy_continuous_bnd f a ->
+  derivable_oo_continuous_bnd f c d.
+Proof.
+Admitted.
+
+(* PR#1662 *)
+Lemma measurable_fun_itv_bndo_bndcP {R : realType} (a : itv_bound R) (b : R)
+    (f : R -> R) :
+  measurable_fun [set` Interval a (BLeft b)] f <->
+  measurable_fun [set` Interval a (BRight b)] f.
+Proof.
+Admitted.
+
+(* PR#1662 *)
+Lemma measurable_fun_itv_obnd_cbndP {R : realType} (a : R) (b : itv_bound R)
+    (f : R -> R) :
+  measurable_fun [set` Interval (BRight a) b] f <->
+  measurable_fun [set` Interval (BLeft a) b] f.
+Proof.
+Admitted.
+
+Section integration_by_partsy_ge0.
+Context {R : realType}.
+Notation mu := lebesgue_measure.
+Local Open Scope ereal_scope.
+Local Open Scope classical_set_scope.
+
+Let itvSay {a : R} {n m} {b0 b1 : bool} :
+  [set` Interval (BSide b0 (a + n%:R)) (BSide b1 (a + m%:R))] `<=`
+    [set` Interval (BSide b0 a) (BInfty _ false)].
+Proof.
+move=> x/=; rewrite 2!in_itv/= andbT => /andP[+ _].
+by case: b0 => /= H; [apply: le_trans H|apply: le_lt_trans H]; rewrite lerDl.
+Qed.
+
+Variables (F G f g : R -> R^o) (a FGoo : R).
+Hypothesis cf : {within `[a, +oo[, continuous f}.
+Hypothesis Foy : derivable_oy_continuous_bnd F a.
+Hypothesis Ff : {in `]a, +oo[%R, F^`() =1 f}.
+Hypothesis cg : {within `[a, +oo[, continuous g}.
+Hypothesis Goy : derivable_oy_continuous_bnd G a.
+Hypothesis Gg : {in `]a, +oo[%R, G^`() =1 g}.
+Hypothesis cvgFG : (F \* G)%R x @[x --> +oo%R] --> FGoo.
+
+Let mFg :  measurable_fun `]a, +oo[ (fun x => (F x * g x)%R).
+Proof.
+apply: (@measurable_funS _ _ _ _ `[a, +oo[) => //.
+  by apply: subset_itvr; rewrite bnd_simp.
+apply: measurable_funM; apply: subspace_continuous_measurable_fun => //.
+exact: (@derivable_oy_continuous_within_itvcy _ R^o).
+Qed.
+
+Let cfG : {within `[a, +oo[, continuous (fun x => (f x * G x)%R)}.
+Proof.
+have/continuous_within_itvcyP[aycf cfa] := cf.
+have/derivable_oy_continuous_within_itvcy/continuous_within_itvcyP[] := Goy.
+move=> aycG cGa.
+apply/continuous_within_itvcyP; split; last exact: cvgM.
+move=> x ax; apply: continuousM; first exact: aycf.
+exact: aycG.
+Qed.
+
+Let mfG : measurable_fun `]a, +oo[ (fun x => (f x * G x)%R).
+Proof.
+apply/measurable_fun_itv_obnd_cbndP.
+exact: subspace_continuous_measurable_fun.
+Qed.
+
+Let Ffai i : {in `]a + i%:R, a + i.+1%:R[%R, F^`() =1 f}.
+Proof. exact/(in1_subset_itv _ Ff)/itvSay. Qed.
+
+Let Ggai i : {in `]a + i%:R, a + i.+1%:R[%R, G^`() =1 g}.
+Proof. exact/(in1_subset_itv _ Gg)/itvSay. Qed.
+
+Let integral_sum_lim :
+ \big[+%R/0%R]_(0 <= i <oo)
+     \int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]) i) (F x * g x)%:E
+ =  (limn (fun n => ((F (a + n.-1%:R) * G (a + n.-1%:R) - F a * G a)%:E
+  + \big[+%R/0%R]_(0 <= i < n) - \int[mu]_(x in
+        seqDU (fun k : nat => `]a, (a + k%:R)]) i) (f x * G x)%:E))).
+Proof.
+apply: congr_lim.
+apply/funext => n.
+case: n.
+  by rewrite big_nat_cond [in RHS]big_nat_cond 2?big_pred0//= 2!addr0 subrr.
+case.
+  rewrite 2!big_nat1 seqDUE -pred_Sn addr0 subrr add0r.
+  by rewrite set_itvoc0 2!integral_set0 oppe0.
+move=> n.
+rewrite big_nat_recl// [in RHS]big_nat_recl//=.
+rewrite seqDUE/= addr0 set_itvoc0 2!integral_set0 oppe0 2!add0r.
+have subset_ai_ay (b b' : bool) i :
+  [set` Interval (BSide b (a + i%:R)) (BSide b' (a + i.+1%:R))] `<=`
+      [set` Interval (BSide b a) (BInfty _ false)].
+  by apply/subitvP; rewrite subitvE bnd_simp; rewrite ?ler_wpDr.
+under eq_bigr => i _.
+  rewrite seqDUE/= integral_itv_obnd_cbnd; last first.
+    exact: (@measurable_funS _ _ _ _ `]a, +oo[).
+    rewrite (integration_by_parts _ _ _ (@Ffai i) _ _ (@Ggai i)); last 5 first.
+    - by rewrite ltrD2l ltr_nat.
+    - exact: continuous_subspaceW cf.
+    - apply: derivable_oy_continuous_bndW_oo Foy.
+      + by rewrite ltrD2l ltr_nat.
+      + by rewrite lerDl.
+    - exact: continuous_subspaceW cg.
+    - apply: derivable_oy_continuous_bndW_oo Goy.
+      + by rewrite ltrD2l ltr_nat.
+      + by rewrite lerDl.
+    over.
+rewrite big_split/=.
+under eq_bigr do rewrite EFinB.
+rewrite telescope_sume// addr0; congr +%E.
+apply: eq_bigr => k _; rewrite seqDUE/= integral_itv_obnd_cbnd//.
+exact: measurable_funS mfG.
+Qed.
+
+Let FGaoo :
+  (F (a + x.-1%:R)%E * G (a + x.-1%:R)%E - F a * G a)%:E @[x --> \oo] -->
+    (FGoo - F a * G a)%:E.
+Proof.
+apply: cvg_EFin; first exact: nearW; apply: (@cvgB _ R^o); last exact: cvg_cst.
+rewrite -cvg_shiftS/=.
+apply: (@cvg_comp _ _ _ _ (F \* G)%R _ +oo%R); last exact: cvgFG; apply/cvgeryP.
+apply: (@cvge_pinftyP R (fun x => (a + x)%:E) +oo).1; last exact: cvgr_idn.
+by apply/cvgeryP; exact: cvg_addrl.
+Qed.
+
+Let sumN_Nsum_fG n :
+ (\sum_(0 <= i < n)
+      (- (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i)
+             (f x * G x)%:E))%E)%R =
+ - (\sum_(0 <= i < n)
+       (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i)
+           (f x * G x)%:E)%E)%R.
+Proof.
+rewrite big_nat_cond fin_num_sumeN; rewrite -?big_nat_cond//; move=> m _.
+rewrite seqDUE integral_itv_obnd_cbnd; last exact: measurable_funS mfG.
+apply: integral_fune_fin_num => //=.
+apply: continuous_compact_integrable; first exact: segment_compact.
+exact: continuous_subspaceW cfG.
+Qed.
+
+Let sumNint_sumintN_fG n :
+ (\sum_(0 <= i < n)
+      (- (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i)
+             (f x * G x)%:E))%E)%R =
+  \sum_(0 <= i < n)
+       (\int[mu]_(x in seqDU (fun k : nat => `]a, (a + k%:R)]%classic) i)
+           (- (f x * G x))%:E)%E.
+Proof.
+rewrite big_nat_cond [RHS]big_nat_cond.
+apply: eq_bigr => i.
+rewrite seqDUE andbT => i0n.
+rewrite 2?integral_itv_obnd_cbnd; last exact: measurable_funS mfG; last first.
+  apply: measurableT_comp => //.
+  exact: measurable_funS mfG.
+rewrite -integralN ?integrable_add_def ?continuous_compact_integrable//.
+  exact: segment_compact.
+exact: continuous_subspaceW cfG.
+Qed.
+
+Lemma integration_by_partsy_ge0_ge0 :
+ {in `]a, +oo[, forall x, 0 <= (f x * G x)%:E} ->
+  {in `]a, +oo[, forall x, 0 <= (F x * g x)%:E} ->
+  \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E -
+  \int[mu]_(x in `[a, +oo[) (f x * G x)%:E.
+Proof.
+move=> fG0 Fg0.
+rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//.
+rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq.
+rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight;
+    last 6 first.
+- by move=> k; apply: measurableD => //; apply: bigsetU_measurable.
+- exact/measurable_EFinP.
+- by move=> ? ?; rewrite fG0// inE.
+- by move=> k; apply: measurableD => //; apply: bigsetU_measurable.
+- exact/measurable_EFinP.
+- by move=> ? ?; rewrite Fg0// inE.
+rewrite integral_sum_lim; apply/cvg_lim => //.
+apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo.
+under eq_cvg do rewrite sumN_Nsum_fG; apply: cvgeN.
+apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x.
+by rewrite seqDUE => anx; apply: fG0; rewrite inE/=; exact/itvSay/anx.
+Qed.
+
+Lemma integration_by_partsy_le0_ge0 :
+  {in `]a, +oo[, forall x, (f x * G x)%:E <= 0} ->
+  {in `]a, +oo[, forall x, 0 <= (F x * g x)%:E} ->
+  \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E +
+  \int[mu]_(x in `[a, +oo[) (- (f x * G x)%:E).
+Proof.
+move=> fG0 Fg0.
+have mMfG : measurable_fun `]a, +oo[ (fun x => (- (f x * G x))%R).
+  exact: measurableT_comp.
+rewrite -integral_itv_obnd_cbnd// -[in RHS]integral_itv_obnd_cbnd//.
+rewrite itv_bndy_bigcup_BRight seqDU_bigcup_eq.
+rewrite 2?ge0_integral_bigcup//= -?seqDU_bigcup_eq -?itv_bndy_bigcup_BRight;
+    last 6 first.
+- by move=> k; apply: measurableD => //; apply: bigsetU_measurable.
+- by apply/measurable_EFinP; exact: measurableT_comp.
+- by move=> ? ?; rewrite EFinN oppe_ge0 fG0// inE.
+- by move=> k; apply: measurableD => //; apply: bigsetU_measurable.
+- exact/measurable_EFinP.
+- by move=> ? ?; rewrite Fg0// inE.
+rewrite integral_sum_lim; apply/cvg_lim => //.
+apply: cvgeD; first exact: fin_num_adde_defr; first exact: FGaoo.
+under eq_cvg do rewrite sumNint_sumintN_fG.
+apply: is_cvg_nneseries_cond => n _ _; apply: integral_ge0 => x.
+rewrite seqDUE => anx; rewrite EFinN oppe_ge0.
+apply: fG0; rewrite inE/=; exact/itvSay/anx.
+Qed.
+
+End integration_by_partsy_ge0.
+
+Section integration_by_partsy_le0.
+Context {R: realType}.
+Notation mu := lebesgue_measure.
+Local Open Scope ereal_scope.
+Local Open Scope classical_set_scope.
+
+Lemma derivable_oy_continuous_bndN (F : R -> R^o) (a : R) :
+  derivable_oy_continuous_bnd F a ->
+  derivable_oy_continuous_bnd (- F)%R a.
+Proof.
+Admitted.
+
+Variables (F G f g : R -> R^o) (a FGoo : R).
+Hypothesis cf : {within `[a, +oo[, continuous f}.
+Hypothesis Foy : derivable_oy_continuous_bnd F a.
+Hypothesis Ff : {in `]a, +oo[%R, F^`() =1 f}.
+Hypothesis cg : {within `[a, +oo[, continuous g}.
+Hypothesis Goy : derivable_oy_continuous_bnd G a.
+Hypothesis Gg : {in `]a, +oo[%R, G^`() =1 g}.
+Hypothesis cvgFG : (F \* G)%R x @[x --> +oo%R] --> FGoo.
+
+Let mFg : measurable_fun `]a, +oo[ (fun x : R => (F x * g x)%R).
+Proof.
+apply: subspace_continuous_measurable_fun => //.
+rewrite continuous_open_subspace// => x ax.
+apply: cvgM.
+  have [+ _]:= Foy; move/derivable_within_continuous.
+  by rewrite continuous_open_subspace//; apply.
+have /continuous_within_itvcyP[+ _] := cg.
+by apply; rewrite inE/= in ax.
+Qed.
+
+Let NintNFg :
+ {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} ->
+  \int[mu]_(x in `[a, +oo[) (F x * g x)%:E =
+  - \int[mu]_(x in `[a, +oo[) (- F x * g x)%:E.
+Proof.
+move=> Fg0.
+rewrite -integral_itv_obnd_cbnd//.
+under eq_integral => x do rewrite -(opprK (F x)) mulNr EFinN.
+rewrite integralN/=; last first.
+  apply: fin_num_adde_defl.
+  apply/EFin_fin_numP; exists 0%R.
+  apply/eqe_oppLRP; rewrite oppe0.
+  apply:integral0_eq => /= x ax.
+  apply: (@ge0_funenegE _ _ `]a, +oo[); last by rewrite inE/=.
+  move=> ?/= ?; rewrite mulNr EFinN oppe_ge0 Fg0//=.
+  by rewrite inE/=.
+rewrite integral_itv_obnd_cbnd//.
+under [X in _ _ X]eq_fun do rewrite mulNr; exact: measurableT_comp.
+Qed.
+
+Lemma integration_by_partsy_le0_le0 :
+ {in `]a, +oo[, forall x, (f x * G x)%:E <= 0} ->
+  {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} ->
+  \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E +
+  \int[mu]_(x in `[a, +oo[) (- (f x * G x)%:E).
+Proof.
+move=> fG0 Fg0.
+rewrite NintNFg//.
+rewrite (@integration_by_partsy_ge0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//; last 6 first.
+- by move=> ?; apply: cvgN; exact: cf.
+- exact: derivable_oy_continuous_bndN.
+- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.
+- by under eq_cvg do rewrite fctE/= mulNr; apply: cvgN.
+- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: fG0.
+- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: Fg0.
+rewrite oppeB; last exact: fin_num_adde_defr.
+rewrite -EFinN opprD 2!opprK mulNr.
+by under eq_integral do rewrite mulNr EFinN.
+Qed.
+
+Lemma integration_by_partsy_ge0_le0 :
+ {in `]a, +oo[, forall x, 0 <= (f x * G x)%:E} ->
+  {in `]a, +oo[, forall x, (F x * g x)%:E <= 0} ->
+  \int[mu]_(x in `[a, +oo[) (F x * g x)%:E = (FGoo - F a * G a)%:E -
+  \int[mu]_(x in `[a, +oo[) (f x * G x)%:E.
+Proof.
+move=> fG0 Fg0.
+rewrite NintNFg//.
+rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//; last 6 first.
+- by move=> ?; apply: cvgN; exact: cf.
+- exact: derivable_oy_continuous_bndN.
+- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.
+- by under eq_cvg do rewrite fctE/= mulNr; apply: cvgN.
+- by move=> ? ?; rewrite mulNr EFinN oppe_le0; apply: fG0.
+- by move=> ? ?; rewrite mulNr EFinN oppe_ge0; apply: Fg0.
+rewrite oppeD; last exact: fin_num_adde_defr.
+rewrite -EFinN opprD 2!opprK mulNr.
+by under eq_integral do rewrite mulNr EFinN oppeK.
+Qed.
+
+End integration_by_partsy_le0.
+
 Section Rintegration_by_parts.
 Context {R : realType}.
 Notation mu := lebesgue_measure.