Generalize integration_by_parts #1674

IshiguroYoshihiro · 2025-07-04T08:24:46Z

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 · 2025-07-15T07:51:01Z

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

IshiguroYoshihiro · 2025-07-28T07:15:45Z

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 · 2025-10-30T09:35:48Z

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 · 2025-10-30T09:37:11Z

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 · 2025-11-03T12:23:49Z

theories/ftc.v

+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.


Suggested change

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.

apply: (@cvg_comp _ _ _ _ (F \* G)%R _ +oo%R); last exact: cvgFG.

by apply: cvg_comp; [apply: cvgr_idn|apply: cvg_addrl].

Tragicus · 2025-11-03T12:33:32Z

theories/ftc.v

+      (\int[mu]_(x in seqDU (fun k => `]a, a + k%:R]) i)
+        (f x * G x)%:E)%E).
+Proof.
+rewrite big_nat_cond fin_num_sumeN; rewrite -?big_nat_cond//; move=> m _.


Suggested change

rewrite big_nat_cond fin_num_sumeN; rewrite -?big_nat_cond//; move=> m _.

rewrite big_nat_cond fin_num_sumeN -?big_nat_cond// => m _.

Tragicus · 2025-11-03T12:33:55Z

theories/ftc.v

+apply: integrable_fin_num => //=.
+apply: continuous_compact_integrable; first exact: segment_compact.
+apply: continuous_subspaceW cfG.
+by apply/subset_itv => //; rewrite bnd_simp// lerDl.


Suggested change

by apply/subset_itv => //; rewrite bnd_simp// lerDl.

by apply: subset_itv; rewrite // bnd_simp// lerDl.

Tragicus · 2025-11-03T12:50:05Z

theories/ftc.v

+  apply: measurableT_comp => //.
+  apply: measurable_funS mfG => //.
+  by apply/subset_itv; rewrite bnd_simp// lerDl.
+  apply: measurable_funS mfG => //.


Suggested change

apply: measurableT_comp => //.

apply: measurable_funS mfG => //.

by apply/subset_itv; rewrite bnd_simp// lerDl.

apply: measurable_funS mfG => //.

- apply: measurableT_comp => //; apply: measurable_funS mfG => //.

by apply/subset_itv; rewrite bnd_simp// lerDl.

- apply: measurable_funS mfG => //.

Tragicus · 2025-11-03T12:50:33Z

theories/ftc.v

+apply: continuous_subspaceW cfG.
+by apply/subset_itv; rewrite bnd_simp// lerDl.


Suggested change

apply: continuous_subspaceW cfG.

by apply/subset_itv; rewrite bnd_simp// lerDl.

by apply: continuous_subspaceW cfG; apply/subset_itv; rewrite bnd_simp// lerDl.

Tragicus · 2025-11-03T13:44:53Z

theories/ftc.v

+move=> fG0 Fg0.
+rewrite NintNFg//.


Suggested change

move=> fG0 Fg0.

rewrite NintNFg//.

move=> fG0 Fg0; rewrite NintNFg//.

Tragicus · 2025-11-03T13:47:24Z

theories/ftc.v

+  by under eq_integral do rewrite mulNr EFinN.
+- by move=> ?; apply: cvgN; exact: cf.
+- exact: derivable_oy_continuous_bndN.
+- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.


Suggested change

- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.

- by move=> ? ?; rewrite fctE derive1N ?Ff => [//|//|]; apply: Foy.1.

.7s faster

Tragicus · 2025-11-03T13:51:32Z

theories/ftc.v

+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.


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//; move: Foy => [+ _]; apply.

- by [].

- by [].

- by [].

1.5s faster

Tragicus · 2025-11-03T13:53:25Z

theories/ftc.v

+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.


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

Tragicus · 2025-11-03T13:59:10Z

theories/realfun.v

+Lemma derivable_oy_continuous_bndN (f : R -> V) (x : R) :
+  derivable_oy_continuous_bnd f x -> derivable_oy_continuous_bnd (- f) x.
+Proof.
+move=> [/= derF Fa]; split; last exact: cvgN.


Suggested change

move=> [/= derF Fa]; split; last exact: cvgN.

case=> /= derF Fa; split; last exact: cvgN.

IshiguroYoshihiro and others added 2 commits October 30, 2025 15:46

integration_by_party

cdc9e90

upd and rebase

0802b9c

affeldt-aist force-pushed the integration_by_partsy_20250704 branch from 949b179 to 0802b9c Compare October 30, 2025 07:07

lint

675d017

affeldt-aist marked this pull request as ready for review October 30, 2025 09:32

Tragicus reviewed Nov 3, 2025

View reviewed changes

affeldt-aist added this to the 1.15.0 milestone Nov 4, 2025

affeldt-aist added the enhancement ✨ This issue/PR is about adding new features enhancing the library label Nov 4, 2025

	rewrite big_nat_cond fin_num_sumeN; rewrite -?big_nat_cond//; move=> m _.
	rewrite big_nat_cond fin_num_sumeN -?big_nat_cond// => m _.

	by apply/subset_itv => //; rewrite bnd_simp// lerDl.
	by apply: subset_itv; rewrite // bnd_simp// lerDl.

		apply: continuous_subspaceW cfG.
		by apply/subset_itv; rewrite bnd_simp// lerDl.

	apply: continuous_subspaceW cfG.
	by apply/subset_itv; rewrite bnd_simp// lerDl.
	by apply: continuous_subspaceW cfG; apply/subset_itv; rewrite bnd_simp// lerDl.

	move=> fG0 Fg0.
	rewrite NintNFg//.
	move=> fG0 Fg0; rewrite NintNFg//.

	- by move=> ? ?; rewrite fctE derive1N ?Ff//; move: Foy => [+ _]; apply.
	- by move=> ? ?; rewrite fctE derive1N ?Ff => [//\|//\|]; apply: Foy.1.

	move=> [/= derF Fa]; split; last exact: cvgN.
	case=> /= derF Fa; split; last exact: cvgN.

Generalize integration_by_parts #1674

Are you sure you want to change the base?

Generalize integration_by_parts #1674

Uh oh!

Conversation

IshiguroYoshihiro commented Jul 4, 2025

Motivation for this change

Checklist

Merge policy

Reminder to reviewers

Uh oh!

Tragicus commented Jul 15, 2025

Uh oh!

IshiguroYoshihiro commented Jul 28, 2025

Uh oh!

affeldt-aist commented Oct 30, 2025

Uh oh!

affeldt-aist commented Oct 30, 2025

Uh oh!

Tragicus left a comment

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

3 participants