integrableOn_Ioi_rpow_of_lt
theorem integrableOn_Ioi_rpow_of_lt :
∀ {a : ℝ},
a < -1 → ∀ {c : ℝ}, 0 < c → MeasureTheory.IntegrableOn (fun t => t ^ a) (Set.Ioi c) MeasureTheory.volume
The theorem `integrableOn_Ioi_rpow_of_lt` states that for any real number `a` less than `-1`, and any positive real number `c`, the function `t ↦ t ^ a` (mapping `t` to `t` raised to the power of `a`) is integrable on the interval `(c, ∞)`. Integrability in this context means that the function is almost everywhere strongly measurable on this interval and the integral of its pointwise norm over the interval is less than infinity.
More concisely: For any real number `a` with `a < -1` and positive real number `c`, the function `x mapsto x ^ a` is integrable on the interval `(c, ∞)`.
|
not_integrableOn_Ioi_cpow
theorem not_integrableOn_Ioi_cpow :
∀ (s : ℂ), ¬MeasureTheory.IntegrableOn (fun x => ↑x ^ s) (Set.Ioi 0) MeasureTheory.volume
The theorem `not_integrableOn_Ioi_cpow` states that for any complex number `s`, the complex power function defined by raising a real number `x` to the power `s` is not integrable over the interval `(0, +∞)`. Here, integrability is defined with respect to the Lebesgue measure (also referred to as `MeasureTheory.volume` in Lean), and a function is said to be integrable if it is almost everywhere strongly measurable and the integral of its pointwise norm over the set is less than infinity.
More concisely: The complex power function, defined as raising a real number to a complex exponent, is not integrable with respect to Lebesgue measure over the interval (0, +∞).
|
not_integrableOn_Ioi_rpow
theorem not_integrableOn_Ioi_rpow :
∀ (s : ℝ), ¬MeasureTheory.IntegrableOn (fun x => x ^ s) (Set.Ioi 0) MeasureTheory.volume
The theorem `not_integrableOn_Ioi_rpow` states that for any real number `s`, the function `x ^ s` (which represents `x` raised to the power `s`) is not integrable over the interval `(0, +∞)`. In mathematical terms, it means that the integral of `x^s` from 0 to infinity does not exist or is not finite, according to the measure theory definition of integrability.
More concisely: The function `x ^ s` is not integrable over the interval `(0, +∞)` for any real number `s`.
|
integrable_inv_one_add_sq
theorem integrable_inv_one_add_sq : MeasureTheory.Integrable (fun x => (1 + x ^ 2)⁻¹) MeasureTheory.volume
The theorem `integrable_inv_one_add_sq` states that the real-valued function `(1 + x^2)⁻¹` is integrable with respect to the Lebesgue measure. In this context, a function is considered integrable if it is both measurable and its integral over the entire domain is finite. Specifically, the function in question is the multiplicative inverse of `(1 + x^2)`, implying that we are looking at the area under the curve of this function over the entire real line. This theorem assures us that this area is indeed finite.
More concisely: The theorem `integrable_inv_one_add_sq` asserts that the function `(1 + x^2)⁻¹` is Lebesgue integrable over the real line.
|