equal
deleted
inserted
replaced
4 Provides lemmas for integration by substitution for the basic integral types. |
4 Provides lemmas for integration by substitution for the basic integral types. |
5 Note that the substitution function must have a nonnegative derivative. |
5 Note that the substitution function must have a nonnegative derivative. |
6 This could probably be weakened somehow. |
6 This could probably be weakened somehow. |
7 *) |
7 *) |
8 |
8 |
9 section \<open>Integration by Substition for the Lebesgue integral\<close> |
9 section \<open>Integration by Substition for the Lebesgue Integral\<close> |
10 |
10 |
11 theory Lebesgue_Integral_Substitution |
11 theory Lebesgue_Integral_Substitution |
12 imports Interval_Integral |
12 imports Interval_Integral |
13 begin |
13 begin |
14 |
14 |