gen of int. by subst + normal distribution

[affeldt-aist]

Motivation for this change

PR #1448 should be merged first merged

to be cleaned @IshiguroYoshihiro

The goal of this PR is to provide integration by substitution over unbounded intervals
to compute integrals.

We already had the following lemmas for integration by substitution:

• integration_by_substitution_decreasing:
  over [F b, F a], decreasing change of vars F
• integration_by_substitution_oppr:
  over [-b, -a], change of vars (fun x => - x)
• integration_by_substitution_increasing:
  over [F a, F b], increasing change of vars F

This PR adds integration by substitution for non-negative functions over rays:

• decreasing_ge0_integration_by_substitutiony:
  over ]-oo, F a], decreasing change of vars F
• ge0_integration_by_substitutionNy:
  over ]-oo, -a], change of vars (fun x => - x)
• increasing_ge0_integration_by_substitutiony:
  over [F a, +oo[, increasing change of vars F
  (proved using above lemmas and the properties of negation)
• increasing_ge0_integration_by_substitutionNy:
  over ]-oo, F b], increasing change of vars F
  (proved using above lemmas and the properties of negation)
• increasing_ge0_integration_by_substitutionT:
  over ]-oo, +oo[, increasing change of vars F
  (proved using above lemmas)

Checklist

• added corresponding entries in CHANGELOG_UNRELEASED.md

• added corresponding documentation in the headers

Reference: How to document

Reminder to reviewers

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

[affeldt-aist]

@IshiguroYoshihiro I asked Saikawa-san to take a look, but could you also check the contents of this PR?

[affeldt-aist]

(CI says red but actually compiles fine on my machine with Coq 8.20 and Coq 8.19...) fixed

[affeldt-aist]

@IshiguroYoshihiro no input about this PR?

[affeldt-aist]

@t6s maybe I can add a piece of LaTeXed documentation as for the PR you already just reviewed.

[affeldt-aist]

@t6s maybe I can add a piece of LaTeXed documentation as for the PR you already just reviewed.

[affeldt-aist]

We have also added the normal distribution has a direct application.

[t6s]

As an impression from the latex header doc, the statements of the added lemmas look good.
The lemma integralT_gauss is a serious example, and I expect that its proof provide a good test for the added lemmas.
I therefore would like to approve this PR although I myself have not checked all the changes by running them.

[t6s]

A minor comment: integralT_gauss deserves to be a Theorem not merely a Lemma.