ContinuousOn.integrableOn_Icc
theorem ContinuousOn.integrableOn_Icc :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} [inst_3 : OpensMeasurableSpace X]
{a b : X} [inst_4 : MeasureTheory.IsFiniteMeasureOnCompacts μ] [inst_5 : Preorder X] [inst_6 : CompactIccSpace X]
[inst_7 : T2Space X], ContinuousOn f (Set.Icc a b) → MeasureTheory.IntegrableOn f (Set.Icc a b) μ
The theorem `ContinuousOn.integrableOn_Icc` states that for any type `X` that is a measurable space, a topological space, a T2 space, and has a preorder, and any type `E` that is a normed communal addition group, given a function `f` from `X` to `E`, a measure `μ` on `X` that is finite on compacts, and two elements `a` and `b` of `X` such that the interval from `a` to `b` is compact, if `f` is continuous on the closed interval from `a` to `b`, then `f` is integrable on that interval with respect to the measure `μ`. In other words, if the function is continuous on a specific, compact interval, then it is also integrable over that same interval.
More concisely: If a continuous function on a compact interval of a measurable space with a preorder and a finite measure on compacts, valued in a normed additive group, then the function is integrable on that interval.
|
MeasureTheory.LocallyIntegrable.integrable_smul_right_of_hasCompactSupport
theorem MeasureTheory.LocallyIntegrable.integrable_smul_right_of_hasCompactSupport :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {μ : MeasureTheory.Measure X} [inst_3 : NormedSpace ℝ E]
[inst_4 : OpensMeasurableSpace X] [inst_5 : T2Space X] {f : X → ℝ},
MeasureTheory.LocallyIntegrable f μ →
∀ {g : X → E}, Continuous g → HasCompactSupport g → MeasureTheory.Integrable (fun x => f x • g x) μ
The theorem states that if we have a function `f` that is locally integrable and another function `g` that is continuous with compact support, then the product of `f` and `g` (denoted as `f • g`) is integrable. Here, being locally integrable means that `f` is integrable over a neighborhood of every point. Being continuous with compact support means `g` is continuous and it equals zero outside a compact set. And being integrable means that the function is measurable, and that its integral (with respect to the measure `μ`) over the entire domain of the function is finite.
More concisely: If `f` is locally integrable and `g` is continuous with compact support, then the product `f • g` is integrable.
|
MeasureTheory.LocallyIntegrableOn.integrableOn_isCompact
theorem MeasureTheory.LocallyIntegrableOn.integrableOn_isCompact :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} {s : Set X},
MeasureTheory.LocallyIntegrableOn f s μ → IsCompact s → MeasureTheory.IntegrableOn f s μ
This theorem states that if a function is locally integrable on a compact set, then it is also integrable on that set. Specifically, for any types `X` and `E` with `X` being both a measurable and topological space and `E` being a normed additive commutative group, for any function `f` from `X` to `E`, any measure `μ` of `X`, and any set `s` of `X`, if the function `f` is locally integrable on the set `s` with respect to the measure `μ`, and if the set `s` is compact, then the function `f` is integrable on the set `s` with respect to the measure `μ`.
More concisely: If a locally integrable function on a compact set is measurable, then it is integrable.
|
ContinuousOn.integrableOn_compact
theorem ContinuousOn.integrableOn_compact :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} [inst_3 : OpensMeasurableSpace X]
{K : Set X} [inst_4 : MeasureTheory.IsFiniteMeasureOnCompacts μ] [inst_5 : T2Space X],
IsCompact K → ContinuousOn f K → MeasureTheory.IntegrableOn f K μ
This theorem states that for any set `K` of a certain type `X` and a function `f` from `X` to `E` (where `E` is a type with a normed add commutative group structure), if `K` is compact and `f` is continuous on `K`, then `f` is integrable on `K` with respect to measure `μ`. This is under several conditions: `X` has both a measurable space and a topological space structure, `E` is a normed add commutative group, the measure `μ` is finite on compact sets, and `X` satisfies the T2 separation axiom (also known as being a Hausdorff space).
More concisely: If `K` is a compact subset of a measurable and Hausdorff space `X` with a topology inducing the given one, and `f` is a continuous function from `X` to a normed add commutative group `E` with finite μ-measure of compact sets, then `f` is integrable with respect to measure `μ` on `K`.
|
MeasureTheory.LocallyIntegrable.integrableOn_isCompact
theorem MeasureTheory.LocallyIntegrable.integrableOn_isCompact :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} {k : Set X},
MeasureTheory.LocallyIntegrable f μ → IsCompact k → MeasureTheory.IntegrableOn f k μ
The theorem `MeasureTheory.LocallyIntegrable.integrableOn_isCompact` states that, given a measurable space `X`, a topological space `X`, and a normed add-commutative group `E`, for any function `f` mapping from `X` to `E`, any measure `μ` on `X`, and any set `k` of `X`, if the function `f` is locally integrable and the set `k` is compact, then the function `f` is integrable on the set `k` with respect to the measure `μ`. In other words, if a function is integrable near every point, then it is integrable over any compact set within the space.
More concisely: If a locally integrable function on a compact set of a measurable space with respect to a measure is defined, then it is integrable.
|
MeasureTheory.locallyIntegrableOn_of_locallyIntegrable_restrict
theorem MeasureTheory.locallyIntegrableOn_of_locallyIntegrable_restrict :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} {s : Set X}
[inst_3 : OpensMeasurableSpace X],
MeasureTheory.LocallyIntegrable f (μ.restrict s) → MeasureTheory.LocallyIntegrableOn f s μ
The theorem `MeasureTheory.locallyIntegrableOn_of_locallyIntegrable_restrict` states that if a function `f` from `X` to `E` is locally integrable with respect to the measure `μ` restricted to a set `s`, then `f` is also locally integrable on `s`. Here, `X` is a measurable space and also a topological space, `E` is a normed add commutative group, and `s` is a set of elements in `X`. This theorem equates local integrability in the restricted measure space to local integrability on the set where the measure is restricted. An equivalent condition is provided when `s` is a closed set, as stated in `locallyIntegrableOn_iff_locallyIntegrable_restrict`.
More concisely: If a function is locally integrable with respect to a measure's restriction to a set, then the function is locally integrable on that set.
|
MeasureTheory.locallyIntegrableOn_iff
theorem MeasureTheory.locallyIntegrableOn_iff :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} {s : Set X}
[inst_3 : LocallyCompactSpace X] [inst_4 : T2Space X],
IsClosed s ∨ IsOpen s →
(MeasureTheory.LocallyIntegrableOn f s μ ↔ ∀ k ⊆ s, IsCompact k → MeasureTheory.IntegrableOn f k μ)
The theorem `MeasureTheory.locallyIntegrableOn_iff` states that for a given set `s` in a space `X` that is either open or closed, and a function `f` from `X` to `E`, `f` is locally integrable on `s` if and only if `f` is integrable on every compact subset contained in `s`. The conditions need `X` to be a measurable and locally compact space with a Hausdorff property (T2 space), `E` to be a normed additive commutative group, and `μ` to be a measure on `X`.
More concisely: A function `f` from a measurable and locally compact T2 space `X` with a Hausdorff measure `μ` to a normed additive commutative group `E` is locally integrable on a set `s` if and only if it is integrable on every compact subset contained in `s`.
|
Continuous.integrable_of_hasCompactSupport
theorem Continuous.integrable_of_hasCompactSupport :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} [inst_3 : OpensMeasurableSpace X]
[inst_4 : MeasureTheory.IsFiniteMeasureOnCompacts μ],
Continuous f → HasCompactSupport f → MeasureTheory.Integrable f μ
The theorem states that if we have a continuous function `f` from a measurable and topological space `X` to a normed additive commutative group `E`, and if this function `f` has compact support, then `f` is integrable with respect to a measure `μ` on `X`. Here integrability means that `f` is measurable and the integral `∫⁻ a, ‖f a‖ ∂μ` is finite. Also, the measure `μ` is assumed to be finite on compacts and the topological space `X` is assumed to be open and measurable. Compact support of `f` means that the closure of the support of `f` is compact or equivalently `f` is equal to `0` outside a compact set.
More concisely: If `f` is a continuous function from a measurable and open, topological space `X` with finite measure on compacts, having compact support, then `f` is integrable with respect to a finite measure `μ` on `X`.
|
MeasureTheory.locallyIntegrableOn_iff_locallyIntegrable_restrict
theorem MeasureTheory.locallyIntegrableOn_iff_locallyIntegrable_restrict :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} {s : Set X}
[inst_3 : OpensMeasurableSpace X],
IsClosed s → (MeasureTheory.LocallyIntegrableOn f s μ ↔ MeasureTheory.LocallyIntegrable f (μ.restrict s))
This theorem states that for any closed set `s`, a function `f` from `X` to `E` is locally integrable on `s` with respect to a measure `μ` if and only if it is locally integrable with respect to the measure `μ` restricted to `s`. Here, `X` is a measurable space and a topological space, `E` is a normed add commutative group, and `s` is a set in `X`. The theorem also assumes that the topology on `X` makes all open sets measurable. In other words, being locally integrable on a closed set is equivalent to being locally integrable with respect to the restricted measure on that set.
More concisely: For any closed set `s` in the measurable and topological space `X`, a function `f` from `X` to the normed add commutative group `E` is locally integrable on `s` with respect to the measure `μ` if and only if it is locally integrable with respect to the restriction of `μ` to `s`.
|
Continuous.locallyIntegrable
theorem Continuous.locallyIntegrable :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} [inst_3 : OpensMeasurableSpace X]
[inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_5 : SecondCountableTopologyEither X E],
Continuous f → MeasureTheory.LocallyIntegrable f μ
The theorem states that for any function `f` mapping from a type `X` to a type `E`, where `X` is equipped with a measurable space structure, a topological space structure, and the second countable topology, and `E` is a normed additive commutative group, if `f` is continuous and the measure `μ` is a locally finite measure, then `f` is locally integrable with respect to the measure `μ`. Here, a function is said to be locally integrable if it is integrable on a neighborhood of every point in `X`.
More concisely: For any continuous function `f` from a second countable, measurable space `(X, Σ, μ)` with a locally finite measure `μ` to a normed additive commutative group `E`, `f` is locally integrable with respect to `μ`.
|
MeasureTheory.LocallyIntegrableOn.exists_nat_integrableOn
theorem MeasureTheory.LocallyIntegrableOn.exists_nat_integrableOn :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} {s : Set X}
[inst_3 : SecondCountableTopology X],
MeasureTheory.LocallyIntegrableOn f s μ →
∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ s ⊆ ⋃ n, u n ∧ ∀ (n : ℕ), MeasureTheory.IntegrableOn f (u n ∩ s) μ
The theorem `MeasureTheory.LocallyIntegrableOn.exists_nat_integrableOn` states that: given a function `f` that is locally integrable on a set `s` within a second countable topological space, then there exists a sequence of open sets `u n` that covers `s` and for each `n`, `f` is integrable on the intersection of set `u n` and `s`. In mathematical terms, if $f$ is locally integrable on set $s$, there exists a sequence of open sets $(u_n)$ such that $s$ is a subset of the union of the $u_n$, and for each $n$, $f$ is integrable on $u_n \cap s$.
More concisely: Given a locally integrable function $f$ on the second countable topological space $X$ and a cover $(u\_n)$ of $X$ by open sets, there exists a sequence of integers $(n\_i)$ such that the function $f$ is integrable on $u\_ {n\_i} \cap X$.
|
MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport
theorem MeasureTheory.LocallyIntegrable.integrable_smul_left_of_hasCompactSupport :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} [inst_3 : NormedSpace ℝ E]
[inst_4 : OpensMeasurableSpace X] [inst_5 : T2Space X],
MeasureTheory.LocallyIntegrable f μ →
∀ {g : X → ℝ}, Continuous g → HasCompactSupport g → MeasureTheory.Integrable (fun x => g x • f x) μ
The theorem states that if we have a function `f` that is locally integrable - meaning that it is integrable on a neighborhood of every point - and another function `g` that is continuous and has compact support - indicating that `g` equals zero outside a compact set - then the function formed by multiplying `g` and `f` element-wise is integrable. This holds for any topological space `X` equipped with a measure `μ`, and a normed add commutative group `E` of functions from `X` to the reals under normal addition. The theorem guarantees the integrability of the product of these specific types of functions.
More concisely: If `f` is a locally integrable function and `g` is a continuous function with compact support, then their element-wise product is integrable.
|
MeasureTheory.LocallyIntegrable.exists_nat_integrableOn
theorem MeasureTheory.LocallyIntegrable.exists_nat_integrableOn :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} [inst_3 : SecondCountableTopology X],
MeasureTheory.LocallyIntegrable f μ →
∃ u, (∀ (n : ℕ), IsOpen (u n)) ∧ ⋃ n, u n = Set.univ ∧ ∀ (n : ℕ), MeasureTheory.IntegrableOn f (u n) μ
The theorem states that if a function is locally integrable in a second countable topological space, then there exists a sequence of open sets which covers the entire space and on each of these open sets, the function is integrable. Here, a function is considered to be locally integrable if it is integrable on a neighborhood around every point. A topological space is second countable if it has a countable base for its topology. An open set is a subset of the topological space, where any point in the set has a neighborhood completely contained in the set. The 'univ' set is the universal set that contains all elements of the given type. And a function is integrable on a set if it is almost everywhere strongly measurable on that set and the integral of its pointwise norm over the set is less than infinity.
More concisely: In a second countable topological space, every locally integrable function admits a countable open cover where the function is integrable on each open set.
|
ContinuousOn.integrableOn_compact'
theorem ContinuousOn.integrableOn_compact' :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} [inst_3 : OpensMeasurableSpace X]
{K : Set X} [inst_4 : MeasureTheory.IsFiniteMeasureOnCompacts μ],
IsCompact K → MeasurableSet K → ContinuousOn f K → MeasureTheory.IntegrableOn f K μ
The theorem states that for any given types `X` and `E`, where `X` is a measurable and topological space and `E` is a normed additive commutative group, for a function `f` from `X` to `E`, a measure `μ` on `X` that is finite on compacts, and a compact set `K` of `X` that is measurable, if `f` is continuous on `K`, then `f` is also integrable on `K` with respect to the measure `μ`. In simpler terms, it says that a continuous function on a compact set is always integrable over this set with respect to any locally finite measure.
More concisely: If `X` is a measurable and topological space, `E` is a normed additive commutative group, `f` is a continuous function from a compact and measurable subset `K` of `X` to `E`, and `μ` is a finite measure on `X`, then `f` is integrable on `K` with respect to `μ`.
|
MeasureTheory.IntegrableOn.continuousOn_mul
theorem MeasureTheory.IntegrableOn.continuousOn_mul :
∀ {X : Type u_1} {R : Type u_5} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
{μ : MeasureTheory.Measure X} [inst_2 : OpensMeasurableSpace X] {K : Set X} [inst_3 : NormedRing R]
[inst_4 : SecondCountableTopologyEither X R] {g g' : X → R} [inst_5 : T2Space X],
ContinuousOn g K →
MeasureTheory.IntegrableOn g' K μ → IsCompact K → MeasureTheory.IntegrableOn (fun x => g x * g' x) K μ
The theorem `MeasureTheory.IntegrableOn.continuousOn_mul` states that for any measurable space `X` which also has a topological space structure (`inst_1`), a measure `μ` on `X`, a set `K` of `X` which is compact, and a normed ring `R`, if a function `g` from `X` to `R` is continuous on `K` and another function `g'` from `X` to `R` is integrable on `K` (almost everywhere strongly measurable on `K` and the integral of its pointwise norm over `K` is less than infinity), then the function that maps `x` in `X` to the product of `g(x)` and `g'(x)` is also integrable on `K`. The additional conditions `inst_2 : OpensMeasurableSpace X` and `inst_3 : NormedRing R` are technical conditions needed to make the definitions of integrability and continuity work correctly in this context.
In simple terms, if one function is continuous and another is integrable on a compact set, then their pointwise product is also integrable on that set.
More concisely: If a function is continuous on a compact set and another function is integrable on that set in a measurable space with a topological structure and a normed ring of scalars, then their pointwise product is integrable on that set.
|
MeasureTheory.LocallyIntegrable.integrableOn_nhds_isCompact
theorem MeasureTheory.LocallyIntegrable.integrableOn_nhds_isCompact :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X},
MeasureTheory.LocallyIntegrable f μ →
∀ {k : Set X}, IsCompact k → ∃ u, IsOpen u ∧ k ⊆ u ∧ MeasureTheory.IntegrableOn f u μ
The theorem `MeasureTheory.LocallyIntegrable.integrableOn_nhds_isCompact` states that if a function `f` from `X` to `E` is locally integrable with respect to a measure `μ`, then for any compact set `k` in `X`, there exists an open set `u` that contains `k`, such that `f` is integrable on `u`. Here, `X` is a measurable space and a topological space, `E` is a normed add commutative group, and `μ` is a measure on `X`. The concept of local integrability in this context means that `f` is integrable over the neighborhood of every point in `X`. A compact set `k` is one for which, for any nontrivial filter on `X` that contains `k`, there is a point in `k` that is a cluster point of the filter. A set `u` is open in the context of the ambient topological space on `X`. Finally, `f` is integrable on a set if it is almost everywhere strongly measurable on that set and the integral of its norm over that set is less than infinity.
More concisely: Given a locally integrable function `f` from a measurable and topological space `(X, Σ, μ)` to a normed add commutative group `E` and a compact set `k ∈ X`, there exists an open set `u ∈ X` containing `k` such that `f` is integrable on `u`.
|
MeasureTheory.LocallyIntegrableOn.exists_countable_integrableOn
theorem MeasureTheory.LocallyIntegrableOn.exists_countable_integrableOn :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} {s : Set X}
[inst_3 : SecondCountableTopology X],
MeasureTheory.LocallyIntegrableOn f s μ →
∃ T, T.Countable ∧ (∀ u ∈ T, IsOpen u) ∧ s ⊆ ⋃ u ∈ T, u ∧ ∀ u ∈ T, MeasureTheory.IntegrableOn f (u ∩ s) μ
The theorem `MeasureTheory.LocallyIntegrableOn.exists_countable_integrableOn` states that for any measurable space `X` and any topological space `X` that is also a second-countable space, given a function `f` from `X` to a normed additive commutative group `E`, a measure `μ` on `X` and a set `s` in `X`, if the function `f` is locally integrable on the set `s` with respect to the measure `μ`, then there exists a countable collection `T` of open sets in `X` such that:
1. Every set `u` in the collection `T` is open.
2. The set `s` is a subset of the union of all sets `u` in the collection `T`.
3. For every set `u` in the collection `T`, the function `f` is integrable on the intersection of `u` and `s` with respect to the measure `μ`.
In simpler terms, if a function is locally integrable on a set in a second countable topological space, we can find countably many open sets covering the original set, and the function will be integrable on each piece of the original set that intersects with those open sets.
More concisely: Given a measurable space `(X, Σ, μ)`, a second-countable topological space `X`, and a locally integrable function `f` on `(X, Σ, μ)` over a normed additive commutative group `E` on a subset `s` of `X`, there exists a countable collection `T` of open sets in `X` such that `s` is a subset of their union and `f` is integrable on each `u ∈ T` and `u ∩ s`.
|
ContinuousOn.locallyIntegrableOn
theorem ContinuousOn.locallyIntegrableOn :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X} [inst_3 : OpensMeasurableSpace X]
{K : Set X} [inst_4 : MeasureTheory.IsLocallyFiniteMeasure μ] [inst_5 : SecondCountableTopologyEither X E],
ContinuousOn f K → MeasurableSet K → MeasureTheory.LocallyIntegrableOn f K μ
The theorem `ContinuousOn.locallyIntegrableOn` states that, given a set `K` of elements of type `X`, a function `f` from `X` to a normed additive commutative group `E`, and a measure `μ` on the measurable space `X`, if `f` is continuous on `K` and `K` is a measurable set, then the function `f` is locally integrable on the set `K` with respect to the measure `μ`. This result holds in the context where the space `X` has both a topological structure and a measurable space structure, `E` is a normed additive commutative group, the measure `μ` is locally finite, and the topological structure of either `X` or `E` is second-countable.
More concisely: If a continuous function on a measurable set in a second-countable topological and measurable space X with a locally finite measure μ maps to a normed additive commutative group E, then the function is locally integrable on X with respect to μ.
|
MeasureTheory.LocallyIntegrable.locallyIntegrableOn
theorem MeasureTheory.LocallyIntegrable.locallyIntegrableOn :
∀ {X : Type u_1} {E : Type u_3} [inst : MeasurableSpace X] [inst_1 : TopologicalSpace X]
[inst_2 : NormedAddCommGroup E] {f : X → E} {μ : MeasureTheory.Measure X},
MeasureTheory.LocallyIntegrable f μ → ∀ (s : Set X), MeasureTheory.LocallyIntegrableOn f s μ
This theorem states that if a function `f` from a type `X` to a type `E` is locally integrable with respect to a measure `μ`, then the function `f` is also locally integrable on any subset `s` of `X` with respect to the same measure `μ`. Here, `X` is a measurable space and a topological space, and `E` is a normed additive commutative group. Local integrability of a function means that it is integrable within any neighborhood of every point in its domain.
More concisely: If a function `f` from a measurable space and topological space `X` to a normed additive commutative group `E` is locally integrable with respect to measure `μ`, then `f` is locally integrable on any subset of `X` with respect to `μ`.
|