intervalIntegral.integral_sub
theorem intervalIntegral.integral_sub :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f g : ℝ → E}
{μ : MeasureTheory.Measure ℝ},
IntervalIntegrable f μ a b →
IntervalIntegrable g μ a b →
∫ (x : ℝ) in a..b, f x - g x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in a..b, g x ∂μ
The theorem named `intervalIntegral.integral_sub` states that for any interval integrable functions `f` and `g` with respect to a measure `μ` on an unordered interval `a..b`, the difference between the integrals of these two functions over the interval `a..b` can be expressed as the integral of the difference of these functions over the same interval.
More formally, given a normed additively commutative group `E` and a normed space over the real numbers `ℝ` and `E`, and given two real-valued functions `f` and `g` that are interval integrable in the interval `a..b` with respect to a measure `μ`, the equality ∫ (x : ℝ) in a..b, f x - g x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ - ∫ (x : ℝ) in a..b, g x ∂μ holds. This is the integral analogue of the fact that the difference of the sum of two numbers is equal to the sum of their differences.
More concisely: The theorem `intervalIntegral.integral_sub` asserts that the integral of the difference of two interval integrable functions `f` and `g` over an interval `a..b` equals the difference of their integrals over the same interval with respect to measure `μ`.
|
IntervalIntegrable.symm
theorem IntervalIntegrable.symm :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
IntervalIntegrable f μ a b → IntervalIntegrable f μ b a
This theorem states that if a function `f` from the real numbers to a normed additive commutative group `E` is 'interval integrable' with respect to a measure `μ` on an interval from `a` to `b`, then the function `f` is also 'interval integrable' with respect to the measure `μ` on the interval from `b` to `a`. In other words, the 'interval integrability' of the function `f` is symmetric with respect to the endpoints `a` and `b` of the interval.
More concisely: If a function `f` is interval integrable with respect to measure `μ` on the interval [`a`, `b`] of a normed additive commutative group `E`, then it is also interval integrable with respect to `μ` on the interval [`b`, `a`].
|
intervalIntegrable_iff
theorem intervalIntegrable_iff :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Ι a b) μ
The theorem states that for a given function `f` mapping real numbers to an element of a normed additive commutative group `E`, and a measure `μ`, the function is interval integrable with respect to `μ` on the interval `a..b` if and only if it is integrable on the interval `Ι a b` with respect to `μ`. This provides an alternative definition of interval integrability. The interval `Ι a b` represents the interval from min(a,b) to max(a,b). In essence, this theorem allows us to state that the concept of interval integrability is equivalent to the function being integrable over the interval from min(a,b) to max(a,b).
More concisely: For a real-valued function `f` on a normed additive commutative group `E` and a measure `μ`, the function `f` is interval integrable with respect to `μ` on the interval `a..b` if and only if it is integrable on the interval `I a b` with respect to `μ`, where `I a b = {x : Real | min a b ≤ x ≤ max a b}`.
|
IntervalIntegrable.continuousOn_mul
theorem IntervalIntegrable.continuousOn_mul :
∀ {A : Type u_5} [inst : NormedRing A] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f g : ℝ → A},
IntervalIntegrable f μ a b → ContinuousOn g (Set.uIcc a b) → IntervalIntegrable (fun x => g x * f x) μ a b
The theorem `IntervalIntegrable.continuousOn_mul` states that for any normed ring `A`, real numbers `a` and `b`, a measure `μ` on the real numbers, and functions `f` and `g` from the real numbers to `A`, if `f` is interval integrable with respect to `μ` on the interval from `a` to `b`, and `g` is continuous on the closed interval from the minimum of `a` and `b` to the maximum of `a` and `b`, then the function that maps `x` to the product of `g(x)` and `f(x)` is also interval integrable with respect to `μ` on the interval from `a` to `b`. This theorem relates the concepts of integration and continuity, and shows that under these conditions, the product of a continuous function and an interval integrable function remains interval integrable.
More concisely: If `f` is interval integrable and `g` is continuous on the interval [a, b], then the product function `x ↔ g(x) * f(x)` is interval integrable on [a, b].
|
IntervalIntegrable.mul_continuousOn
theorem IntervalIntegrable.mul_continuousOn :
∀ {A : Type u_5} [inst : NormedRing A] {a b : ℝ} {μ : MeasureTheory.Measure ℝ} {f g : ℝ → A},
IntervalIntegrable f μ a b → ContinuousOn g (Set.uIcc a b) → IntervalIntegrable (fun x => f x * g x) μ a b
The theorem `IntervalIntegrable.mul_continuousOn` states that for any normed ring `A`, real numbers `a` and `b`, a measure `μ`, and functions `f` and `g` mapping real numbers to elements of `A`, if `f` is interval integrable with respect to `μ` on the interval `a` to `b` and `g` is continuous on the closed interval from `a` to `b` (inclusive), then the function that maps each `x` in the domain to the product of `f(x)` and `g(x)` is also interval integrable with respect to `μ` on the interval from `a` to `b`. This means that the product of an interval integrable function and a continuous function on the closed interval is also interval integrable.
More concisely: If `f` is interval integrable and `g` is continuous on a closed interval, then the product function `x ↦ f(x) * g(x)` is interval integrable.
|
intervalIntegral.integral_neg
theorem intervalIntegral.integral_neg :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}, ∫ (x : ℝ) in a..b, -f x ∂μ = -∫ (x : ℝ) in a..b, f x ∂μ
This theorem states that for any real numbers `a` and `b`, any function `f` from the real numbers to a normed additive commutative group `E` which is also a normed space over the real numbers, and any measure `μ` on the real numbers, the integral over the interval from `a` to `b` of the negation of `f` (i.e., `-f(x)`) with respect to `μ` is equal to the negation of the integral over the same interval of `f` with respect to `μ`. In more mathematical terms, the theorem says that ∫_{a}^{b} -f(x) dμ = -∫_{a}^{b} f(x) dμ. This theorem asserts the linearity property of the integral with respect to scalar multiplication.
More concisely: For any real numbers `a` and `b`, any function `f` from the real numbers to a normed additive commutative group `E` which is also a normed space over the real numbers, and any measure `μ` on the real numbers, the integral of `-f(x)` with respect to `μ` over the interval [`a`, `b`] is equal to the negative of the integral of `f(x)` with respect to `μ` over the same interval.
|
intervalIntegral.integral_of_ge
theorem intervalIntegral.integral_of_ge :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}, b ≤ a → ∫ (x : ℝ) in a..b, f x ∂μ = -∫ (x : ℝ) in Set.Ioc b a, f x ∂μ
The theorem `intervalIntegral.integral_of_ge` states that for any normed add commutative group `E` and any normed space over `E` with real numbers, given real numbers `a` and `b`, a function `f` from real numbers to `E`, and a measure `μ` on the real numbers, if `b` less than or equal to `a`, then the integral of `f` over the interval from `a` to `b` with respect to `μ` is equal to the negative of the integral of `f` over the left-open right-closed interval from `b` to `a` with respect to `μ`. In mathematical terms, this can be written as:
If $b \leq a$, then $\int_{a}^{b} f(x) d\mu = - \int_{\{x | b < x \leq a \}} f(x) d\mu$.
More concisely: For any normed add commutative group `E`, normed space over `R` with real numbers, measure `μ` on real numbers, real numbers `a` and `b` with `b ≤ a`, and function `f` from real numbers to `E`: The integral of `f` over the interval from `a` to `b` with respect to `μ` is equal to the negation of the integral of `f` over the left-open right-closed interval from `b` to `a` with respect to `μ`. In symbols: $\int_{a}^{b} f(x) d\mu = - \int_{b}^{a} f(x) d\mu$.
|
intervalIntegral.integral_same
theorem intervalIntegral.integral_same :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a : ℝ} {f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}, ∫ (x : ℝ) in a..a, f x ∂μ = 0
This theorem states that for any normed additivity commutative group `E`, and any normed space `E` over the real numbers, the integral of any real-valued function `f` over the interval from `a` to `a` (i.e., an interval with the same lower and upper bound) with respect to a given measure `μ` is always equal to zero. This is essentially stating that the integral over an interval of zero width is zero, regardless of the function and the measure used.
More concisely: For any normed additive commutative group `E` over the real numbers, any normed space `E` with real-valued function `f`, and any measure `μ` on an interval `[a, a]`, ∫(f dμ) = 0.
|
intervalIntegral.integral_comp_mul_left
theorem intervalIntegral.integral_comp_mul_left :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
c ≠ 0 → ∫ (x : ℝ) in a..b, f (c * x) = c⁻¹ • ∫ (x : ℝ) in c * a..c * b, f x
This theorem states that for any normed addition commutative group `E`, which is also a normed space over the real numbers, and for any real numbers `a`, `b`, and `c` (where `c` is not equal to zero), the integral of the function `f(c * x)` from `a` to `b` equals `c` to the power of `-1` times the integral of the function `f(x)` from `c * a` to `c * b`. Basically, it's a statement about the change of variables in integration in the context of normed spaces.
More concisely: For any normed additive group `E` over the real numbers, and for any continuously differentiable function `f` and real numbers `a, b, c (≠ 0)`, the integral of `f(c*x)` from `a/c` to `b/c` equals `1/c` times the integral of `f(x)` from `a` to `b`.
|
ContinuousOn.intervalIntegrable
theorem ContinuousOn.intervalIntegrable :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ}
[inst_1 : MeasureTheory.IsLocallyFiniteMeasure μ] {u : ℝ → E} {a b : ℝ},
ContinuousOn u (Set.uIcc a b) → IntervalIntegrable u μ a b
The theorem `ContinuousOn.intervalIntegrable` states that for any function `u` from real numbers to a normed additive commutative group `E`, and any two real numbers `a` and `b`, if the function `u` is continuous on the set of elements lying between `a` and `b` (inclusive), then `u` is interval integrable with respect to a locally finite measure `μ` on the unordered interval from `a` to `b`. In other words, the function `u` is integrable on both intervals from `a` to `b` (exclusive of `a`, inclusive of `b`) and from `b` to `a` (exclusive of `b`, inclusive of `a`) with respect to the measure `μ`.
More concisely: If a real-valued function `u` on a normed additive commutative group `E` is continuous on the interval [`a`, `b`], then `u` is integrable with respect to a locally finite measure `μ` on both the intervals [`a`, `b`) and (`b`, `a`].
|
intervalIntegral.intervalIntegral_pos_of_pos_on
theorem intervalIntegral.intervalIntegral_pos_of_pos_on :
∀ {f : ℝ → ℝ} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b →
(∀ x ∈ Set.Ioo a b, 0 < f x) → a < b → 0 < ∫ (x : ℝ) in a..b, f x
This theorem states that if a real-valued function `f` is interval integrable over a real interval `(a, b]` such that `a < b`, and the function is positive within the open interval `(a, b)`, then the integral of the function over the interval `a..b` is strictly positive. In other words, for an interval integrable function `f`, if `f` is positive for all `x` within the open interval from `a` to `b`, then the integral of `f` from `a` to `b` is greater than zero.
More concisely: If a real-valued function `f` is interval integrable over `(a, b]` with `a < b` and is positive on the open interval `(a, b)`, then `∫(f) dx from a to b > 0`.
|
Mathlib.MeasureTheory.Integral.IntervalIntegral._auxLemma.3
theorem Mathlib.MeasureTheory.Integral.IntervalIntegral._auxLemma.3 :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
[inst_1 : MeasureTheory.IsLocallyFiniteMeasure μ] {c : E}, IntervalIntegrable (fun x => c) μ a b = True
This theorem states that for any type `E` that forms a normed additive commutative group, for any real numbers `a` and `b`, for any measure `μ` which is a locally finite measure, and for any constant function `c` of type `E`, the function `c` is interval integrable with respect to the measure `μ` on the unordered interval between `a` and `b`. In simpler terms, it means that a constant function is always interval integrable on any real interval under any locally finite measure.
More concisely: For any normed additive commutative group type `E`, constant function `c` of type `E`, and locally finite measure `μ`, the constant function `c` is interval integrable on any unordered real interval with respect to the measure `μ`.
|
intervalIntegral.intervalIntegral_pos_of_pos
theorem intervalIntegral.intervalIntegral_pos_of_pos :
∀ {f : ℝ → ℝ} {a b : ℝ},
IntervalIntegrable f MeasureTheory.volume a b → (∀ (x : ℝ), 0 < f x) → a < b → 0 < ∫ (x : ℝ) in a..b, f x
The theorem `intervalIntegral_pos_of_pos` states that given a function `f` from real numbers to real numbers, which is strictly positive for every real number, and two real numbers `a` and `b` such that `a < b`, if `f` is interval integrable with respect to the Lebesgue measure on the interval from `a` to `b`, then the integral of `f` over this interval is strictly positive. This affirms the intuitive idea that integrating (accumulating) positive quantities over an interval yields a positive result. Note that there is a related theorem, `intervalIntegral_pos_of_pos_on`, which only requires the function `f` to be positive on the interval `(a, b)` instead of everywhere.
More concisely: If `f` is a strictly positive, real-valued function that is Lebesgue integrable on the interval [`a`, `b`] where `a < b`, then the integral of `f` over this interval is strictly positive.
|
intervalIntegral.integral_pos_iff_support_of_nonneg_ae'
theorem intervalIntegral.integral_pos_iff_support_of_nonneg_ae' :
∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
(μ.restrict (Ι a b)).ae.EventuallyLE 0 f →
IntervalIntegrable f μ a b →
(0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < ↑↑μ (Function.support f ∩ Set.Ioc a b))
This theorem states that for any real-valued function `f`, two real numbers `a` and `b`, and a measure `μ` on the real numbers, if `f` is nonnegative (almost everywhere with respect to the restriction of `μ` to the interval from `a` to `b`) and is interval integrable with respect to `μ` on an unordered interval `a` to `b`, then the integral of `f` over the interval `a` to `b` is positive if and only if `a` is less than `b` and the measure of the set intersection between the support of `f` (i.e. the set of points where `f` is nonzero) and the left-open right-closed interval from `a` to `b` is positive.
More concisely: A real-valued function `f` integrable over an interval `[a, b]` with nonnegative values almost everywhere and positive measure of the intersection of `[a, b]` with the support of `f` implies that the integral of `f` over `[a, b]` is positive if and only if `a < b`.
|
intervalIntegral.integral_const
theorem intervalIntegral.integral_const :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : CompleteSpace E] [inst_2 : NormedSpace ℝ E] {a b : ℝ}
(c : E), ∫ (x : ℝ) in a..b, c = (b - a) • c
This theorem states that for any type `E` that forms a normed additive commutative group, is a complete space, and also a normed space over the real numbers (`ℝ`), given any two real numbers `a` and `b` and any element `c` of type `E`, the definite integral from `a` to `b` of a constant function `c` is equal to `(b - a) • c`. In other words, the integral of a constant function over an interval is simply the width of the interval times the constant, scaled appropriately for the type `E`.
More concisely: For any normed additive commutative group `E` complete over the real numbers `ℝ`, the definite integral of a constant function `c` over an interval `[a, b]` in `E` equals `(b - a) • c`.
|
MeasureTheory.Integrable.intervalIntegrable
theorem MeasureTheory.Integrable.intervalIntegrable :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
MeasureTheory.Integrable f μ → IntervalIntegrable f μ a b
The theorem states that if a function `f` is integrable with respect to a given measure `μ`, then it is also interval integrable with respect to `μ` on the interval from `a` to `b`, inclusive. In other words, if `f` meets the conditions of measurability and finite integral over the entire domain under the measure `μ`, then it also meets these conditions when restricted to any interval `[a, b]` under the same measure. The terms "integrable" and "interval integrable" are used in the sense defined in Measure Theory, with "integrable" implying that the function is AEStronglyMeasurable and has a finite integral, and "interval integrable" implying that the function is integrable on the intervals `(a, b]` and `(b, a]`.
More concisely: If a function is integrable with respect to a measure, then it is interval integrable on any subinterval under the same measure.
|
IntervalIntegrable.trans
theorem IntervalIntegrable.trans :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ} {a b c : ℝ},
IntervalIntegrable f μ a b → IntervalIntegrable f μ b c → IntervalIntegrable f μ a c
The theorem `IntervalIntegrable.trans` states that for any type `E` that forms a normed additive commutative group, any real-valued function `f` on `E`, any measure `μ` on the real numbers, and any real numbers `a`, `b`, and `c`, if `f` is interval integrable with respect to measure `μ` on the unordered intervals `a..b` and `b..c`, then `f` is also interval integrable with respect to measure `μ` on the unordered interval `a..c`. In simpler terms, this is the transitivity property for interval integrability: if `f` is interval integrable over two intervals that share an endpoint, then `f` is interval integrable over the whole interval encompassing both.
More concisely: If `f` is interval integrable with respect to measure `μ` on the unordered intervals `a..b` and `b..c` of a normed additive commutative group `E`, then `f` is interval integrable with respect to `μ` on the unordered interval `a..c` of `E`.
|
intervalIntegrable_iff_integrableOn_Ioc_of_le
theorem intervalIntegrable_iff_integrableOn_Ioc_of_le :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
a ≤ b → (IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b) μ)
The theorem `intervalIntegrable_iff_integrableOn_Ioc_of_le` states that for all real-valued functions `f` and real numbers `a` and `b` (with `a` less than or equal to `b`), and given a measure `μ`, then the function `f` is interval integrable on the interval from `a` to `b` with respect to the measure `μ` if and only if `f` is integrable on the left-open right-closed interval from `a` to `b` with respect to the measure. Essentially, this theorem establishes an equivalence between the interval integrability of a function and its integrability over a left-open right-closed interval under the condition that the lower bound is less than or equal to the upper bound.
More concisely: A real-valued function is interval integrable on [a, b] with respect to a measure if and only if it is integrable on the left-open right-closed interval Ioc(a, b) with respect to that measure.
|
intervalIntegrable_const
theorem intervalIntegrable_const :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
[inst_1 : MeasureTheory.IsLocallyFiniteMeasure μ] {c : E}, IntervalIntegrable (fun x => c) μ a b
The theorem `intervalIntegrable_const` states that for any real numbers `a` and `b`, any measure `μ` on the real numbers that is locally finite, and any element `c` of a given normed additive commutative group `E`, the constant function `fun x => c` is interval integrable with respect to `μ` on the interval from `a` to `b`. This means that the constant function is integrable on both of the intervals `(a, b]` and `(b, a]`, which is equivalent to being integrable on the interval `(min(a, b), max(a, b)]`.
More concisely: For any locally finite measure μ on the real numbers and any constant function f(x) = c, the function is integrable with respect to μ on any interval [a, b].
|
intervalIntegral.integral_congr
theorem intervalIntegral.integral_congr :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f g : ℝ → E}
{μ : MeasureTheory.Measure ℝ} {a b : ℝ},
Set.EqOn f g (Set.uIcc a b) → ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
This theorem states that if two functions `f` and `g`, mapping from the real numbers to a normed additive commutative group `E`, are equal on an interval including the endpoints `a` and `b` (denoted as `[a, b]`), then the interval integrals of the two functions over the interval `[a, b]` are also equal. The interval integral is taken with respect to a measure `μ`. In other words, if `f(x) = g(x)` for all `x` in `[a, b]`, then the integral of `f` from `a` to `b` is the same as the integral of `g` from `a` to `b`.
More concisely: If functions `f` and `g` are equal on an interval `[a, b]` in a normed additive commutative group `E` with respect to a measure `μ`, then their integrals from `a` to `b` are equal: `∫[a,b] f(x) δx = ∫[a,b] g(x) δx`.
|
intervalIntegral.integral_of_le
theorem intervalIntegral.integral_of_le :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
{μ : MeasureTheory.Measure ℝ}, a ≤ b → ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in Set.Ioc a b, f x ∂μ
This theorem states that for any normed additive commutative group `E` and any normed space over the real numbers `ℝ` with elements `a` and `b` such that `a` is less than or equal to `b`, and any function `f` from the real numbers to `E`, and any measure `μ`, the definite integral of `f` with respect to `μ` over the interval from `a` to `b` is equal to the integral of `f` with respect to `μ` over the left-open right-closed interval from `a` to `b` - denoted `Set.Ioc a b`. In other words, the theorem asserts the equality of two different ways of defining the integral of a function on an interval in the real numbers.
More concisely: For any normed additive commutative group `E`, any normed space over the real numbers with elements `a` and `b` such that `a ≤ b`, any function `f` from the real numbers to `E`, and any measure `μ`, the definite integrals of `f` with respect to `μ` over the interval `[a, b]` and the left-open right-closed interval `Set.Ioc a b` are equal.
|
intervalIntegral.integral_comp_mul_add
theorem intervalIntegral.integral_comp_mul_add :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
c ≠ 0 → ∀ (d : ℝ), ∫ (x : ℝ) in a..b, f (c * x + d) = c⁻¹ • ∫ (x : ℝ) in c * a + d..c * b + d, f x
The theorem `intervalIntegral.integral_comp_mul_add` states that for all real numbers `a`, `b`, `c` and `d`, with `c` not equal to zero, and for any function `f` mapping real numbers to elements of a normed space over the real numbers, the integral over the interval `[a, b]` of `f` composed with the linear transformation `x ↦ c * x + d` equals `c` inverse scaled by the integral over the interval `[c * a + d, c * b + d]` of `f`. In other words, it expresses how linear transformations of the input variable affect the value of definite integrals.
More concisely: For real numbers `a`, `b`, `c ≠ 0`, and a function `f` mapping real numbers to elements of a normed space, the definite integral of `f` over `[a, b]` equals `c⁻¹` times the definite integral of `f` over `[c*a + d, c*b + d]`, where `d = c*a + b`.
|
intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero
theorem intervalIntegral.integral_lt_integral_of_ae_le_of_measure_setOf_lt_ne_zero :
∀ {f g : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
a ≤ b →
IntervalIntegrable f μ a b →
IntervalIntegrable g μ a b →
(μ.restrict (Set.Ioc a b)).ae.EventuallyLE f g →
↑↑(μ.restrict (Set.Ioc a b)) {x | f x < g x} ≠ 0 →
∫ (x : ℝ) in a..b, f x ∂μ < ∫ (x : ℝ) in a..b, g x ∂μ
This theorem states that if we have two real-valued functions `f` and `g` that are interval integrable over an interval `a..b` with `a ≤ b`, and for almost every `x` in the interval `(a, b]`, `f(x)` is less than or equal to `g(x)`, and on a subset of `(a, b]` with non-zero measure `f(x)` is strictly less than `g(x)`, then the integral of `f` over the interval `a..b` is strictly less than the integral of `g` over the same interval. The measure `μ` can be any measure defined on the real numbers.
More concisely: If real-valued functions `f` and `g` are interval integrable over `[a, b]` with `a ≤ b`, `f(x) ≤ g(x)` almost everywhere in `(a, b]` except on a subset of positive measure where `f(x) < g(x)`, then `∫[a, b] f dx < ∫[a, b] g dx`.
|
intervalIntegral.integral_smul
theorem intervalIntegral.integral_smul :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
{𝕜 : Type u_6} [inst_2 : NontriviallyNormedField 𝕜] [inst_3 : NormedSpace 𝕜 E] [inst_4 : SMulCommClass ℝ 𝕜 E]
(r : 𝕜) (f : ℝ → E), ∫ (x : ℝ) in a..b, r • f x ∂μ = r • ∫ (x : ℝ) in a..b, f x ∂μ
This theorem, `intervalIntegral.integral_smul`, states that for any normed add commutative group E, normed space over the reals ℝ and 𝕜, any measure μ on the reals, and any type 𝕜 with a nontrivial normed field structure, normed space structure over E, and a scalar multiplication commutative class structure, the interval integral of a function `f` multiplied by a scalar `r` over an interval `[a, b]` is equal to the scalar `r` multiplied by the integral of the function `f` over the same interval. In mathematical terms, for all real numbers a and b, scalar r, and function f, ∫ (x : ℝ) in a..b, r • f x ∂μ = r • ∫ (x : ℝ) in a..b, f x ∂μ. This is a generalization of the well-known property of definite integrals where the integral of a scalar multiple of a function is the scalar multiple of the integral of the function.
More concisely: For any normed add commutative group E, normed space over the reals ℝ, measure μ on the reals, and scalar r in a normed field 𝕜, the integral of the product of r and a function f over an interval [a, b] is equal to the product of r and the integral of f over the same interval.
|
Filter.Tendsto.eventually_intervalIntegrable_ae
theorem Filter.Tendsto.eventually_intervalIntegrable_ae :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ}
{l l' : Filter ℝ},
StronglyMeasurableAtFilter f l' μ →
∀ [inst_1 : Filter.TendstoIxxClass Set.Ioc l l'] [inst_2 : l'.IsMeasurablyGenerated],
μ.FiniteAtFilter l' →
∀ {c : E},
Filter.Tendsto f (l' ⊓ μ.ae) (nhds c) →
∀ {u v : ι → ℝ} {lt : Filter ι},
Filter.Tendsto u lt l →
Filter.Tendsto v lt l → ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (u t) (v t)
The theorem `Filter.Tendsto.eventually_intervalIntegrable_ae` states the following: Given a function `f` from real numbers to elements of a normed addition commutative group `E`, a measure `μ` on real numbers, and two filters `l` and `l'` on real numbers, if `f` is strongly measurable at filter `l'` with respect to `μ` and `f` has a finite limit at the infimum of `l'` and the almost everywhere filter of `μ`, then `f` is interval integrable on an interval defined by two functions `u` and `v` if both `u` and `v` tend to `l`. This is under the conditions that the interval `Ioc u v` is included in `l'` for every `s` in `l'`, `l'` is measurably generated, `μ` is finite at `l'`, `l'` is included in the preimage of `Ioc u v` under `l`, and `u` and `v` are functions from some index type `ι` to real numbers such that for every `t` in the filter on `ι`, `u t` and `v t` are real numbers. The theorem shows that under these conditions, `f` is interval integrable on the interval `u..v` for almost every `t`.
More concisely: Given a strongly measurable and limit function `f` on a measure space with respect to filters `l` and `l'`, if `l'` is a measurable filter, `μ` is finite on `l'`, and `l'` is included in the preimage of an interval under `l`, then `f` is almost everywhere interval integrable on the interval defined by the limits of `l'`.
|
intervalIntegral.integral_comp_mul_right
theorem intervalIntegral.integral_comp_mul_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
c ≠ 0 → ∫ (x : ℝ) in a..b, f (x * c) = c⁻¹ • ∫ (x : ℝ) in a * c..b * c, f x
This theorem states that for any normed additive commutative group `E` that is also a normed space over the real numbers, given any real numbers `a`, `b` and `c` and a function `f` from the real numbers to `E`, if `c` is not zero, then the interval integral from `a` to `b` of `f` applied to `x * c` equals `c` inverse scaled by the interval integral from `a * c` to `b * c` of `f x`. In other words, it describes a property of interval integrals where the scaling of the variable of integration can be moved outside of the integral.
More concisely: For any normed additive commutative group `E` over the real numbers, if `f` is a function from the real numbers to `E`, and `a`, `b`, and `c` are real numbers with `c ≠ 0`, then ∫[a, b] (`x ↦ f(x * c)`) dx = (1/`c`) ∫[a*c, b*c] (`x ↦ f x`) dx.
|
intervalIntegral.integral_add_adjacent_intervals
theorem intervalIntegral.integral_add_adjacent_intervals :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} {f : ℝ → E}
{μ : MeasureTheory.Measure ℝ},
IntervalIntegrable f μ a b →
IntervalIntegrable f μ b c →
∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in b..c, f x ∂μ = ∫ (x : ℝ) in a..c, f x ∂μ
This theorem states that for any real numbers `a`, `b`, and `c`, and a function `f` from real numbers to a normed additively commutative group `E` that is interval-integrable with respect to a measure `μ` on intervals `a..b` and `b..c`, the sum of the integrals of `f` with respect to `μ` over the intervals `a..b` and `b..c` is equal to the integral of `f` with respect to `μ` over the interval `a..c`. This is a formal statement of the property of additivity of integration over adjacent intervals.
More concisely: For any real numbers `a < b < c` and a function `f` integrable over `[a, b]` and `[b, c]` with respect to a measure `μ`, the integral of `f` over `[a, c]` is equal to the sum of the integrals over `[a, b]` and `[b, c]`.
|
Filter.Tendsto.eventually_intervalIntegrable
theorem Filter.Tendsto.eventually_intervalIntegrable :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ}
{l l' : Filter ℝ},
StronglyMeasurableAtFilter f l' μ →
∀ [inst_1 : Filter.TendstoIxxClass Set.Ioc l l'] [inst_2 : l'.IsMeasurablyGenerated],
μ.FiniteAtFilter l' →
∀ {c : E},
Filter.Tendsto f l' (nhds c) →
∀ {u v : ι → ℝ} {lt : Filter ι},
Filter.Tendsto u lt l →
Filter.Tendsto v lt l → ∀ᶠ (t : ι) in lt, IntervalIntegrable f μ (u t) (v t)
This theorem states that for a function `f : ℝ → E` with a finite limit at a filter `l'`, if `l'` is a measurably generated filter and `l` is a filter such that each set in `l'` eventually includes the left-open right-closed interval `(u, v]` as both `u` and `v` tend to `l`, then `f` is interval integrable on `u` to `v`, provided that both `u` and `v` tend to `l`. The measure `μ` needs to be finite at `l'`. The theorem also discusses the mechanism of Lean's typeclass instances, which allows Lean to find `l'` based on `l` but not the other way round. So, applying `Filter.Tendsto.eventually_intervalIntegrable` will generate goals `Filter ℝ` and `TendstoIxxClass Ioc ?m_1 l'`.
More concisely: Given a function `f : ℝ → E` with a finite limit at a measurably generated filter `l'`, if `l'` is such that every set in `l'` eventually includes the interval `(u, v]` for all `u, v` tendering to `l`, and `μ(l')` is finite, then `f` is interval integrable on `[u, v]` for all `u, v` tending to `l`.
|
intervalIntegral.integral_congr_ae
theorem intervalIntegral.integral_congr_ae :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f g : ℝ → E}
{μ : MeasureTheory.Measure ℝ},
(∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → f x = g x) → ∫ (x : ℝ) in a..b, f x ∂μ = ∫ (x : ℝ) in a..b, g x ∂μ
This theorem states that for all real numbers 'a' and 'b' and for all functions 'f' and 'g' from the real numbers to a normed space 'E', if almost everywhere with respect to a given measure 'μ', 'f' and 'g' are equal on the interval from 'a' to 'b', then the interval integrals of 'f' and 'g' over that interval with respect to 'μ' are equal. This is a statement about the equality of integrals under the condition of almost everywhere equality of the functions being integrated.
More concisely: If real-valued functions $f$ and $g$ on a measure space agree almost everywhere on an interval with respect to a given measure, then their integrals over that interval are equal.
|
intervalIntegral.integral_symm
theorem intervalIntegral.integral_symm :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f : ℝ → E} {μ : MeasureTheory.Measure ℝ}
(a b : ℝ), ∫ (x : ℝ) in b..a, f x ∂μ = -∫ (x : ℝ) in a..b, f x ∂μ
This theorem, `intervalIntegral.integral_symm`, states that for any real-numbered function `f` and measure `μ`, the integral of `f` over the interval from `b` to `a` is the negation of the integral of `f` over the interval from `a` to `b`. This comes from the properties of the integral in real analysis and holds for any function `f` that is integrable with respect to the given measure `μ` over the given interval.
More concisely: For any integrable function `f` and measure `μ`, the integral of `f` over the interval `[a, b]` is equal to the negation of the integral of `f` over the interval `[b, a]`.
|
intervalIntegral.intervalIntegral_eq_integral_uIoc
theorem intervalIntegral.intervalIntegral_eq_integral_uIoc :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) (a b : ℝ)
(μ : MeasureTheory.Measure ℝ),
∫ (x : ℝ) in a..b, f x ∂μ = (if a ≤ b then 1 else -1) • ∫ (x : ℝ) in Ι a b, f x ∂μ
This theorem states that for any real-valued function `f` and any two real numbers `a` and `b`, under certain conditions, the interval integral of `f` from `a` to `b` with respect to a measure `μ` is equal to the integral of `f` over the interval from `a` to `b`, possibly negated depending on the order of `a` and `b`. Specifically, if `a` is less than or equal to `b`, the result is positive; otherwise, it's negated. The conditions required are that the function's codomain `E` is a normed add-commutative group and also a normed space over the real numbers.
More concisely: For any real-valued function `f` with codomain in a normed add-commutative group and normed space over the real numbers, the interval integral of `f` with respect to a measure `μ` from `a` to `b` equals the integral of `f` over the interval and is positive if `a` <= `b`, or negated otherwise.
|
Continuous.intervalIntegrable
theorem Continuous.intervalIntegrable :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] {μ : MeasureTheory.Measure ℝ}
[inst_1 : MeasureTheory.IsLocallyFiniteMeasure μ] {u : ℝ → E},
Continuous u → ∀ (a b : ℝ), IntervalIntegrable u μ a b
The theorem states that for any continuous function `u` mapping real numbers to a normed additively commutative group `E`, and for any locally finite measure `μ` on the real numbers, the function `u` is interval integrable with respect to the measure `μ` on any unordered interval `a..b`. In other words, the function is integrable on both intervals `(a, b]` and `(b, a]`. In mathematical terms, it's equivalent to saying that the function `u` is integrable on the interval `(min a b, max a b]`.
More concisely: For any continuous function from real numbers to a normed additively commutative group and any locally finite measure on real numbers, the function is interval integrable with respect to the measure on any unordered interval, equivalently integrable on the interval with minimum and maximum endpoints.
|
intervalIntegral.integral_const_of_cdf
theorem intervalIntegral.integral_const_of_cdf :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : CompleteSpace E] [inst_2 : NormedSpace ℝ E] {a b : ℝ}
{μ : MeasureTheory.Measure ℝ} [inst_3 : MeasureTheory.IsFiniteMeasure μ] (c : E),
∫ (x : ℝ) in a..b, c ∂μ = ((↑↑μ (Set.Iic b)).toReal - (↑↑μ (Set.Iic a)).toReal) • c
The theorem `intervalIntegral.integral_const_of_cdf` states that if `μ` is a finite measure, then the integral of a constant `c` over the interval from `a` to `b` with respect to `μ` is equal to the difference of the measures of the left-infinite right-closed intervals ending at `b` and `a` respectively, each scaled by `c`. In mathematical terms, this means that for any constant `c` and any finite measure `μ`, the integral from `a` to `b` of `c` with respect to `μ` equals the difference between the measures of the sets of all real numbers less than or equal to `b` and `a` respectively, multiplied by `c`.
More concisely: For any constant `c` and finite measure `μ`, the integral of `c` from `a` to `b` with respect to `μ` equals `c * (μ([a, ∞[) - μ([a, b]))`.
|
intervalIntegral.integral_comp_sub_mul
theorem intervalIntegral.integral_comp_sub_mul :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
c ≠ 0 → ∀ (d : ℝ), ∫ (x : ℝ) in a..b, f (d - c * x) = c⁻¹ • ∫ (x : ℝ) in d - c * b..d - c * a, f x
This theorem states that for any normed add commutative group E, and any normed space over the real numbers with an element of E, given a real number `c` that is not equal to zero, a function `f` from the real numbers to E, and another real number `d`, the integral over the interval `[a, b]` of `f` composed with the function `x ↦ d - c * x` is equal to `c` inverse scaled by the integral over the interval `[d - c * b, d - c * a]` of `f`. This theorem basically describes the change of variables in an integral with respect to a linear substitution.
More concisely: For any commutative normed additive group E, real number c ≠ 0, real numbers a ≤ b, and a real-valued function f on the real numbers, the integral of f(x) * (d - c*x) dx over [a, b] is equal to c^(-1) * integral of f(x) dx over [d - c*b, d - c*a].
|
intervalIntegral.norm_integral_eq_norm_integral_Ioc
theorem intervalIntegral.norm_integral_eq_norm_integral_Ioc :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ}
(f : ℝ → E), ‖∫ (x : ℝ) in a..b, f x ∂μ‖ = ‖∫ (x : ℝ) in Ι a b, f x ∂μ‖
This theorem states that for any type `E` which is a normed addition-commutative group and also a normed space over the real numbers, and for any real numbers `a` and `b`, and any measure `μ` on the real numbers, and any function `f` from the real numbers to `E`, the norm of the interval integral of `f` from `a` to `b` with respect to `μ` is equal to the norm of the interval integral of `f` over the half-open interval from `a` to `b` with respect to `μ`. This means that the way we choose the end points of the interval (inclusive or exclusive) does not impact the norm of the integral.
More concisely: For any normed additive commutative group and normed space `E` over the real numbers, any measure `μ` on the real numbers, any function `f` from the real numbers to `E`, and real numbers `a` and `b`, the norms of the interval integrals of `f` from `a` to `b` and from `a` to `b` (half-open) with respect to `μ` are equal.
|
intervalIntegral.integral_pos_iff_support_of_nonneg_ae
theorem intervalIntegral.integral_pos_iff_support_of_nonneg_ae :
∀ {f : ℝ → ℝ} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
μ.ae.EventuallyLE 0 f →
IntervalIntegrable f μ a b →
(0 < ∫ (x : ℝ) in a..b, f x ∂μ ↔ a < b ∧ 0 < ↑↑μ (Function.support f ∩ Set.Ioc a b))
The theorem `intervalIntegral.integral_pos_iff_support_of_nonneg_ae` states that for any real-valued function `f` and any real numbers `a` and `b`, given a measure `μ` on the real numbers, if `f` is almost everywhere nonnegative (meaning that `f(x)` is greater than or equal to zero for almost all `x`), and `f` is interval integrable with respect to `μ` on the unordered interval from `a` to `b`, then the integral of `f` over the interval from `a` to `b` is positive if and only if `a` is less than `b` and the measure of the set of points where `f` is not zero, intersected with the interval from `a` to `b`, is positive.
To put it in simple terms, if a function is nonnegative almost everywhere and is integrable over an interval, the integral over that interval is positive only if the interval is not degenerate (`a < b`) and there are points in the interval where the function is nonzero.
More concisely: A real-valued function that is almost everywhere nonnegative and interval integrable with respect to a measure on an interval (a, b) has a positive integral if and only if (a < b) and the measure of the subset where the function is nonzero on the interval is positive.
|
IntervalIntegrable.add
theorem IntervalIntegrable.add :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] {f g : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
IntervalIntegrable f μ a b → IntervalIntegrable g μ a b → IntervalIntegrable (fun x => f x + g x) μ a b
The theorem `IntervalIntegrable.add` states that, for any normed additive commutative group `E`, if two real-valued functions `f` and `g` are both interval integrable with respect to a measure `μ` on an unordered interval from `a` to `b`, then their pointwise sum `(fun x => f x + g x)` is also interval integrable on the same interval with respect to the same measure. This means that the property of being interval integrable is closed under the operation of pointwise addition of functions.
More concisely: If `f` and `g` are interval integrable functions on an unordered interval `[a, b]` with respect to a measure `μ` over a normed additive commutative group `E`, then their pointwise sum `f + g` is also interval integrable on `[a, b]` with respect to `μ`.
|
intervalIntegral.integral_comp_add_right
theorem intervalIntegral.integral_comp_add_right :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} (f : ℝ → E) (d : ℝ),
∫ (x : ℝ) in a..b, f (x + d) = ∫ (x : ℝ) in a + d..b + d, f x
This theorem states that for any normed additively commutative group `E` and any normed space over the real numbers `ℝ` with elements of type `E`, given two real numbers `a` and `b`, a function `f` from real numbers to `E`, and another real number `d`, the integral of `f` evaluated at `(x + d)` over the interval `[a, b]` is equal to the integral of `f` evaluated at `x` over the interval `[a + d, b + d]`. In other words, adding a constant `d` to the variable of integration inside the integral and to the limits of integration outside the integral does not change the value of the integral.
More concisely: For any normed additively commutative group `E` and real-valued function `f` on an interval `[a, b]`, the integral of `f` over `[a, b]` is equal to the integral of `f` over `[a + d, b + d]` for any real number `d`.
|
Mathlib.MeasureTheory.Integral.IntervalIntegral._auxLemma.1
theorem Mathlib.MeasureTheory.Integral.IntervalIntegral._auxLemma.1 :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
IntervalIntegrable f μ a b = MeasureTheory.IntegrableOn f (Ι a b) μ
This theorem states that for any normed additive commutative group `E`, a real-valued function `f`, and two real numbers `a` and `b`, and a measure `μ` of real numbers, the function `f` is interval integrable with respect to measure `μ` on an unordered interval `a..b` if and only if it is integrable on the interval `Ι a b`. In mathematical terms, a function `f` is interval integrable between two points `a` and `b` if it is integrable (almost everywhere strongly measurable, and the integral of its pointwise norm is finite) over both the intervals `(a, b]` and `(b, a]`. This theorem says that this is equivalent to the function being integrable over the interval `Ι a b`, which represents the interval from `min(a, b)` to `max(a, b)`.
More concisely: A real-valued function `f` is interval integrable with respect to a measure `μ` over an unordered interval `[a, b]` if and only if it is integrable over the interval `[min(a, b) max(a, b)]`.
|
intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt
theorem intervalIntegral.integral_lt_integral_of_continuousOn_of_le_of_exists_lt :
∀ {f g : ℝ → ℝ} {a b : ℝ},
a < b →
ContinuousOn f (Set.Icc a b) →
ContinuousOn g (Set.Icc a b) →
(∀ x ∈ Set.Ioc a b, f x ≤ g x) →
(∃ c ∈ Set.Icc a b, f c < g c) → ∫ (x : ℝ) in a..b, f x < ∫ (x : ℝ) in a..b, g x
The theorem states that if `f` and `g` are two real-valued functions that are continuous on a closed interval `[a, b]` where `a` is less than `b`, and for every `x` in the open interval `(a, b]`, `f(x)` is less than or equal to `g(x)`, and if there exists a point `c` in `[a, b]` such that `f(c)` is strictly less than `g(c)`, then the integral of `f` from `a` to `b` is strictly less than the integral of `g` from `a` to `b`. In mathematical terms, if $f$ and $g$ are continuous on $[a, b]$, $a < b$, $f(x) \leq g(x)$ on $(a, b]$, and $f(c) < g(c)$ for some $c \in [a, b]$, then $\int_{a}^{b} f(x) dx < \int_{a}^{b} g(x) dx$.
More concisely: If `f` and `g` are continuous real-valued functions on a closed interval `[a, b]` with `a < b`, `f(x) ≤ g(x)` for all `x ∈ (a, b]`, and there exists a point `c ∈ [a, b]` with `f(c) < g(c)`, then `∫[a,b] f(x) dx < ∫[a,b] g(x) dx`.
|
intervalIntegral.integral_comp_add_mul
theorem intervalIntegral.integral_comp_add_mul :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b c : ℝ} (f : ℝ → E),
c ≠ 0 → ∀ (d : ℝ), ∫ (x : ℝ) in a..b, f (d + c * x) = c⁻¹ • ∫ (x : ℝ) in d + c * a..d + c * b, f x
This theorem states that for any function `f` from real numbers to a normed space `E`, given real numbers `a`, `b`, `c` with `c` not equal to zero, and any real number `d`, we could rewrite the integral of `f` of `d + c * x` over the interval from `a` to `b` as `c⁻¹` times the integral of `f` over the interval from `d + c * a` to `d + c * b`. This theorem essentially establishes a property of a linear change of variables in definite integrals.
More concisely: For any real-valued function `f` on a normed space `E` and real numbers `a`, `b`, `c` not equal to zero, the integral of `f` over the interval `[a, b]` with respect to the variable `x` is equal to `c⁻¹` times the integral of `f(d + c * x)` over the interval `[d + c * a, d + c * b]`, where `d` is any real number.
|
intervalIntegral.integral_zero
theorem intervalIntegral.integral_zero :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {μ : MeasureTheory.Measure ℝ},
∫ (x : ℝ) in a..b, 0 ∂μ = 0
This theorem states that for any real numbers `a` and `b`, and for any measure `μ`, the definite integral of the function which is identically zero over the interval from `a` to `b` is zero. This is valid regardless of the specific nature of the normed add commutative group `E` and the normed space `E` over the real numbers.
More concisely: For any real numbers `a` and `b`, and for any measure `μ`, the definite integral of the zero function over the interval [`a`, `b`] is zero.
|
intervalIntegrable_iff_integrableOn_Icc_of_le
theorem intervalIntegrable_iff_integrableOn_Icc_of_le :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] {f : ℝ → E} {a b : ℝ},
a ≤ b →
∀ {μ : MeasureTheory.Measure ℝ} [inst_1 : MeasureTheory.NoAtoms μ],
IntervalIntegrable f μ a b ↔ MeasureTheory.IntegrableOn f (Set.Icc a b) μ
The theorem `intervalIntegrable_iff_integrableOn_Icc_of_le` states that for any real-valued function `f`, any measure `μ` on the real numbers, and any two real numbers `a` and `b` such that `a` is less than or equal to `b`, the function `f` is interval integrable with respect to `μ` on the interval from `a` to `b` if and only if `f` is integrable on the closed interval from `a` to `b` with respect to `μ`. Here, a function is said to be interval integrable if it is integrable on both the open intervals `(a, b]` and `(b, a]`. A function is integrable on a set if it is almost everywhere strongly measurable on that set and the integral of its pointwise norm over that set is less than infinity. This theorem is under the assumption that the measure `μ` has no atoms (i.e., there are no subsets of the real numbers with positive measure that contain only a single point).
More concisely: A real-valued function is interval integrable with respect to a measure with no atoms on the interval [a, b] if and only if it is integrable on the closed interval Icc[a, b] with respect to that measure.
|