intervalIntegral.continuous_of_dominated_interval
theorem intervalIntegral.continuous_of_dominated_interval :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ}
{X : Type u_5} [inst_2 : TopologicalSpace X] [inst_3 : FirstCountableTopology X] {F : X → ℝ → E} {bound : ℝ → ℝ}
{a b : ℝ},
(∀ (x : X), MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))) →
(∀ (x : X), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t) →
IntervalIntegrable bound μ a b →
(∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Continuous fun x => F x t) → Continuous fun x => ∫ (t : ℝ) in a..b, F x t ∂μ
This theorem is about the continuity of the interval integral with respect to a parameter. It states that given a function `F` mapping from `X` to a function from `ℝ` to `E`, where each `F x` is almost everywhere strongly measurable on the interval `[a, b]`, and is bounded by a function that is independent of `x` and integrable on `[a, b]`, if the function `(fun x ↦ F x t)` is continuous for almost every `t` in `[a, b]`, then the function `(fun x ↦ ∫ t in a..b, F x t ∂μ)` is continuous. In simpler terms, if the functions `F x` have certain measurability, boundedness, and continuity properties, then the integral of `F x` over the interval `[a, b]` is a continuous function of `x`.
More concisely: If `F : X -> ℝ -> E` is a family of almost everywhere strongly measurable functions on `[a, b]` with bounded and integrable norm, and `(F x)` is continuous for almost every `t` in `[a, b]`, then the function `x => ∫ t in a..b, F x t ∂μ` is continuous.
|
intervalIntegral.continuousAt_of_dominated_interval
theorem intervalIntegral.continuousAt_of_dominated_interval :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ}
{X : Type u_5} [inst_2 : TopologicalSpace X] [inst_3 : FirstCountableTopology X] {F : X → ℝ → E} {x₀ : X}
{bound : ℝ → ℝ} {a b : ℝ},
(∀ᶠ (x : X) in nhds x₀, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))) →
(∀ᶠ (x : X) in nhds x₀, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t) →
IntervalIntegrable bound μ a b →
(∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ContinuousAt (fun x => F x t) x₀) →
ContinuousAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) x₀
This theorem, named `intervalIntegral.continuousAt_of_dominated_interval`, addresses the continuity of an interval integral with respect to a parameter at a certain point. Specifically, consider a function `F` mapping from a topological space `X` to a real-valued function on `E`, and a fixed point `x₀` in `X`. Assume that for almost every real number `t` in the interval `[a, b]`, `F x` is almost everywhere measurable on `[a, b]` for `x` in a neighborhood of `x₀` and it is bounded by a function `bound` that is independent of `x` and is integrable on `[a, b]`. If the function `(fun x ↦ F x t)` is continuous at `x₀` for almost every `t` in `[a, b]`, then the function `(fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀`, which represents the interval integral of `F x t` with respect to `μ`, is also continuous at `x₀`.
More concisely: If a function `F : X → ℝ → ℝ` satisfies certain conditions, then the function `x ↦ ∫ t in [a, b], F x t dμ` is continuous at `x₀` if `F x` is continuous at `x₀` for almost every `t` in `[a, b]`.
|
MeasureTheory.hasSum_integral_of_dominated_convergence
theorem MeasureTheory.hasSum_integral_of_dominated_convergence :
∀ {α : Type u_1} {G : Type u_3} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {ι : Type u_4} [inst_2 : Countable ι] {F : ι → α → G} {f : α → G}
(bound : ι → α → ℝ),
(∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F n) μ) →
(∀ (n : ι), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound n a) →
(∀ᵐ (a : α) ∂μ, Summable fun n => bound n a) →
MeasureTheory.Integrable (fun a => ∑' (n : ι), bound n a) μ →
(∀ᵐ (a : α) ∂μ, HasSum (fun n => F n a) (f a)) →
HasSum (fun n => ∫ (a : α), F n a ∂μ) (∫ (a : α), f a ∂μ)
This is the Lebesgue dominated convergence theorem for series. The theorem states that for any measure space `α` with a measure `μ`, normed add commutative group `G`, normed space `ℝ G`, and a countable index set `ι`. Given a series of functions `F : ι → α → G` and a function `f : α → G` which are almost everywhere (AE) strongly measurable with respect to the measure `μ`, and a bounding function `bound : ι → α → ℝ`. If for every index `n`, almost everywhere in the measure space `α`, the norm of the function `F n` is less than or equal to the function `bound n`, and the series of functions `bound n a` is summable, and the integral over the measure space `α` of the infinite sum of `bound n a` is finite, and almost everywhere in the measure space `α`, there exists a sum of the series `(F n a)` which is equal to `f a`, then there exists a sum of the series `(∫ (a : α), F n a ∂μ)` which is equal to `(∫ (a : α), f a ∂μ)`. This theorem is a key result in measure theory, allowing the interchange of summation and integration in certain circumstances.
More concisely: If a series of almost everywhere strongly measurable functions from a measure space to a normed add commutative group, each bounded almost everywhere by a summable function, converges almost everywhere to a function, then the series of integrals of the functions converges to the integral of the limit function with respect to the given measure.
|
intervalIntegral.hasSum_integral_of_dominated_convergence
theorem intervalIntegral.hasSum_integral_of_dominated_convergence :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
{μ : MeasureTheory.Measure ℝ} {ι : Type u_5} [inst_2 : Countable ι] {F : ι → ℝ → E} (bound : ι → ℝ → ℝ),
(∀ (n : ι), MeasureTheory.AEStronglyMeasurable (F n) (μ.restrict (Ι a b))) →
(∀ (n : ι), ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F n t‖ ≤ bound n t) →
(∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → Summable fun n => bound n t) →
IntervalIntegrable (fun t => ∑' (n : ι), bound n t) μ a b →
(∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → HasSum (fun n => F n t) (f t)) →
HasSum (fun n => ∫ (t : ℝ) in a..b, F n t ∂μ) (∫ (t : ℝ) in a..b, f t ∂μ)
This theorem is a version of the Lebesgue Dominated Convergence Theorem for parametric interval integrals. It specifies that given a measure 'μ' and a sequence of functions 'F : ι → ℝ → E', where each function is almost everywhere strongly measurable with respect to the measure restricted to a given interval '[a, b]', and almost everywhere within this interval, the norm of each function is bounded by a certain function 'bound', which is also summable. Moreover, if the function 'f' is the limit of the sequence of functions 'F' almost everywhere in the interval, and the interval integral of the sum of the bounding functions is well-defined, then the interval integral of the limit function 'f' is equal to the limit of the interval integrals of the functions in the sequence 'F'. In other words, swapping the order of taking limit and interval integral is justified under these conditions.
More concisely: Given a measure 'μ', a sequence of almost everywhere strongly measurable and norm-bounded functions 'F : ι → L¹([a, b], μ), and a function 'f' that is the almost everywhere limit of the sequence 'F' in [a, b], if the interval integrals of the bounding functions are summable, then the limit function 'f' is integrable and ∫[a, b] f dμ = limₙ ∫[a, b] Fₙ dμ.
|
MeasureTheory.tendsto_integral_filter_of_dominated_convergence
theorem MeasureTheory.tendsto_integral_filter_of_dominated_convergence :
∀ {α : Type u_1} {G : Type u_3} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {ι : Type u_4} {l : Filter ι} [inst_2 : l.IsCountablyGenerated] {F : ι → α → G}
{f : α → G} (bound : α → ℝ),
(∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) μ) →
(∀ᶠ (n : ι) in l, ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) →
MeasureTheory.Integrable bound μ →
(∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) l (nhds (f a))) →
Filter.Tendsto (fun n => ∫ (a : α), F n a ∂μ) l (nhds (∫ (a : α), f a ∂μ))
The theorem `MeasureTheory.tendsto_integral_filter_of_dominated_convergence` is a version of the Lebesgue Dominated Convergence theorem for filters with a countable basis. This theorem says that, given a measure space, a measure and a filter (that has a countable basis) over a function from indices to the space of measurable functions, if for almost every `n` in this filter, the function `F n` is almost everywhere strongly measurable and for almost all `a` in the measure, the norm of `F n a` is less than or equal to some bound, and if the bound is an integrable function, and if for almost all `a` in the measure, the function `F n a` tends to `f a` in the neighborhood filter, then the function that maps `n` to the integral of `F n a` under the measure tends to the integral of `f a` under the measure in the original filter. In simpler terms, it states that if a sequence of functions converges almost everywhere, is dominated by an integrable function, and each function in the sequence is almost everywhere strongly measurable, then the integral of the limit function is the limit of the integrals of the functions in the sequence.
More concisely: If a sequence of almost everywhere strongly measurable functions, each dominated by an integrable function, converges almost everywhere, then the integrals of the converging sequence converge to the integral of their limit function.
|
intervalIntegral.hasSum_intervalIntegral_of_summable_norm
theorem intervalIntegral.hasSum_intervalIntegral_of_summable_norm :
∀ {ι : Type u_1} {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : CompleteSpace E] [inst_2 : NormedSpace ℝ E]
{a b : ℝ} [inst_3 : Countable ι] {f : ι → C(ℝ, E)},
(Summable fun i => ‖ContinuousMap.restrict (↑{ carrier := Set.uIcc a b, isCompact' := ⋯ }) (f i)‖) →
HasSum (fun i => ∫ (x : ℝ) in a..b, (f i) x) (∫ (x : ℝ) in a..b, ∑' (i : ι), (f i) x)
This theorem states that interval integrals commute with countable sums, under the condition that the supremum norms of the functions are summable. This is a special case of the dominated convergence theorem. More specifically, given a countable series of continuous real-valued functions indexed by ι, if the supremum norms of the restrictions of these functions to the interval [a, b] are summable, then the countable sum of the interval integrals of these functions equals to the interval integral of the countable sum of these functions.
More concisely: If a countable series of continuous real-valued functions on an interval [a, b] has summable supremum norms, then the interval integrals of the series are equal to the interval integral of their sum.
|
intervalIntegral.tendsto_integral_filter_of_dominated_convergence
theorem intervalIntegral.tendsto_integral_filter_of_dominated_convergence :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b : ℝ} {f : ℝ → E}
{μ : MeasureTheory.Measure ℝ} {ι : Type u_5} {l : Filter ι} [inst_2 : l.IsCountablyGenerated] {F : ι → ℝ → E}
(bound : ℝ → ℝ),
(∀ᶠ (n : ι) in l, MeasureTheory.AEStronglyMeasurable (F n) (μ.restrict (Ι a b))) →
(∀ᶠ (n : ι) in l, ∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → ‖F n x‖ ≤ bound x) →
IntervalIntegrable bound μ a b →
(∀ᵐ (x : ℝ) ∂μ, x ∈ Ι a b → Filter.Tendsto (fun n => F n x) l (nhds (f x))) →
Filter.Tendsto (fun n => ∫ (x : ℝ) in a..b, F n x ∂μ) l (nhds (∫ (x : ℝ) in a..b, f x ∂μ))
The Lebesgue Dominated Convergence theorem for filters with a countable basis is stated as follows: Given a normed additive commutative group `E` and normed space over the reals `ℝ` with a measure `μ` and a filter `l` with a countable basis, a sequence of functions `F : ι → ℝ → E` that are `AEStronglyMeasurable` and bounded by a function `bound`, if the function `bound` is interval integrable and for almost every `x` in the interval 'a' to 'b', the sequence `F` converges to a function `f` at `x`, then the interval integrals of the functions `F` also converge to the interval integral of the function `f` with respect to the measure `μ`. In mathematical notation, if $F_n(x)$ converges to $f(x)$ for almost every $x$ and is dominated by a Lebesgue integrable function `bound`, then $\int_a^b F_n(x) dμ$ converges to $\int_a^b f(x) dμ$.
More concisely: If `F : ι → ℝ → E` is a sequence of `AEStronglyMeasurable` and bounded functions on a normed additive commutative group `E` over the reals `ℝ` with a measure `μ`, dominated by a Lebesgue integrable function `bound`, and converging almost everywhere to a function `f` on the interval '[a, b]', then the interval integrals of `F` converge to the interval integral of `f` with respect to `μ`. In mathematical notation, $\int_a^b \lim\_{n\to\infty} F_n(x) d\mu = \lim\_{n\to\infty} \int_a^b F_n(x) d\mu$.
|
intervalIntegral.continuousWithinAt_of_dominated_interval
theorem intervalIntegral.continuousWithinAt_of_dominated_interval :
∀ {E : Type u_3} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {μ : MeasureTheory.Measure ℝ}
{X : Type u_5} [inst_2 : TopologicalSpace X] [inst_3 : FirstCountableTopology X] {F : X → ℝ → E} {x₀ : X}
{bound : ℝ → ℝ} {a b : ℝ} {s : Set X},
(∀ᶠ (x : X) in nhdsWithin x₀ s, MeasureTheory.AEStronglyMeasurable (F x) (μ.restrict (Ι a b))) →
(∀ᶠ (x : X) in nhdsWithin x₀ s, ∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ‖F x t‖ ≤ bound t) →
IntervalIntegrable bound μ a b →
(∀ᵐ (t : ℝ) ∂μ, t ∈ Ι a b → ContinuousWithinAt (fun x => F x t) s x₀) →
ContinuousWithinAt (fun x => ∫ (t : ℝ) in a..b, F x t ∂μ) s x₀
This theorem states the continuity of interval integral with respect to a parameter, at a point within a set. Let's denote `F : X → ℝ → E` as a function that maps a point in `X` and a real number to a space `E`. The theorem assumes that `F x` is almost everywhere measurable on an unordered interval `[a, b]` for each `x` in a neighbourhood of some point `x₀` within a given set `s` and at `x₀` itself. It also assumes that `F x` is bounded by a function that is integrable on `[a, b]` and does not depend on `x` in a neighbourhood of `x₀` within `s`. If the function `(fun x ↦ F x t)` is continuous at `x₀` within `s` for almost every `t` in `[a, b]`, then the function `(fun x ↦ ∫ t in a..b, F x t ∂μ) s x₀` is also continuous at `x₀` within `s`. Here, ∫ denotes the integral of the function over the interval `[a, b]` with respect to the measure `μ`.
More concisely: If `F : X → ℝ → E` is an almost everywhere measurable and locally bounded function on an interval `[a, b]` such that `F x` is continuous in `x` almost everywhere in `s` and `∫|F x|∂μ` is finite for all `x` in a neighborhood of `x₀` in `s`, then the function `x ↦ ∫ t in a..b, F x t ∂μ` is continuous at `x₀` in `s`.
|
intervalIntegral.continuousWithinAt_primitive
theorem intervalIntegral.continuousWithinAt_primitive :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b₀ b₁ b₂ : ℝ}
{μ : MeasureTheory.Measure ℝ} {f : ℝ → E},
↑↑μ {b₀} = 0 →
IntervalIntegrable f μ (min a b₁) (max a b₂) →
ContinuousWithinAt (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Set.Icc b₁ b₂) b₀
This theorem states that for any normed additively commutative group `E` and normed space over the real numbers, given five real numbers `a`, `b₀`, `b₁`, `b₂`, a measure `μ` on the real numbers, and a function `f` from the real numbers to `E`, if the measure of the singleton set `{b₀}` is zero and the function `f` is interval integrable with respect to the measure `μ` on the interval from `min(a, b₁)` to `max(a, b₂)`, then the function that maps a real number `b` to the interval integral of `f` from `a` to `b` with respect to the measure `μ` is continuous at the point `b₀` within the closed interval from `b₁` to `b₂`. In other words, as `b` tends to `b₀` within the interval `[b₁, b₂]`, the integral of `f` from `a` to `b` tends to the integral of `f` from `a` to `b₀`.
More concisely: If `E` is a normed additively commutative group, `μ` is a measure on the real numbers with `{b₀}` having measure 0, and `f` is interval integrable on `[min(a, b₁), max(a, b₂)]`, then the function that maps `b` to the interval integral of `f` from `a` to `b` with respect to `μ` is continuous at `b₀`.
|
intervalIntegral.continuousOn_primitive_interval'
theorem intervalIntegral.continuousOn_primitive_interval' :
∀ {E : Type u_1} [inst : NormedAddCommGroup E] [inst_1 : NormedSpace ℝ E] {a b₁ b₂ : ℝ}
{μ : MeasureTheory.Measure ℝ} {f : ℝ → E} [inst_2 : MeasureTheory.NoAtoms μ],
IntervalIntegrable f μ b₁ b₂ →
a ∈ Set.uIcc b₁ b₂ → ContinuousOn (fun b => ∫ (x : ℝ) in a..b, f x ∂μ) (Set.uIcc b₁ b₂)
The theorem `intervalIntegral.continuousOn_primitive_interval'` states that for any real numbers `a`, `b₁`, and `b₂`, a measure `μ` on the real numbers, and a function `f` mapping real numbers to an element of a normed add commutative group `E` (also a normed space over the real numbers), under the assumption that `μ` has no atoms (i.e., there is no set of measure zero with a non-empty interior), if `f` is interval integrable with respect to `μ` on the unordered interval from `b₁` to `b₂`, then the function defined as the interval integral of `f` from `a` to `b` with respect to `μ` is continuous on the set of elements lying between `b₁` and `b₂`, inclusive. The continuity is ensured for every point of that set with respect to that set. In other words, the integral function behaves nicely (is continuous) when calculated over intervals within the set bounded by `b₁` and `b₂`.
More concisely: If a measure with no atoms has a function that is interval integrable on an interval, then the integral function is continuous on that interval.
|
MeasureTheory.tendsto_integral_of_dominated_convergence
theorem MeasureTheory.tendsto_integral_of_dominated_convergence :
∀ {α : Type u_1} {G : Type u_3} [inst : NormedAddCommGroup G] [inst_1 : NormedSpace ℝ G] {m : MeasurableSpace α}
{μ : MeasureTheory.Measure α} {F : ℕ → α → G} {f : α → G} (bound : α → ℝ),
(∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (F n) μ) →
MeasureTheory.Integrable bound μ →
(∀ (n : ℕ), ∀ᵐ (a : α) ∂μ, ‖F n a‖ ≤ bound a) →
(∀ᵐ (a : α) ∂μ, Filter.Tendsto (fun n => F n a) Filter.atTop (nhds (f a))) →
Filter.Tendsto (fun n => ∫ (a : α), F n a ∂μ) Filter.atTop (nhds (∫ (a : α), f a ∂μ))
The **Lebesgue dominated convergence theorem** provides conditions for the convergence of the integrals of a sequence of functions given their almost everywhere convergence. Given a sequence of functions `F : ℕ → α → G` and a function `f : α → G`, in a measure space `α` equipped with a measure `μ`, and a normed space `G`, if every function in the sequence `F` is "almost everywhere strongly measurable" with respect to `μ`, and there exists a "bound" function that is integrable with respect to `μ` and dominates every function in the sequence `F` almost everywhere, then if the sequence of functions `F` converges almost everywhere to the function `f`, the Lebesgue integral of the sequence `F` converges to the Lebesgue integral of `f`. In simpler terms, this theorem states that as long as the functions in the sequence `F` do not oscillate too much and are dominated by an integrable function, the integral of the limit is the limit of the integrals.
More concisely: If a sequence of almost everywhere strongly measurable functions from a measure space to a normed vector space converges almost everywhere to a function, and there exists an integrable dominating function, then the sequence of integrals converges to the integral of the limit function.
|