MeasureTheory.integrableOn_union
theorem MeasureTheory.integrableOn_union :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s t : Set α}
{μ : MeasureTheory.Measure α},
MeasureTheory.IntegrableOn f (s ∪ t) μ ↔ MeasureTheory.IntegrableOn f s μ ∧ MeasureTheory.IntegrableOn f t μ
This theorem, `MeasureTheory.integrableOn_union`, states that for any measure space `α`, any normed additive commutative group `E`, any function `f` from `α` to `E`, any two sets `s` and `t` of `α`, and any measure `μ` on `α`, the function `f` is integrable on the union of `s` and `t` with respect to the measure `μ` if and only if `f` is integrable on both `s` and `t` separately with respect to `μ`. In mathematical terms, if $\int_{s \cup t} |f| d\mu < \infty$, then $\int_s |f| d\mu < \infty$ and $\int_t |f| d\mu < \infty$, and vice versa.
More concisely: A function from a measure space to a normed additive commutative group is integrable over the union of two sets if and only if it is integrable over each set separately.
|
ContinuousOn.stronglyMeasurableAtFilter
theorem ContinuousOn.stronglyMeasurableAtFilter :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : TopologicalSpace β]
[inst_4 : TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : SecondCountableTopologyEither α β] {f : α → β}
{s : Set α} {μ : MeasureTheory.Measure α},
IsOpen s → ContinuousOn f s → ∀ x ∈ s, StronglyMeasurableAtFilter f (nhds x) μ
The theorem states that if a function is continuous on an open set `s`, then the function is strongly measurable at every point `x` in `s` with respect to the neighborhood filter of `x`, provided that either the source space or the target space is second-countable. Here, a function is strongly measurable at a filter if it is almost everywhere strongly measurable with respect to the measure restricted to a set within the filter. Secondly, a space is second-countable if it has a countable base for its topology. Continuous on an open set means that the function is continuous at every point within that set. The neighborhood filter at a point is the infimum over the principal filters of all open sets containing that point.
More concisely: If a function is continuous on an open set in a second-countable topological space, then it is strongly measurable at every point in the set with respect to the neighborhood filter of that point.
|
MeasureTheory.integrableOn_congr_fun
theorem MeasureTheory.integrableOn_congr_fun :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f g : α → E} {s : Set α}
{μ : MeasureTheory.Measure α},
Set.EqOn f g s → MeasurableSet s → (MeasureTheory.IntegrableOn f s μ ↔ MeasureTheory.IntegrableOn g s μ)
The theorem `MeasureTheory.integrableOn_congr_fun` states that for any type `α` with a measurable space structure and any normed add commutative group `E`, given two functions `f` and `g` from `α` to `E`, a set `s` of type `α`, and a measure `μ` on `α`, if `f` and `g` are equal on set `s` and `s` is a measurable set, then `f` is integrable on set `s` with respect to measure `μ` if and only if `g` is also integrable on the same set with respect to the same measure. In other words, the integrability of two functions that are equal on a measurable set is equivalent.
More concisely: If `s` is a measurable subset of a measurable space `(α, Σ, μ)` and `f = g` almost everywhere on `s`, then `f` and `g` are integrable on `s` with respect to `μ` if and only if they are both integrable.
|
MeasureTheory.Integrable.integrableOn
theorem MeasureTheory.Integrable.integrableOn :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s : Set α}
{μ : MeasureTheory.Measure α}, MeasureTheory.Integrable f μ → MeasureTheory.IntegrableOn f s μ
The theorem `MeasureTheory.Integrable.integrableOn` states that for any types `α` and `E`, where `α` has a measurable space structure and `E` is a normed add commutative group, and for any function `f` from `α` to `E`, any set `s` of type `α`, and any measure `μ` on `α`, if the function `f` is integrable with respect to the measure `μ`, then the function `f` is also integrable on the set `s` with respect to the measure `μ`. In other words, if a function is integrable over the whole space, it is also integrable on any subset of that space.
More concisely: If a function is integrable with respect to a measure on a measurable space, then it is integrable over any measurable subset of that space.
|
MeasureTheory.IntegrableOn.integrable_of_forall_not_mem_eq_zero
theorem MeasureTheory.IntegrableOn.integrable_of_forall_not_mem_eq_zero :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s : Set α}
{μ : MeasureTheory.Measure α},
MeasureTheory.IntegrableOn f s μ → (∀ x ∉ s, f x = 0) → MeasureTheory.Integrable f μ
The theorem `MeasureTheory.IntegrableOn.integrable_of_forall_not_mem_eq_zero` states that for any two types `α` and `E`, where `α` is a measurable space and `E` is a normed group, if a function `f` from `α` to `E` is integrable over a set `s` with respect to the measure `μ`, and the function `f` equals zero for all elements outside the set `s`, then the function `f` is integrable with respect to the measure `μ`. This theorem connects the concept of a function being integrable on a specific set to the function being integrable over the entire space, given particular conditions.
More concisely: If a measurable function from a measurable space to a normed group is integrable over a set and vanishes outside that set, then the function is integrable over the entire space.
|
ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin
theorem ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin :
∀ {α : Type u_5} {β : Type u_6} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : TopologicalSpace β]
[inst_4 : TopologicalSpace.PseudoMetrizableSpace β] [inst_5 : SecondCountableTopologyEither α β] {f : α → β}
{s : Set α} {μ : MeasureTheory.Measure α},
ContinuousOn f s → MeasurableSet s → ∀ (x : α), StronglyMeasurableAtFilter f (nhdsWithin x s) μ
The theorem `ContinuousOn.stronglyMeasurableAtFilter_nhdsWithin` states that for any function `f` from a measurable space `α` to a topological space `β`, if `f` is continuous on a measurable set `s` and `s` itself is measurable, then `f` is strongly measurable at the filter `nhdsWithin x s` (the "neighborhood within" filter, which contains sets that intersect with `s` and a neighborhood of `x`) for all `x` in `α`. This holds under the conditions that `α` is a topological space, is an open measurable space, and `β` is a pseudometrizable topological space and either `α` or `β` has a second countable topology.
More concisely: If `f: α → β` is a continuous function on the measurable set `s` of the topological space `α` (which is itself measurable, open, and second countable or pseudometrizable), then `f` is strongly measurable at the filter `nhdsWithin x s` for all `x` in `α`.
|
Filter.Tendsto.integrableAtFilter
theorem Filter.Tendsto.integrableAtFilter :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E}
{μ : MeasureTheory.Measure α} {l : Filter α} [inst_2 : l.IsMeasurablyGenerated],
StronglyMeasurableAtFilter f l μ →
μ.FiniteAtFilter l → ∀ {b : E}, Filter.Tendsto f l (nhds b) → MeasureTheory.IntegrableAtFilter f l μ
The theorem `Filter.Tendsto.integrableAtFilter` states that for any measurable space `α`, normed additive commutative group `E`, function `f` from `α` to `E`, measure `μ`, and a filter `l` over `α` that is measurably generated, if `f` is strongly measurable at filter `l` with respect to measure `μ`, and if measure `μ` is finite at filter `l`, then for any `b` in `E`, if `f` tends to `b` at filter `l` (meaning, for every neighborhood of `b`, the preimage of this neighborhood under `f` is a set in the filter `l`), `f` is integrable at filter `l`. In other words, the function `f` is integrable at the filter `l` if it is strongly measurable, the measure is finite, and the function tends to some point in the target space when evaluated on the sets of the filter.
More concisely: If a strongly measurable function from a measurable space to a normed additive commutative group tends to a limit at a measurably generated filter with finite measure, then the function is integrable at that filter.
|
MeasureTheory.IntegrableOn.union
theorem MeasureTheory.IntegrableOn.union :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s t : Set α}
{μ : MeasureTheory.Measure α},
MeasureTheory.IntegrableOn f s μ → MeasureTheory.IntegrableOn f t μ → MeasureTheory.IntegrableOn f (s ∪ t) μ
The theorem `MeasureTheory.IntegrableOn.union` states that for any given measurable space `α`, normed additive commutative group `E`, a function `f` from `α` to `E`, two sets `s` and `t` of `α`, and a measure `μ` on `α`, if the function `f` is integrable on the set `s` with respect to the measure `μ` and also integrable on the set `t` with respect to the measure `μ`, then the function `f` is integrable on the union of the sets `s` and `t` with respect to the same measure `μ`.
In mathematical terms, if a function is integrable on two separate sets, it is also integrable on the union of those two sets.
More concisely: If `f : α → E` is integrable with respect to measure `μ` on sets `s` and `t` of `α`, then `f` is integrable on their union `s ∪ t`.
|
MeasureTheory.IntegrableAtFilter.neg
theorem MeasureTheory.IntegrableAtFilter.neg :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
{μ : MeasureTheory.Measure α} {l : Filter α} {f : α → E},
MeasureTheory.IntegrableAtFilter f l μ → MeasureTheory.IntegrableAtFilter (-f) l μ
The theorem `MeasureTheory.IntegrableAtFilter.neg` states that for any measurable space `α`, normed additive commutative group `E`, measure `μ` on `α`, filter `l` on `α`, and function `f` from `α` to `E`, if `f` is integrable at the filter `l`, then the negation of `f`, denoted by `-f`, is also integrable at the same filter `l`. Essentially, it implies that the integrability property at a particular filter is preserved under the operation of function negation.
More concisely: If a measurable function $f : \alpha \to E$ is integrable at the filter $l$ on the measurable space $(\alpha, \Sigma, \mu)$, then the negation of $f$, $-f$, is also integrable at the filter $l$.
|
ContinuousOn.aestronglyMeasurable_of_isCompact
theorem ContinuousOn.aestronglyMeasurable_of_isCompact :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : TopologicalSpace β]
[inst_4 : TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {s : Set α} {μ : MeasureTheory.Measure α},
ContinuousOn f s → IsCompact s → MeasurableSet s → MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
This theorem states that for any function `f` which maps elements from a measurable space `α` to a topological space `β`, and for any compact measurable subset `s` of `α`, if the function `f` is continuous on this subset `s`, then `f` is almost everywhere strongly measurable with respect to the measure `μ` restricted to `s`. Here, "almost everywhere strongly measurable" means that the function is almost everywhere equal to the limit of a sequence of simple functions, and "continuous on `s`" means that `f` is continuous at every point in `s`. The condition "compact" for the set `s` means that for every nontrivial filter `f` that contains `s`, there exists an element of `s` that is a cluster point for the filter `f`.
More concisely: If `f` is a function from a measurable space `α` to a topological space `β`, `s` is a compact measurable subset of `α`, and `f` is continuous on `s`, then `f` is almost everywhere strongly measurable with respect to the restriction of the measure `μ` on `s`.
|
MeasureTheory.Integrable.integrableAtFilter
theorem MeasureTheory.Integrable.integrableAtFilter :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E}
{μ : MeasureTheory.Measure α},
MeasureTheory.Integrable f μ → ∀ (l : Filter α), MeasureTheory.IntegrableAtFilter f l μ
The theorem `MeasureTheory.Integrable.integrableAtFilter` states that for any given measurable space `α`, type `E` forming a Normed Additive Commutative Group, a function `f` mapping from `α` to `E`, and a measure `μ` on `α`, if the function `f` is integrable with respect to the measure `μ`, then `f` is integrable at any filter `l` on `α` with respect to the same measure `μ`. In other words, if a function is integrable over the whole space, it is also integrable over any subset of that space described by a filter.
More concisely: If a measurable function is integrable with respect to a measure, then it is integrable with respect to any filter on the measurable space with respect to the same measure.
|
MeasureTheory.IntegrableOn.of_forall_diff_eq_zero
theorem MeasureTheory.IntegrableOn.of_forall_diff_eq_zero :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s t : Set α}
{μ : MeasureTheory.Measure α},
MeasureTheory.IntegrableOn f s μ → MeasurableSet t → (∀ x ∈ t \ s, f x = 0) → MeasureTheory.IntegrableOn f t μ
This theorem states that for any measure space `α`, any normed additively commutative group `E`, any function `f` from `α` to `E`, and any two sets `s` and `t` of `α`, given a measure `μ` on `α`, if the function `f` is integrable on the set `s` under measure `μ`, and the function `f` vanishes on the set difference `t \ s` (i.e., for all `x` in `t \ s`, `f(x) = 0`), and the set `t` is measurable, then the function `f` is also integrable on the set `t` under measure `μ`.
In other words, if a function is integrable on a set and equals zero everywhere outside this set within a larger measurable set, then the function is also integrable on the larger set.
More concisely: If a measurable function that is integrable on a set in a measure space equals zero almost everywhere on the difference of another measurable set and the first set, then the function is integrable on the larger measurable set.
|
ContinuousOn.aestronglyMeasurable_of_isSeparable
theorem ContinuousOn.aestronglyMeasurable_of_isSeparable :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalSpace.PseudoMetrizableSpace α] [inst_3 : OpensMeasurableSpace α]
[inst_4 : TopologicalSpace β] [inst_5 : TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {s : Set α}
{μ : MeasureTheory.Measure α},
ContinuousOn f s →
MeasurableSet s → TopologicalSpace.IsSeparable s → MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
This theorem asserts that if a given function is continuous on a separable set `s`, then this function is almost everywhere strongly measurable with respect to a measure restricted to `s`. More specifically, given a measure space `α`, a topological space `α`, a pseudometrizable space `α`, an opens measurable space `α`, a topological space `β`, a pseudometrizable space `β`, a function `f` from `α` to `β`, a set `s` in `α`, and a measure `μ` on `α`, if `f` is continuous on `s`, `s` is a measurable set, and `s` is separable (i.e., it is contained in the closure of a countable set), then `f` is almost everywhere strongly measurable with respect to the measure `μ` restricted to `s`. Here, a function is called almost everywhere strongly measurable if it is almost everywhere equal to the limit of a sequence of simple functions.
More concisely: If a continuous function on a separable, measurable subset of a pseudometrizable topological space with respect to a measure is restricted to that subset, then the function is almost everywhere equal to the limit of a sequence of simple functions with respect to the measure on that subset.
|
Filter.Tendsto.integrableAtFilter_ae
theorem Filter.Tendsto.integrableAtFilter_ae :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E}
{μ : MeasureTheory.Measure α} {l : Filter α} [inst_2 : l.IsMeasurablyGenerated],
StronglyMeasurableAtFilter f l μ →
μ.FiniteAtFilter l → ∀ {b : E}, Filter.Tendsto f (l ⊓ μ.ae) (nhds b) → MeasureTheory.IntegrableAtFilter f l μ
This theorem states that for a function `f` from a measurable space `α` to a normed additive commutative group `E` and a given measure `μ` on `α`, if the function is strongly measurable at a filter `l` with respect to the measure `μ`, and the measure `μ` is finite at the filter `l`, then for any element `b` of `E`, if the function `f` tends to `b` at the intersection of `l` and the set of almost everywhere defined points of `μ` (denoted by `l ⊓ μ.ae`), then `f` is integrable at the filter `l`. In other words, under these conditions, we can integrate the function `f` over the sets in the filter `l`.
More concisely: If a strongly measurable function from a measurable space to a normed additive commutative group tends to a limit at the intersection of a filter and the set of almost everywhere defined points with respect to a finite measure, then the function is integrable with respect to that measure at the filter.
|
MeasureTheory.IntegrableAtFilter.filter_mono
theorem MeasureTheory.IntegrableAtFilter.filter_mono :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E}
{μ : MeasureTheory.Measure α} {l l' : Filter α},
l ≤ l' → MeasureTheory.IntegrableAtFilter f l' μ → MeasureTheory.IntegrableAtFilter f l μ
The theorem `MeasureTheory.IntegrableAtFilter.filter_mono` states that for any types `α` and `E`, where `α` has a measurable space structure and `E` has a normed add commutative group structure, and given a function `f` from `α` to `E`, a measure `μ` on `α`, and two filters `l` and `l'` on `α`, if `l` is less than or equal to `l'` and the function `f` is integrable at filter `l'`, then `f` is also integrable at filter `l`.
In other words, if the function is integrable at a certain level of 'coarseness' given by the filter `l'`, it is also integrable at finer levels of 'coarseness' given by any filter `l` that is a subset of `l'`.
More concisely: If `μ` is a measure on a measurable space `(α, Σ)`, `E` is a normed add commutative group, `f: α → E` is integrable at filter `l'`, and `l` is a filter on `α` with `l ≤ l'`, then `f` is integrable at filter `l`.
|
MeasureTheory.integrableOn_univ
theorem MeasureTheory.integrableOn_univ :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E}
{μ : MeasureTheory.Measure α}, MeasureTheory.IntegrableOn f Set.univ μ ↔ MeasureTheory.Integrable f μ
The theorem `MeasureTheory.integrableOn_univ` states that for any measure space `α`, any normed additive commutative group `E`, any function `f` from `α` to `E`, and any measure `μ` on `α`, the function `f` is integrable across the entire set of `α` (represented as `Set.univ`) with respect to the measure `μ` if and only if `f` is integrable with respect to `μ`. In simpler terms, a function is integrable over the whole space if and only if it is integrable when considered on any subset of the space. This is in line with the definition of integrability that requires the function to be almost everywhere strongly measurable and that the integral of its pointwise norm over the considered set is finite.
More concisely: For any measure space, normed additive commutative group, function, and measure, a function is integrable with respect to the measure over the entire space if and only if it is integrable on every subset of the space.
|
Mathlib.MeasureTheory.Integral.IntegrableOn._auxLemma.2
theorem Mathlib.MeasureTheory.Integral.IntegrableOn._auxLemma.2 :
∀ {α : Type u_1} {β : Type u_2} [inst : NormedAddCommGroup β] {x : MeasurableSpace α} {f : α → β},
MeasureTheory.Integrable f 0 = True
This theorem states that for any types `α` and `β`, where `β` is a normed additive commutative group, any measurable function `f` from `α` to `β` is integrable with respect to the zero measure. In mathematical terms, the theorem says that $\int_{0}^{} |f(a)| da$ is finite for every function `f` from `α` to `β`, where `α` is any type and `β` is a normed additive commutative group.
More concisely: Every measurable function from a type `α` to a normed additive commutative group `β` has finite integral of absolute value.
|
MeasureTheory.IntegrableAtFilter.add
theorem MeasureTheory.IntegrableAtFilter.add :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E]
{μ : MeasureTheory.Measure α} {l : Filter α} {f g : α → E},
MeasureTheory.IntegrableAtFilter f l μ →
MeasureTheory.IntegrableAtFilter g l μ → MeasureTheory.IntegrableAtFilter (f + g) l μ
The theorem `MeasureTheory.IntegrableAtFilter.add` states that for any measure space `α`, any normed add commutative group `E`, any measure `μ` on `α`, any filter `l` on `α`, and any two functions `f` and `g` from `α` to `E`, if `f` is integrable at filter `l` with respect to measure `μ` and `g` is also integrable at filter `l` with respect to measure `μ`, then the function `f + g` (which represents the pointwise addition of `f` and `g`) is also integrable at filter `l` with respect to measure `μ`. In other words, the integrability property at a filter is preserved under the addition of two integrable functions.
More concisely: If `f` and `g` are integrable functions with respect to measure `μ` at filter `l` on measure space `α`, then their pointwise sum `f + g` is also integrable with respect to `μ` at `l`.
|
ContinuousOn.aemeasurable
theorem ContinuousOn.aemeasurable :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β]
[inst_5 : BorelSpace β] {f : α → β} {s : Set α} {μ : MeasureTheory.Measure α},
ContinuousOn f s → MeasurableSet s → AEMeasurable f (μ.restrict s)
The theorem states that if a function `f` is continuous on a set `s`, then `f` is almost everywhere measurable with respect to the measure `μ` restricted to `s`. Here, being "almost everywhere measurable" means that `f` is equal almost everywhere to a measurable function. This applies to functions `f` from a measurable space `α` to a Borel space `β`, where `α` is also a topological space and `β` is also a measurable space. The set `s` must be a measurable set within the measurable space `α`.
More concisely: If `f: α → β` is a continuous function on the measurable set `s ⊆ α` in the measurable space `α`, then `f` is almost everywhere equal to a measurable function on `s`.
|
MeasureTheory.IntegrableOn.restrict
theorem MeasureTheory.IntegrableOn.restrict :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s t : Set α}
{μ : MeasureTheory.Measure α},
MeasureTheory.IntegrableOn f s μ → MeasurableSet s → MeasureTheory.IntegrableOn f s (μ.restrict t)
This theorem states that for any two sets `s` and `t` of elements of type `α`, a function `f : α → E` that maps elements from `α` to a normed add commutative group `E`, and a measure `μ` defined on `α`, if `f` is almost everywhere strongly measurable on `s` and the integral of its pointwise norm over `s` is less than infinity (i.e., `f` is "integrable on `s` with respect to `μ`"), and if `s` is a measurable set, then `f` is also integrable on `s` with respect to the measure `μ` restricted to `t`. In other words, if a function is integrable on a measurable set, it remains integrable even when the underlying measure is restricted to another set.
More concisely: If `s` and `t` are sets of elements of type `α`, `f : α → E` is a strongly measurable function from `s` to a normed add commutative group `E`, `μ` is a measure on `α`, and `s` is measurable with `∫₡(‖f‖) ds < ∞`, then `f` is integrable on `s` with respect to `μ` restricted to `t`.
|
integrableOn_Icc_iff_integrableOn_Ioc
theorem integrableOn_Icc_iff_integrableOn_Ioc :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] [inst_2 : PartialOrder α]
[inst_3 : MeasurableSingletonClass α] {f : α → E} {μ : MeasureTheory.Measure α} {a b : α}
[inst_4 : MeasureTheory.NoAtoms μ],
MeasureTheory.IntegrableOn f (Set.Icc a b) μ ↔ MeasureTheory.IntegrableOn f (Set.Ioc a b) μ
The theorem `integrableOn_Icc_iff_integrableOn_Ioc` states that for any measurable space `α`, normed add commutative group `E`, partial order on `α`, measure `μ` on `α` that has no atoms, and function `f` from `α` to `E`, the function `f` is integrable on the closed interval from `a` to `b` (i.e., `Set.Icc a b`) with respect to the measure `μ` if and only if `f` is integrable on the open-closed interval from `a` to `b` (i.e., `Set.Ioc a b`) with respect to the same measure `μ`. In other words, the integrability of the function on the closed interval is equivalent to its integrability on the open-closed interval under the given conditions.
More concisely: For any measurable space, normed add commutative group, and measurable function with no atoms, the function is integrable over a closed interval if and only if it is integrable over the corresponding open-closed interval with respect to the given measure.
|
MeasureTheory.IntegrableOn.integrable_indicator
theorem MeasureTheory.IntegrableOn.integrable_indicator :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s : Set α}
{μ : MeasureTheory.Measure α},
MeasureTheory.IntegrableOn f s μ → MeasurableSet s → MeasureTheory.Integrable (s.indicator f) μ
The theorem `MeasureTheory.IntegrableOn.integrable_indicator` states that for any set `s` of elements of type `α`, and any function `f` mapping elements of `α` to the normed add-commutative group `E`, if `f` is integrable on `s` with respect to a measure `μ` and `s` is a measurable set, then the indicator function of `s` with respect to `f` is integrable with respect to `μ`. In more mathematical terms, if the integral of `f` over set `s` is finite and `s` is measurable, then the integral of the function which equals `f` on `s` and zero otherwise, is also finite.
More concisely: If a function `f` is integrable over a measurable set `s` with finite integral, then the indicator function of `s` with respect to `f` is also integrable with finite integral.
|
MeasureTheory.IntegrableOn.integrable
theorem MeasureTheory.IntegrableOn.integrable :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s : Set α}
{μ : MeasureTheory.Measure α}, MeasureTheory.IntegrableOn f s μ → MeasureTheory.Integrable f (μ.restrict s)
The theorem `MeasureTheory.IntegrableOn.integrable` states that given any measurable space `α`, a normed additive commutative group `E`, a function `f` from `α` to `E`, a set `s` of type `α`, and a measure `μ` on `α`, if the function `f` is integrable on the set `s` with respect to measure `μ`, then `f` is also integrable with respect to the restriction of measure `μ` to set `s`. In mathematical terms, the integrability of a function on a set implies its integrability on the measure restricted to that set.
More concisely: If a function is integrable with respect to a measure on a set, then it is integrable with respect to the restriction of that measure to the set.
|
MeasureTheory.IntegrableOn.mono
theorem MeasureTheory.IntegrableOn.mono :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s t : Set α}
{μ ν : MeasureTheory.Measure α},
MeasureTheory.IntegrableOn f t ν → s ⊆ t → μ ≤ ν → MeasureTheory.IntegrableOn f s μ
The theorem `MeasureTheory.IntegrableOn.mono` states that for any types `α` and `E`, with `α` having a `MeasurableSpace` instance and `E` having a `NormedAddCommGroup` instance, and given a function `f` from `α` to `E` and sets `s` and `t` of type `α`, if the function `f` is integrable over the set `t` with respect to measure `ν`, then if `s` is a subset of `t` and measure `μ` is less than or equal to `ν`, it follows that `f` is also integrable over the set `s` with respect to measure `μ`. In other words, this theorem states the monotonicity of the integrability of a function over a set with respect to a measure.
More concisely: If `f` is a integrable function from a measurable space `(α, Σ, ν)` to a normed additive group `(E, +, ∥⋅∥)`, and `s ⊆ t` are sets in `α` with `μ(s) ≤ ν(t)`, then `f` is integrable over `s` with respect to measure `μ`.
|
MeasureTheory.IntegrableOn.restrict_toMeasurable
theorem MeasureTheory.IntegrableOn.restrict_toMeasurable :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s : Set α}
{μ : MeasureTheory.Measure α},
MeasureTheory.IntegrableOn f s μ →
(∀ x ∈ s, f x ≠ 0) → μ.restrict (MeasureTheory.toMeasurable μ s) = μ.restrict s
This theorem states that for any type `α` and `E`, where `E` is a normed add commutative group and `α` is a measurable space, given a function `f` from `α` to `E`, a set `s` of type `α`, and a measure `μ` over `α`, if the function `f` is integrable over the set `s` and nonzero at every point in `s`, then the restriction of the measure `μ` to the measurable hull of `s` (denoted by `MeasureTheory.toMeasurable μ s`) is the same as its restriction to the set `s`. In other words, the behavior of the measure `μ` is consistent when it is restricted to the set `s` and when it is restricted to the measurable hull of `s` under the provided conditions.
More concisely: If `f` is a measurable, integrable, and nonzero function from a measurable space `α` to a normed add commutative group `E`, and `s` is a measurable set with `μ(s)` finite, then `MeasureTheory.toMeasurable μ s = μ s`.
|
MeasureTheory.IntegrableAtFilter.of_inf_ae
theorem MeasureTheory.IntegrableAtFilter.of_inf_ae :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E}
{μ : MeasureTheory.Measure α} {l : Filter α},
MeasureTheory.IntegrableAtFilter f (l ⊓ μ.ae) μ → MeasureTheory.IntegrableAtFilter f l μ
The theorem `MeasureTheory.IntegrableAtFilter.of_inf_ae` states that for any measure space `α`, any normed additive commutative group `E`, any function `f` from `α` to `E`, any measure `μ` on `α`, and any filter `l` on `α`, if `f` is integrable at the infimum filter of `l` and the almost everywhere filter of `μ`, then `f` is also integrable at filter `l`.
In simpler terms, this theorem means that if a function is integrable almost everywhere with respect to a certain set-defined filter, then it is also integrable with respect to the original filter.
More concisely: If a function is integrable with respect to both the infimum filter and almost everywhere filter of a measure on a measure space, then it is integrable with respect to the given filter.
|
MeasureTheory.integrable_indicator_iff
theorem MeasureTheory.integrable_indicator_iff :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s : Set α}
{μ : MeasureTheory.Measure α},
MeasurableSet s → (MeasureTheory.Integrable (s.indicator f) μ ↔ MeasureTheory.IntegrableOn f s μ)
The theorem `MeasureTheory.integrable_indicator_iff` asserts that for any given measurable space `α`, normed add commutative group `E`, function `f : α → E`, set `s : Set α`, and measure `μ : MeasureTheory.Measure α`, if `s` is a measurable set, then `f` is integrable with respect to the indicator function of `s` under measure `μ` if and only if `f` is integrable over the set `s` under measure `μ`. In other words, the integrability of `f` according to the indicator function of set `s` is equivalent to the integrability of `f` on the set `s`.
More concisely: For any measurable space, normed add commutative group, measurable function, measurable set, and measure, the function is integrable with respect to the indicator function of the set if and only if it is integrable over the set.
|
MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter
theorem MeasureTheory.Measure.FiniteAtFilter.integrableAtFilter :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E}
{μ : MeasureTheory.Measure α} {l : Filter α} [inst_2 : l.IsMeasurablyGenerated],
StronglyMeasurableAtFilter f l μ →
μ.FiniteAtFilter l →
Filter.IsBoundedUnder (fun x x_1 => x ≤ x_1) l (norm ∘ f) → MeasureTheory.IntegrableAtFilter f l μ
The theorem states that if a measure `μ` is finite at a filter `l` and there is a function `f` with the property that its norm is bounded above on sets from `l`, then `f` is said to be integrable at `l`. Specifically, we require that `f` is strongly measurable at filter `l` with respect to measure `μ`, `μ` is finite at filter `l` and the norm of `f` is eventually bounded by some uniform bound on `l`. If these conditions are met, then there exists a set in `l` on which `f` is integrable with respect to measure `μ`.
More concisely: If a strongly measurable function `f` with respect to a finite measure `μ` on a filter `l` has a bounded norm on sets from `l`, then there exists a set in `l` on which `f` is integrable with respect to `μ`.
|
MeasureTheory.IntegrableOn.of_ae_diff_eq_zero
theorem MeasureTheory.IntegrableOn.of_ae_diff_eq_zero :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s t : Set α}
{μ : MeasureTheory.Measure α},
MeasureTheory.IntegrableOn f s μ →
MeasureTheory.NullMeasurableSet t μ → (∀ᵐ (x : α) ∂μ, x ∈ t \ s → f x = 0) → MeasureTheory.IntegrableOn f t μ
This theorem states that if a function is integrable on a set `s` and it vanishes on the set difference `t \ s`, then it's also integrable on `t` provided `t` is a null-measurable set. Here, a function is called 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. A set is said to be null-measurable if it can be approximated by a measurable set up to a set of null measure. The condition of the function vanishing on `t \ s` means that for almost all elements `x` in `t \ s`, `f(x)` equals zero. The symbol `∀ᵐ (x : α) ∂μ` denotes "for almost all `x` with respect to the measure `μ`".
More concisely: If a function integrable on a null-measurable set is zero almost everywhere on their difference with another set, then it is integrable on that second set.
|
MeasureTheory.integrableOn_empty
theorem MeasureTheory.integrableOn_empty :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E}
{μ : MeasureTheory.Measure α}, MeasureTheory.IntegrableOn f ∅ μ
The theorem `MeasureTheory.integrableOn_empty` asserts that, given any measurable space `α`, a normed additive commutative group `E`, a function `f` from `α` to `E`, and a measure `μ` on `α`, the function `f` is integrable over the empty set with respect to the measure `μ`. In other words, for any function and any measure, the function is always integrable on the empty set, which is a consequence of the fact that the integral over an empty set is always well-defined and finite.
More concisely: The empty set is integrable with respect to any measure for any integrable function.
|
MeasureTheory.integrableOn_const
theorem MeasureTheory.integrableOn_const :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {s : Set α}
{μ : MeasureTheory.Measure α} {C : E}, MeasureTheory.IntegrableOn (fun x => C) s μ ↔ C = 0 ∨ ↑↑μ s < ⊤
The theorem `MeasureTheory.integrableOn_const` states that for any set `s` of type `α`, any measure `μ` on `α`, and any constant `C` of type `E`, the constant function that returns `C` for every input is integrable on the set `s` with respect to the measure `μ` if and only if `C` is zero or the measure of the set `s` is finite. This is a statement about the conditions under which the integral of a constant function over a set is defined and finite. In the context of measure theory, this theorem is a fundamental result connecting the concepts of integrability, constant functions, and finiteness of measures.
More concisely: A constant function is integrable with respect to a measure on a set if and only if the constant is zero or the measure of the set is finite.
|
ContinuousOn.aestronglyMeasurable
theorem ContinuousOn.aestronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
[inst_2 : TopologicalSpace β] [h : SecondCountableTopologyEither α β] [inst_3 : OpensMeasurableSpace α]
[inst_4 : TopologicalSpace.PseudoMetrizableSpace β] {f : α → β} {s : Set α} {μ : MeasureTheory.Measure α},
ContinuousOn f s → MeasurableSet s → MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
The theorem states that for any function `f` from a type `α` to a type `β`, if `f` is continuous on a set `s` and `s` is a measurable set, then `f` is almost everywhere strongly measurable with respect to the measure `μ` restricted to set `s`. This holds provided that either the source type `α` or the target type `β` has a second-countable topology, the source type `α` has a topological space structure which is measurable, and the target type `β` is a pseudo-metrizable space. "Almost everywhere strongly measurable" means that the function is almost everywhere equal to the limit of a sequence of simple functions.
More concisely: If `f` is a continuous function from a measurable set `s` of a second-countable, measurable topological space `α` to a pseudo-metrizable space `β`, then `f` is almost everywhere equal to the limit of a sequence of simple functions on `s` with respect to the measure `μ`.
|
MeasureTheory.integrableOn_singleton_iff
theorem MeasureTheory.integrableOn_singleton_iff :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E}
{μ : MeasureTheory.Measure α} {x : α} [inst_2 : MeasurableSingletonClass α],
MeasureTheory.IntegrableOn f {x} μ ↔ f x = 0 ∨ ↑↑μ {x} < ⊤
This theorem, `MeasureTheory.integrableOn_singleton_iff`, states that for any measure space `α`, any normed additive commutative group `E`, any function `α → E`, any measure `μ` on `α`, and any element `x` of `α`, the property that the function is integrable over the singleton set `{x}` (in the sense of the measure `μ`) is equivalent to one of two conditions: either the function evaluates to `0` at `x`, or the measure of the singleton set `{x}` is less than infinity. This is true under the assumption that `α` is a measurable singleton class, meaning that every singleton subset of `α` is measurable.
More concisely: For any measurable singleton class α, normed additive commutative group E, function ƒ: α → E, measure μ on α, and x ∈ α, the function ƒ is integrable over the singleton {x} with respect to μ if and only if μ({x}) < ∞ or ƒ(x) = 0.
|
MeasureTheory.IntegrableOn.integrable_of_ae_not_mem_eq_zero
theorem MeasureTheory.IntegrableOn.integrable_of_ae_not_mem_eq_zero :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s : Set α}
{μ : MeasureTheory.Measure α},
MeasureTheory.IntegrableOn f s μ → (∀ᵐ (x : α) ∂μ, x ∉ s → f x = 0) → MeasureTheory.Integrable f μ
This theorem states that for any function `f` from a type `α` to a type `E` (where `α` is equipped with measurable space structure and `E` is a normed additive commutative group), and any set `s` of type `α`, if `f` is integrable on `s` and for almost every `x` in `α`, `f(x) = 0` whenever `x` is not in `s`, then `f` is integrable over the whole space `α`. Essentially, this theorem tells us that a function that is integrable on a set and vanishes almost everywhere outside of that set, is integrable on the whole space.
More concisely: If a function from a measurable space to a normed additive commutative group is integrable over a set and vanishes almost everywhere outside of it, then the function is integrable over the entire measurable space.
|
MeasureTheory.IntegrableOn.mono_set
theorem MeasureTheory.IntegrableOn.mono_set :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s t : Set α}
{μ : MeasureTheory.Measure α}, MeasureTheory.IntegrableOn f t μ → s ⊆ t → MeasureTheory.IntegrableOn f s μ
The theorem `MeasureTheory.IntegrableOn.mono_set` states that for any two sets `s` and `t` of a certain type `α`, given that we have a measurable space over `α` and a normed additive commutative group over another type `E`, if a function `f` from `α` to `E` is integrable on the set `t` with respect to a measure `μ`, and the set `s` is a subset of `t`, then the function `f` is also integrable on the set `s` with respect to the same measure `μ`. In other words, if a function is integrable over a larger set, it is also integrable over any of its subsets.
More concisely: If `f` is integrable over the set `t` with respect to measure `μ` and `s` is a subset of `t`, then `f` is integrable over the set `s` with respect to `μ`.
|
MeasureTheory.Integrable.indicator
theorem MeasureTheory.Integrable.indicator :
∀ {α : Type u_1} {E : Type u_3} [inst : MeasurableSpace α] [inst_1 : NormedAddCommGroup E] {f : α → E} {s : Set α}
{μ : MeasureTheory.Measure α},
MeasureTheory.Integrable f μ → MeasurableSet s → MeasureTheory.Integrable (s.indicator f) μ
The theorem `MeasureTheory.Integrable.indicator` states that for any type `α` equipped with a measurable space structure, any normed additively commutative group `E`, any function `f` from `α` to `E`, any set `s` of type `α`, and any measure `μ` on `α`, if `f` is integrable with respect to measure `μ` and `s` is a measurable set, then the function that is equal to `f` on set `s` and equals zero elsewhere, (also known as the indicator function of `s` with respect to `f`), is also integrable with respect to measure `μ`.
More concisely: If `f:` `α` -> `E` is integrable, `s` is a measurable set of `α`, and `μ` is a measure on `α`, then the indicator function `1[_]` of `s` with respect to `f` (i.e., `1[_] = f on s` and `1[_] = 0` elsewhere) is integrable with respect to `μ`.
|