measurable_smul_const
theorem measurable_smul_const :
∀ {α : Type u_1} [inst : MeasurableSpace α] {𝕜 : Type u_2} [inst_1 : NontriviallyNormedField 𝕜]
[inst_2 : CompleteSpace 𝕜] [inst_3 : MeasurableSpace 𝕜] [inst_4 : BorelSpace 𝕜] {E : Type u_3}
[inst_5 : NormedAddCommGroup E] [inst_6 : NormedSpace 𝕜 E] [inst_7 : MeasurableSpace E] [inst_8 : BorelSpace E]
{f : α → 𝕜} {c : E}, c ≠ 0 → ((Measurable fun x => f x • c) ↔ Measurable f)
The theorem `measurable_smul_const` states that for any two types `α` and `𝕜`, where `α` is a measurable space and `𝕜` is a non-trivially normed field with complete space, borel space, and measurable properties; for any type `E` which is a normed add commutative group, a normed space over `𝕜`, and also a borel and measurable space; for any function `f : α → 𝕜` and any constant `c : E` which is not equal to zero, the function `f` multiplied by the constant `c` (denoted as `f x • c`) is measurable if and only if `f` itself is measurable.
In mathematical terms, it essentially says that for a non-zero constant, the measurability of a scalar multiplication of a function is equivalent to the measurability of the function itself.
More concisely: For any measurable function between measurable spaces and a non-trivially normed field with complete space, borel space, and measurable properties, the scalar multiplication of the function by a non-zero constant is measurable if and only if the function itself is measurable.
|
ContinuousLinearMap.measurable_apply
theorem ContinuousLinearMap.measurable_apply :
∀ {𝕜 : Type u_2} [inst : NontriviallyNormedField 𝕜] {E : Type u_3} [inst_1 : NormedAddCommGroup E]
[inst_2 : NormedSpace 𝕜 E] {F : Type u_4} [inst_3 : NormedAddCommGroup F] [inst_4 : NormedSpace 𝕜 F]
[inst_5 : MeasurableSpace F] [inst_6 : BorelSpace F] (x : E), Measurable fun f => f x
This theorem states that for any non-trivially normed field `𝕜`, normed additive commutative groups `E` and `F`, and a normed space over `𝕜` for `E` and `F` with `F` being a measurable space and a Borel space, for any element `x` from `E`, the function application that maps every continuous linear map `f` to `f x` is measurable. In other words, if `f` is a continuous linear map and `x` is a point in the domain, then the function that takes `f` to `f(x)` is measurable. This means that the preimage of any measurable set under this function is also a measurable set.
More concisely: For any non-trivially normed field `𝕜`, if `E` and `F` are normed additive commutative groups and `F` is a measurable Borel space, then the function that maps every continuous linear map from `E` to `F` to its application to a fixed `x` in `E` is measurable.
|