-
Notifications
You must be signed in to change notification settings - Fork 259
/
ContinuousLinearMap.lean
112 lines (83 loc) · 4.41 KB
/
ContinuousLinearMap.lean
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
/-
Copyright (c) 2020 Patrick Massot. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Patrick Massot
-/
import Mathlib.MeasureTheory.Constructions.BorelSpace.Basic
import Mathlib.Analysis.NormedSpace.OperatorNorm.NormedSpace
import Mathlib.Topology.Algebra.Module.FiniteDimension
#align_import measure_theory.constructions.borel_space.continuous_linear_map from "leanprover-community/mathlib"@"bf6a01357ff5684b1ebcd0f1a13be314fc82c0bf"
/-!
# Measurable functions in normed spaces
-/
open MeasureTheory
variable {α : Type*} [MeasurableSpace α]
namespace ContinuousLinearMap
variable {𝕜 : Type*} [NormedField 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace E]
[OpensMeasurableSpace E] {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F] [MeasurableSpace F]
[BorelSpace F]
@[fun_prop, measurability]
protected theorem measurable (L : E →L[𝕜] F) : Measurable L :=
L.continuous.measurable
#align continuous_linear_map.measurable ContinuousLinearMap.measurable
@[fun_prop]
theorem measurable_comp (L : E →L[𝕜] F) {φ : α → E} (φ_meas : Measurable φ) :
Measurable fun a : α => L (φ a) :=
L.measurable.comp φ_meas
#align continuous_linear_map.measurable_comp ContinuousLinearMap.measurable_comp
end ContinuousLinearMap
namespace ContinuousLinearMap
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] {F : Type*} [NormedAddCommGroup F]
[NormedSpace 𝕜 F]
instance instMeasurableSpace : MeasurableSpace (E →L[𝕜] F) :=
borel _
#align continuous_linear_map.measurable_space ContinuousLinearMap.instMeasurableSpace
instance instBorelSpace : BorelSpace (E →L[𝕜] F) :=
⟨rfl⟩
#align continuous_linear_map.borel_space ContinuousLinearMap.instBorelSpace
@[fun_prop, measurability]
theorem measurable_apply [MeasurableSpace F] [BorelSpace F] (x : E) :
Measurable fun f : E →L[𝕜] F => f x :=
(apply 𝕜 F x).continuous.measurable
#align continuous_linear_map.measurable_apply ContinuousLinearMap.measurable_apply
@[measurability]
theorem measurable_apply' [MeasurableSpace E] [OpensMeasurableSpace E] [MeasurableSpace F]
[BorelSpace F] : Measurable fun (x : E) (f : E →L[𝕜] F) => f x :=
measurable_pi_lambda _ fun f => f.measurable
#align continuous_linear_map.measurable_apply' ContinuousLinearMap.measurable_apply'
@[measurability]
theorem measurable_coe [MeasurableSpace F] [BorelSpace F] :
Measurable fun (f : E →L[𝕜] F) (x : E) => f x :=
measurable_pi_lambda _ measurable_apply
#align continuous_linear_map.measurable_coe ContinuousLinearMap.measurable_coe
end ContinuousLinearMap
section ContinuousLinearMapNontriviallyNormedField
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace E] [BorelSpace E]
{F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
@[fun_prop, measurability]
theorem Measurable.apply_continuousLinearMap {φ : α → F →L[𝕜] E} (hφ : Measurable φ) (v : F) :
Measurable fun a => φ a v :=
(ContinuousLinearMap.apply 𝕜 E v).measurable.comp hφ
#align measurable.apply_continuous_linear_map Measurable.apply_continuousLinearMap
@[measurability]
theorem AEMeasurable.apply_continuousLinearMap {φ : α → F →L[𝕜] E} {μ : Measure α}
(hφ : AEMeasurable φ μ) (v : F) : AEMeasurable (fun a => φ a v) μ :=
(ContinuousLinearMap.apply 𝕜 E v).measurable.comp_aemeasurable hφ
#align ae_measurable.apply_continuous_linear_map AEMeasurable.apply_continuousLinearMap
end ContinuousLinearMapNontriviallyNormedField
section NormedSpace
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜] [CompleteSpace 𝕜] [MeasurableSpace 𝕜]
variable [BorelSpace 𝕜] {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E] [MeasurableSpace E]
[BorelSpace E]
theorem measurable_smul_const {f : α → 𝕜} {c : E} (hc : c ≠ 0) :
(Measurable fun x => f x • c) ↔ Measurable f :=
(closedEmbedding_smul_left hc).measurableEmbedding.measurable_comp_iff
#align measurable_smul_const measurable_smul_const
theorem aemeasurable_smul_const {f : α → 𝕜} {μ : Measure α} {c : E} (hc : c ≠ 0) :
AEMeasurable (fun x => f x • c) μ ↔ AEMeasurable f μ :=
(closedEmbedding_smul_left hc).measurableEmbedding.aemeasurable_comp_iff
#align ae_measurable_smul_const aemeasurable_smul_const
end NormedSpace