MeasureTheory.StronglyMeasurable.mono
theorem MeasureTheory.StronglyMeasurable.mono :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m m' : MeasurableSpace α} [inst : TopologicalSpace β],
MeasureTheory.StronglyMeasurable f → m' ≤ m → MeasureTheory.StronglyMeasurable f
The theorem `MeasureTheory.StronglyMeasurable.mono` states that for any two types `α` and `β`, given a function `f` from `α` to `β`, and two `MeasurableSpace` instances `m` and `m'` on `α`, if `f` is strongly measurable (in the sense that `f` is the limit of simple functions) and `m'` is a subspace of `m`, then `f` is also strongly measurable with respect to `m'`. Here, the topological space structure is on `β` and the measurability of `f` is with respect to the measurable spaces on `α`. The ≤ symbol represents the subspace relation between two measurable spaces.
More concisely: If `f` is a strongly measurable function from a measurable space `(α, m)` to another measurable space `(β, βTOP)`, and `(α, m')` is a subspace of `(α, m)`, then `f` is strongly measurable with respect to `(α, m')`.
|
HasCompactSupport.stronglyMeasurable_of_prod
theorem HasCompactSupport.stronglyMeasurable_of_prod :
∀ {α : Type u_1} {X : Type u_5} {Y : Type u_6} [inst : Zero α] [inst_1 : TopologicalSpace X]
[inst_2 : TopologicalSpace Y] [inst_3 : MeasurableSpace X] [inst_4 : MeasurableSpace Y]
[inst_5 : OpensMeasurableSpace X] [inst_6 : OpensMeasurableSpace Y] [inst_7 : TopologicalSpace α]
[inst_8 : TopologicalSpace.PseudoMetrizableSpace α] {f : X × Y → α},
Continuous f → HasCompactSupport f → MeasureTheory.StronglyMeasurable f
The theorem `HasCompactSupport.stronglyMeasurable_of_prod` states that for any continuous function `f` with compact support on a product space of types `X` and `Y`, it is strongly measurable with respect to the product sigma-algebra. Here, strong measurability means that the function `f` can be approximated by a sequence of simple functions. This is particularly noteworthy in the case where the spaces `X` and `Y` are not separable, meaning that the product of the Borel sigma algebras might not contain all open sets, yet it still contains enough open sets to approximate compactly supported continuous functions.
More concisely: A continuous function with compact support on the product of two spaces is strongly measurable with respect to the product sigma-algebra.
|
MeasureTheory.stronglyMeasurable_const
theorem MeasureTheory.stronglyMeasurable_const :
∀ {α : Type u_5} {β : Type u_6} {x : MeasurableSpace α} [inst : TopologicalSpace β] {b : β},
MeasureTheory.StronglyMeasurable fun x => b
The theorem `MeasureTheory.stronglyMeasurable_const` states that for any type `α` equipped with a measurable space structure `x`, any type `β` equipped with a topological space structure, and any element `b` of type `β`, the constant function that maps each element of type `α` to `b` is strongly measurable. Here, a function is considered strongly measurable if it is the limit of a sequence of simple functions.
More concisely: For any measurable spaces (α, x) and (β, τ), and any topological space (β), the constant function from α to β, sending all elements to a fixed element b, is strongly measurable.
|
MeasureTheory.FinStronglyMeasurable.measurable
theorem MeasureTheory.FinStronglyMeasurable.measurable :
∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [inst : Zero β]
[inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : MeasurableSpace β]
[inst_4 : BorelSpace β], MeasureTheory.FinStronglyMeasurable f μ → Measurable f
This theorem states that a finitely strongly measurable function is also a measurable function. In detail, given types `α` and `β`, a measure space `m0` on `α`, measure `μ` on `α`, and a function `f` from `α` to `β`, if `β` has a zero element, `β` is a topological space and pseudo metrizable space, and `β` is also a measurable space with a Borel sigma algebra, then if function `f` is finitely strongly measurable with respect to measure `μ`, it is also a measurable function.
To clarify, a function is finitely strongly measurable with respect to a measure if it is the limit of simple functions whose support has finite measure. A function is measurable if the preimage of every measurable set under the function is also measurable.
More concisely: If `α` is a measure space with measure `μ`, `β` is a measurable space with a Borel sigma algebra and has a zero element, and `f: α -> β` is finitely strongly measurable with respect to `μ`, then `f` is measurable.
|
MeasureTheory.AEStronglyMeasurable.mono_measure
theorem MeasureTheory.AEStronglyMeasurable.mono_measure :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} {ν : MeasureTheory.Measure α},
MeasureTheory.AEStronglyMeasurable f μ → ν ≤ μ → MeasureTheory.AEStronglyMeasurable f ν
This theorem states that for any types `α` and `β`, a measurable space `m` on `α`, a measure `μ` on `α`, a topological space structure on `β`, a function `f` from `α` to `β`, and another measure `ν` on `α`, if the function `f` is almost everywhere strongly measurable with respect to the measure `μ`, and the measure `ν` is less than or equal to the measure `μ`, then the function `f` is also almost everywhere strongly measurable with respect to the measure `ν`. In other words, the property of a function being almost everywhere strongly measurable under a measure is preserved when we replace the measure with another that is smaller or equal.
More concisely: If `α`, `β`, `m` a measurable space on `α`, `μ` a measure on `α`, `ν` another measure on `α` with `ν ≤ μ`, `f` a strongly measurable function from `α` to `β` with respect to `μ`, then `f` is also strongly measurable with respect to `ν`.
|
Measurable.add_stronglyMeasurable
theorem Measurable.add_stronglyMeasurable :
∀ {α : Type u_5} {E : Type u_6} {x : MeasurableSpace α} [inst : AddGroup E] [inst_1 : TopologicalSpace E]
[inst_2 : MeasurableSpace E] [inst_3 : BorelSpace E] [inst_4 : ContinuousAdd E]
[inst_5 : TopologicalSpace.PseudoMetrizableSpace E] {g f : α → E},
Measurable g → MeasureTheory.StronglyMeasurable f → Measurable (g + f)
The theorem `Measurable.add_stronglyMeasurable` states that in a normed vector space, the sum of a measurable function and a strongly measurable function is always measurable. This holds for any measurable space and any addition group that also has the structure of a topological space, a measurable space, and a Borel space. The addition operation must be continuous, and the topological space must be pseudo-metrizable. Please note that without further assumptions regarding second-countability, this statement does not generally hold true for the sum of two measurable functions.
More concisely: In a normed vector space with the structure of a topological space, a measurable space, and a Borel space, the sum of a measurable function and a strongly measurable function is measurable, provided the addition operation is continuous and the topological space is pseudo-metrizable.
|
aestronglyMeasurable_indicator_iff
theorem aestronglyMeasurable_indicator_iff :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} [inst_1 : Zero β] {s : Set α},
MeasurableSet s →
(MeasureTheory.AEStronglyMeasurable (s.indicator f) μ ↔ MeasureTheory.AEStronglyMeasurable f (μ.restrict s))
The theorem `aestronglyMeasurable_indicator_iff` states that for any type `α`, `β`, a measurable space `m` on `α`, a measure `μ` on `α`, a topological space structure on `β`, a zero element in `β`, and a set `s` of `α`, given that `s` is measurable, a function `f` from `α` to `β` is almost everywhere strongly measurable with respect to `μ` when applied to the indicator function of `s` if and only if `f` is almost everywhere strongly measurable with respect to the restriction of the measure `μ` to the set `s`. Here, an "indicator function" is a function that takes the value `f a` if `a` belongs to `s`, and `0` otherwise. "Almost everywhere strongly measurable" means that the function is almost everywhere equal to the limit of a sequence of simple functions.
More concisely: For any measurable space `(α, m)`, measure `μ` on `α`, topological space `(β, τ)`, zero element `0_β` in `β`, measurable set `s ε α`, and measurable function `f : α → β`, `f` is almost everywhere equal to the indicator function of `s` with respect to `μ` if and only if `f` is almost everywhere equal to the restriction of `f` to `s` with respect to the restriction of `μ` to `s`.
|
aestronglyMeasurable_iff_aemeasurable
theorem aestronglyMeasurable_iff_aemeasurable :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} [inst_1 : MeasurableSpace β] [inst_2 : TopologicalSpace.PseudoMetrizableSpace β]
[inst_3 : BorelSpace β] [inst_4 : SecondCountableTopology β],
MeasureTheory.AEStronglyMeasurable f μ ↔ AEMeasurable f μ
The theorem `aestronglyMeasurable_iff_aemeasurable` states that for a function `f` from a measurable space `α` to a topological space `β` with a measure `μ`, the function is "Almost Everywhere Strongly Measurable" if and only if it is "Almost Everywhere Measurable". This equivalence holds when the topological space `β` has properties such as being pseudometrizable (having a metric that induces the topology), being a Borel space (the σ-algebra is the Borel σ-algebra), and having a second countable topology (having a countable basis). In simple terms, the function is almost everywhere equivalent to the limit of a sequence of simple functions if and only if it coincides almost everywhere with a measurable function under these specific conditions.
More concisely: A measurable function from a measurable space to a topological space with a measure is almost everywhere strongly measurable if and only if it is almost everywhere equal to a measurable function, under the conditions that the topological space is pseudometrizable, a Borel space, and has a second countable topology.
|
MeasureTheory.AEStronglyMeasurable.ennnorm
theorem MeasureTheory.AEStronglyMeasurable.ennnorm :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5}
[inst : SeminormedAddCommGroup β] {f : α → β},
MeasureTheory.AEStronglyMeasurable f μ → AEMeasurable (fun a => ↑‖f a‖₊) μ
This theorem states that for all types `α` and `β`, where `α` has a `MeasurableSpace` structure, `β` has a `SeminormedAddCommGroup` structure, and `μ` is a `MeasureTheory.Measure` on `α`, if a function `f` from `α` to `β` is "almost everywhere strongly measurable" with respect to measure `μ`, then the function that maps each element `a` of `α` to the nonnegative extended real norm of `f(a)` is "almost everywhere measurable" with respect to the same measure `μ`. In mathematical terms, it states that if a function is almost everywhere strongly measurable, then its norm is also almost everywhere measurable.
More concisely: If a function from a measurable space to a seminormed additive commutative group is almost everywhere strongly measurable with respect to a measure, then the function mapping each element to the nonnegative extended real norm of its image is almost everywhere measurable with respect to the same measure.
|
MeasureTheory.finStronglyMeasurable_of_measurable
theorem MeasureTheory.finStronglyMeasurable_of_measurable :
∀ {α : Type u_1} {G : Type u_5} [inst : SeminormedAddCommGroup G] [inst_1 : MeasurableSpace G]
[inst_2 : BorelSpace G] [inst_3 : SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.SigmaFinite μ],
Measurable f → MeasureTheory.FinStronglyMeasurable f μ
This theorem states that in a space with a second-countable topology and a sigma-finite measure, any measurable function is also finitely strongly measurable. Here, a function is considered measurable if the preimage of every measurable set is measurable. On the other hand, a function is said to be finitely strongly measurable with respect to a measure if it is the limit of simple functions whose supports have finite measure. The said spaces are seminormed add commutative groups with a Borel measurable space structure. The measure is defined over a measurable space.
More concisely: In a second-countable topological space with a sigma-finite measure, every measurable function is also finitely strongly measurable.
|
Measurable.stronglyMeasurable_add
theorem Measurable.stronglyMeasurable_add :
∀ {α : Type u_5} {E : Type u_6} {x : MeasurableSpace α} [inst : AddGroup E] [inst_1 : TopologicalSpace E]
[inst_2 : MeasurableSpace E] [inst_3 : BorelSpace E] [inst_4 : ContinuousAdd E]
[inst_5 : TopologicalSpace.PseudoMetrizableSpace E] {g f : α → E},
Measurable g → MeasureTheory.StronglyMeasurable f → Measurable (f + g)
The theorem states that in a normed vector space, if we have a function `g` which is measurable and another function `f` which is strongly measurable, then the addition of these two functions is also measurable. It's important to note that without further assumptions of second-countability, this property does not hold for the addition of two measurable functions. In other words, the measurability of the sum of two functions does not necessarily follow from the measurability of the individual functions without additional conditions.
More concisely: In a normed vector space, if `g` is measurable and `f` is strongly measurable, then their sum `f + g` is measurable. (Without second-countability, this may not hold for the sum of two measurable functions.)
|
MeasureTheory.AEStronglyMeasurable.comp_measurable
theorem MeasureTheory.AEStronglyMeasurable.comp_measurable :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {g : α → β} {γ : Type u_5} {x : MeasurableSpace γ}
{x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ},
MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) →
Measurable f → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
The theorem `MeasureTheory.AEStronglyMeasurable.comp_measurable` states that for any two types `α` and `β` with `β` being a topological space, and any function `g : α → β`, along with another type `γ` and measurable spaces `x` and `x_1` associated to `γ` and `α` respectively, and a function `f : γ → α`, and a measure `μ` on `γ`, if `g` is `AEStronglyMeasurable` with respect to the measure `μ` pushed forward by `f`, and if `f` is a measurable function, then the composition function `g ∘ f` is also `AEStronglyMeasurable` with respect to the measure `μ`.
In simpler terms, if a function `g` is almost everywhere equal to the limit of a sequence of simple functions with respect to a measure `μ` transformed by another function `f`, and if `f` is a function such that the preimage of every measurable set is measurable, then the combination of these two functions (i.e., `g ∘ f`) is also almost everywhere equal to the limit of a sequence of simple functions with respect to the original measure `μ`.
More concisely: If `g : α → β` is `AEStronglyMeasurable` with respect to the measure `μ` pushed forward by a measurable function `f : γ → α`, then the composition `g ∘ f` is `AEStronglyMeasurable` with respect to the measure `μ` on `γ`.
|
MeasureTheory.aestronglyMeasurable_const
theorem MeasureTheory.aestronglyMeasurable_const :
∀ {α : Type u_5} {β : Type u_6} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{b : β}, MeasureTheory.AEStronglyMeasurable (fun x => b) μ
The theorem `MeasureTheory.aestronglyMeasurable_const` states that for any types `α` and `β`, where `α` is equipped with a measurable space structure, `β` is equipped with a topological space structure, and a measure `μ` on `α`, for any constant function `b` from `α` to `β`, the function `(fun x => b)` is `AEStronglyMeasurable` with respect to the measure `μ`. This means that the constant function is almost everywhere equal to the limit of a sequence of simple functions.
More concisely: For any measurable space `(α, Σ)`, topological space `(β, τ)`, measure `μ` on `(α, Σ)`, and constant function `b : α → β`, the function `(fun x => b)` is `AEStronglyMeasurable` with respect to `μ`.
|
MeasureTheory.StronglyMeasurable.aemeasurable
theorem MeasureTheory.StronglyMeasurable.aemeasurable :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : MeasurableSpace α} [inst : TopologicalSpace β]
[inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [inst_3 : BorelSpace β]
{μ : MeasureTheory.Measure α}, MeasureTheory.StronglyMeasurable f → AEMeasurable f μ
The theorem states that a strongly measurable function is also almost everywhere measurable. In other words, if a function is the limit of simple functions (that is, it is strongly measurable), then there exists a measurable function that is equivalent to the original function almost everywhere.
More concisely: A strongly measurable function is almost everywhere equal to a measurable function.
|
MeasureTheory.StronglyMeasurable.isSeparable_range
theorem MeasureTheory.StronglyMeasurable.isSeparable_range :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} [inst : TopologicalSpace β],
MeasureTheory.StronglyMeasurable f → TopologicalSpace.IsSeparable (Set.range f)
The theorem `MeasureTheory.StronglyMeasurable.isSeparable_range` states that for any strongly measurable function `f` mapping from a type `α` (with a measurable space structure `m`) to a type `β` (with a topological space structure), the range of `f` is a separable set in the topological space `β`. In other words, the image of `f` is contained in the closure of a countable subset of `β`. Here, a function `f` is strongly measurable if it can be approximated by a sequence of simple functions.
More concisely: The range of any strongly measurable function from a measurable space to a topological space is separable.
|
AEMeasurable.aestronglyMeasurable
theorem AEMeasurable.aestronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} [inst_1 : MeasurableSpace β] [inst_2 : TopologicalSpace.PseudoMetrizableSpace β]
[inst_3 : OpensMeasurableSpace β] [inst_4 : SecondCountableTopology β],
AEMeasurable f μ → MeasureTheory.AEStronglyMeasurable f μ
The theorem states that in a space with a second countable topology, if a function is almost everywhere measurable with respect to a measure, then the function is also almost everywhere strongly measurable with respect to the same measure. Here, "almost everywhere measurable" means that the function coincides almost everywhere with a measurable function, and "almost everywhere strongly measurable" means that the function is almost everywhere equal to the limit of a sequence of simple functions. This statement applies to functions from a measurable space to a topological space that is pseudometrizable, has an opens measurable space structure, and has a second countable topology.
More concisely: In a second countable, pseudometrizable topological space with an measurable structure, any almost everywhere measurable function is almost everywhere strongly measurable.
|
MeasureTheory.StronglyMeasurable.neg
theorem MeasureTheory.StronglyMeasurable.neg :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Neg β]
[inst_2 : ContinuousNeg β], MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable (-f)
This theorem states that for any types `α` and `β`, if `β` is a topological space with a negation operation that is continuous, and `f` is a function from `α` to `β`, then if `f` is strongly measurable (i.e., it is the limit of simple functions), the function `-f` (obtained by negating the output of `f` for each input) is also strongly measurable. In other words, the strong measurability property is preserved under the operation of negation for functions on topological spaces with a continuous negation operation.
More concisely: If `f` is a strongly measurable function from a topological space `α` to a topological space `β` with a continuous negation operation, then the negation of `f` is also strongly measurable.
|
MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_le
theorem MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_le :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : SeminormedAddCommGroup β] {m m0 : MeasurableSpace α}
(hm : m ≤ m0),
MeasureTheory.StronglyMeasurable f →
∀ (μ : MeasureTheory.Measure α) [inst_1 : MeasureTheory.SigmaFinite (μ.trim hm)],
∃ s, (∀ (n : ℕ), MeasurableSet (s n) ∧ ↑↑μ (s n) < ⊤ ∧ ∀ x ∈ s n, ‖f x‖ ≤ ↑n) ∧ ⋃ i, s i = Set.univ
The theorem `MeasureTheory.StronglyMeasurable.exists_spanning_measurableSet_norm_le` states that given a function `f` which is strongly measurable with respect to a sub-sigma-algebra `m` and a measure that is sigma-finite on `m`, there exists a sequence of measurable sets with finite measure such that `f` has bounded norm on each of these sets. In other words, on each of these sets, the norm of `f` is less than or equal to a certain natural number `n`. Furthermore, the union of all these sets spans the entire universal set, which means that every element of the type is included in one of these sets. In particular, `f` is integrable on each of these sets.
More concisely: Given a strongly measurable function `f` with respect to a sigma-finite measure `m`, there exists a sequence of measurable sets with finite measure, whose union covers the entire universal set, such that the norm of `f` is bounded on each set.
|
Continuous.comp_aestronglyMeasurable
theorem Continuous.comp_aestronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ] {g : β → γ} {f : α → β},
Continuous g → MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => g (f x)) μ
The theorem states that if we have a continuous function `g` from a topological space `β` to another topological space `γ`, and another function `f` from a measurable space `α` to `β` that is `AEStronglyMeasurable` (almost everywhere strongly measurable) with respect to a measure `μ`, then the composition of `g` and `f` (given by `g(f(x))`) is also `AEStronglyMeasurable` with respect to the same measure `μ`. This is to say, almost everywhere, the composition of `g` and `f` matches the limit of a sequence of simple functions.
More concisely: If `g: β -> γ` is continuous and `f: α -> β` is `AEStronglyMeasurable`, then the composition `g ∘ f: α -> γ` is also `AEStronglyMeasurable`.
|
MeasureTheory.aefinStronglyMeasurable_of_aemeasurable
theorem MeasureTheory.aefinStronglyMeasurable_of_aemeasurable :
∀ {α : Type u_1} {G : Type u_5} [inst : SeminormedAddCommGroup G] [inst_1 : MeasurableSpace G]
[inst_2 : BorelSpace G] [inst_3 : SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.SigmaFinite μ],
AEMeasurable f μ → MeasureTheory.AEFinStronglyMeasurable f μ
The theorem `MeasureTheory.aefinStronglyMeasurable_of_aemeasurable` states that in a space with a second countable topology and a sigma-finite measure, any function that is "almost everywhere measurable" (i.e., coincides almost everywhere with a measurable function) is also "almost everywhere finitely strongly measurable". This latter term means that the function is almost everywhere equal to the limit of a sequence of simple functions, each of which has support with finite measure. In more formal terms, for any `α → G` function `f` and any measure `μ` on `α`, if `f` is `AEMeasurable` with respect to `μ`, then `f` is also `AEFinStronglyMeasurable` with respect to `μ`.
More concisely: In a second countable space with a sigma-finite measure, any almost everywhere measurable function is almost everywhere equal to the limit of a sequence of simple functions with finite support measures.
|
Continuous.stronglyMeasurable_of_hasCompactMulSupport
theorem Continuous.stronglyMeasurable_of_hasCompactMulSupport :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β]
[inst_5 : TopologicalSpace.PseudoMetrizableSpace β] [inst_6 : BorelSpace β] [inst_7 : One β] {f : α → β},
Continuous f → HasCompactMulSupport f → MeasureTheory.StronglyMeasurable f
The theorem "Continuous.stronglyMeasurable_of_hasCompactMulSupport" states that if a function `f` mapping between two spaces `α` and `β` is continuous and has compact multiplicative support, then it is strongly measurable. In other words, a continuous function whose multiplicative support's closure is compact can be approximated by a sequence of simple functions. Both `α` and `β` are topological spaces, with `α` also being a measurable space and `β` a pseudometrizable Borel space with a defined multiplicative identity.
More concisely: If a continuous function between a measurable and a pseudometrizable Borel space with a multiplicative identity has compact multiplicative support, then it is strongly measurable.
|
MeasureTheory.FinStronglyMeasurable.tendsto_approx
theorem MeasureTheory.FinStronglyMeasurable.tendsto_approx :
∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [inst : Zero β]
[inst_1 : TopologicalSpace β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (x : α),
Filter.Tendsto (fun n => ↑(hf.approx n) x) Filter.atTop (nhds (f x))
The theorem `MeasureTheory.FinStronglyMeasurable.tendsto_approx` states that for any function `f` from type `α` to `β`, where `β` is a topological space and has a zero, and `f` is `FinStronglyMeasurable` with respect to a measurable space `m0` and a measure `μ`, for any `x` in `α`, the sequence of approximations of `f` at `x` given by `MeasureTheory.FinStronglyMeasurable.approx` tends towards the value of `f` at `x` as `n` goes to infinity. This is to say, for every neighborhood of `f(x)`, there exists some natural number `N` such that for all `n > N`, `MeasureTheory.FinStronglyMeasurable.approx hf n x` is in that neighborhood. The `FinStronglyMeasurable` property means that `f` can be approximated by a sequence of simple functions with finite measure support.
More concisely: For any FinStronglyMeasurable function `f` from `α` to a topological space `β` with a zero, and for all `x` in `α`, the sequence of approximations `MeasureTheory.FinStronglyMeasurable.approx hf n x` converges to `f(x)` as `n` goes to infinity.
|
MeasureTheory.AEStronglyMeasurable.comp_aemeasurable
theorem MeasureTheory.AEStronglyMeasurable.comp_aemeasurable :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {g : α → β} {γ : Type u_5} {x : MeasurableSpace γ}
{x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ},
MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) →
AEMeasurable f μ → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
The theorem `MeasureTheory.AEStronglyMeasurable.comp_aemeasurable` states that for any given types `α`, `β`, and `γ`, topological space `β`, function `g` from `α` to `β`, measurable spaces `x` for `γ` and `x_1` for `α`, function `f` from `γ` to `α`, and a measure `μ` over `γ`, if `g` is almost everywhere strongly measurable with respect to the pushforward of measure `μ` by `f`, and `f` is almost everywhere measurable with respect to the measure `μ`, then the composition of `g` and `f` (i.e., `g ∘ f`) is almost everywhere strongly measurable with respect to the measure `μ`.
In other words, under the described conditions, almost everywhere strong measurability and almost everywhere measurability are preserved under function composition.
More concisely: If functions `f` and `g` are almost everywhere measurable with respect to a measure `μ`, and `g` is almost everywhere strongly measurable with respect to the pushforward of `μ` by `f`, then their composition `g ∘ f` is almost everywhere strongly measurable with respect to `μ`.
|
MeasureTheory.StronglyMeasurable.add
theorem MeasureTheory.StronglyMeasurable.add :
∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Add β]
[inst_2 : ContinuousAdd β],
MeasureTheory.StronglyMeasurable f →
MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f + g)
The theorem `MeasureTheory.StronglyMeasurable.add` states that for any two functions `f` and `g` from a type `α` to a type `β` (where `α` comes equipped with a measurable space structure and `β` has a topological space structure, an addition operation, and this addition operation is continuous), if both `f` and `g` are strongly measurable (meaning that they can be approximated as the limit of simple functions), then their sum function `(f + g)` is also strongly measurable. This theorem is fundamental in the theory of integration, as it allows us to construct integrable functions as limits of simple functions.
More concisely: If `f` and `g` are strongly measurable functions from the measurable space `(α, Σ)` to the topological space `(β, τ)` with a continuous addition operation, then their sum `(f + g)` is also strongly measurable.
|
Measurable.stronglyMeasurable
theorem Measurable.stronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : MeasurableSpace β]
[inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace.PseudoMetrizableSpace β]
[inst_3 : SecondCountableTopology β] [inst_4 : OpensMeasurableSpace β],
Measurable f → MeasureTheory.StronglyMeasurable f
This theorem states that in a space with a second-countable topology, if a function is measurable, then it is also strongly measurable. More specifically, given a function `f` from an arbitrary type `α` to a type `β`, where `β` has a topological space structure, a pseudo-metrizable space structure, a second-countable topology, and an open measurable space, and both `α` and `β` have measurable space structures, if `f` is a measurable function (meaning that the preimage of every measurable set in `β` is a measurable set in `α`), then `f` is also a strongly measurable function (meaning that it is the limit of a sequence of simple functions).
More concisely: In a second-countable, pseudo-metrizable space with a measurable space structure, a measurable function from a measurable space to the space is also strongly measurable.
|
MeasureTheory.StronglyMeasurable.div
theorem MeasureTheory.StronglyMeasurable.div :
∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Div β]
[inst_2 : ContinuousDiv β],
MeasureTheory.StronglyMeasurable f →
MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f / g)
The theorem `MeasureTheory.StronglyMeasurable.div` states that for any two functions `f` and `g` from a measurable space `α` to a topological space `β` that supports division and has continuous division, if both `f` and `g` are strongly measurable (meaning, each of them is the limit of a sequence of simple functions), then the function obtained by dividing `f` by `g` (i.e., `(f / g)`) is also strongly measurable.
More concisely: If `f` and `g` are strongly measurable functions from a measurable space to a topological space supporting and having continuous division, then their quotient `f / g` is also strongly measurable.
|
MeasureTheory.AEStronglyMeasurable.add
theorem MeasureTheory.AEStronglyMeasurable.add :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f g : α → β} [inst_1 : Add β] [inst_2 : ContinuousAdd β],
MeasureTheory.AEStronglyMeasurable f μ →
MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (f + g) μ
The theorem `MeasureTheory.AEStronglyMeasurable.add` states that for any topological addable space `β`, given two functions `f` and `g` from a measurable space `α` to `β` that are almost everywhere strongly measurable with respect to a measure `μ`, the function obtained by pointwise addition of `f` and `g` is also almost everywhere strongly measurable with respect to the same measure `μ`. This holds provided that the addition operation on `β` is continuous. In other words, if `f` and `g` are almost everywhere equal to the limit of a sequence of simple functions, then so is `(f + g)`.
More concisely: If `α` is a measurable space, `β` is a topological additive space with a continuous addition operation, and `f` and `g` are almost everywhere strongly measurable functions from `α` to `β`, then `f + g` is almost everywhere strongly measurable.
|
MeasureTheory.stronglyMeasurable_const'
theorem MeasureTheory.stronglyMeasurable_const' :
∀ {α : Type u_5} {β : Type u_6} {m : MeasurableSpace α} [inst : TopologicalSpace β] {f : α → β},
(∀ (x y : α), f x = f y) → MeasureTheory.StronglyMeasurable f
This theorem, `MeasureTheory.stronglyMeasurable_const'`, asserts that for any types `α` and `β`, where `α` has a `MeasurableSpace` structure and `β` has a `TopologicalSpace` structure, if a function `f : α → β` satisfies that all its outputs are the same (i.e., `f x = f y` for all `x, y` in `α`), then `f` is strongly measurable. Here, a function is defined to be strongly measurable if it is the limit of a sequence of simple functions. This version of the theorem is applicable even if `α` and `β` are empty types.
More concisely: If `α` is a measurable space and `β` is a topological space, and `f : α → β` is a constant function, then `f` is strongly measurable.
|
MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk
theorem MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ),
MeasureTheory.StronglyMeasurable (MeasureTheory.AEStronglyMeasurable.mk f hf)
The theorem `MeasureTheory.AEStronglyMeasurable.stronglyMeasurable_mk` states that for any function `f` from a measure space `α` to a topological space `β`, and for any measure `μ` on `α`, if `f` is almost everywhere strongly measurable with respect to `μ` (meaning that it is almost everywhere equal to the limit of a sequence of simple functions), then the function `MeasureTheory.AEStronglyMeasurable.mk f hf` is strongly measurable. In other words, `MeasureTheory.AEStronglyMeasurable.mk f hf` can also be represented as the limit point of a sequence of simple functions.
More concisely: If a function from a measure space to a topological space is almost everywhere equal to the limit of a sequence of simple functions with respect to a given measure, then it is strongly measurable.
|
MeasureTheory.AEStronglyMeasurable.mul
theorem MeasureTheory.AEStronglyMeasurable.mul :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f g : α → β} [inst_1 : Mul β] [inst_2 : ContinuousMul β],
MeasureTheory.AEStronglyMeasurable f μ →
MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (f * g) μ
This theorem states that for any given types `α` and `β`, where `α` is equipped with a measurable space structure and `β` is equipped with topological space as well as multiplication structures, and `μ` is a measure on `α`, if two functions `f` and `g` from `α` to `β` are almost everywhere strongly measurable with respect to the measure `μ`, then their pointwise product function `(f * g)` is also almost everywhere strongly measurable with respect to the same measure `μ`. Here, almost everywhere strongly measurable means that the function is almost everywhere equal to the limit of a sequence of simple functions. The multiplication on `β` is assumed to be continuous.
More concisely: Given measurable spaces `(α, Σα)` and `(β, Σβ)`, measurable functions `f, g : α → β`, a measure `μ : Σα → ℝ`, and assuming `μ` is a measure on `α`, `β` is a topological space with a continuous multiplication, and `f` and `g` are almost everywhere strongly measurable with respect to `μ`, then their pointwise product `f * g : α → β` is almost everywhere strongly measurable with respect to `μ`.
|
MeasureTheory.AEStronglyMeasurable.smul
theorem MeasureTheory.AEStronglyMeasurable.smul :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{𝕜 : Type u_5} [inst_1 : TopologicalSpace 𝕜] [inst_2 : SMul 𝕜 β] [inst_3 : ContinuousSMul 𝕜 β] {f : α → 𝕜}
{g : α → β},
MeasureTheory.AEStronglyMeasurable f μ →
MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun x => f x • g x) μ
The theorem `MeasureTheory.AEStronglyMeasurable.smul` states that if we have a measure space `m` over a type `α`, a measure `μ` on this space, a topological space `β`, a type `𝕜` that also has a topological space structure, a scalar multiplication operation on `𝕜` and `β`, and this scalar multiplication operation is continuous, then given two functions `f : α → 𝕜` and `g : α → β` that are almost everywhere strongly measurable with respect to measure `μ`, their scalar multiplication (i.e., the function `(fun x => f x • g x) : α → β` which takes an element `x` from `α` and maps it to the scalar multiplication of `f(x)` and `g(x)`) is also almost everywhere strongly measurable with respect to the same measure `μ`.
More concisely: If `m` is a measure space, `μ` is a measure on `α`, `β` is a topological space, `𝕜` is a topological vector space over the real or complex numbers, `f : α → 𝕜` and `g : α → β` are almost everywhere strongly measurable, and scalar multiplication on `𝕜` is continuous, then the scalar multiplication of `f` and `g`, i.e., `(fun x => f x • g x) : α → β`, is also almost everywhere strongly measurable with respect to `μ`.
|
MeasureTheory.stronglyMeasurable_zero
theorem MeasureTheory.stronglyMeasurable_zero :
∀ {α : Type u_5} {β : Type u_6} {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Zero β],
MeasureTheory.StronglyMeasurable 0
The theorem `MeasureTheory.stronglyMeasurable_zero` states that for any measurable space `α` and any topological space `β` that has a zero element, the zero function, which maps every element of `α` to the zero of `β`, is strongly measurable. Recall that a function is strongly measurable if it is the limit of a sequence of simple functions.
More concisely: For any measurable space `α` and topological space `β` with a zero element, the zero function from `α` to `β` is strongly measurable, i.e., it is the limit of a sequence of simple functions.
|
MeasureTheory.StronglyMeasurable.indicator
theorem MeasureTheory.StronglyMeasurable.indicator :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Zero β],
MeasureTheory.StronglyMeasurable f →
∀ {s : Set α}, MeasurableSet s → MeasureTheory.StronglyMeasurable (s.indicator f)
This theorem states that for any type `α` and `β`, and any function `f` from `α` to `β`, given a measurable space structure on `α`, a topological space structure and a zero element on `β`, if the function `f` is strongly measurable (i.e., it is the limit of simple functions), then for any set `s` of type `α` that is a measurable set, the indicator function of `s` with respect to `f` is also strongly measurable. The indicator function `Set.indicator s f` is defined as `f a` when `a` is in `s` and `0` otherwise.
More concisely: If `f` is a strongly measurable function from a measurable space `(α, Σ)` to a topological space `(β, τ)` with a zero element, then for any measurable set `s ∈ Σ`, the indicator function `Set.indicator s f` is also strongly measurable.
|
exists_stronglyMeasurable_limit_of_tendsto_ae
theorem exists_stronglyMeasurable_limit_of_tendsto_ae :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
[inst_1 : TopologicalSpace.PseudoMetrizableSpace β] {f : ℕ → α → β},
(∀ (n : ℕ), MeasureTheory.AEStronglyMeasurable (f n) μ) →
(∀ᵐ (x : α) ∂μ, ∃ l, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds l)) →
∃ f_lim,
MeasureTheory.StronglyMeasurable f_lim ∧
∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) Filter.atTop (nhds (f_lim x))
This theorem states that if we have a sequence of functions that are almost everywhere strongly measurable (meaning that each function in sequence is almost everywhere equal to the limit of a sequence of simple functions) and this sequence of functions converges almost everywhere (that is, for almost every `x`, there exists a limit `l` where the function values at `x` tend to `l`), then there exists an almost everywhere limit function `f_lim` which is strongly measurable (meaning it is the limit of simple functions) and for almost every `x`, the sequence of function values at `x` converges to `f_lim(x)`.
In other words, we can always find a strongly measurable function that is the limit of a sequence of almost everywhere strongly measurable functions, provided that the sequence of functions converges almost everywhere.
More concisely: If a sequence of almost everywhere strongly measurable functions converges almost everywhere, then there exists a unique strongly measurable function that is the almost everywhere limit of the sequence.
|
MeasureTheory.AEStronglyMeasurable.mono'
theorem MeasureTheory.AEStronglyMeasurable.mono' :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ ν : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β},
ν.AbsolutelyContinuous μ → MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable f ν
The theorem `MeasureTheory.AEStronglyMeasurable.mono'` states that for any types `α` and `β`, a measurable space `m` on `α`, two measures `μ` and `ν` on `α`, a topological space structure on `β`, and a function `f` from `α` to `β`, if the measure `ν` is absolutely continuous with respect to the measure `μ` (i.e., if for any set `s` such that `μ(s) = 0`, we have `ν(s) = 0`), and if the function `f` is almost everywhere strongly measurable with respect to the measure `μ` (i.e., it is almost everywhere equal to the limit of a sequence of simple functions with respect to the measure `μ`), then `f` is also almost everywhere strongly measurable with respect to the measure `ν`.
More concisely: If a function between measurable spaces is almost everywhere equal to the limit of simple functions with respect to a measure that is absolutely continuous with respect to another measure, then the function is almost everywhere strongly measurable with respect to the second measure.
|
MeasureTheory.AEStronglyMeasurable.aemeasurable
theorem MeasureTheory.AEStronglyMeasurable.aemeasurable :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5} [inst : MeasurableSpace β]
[inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace.PseudoMetrizableSpace β] [inst_3 : BorelSpace β]
{f : α → β}, MeasureTheory.AEStronglyMeasurable f μ → AEMeasurable f μ
This theorem states that for any measure space `α` with measure `μ`, and for any space `β` that is a measurable, topological, pseudometrizable and Borel space, if a function `f` from `α` to `β` is almost everywhere strongly measurable with respect to `μ`, then `f` is also almost everywhere measurable with respect to `μ`.
In more detail, a function is almost everywhere strongly measurable if on almost all of the domain, it is equal to the limit of a sequence of simple functions. On the other hand, a function is almost everywhere measurable if it coincides almost everywhere with a measurable function. This theorem shows that if the stronger condition of almost everywhere strong measurability is met, then the function is indeed almost everywhere measurable.
More concisely: For any measure space `(α, μ)` and any measurable, topological, pseudometrizable and Borel space `(β, Δ)`, a strongly almost everywhere measurable function `f : α → β` is almost everywhere measurable.
|
Embedding.comp_stronglyMeasurable_iff
theorem Embedding.comp_stronglyMeasurable_iff :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace β]
[inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : TopologicalSpace γ]
[inst_3 : TopologicalSpace.PseudoMetrizableSpace γ] {g : β → γ} {f : α → β},
Embedding g → ((MeasureTheory.StronglyMeasurable fun x => g (f x)) ↔ MeasureTheory.StronglyMeasurable f)
This theorem states that for any types `α`, `β`, and `γ`, given a measurable space `α` and topological spaces `β` and `γ` that are also pseudometrizable, if `g` is a topological embedding from `β` to `γ` and `f` is a function from `α` to `β`, then the function `f` is strongly measurable if and only if the composition of `g` with `f` (denoted as `g ∘ f`) is strongly measurable. Here, a function is considered strongly measurable if it can be approximated by a sequence of simple functions, with the limit of the sequence converging to the function for all points in the domain.
More concisely: Given measurable spaces `α`, topological spaces `β` and `γ` that are pseudometrizable, a topological embedding `g` from `β` to `γ`, and a function `f` from `α` to `β`, the function `f` is strongly measurable if and only if the composition `g ∘ f` is strongly measurable.
|
MeasureTheory.AEStronglyMeasurable.prod_mk
theorem MeasureTheory.AEStronglyMeasurable.prod_mk :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α}
[inst : TopologicalSpace β] [inst_1 : TopologicalSpace γ] {f : α → β} {g : α → γ},
MeasureTheory.AEStronglyMeasurable f μ →
MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.AEStronglyMeasurable (fun x => (f x, g x)) μ
This theorem states that for any two functions `f : α → β` and `g : α → γ` defined on a measure space `(α, m, μ)`, where `α` is a set, `m` is a σ-algebra on `α`, and `μ` is a measure on `m`, if both `f` and `g` are almost everywhere strongly measurable with respect to measure `μ`, then the function that takes `x` in `α` to the pair `(f x, g x)` in `β × γ` is also almost everywhere strongly measurable with respect to `μ`. In other words, the property of being almost everywhere strongly measurable is preserved under forming the product of two functions. Here, a function is said to be almost everywhere strongly measurable if it is almost everywhere equal to the limit of a sequence of simple functions.
More concisely: If `f : α → β` and `g : α → γ` are almost everywhere strongly measurable functions on the measure space `(α, m, μ)`, then the function `x ↦ (f x, g x)` from `α` to `β × γ` is also almost everywhere strongly measurable.
|
MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on
theorem MeasureTheory.StronglyMeasurable.stronglyMeasurable_of_measurableSpace_le_on :
∀ {α : Type u_5} {E : Type u_6} {m m₂ : MeasurableSpace α} [inst : TopologicalSpace E] [inst_1 : Zero E] {s : Set α}
{f : α → E},
MeasurableSet s →
(∀ (t : Set α), MeasurableSet (s ∩ t) → MeasurableSet (s ∩ t)) →
MeasureTheory.StronglyMeasurable f → (∀ x ∉ s, f x = 0) → MeasureTheory.StronglyMeasurable f
This theorem states that for any types `α` and `E`, and any two measurable spaces `m` and `m₂` over `α`, along with a given topological space over `E` and a zero element of `E`, if we have a set `s` of `α` and a function `f` from `α` to `E`. If the set `s` is measurable in `m`, and for any set `t` of `α`, the intersection of `s` and `t` is measurable both in `m` and `m₂`, and if the function `f` is `m`-strongly-measurable (i.e., it is the limit of simple functions) and equals zero for all elements not in `s`, then the function `f` is also `m₂`-strongly-measurable.
In other words, if a function is strongly-measurable in one σ-algebra and supported on a set that is measurable in both σ-algebras, then it is also strongly-measurable in the second σ-algebra.
More concisely: If a strongly-measurable function equal to zero outside a measurable set is intersect-measurable with another measurable set, then it is also strongly-measurable with respect to the second measurable structure.
|
MeasureTheory.StronglyMeasurable.tendsto_approx
theorem MeasureTheory.StronglyMeasurable.tendsto_approx :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : TopologicalSpace β] {x : MeasurableSpace α}
(hf : MeasureTheory.StronglyMeasurable f) (x_1 : α),
Filter.Tendsto (fun n => ↑(hf.approx n) x_1) Filter.atTop (nhds (f x_1))
The theorem `MeasureTheory.StronglyMeasurable.tendsto_approx` states that for all types `α` and `β`, and a function `f` from `α` to `β`, if the function is strongly measurable (i.e., it can be approximated by a sequence of simple functions), then for every point `x_1` of type `α`, the sequence of approximations at `x_1` tends to `f(x_1)` as `n` tends to infinity. Here, 'tends to' is defined in the sense of filter: for every neighborhood of `f(x_1)`, there exists some `n` such that for all `m ≥ n`, the `m`-th approximation at `x_1` is inside that neighborhood.
More concisely: For any type `α` and `β`, and strongly measurable function `f : α → β`, for every `x_1 : α`, the sequence of approximations of `f` at `x_1` converges to `f(x_1)` in the sense of filters.
|
Continuous.stronglyMeasurable
theorem Continuous.stronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : TopologicalSpace β]
[inst_4 : TopologicalSpace.PseudoMetrizableSpace β] [h : SecondCountableTopologyEither α β] {f : α → β},
Continuous f → MeasureTheory.StronglyMeasurable f
The theorem states that a continuous function is strongly measurable if either the source space or the target space is second-countable. Here, a function is considered strongly measurable if it is the limit of simple functions. A space is said to be second-countable if it has a countable basis for its topology. A function is continuous if the preimage of every open set in the target space is open in the source space.
More concisely: A continuous function between second-countable topological spaces is strongly measurable.
|
MeasureTheory.stronglyMeasurable_one
theorem MeasureTheory.stronglyMeasurable_one :
∀ {α : Type u_5} {β : Type u_6} {x : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : One β],
MeasureTheory.StronglyMeasurable 1
The theorem `MeasureTheory.stronglyMeasurable_one` states that for any measurable space `α`, any topological space `β`, and given that `β` has a defined "one" operation, the constant function `1` is `StronglyMeasurable`. Here, `StronglyMeasurable` means that the function can be obtained as the limit of a sequence of simple functions.
More concisely: For any measurable space `α` and topological space `β` with a defined "one" operation, the constant function `1` from `α` to `β` is StronglyMeasurable.
|
MeasureTheory.AEStronglyMeasurable.congr
theorem MeasureTheory.AEStronglyMeasurable.congr :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f g : α → β},
MeasureTheory.AEStronglyMeasurable f μ → μ.ae.EventuallyEq f g → MeasureTheory.AEStronglyMeasurable g μ
The theorem `MeasureTheory.AEStronglyMeasurable.congr` states that for any measurable space `α`, measure `μ` on `α`, and a topological space `β`, if a function `f` from `α` to `β` is Almost Everywhere (AE) Strongly Measurable with respect to `μ` and `f` is almost everywhere equal to another function `g` (i.e., `f` and `g` are equal except possibly on a set of measure zero), then `g` is also AE Strongly Measurable with respect to `μ`. In other words, the property of being AE Strongly Measurable is preserved under almost everywhere equality of functions.
More concisely: If `f` is AE Strongly Measurable and almost everywhere equal to `g` on a measurable space `(α, Σ, μ)`, then `g` is also AE Strongly Measurable with respect to `(α, Σ, μ)`.
|
MeasureTheory.aestronglyMeasurable_zero
theorem MeasureTheory.aestronglyMeasurable_zero :
∀ {α : Type u_5} {β : Type u_6} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
[inst_1 : Zero β], MeasureTheory.AEStronglyMeasurable 0 μ
The theorem `MeasureTheory.aestronglyMeasurable_zero` states that for any types `α` and `β`, a measurable space `α`, a measure `μ` on `α`, and a topology on `β`, if `β` has a zero element, then the zero function from `α` to `β` is `AEStronglyMeasurable` with respect to the measure `μ`. In other words, the zero function is almost everywhere equal to the limit of a sequence of simple functions.
More concisely: Given a measurable space `(α, Σ, μ)`, a topology on `β` with a zero element, the constant function `0 : α → β` is AES-measurable with respect to `μ`.
|
MeasureTheory.StronglyMeasurable.sub
theorem MeasureTheory.StronglyMeasurable.sub :
∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Sub β]
[inst_2 : ContinuousSub β],
MeasureTheory.StronglyMeasurable f →
MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f - g)
The theorem `MeasureTheory.StronglyMeasurable.sub` states that for any two functions `f` and `g` from a measurable space `α` to a topological space `β` that supports subtraction and has continuous subtraction, if both `f` and `g` are strongly measurable (i.e., each is a limit of simple functions), then their difference `f - g` is also strongly measurable.
More concisely: If two functions from a measurable space to a topological space with continuous subtraction are strongly measurable, then their difference is also strongly measurable.
|
Measurable.sub_stronglyMeasurable
theorem Measurable.sub_stronglyMeasurable :
∀ {α : Type u_5} {E : Type u_6} {x : MeasurableSpace α} [inst : AddCommGroup E] [inst_1 : TopologicalSpace E]
[inst_2 : MeasurableSpace E] [inst_3 : BorelSpace E] [inst_4 : ContinuousAdd E] [inst_5 : ContinuousNeg E]
[inst_6 : TopologicalSpace.PseudoMetrizableSpace E] {g f : α → E},
Measurable g → MeasureTheory.StronglyMeasurable f → Measurable (g - f)
The theorem `Measurable.sub_stronglyMeasurable` states that in a pseudo-metrizable normed vector space, if we have a measurable function `g` and a strongly measurable function `f` (a function that is the limit of simple functions), then the function resulting from the subtraction of `f` from `g` is also measurable. It's important to note that without additional second-countability assumptions, the subtraction of two measurable functions may not necessarily result in a measurable function.
More concisely: In a pseudo-metrizable normed vector space, if `g` is measurable and `f` is strongly measurable, then their difference `g - f` is measurable.
|
MeasureTheory.StronglyMeasurable.prod_mk
theorem MeasureTheory.StronglyMeasurable.prod_mk :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {m : MeasurableSpace α} [inst : TopologicalSpace β]
[inst_1 : TopologicalSpace γ] {f : α → β} {g : α → γ},
MeasureTheory.StronglyMeasurable f →
MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun x => (f x, g x)
The theorem `MeasureTheory.StronglyMeasurable.prod_mk` states that for any two functions `f` and `g`, where `f` maps a measurable space `α` to a topological space `β` and `g` maps the same measurable space `α` to another topological space `γ`, if both `f` and `g` are strongly measurable (i.e., each is the limit of a sequence of simple functions), then the function that maps `x` in `α` to the ordered pair `(f x, g x)` is also strongly measurable.
More concisely: If `f : α → β` and `g : α → γ` are strongly measurable functions from a measurable space `α` to topological spaces `β` and `γ`, respectively, then the function `x ↦ (f x, g x)` from `α` to `β × γ` is also strongly measurable.
|
MeasureTheory.StronglyMeasurable.of_finite
theorem MeasureTheory.StronglyMeasurable.of_finite :
∀ {α : Type u_1} {β : Type u_2} [inst : Finite α] {x : MeasurableSpace α} [inst : MeasurableSingletonClass α]
[inst : TopologicalSpace β] (f : α → β), MeasureTheory.StronglyMeasurable f
The theorem `MeasureTheory.StronglyMeasurable.of_finite` states that for any function `f` mapping from a finite type `α` to a topological space `β`, `f` is strongly measurable. In particular, this theorem applies when the measurable space over `α` is a measurable singleton class. Here, a function is defined as strongly measurable if it is the limit of simple functions.
More concisely: A function from a finite type to a topological space is strongly measurable.
|
MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk
theorem MeasureTheory.AEFinStronglyMeasurable.finStronglyMeasurable_mk :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} [inst_1 : Zero β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ),
MeasureTheory.FinStronglyMeasurable (MeasureTheory.AEFinStronglyMeasurable.mk f hf) μ
This theorem states that for any function `f` from type `α` to `β`, where `α` is a measurable space, `β` is a topological space with zero, and `μ` is a measure on `α`, if `f` is almost everywhere finitely strongly measurable with respect to `μ` (i.e., it almost everywhere equals to the limit of a sequence of simple functions with finite measure support), then the sequence of simple functions obtained by applying the `MeasureTheory.AEFinStronglyMeasurable.mk` method to `f` is also finitely strongly measurable with respect to `μ`. In other words, this sequence of simple functions converges to `f` and each simple function in the sequence has a finite measure support.
More concisely: If a function `f` from a measurable space `α` to a topological space `β` with zero is almost everywhere finitely strongly measurable with respect to a measure `μ` on `α`, then the sequence of simple functions obtained by applying `MeasureTheory.AEFinStronglyMeasurable.mk` to `f` is also finitely strongly measurable with respect to `μ`.
|
MeasureTheory.StronglyMeasurable.measurableSet_le
theorem MeasureTheory.StronglyMeasurable.measurableSet_le :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Preorder β]
[inst_2 : OrderClosedTopology β] [inst_3 : TopologicalSpace.PseudoMetrizableSpace β] {f g : α → β},
MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasurableSet {a | f a ≤ g a}
This theorem states that for every pair of functions `f` and `g` from an arbitrary type `α` to an ordered type `β` equipped with a topological space, a pre-order structure, an order-closed topology, and a pseudometrizable topological space, if both `f` and `g` are strongly measurable (meaning they are limits of simple functions), then the set of elements `a` in `α` for which `f(a)` is less than or equal to `g(a)` is a measurable set.
More concisely: For functions `f` and `g` from an arbitrary type `α` to an ordered and pseudometrizable topological space `β`, if `f` and `g` are strongly measurable, then the set `{a : α | f a ≤ g a}` is measurable.
|
MeasureTheory.AEStronglyMeasurable.norm
theorem MeasureTheory.AEStronglyMeasurable.norm :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {β : Type u_5}
[inst : SeminormedAddCommGroup β] {f : α → β},
MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (fun x => ‖f x‖) μ
The theorem `MeasureTheory.AEStronglyMeasurable.norm` states that for any type `α` with a measurable space structure `m`, a measure `μ` over that measurable space, a type `β` which is a seminormed add commutative group, and any function `f` from `α` to `β`, if the function `f` is almost everywhere strongly measurable with respect to measure `μ`, then the function that takes `x` in `α` to the norm of `f(x)` in `β` is also almost everywhere strongly measurable with respect to the measure `μ`. In other words, if a function is almost everywhere strongly measurable, then so is its norm function, under the same measure.
More concisely: If `f: α → β` is almost everywhere strongly measurable with respect to measure `μ` on measurable space `(α, m)`, then the function `x ↦ ||f x||β` is also almost everywhere strongly measurable with respect to `μ`.
|
MeasureTheory.FinStronglyMeasurable.stronglyMeasurable
theorem MeasureTheory.FinStronglyMeasurable.stronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [inst : Zero β]
[inst_1 : TopologicalSpace β], MeasureTheory.FinStronglyMeasurable f μ → MeasureTheory.StronglyMeasurable f
This theorem states that if a function is finitely strongly measurable with respect to a given measure, it is also strongly measurable. In more detail, given a measurable space `α`, a measure `μ` on `α`, a function `f` from `α` to a topological space `β` that is equipped with a zero element, if the function `f` satisfies the property of being finitely strongly measurable (i.e., it can be approximated by a sequence of simple functions whose supports have finite measure), then `f` also satisfies the property of being strongly measurable (i.e., it can be approximated by a sequence of simple functions).
More concisely: If a function from a measurable space to a topological space, equipped with a zero element, is finitely strongly measurable with respect to a given measure, then it is strongly measurable.
|
aestronglyMeasurable_of_tendsto_ae
theorem aestronglyMeasurable_of_tendsto_ae :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{ι : Type u_5} [inst_1 : TopologicalSpace.PseudoMetrizableSpace β] (u : Filter ι) [inst_2 : u.NeBot]
[inst_3 : u.IsCountablyGenerated] {f : ι → α → β} {g : α → β},
(∀ (i : ι), MeasureTheory.AEStronglyMeasurable (f i) μ) →
(∀ᵐ (x : α) ∂μ, Filter.Tendsto (fun n => f n x) u (nhds (g x))) → MeasureTheory.AEStronglyMeasurable g μ
This theorem states that if you have a sequence of functions (`f` indexed by `ι`) from some measurable space `α` to a topological space `β`, where each function is almost everywhere strongly measurable with respect to a measure `μ` (meaning that each function is almost everywhere equal to the limit of a sequence of simple functions), and if the limit of this sequence of functions at nearly every point in the measurable space `α` converges (in the sense of filter convergence, i.e. for every neighbourhood of the limit, the preimage under the function is a neighbourhood of the sequence index) to a function `g`, then the function `g` itself is almost everywhere strongly measurable with respect to the measure `μ`.
In formal terms, for almost every `x` in `α`, if the sequence `f n x` tends to `g x` with respect to the filter `u`, then `g` is almost everywhere strongly measurable. The concepts of "almost everywhere" and "tend to" are defined according to measure theory and topology, respectively. The sequence of functions `f` is indexed by elements of the type `ι`, and the theorem assumes that the filter `u` has the properties `u.NeBot` and `u.IsCountablyGenerated`, which ensure that the filter `u` is non-trivial and countably generated, respectively. The topological space `β` is also assumed to be a pseudometrizable space.
More concisely: If `{f : α → β | ∀ ι, f ι is almost everywhere strongly measurable with respect to `μ`, and the sequence `{f ι}` converges almost everywhere to a function `g` with respect to filter `u`, then `g` is almost everywhere strongly measurable with respect to `μ`.
|
MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite
theorem MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} [inst_1 : Zero β] [inst_2 : T2Space β],
MeasureTheory.AEFinStronglyMeasurable f μ →
∃ t, MeasurableSet t ∧ (μ.restrict tᶜ).ae.EventuallyEq f 0 ∧ MeasureTheory.SigmaFinite (μ.restrict t)
The theorem `MeasureTheory.AEFinStronglyMeasurable.exists_set_sigmaFinite` states that for any measurable space `α`, measure `μ` on `α`, topological space `β`, and a function `f` from `α` to `β`, if `f` is almost everywhere finitely strongly measurable with respect to `μ`, then there exists a measurable set `t` such that `f` is almost everywhere equal to zero with respect to the measure restricted to the complement of `t` and the measure restricted to `t` is sigma-finite. Here, a function is said to be almost everywhere finitely strongly measurable if it is almost everywhere equal to the limit of a sequence of simple functions with support of finite measure. Sigma-finite means that the set can be partitioned into a countable collection of measurable sets with finite measure.
More concisely: Given a measurable space `(α, Σ, μ)`, topological space `(β, τ)`, and a function `f : α → β` almost everywhere finitely strongly measurable with respect to `μ`, there exists a measurable set `t ∈ Σ` such that the restriction of `μ` to `t` is sigma-finite and `f` is almost everywhere equal to zero on the complement of `t`.
|
MeasureTheory.aefinStronglyMeasurable_iff_aemeasurable
theorem MeasureTheory.aefinStronglyMeasurable_iff_aemeasurable :
∀ {α : Type u_1} {G : Type u_5} [inst : SeminormedAddCommGroup G] [inst_1 : MeasurableSpace G]
[inst_2 : BorelSpace G] [inst_3 : SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.SigmaFinite μ],
MeasureTheory.AEFinStronglyMeasurable f μ ↔ AEMeasurable f μ
The theorem states that in a space with a second countable topology and a sigma-finite measure, the properties of a function being `AEFinStronglyMeasurable` and `AEMeasurable` are equivalent. That is, a function is almost everywhere strongly measurable with respect to a measure (meaning it is almost everywhere equal to the limit of a sequence of simple functions with support with finite measure) if and only if it is almost everywhere measurable (meaning it coincides almost everywhere with a measurable function). This holds for functions from any type to a seminormed add commutative group with a Borel space structure.
More concisely: In a second countable topological space with a sigma-finite measure, a function is almost everywhere strongly measurable if and only if it is almost everywhere measurable, for functions between any type and a seminormed additive commutative group with a Borel structure.
|
MeasureTheory.StronglyMeasurable.mul
theorem MeasureTheory.StronglyMeasurable.mul :
∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Mul β]
[inst_2 : ContinuousMul β],
MeasureTheory.StronglyMeasurable f →
MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (f * g)
The theorem `MeasureTheory.StronglyMeasurable.mul` states that if we have two functions `f` and `g` from a type `α` to a type `β` (where `α` is a measurable space, `β` is a topological space, and `β` also has a multiplication operation that is continuous), and if both of these functions are strongly measurable (i.e., each can be approximated by a sequence of simple functions), then their product function `f * g` is also strongly measurable. In mathematical terms, this theorem states that the set of strongly measurable functions is closed under multiplication, assuming the multiplication operation is continuous.
More concisely: If `f` and `g` are strongly measurable functions from a measurable space `α` to a topological space `β` with a continuous multiplication operation, then their product `f * g` is also strongly measurable.
|
MeasureTheory.StronglyMeasurable.inv
theorem MeasureTheory.StronglyMeasurable.inv :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] [inst_1 : Inv β]
[inst_2 : ContinuousInv β], MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable f⁻¹
This theorem states that for any function `f` from type `α` to `β`, where `α` is a measurable space and `β` is a topological space with an inversion function that is continuous, if `f` is `StronglyMeasurable` (i.e., it can be represented as the limit of simple functions), then the inverse of `f` (denoted as `f⁻¹`) is also `StronglyMeasurable`. In other words, the property of being `StronglyMeasurable` is preserved under continuous inversion.
More concisely: If `f : α → β` is a Strongly Measurable function between measurable space `α` and topological space `β` with a continuous inversion function, then the inverse `f⁻¹ : β → α` is also Strongly Measurable.
|
MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk
theorem MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} [inst_1 : Zero β] (hf : MeasureTheory.AEFinStronglyMeasurable f μ),
μ.ae.EventuallyEq f (MeasureTheory.AEFinStronglyMeasurable.mk f hf)
The theorem `MeasureTheory.AEFinStronglyMeasurable.ae_eq_mk` states that for any measured space `(α, m)`, measure `μ` on `α`, topological space `β`, a function `f : α → β`, if `f` is almost everywhere (a.e.) finitely strongly measurable with respect to `μ` (denoted as `MeasureTheory.AEFinStronglyMeasurable f μ`), then `f` is almost everywhere equal to the measure-theoretically "reconstructed" version of `f` (denoted as `MeasureTheory.AEFinStronglyMeasurable.mk f hf`).
In other words, under the conditions of the theorem, the original function `f` and its measure-theoretically reconstructed version are equal almost everywhere with respect to measure `μ`.
More concisely: If `(α, m)` is a measured space, `μ` is a measure on `α`, `β` is a topological space, `f : α → β` is a.e. finitely strongly measurable with respect to `μ`, then `f` is almost everywhere equal to its measure-theoretic reconstruction `MeasureTheory.AEFinStronglyMeasurable.mk f hf` with respect to `μ`.
|
MeasureTheory.AEStronglyMeasurable.restrict
theorem MeasureTheory.AEStronglyMeasurable.restrict :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β},
MeasureTheory.AEStronglyMeasurable f μ → ∀ {s : Set α}, MeasureTheory.AEStronglyMeasurable f (μ.restrict s)
The theorem `MeasureTheory.AEStronglyMeasurable.restrict` states that for any types `α` and `β`, any measurable space `m` on `α`, any measure `μ` on `α`, any topological space structure on `β`, any function `f` from `α` to `β`, and any set `s` of `α`, if `f` is almost everywhere strongly measurable with respect to the measure `μ`, then `f` is also almost everywhere strongly measurable with respect to the measure `μ` restricted to the set `s`. In other words, the property of being almost everywhere strongly measurable is preserved under the restriction of the measure to a subset of the domain.
More concisely: If `f` is almost everywhere strongly measurable with respect to measure `μ` on type `α`, then `f` is almost everywhere strongly measurable with respect to the restriction of `μ` to any subset `s` of `α`.
|
MeasureTheory.SimpleFunc.aestronglyMeasurable
theorem MeasureTheory.SimpleFunc.aestronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} {x : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
(f : MeasureTheory.SimpleFunc α β), MeasureTheory.AEStronglyMeasurable (↑f) μ
This theorem states that for all simple functions `f` from a measurable space `α` to a topological space `β`, `f` is "almost everywhere strongly measurable" with respect to any measure `μ` on `α`. Here, a function is said to be "almost everywhere strongly measurable" if it is almost everywhere equal to the limit of a sequence of simple functions.
More concisely: A simple function `f` from a measurable space `α` to a topological space `β` is almost everywhere equal to the limit of a sequence of simple functions with respect to any measure `μ` on `α`.
|
MeasureTheory.StronglyMeasurable.ite
theorem MeasureTheory.StronglyMeasurable.ite :
∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {x : MeasurableSpace α} [inst : TopologicalSpace β] {p : α → Prop}
{x_1 : DecidablePred p},
MeasurableSet {a | p a} →
MeasureTheory.StronglyMeasurable f →
MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable fun x => if p x then f x else g x
This theorem states that, for a given measure space `α`, topological space `β`, two functions `f` and `g` from `α` to `β`, a predicate `p` on `α`, and assuming that the predicate `p` is decidable, if the set of elements in `α` satisfying `p` is measurable, and both `f` and `g` are strongly measurable functions, then the function that maps an element `x` from `α` to `f(x)` if `p(x)` is true, and to `g(x)` otherwise, is also strongly measurable.
In other words, the strong measurability of `f` and `g` and the measurability of the set where `p` is true, ensure the strong measurability of the piecewise function that's defined by `p`, `f`, and `g`.
More concisely: Given a measurable set `A` in a measure space `α`, and strongly measurable functions `f` and `g` from `α` to a topological space `β`, the function `h(x) := if p(x) then f(x) else g(x)` is strongly measurable, where `p` is a decidable predicate on `α`.
|
MeasureTheory.StronglyMeasurable.nnnorm
theorem MeasureTheory.StronglyMeasurable.nnnorm :
∀ {α : Type u_1} {x : MeasurableSpace α} {β : Type u_5} [inst : SeminormedAddCommGroup β] {f : α → β},
MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => ‖f x‖₊
The theorem `MeasureTheory.StronglyMeasurable.nnnorm` states that for any measurable space `α`, seminormed add commutative group `β`, and function `f` from `α` to `β`, if `f` is strongly measurable (i.e., it is the limit of simple functions), then the function that maps each element of `α` to the non-negative norm of `f` applied to that element is also strongly measurable. In simpler terms, taking the non-negative norm of a strongly measurable function results in another strongly measurable function.
More concisely: Given a measurable space `α`, a seminormed add commutative group `β`, and a strongly measurable function `f` from `α` to `β`, the function mapping each `x ∈ α` to the non-negative norm `||f(x)||` is also strongly measurable.
|
MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_eq_fun
theorem MeasureTheory.AEStronglyMeasurable.nullMeasurableSet_eq_fun :
∀ {α : Type u_1} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} {E : Type u_5} [inst : TopologicalSpace E]
[inst_1 : TopologicalSpace.MetrizableSpace E] {f g : α → E},
MeasureTheory.AEStronglyMeasurable f μ →
MeasureTheory.AEStronglyMeasurable g μ → MeasureTheory.NullMeasurableSet {x | f x = g x} μ
This theorem states that for any measure space `α` with a measure `μ`, and any two functions `f` and `g` from `α` to a topological and metrizable space `E`, if both `f` and `g` are almost everywhere strongly measurable with respect to measure `μ`, then the set of points in `α` where `f` equals `g` is a null measurable set with respect to `μ`. In other words, the set of points where `f` and `g` are equal can be approximated by a measurable set up to a set of null measure.
More concisely: If two almost everywhere strongly measurable functions from a measure space to a topological and metrizable space have the same value almost everywhere, then the set of points where they differ is a null measurable set.
|
MeasureTheory.StronglyMeasurable.const_smul
theorem MeasureTheory.StronglyMeasurable.const_smul :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : TopologicalSpace β] {𝕜 : Type u_5}
[inst_1 : SMul 𝕜 β] [inst_2 : ContinuousConstSMul 𝕜 β],
MeasureTheory.StronglyMeasurable f → ∀ (c : 𝕜), MeasureTheory.StronglyMeasurable (c • f)
The theorem `MeasureTheory.StronglyMeasurable.const_smul` states that if a function `f` from a measurable space `α` to a topological space `β` is strongly measurable (meaning there exists a sequence of simple functions that converges to `f`), then for any scalar `c` from a type `𝕜` which supports scalar multiplication with `β` and for which scalar multiplication is continuous, the function `c•f` (scalar multiple of `f`) is also strongly measurable.
More concisely: If a strongly measurable function from a measurable space to a topological space is multiplied by a scalar from a scalar multiplication-supporting, continuosly scalar-multiplicative type, the resulting function is also strongly measurable.
|
Finset.stronglyMeasurable_sum'
theorem Finset.stronglyMeasurable_sum' :
∀ {α : Type u_1} {M : Type u_5} [inst : AddCommMonoid M] [inst_1 : TopologicalSpace M] [inst_2 : ContinuousAdd M]
{m : MeasurableSpace α} {ι : Type u_6} {f : ι → α → M} (s : Finset ι),
(∀ i ∈ s, MeasureTheory.StronglyMeasurable (f i)) → MeasureTheory.StronglyMeasurable (s.sum fun i => f i)
The theorem `Finset.stronglyMeasurable_sum'` states that for any type `α`, any type `M` with additional structures of an additive commutative monoid and a topological space, any measurable space `m` over `α`, any type `ι`, any function `f` from `ι` to `α` to `M`, and any finite set `s` of `ι`, if every function `f i`, where `i` is an element of `s`, is strongly measurable (i.e., it is the limit of simple functions), then the sum of the functions `f i` over all `i` in `s` is also strongly measurable. This is the case under the assumption that the addition operation is continuous in the topology of `M`.
More concisely: If `α`, `M` is an additive commutative monoid and topological space, `m` is a measurable space over `α`, `ι` is a type, `f : ι → α → M` is a function, `s` is a finite set of `ι`, and each `f i` is strongly measurable with respect to `m` and the addition in `M` is continuous, then the sum of `f i` over `s` is also strongly measurable.
|
MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving
theorem MeasureTheory.AEStronglyMeasurable.comp_quasiMeasurePreserving :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {g : α → β} {γ : Type u_5} {x : MeasurableSpace γ}
{x_1 : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ} {ν : MeasureTheory.Measure α},
MeasureTheory.AEStronglyMeasurable g ν →
MeasureTheory.Measure.QuasiMeasurePreserving f μ ν → MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
This is a theorem about the composition of certain types of measurable functions. It states that if a function `g` is "almost everywhere strongly measurable" with respect to a measure `ν`, and another function `f` is "quasi-measure preserving" from a measure `μ` to `ν`, then the composition of the two functions `g ∘ f` is also "almost everywhere strongly measurable" with respect to the measure `μ`.
Here, a function is considered "almost everywhere strongly measurable" if it is almost everywhere equal to the limit of a sequence of simple functions. A function is "quasi-measure preserving" if it transforms one measure to another in a way that preserves the measure of sets up to sets of measure zero.
More concisely: If a function `g` is almost everywhere strongly measurable with respect to measure `ν`, and another function `f` is quasi-measure preserving from measure `μ` to `ν`, then the composition `g ∘ f` is almost everywhere strongly measurable with respect to measure `μ`.
|
MeasureTheory.StronglyMeasurable.piecewise
theorem MeasureTheory.StronglyMeasurable.piecewise :
∀ {α : Type u_1} {β : Type u_2} {f g : α → β} {m : MeasurableSpace α} [inst : TopologicalSpace β] {s : Set α}
{x : DecidablePred fun x => x ∈ s},
MeasurableSet s →
MeasureTheory.StronglyMeasurable f →
MeasureTheory.StronglyMeasurable g → MeasureTheory.StronglyMeasurable (s.piecewise f g)
This theorem states that, given two strongly measurable functions `f` and `g` from a type `α` to a type `β`, a measurable set `s` of type `α`, and a decidable predicate `x` such that `x ∈ s`, if `f` and `g` are strongly measurable, then the piecewise function defined on `s` that equals `f` on the set `s` and `g` on its complement is also strongly measurable. Note that `β` is endowed with a topology, and `α` with a measurable space structure. Strong measurability of a function means that it can be approximated pointwise by a sequence of simple functions.
More concisely: Given two strongly measurable functions `f` and `g` from a measurable space `(α, Σ)` to a topological space `(β, τ)`, a measurable set `s ∈ Σ`, and a decidable predicate `x ∈ s`, the piecewise function `x ↦ if h x ∈ s then f x else g x` is strongly measurable, where `h` is the characteristic function of `s`.
|
stronglyMeasurable_of_tendsto
theorem stronglyMeasurable_of_tendsto :
∀ {α : Type u_1} {β : Type u_2} {ι : Type u_5} {m : MeasurableSpace α} [inst : TopologicalSpace β]
[inst_1 : TopologicalSpace.PseudoMetrizableSpace β] (u : Filter ι) [inst_2 : u.NeBot]
[inst_3 : u.IsCountablyGenerated] {f : ι → α → β} {g : α → β},
(∀ (i : ι), MeasureTheory.StronglyMeasurable (f i)) →
Filter.Tendsto f u (nhds g) → MeasureTheory.StronglyMeasurable g
The theorem `stronglyMeasurable_of_tendsto` states that if a sequence of functions, each of which is strongly measurable, converges to a limit function `g` with respect to a certain filter `u`, then this limit function `g` is also strongly measurable. Here, a function is called strongly measurable if it is the limit of simple functions. Furthermore, the convergence of the sequence of functions is defined in the sense that for each neighborhood of `g`, the preimage under the sequence of functions is a neighborhood in the filter `u`. This theorem is applicable in the context of a measurable space and two topological spaces, where the second topological space is pseudo-metrizable.
More concisely: If each function in a sequence of strongly measurable functions converges to a limit function with respect to a filter, then the limit function is also strongly measurable.
|
stronglyMeasurable_iff_measurable
theorem stronglyMeasurable_iff_measurable :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {mα : MeasurableSpace α} [inst : MeasurableSpace β]
[inst_1 : TopologicalSpace β] [inst_2 : TopologicalSpace.MetrizableSpace β] [inst_3 : BorelSpace β]
[inst_4 : SecondCountableTopology β], MeasureTheory.StronglyMeasurable f ↔ Measurable f
The theorem `stronglyMeasurable_iff_measurable` states that for any function `f` mapping from a type `α` to a type `β`, where `α` is a measurable space, `β` is a topological space, metrizable, a Borel space, and has a second countable topology, the function `f` is strongly measurable if and only if it is measurable. Here, a strongly measurable function is defined as one that is the limit of simple functions, and a function is measurable if the preimage of every measurable set is also a measurable set.
More concisely: A function between measurable and second countable Borel spaces is strongly measurable if and only if it is measurable.
|
MeasureTheory.AEStronglyMeasurable.neg
theorem MeasureTheory.AEStronglyMeasurable.neg :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} [inst_1 : Neg β] [inst_2 : ContinuousNeg β],
MeasureTheory.AEStronglyMeasurable f μ → MeasureTheory.AEStronglyMeasurable (-f) μ
The theorem `MeasureTheory.AEStronglyMeasurable.neg` states that for any given type `α`, type `β`, a measurable space `m` on `α`, a measure `μ` on that measurable space, a function `f` from `α` to `β`, and given that `β` is a topological space that supports negation operation and the negation operation is continuous, if the function `f` is almost everywhere strongly measurable with respect to measure `μ`, then the negative of function `f` (denoted as `-f`), is also almost everywhere strongly measurable with respect to the same measure `μ`. In other words, the property of being almost everywhere strongly measurable is preserved under the negation operation.
More concisely: If `f : α → β` is almost everywhere strongly measurable with respect to measure `μ` on measurable space `(α, Σ)` and `β` is a topological space with a continuous negation operation, then `-f` is almost everywhere strongly measurable with respect to `μ`.
|
MeasureTheory.StronglyMeasurable.measurable
theorem MeasureTheory.StronglyMeasurable.measurable :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {x : MeasurableSpace α} [inst : TopologicalSpace β]
[inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [inst_3 : BorelSpace β],
MeasureTheory.StronglyMeasurable f → Measurable f
The theorem states that a strongly measurable function is also measurable. In other words, if a function is defined such that it is the limit of simple functions (which is the definition of being strongly measurable), then this function also has the property of being measurable, meaning that the preimage of every measurable set under this function is also a measurable set. This theorem holds for any types `α` and `β` where `α` is a measurable space and `β` is a topological space, pseudo-metrizable space, measurable space, and Borel space.
More concisely: A strongly measurable function between measurable spaces is measurable.
|
Continuous.stronglyMeasurable_of_mulSupport_subset_isCompact
theorem Continuous.stronglyMeasurable_of_mulSupport_subset_isCompact :
∀ {α : Type u_1} {β : Type u_2} [inst : MeasurableSpace α] [inst_1 : TopologicalSpace α]
[inst_2 : OpensMeasurableSpace α] [inst_3 : MeasurableSpace β] [inst_4 : TopologicalSpace β]
[inst_5 : TopologicalSpace.PseudoMetrizableSpace β] [inst_6 : BorelSpace β] [inst_7 : One β] {f : α → β},
Continuous f → ∀ {k : Set α}, IsCompact k → Function.mulSupport f ⊆ k → MeasureTheory.StronglyMeasurable f
The theorem `Continuous.strongly_measurable_of_mulSupport_subset_isCompact` states that for any continuous function `f` from a measurable and topological space `α` to a measurable, topological, pseudometrizable, and one-space `β`, if the support of this function (defined as the set of points `x` in `α` where `f(x) ≠ 1`) is a subset of a compact set `k` in `α`, then `f` is strongly measurable. A function is strongly measurable if it is the limit of simple functions. A set is compact if for every nontrivial filter `f` that contains the set, there exists an element of the set such that every set of the filter meets every neighborhood of the element.
More concisely: If a continuous function from a measurable and topological space to a measurable, topological, pseudometrizable, and one-space with compact support is defined on a compact set, then the function is strongly measurable.
|
MeasurableEmbedding.aestronglyMeasurable_map_iff
theorem MeasurableEmbedding.aestronglyMeasurable_map_iff :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {γ : Type u_5} {mγ : MeasurableSpace γ}
{mα : MeasurableSpace α} {f : γ → α} {μ : MeasureTheory.Measure γ},
MeasurableEmbedding f →
∀ {g : α → β},
MeasureTheory.AEStronglyMeasurable g (MeasureTheory.Measure.map f μ) ↔
MeasureTheory.AEStronglyMeasurable (g ∘ f) μ
The theorem `MeasurableEmbedding.aestronglyMeasurable_map_iff` states that for any topological space `β`, any types `γ` and `α`, any measurable spaces `mγ` and `mα`, any function `f` from `γ` to `α`, any measure `μ` on `γ`, and any measurable embedding `f`, for any function `g` from `α` to `β`, `g` is almost everywhere strongly measurable with respect to the measure obtained by pushing forward `μ` by `f` if and only if the function composed of `g` and `f` is almost everywhere strongly measurable with respect to `μ`.
This means that the property of a function being almost everywhere strongly measurable is preserved under the operation of changing the domain via a measurable embedding and then applying the function. In terms of measure theory, it asserts a connection between the notions of measure and almost everywhere strong measurability under the operation of pushforward by a measurable embedding.
More concisely: For any measurable spaces `mγ`, `mα`, `β`, type `γ` and `α`, measurable embedding `f : γ → α`, measure `μ` on `γ`, function `g : α → β`, and almost everywhere strongly measurable functions `f` and `g`, the composition `g ∘ f` is almost everywhere strongly measurable with respect to `μ` if and only if `g` is almost everywhere strongly measurable with respect to the pushforward measure `μ` _via_ `f`.
|
MeasureTheory.StronglyMeasurable.comp_measurable
theorem MeasureTheory.StronglyMeasurable.comp_measurable :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} [inst : TopologicalSpace β] {x : MeasurableSpace α}
{x_1 : MeasurableSpace γ} {f : α → β} {g : γ → α},
MeasureTheory.StronglyMeasurable f → Measurable g → MeasureTheory.StronglyMeasurable (f ∘ g)
The theorem `MeasureTheory.StronglyMeasurable.comp_measurable` states that for all types `α`, `β`, and `γ`, given a topological space over `β`, a measurable space over `α`, and another measurable space over `γ`, if we have a function `f` from `α` to `β` that is strongly measurable (i.e., it can be approximated by a sequence of simple functions) and a function `g` from `γ` to `α` that is measurable (i.e., the preimage of every measurable set under `g` is also measurable), then the composition of `f` and `g` (denoted by `f ∘ g`) is also strongly measurable. This implies that the property of being strongly measurable is preserved under composition with a measurable function.
More concisely: If `f: α → β` is strongly measurable and `g: γ → α` is measurable, then the composition `f ∘ g: γ → β` is also strongly measurable.
|
MeasureTheory.StronglyMeasurable.ennnorm
theorem MeasureTheory.StronglyMeasurable.ennnorm :
∀ {α : Type u_1} {x : MeasurableSpace α} {β : Type u_5} [inst : SeminormedAddCommGroup β] {f : α → β},
MeasureTheory.StronglyMeasurable f → Measurable fun a => ↑‖f a‖₊
The theorem `MeasureTheory.StronglyMeasurable.ennnorm` states that for any type `α` with a `MeasurableSpace` structure, any type `β` with a `SeminormedAddCommGroup` structure, and any function `f` from `α` to `β`, if `f` is strongly measurable (that is, it is the limit of simple functions), then the function that maps each element `a` in `α` to the seminorm of `f(a)` is also measurable. In other words, the seminorm function preserves measurability when applied to a strongly measurable function.
More concisely: If `f` is a strongly measurable function from a measurable space `(α, Σ)` to a seminormed additive commutative group `(β, ∥.∥)`, then the function `x ↦ ∥f(x)∥` is measurable.
|
Measurable.aestronglyMeasurable
theorem Measurable.aestronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} [inst : TopologicalSpace β] {f : α → β} {x : MeasurableSpace α}
{μ : MeasureTheory.Measure α} [inst_1 : MeasurableSpace β] [inst_2 : TopologicalSpace.PseudoMetrizableSpace β]
[inst_3 : SecondCountableTopology β] [inst_4 : OpensMeasurableSpace β],
Measurable f → MeasureTheory.AEStronglyMeasurable f μ
This theorem states that in a space with a second-countable topology, if a function `f` is measurable, then it is also almost everywhere (a.e.) strongly measurable with respect to a measure `μ`. Here, a function is said to be measurable if the preimage of every measurable set is also measurable. A function is almost everywhere strongly measurable if it is almost everywhere equal to the limit of a sequence of simple functions. The space in question must be pseudometrizable and the open sets in this space must be measurable.
More concisely: In a second-countable, pseudometrizable space with measurable open sets, every measurable function is almost everywhere strongly measurable.
|
stronglyMeasurable_iff_measurable_separable
theorem stronglyMeasurable_iff_measurable_separable :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} {m : MeasurableSpace α} [inst : TopologicalSpace β]
[inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β] [inst_3 : BorelSpace β],
MeasureTheory.StronglyMeasurable f ↔ Measurable f ∧ TopologicalSpace.IsSeparable (Set.range f)
This theorem states that for any function 'f' from type 'α' to type 'β', with 'α' being a measurable space and 'β' being a topologically space, a pseudo-metrizable space, a measurable space, and a Borel space, the function 'f' is strongly measurable if and only if it is a measurable function and its range is a separable set. In terms of mathematics, a function is strongly measurable if it can be approximated by a sequence of simple functions, it is measurable if the preimage of every measurable set is also measurable, and its range is separable if it is included in the closure of a countable set.
More concisely: A function from a measurable space to a separable, Borel subspace of a topological space is strongly measurable if and only if it is measurable.
|
MeasureTheory.StronglyMeasurable.measurableSet_eq_fun
theorem MeasureTheory.StronglyMeasurable.measurableSet_eq_fun :
∀ {α : Type u_1} {m : MeasurableSpace α} {E : Type u_5} [inst : TopologicalSpace E]
[inst_1 : TopologicalSpace.MetrizableSpace E] {f g : α → E},
MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable g → MeasurableSet {x | f x = g x}
The theorem `MeasureTheory.StronglyMeasurable.measurableSet_eq_fun` states that for any two functions `f` and `g` from a measurable space `α` to a topological and metrizable space `E`, if both `f` and `g` are strongly measurable (i.e., each one is the limit of a sequence of simple functions), then the set of points in `α` where `f` and `g` agree is a measurable set. In other words, the set of all `x` in `α` such that `f(x)` equals `g(x)` is measurable.
More concisely: If `f` and `g` are two strongly measurable functions from a measurable space `α` to a topological and metrizable space `E`, then the set `{x ∈ α | f(x) = g(x)}` is measurable.
|
MeasureTheory.AEStronglyMeasurable.const_smul
theorem MeasureTheory.AEStronglyMeasurable.const_smul :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} {𝕜 : Type u_5} [inst_1 : SMul 𝕜 β] [inst_2 : ContinuousConstSMul 𝕜 β],
MeasureTheory.AEStronglyMeasurable f μ → ∀ (c : 𝕜), MeasureTheory.AEStronglyMeasurable (c • f) μ
The theorem `MeasureTheory.AEStronglyMeasurable.const_smul` states that for any types `α` and `β`, a measurable space `m` over `α`, a measure `μ` over the measurable space, a function `f` from `α` to `β`, a type `𝕜`, and the assumptions that the type `β` has a topological space structure, `𝕜` and `β` have a scalar multiplication operation, and that the scalar multiplication operation is continuously constant, if the function `f` is almost everywhere strongly measurable with respect to the measure `μ`, then for any element `c` of type `𝕜`, the function `c • f` (which denotes the scalar multiplication of `c` and `f`) is also almost everywhere strongly measurable with respect to the measure `μ`. In simpler terms, the scalar multiplication of a measurable function remains measurable.
More concisely: If a function between measurable spaces is almost everywhere strongly measurable and the scalar multiplication on its codomain is continuously constant, then the scalar multiplication of the function with any scalar is also almost everywhere strongly measurable.
|
Continuous.aestronglyMeasurable
theorem Continuous.aestronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} [inst_1 : TopologicalSpace α] [inst_2 : OpensMeasurableSpace α]
[inst_3 : TopologicalSpace.PseudoMetrizableSpace β] [inst_4 : SecondCountableTopologyEither α β],
Continuous f → MeasureTheory.AEStronglyMeasurable f μ
The theorem states that for any continuous function `f` from a measurable space `α` to a topological space `β`, the function is almost everywhere strongly measurable with respect to a measure `μ`, provided one of the two spaces, either `α` or `β`, has a second-countable topology. Here, a function is called almost everywhere strongly measurable if it is almost everywhere equal to the limit of a sequence of simple functions. A space having a second-countable topology means that it has a countable base for its topology. The conditions that `α` is an open measurable space and `β` is a pseudo-metrizable space are also required.
More concisely: If `α` is an open measurable space, `β` is a pseudo-metrizable space, and one of them has a second-countable topology, then every continuous function `f` from `α` to `β` is almost everywhere strongly measurable with respect to any measure `μ` on `α`.
|
MeasureTheory.FinStronglyMeasurable.fin_support_approx
theorem MeasureTheory.FinStronglyMeasurable.fin_support_approx :
∀ {α : Type u_1} {β : Type u_2} {m0 : MeasurableSpace α} {μ : MeasureTheory.Measure α} {f : α → β} [inst : Zero β]
[inst_1 : TopologicalSpace β] (hf : MeasureTheory.FinStronglyMeasurable f μ) (n : ℕ),
↑↑μ (Function.support ↑(hf.approx n)) < ⊤
The theorem `MeasureTheory.FinStronglyMeasurable.fin_support_approx` states that for any given function `f` from `α` to `β`, if `f` is FinStronglyMeasurable with respect to a measure `μ`, then for any natural number `n`, the measure of the support (i.e., the set of points `x` such that `f(x) ≠ 0`) of the `n`-th approximating simple function in the sequence guaranteed by `f`'s FinStronglyMeasurability is finite (i.e., less than infinity). Here, the approximating sequence of simple functions is produced by the existence property in the definition of FinStronglyMeasurable functions. In other words, every function in the approximating sequence for `f` has finite measure support.
More concisely: For any FinStronglyMeasurable function `f` from a measurable space `(α, Σ)` to another measurable space `(β, Τ)` and any natural number `n`, the support of the `n`-th approximating simple function in the sequence guaranteed by `f`'s FinStronglyMeasurability has finite measure.
|
MeasureTheory.finStronglyMeasurable_iff_measurable
theorem MeasureTheory.finStronglyMeasurable_iff_measurable :
∀ {α : Type u_1} {G : Type u_5} [inst : SeminormedAddCommGroup G] [inst_1 : MeasurableSpace G]
[inst_2 : BorelSpace G] [inst_3 : SecondCountableTopology G] {f : α → G} {_m0 : MeasurableSpace α}
(μ : MeasureTheory.Measure α) [inst_4 : MeasureTheory.SigmaFinite μ],
MeasureTheory.FinStronglyMeasurable f μ ↔ Measurable f
The theorem states that in a space with a second countable topology and a sigma-finite measure, a function is FinStronglyMeasurable with respect to a measure if and only if it is Measurable. Specifically, a function `f` from a type `α` to a seminormed add commutative group `G` (which has a Borel space structure, a second countable topology, and a measurable space structure) is FinStronglyMeasurable with respect to a measure `μ` on `α` (which is sigma-finite) if and only if `f` is Measurable.
In the context of measure theory, a function is FinStronglyMeasurable if it is the limit of simple functions whose support has finite measure, and it is Measurable if the preimage of every measurable set is measurable. Thus, this theorem connects these two notions of measurability in a certain topological context.
More concisely: In a second countable measurable space with a sigma-finite measure, a function is Fin Strongly Measurable if and only if it is Measurable.
|
Continuous.comp_stronglyMeasurable
theorem Continuous.comp_stronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} {γ : Type u_3} {x : MeasurableSpace α} [inst : TopologicalSpace β]
[inst_1 : TopologicalSpace γ] {g : β → γ} {f : α → β},
Continuous g → MeasureTheory.StronglyMeasurable f → MeasureTheory.StronglyMeasurable fun x => g (f x)
The theorem `Continuous.comp_stronglyMeasurable` states that for any three types `α`, `β`, and `γ`, where `α` is a measurable space and `β`, `γ` are topological spaces, if `g` is a continuous function from `β` to `γ`, and `f` is a function from `α` to `β` that is strongly measurable (meaning it can be approximated by a sequence of simple functions), then the composition function `g ∘ f` is also strongly measurable. In other words, the composition of a continuous function and a strongly measurable function is again strongly measurable.
More concisely: If `g` is continuous and `f` is strongly measurable, then the composition `g ∘ f` is also strongly measurable. (Assuming `α` is a measurable space and `β`, `γ` are topological spaces.)
|
aestronglyMeasurable_iff_aemeasurable_separable
theorem aestronglyMeasurable_iff_aemeasurable_separable :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} [inst_1 : TopologicalSpace.PseudoMetrizableSpace β] [inst_2 : MeasurableSpace β]
[inst_3 : BorelSpace β],
MeasureTheory.AEStronglyMeasurable f μ ↔
AEMeasurable f μ ∧ ∃ t, TopologicalSpace.IsSeparable t ∧ ∀ᵐ (x : α) ∂μ, f x ∈ t
The theorem `aestronglyMeasurable_iff_aemeasurable_separable` states that, for any function `f` from a measurable space `α` to a topological space `β` with respect to measure `μ`, the function is almost everywhere strongly measurable if and only if it is almost everywhere measurable and there exists a set `t` such that `t` is a separable set (i.e., it can be approximated by a countable set) and, except possibly on a set of measure zero, the range of the function `f` is contained in `t`. This theorem holds under the conditions that `β` is a pseudometrizable space, a measurable space, and a Borel space.
More concisely: A measurable function from a measurable space to a separable, pseudometrizable, Borel space is almost everywhere strongly measurable if and only if it is almost everywhere measurable and has range contained in a separable subset, up to a set of measure zero.
|
MeasureTheory.StronglyMeasurable.aestronglyMeasurable
theorem MeasureTheory.StronglyMeasurable.aestronglyMeasurable :
∀ {α : Type u_5} {β : Type u_6} {x : MeasurableSpace α} [inst : TopologicalSpace β] {f : α → β}
{μ : MeasureTheory.Measure α}, MeasureTheory.StronglyMeasurable f → MeasureTheory.AEStronglyMeasurable f μ
This theorem states that for any function `f` from a type `α` to a type `β`, with `α` having a measurable space structure and `β` a topological space structure, and given a measure `μ` on `α`, if `f` is strongly measurable (i.e., it is the limit of a sequence of simple functions), then `f` is also almost everywhere strongly measurable with respect to the measure `μ`. In other words, `f` is almost everywhere equal to a limit of a sequence of simple functions, except possibly on a set of measure zero.
More concisely: If `f` is a strongly measurable function from a measurable space `(α, Σ)` to a topological space `(β, τ)` with respect to a measure `μ`, then `f` is almost everywhere equal to a limit of simple functions in `L^1(μ)`.
|
MeasureTheory.AEStronglyMeasurable.ae_eq_mk
theorem MeasureTheory.AEStronglyMeasurable.ae_eq_mk :
∀ {α : Type u_1} {β : Type u_2} {m : MeasurableSpace α} {μ : MeasureTheory.Measure α} [inst : TopologicalSpace β]
{f : α → β} (hf : MeasureTheory.AEStronglyMeasurable f μ),
μ.ae.EventuallyEq f (MeasureTheory.AEStronglyMeasurable.mk f hf)
The theorem `MeasureTheory.AEStronglyMeasurable.ae_eq_mk` states that for any function `f` from `α` to `β` that is almost everywhere strongly measurable with respect to a measure `μ`, `f` is almost everywhere equal to its associated `MeasureTheory.AEStronglyMeasurable.mk f hf`. Here, `α` is a type with a `MeasurableSpace` structure, `β` is a type with a `TopologicalSpace` structure, and `μ` is a measure on `α`. The "almost everywhere" condition means that the set of points in `α` where `f` and `MeasureTheory.AEStronglyMeasurable.mk f hf` differ is a null set with respect to the measure `μ`. In other words, `f` and `MeasureTheory.AEStronglyMeasurable.mk f hf` are identical except possibly on a set of measure zero.
More concisely: A strongly almost everywhere measurable function from a measurable space to a topological space is almost everywhere equal to its associated measurable function constructed from its measurability hypothesis.
|
MeasureTheory.StronglyMeasurable.finStronglyMeasurable
theorem MeasureTheory.StronglyMeasurable.finStronglyMeasurable :
∀ {α : Type u_1} {β : Type u_2} {f : α → β} [inst : TopologicalSpace β] [inst_1 : Zero β] {m0 : MeasurableSpace α},
MeasureTheory.StronglyMeasurable f →
∀ (μ : MeasureTheory.Measure α) [inst_2 : MeasureTheory.SigmaFinite μ],
MeasureTheory.FinStronglyMeasurable f μ
The theorem `MeasureTheory.StronglyMeasurable.finStronglyMeasurable` states that for all strongly measurable functions `f` from `α` to `β` (where `β` is a topological space and `α` is a measurable space), if the measure `μ` on `α` is sigma-finite, then `f` is also finitely strongly measurable with respect to `μ`. Here, a function is said to be strongly measurable if it is the limit of simple functions, and it is said to be finitely strongly measurable with respect to a measure if it is the limit of simple functions whose support has finite measure.
More concisely: If `f` is a strongly measurable function from the sigma-finite measurable space `(α, Σ, μ)` to a topological space `β`, then `f` is finitely strongly measurable.
|