Generalize integration_by_parts

[IshiguroYoshihiro]

Motivation for this change

Add a part of generalized version of integration by parts for unbound intervals `[a, +oo[.
This PR is over #1656 and #1662.
I don't sure that I should add 4 more lemmas and complete all variation of integration by parts for unbound intervals.
I think that 8 similar lemmas would be a mess. So, I'd like to somehow make them up into one or two lemmas, but I don't have an idea.

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Merge policy

As a rule of thumb:

• PRs with several commits that make sense individually and that
  all compile are preferentially merged into master.
• PRs with disorganized commits are very likely to be squash-rebased.

Reminder to reviewers

• Read this Checklist
• Put a milestone if possible
• Check labels

[Tragicus]

Are not all 4 versions the same, the only difference being whether the minus is inside or outside the integral?

[IshiguroYoshihiro]

Are not all 4 versions the same, the only difference being whether the minus is inside or outside the integral?

If you said that these lemmas can be proved with one of them, I think it is no.
As you can see, the version of le0_ge0 and le0_le0 can be proved with ge0_ge0 or ge0_le0, but ge0_le0 can not proved from ge0_ge0.
Because that integration by substitusion using a transformation F -> F \o -%R change the unbounded side of the interval from `[a, +oo[ to `[-oo, - a[, I may have to set 4 more variations of this lemma for `[-oo, -a[.
It will makes messy for the use to set 8 variation of the lemma. So I will consider some good way.

[affeldt-aist]

Are not all 4 versions the same, the only difference being whether the minus is inside or outside the integral?

Indeed le0_le0 is the same as ge0_ge0 (and it is proved as such).
Similarly, for ge0_le0 vs. le0_ge0.
I don't think we can have more sharing.
Do you think that we should work towards a general version? A single lemma encompassing them all?

[affeldt-aist]

Are not all 4 versions the same, the only difference being whether the minus is inside or outside the integral?

Indeed le0_le0 is the same as ge0_ge0 (and it is proved as such). Similarly, for ge0_le0 vs. le0_ge0. I don't think we can have more sharing. Do you think that we should work towards a general version? A single lemma encompassing them all?

To give a bit of context, these lemmas have been written this way after having been tested to formalize the Gamma function. Maybe their apparent specialization is the result of practical considerations? @IshiguroYoshihiro can you confirm? (Or am I remembering wrong?)

[Tragicus]

Sorry, I am back.
One way to factorize would be to ask for the relevant functions to have constant sign. I was also wondering whether we want to generalize over the interval, instead of [a, +oo[. We would require that the relevant functions are derivable on the interior of the interval and have limits at the boundaries.
@affeldt-aist Some of the following suggestions are quite ugly but save a lot of time, what do you think?

[Tragicus]

Suggested change

	rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//.
	- rewrite oppeD; last exact: fin_num_adde_defr.
	rewrite -EFinN opprD 2!opprK mulNr.
	by under eq_integral do rewrite mulNr EFinN oppeK.
	- by move=> ?; apply: cvgN; exact: cf.
	- exact: derivable_oy_continuous_bndN.
	- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.
	rewrite (@integration_by_partsy_le0_ge0 R (- F)%R G (- f)%R g a (- FGoo))//.
	- rewrite oppeD; last exact: fin_num_adde_defr.
	rewrite -EFinN opprD 2!opprK mulNr.
	by under eq_integral do rewrite mulNr EFinN oppeK.
	- by move=> ?; apply: cvgN; exact: cf.
	- exact: derivable_oy_continuous_bndN.
	- by move=> ? ?; rewrite fctE derive1N ?Ff => [//|//|]; apply: Foy.1.

.6s faster

[affeldt-aist]

To give a bit of context, these lemmas have been written this way after having been tested to formalize the Gamma function.

FYI, here is the PR that formalizes the Gamma function:
#1762

One way to factorize would be to ask for the relevant functions to have constant sign. I was also wondering whether we want to generalize over the interval, instead of [a, +oo[. We would require that the relevant functions are derivable on the interior of the interval and have limits at the boundaries.

This has not been tested yet (by lack of time). :-(

Some of the following suggestions are quite ugly but save a lot of time, what do you think?

We have merged all of them. Thanks for identifying the performance issues, that helps.

[t6s]

I suggest keeping 4 lemmas as is, and additionally, provide a unified interface lemma that use the constant_sign predicate

[t6s]

looking at the code for a while, I noticed there can be some helper lemmas added:

Lemma seqDU0 : forall {T : Type} (F : (set T)^nat), seqDU F 0%N = F 0%N.
Proof. by move=> ? ?; rewrite /seqDU/= big_ord0 setD0. Qed.

Lemma seqDU1_itv : forall {R : realDomainType} (r : R) b1 b2,
  seqDU (fun n => [set` Interval (BSide b1 r) (BSide b2 (r + n%:R))]) 1 =
  [set` Interval (BSide (b1 && b2) r) (BSide b2 (r + 1%:R))].
Proof.
move=> ? r b1 b2.
rewrite /seqDU big_ord1/= addr0 setDE.
case: b1; case: b2; rewrite (set_itvco0,set_itv1,set_itvoo0,set_itvoc0) ?setC0 ?setIT//.
by rewrite -setDE setDitv1l.
Qed.

Lemma seqDUSn_itv_notoo : forall {R : realDomainType} n (r : R) b1 b2,
  (b1 == true) || (b2 == false) -> (* not a seqDU of open intervals *)
  seqDU (fun n => [set` Interval (BSide b1 r) (BSide b2 (r + n%:R))]) n.+1 =
  [set` Interval (BSide b2 (r + n%:R)) (BSide b2 (r + n.+1%:R))].
Proof.
move=> ? n r b1 b2 b12.
rewrite seqDU_seqD; last first.
  apply/nondecreasing_seqP => k; apply/subsetPset/subset_itvl.
  by rewrite bnd_simp lerD2l ler_nat.
rewrite eqEsubset; split => x /= /[!in_itv] /=.
  move=> [] /andP[-> ->] /[!andbT] /= /negP.
  clear b12.
  by case: b1; case: b2; rewrite /= -?ltNge -?leNgt.
move=> /andP[rnx ->]; rewrite andbT; split.
  move: b12.
  case: b1 => /=.
    by move=> _; have/lteifW/(le_trans _) := rnx; apply; rewrite lerDl.
  by move: rnx; case: b2 => //= + _  => /(le_lt_trans _); apply; rewrite lerDl.
by apply/negP; rewrite negb_and [X in _ || X]lteifN ?negbK// orbT.
Qed.

Lemma seqDUSSn_itv : forall {R : realDomainType} n (r : R) b1 b2,
  seqDU (fun n => [set` Interval (BSide b1 r) (BSide b2 (r + n%:R))]) n.+2 =
  [set` Interval (BSide b2 (r + n.+1%:R)) (BSide b2 (r + n.+2%:R))].
Proof.
move=> ? n r b1 b2.
case/boolP: ((b1 == true) || (b2 == false)); first by move/seqDUSn_itv_notoo.
case: b1; case: b2 => // _.
rewrite seqDU_seqD; last first.
  apply/nondecreasing_seqP => k; apply/subsetPset/subset_itvl.
  by rewrite bnd_simp lerD2l ler_nat.
rewrite eqEsubset; split => x /= /[!in_itv] /=.
  by move=> [] /andP[-> ->] /[!andbT] /= /negP; rewrite -leNgt.
move=> /andP[rnx ->].
rewrite andbT; split; first by rewrite (lt_le_trans _ rnx)// ltrDl.
by apply/negP; rewrite negb_and -!leNgt rnx orbT.
Qed.

Lemma set_itv_Sset1 :
  forall [disp : Order.disp_t] [T : porderType disp] (x : T) b1 b2 ,
    [set` Interval (BSide b1 x) (BSide b2 x)] `<=` [set x].
Proof.
move=> ? ? ? b1 b2.
by case: b1; case: b2; rewrite (set_itv1,set_itvoo0,set_itvxx).
Qed.

Lemma seqDUn_sSet_itvcc : forall {R : realDomainType} n (r : R) b1 b2,
  seqDU (fun n => [set` Interval (BSide b1 r) (BSide b2 (r + n%:R))]) n `<=`
    `[r + n.-1%:R, r + n%:R].
Proof.
move=> ? n r b1 b2.
case: n => [|n /=].
  by rewrite seqDU0 addr0; apply: subset_itvScc; rewrite bnd_simp.
case: n => [|n /=].
  by rewrite seqDU1_itv addr0; apply: subset_itvScc; rewrite bnd_simp.
by rewrite seqDUSSn_itv; apply: subset_itvScc; rewrite bnd_simp.
Qed.

(* generalizations of lemmas of the same names *)
Lemma integral_itv_obnd_cbnd :
  forall {R : realType} [r : R] [b : itv_bound R] [f : R -> R] lr,
    measurable_fun [set` Interval (BRight r) b] f ->
    \int[mu]_(x in [set` Interval (BSide lr r) b]) (f x)%:E =
    \int[mu]_(x in [set` Interval (BLeft r) b]) (f x)%:E.
Proof. by move=> ? ? ? ?; case; [by []|exact: integral_itv_obnd_cbnd]. Qed.

Lemma integral_itv_bndo_bndc :
  forall {R : realType} [a : itv_bound R] [r : R] [f : R -> R] lr,
    measurable_fun [set` Interval a (BLeft r)] f ->
    \int[mu]_(x in [set` Interval a (BSide lr r)]) (f x)%:E =
    \int[mu]_(x in [set` Interval a (BRight r)]) (f x)%:E.
Proof. by move=> ? ? ? ?; case; [exact: integral_itv_bndo_bndc|by []]. Qed.

Lemma measurable_fun_itv_bnd :
  forall [R : realType] [x y : R] [b1 b2 b3 b4 : bool] [f : R -> R],
  measurable_fun [set` Interval (BSide b1 x) (BSide b2 y)] f ->
  measurable_fun [set` Interval (BSide b3 x) (BSide b4 y)] f.
Proof.
move=> ? x y ? ? ? ? ? f_measurable.
apply: (measurable_funS `[x, y]) => //.
  by apply: subset_itvScc; rewrite bnd_simp.
exact: (measurable_fun_itv_cc f_measurable).
Qed.

Lemma integral_itv_bnd :
  forall {R : realType} [x y : R] [f : R -> R] (b1 b2 b3 b4 : bool),
  measurable_fun `]x, y[ f ->
  \int[mu]_(z in [set` Interval (BSide b1 x) (BSide b2 y)]) (f z)%:E =
  \int[mu]_(z in [set` Interval (BSide b3 x) (BSide b4 y)]) (f z)%:E.
Proof.
move=> ? x y ? ? ? ? ? f_measurable.
do 2 (rewrite integral_itv_bndo_bndc; last exact: (measurable_fun_itv_bnd f_measurable)).
do 2 (rewrite integral_itv_obnd_cbnd; last exact: (measurable_fun_itv_bnd f_measurable)).
by [].
Qed.

Lemma integral_itv_bndcc :
  forall {R : realType} [x y : R] [f : R -> R] (b1 b2: bool),
  measurable_fun `]x, y[ f ->
  \int[mu]_(z in [set` Interval (BSide b1 x) (BSide b2 y)]) (f z)%:E =
  \int[mu]_(z in `[x, y]) (f z)%:E.
Proof. move=> *; exact: integral_itv_bnd. Qed.

[t6s]

Section integralN.
Local Open Scope order_scope.

Lemma lef0_integralN
  {d : measure_display} {T : measurableType d} {R : realType} {mu : measure T R}
  (D : set T) (f : T -> \bar R) :
  d.-measurable D ->
  {in D, forall x, f x <= 0} ->
  (\int[mu]_(x in D) - f x)%E = (- (\int[mu]_(x in D) f x))%E.
Proof.
move=> mD lef0; rewrite integralN// fin_num_adde_defr//.
under eq_integral => ? ?.
  by rewrite (le0_funeposE lef0); first over; rewrite inE.
by rewrite integral_cst// mul0e.
Qed.

Lemma le0f_integralN
  {d : measure_display} {T : measurableType d} {R : realType} {mu : measure T R}
  (D : set T) (f : T -> \bar R) :
  d.-measurable D ->
  {in D, forall x, 0%E <= f x} ->
  (\int[mu]_(x in D) - f x)%E = (- (\int[mu]_(x in D) f x))%E.
Proof.
move=> mD le0f; rewrite integralN// fin_num_adde_defl//.
under eq_integral => ? ?.
  by rewrite (ge0_funenegE le0f); first over; rewrite inE.
by rewrite integral_cst// mul0e.
Qed.

End integralN.

[t6s]

leading to generalization of sum_integral_limn:

Let sumN_Nsum_fG n b1 b2 :
  (b1 == true) || (b2 == false) ->
  \sum_(0 <= i < n)
    (- (\int[mu]_(x in seqDU (fun k => [set` Interval (BSide b1 a) (BSide b2 (a + k%:R))]) i)
         (f x * G x)%:E))%E =
  - (\sum_(0 <= i < n)
      (\int[mu]_(x in seqDU (fun k => [set` Interval (BSide b1 a) (BSide b2 (a + k%:R))]) i)
        (f x * G x)%:E)%E).
Proof.
move=> b12.
rewrite big_nat_cond fin_num_sumeN -?big_nat_cond// => m _.
case: m => [|m].
  by rewrite seqDU0 addr0 (integral_Sset1 a)//; exact: set_itv_Sset1.
rewrite seqDUSn_itv_notoo//.
rewrite integral_itv_bndcc; last first.
  apply: (measurable_funS `[a, +oo[) => //.
  by apply/subset_itv => //; rewrite bnd_simp// lerDl.
apply: integrable_fin_num => //=.
apply: continuous_compact_integrable; first exact: segment_compact.
apply: continuous_subspaceW cfG.
by apply: subset_itv; rewrite // bnd_simp// lerDl.
Qed.

Let sum_integral_limn b1 b2 :
  (b1 == true) || (b2 == false) ->
  \sum_(0 <= i <oo)
    \int[mu]_(x in seqDU (fun k => [set` Interval (BSide b1 a) (BSide b2 (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
                    + \sum_(0 <= i < n)
                    - \int[mu]_(x in seqDU (fun k => [set` Interval (BSide b1 a) (BSide b2 (a + k%:R))]) i)
                        (f x * G x)%:E).
Proof.
move=> b12.
apply/congr_lim/funext; case.
  by rewrite big_nat_cond [in RHS]big_nat_cond 2?big_pred0//= 2!addr0 subrr.
case=> [|n].
  rewrite 2!big_nat1 seqDU0 -pred_Sn addr0 subrr add0r.
  rewrite !(integral_Sset1 a) ?oppe0//; exact: set_itv_Sset1.
rewrite big_nat_recl// [in RHS]big_nat_recl//=.
rewrite seqDU0 addr0 !(integral_Sset1 a); [|exact: set_itv_Sset1|exact: set_itv_Sset1].
rewrite oppe0 2!add0r.
under eq_bigr => i _.
  rewrite seqDUSn_itv_notoo//= (integral_itv_bndcc b2 b2); last first.
    apply: (measurable_funS `[a, +oo[) => //.
    by apply/subset_itv => //; rewrite bnd_simp lerDl.
  rewrite (integration_by_parts _ _ _ (@Ffai i) _ _ (@Ggai i)); last 5 first.
  - by rewrite ltrD2l ltr_nat.
  - apply: continuous_subspaceW cf.
    by apply/subset_itv => //; rewrite bnd_simp lerDl.
  - apply: derivable_oy_continuousWoo Foy.
    + by rewrite ltrD2l ltr_nat.
    + by rewrite lerDl.
  - apply: continuous_subspaceW cg.
    by apply/subset_itv => //; rewrite bnd_simp lerDl.
  - apply: derivable_oy_continuousWoo Goy.
    + by rewrite ltrD2l ltr_nat.
    + by rewrite lerDl.
  over.
rewrite big_split/=.
under eq_bigr do rewrite EFinB.
rewrite telescope_sume => [|//|//]; rewrite addr0; congr +%E.
apply: eq_bigr => k _; rewrite seqDUSn_itv_notoo; last by [].
rewrite [in RHS]integral_itv_bndcc; first by [].
apply: measurable_funS mfG => //.
by apply/subset_itv => //; rewrite bnd_simp lerDl.
Qed.

[affeldt-aist]

looking at the code for a while, I noticed there can be some helper lemmas added:
...

on our side, we were trying to get rid of seqDU that does not seem to be here for good reasons :-/

[t6s]

looking at the code for a while, I noticed there can be some helper lemmas added:
...

on our side, we were trying to get rid of seqDU that does not seem to be here for good reasons :-/

that sounds better

[t6s]

I suggest keeping 4 lemmas as is, and additionally, provide a unified interface lemma that use the constant_sign predicate

I have changed my mind to endorse constant_sign, as this notion can be handily expressed
by (f <= 0) || (0 <= f) using FunOrder.lef, and moreover, it contradicts Num.sgr.

[t6s]

The main lemmas look good.
After trying to remove subset_itvoSo_cSc, this PR will be ready for merging.

[t6s]

This lemma can be an instance of the monotonicity of the closure operator.

[t6s]

This section appears to be sharing many things with the previous one.
Maybe merge the two?