mathlib3 documentation

measure_theory.constructions.borel_space.continuous_linear_map

Measurable functions in normed spaces #

THIS FILE IS SYNCHRONIZED WITH MATHLIB4. Any changes to this file require a corresponding PR to mathlib4.

source
@[protected, measurability]
theorem continuous_linear_map.measurable {π•œ : Type u_2} [normed_field π•œ] {E : Type u_3} [normed_add_comm_group E] [normed_space π•œ E] [measurable_space E] [opens_measurable_space E] {F : Type u_4} [normed_add_comm_group F] [normed_space π•œ F] [measurable_space F] [borel_space F] (L : E β†’L[π•œ] F) :
measurable ⇑L
source
theorem continuous_linear_map.measurable_comp {Ξ± : Type u_1} [measurable_space Ξ±] {π•œ : Type u_2} [normed_field π•œ] {E : Type u_3} [normed_add_comm_group E] [normed_space π•œ E] [measurable_space E] [opens_measurable_space E] {F : Type u_4} [normed_add_comm_group F] [normed_space π•œ F] [measurable_space F] [borel_space F] (L : E β†’L[π•œ] F) {Ο† : Ξ± β†’ E} (Ο†_meas : measurable Ο†) :
measurable (Ξ» (a : Ξ±), ⇑L (Ο† a))
source
@[protected, instance]
def continuous_linear_map.measurable_space {π•œ : Type u_2} [nontrivially_normed_field π•œ] {E : Type u_3} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_4} [normed_add_comm_group F] [normed_space π•œ F] :
measurable_space (E β†’L[π•œ] F)
Equations
source
@[protected, instance]
def continuous_linear_map.borel_space {π•œ : Type u_2} [nontrivially_normed_field π•œ] {E : Type u_3} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_4} [normed_add_comm_group F] [normed_space π•œ F] :
borel_space (E β†’L[π•œ] F)
source
@[measurability]
theorem continuous_linear_map.measurable_apply {π•œ : Type u_2} [nontrivially_normed_field π•œ] {E : Type u_3} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_4} [normed_add_comm_group F] [normed_space π•œ F] [measurable_space F] [borel_space F] (x : E) :
measurable (Ξ» (f : E β†’L[π•œ] F), ⇑f x)
source
@[measurability]
theorem continuous_linear_map.measurable_apply' {π•œ : Type u_2} [nontrivially_normed_field π•œ] {E : Type u_3} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_4} [normed_add_comm_group F] [normed_space π•œ F] [measurable_space E] [opens_measurable_space E] [measurable_space F] [borel_space F] :
measurable (Ξ» (x : E) (f : E β†’L[π•œ] F), ⇑f x)
source
@[measurability]
theorem continuous_linear_map.measurable_coe {π•œ : Type u_2} [nontrivially_normed_field π•œ] {E : Type u_3} [normed_add_comm_group E] [normed_space π•œ E] {F : Type u_4} [normed_add_comm_group F] [normed_space π•œ F] [measurable_space F] [borel_space F] :
measurable (Ξ» (f : E β†’L[π•œ] F) (x : E), ⇑f x)
source
@[measurability]
theorem measurable.apply_continuous_linear_map {Ξ± : Type u_1} [measurable_space Ξ±] {π•œ : Type u_2} [nontrivially_normed_field π•œ] {E : Type u_3} [normed_add_comm_group E] [normed_space π•œ E] [measurable_space E] [borel_space E] {F : Type u_4} [normed_add_comm_group F] [normed_space π•œ F] {Ο† : Ξ± β†’ (F β†’L[π•œ] E)} (hΟ† : measurable Ο†) (v : F) :
measurable (Ξ» (a : Ξ±), ⇑(Ο† a) v)
source
@[measurability]
theorem ae_measurable.apply_continuous_linear_map {Ξ± : Type u_1} [measurable_space Ξ±] {π•œ : Type u_2} [nontrivially_normed_field π•œ] {E : Type u_3} [normed_add_comm_group E] [normed_space π•œ E] [measurable_space E] [borel_space E] {F : Type u_4} [normed_add_comm_group F] [normed_space π•œ F] {Ο† : Ξ± β†’ (F β†’L[π•œ] E)} {ΞΌ : measure_theory.measure Ξ±} (hΟ† : ae_measurable Ο† ΞΌ) (v : F) :
ae_measurable (Ξ» (a : Ξ±), ⇑(Ο† a) v) ΞΌ
source
theorem measurable_smul_const {Ξ± : Type u_1} [measurable_space Ξ±] {π•œ : Type u_2} [nontrivially_normed_field π•œ] [complete_space π•œ] [measurable_space π•œ] [borel_space π•œ] {E : Type u_3} [normed_add_comm_group E] [normed_space π•œ E] [measurable_space E] [borel_space E] {f : Ξ± β†’ π•œ} {c : E} (hc : c β‰  0) :
measurable (Ξ» (x : Ξ±), f x β€’ c) ↔ measurable f
source
theorem ae_measurable_smul_const {Ξ± : Type u_1} [measurable_space Ξ±] {π•œ : Type u_2} [nontrivially_normed_field π•œ] [complete_space π•œ] [measurable_space π•œ] [borel_space π•œ] {E : Type u_3} [normed_add_comm_group E] [normed_space π•œ E] [measurable_space E] [borel_space E] {f : Ξ± β†’ π•œ} {ΞΌ : measure_theory.measure Ξ±} {c : E} (hc : c β‰  0) :
ae_measurable (Ξ» (x : Ξ±), f x β€’ c) ΞΌ ↔ ae_measurable f ΞΌ