intervalIntegral.intervalIntegrable_rpow
theorem intervalIntegral.intervalIntegrable_rpow :
∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [inst : MeasureTheory.IsLocallyFiniteMeasure μ] {r : ℝ},
0 ≤ r ∨ 0 ∉ Set.uIcc a b → IntervalIntegrable (fun x => x ^ r) μ a b
The theorem `intervalIntegral.intervalIntegrable_rpow` states that for any two real numbers `a` and `b`, a measure `μ` which is locally finite, and a real number `r`, the function `x ↦ x ^ r` is interval integrable with respect to `μ` on the unordered interval `a..b` if either `r` is nonnegative or `0` is not in the interval `a..b` (inclusive). The term "interval integrable" here means that the function is integrable on the intervals `(min a b, max a b]` and `(max a b, min a b]`. One of these intervals is always empty, so this property is essentially saying that the function is integrable on `(min a b, max a b]`.
More concisely: For any locally finite measure μ, real numbers a < b, and real number r ≥ 0, the function x → x^r is interval integrable with respect to μ on the unordered interval a..b.
|
integral_sin_pow
theorem integral_sin_pow :
∀ {a b : ℝ} (n : ℕ),
∫ (x : ℝ) in a..b, x.sin ^ (n + 2) =
(a.sin ^ (n + 1) * a.cos - b.sin ^ (n + 1) * b.cos) / (↑n + 2) +
(↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, x.sin ^ n
The theorem `integral_sin_pow` states the reduction formula for the integral of `sin(x)^n` for any natural number `n` greater than or equal to 2. Specifically, the integral from `a` to `b` of `sin(x)^(n+2)` is equal to the difference of the product of `sin(a)^(n+1)` and `cos(a)`, and the product of `sin(b)^(n+1)` and `cos(b)`, all divided by `n+2`, plus the product of `n+1` and the integral from `a` to `b` of `sin(x)^n`, all divided by `n+2`.
More concisely: For any natural number `n` greater than or equal to 2, the integral of `sin(x)^n` from `a` to `b` is equal to [(sin(a)^(n+1)*cos(a) - sin(b)^(n+1)*cos(b)) / (n+2)] + [(n+1)/(n+2)] * integral from `a` to `b` of `sin(x)^n`.
|
intervalIntegral.intervalIntegrable_cpow
theorem intervalIntegral.intervalIntegrable_cpow :
∀ {a b : ℝ} {μ : MeasureTheory.Measure ℝ} [inst : MeasureTheory.IsLocallyFiniteMeasure μ] {r : ℂ},
0 ≤ r.re ∨ 0 ∉ Set.uIcc a b → IntervalIntegrable (fun x => ↑x ^ r) μ a b
The theorem `intervalIntegral.intervalIntegrable_cpow` states that for any real numbers `a` and `b`, a measure `μ` on the real numbers that is locally finite, and a complex number `r`, if either the real part of `r` is non-negative or zero is not included in the "unordered" interval between `a` and `b` (inclusive), then the function which maps each real number `x` to `x` raised to the power `r` (where `x` is considered as a complex number) is interval integrable with respect to the measure `μ` on the interval from `a` to `b`. The "unordered" interval between `a` and `b` is defined as the set of all real numbers between the minimum and maximum of `a` and `b`, inclusive. "Interval integrable" means that the function is integrable on both the open interval from `a` to `b` and the open interval from `b` to `a`.
More concisely: For any locally finite measure μ on the real numbers and complex numbers r with non-negative real part, or zero not contained in the interval [a, b], the function x ↔ x^r is interval integrable with respect to μ on the interval [a, b].
|
integral_cos_pow
theorem integral_cos_pow :
∀ {a b : ℝ} (n : ℕ),
∫ (x : ℝ) in a..b, x.cos ^ (n + 2) =
(b.cos ^ (n + 1) * b.sin - a.cos ^ (n + 1) * a.sin) / (↑n + 2) +
(↑n + 1) / (↑n + 2) * ∫ (x : ℝ) in a..b, x.cos ^ n
This theorem states the reduction formula for the definite integral of cosine to the power of `n` (where `n` is a natural number greater than or equal to 2) with respect to `x` from `a` to `b`. The integral of `cos x ^ (n + 2)` equals the term `(b.cos ^ (n + 1) * b.sin - a.cos ^ (n + 1) * a.sin) / (n + 2)` plus the term `((n + 1) / (n + 2))` multiplied by the integral of `cos x ^ n` from `a` to `b`. The theorem provides a way to reduce the complexity of the integral by reducing the power of the cosine function.
More concisely: The definite integral of cos^(n+2) dx from a to b equals [(b.cos^(n+1) * b.sin - a.cos^(n+1) * a.sin) / (n+2)] + ((n+1) / (n+2)) * integral of cos^n dx from a to b, where n is a natural number greater than or equal to 2.
|
integral_inv
theorem integral_inv : ∀ {a b : ℝ}, 0 ∉ Set.uIcc a b → ∫ (x : ℝ) in a..b, x⁻¹ = (b / a).log
This theorem, `integral_inv`, states that for any two real numbers `a` and `b`, if zero does not lie in the set of elements between `a` and `b` (inclusive), then the integral of the function `x⁻¹` (the reciprocal of `x`) from `a` to `b` is equal to the logarithm of `b` divided by `a`. In mathematical terms, it says that if 0 is not in the closed interval [a, b], then the definite integral from `a` to `b` of `1/x` dx equals to the natural logarithm of `b / a`.
More concisely: If the interval [a, b] in the real numbers excludes zero, then ∫(1/x dx) = ln(b/a).
|
intervalIntegral.integrableOn_Ioo_rpow_iff
theorem intervalIntegral.integrableOn_Ioo_rpow_iff :
∀ {s t : ℝ}, 0 < t → (MeasureTheory.IntegrableOn (fun x => x ^ s) (Set.Ioo 0 t) MeasureTheory.volume ↔ -1 < s) := by
sorry
The theorem `intervalIntegral.integrableOn_Ioo_rpow_iff` states that for any real numbers `s` and `t` where `t` is positive, the power function `x ↦ x^s` is integrable on the open interval `(0, t)` (meaning the function is almost everywhere strongly measurable on this interval and the integral of the pointwise norm over this interval is less than infinity) if and only if `s` is greater than `-1`. In other words, the integral of `x^s` from `0` to `t` exists and is a finite real number if `s > -1`.
More concisely: The power function x ↦ x^s is integrable on the open interval (0, t) if and only if s > -1.
|
integral_sin_pow_mul_cos_pow_odd
theorem integral_sin_pow_mul_cos_pow_odd :
∀ {a b : ℝ} (m n : ℕ),
∫ (x : ℝ) in a..b, x.sin ^ m * x.cos ^ (2 * n + 1) = ∫ (u : ℝ) in a.sin..b.sin, u ^ m * (1 - u ^ 2) ^ n
This theorem, named `integral_sin_pow_mul_cos_pow_odd`, describes a simplification of an integral involving the powers of sine and cosine functions. More specifically, for any real numbers `a` and `b`, and natural numbers `m` and `n`, the integral from `a` to `b` of `sin(x)^m * cos(x)^(2n+1)` is equal to the integral from `sin(a)` to `sin(b)` of `u^m * (1 - u^2)^n`. In other words, it transforms an integral involving both sine and cosine to an equivalent integral involving only sine, which could simplify its computation. This is particularly useful when `n` is odd.
More concisely: For any real numbers `a` and `b` and natural numbers `m` and `n`, the integral from `a` to `b` of `sin(x)^m * cos(x)^(2n+1)` equals the integral from `sin(a)` to `sin(b)` of `u^m * (1 - u^2)^n`.
|
integral_pow_abs_sub_uIoc
theorem integral_pow_abs_sub_uIoc :
∀ {a b : ℝ} (n : ℕ), ∫ (x : ℝ) in Ι a b, |x - a| ^ n = |b - a| ^ (n + 1) / (↑n + 1)
This theorem states that the integral of the absolute difference between `x` and `a` raised to power `n` over the interval from `a` to `b` is equal to the absolute difference between `b` and `a` raised to the power `n + 1`, divided by `n + 1`. This particular integral is used in the proof of the Picard-Lindelöf/Cauchy-Lipschitz theorem. In terms of mathematical notation, it would look like:
For all real numbers `a` and `b` and for all natural numbers `n`,
∫ from a to b of |x - a|^n dx = |b - a|^(n + 1) / (n + 1)
More concisely: For all real numbers `a`, `b`, and natural number `n`, the integral of `|x - a|^n` from `a` to `b` equals `|b - a|^{n+1} / (n + 1)`.
|
intervalIntegral.intervalIntegrable_rpow'
theorem intervalIntegral.intervalIntegrable_rpow' :
∀ {a b r : ℝ}, -1 < r → IntervalIntegrable (fun x => x ^ r) MeasureTheory.volume a b
This theorem states that for any real numbers `a`, `b`, and `r` such that `r` is greater than `-1`, the function `f(x) = x^r` is interval integrable with respect to Lebesgue measure on the interval `a..b`. In other words, `f(x) = x^r` is integrable on both intervals `(a, b]` and `(b, a]`. Note that the theorem applies to any unordered interval `a..b` and one of these intervals is always empty, so this property can equivalently be expressed as `f` being integrable on `(min a b, max a b]`. A related but more generalized version of this theorem, called `intervalIntegrable_rpow`, applies to any locally finite measure, but it requires a stronger condition on `r`.
More concisely: For any real numbers `a`, `b`, and `r` with `r > -1`, the function `x => x^r` is Lebesgue integrable on the interval `[min a b, max a b]`.
|
integral_sin_pow_odd_mul_cos_pow
theorem integral_sin_pow_odd_mul_cos_pow :
∀ {a b : ℝ} (m n : ℕ),
∫ (x : ℝ) in a..b, x.sin ^ (2 * m + 1) * x.cos ^ n = ∫ (u : ℝ) in b.cos..a.cos, u ^ n * (1 - u ^ 2) ^ m
This theorem is about the simplification of a definite integral involving the sine and cosine functions. Specifically, it states that for any real numbers `a` and `b`, and natural numbers `m` and `n`, the integral from `a` to `b` of `sin(x)` to the power of `(2*m + 1)` times `cos(x)` to the power of `n`, is equal to the integral from `cos(b)` to `cos(a)` of `u` to the power of `n` times `(1 - u^2)` to the power of `m`. Essentially, this theorem provides a transformation for integrals where the power of sine is odd, swapping the integration variable from sine to cosine and adjusting the integrand accordingly. This can be used to simplify the computation of such integrals.
More concisely: For real numbers `a` and `b` and natural numbers `m` and `n`, the integral from `a` to `b` of `sin(x)^(2m+1) * cos(x)^n` dx equals the integral from `cos(a)` to `cos(b)` of `u^n * (1 - u^2)^m` du.
|
integral_sin_pow_even_mul_cos_pow_even
theorem integral_sin_pow_even_mul_cos_pow_even :
∀ {a b : ℝ} (m n : ℕ),
∫ (x : ℝ) in a..b, x.sin ^ (2 * m) * x.cos ^ (2 * n) =
∫ (x : ℝ) in a..b, ((1 - (2 * x).cos) / 2) ^ m * ((1 + (2 * x).cos) / 2) ^ n
This theorem states that for all real numbers `a` and `b`, and for all natural numbers `m` and `n`, the integral of `sin(x) ^ (2m) * cos(x) ^ (2n)` from `a` to `b` is equal to the integral of `((1 - cos(2x)) / 2) ^ m * ((1 + cos(2x)) / 2) ^ n` from `a` to `b`. Essentially, it simplifies the integral of a product of even powers of sine and cosine.
More concisely: For all real numbers `a` and `b`, and natural numbers `m` and `n`, the integral of `sin(x) ^ (2m) * cos(x) ^ (2n)` from `a` to `b` equals the integral of `((1 - cos(2x)) / 2) ^ m * ((1 + cos(2x)) / 2) ^ n` from `a` to `b`.
|
integral_sin_mul_cos₂
theorem integral_sin_mul_cos₂ : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, x.sin * x.cos = (a.cos ^ 2 - b.cos ^ 2) / 2
This theorem states that for any two real numbers `a` and `b`, the definite integral from `a` to `b` of the function `sin(x) * cos(x)` is equal to `(cos²(a) - cos²(b)) / 2`. This gives the area under the curve of the function `sin(x) * cos(x)` over the interval `[a, b]`, expressed in terms of the cosine squared function. Refer to the theorem `integral_sin_mul_cos₁` for this integral expressed in terms of sine squared.
More concisely: The definite integral of `sin(x) * cos(x)` from `a` to `b` equals `(cos²(a) - cos²(b)) / 2`.
|
integral_pow
theorem integral_pow : ∀ {a b : ℝ} (n : ℕ), ∫ (x : ℝ) in a..b, x ^ n = (b ^ (n + 1) - a ^ (n + 1)) / (↑n + 1) := by
sorry
This theorem, `integral_pow`, states that for any real numbers `a` and `b`, and any natural number `n`, the definite integral of `x^n` with respect to `x` from `a` to `b` is equal to `(b^(n+1) - a^(n+1))/(n+1)`. In mathematical notation, this would be written as `∫_a^b x^n dx = (b^(n+1) - a^(n+1)) / (n+1)`.
More concisely: The definite integral of `x^n` from `a` to `b` equals `(b^(n+1) - a^(n+1)) / (n+1)`.
|
intervalIntegral.intervalIntegrable_cpow'
theorem intervalIntegral.intervalIntegrable_cpow' :
∀ {a b : ℝ} {r : ℂ}, -1 < r.re → IntervalIntegrable (fun x => ↑x ^ r) MeasureTheory.volume a b
This theorem states that for any two real numbers `a` and `b`, and any complex number `r` with its real part greater than -1, the function that maps x (a real number) to the complex power of x (i.e., `x ^ r`) is interval integrable with respect to the Lebesgue measure on the interval `a..b`. This means that the function is integrable on both intervals `(a, b]` and `(b, a]`. Note that 'interval integrable' is a property equivalent to the function being integrable on the interval `(min a b, max a b]`. There is also a more general version of this theorem that applies to any locally finite measure but requires a stronger condition on `r`, which can be found at `intervalIntegrable_cpow`.
More concisely: For any real numbers `a` and `b` and complex number `r` with real part greater than -1, the complex power function `x => x ^ r` is Lebesgue integrable on the interval `[a, b]`. (Equivalently, it is integrable on both `(a, b]` and `[b, a]`.)
|
intervalIntegral.integrableOn_Ioo_cpow_iff
theorem intervalIntegral.integrableOn_Ioo_cpow_iff :
∀ {s : ℂ} {t : ℝ},
0 < t → (MeasureTheory.IntegrableOn (fun x => ↑x ^ s) (Set.Ioo 0 t) MeasureTheory.volume ↔ -1 < s.re)
The theorem `intervalIntegral.integrableOn_Ioo_cpow_iff` states that for any complex number `s` and any positive real number `t`, the complex power function `x ↦ x^s` is integrable on the open interval `(0, t)` (meaning that the function is almost everywhere strongly measurable on this interval and the integral of its pointwise norm over this interval is less than infinity) if and only if the real part of `s` is greater than `-1`. This theorem thus characterizes the conditions under which integration of the complex power function over a left-open right-open interval is feasible.
More concisely: The complex power function x ↦ x^s is integrable on the open interval (0, t) in the complex numbers if and only if the real part of s is greater than -1.
|
integral_sin_mul_cos₁
theorem integral_sin_mul_cos₁ : ∀ {a b : ℝ}, ∫ (x : ℝ) in a..b, x.sin * x.cos = (b.sin ^ 2 - a.sin ^ 2) / 2
This theorem states that for all real numbers `a` and `b`, the integral of the function `sin(x) * cos(x)` from `a` to `b` is equal to one half the difference of the squares of `sin(b)` and `sin(a)`. This provides a way to evaluate the definite integral of the product of the sine and cosine functions in terms of the square of the sine function.
More concisely: The definite integral of `sin(x) * cos(x)` from `a` to `b` equals half the difference of `sin²(b)` and `sin²(a)`.
|