# Measurable functions in normed spaces #

source
theorem ContinuousLinearMap.measurable {R : Type u_2} {E : Type u_3} {F : Type u_4} [Semiring R] [SeminormedAddCommGroup E] [Module R E] [MeasurableSpace E] [OpensMeasurableSpace E] [SeminormedAddCommGroup F] [Module R F] [MeasurableSpace F] [BorelSpace F] (L : E →L[R] F) :
Measurable ⇑L
source
theorem ContinuousLinearMap.measurable_comp {α : Type u_1} [MeasurableSpace α] {R : Type u_2} {E : Type u_3} {F : Type u_4} [Semiring R] [SeminormedAddCommGroup E] [Module R E] [MeasurableSpace E] [OpensMeasurableSpace E] [SeminormedAddCommGroup F] [Module R F] [MeasurableSpace F] [BorelSpace F] (L : E →L[R] F) {φ : α → E} (φ_meas : Measurable φ) :
Measurable fun (a : α) => L (φ a)
source
instance ContinuousLinearMap.instMeasurableSpace {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
MeasurableSpace (E →L[𝕜] F)
Equations

- ContinuousLinearMap.instMeasurableSpace = borel (E →L[𝕜] F)

source
instance ContinuousLinearMap.instBorelSpace {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] :
BorelSpace (E →L[𝕜] F)
source
theorem ContinuousLinearMap.measurable_apply {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [MeasurableSpace F] [BorelSpace F] (x : E) :
Measurable fun (f : E →L[𝕜] F) => f x
source
theorem ContinuousLinearMap.measurable_apply' {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [MeasurableSpace E] [OpensMeasurableSpace E] [MeasurableSpace F] [BorelSpace F] :
Measurable fun (x : E) (f : E →L[𝕜] F) => f x
source
theorem ContinuousLinearMap.measurable_coe {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [MeasurableSpace F] [BorelSpace F] :
Measurable fun (f : E →L[𝕜] F) (x : E) => f x
source
theorem Measurable.apply_continuousLinearMap {α : Type u_1} [MeasurableSpace α] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace E] [BorelSpace E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {φ : α → F →L[𝕜] E} (hφ : Measurable φ) (v : F) :
Measurable fun (a : α) => (φ a) v
source
theorem AEMeasurable.apply_continuousLinearMap {α : Type u_1} [MeasurableSpace α] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace E] [BorelSpace E] {F : Type u_4} [NormedAddCommGroup F] [NormedSpace 𝕜 F] {φ : α → F →L[𝕜] E} {μ : MeasureTheory.Measure α} (hφ : AEMeasurable φ μ) (v : F) :
AEMeasurable (fun (a : α) => (φ a) v) μ
source
theorem measurable_smul_const {α : Type u_1} [MeasurableSpace α] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [MeasurableSpace 𝕜] [BorelSpace 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace E] [BorelSpace E] {f : α → 𝕜} {c : E} (hc : c ≠ 0) :
(Measurable fun (x : α) => f x • c) ↔ Measurable f
source
theorem aemeasurable_smul_const {α : Type u_1} [MeasurableSpace α] {𝕜 : Type u_2} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [MeasurableSpace 𝕜] [BorelSpace 𝕜] {E : Type u_3} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace E] [BorelSpace E] {f : α → 𝕜} {μ : MeasureTheory.Measure α} {c : E} (hc : c ≠ 0) :
AEMeasurable (fun (x : α) => f x • c) μ ↔ AEMeasurable f μ