# Documentation

Mathlib.MeasureTheory.Constructions.BorelSpace.ContinuousLinearMap

# 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} [] :
instance ContinuousLinearMap.instBorelSpace {𝕜 : Type u_2} {E : Type u_3} [] {F : Type u_4} [] :
BorelSpace (E →L[𝕜] F)
theorem ContinuousLinearMap.measurable_apply {𝕜 : Type u_2} {E : Type u_3} [] {F : Type u_4} [] [] [] (x : E) :
Measurable fun f => f x
theorem ContinuousLinearMap.measurable_apply' {𝕜 : Type u_2} {E : Type u_3} [] {F : Type u_4} [] [] [] [] :
Measurable fun x f => f x
theorem ContinuousLinearMap.measurable_coe {𝕜 : Type u_2} {E : Type u_3} [] {F : Type u_4} [] [] [] :
Measurable fun f x => 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)