Measurable functions in normed spaces #
theorem
ContinuousLinearMap.measurable
{𝕜 : Type u_2}
[NormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[MeasurableSpace F]
[BorelSpace F]
(L : E →L[𝕜] F)
:
Measurable ⇑L
theorem
ContinuousLinearMap.measurable_comp
{α : Type u_1}
[MeasurableSpace α]
{𝕜 : Type u_2}
[NormedField 𝕜]
{E : Type u_3}
[NormedAddCommGroup E]
[NormedSpace 𝕜 E]
[MeasurableSpace E]
[OpensMeasurableSpace E]
{F : Type u_4}
[NormedAddCommGroup F]
[NormedSpace 𝕜 F]
[MeasurableSpace F]
[BorelSpace F]
(L : E →L[𝕜] F)
{φ : α → E}
(φ_meas : Measurable φ)
:
Measurable fun (a : α) => L (φ a)
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)
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)
Equations
- ⋯ = ⋯
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
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
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
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
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) μ
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
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 μ