MeasureTheory.integral_comp_smul_deriv_Ioi
theorem MeasureTheory.integral_comp_smul_deriv_Ioi :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {f f' : ℝ → ℝ} {g : ℝ → E} {a : ℝ},
ContinuousOn f (Set.Ici a) →
Filter.Tendsto f Filter.atTop Filter.atTop →
(∀ x ∈ Set.Ioi a, HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
ContinuousOn g (f '' Set.Ioi a) →
MeasureTheory.IntegrableOn g (f '' Set.Ici a) MeasureTheory.volume →
MeasureTheory.IntegrableOn (fun x => f' x • (g ∘ f) x) (Set.Ici a) MeasureTheory.volume →
∫ (x : ℝ) in Set.Ioi a, f' x • (g ∘ f) x = ∫ (u : ℝ) in Set.Ioi (f a), g u
This theorem is a change-of-variables formula for integrals on the half-open interval $(a, \infty)$, for vector-valued functions. Specifically, it states that given functions $f, f': \mathbb{R} \to \mathbb{R}$, and $g: \mathbb{R} \to E$, where $E$ is a normed additive commutative group with a normed space over $\mathbb{R}$, and a real number $a$, if $f$ is continuous on the closed interval $[a, \infty)$, $f$ tends to infinity as its argument does, and $f$ has a derivative $f'(x)$ at every point in $(a, \infty)$, and if $g$ is continuous and integrable on the image of $f$ on $(a, \infty)$, and the function $x \mapsto f'(x) \cdot (g \circ f)(x)$ is integrable on $[a, \infty)$, then the integral of $f'(x) \cdot (g \circ f)(x)$ over $(a, \infty)$ equals the integral of $g(u)$ over the interval $(f(a), \infty)$.
In other words, this theorem is a special case of the change of variable formula for integrals, applied to an interval of the form $(a, \infty)$, and for vector-valued functions.
More concisely: If $f: (a, \infty) \to \mathbb{R}$, $f'(x)$ exists for all $x \in (a, \infty)$, $g: \operatorname{Im} f \to E$ is continuous and integrable, and $f$ is continuous, tends to infinity, and has an integrable product derivatives $f'(x) \cdot (g \circ f)(x)$, then $\int_{a}^{\infty} f'(x) \cdot (g \circ f)(x) \, dx = \int_{f(a)}^{\infty} g(u) \, du$.
|
MeasureTheory.AECover.integral_tendsto_of_countably_generated
theorem MeasureTheory.AECover.integral_tendsto_of_countably_generated :
∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
{l : Filter ι} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : l.IsCountablyGenerated]
{φ : ι → Set α},
MeasureTheory.AECover μ l φ →
∀ {f : α → E},
MeasureTheory.Integrable f μ →
Filter.Tendsto (fun i => ∫ (x : α) in φ i, f x ∂μ) l (nhds (∫ (x : α), f x ∂μ))
The theorem `MeasureTheory.AECover.integral_tendsto_of_countably_generated` states that for any types `α`, `ι`, and `E`, given a measurable space `α`, a measure `μ` on `α`, a filter `l` on `ι` that is countably generated, and a function `φ` mapping `ι` to a set of `α` such that `φ` forms an almost everywhere cover with respect to `μ` and `l`. Then for any function `f` from `α` to `E` that is integrable with respect to `μ`, the limit as `i` tends to infinity (in the sense of the filter `l`) of the integral over the set `φ(i)` of `f` with respect to `μ` is equal to the integral over the entire space `α` of `f` with respect to `μ`. This is essentially saying that if we have a sequence of sets that covers almost everywhere in the space, the limit of the integrals of a function over these sets is the same as the integral of the function over the whole space.
More concisely: Given a measurable space `(α, Σ, μ)`, a countably generated filter `l` on `ι`, a measurable function `φ : ι -> Σ`, an almost everywhere cover `φ` of `α` with respect to `μ` and `l`, and an integrable function `f : α -> E`, the limit as `i` in `l` tends to infinity of the integrals of `f` over `φ(i)` equals the integral of `f` over `α`.
|
MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_tendsto
theorem MeasureTheory.integrableOn_Iic_of_intervalIntegral_norm_tendsto :
∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [inst : l.NeBot]
[inst : l.IsCountablyGenerated] [inst : NormedAddCommGroup E] {a : ι → ℝ} {f : ℝ → E} (I b : ℝ),
(∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) b) μ) →
Filter.Tendsto a l Filter.atBot →
Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b, ‖f x‖ ∂μ) l (nhds I) →
MeasureTheory.IntegrableOn f (Set.Iic b) μ
This theorem states that if a real-valued function `f` is integrable on a series of intervals `Ioc (a i) b`, where each `a i` approaches negative infinity, and if the integral of the norm of `f` over each such interval converges to a real number `I`, then `f` is integrable on the semi-infinite interval `Iic b`, which extends from negative infinity to `b`. This is true regardless of the specific filter `l` used to define the limit, as long as that filter is nonempty, countably generated, and the sequence `a` of lower bounds of the intervals tends to negative infinity along the filter.
More concisely: If a real-valued function `f` is integrable on each interval `[a i, b]` as `a i` approaches negative infinity in a nonempty, countably generated filter, and the integrals of `|f|`'s norms converge, then `f` is integrable on the semi-infinite interval `[-\infty, b]`.
|
MeasureTheory.aecover_Ioo_of_Ioo
theorem MeasureTheory.aecover_Ioo_of_Ioo :
∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
[inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [inst_3 : OrderClosedTopology α]
[inst_4 : OpensMeasurableSpace α] {a b : ι → α} {A B : α},
Filter.Tendsto a l (nhds A) →
Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun i => Set.Ioo (a i) (b i)
This theorem, `MeasureTheory.aecover_Ioo_of_Ioo`, states that for any types `α` and `ι`, given a measurable space `α`, a measure `μ` on this space, a filter `l` on `ι`, and the fact that `α` has a linear order, a topological space structure, an order-closed topology, and is open and measurable, along with functions `a` and `b` from `ι` to `α`, and elements `A` and `B` of `α`. If the function `a` tends to `A` along the filter `l`, and the function `b` tends to `B` along the same filter `l`, then `μ` restricted to the open interval `(A, B)` ("almost everywhere") covers the set of open intervals `(a i, b i)` for `i` in the filter `l`.
In other words, if we have two sequences `a` and `b` that respectively converge to `A` and `B`, then almost every point in the open interval `(A, B)` can be found in one of the open intervals `(a i, b i)`.
More concisely: Given a measurable space with a linear order, measure, filter, topology, and measurability properties, if functions `a` and `b` converge to `A` and `B` respectively along the filter, then almost every point in the open interval `(A, B)` lies in some `(a i, b i)` for `i` in the filter.
|
HasCompactSupport.integral_Ioi_deriv_eq
theorem HasCompactSupport.integral_Ioi_deriv_eq :
∀ {E : Type u_1} {f : ℝ → E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E],
ContDiff ℝ 1 f → HasCompactSupport f → ∀ (b : ℝ), ∫ (x : ℝ) in Set.Ioi b, deriv f x = -f b
This theorem states a special case of the `integral_Ioi_of_hasDerivAt_of_tendsto` theorem, with the assumption that the function `f` is continuously differentiable with compact support. Specifically, for any real-valued function `f` that maps to a normed additively commutative group `E`, which is also a normed space over the real numbers and a complete space, if `f` is continuously differentiable and has compact support, then for any real number `b`, the integral over the interval `(b, +∞)` of the derivative of `f` is equal to negative of the function `f` evaluated at `b`.
More concisely: If `f` is a continuously differentiable real-valued function with compact support on a complete normed space `E`, then `����(df/dx)(x: E | x > b) dx = -f(b)`.
|
MeasureTheory.AECover.integrable_of_integral_norm_bounded
theorem MeasureTheory.AECover.integrable_of_integral_norm_bounded :
∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
{l : Filter ι} [inst_1 : NormedAddCommGroup E] [inst_2 : l.NeBot] [inst_3 : l.IsCountablyGenerated]
{φ : ι → Set α},
MeasureTheory.AECover μ l φ →
∀ {f : α → E} (I : ℝ),
(∀ (i : ι), MeasureTheory.IntegrableOn f (φ i) μ) →
(∀ᶠ (i : ι) in l, ∫ (x : α) in φ i, ‖f x‖ ∂μ ≤ I) → MeasureTheory.Integrable f μ
The theorem `MeasureTheory.AECover.integrable_of_integral_norm_bounded` states that, for a given measurable space `α`, a set `ι`, a normed additive commutative group `E`, a measure `μ` on `α`, a filter `l` on `ι` that is countably generated and not the bottom filter, and a function `φ` from `ι` to the set of `α`, if `φ` is an almost everywhere cover with respect to `μ` and `l`, then for any function `f` from `α` to `E` and any real number `I`, if `f` is integrable on each set `φ i` (for every `i` in `ι`), and if the integral of the norm of `f` over each set `φ i` is almost everywhere bounded by `I` (with respect to the filter `l`), then `f` is integrable with respect to the measure `μ`. In simpler terms, if a function is integrable on each set in a countable collection of sets that almost everywhere covers a space, and if the integral of the function's norm is bounded on these sets, then the function is integrable over the entire space.
More concisely: If a function is integrable and has bounded integral norm on each set of a countably generated, non-bottom filter covering a measurable space, then the function is integrable over the entire space.
|
MeasureTheory.integrableOn_Ioi_deriv_of_nonpos
theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonpos :
∀ {g g' : ℝ → ℝ} {a l : ℝ},
ContinuousWithinAt g (Set.Ici a) a →
(∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x) →
(∀ x ∈ Set.Ioi a, g' x ≤ 0) →
Filter.Tendsto g Filter.atTop (nhds l) → MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume
This theorem states that if a real-valued function `g` has a limit at positive infinity, is continuous at `a⁺`, and its derivative `g'` is non-positive for all `x` in the open interval `(a, +∞)`, then `g'` is integrable over this interval.
In more detail, given the function `g`, its derivative `g'`, and two real numbers `a` and `l`, if `g` is continuous within the closed interval `[a, +∞)`, has a derivative at every point in the open interval `(a, +∞)` that is equal to `g'(x)` and is less than or equal to zero, and moreover `g` tends to `l` as `x` goes to positive infinity, then the derivative `g'` is integrable over the interval `(a, +∞)`. The notion of integrability used here is with respect to the Lebesgue measure.
More concisely: If a real-valued function `g` is continuous at `a+`, has a limit at infinity, and its derivative `g'` is non-positive and integrable on the open interval `(a, +∞)`, then `g'` is integrable over `(a, +∞)`.
|
MeasureTheory.integrable_of_intervalIntegral_norm_tendsto
theorem MeasureTheory.integrable_of_intervalIntegral_norm_tendsto :
∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [inst : l.NeBot]
[inst : l.IsCountablyGenerated] [inst : NormedAddCommGroup E] {a b : ι → ℝ} {f : ℝ → E} (I : ℝ),
(∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc (a i) (b i)) μ) →
Filter.Tendsto a l Filter.atBot →
Filter.Tendsto b l Filter.atTop →
Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b i, ‖f x‖ ∂μ) l (nhds I) → MeasureTheory.Integrable f μ
This theorem states that if a function `f` is integrable on a sequence of intervals `(a i, b i]` where `a i` approaches negative infinity and `b i` approaches positive infinity, and if the integral of the norm of `f` over these intervals converges to a real number `I` along a filter `l`, then `f` is integrable over the whole real line. In other words, from a sequence of smaller integrable pieces whose integrals converge, we can infer that the function is integrable over the entire domain.
More concisely: If a function `f` is integrable over a sequence of intervals `(a i, b i]` with `a i` approaching negative infinity and `b i` approaching positive infinity such that the integrals of `|f|` converge to a real number `I` along a filter `l`, then `f` is integrable over the entire real line.
|
MeasureTheory.AECover.lintegral_tendsto_of_countably_generated
theorem MeasureTheory.AECover.lintegral_tendsto_of_countably_generated :
∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
[inst_1 : l.IsCountablyGenerated] {φ : ι → Set α},
MeasureTheory.AECover μ l φ →
∀ {f : α → ENNReal},
AEMeasurable f μ → Filter.Tendsto (fun i => ∫⁻ (x : α) in φ i, f x ∂μ) l (nhds (∫⁻ (x : α), f x ∂μ))
The theorem `MeasureTheory.AECover.lintegral_tendsto_of_countably_generated` states that for any measurable space `α` and index set `ι`, a given measure `μ` on `α`, and a countably generated filter `l` on `ι`, if you have a family of sets `φ : ι → Set α` that forms an almost-everywhere cover with respect to measure `μ` and filter `l`, then for any function `f : α → ENNReal` that is almost everywhere measurable, the limit as `i` tends to the filter `l` of the Lebesgue integral of `f` over the set `φ i` (denoted as `∫⁻ (x : α) in φ i, f x ∂μ`) is equal to the Lebesgue integral of `f` over the entire space `α` (denoted as `∫⁻ (x : α), f x ∂μ`), where the limit is taken with respect to the neighborhood filter at the integral value over the entire space.
This theorem is essentially telling us about the behavior of the integral of a function over a sequence of sets that converges almost everywhere to the whole space.
More concisely: Given a measurable space, a countably generated filter, a measurable family of sets forming an almost-everywhere cover, and a almost everywhere measurable function, the limit of the Lebesgue integrals of the function over the covers as the filter converges to the entire space equals the Lebesgue integral over the entire space.
|
MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto
theorem MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto :
∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} {m : E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E],
ContinuousWithinAt f (Set.Iic a) a →
(∀ x ∈ Set.Iio a, HasDerivAt f (f' x) x) →
MeasureTheory.IntegrableOn f' (Set.Iic a) MeasureTheory.volume →
Filter.Tendsto f Filter.atBot (nhds m) → ∫ (x : ℝ) in Set.Iic a, f' x = f a - m
The theorem is a version of the **Fundamental Theorem of Calculus-2**, applied to semi-infinite intervals `(-∞, a)`. It states that if a function `f` has a limit `m` at `-∞` and its derivative `f'` is integrable, then the integral of `f'` over the interval `(-∞, a)` is equal to `f(a) - m`. The theorem assumes that `f` is differentiable on `(-∞, a)` and continuous at `a⁻`. Note that under these conditions, `f` will always have a limit at `-∞`.
In more formal terms, if `ContinuousWithinAt f (Set.Iic a) a`, for all `x` in `Set.Iio a, HasDerivAt f (f' x) x`, and `MeasureTheory.IntegrableOn f' (Set.Iic a) MeasureTheory.volume`, then if `Filter.Tendsto f Filter.atBot (nhds m)`, the integral of `f'` from `-∞` to `a`, denoted as `∫ (x : ℝ) in Set.Iic a, f' x`, is equal to `f(a) - m`.
More concisely: If a function `f` is differentiable and integrable with a limit `m` at `-∞` on the semi-interval `(-∞, a)`, then `∫ (x : ℝ) in Set.Iic a, f' x = f(a) - m`.
|
MeasureTheory.aecover_Ioo_of_Ico
theorem MeasureTheory.aecover_Ioo_of_Ico :
∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
[inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [inst_3 : OrderClosedTopology α]
[inst_4 : OpensMeasurableSpace α] {a b : ι → α} {A B : α},
Filter.Tendsto a l (nhds A) →
Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun i => Set.Ico (a i) (b i)
This theorem states that for every type `α` and `ι`, given a measurable space `α` and a measure `μ` on this space, a filter `l` on `ι`, a linear order on `α`, a topological space structure on `α`, order closed topology on `α`, open set measurability on `α`, function `a` and `b` from `ι` to `α`, and constants `A` and `B` of `α`, if `a` and `b` tend to `A` and `B` respectively with respect to the filter `l` and the neighborhood filter at `A` and `B`, then there exists an almost everywhere cover of the measure space restricted to the open interval `(A, B)`, i.e., excluding `A` and `B`, by the increasing countable union of the closed-open intervals `[a(i), b(i))` for each `i` in `ι`, where `i` is drawn from the filter `l`.
More concisely: Given a measurable space with a measure, a filter, a linear order, topology, and open set measurability, if functions `a` and `b` tend to `A` and `B` respectively with respect to the filter and neighborhood filters at `A` and `B`, there exists an almost everywhere cover of the open interval `(A, B)` by the increasing countable union of closed-open intervals `[a(i), b(i))` from the filter.
|
MeasureTheory.integrableOn_Ioi_deriv_of_nonpos'
theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonpos' :
∀ {g g' : ℝ → ℝ} {a l : ℝ},
(∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x) →
(∀ x ∈ Set.Ioi a, g' x ≤ 0) →
Filter.Tendsto g Filter.atTop (nhds l) → MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume
The theorem `MeasureTheory.integrableOn_Ioi_deriv_of_nonpos'` states that: for any real-valued functions `g` and `g'`, and any real numbers `a` and `l`, if `g` has a derivative `g'` at every point `x` in the interval `[a, +∞)`, and `g'` is nonpositive for every point `x` in the interval `(a, +∞)`, and the function `g` has a limit `l` as `x` approaches infinity, then the derivative `g'` is integrable (in the sense of Lebesgue) over the interval `(a, +∞)`.
More concisely: If a real-valued function `g` has a derivative `g'` that is nonpositive and integrable over `(a, +∞)`, and `g` has a limit `l` as `x` approaches infinity, then `g'` is integrable over `(a, +∞)`.
|
MeasureTheory.AECover.mono
theorem MeasureTheory.AECover.mono :
∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
{ν : MeasureTheory.Measure α} {φ : ι → Set α},
MeasureTheory.AECover μ l φ → ν ≤ μ → MeasureTheory.AECover ν l φ
The theorem `MeasureTheory.AECover.mono` states that for any types `α` and `ι`, where `α` is equipped with a `MeasurableSpace` structure, and any measures `μ` and `ν` on `α`, a filter `l` on `ι`, and a function `φ` from `ι` to the set of `α`, if `φ` forms almost everywhere (a.e.) covers for the measure `μ` with respect to filter `l`, and `ν` is less than or equal to `μ` (i.e., `ν` is absolutely continuous with respect to `μ`), then `φ` also forms a.e. covers for the measure `ν` with respect to the same filter `l`. This theorem provides a monotonicity property for measures with respect to almost everywhere covers.
More concisely: If `φ` is an almost everywhere `μ`-covering function for a filter `l` on `ι` with respect to a measure `μ` on `α`, and `ν` is absolutely continuous with respect to `μ`, then `φ` is also an almost everywhere `ν`-covering function for filter `l` on `ι`.
|
MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto'
theorem MeasureTheory.integral_Iic_of_hasDerivAt_of_tendsto' :
∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} {m : E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E],
(∀ x ∈ Set.Iic a, HasDerivAt f (f' x) x) →
MeasureTheory.IntegrableOn f' (Set.Iic a) MeasureTheory.volume →
Filter.Tendsto f Filter.atBot (nhds m) → ∫ (x : ℝ) in Set.Iic a, f' x = f a - m
This theorem is a version of the Fundamental Theorem of Calculus-2 on semi-infinite intervals `(-∞, a)`. It states that given a function, `f`, that has a derivative, `f'`, and a limit, `m`, at `-∞`, if `f'` is integrable over the interval `(-∞, a)`, then the integral of `f'` on `(-∞, a)` equals `f(a) - m`. This version of the theorem assumes that the function `f` is differentiable on the closed interval `(-∞, a]`. It is also noted that a function with these properties always has a limit at `-∞`.
More concisely: If a function `f` with limit `m` at `-∞`, having a derivative `f'` that is integrable over `(-∞, a)`, is differentiable on `[-∞, a]`, then `∫(-∞, a] f' dx = f(a) - m`.
|
MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto'
theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto' :
∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} {m : E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E],
(∀ x ∈ Set.Ici a, HasDerivAt f (f' x) x) →
MeasureTheory.IntegrableOn f' (Set.Ioi a) MeasureTheory.volume →
Filter.Tendsto f Filter.atTop (nhds m) → ∫ (x : ℝ) in Set.Ioi a, f' x = m - f a
This theorem is a version of the second Fundamental Theorem of Calculus for semi-infinite intervals $(a, +\infty)$. It states that if a function $f$ has a limit $m$ at infinity, and its derivative $f'$ is integrable over the interval $(a, +\infty)$, and additionally, if the function $f$ is differentiable on the interval $[a, +\infty)$, then the integral of $f'$ over $(a, +\infty)$ equals to the difference $m - f(a)$. This theorem thus connects the limit of the function at infinity, its derivative and the value of the function at the point $a$.
More concisely: If a differentiable function $f$ on $(a, \infty)$ has a limit $m$ as $x \to \infty$ and its derivative $f'$ is integrable on $(a, \infty)$, then $\int\_a^\infty f'(x) dx = m - f(a)$.
|
MeasureTheory.AECover.inter
theorem MeasureTheory.AECover.inter :
∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
{φ ψ : ι → Set α},
MeasureTheory.AECover μ l φ → MeasureTheory.AECover μ l ψ → MeasureTheory.AECover μ l fun i => φ i ∩ ψ i
The theorem titled `MeasureTheory.AECover.inter` states that for all types `α` and `ι`, where `α` is equipped with a measurable space structure and `μ` is a measure on this space, given a filter `l` on `ι` and two functions `φ` and `ψ` from `ι` to the set of `α`, if both `φ` and `ψ` are almost everywhere covers (AECovers) with respect to measure `μ` and filter `l`, then the elementwise intersection of the sets given by `φ` and `ψ` is also an almost everywhere cover with respect to the same measure `μ` and filter `l`. In terms of measure theory, this theorem ensures that intersection of two AECovers is also an AECover.
More concisely: If `φ` and `ψ` are two almost everywhere covers of a measurable space `(α, Σ, μ)` with respect to filter `l`, then their elementwise intersection `φ ∩ ψ` is also an almost everywhere cover.
|
MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_tendsto
theorem MeasureTheory.integrableOn_Ioi_of_intervalIntegral_norm_tendsto :
∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [inst : l.NeBot]
[inst : l.IsCountablyGenerated] [inst : NormedAddCommGroup E] {b : ι → ℝ} {f : ℝ → E} (I a : ℝ),
(∀ (i : ι), MeasureTheory.IntegrableOn f (Set.Ioc a (b i)) μ) →
Filter.Tendsto b l Filter.atTop →
Filter.Tendsto (fun i => ∫ (x : ℝ) in a..b i, ‖f x‖ ∂μ) l (nhds I) →
MeasureTheory.IntegrableOn f (Set.Ioi a) μ
The theorem states that, for a function `f` mapping real numbers to an element of a normed additive commutative group `E`, if it is integrable on every interval of the form (a, b_i) and if the integral of the norm of `f(x)` from `a` to `b_i` converges to a real number `I` as `b_i` goes to infinity along a certain filter `l`, then `f` is integrable on the interval (a, ∞). Here, integrability of a function on a set means that the function is almost everywhere strongly measurable on that set and the integral of its pointwise norm over that set is less than infinity. The condition on `b_i` tending to infinity along a filter `l` is formalized using the concept of the limit of a function (`Filter.Tendsto`), with `l` being the source filter and the filter representing `→ ∞` (`Filter.atTop`) being the target filter.
More concisely: If a real-valued function `f` is integrable on every interval `(a, b_i)` and the limit as `b_i` approaches infinity along a filter `l` of the integrals of the norm of `f(x)` from `a` to `b_i` exists, then `f` is integrable on the interval `(a, ∞)`.
|
MeasureTheory.aecover_Ioi_of_Ioi
theorem MeasureTheory.aecover_Ioi_of_Ioi :
∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
[inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [inst_3 : OrderClosedTopology α]
[inst_4 : OpensMeasurableSpace α] {a : ι → α} {A : α},
Filter.Tendsto a l (nhds A) → MeasureTheory.AECover (μ.restrict (Set.Ioi A)) l fun i => Set.Ioi (a i)
This theorem states that for any measurable space `α`, any type `ι`, a measure `μ` on the measurable space `α`, a filter `l` on `ι`, a linear order on `α`, a topological space on `α`, an order-closed topology on `α`, an open-measurable space on `α`, and a function `a` from `ι` to `α`, if the function `a` tends to the neighborhood filter at a particular `A` in `α` under the filter `l`, then almost-everywhere cover (`AECover`) holds for the restriction of the measure `μ` to the set of all `α`'s greater than `A` (denoted by `Set.Ioi A`), with respect to the filter `l` and the function that maps each `i` in `ι` to the set of all `α`'s greater than `a i` (denoted by `Set.Ioi (a i)`).
In simpler terms, it states that if we are considering a measure restricted to values greater than a certain limit `A`, and if a function `a` tends to this limit under a certain filter, then almost everywhere (except possibly on a set of measure zero) each point `i` is associated with a set of values greater than `a i`.
More concisely: If `α` is a measurable space, `μ` is a measure on `α`, `l` is a filter on a type `ι`, `a : ι → α`, and `A ∈ α`, if `a` tends to the neighborhood filter of `A` under `l`, then `μ` almost-everywhere covers `Set.Ioi A` by the sets `Set.Ioi (a i)` for each `i ∈ ι` with respect to `l`.
|
MeasureTheory.integrableOn_Ioi_deriv_of_nonneg'
theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonneg' :
∀ {g g' : ℝ → ℝ} {a l : ℝ},
(∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x) →
(∀ x ∈ Set.Ioi a, 0 ≤ g' x) →
Filter.Tendsto g Filter.atTop (nhds l) → MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume
This theorem states that if a real-valued function `g` has a limit `l` at infinity, is differentiable on the left-closed and right-infinite interval `[a, +∞)`, with derivative `g'`, and the derivative `g'` is nonnegative on the left-open and right-infinite interval `(a, +∞)`, then `g'` is integrable on this latter interval.
To be more specific, the function `g` is assumed to have the derivative `g'(x)` at each point `x` in the interval `[a, +∞)` (denoted by the statement `∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x`). The derivative `g'` is also required to be nonnegative for all `x` in the interval `(a, +∞)` (expressed as `∀ x ∈ Set.Ioi a, 0 ≤ g' x`). Furthermore, `g` is assumed to have a limit `l` as `x` approaches infinity (expressed by `Filter.Tendsto g Filter.atTop (nhds l)`). Under these conditions, the theorem asserts that the derivative `g'` is integrable on the interval `(a, +∞)` with respect to the Lebesgue measure (`MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume`).
More concisely: If a real-valued function `g` with limit `l` at infinity, having a nonnegative, integrable derivative on the right-open interval `(a, +∞)`, is differentiable on the left-closed and right-infinite interval `[a, +∞)`, then `g'` is integrable on `(a, +∞)` with respect to Lebesgue measure.
|
MeasureTheory.aecover_Ioi
theorem MeasureTheory.aecover_Ioi :
∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
[inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [inst_3 : OrderClosedTopology α]
[inst_4 : OpensMeasurableSpace α] {a : ι → α},
Filter.Tendsto a l Filter.atBot → ∀ [inst_5 : NoMinOrder α], MeasureTheory.AECover μ l fun i => Set.Ioi (a i)
The theorem `MeasureTheory.aecover_Ioi` states that for any types `α` and `ι`, given a measurable space over `α` and a measure `μ` on that space, a filter `l` over `ι`, and a function `a` from `ι` to `α`, if `a` tends to negative infinity as per the filter `l`, then under the conditions that `α` has a linear order, a topological space, a closed order topology, and an open measurable space, and that `α` has no minimum order, there will always exist an almost everywhere convergent cover of the measure `μ` with respect to the filter `l`, where the cover is defined as the set of all elements greater than `a i` for all `i` in `ι`. In other words, we can cover almost all of the measurable space with sets of the form `(a i, ∞)` where `a i` is decreasing to negative infinity.
More concisely: Given a measurable space with a measure, a filter tending to negative infinity, and a decreasing sequence in a linearly ordered, topological space with no minimum, there exists an almost everywhere convergent cover by sets of the form `(a i, ∞)` where `a i` decreases through the filter.
|
MeasureTheory.integrableOn_Ioi_comp_rpow_iff'
theorem MeasureTheory.integrableOn_Ioi_comp_rpow_iff' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) {p : ℝ},
p ≠ 0 →
(MeasureTheory.IntegrableOn (fun x => x ^ (p - 1) • f (x ^ p)) (Set.Ioi 0) MeasureTheory.volume ↔
MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume)
This theorem states that for any normed additively commutative group `E` over the reals and any function `f` from the reals to `E`, and for any real number `p` different from 0, the function `f` is integrable over the interval `(0, ∞)` with respect to the Lebesgue measure if and only if the following modified function is also integrable over the same interval: for each `x`, multiply `f` evaluated at `x` to the power `p` by `x` to the power of `p - 1`. This theorem essentially asserts that the substitution `y = x ^ p` in integrals over `(0, ∞)` preserves the integrability of the function, without involving an absolute value of `p` factor.
More concisely: For a normed additively commutative group `E` over the reals, a function `f` from the reals to `E`, and real number `p ≠ 0`, `f` is Lebesgue integrable over `(0, ∞)` if and only if the function `x ↦ x^(p-1) * f(x)^p` is also Lebesgue integrable over `(0, ∞)`.
|
MeasureTheory.integral_comp_mul_left_Ioi
theorem MeasureTheory.integral_comp_mul_left_Ioi :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : ℝ → E) (a : ℝ) {b : ℝ},
0 < b → ∫ (x : ℝ) in Set.Ioi a, g (b * x) = b⁻¹ • ∫ (x : ℝ) in Set.Ioi (b * a), g x
This theorem states that for any normed additive commutative group `E`, any normed space over the reals `E`, a function `g` from the reals to `E`, and two real numbers `a` and `b` (where `b` is positive), the integral of `g` composed with multiplication by `b` over the open interval from `a` to infinity is equal to `b` inverse scaled by the integral of `g` over the open interval from `b*a` to infinity. In other words, it says that the integral of a function over a stretched interval can be calculated by adjusting the integrand function and scale the result by the reciprocal of the stretching factor.
More concisely: For any normed additive commutative group `E`, any normed space over the reals `E`, and real-valued function `g`, the integral of `g` multiplied by `b` from `a` to infinity equals `b^{-1}` times the integral of `g` from `b*a` to infinity.
|
MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto
theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_tendsto :
∀ {E : Type u_1} {f f' : ℝ → E} {a : ℝ} {m : E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E]
[inst_2 : CompleteSpace E],
ContinuousWithinAt f (Set.Ici a) a →
(∀ x ∈ Set.Ioi a, HasDerivAt f (f' x) x) →
MeasureTheory.IntegrableOn f' (Set.Ioi a) MeasureTheory.volume →
Filter.Tendsto f Filter.atTop (nhds m) → ∫ (x : ℝ) in Set.Ioi a, f' x = m - f a
This theorem is a version of the Fundamental Theorem of Calculus-2, focusing on semi-infinite intervals $(a, +\infty)$. It states that if a function has a limit `m` at infinity and its derivative is integrable, then the integral of the derivative over the interval $(a, +\infty)$ is equal to `m - f a`. This is under the assumption that the function is differentiable on the interval $(a, +\infty)$ and continuous at `a⁺`. In more formal terms, for a function `f` with derivative `f'` and a real number `a`, if `f` is continuous at `a` within the closed interval [a, +\infty), and for all `x` in the open interval (a, +\infty), `f` has a derivative at `x` that equals `f'(x)`, and if `f'` is integrable on the interval (a, +\infty), and if `f` tends to `m` at infinity, then the integral of `f'` over the interval (a, +\infty) equals `m - f a`.
More concisely: If a differentiable function `f` on the interval $(a,+\infty)$ with continuous derivative `f'` has a limit `m` at infinity and is integrable on $(a,+\infty)$, then $\int\_a^\infty f'(x) dx = m - f(a)$.
|
MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg
theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg :
∀ {g g' : ℝ → ℝ} {a l : ℝ},
ContinuousWithinAt g (Set.Ici a) a →
(∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x) →
(∀ x ∈ Set.Ioi a, 0 ≤ g' x) →
Filter.Tendsto g Filter.atTop (nhds l) → ∫ (x : ℝ) in Set.Ioi a, g' x = l - g a
This theorem states that for a function `g` that is differentiable on the open interval `(a, +∞)` and continuous at a point `a` within the closed interval `[a, +∞)`, if the derivative of the function `g` is nonnegative on `(a, +∞)`, and the function `g` has a limit `l` as `x` approaches infinity, then the integral of the derivative of `g` over the interval `(a, +∞)` is equal to `l - g(a)`. The function's derivative is also integrable on `(a, +∞)` as described in `integrable_on_Ioi_deriv_of_nonneg`.
More concisely: If a function `g` is differentiable on `(a, +∞)`, continuous at `a`, has nonnegative derivative on `(a, +∞)`, and has a limit `l` as `x` approaches infinity, then `∫(g' dx) = l - g(a)`.
|
MeasureTheory.aecover_Ioo_of_Ioc
theorem MeasureTheory.aecover_Ioo_of_Ioc :
∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
[inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [inst_3 : OrderClosedTopology α]
[inst_4 : OpensMeasurableSpace α] {a b : ι → α} {A B : α},
Filter.Tendsto a l (nhds A) →
Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun i => Set.Ioc (a i) (b i)
This theorem, `MeasureTheory.aecover_Ioo_of_Ioc`, states that for any types `α` and `ι`, a measurable space structure on `α`, a measure `μ` on `α`, a filter `l` on `ι`, a linear order, a topological space, an order closed topology and an open measurable space on `α`, given two function `a` and `b` mapping from `ι` to `α` and two real numbers `A` and `B`. If the function `a` tends to `A` with respect to filter `l` and the neighborhood filter at `A` and the function `b` tends to `B` with respect to filter `l` and the neighborhood filter at `B`, then the sequence of intervals `(a i, b i]` forms an almost everywhere convergent (aecover) sequence with respect to the measure restricted to the open interval `(A, B)` and the filter `l`. The term "almost everywhere" means that the set of `ι`'s where the property does not hold is of measure zero.
More concisely: Given measurable spaces `(α, μ)`, filters `l` on index set `ι`, linear order `<`, topological space `(α, τ)`, open measurable space `(α, μℙ)`, functions `a, b: ι → α`, real numbers `A, B`, and if `a` converges to `A` and `b` converges to `B` with respect to filters `l` and their neighborhood filters, then the sequence `(a i, b i]` is almost everywhere convergent to `A` with respect to measure `μ` restricted to the open interval `(A, B)` on set `α`.
|
HasCompactSupport.integral_Iic_deriv_eq
theorem HasCompactSupport.integral_Iic_deriv_eq :
∀ {E : Type u_1} {f : ℝ → E} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] [inst_2 : CompleteSpace E],
ContDiff ℝ 1 f → HasCompactSupport f → ∀ (b : ℝ), ∫ (x : ℝ) in Set.Iic b, deriv f x = f b
This theorem states that for a real-valued function `f` on a type `E` that is a normed additive commutative group, a normed space over the real numbers, and a complete space, if `f` is continuously differentiable of order `1` and has compact support, then the integral of the derivative of `f` over the closed interval from negative infinity up to a given real number `b` is equal to the value of `f` at `b`. In other words, this is a special case of the Fundamental Theorem of Calculus for functions with compact support.
More concisely: If `f` is a continuously differentiable, real-valued function of compact support on a complete normed additive commutative group `E`, then the integral of `f'` over `E` from `-(∞, ∞)` to `b` equals `f(b)`.
|
MeasureTheory.integral_comp_mul_deriv_Ioi
theorem MeasureTheory.integral_comp_mul_deriv_Ioi :
∀ {f f' g : ℝ → ℝ} {a : ℝ},
ContinuousOn f (Set.Ici a) →
Filter.Tendsto f Filter.atTop Filter.atTop →
(∀ x ∈ Set.Ioi a, HasDerivWithinAt f (f' x) (Set.Ioi x) x) →
ContinuousOn g (f '' Set.Ioi a) →
MeasureTheory.IntegrableOn g (f '' Set.Ici a) MeasureTheory.volume →
MeasureTheory.IntegrableOn (fun x => (g ∘ f) x * f' x) (Set.Ici a) MeasureTheory.volume →
∫ (x : ℝ) in Set.Ioi a, (g ∘ f) x * f' x = ∫ (u : ℝ) in Set.Ioi (f a), g u
The theorem `MeasureTheory.integral_comp_mul_deriv_Ioi` is a change-of-variables formula for integrals of scalar-valued functions over the interval `(a, ∞)`. It states that for any three real-valued functions `f`, `f'`, and `g`, and any real number `a`, given that `f` is continuous on the interval `[a, ∞)`, `f` tends to infinity as `x` tends to infinity, `f` has a derivative `f'(x)` at every point `x` in `(a, ∞)`, `g` is continuous on the image of `(a, ∞)` under `f`, `g` is integrable on the image of `[a, ∞)` under `f` with respect to the Lebesgue measure, and the function `x ↦ (g ∘ f)(x) * f'(x)` is integrable on `[a, ∞)` with respect to the Lebesgue measure, then the integral of `x ↦ (g ∘ f)(x) * f'(x)` over `(a, ∞)` is equal to the integral of `g` over `(f(a), ∞)`.
More concisely: If `f` is a continuous, increasing function tending to infinity, `f'(x)` exists for all `x` in `(a, ∞)`, `g` is continuous and integrable on `(f(a), ∞)`, then the integral of `g ∘ f(x) * f'(x)` over `[a, ∞)` equals the integral of `g` over `(f(a), ∞)`.
|
MeasureTheory.aecover_Ici
theorem MeasureTheory.aecover_Ici :
∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
[inst_1 : Preorder α] [inst_2 : TopologicalSpace α] [inst_3 : OrderClosedTopology α]
[inst_4 : OpensMeasurableSpace α] {a : ι → α},
Filter.Tendsto a l Filter.atBot → MeasureTheory.AECover μ l fun i => Set.Ici (a i)
The theorem `MeasureTheory.aecover_Ici` states that for any preordered, topological type `α` that also has order-closed topology and is an open measurable space, and for any function `a` from some type `ι` into `α`, if `a` tends to negative infinity (`Filter.atBot`) along a filter `l` on `ι`, then the function `i => Set.Ici (a i)` creates an almost everywhere cover (or: AECover) of the measure space determined by measure `μ` and the same filter `l`.
Here, the "almost everywhere cover" or AECover refers to a collection of sets indexed by `ι`, such that almost every point in the measure space is in one of the sets for large enough index according to the order on `ι`. The "tends to negative infinity" (`Filter.atBot`) concept signifies that for each real number, all sufficiently large elements in the sequence `a` are less than or equal to this number. The function `i => Set.Ici (a i)` generates the set of all elements in `α` that are greater than or equal to `a i` for each `i` in `ι`.
More concisely: Given a preordered, topological space α with order-closed topology and measurable structures, if a function from ι to α tends to negative infinity along filter l, then the family {Set.Ici (ai) | i ∈ ι} forms an almost everywhere cover of the measure space determined by measure μ and filter l.
|
MeasureTheory.AECover.integral_eq_of_tendsto
theorem MeasureTheory.AECover.integral_eq_of_tendsto :
∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
{l : Filter ι} [inst_1 : NormedAddCommGroup E] [inst_2 : NormedSpace ℝ E] [inst_3 : l.NeBot]
[inst_4 : l.IsCountablyGenerated] {φ : ι → Set α},
MeasureTheory.AECover μ l φ →
∀ {f : α → E} (I : E),
MeasureTheory.Integrable f μ →
Filter.Tendsto (fun n => ∫ (x : α) in φ n, f x ∂μ) l (nhds I) → ∫ (x : α), f x ∂μ = I
The theorem `MeasureTheory.AECover.integral_eq_of_tendsto` states that given a measurable space `α`, an index set `ι`, and a normed additive commutative group `E` over the real numbers, and given a filter `l` on `ι` that is countably generated and not the bottom filter, if `φ : ι → Set α` is an almost everywhere cover with respect to a measure `μ` and filter `l`, then for any `f : α → E` that is integrable with respect to `μ` and any `I : E`, if the sequence of integrals of `f` over the sets `φ n` converges in the filter `l` to `I` in the neighborhood filter of `I`, then the integral of `f` over the entire space `α` equals `I`.
In other words, if `f` is integrable, and the integrals of `f` over an almost everywhere cover of our space converge to a value `I`, then the overall integral of `f` must equal `I`.
More concisely: Given a measurable space with a countably generated, non-bottom filter, an almost everywhere covering family of sets, a measurable function, and a sequence of integrals of the function over the sets in the family converging to a limit, the limit is equal to the integral of the function over the entire space.
|
MeasureTheory.integrableOn_Ioi_deriv_of_nonneg
theorem MeasureTheory.integrableOn_Ioi_deriv_of_nonneg :
∀ {g g' : ℝ → ℝ} {a l : ℝ},
ContinuousWithinAt g (Set.Ici a) a →
(∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x) →
(∀ x ∈ Set.Ioi a, 0 ≤ g' x) →
Filter.Tendsto g Filter.atTop (nhds l) → MeasureTheory.IntegrableOn g' (Set.Ioi a) MeasureTheory.volume
This theorem, `MeasureTheory.integrableOn_Ioi_deriv_of_nonneg`, states that for any real-valued functions `g` and `g'` and any real numbers `a` and `l`, if `g` is continuous at `a` within the set of all real numbers greater than or equal to `a`, and if `g` has a derivative `g'(x)` at any point `x` strictly greater than `a`, with `g'(x)` being nonnegative for such `x`, and if `g` tends to `l` as `x` tends to infinity, then `g'` is integrable on the interval `(a, +∞)` with respect to the Lebesgue measure.
More concisely: If a real-valued function `g` is continuous at `a`, has nonnegative, integrable derivative on `(a, +∞)`, and tends to a limit `l` as `x` approaches infinity, then `g` is integrable on `(a, +∞)`.
|
MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos
theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos :
∀ {g g' : ℝ → ℝ} {a l : ℝ},
ContinuousWithinAt g (Set.Ici a) a →
(∀ x ∈ Set.Ioi a, HasDerivAt g (g' x) x) →
(∀ x ∈ Set.Ioi a, g' x ≤ 0) →
Filter.Tendsto g Filter.atTop (nhds l) → ∫ (x : ℝ) in Set.Ioi a, g' x = l - g a
This theorem states that if we have a real-valued function `g` (a function from real numbers to real numbers), whose derivative `g'` is nonpositive on the interval `(a, +∞)` and `g` is continuous at `a` from the right, then if `g` tends to a limit `l` as `x` approaches infinity, the integral of `g'` over `(a, +∞)` is equal to `l - g(a)`. The theorem assumes the function `g` is differentiable on `(a, +∞)` and continuous at `a` from the right. This is a significant statement in calculus, illustrating the connection between the properties of a function, its derivative, the limit behavior of the function, and the integral of its derivative.
More concisely: If a real-valued function `g` is differentiable with nonpositive derivative on `(a, +∞)`, continuous at `a` from the right, and tends to a limit `l` as `x` approaches infinity, then `∫(g'(x) dx) from a to +∞ = l - g(a)`.
|
MeasureTheory.aecover_Ioo_of_Icc
theorem MeasureTheory.aecover_Ioo_of_Icc :
∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
[inst_1 : LinearOrder α] [inst_2 : TopologicalSpace α] [inst_3 : OrderClosedTopology α]
[inst_4 : OpensMeasurableSpace α] {a b : ι → α} {A B : α},
Filter.Tendsto a l (nhds A) →
Filter.Tendsto b l (nhds B) → MeasureTheory.AECover (μ.restrict (Set.Ioo A B)) l fun i => Set.Icc (a i) (b i)
The theorem `MeasureTheory.aecover_Ioo_of_Icc` states that for any measurable space `α`, index type `ι`, measure `μ`, filter `l`, order-relevant and topology-relevant instances, and functions `a` and `b` mapping from `ι` to `α`, if `a` and `b` both tend towards some values `A` and `B` (respectively) with respect to the neighborhood filter, then we can almost everywhere cover the open interval `(A, B)` (with respect to the measure restricted to `(A, B)`) using closed intervals `[a(i), b(i)]` as `i` ranges over the index set under the filter `l`. This theorem characterizes a key property of measure theory in handling the transition from open to closed intervals.
More concisely: Given a measurable space, if functions mapping from an index set to the space tend towards two values, then there exists a sequence of closed intervals almost covering the open interval between those values with respect to the measure restricted to that interval.
|
MeasureTheory.integrableOn_Ioi_comp_rpow_iff
theorem MeasureTheory.integrableOn_Ioi_comp_rpow_iff :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (f : ℝ → E) {p : ℝ},
p ≠ 0 →
(MeasureTheory.IntegrableOn (fun x => (|p| * x ^ (p - 1)) • f (x ^ p)) (Set.Ioi 0) MeasureTheory.volume ↔
MeasureTheory.IntegrableOn f (Set.Ioi 0) MeasureTheory.volume)
This theorem states that for any real number `p` different from zero, a function `f` from the real numbers to a normed add-commutative group `E` is integrable over the set of real numbers greater than zero if and only if the function `g` defined as `g(x) = (|p| * x ^ (p - 1)) • f (x ^ p)` is integrable over the same set. Here, the operation `•` denotes the scalar multiplication in the vector space `E`, and `x ^ p` denotes the power of `x` to `p`. This theorem essentially says that the substitution `y = x ^ p` in integrals over the interval `(0, ∞)` preserves integrability.
More concisely: For any real number `p ≠ 0` and integrable function `f` from the positive real numbers to a normed add-commutative group `E`, the function `g(x) = (|p| * x ^ (p - 1)) • f (x ^ p)` is also integrable over the same interval.
|
MeasureTheory.intervalIntegral_tendsto_integral_Ioi
theorem MeasureTheory.intervalIntegral_tendsto_integral_Ioi :
∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [inst : l.IsCountablyGenerated]
[inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {b : ι → ℝ} {f : ℝ → E} (a : ℝ),
MeasureTheory.IntegrableOn f (Set.Ioi a) μ →
Filter.Tendsto b l Filter.atTop →
Filter.Tendsto (fun i => ∫ (x : ℝ) in a..b i, f x ∂μ) l (nhds (∫ (x : ℝ) in Set.Ioi a, f x ∂μ))
This theorem states that given any real-valued function `f` that is integrable over the interval `(a, ∞)` with respect to a measure `μ`, and a sequence of real numbers `b(i)` that tends to infinity, the limit of the function `f` integrated over the interval `[a, b(i)]` as `i` tends to infinity is equal to the integral of the function `f` over the interval `(a, ∞)`. In other words, as we extend the upper limit `b(i)` of our integral to infinity, the value of the integral becomes the integral of the function over the entire interval `(a, ∞)`.
More concisely: If `f` is an integrable real-valued function on the interval `(a, ∞)` with respect to `μ`, then `∫(a, ∞) f(x) dμ(x) = lim(i→∞) ∫(a, b(i)) f(x) dμ(x)`, where `b(i)` is a sequence tending to infinity.
|
MeasureTheory.integral_comp_rpow_Ioi
theorem MeasureTheory.integral_comp_rpow_Ioi :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] (g : ℝ → E) {p : ℝ},
p ≠ 0 → ∫ (x : ℝ) in Set.Ioi 0, (|p| * x ^ (p - 1)) • g (x ^ p) = ∫ (y : ℝ) in Set.Ioi 0, g y
This theorem, titled "Substitution `y = x ^ p` in integrals over `Ioi 0`", states that given a normed additively commutative group `E` and a normed space over `E`, for any real function `g` and any real number `p` not equal to zero, the integral from zero to infinity of `(|p| * x ^ (p - 1)) * g (x ^ p)` with respect to `x` is the same as the integral from zero to infinity of `g(y)` with respect to `y`. In simpler terms, it states that performing the substitution `y = x ^ p` in such integrals results in the same value.
More concisely: For a normed additive commutative group `E` and a normed space over `E`, the integral from 0 to infinity of `|p| * x ^ (p-1) * g(x ^ p) dx` equals the integral from 0 to infinity of `g(y) dy`, where `g` is a real function and `p` is a non-zero real number. (Substitution of `y = x ^ p` preserves integral values in these integrals.)
|
MeasureTheory.intervalIntegral_tendsto_integral_Iic
theorem MeasureTheory.intervalIntegral_tendsto_integral_Iic :
∀ {ι : Type u_1} {E : Type u_2} {μ : MeasureTheory.Measure ℝ} {l : Filter ι} [inst : l.IsCountablyGenerated]
[inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a : ι → ℝ} {f : ℝ → E} (b : ℝ),
MeasureTheory.IntegrableOn f (Set.Iic b) μ →
Filter.Tendsto a l Filter.atBot →
Filter.Tendsto (fun i => ∫ (x : ℝ) in a i..b, f x ∂μ) l (nhds (∫ (x : ℝ) in Set.Iic b, f x ∂μ))
The theorem `MeasureTheory.intervalIntegral_tendsto_integral_Iic` states that for all types `ι` and `E`, a measure `μ` on the real numbers, a filter `l` on `ι` that is countably generated, a normed additively commutative group `E` that is also a normed space over the real numbers, a function `a` from `ι` to the real numbers, a function `f` from the real numbers to `E`, and a real number `b`, if `f` is integrable on the set of real numbers less than or equal to `b` with respect to the measure `μ`, and if `a` tends to negative infinity with respect to the filter `l`, then the integral of `f` from `a(i)` to `b` with respect to `μ` tends to the integral of `f` over the set of real numbers less than or equal to `b` with respect to `μ` as `i` tends to negative infinity with respect to the filter `l`.
In simpler terms, this theorem relates the integral of a function over a semi-infinite interval to the limit of integrals of the function over finite intervals within that semi-infinite interval as one endpoint of the finite interval tends to negative infinity.
More concisely: For a countably generated filter `l` on `ι`, measure `μ` on the real numbers, normed additively commutative group `E`, integrable function `f` from the real numbers to `E`, and real number `b`, if `a(i)` tends to negative infinity with respect to `l` and the integral of `f` from `a(i)` to `b` tends to a limit with respect to `i` in `l`, then this limit is equal to the integral of `f` over the real numbers less than or equal to `b` with respect to `μ`.
|
MeasureTheory.AECover.integrable_of_lintegral_nnnorm_bounded
theorem MeasureTheory.AECover.integrable_of_lintegral_nnnorm_bounded :
∀ {α : Type u_1} {ι : Type u_2} {E : Type u_3} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α}
{l : Filter ι} [inst_1 : NormedAddCommGroup E] [inst_2 : l.NeBot] [inst_3 : l.IsCountablyGenerated]
{φ : ι → Set α},
MeasureTheory.AECover μ l φ →
∀ {f : α → E} (I : ℝ),
MeasureTheory.AEStronglyMeasurable f μ →
(∀ᶠ (i : ι) in l, ∫⁻ (x : α) in φ i, ↑‖f x‖₊ ∂μ ≤ ENNReal.ofReal I) → MeasureTheory.Integrable f μ
This theorem states that for any types `α`, `ι`, and `E`, given a measurable space `α`, a measure `μ` on `α`, a filter `l` on `ι` that is neither bottom nor empty and is countably generated, and a sequence of sets `φ` indexed by `ι` that forms an almost everywhere cover for `μ` and `l`, for any function `f` from `α` to `E`, if `f` is almost everywhere strongly measurable with respect to `μ`, and the nonnegative extended real number integral over each set `φ i` of the nonnegative part of the norm of `f` is almost everywhere less than or equal to some real number `I`, then `f` is integrable with respect to `μ`. That is, `f` is both almost everywhere strongly measurable and has finite integral.
More concisely: If `α` is a measurable space, `μ` is a measure on `α`, `l` is a countably generated, non-empty filter on `ι`, `φ` is an almost everywhere cover for `μ` and `l`, `f` is a strongly measurable function from `α` to a normed vector space `E`, and the nonnegative part of the norm of `f` is almost everywhere integrable over each `φ i` with respect to `μ` and sums up to a finite value `I`, then `f` is integrable with respect to `μ`.
|
MeasureTheory.AECover.superset
theorem MeasureTheory.AECover.superset :
∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
{φ ψ : ι → Set α},
MeasureTheory.AECover μ l φ →
(∀ (i : ι), φ i ⊆ ψ i) → (∀ (i : ι), MeasurableSet (ψ i)) → MeasureTheory.AECover μ l ψ
The theorem `MeasureTheory.AECover.superset` states that for any type `α`, index type `ι`, ambient measure space on `α` and a measure `μ` on `α`, given a filter `l` on `ι` and mappings `φ`, `ψ` from `ι` to the set of `α`, if `φ` forms an almost everywhere (a.e.) cover with respect to measure `μ` and filter `l`, and for every element `i` of `ι`, the set corresponding to `i` in `φ` is a subset of the set corresponding to `i` in `ψ`, and each of these `ψ` sets is measurable, then `ψ` also forms an almost everywhere cover with respect to the same measure `μ` and filter `l`.
In mathematical terms, an almost everywhere cover implies that for almost all points, we can find an element in the index such that the point is covered by the corresponding set. This theorem is about preserving this property under taking supersets that are measurable.
More concisely: If `φ` is an almost everywhere cover of `α` with respect to measure `μ` and filter `l` on index type `ι`, and for all `i ∈ ι`, `φ i` is a subset of `ψ i`, and each `ψ i` is measurable, then `ψ` is also an almost everywhere cover of `α` with respect to `μ` and `l`.
|
MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos'
theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonpos' :
∀ {g g' : ℝ → ℝ} {a l : ℝ},
(∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x) →
(∀ x ∈ Set.Ioi a, g' x ≤ 0) → Filter.Tendsto g Filter.atTop (nhds l) → ∫ (x : ℝ) in Set.Ioi a, g' x = l - g a
This theorem states that if a real-valued function `g` has a derivative `g'` at every point in the left-closed right-infinite interval greater than or equal to `a` (denoted as `[a, +∞)`), and this derivative is nonpositive for all points in the left-open right-infinite interval greater than `a` (denoted as `(a, +∞)`), and if `g` has a limit `l` at infinity, then the integral of the derivative `g'` over the interval `(a, +∞)` equals `l - g(a)`. In other words, the theorem relates the integral of a function's derivative on an open interval to the difference between the function's limit at infinity and its value at the lower bound of the interval, given certain conditions on the derivative.
More concisely: If a real-valued function `g` has a nonpositive, integrable derivative on the interval `(a, +∞)`, and has a limit `l` as `x` approaches infinity, then `∫(g'(x) dx) = l - g(a)`.
|
MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg'
theorem MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg' :
∀ {g g' : ℝ → ℝ} {a l : ℝ},
(∀ x ∈ Set.Ici a, HasDerivAt g (g' x) x) →
(∀ x ∈ Set.Ioi a, 0 ≤ g' x) → Filter.Tendsto g Filter.atTop (nhds l) → ∫ (x : ℝ) in Set.Ioi a, g' x = l - g a
The theorem `MeasureTheory.integral_Ioi_of_hasDerivAt_of_nonneg'` states that for any two functions `g` and `g'` mapping real numbers to real numbers, any two real numbers `a` and `l`, if the function `g` has a derivative `g'` at any point `x` in the interval `[a, +∞)`, and `g'` is nonnegative for all `x` in the interval `(a, +∞)`, and if the function `g` has a limit `l` at infinity, then the integral of the derivative `g'` on the interval `(a, +∞)` equals `l - g(a)`. Please note that the derivative `g'` is assumed to be integrable on `(a, +∞)` in this statement.
More concisely: If function `g` has a nonnegative, integrable derivative `g'` on `(a, +∞)`, and `g` has a finite limit `l` as `x` approaches infinity, then `∫(g' dx) from a to ∞ = l - g(a)`.
|
MeasureTheory.aecover_Iic
theorem MeasureTheory.aecover_Iic :
∀ {α : Type u_1} {ι : Type u_2} [inst : MeasurableSpace α] {μ : MeasureTheory.Measure α} {l : Filter ι}
[inst_1 : Preorder α] [inst_2 : TopologicalSpace α] [inst_3 : OrderClosedTopology α]
[inst_4 : OpensMeasurableSpace α] {b : ι → α},
Filter.Tendsto b l Filter.atTop → MeasureTheory.AECover μ l fun i => Set.Iic (b i)
The theorem `MeasureTheory.aecover_Iic` states that for any type `α` that is a measurable space, preordered, a topological space, and has an order-closed topology and is an open measurable space, and any function `b` from some type `ι` to `α`, if `b` tends to infinity with respect to some filter `l` on `ι`, then the sequence of left-infinite right-closed intervals `Set.Iic (b i)` almost everywhere covers the measure space `μ` with respect to the filter `l`. Here "almost everywhere" means except on a subset of measure zero.
In LaTeX terms, if $b : ι \rightarrow α$ and $b \rightarrow ∞$ when $i$ approaches some limit point with respect to the filter $l$, then $\{x | x ≤ b(i)\}$ almost everywhere covers $\mu$ as $i$ varies over the filter $l$.
More concisely: If `α` is a measurable space, preordered, a topological space with order-closed topology, and an open measurable space, and `b : ι -> α` tends to infinity with respect to a filter `l` on `ι`, then the sequence of left-infinite right-closed intervals `Set.Iic (b i)` almost everywhere covers `μ` as `i` varies over the filter `l`.
|