[affeldt-aist]

Motivation for this change

This PR introduces a definition of measure induced by a measurable function,
similarly to the notion of signed measure induced by an integrable function in radon_nikodym.v.
The code is essentially coming from PR #2116 as one step towards its review.
It is used twice in PR #2116, hence justifying this PR.

fyi: @lyonel2017

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

[IshiguroYoshihiro]

I think that this PR is worth merging, but the name induced measure could be reconsidered.

This PR introduces a measure with a density function. It is related to the Radon–Nikodym derivative.
The files in the probability_theory directory will benefit the most, because some well-known probability measures, such as normal_prob, are formalized with density functions and can have their definitions rewritten using induced measures.

However, the term ‘induced measure’ as used in this PR may cause confusion.
‘Induced measure’ are sometimes used to refer to pushforward measures, which are not the same as measure with density functions. So, users may not be able to understand which kind of measure ‘induced measure’ refers to from its name.

[IshiguroYoshihiro]

By definition, this f can be called a density function of the induced measure.
How about writing it in the description?

[IshiguroYoshihiro]

induced_measure is analogous to lebesgue_stieltjes_measure. The difference is that induced_measure uses its density function, whereas lebesgue_stieltjes_measure uses its cumulative function.
It would be useful to clarify the difference between lebesgue_stieltjes_measure and induced_measure.

[affeldt-aist]

It is a bit difficult to draw a parallel in the documentation because lebesgue_stieltjes_measure is defined using measure_extension instead of integral.

[affeldt-aist]

@IshiguroYoshihiro

Thank you very much for the review!
I have applied your comments and in particular renamed induced_measure with measure_of_density
(and induced_charge with charge_of_density).
I have also used measure_of_density to change the definition of normal_prob as you suggested.

fyi: @lyonel2017 @strub