# Measurable functions in normed spaces #

theorem ContinuousLinearMap.measurable {𝕜 : Type u_2} [] {E : Type u_3} [] [] {F : Type u_4} [] [] [] (L : E →L[𝕜] F) :
theorem ContinuousLinearMap.measurable_comp {α : Type u_1} [] {𝕜 : Type u_2} [] {E : Type u_3} [] [] {F : Type u_4} [] [] [] (L : E →L[𝕜] F) {φ : αE} (φ_meas : ) :
Measurable fun (a : α) => L (φ a)
instance ContinuousLinearMap.instMeasurableSpace {𝕜 : Type u_2} {E : Type u_3} [] {F : Type u_4} [] :
Equations
• ContinuousLinearMap.instMeasurableSpace = borel (E →L[𝕜] F)
instance ContinuousLinearMap.instBorelSpace {𝕜 : Type u_2} {E : Type u_3} [] {F : Type u_4} [] :
BorelSpace (E →L[𝕜] F)
Equations
• =
theorem ContinuousLinearMap.measurable_apply {𝕜 : Type u_2} {E : Type u_3} [] {F : Type u_4} [] [] [] (x : E) :
Measurable fun (f : E →L[𝕜] F) => f x
theorem ContinuousLinearMap.measurable_apply' {𝕜 : Type u_2} {E : Type u_3} [] {F : Type u_4} [] [] [] [] :
Measurable fun (x : E) (f : E →L[𝕜] F) => f x
theorem ContinuousLinearMap.measurable_coe {𝕜 : Type u_2} {E : Type u_3} [] {F : Type u_4} [] [] [] :
Measurable fun (f : E →L[𝕜] F) (x : E) => f x
theorem Measurable.apply_continuousLinearMap {α : Type u_1} [] {𝕜 : Type u_2} {E : Type u_3} [] [] [] {F : Type u_4} [] {φ : αF →L[𝕜] E} (hφ : ) (v : F) :
Measurable fun (a : α) => (φ a) v
theorem AEMeasurable.apply_continuousLinearMap {α : Type u_1} [] {𝕜 : Type u_2} {E : Type u_3} [] [] [] {F : Type u_4} [] {φ : αF →L[𝕜] E} {μ : } (hφ : ) (v : F) :
AEMeasurable (fun (a : α) => (φ a) v) μ
theorem measurable_smul_const {α : Type u_1} [] {𝕜 : Type u_2} [] [] [] {E : Type u_3} [] [] [] {f : α𝕜} {c : E} (hc : c 0) :
(Measurable fun (x : α) => f x c)
theorem aemeasurable_smul_const {α : Type u_1} [] {𝕜 : Type u_2} [] [] [] {E : Type u_3} [] [] [] {f : α𝕜} {μ : } {c : E} (hc : c 0) :
AEMeasurable (fun (x : α) => f x c) μ