-
Notifications
You must be signed in to change notification settings - Fork 307
/
Linear.lean
154 lines (119 loc) · 6.1 KB
/
Linear.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
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
/-
Copyright (c) 2019 Jeremy Avigad. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Jeremy Avigad, Sébastien Gouëzel, Yury Kudryashov
-/
import Mathlib.Analysis.Calculus.FDeriv.Basic
import Mathlib.Analysis.NormedSpace.BoundedLinearMaps
#align_import analysis.calculus.fderiv.linear from "leanprover-community/mathlib"@"e3fb84046afd187b710170887195d50bada934ee"
/-!
# The derivative of bounded linear maps
For detailed documentation of the Fréchet derivative,
see the module docstring of `Analysis/Calculus/FDeriv/Basic.lean`.
This file contains the usual formulas (and existence assertions) for the derivative of
bounded linear maps.
-/
open Filter Asymptotics ContinuousLinearMap Set Metric
open scoped Classical
open Topology NNReal Filter Asymptotics ENNReal
noncomputable section
section
variable {𝕜 : Type*} [NontriviallyNormedField 𝕜]
variable {E : Type*} [NormedAddCommGroup E] [NormedSpace 𝕜 E]
variable {F : Type*} [NormedAddCommGroup F] [NormedSpace 𝕜 F]
variable {G : Type*} [NormedAddCommGroup G] [NormedSpace 𝕜 G]
variable {G' : Type*} [NormedAddCommGroup G'] [NormedSpace 𝕜 G']
variable {f f₀ f₁ g : E → F}
variable {f' f₀' f₁' g' : E →L[𝕜] F}
variable (e : E →L[𝕜] F)
variable {x : E}
variable {s t : Set E}
variable {L L₁ L₂ : Filter E}
section ContinuousLinearMap
/-!
### Continuous linear maps
There are currently two variants of these in mathlib, the bundled version
(named `ContinuousLinearMap`, and denoted `E →L[𝕜] F`), and the unbundled version (with a
predicate `IsBoundedLinearMap`). We give statements for both versions. -/
@[fun_prop]
protected theorem ContinuousLinearMap.hasStrictFDerivAt {x : E} : HasStrictFDerivAt e e x :=
(isLittleO_zero _ _).congr_left fun x => by simp only [e.map_sub, sub_self]
#align continuous_linear_map.has_strict_fderiv_at ContinuousLinearMap.hasStrictFDerivAt
protected theorem ContinuousLinearMap.hasFDerivAtFilter : HasFDerivAtFilter e e x L :=
.of_isLittleO <| (isLittleO_zero _ _).congr_left fun x => by simp only [e.map_sub, sub_self]
#align continuous_linear_map.has_fderiv_at_filter ContinuousLinearMap.hasFDerivAtFilter
@[fun_prop]
protected theorem ContinuousLinearMap.hasFDerivWithinAt : HasFDerivWithinAt e e s x :=
e.hasFDerivAtFilter
#align continuous_linear_map.has_fderiv_within_at ContinuousLinearMap.hasFDerivWithinAt
@[fun_prop]
protected theorem ContinuousLinearMap.hasFDerivAt : HasFDerivAt e e x :=
e.hasFDerivAtFilter
#align continuous_linear_map.has_fderiv_at ContinuousLinearMap.hasFDerivAt
@[simp, fun_prop]
protected theorem ContinuousLinearMap.differentiableAt : DifferentiableAt 𝕜 e x :=
e.hasFDerivAt.differentiableAt
#align continuous_linear_map.differentiable_at ContinuousLinearMap.differentiableAt
@[fun_prop]
protected theorem ContinuousLinearMap.differentiableWithinAt : DifferentiableWithinAt 𝕜 e s x :=
e.differentiableAt.differentiableWithinAt
#align continuous_linear_map.differentiable_within_at ContinuousLinearMap.differentiableWithinAt
@[simp]
protected theorem ContinuousLinearMap.fderiv : fderiv 𝕜 e x = e :=
e.hasFDerivAt.fderiv
#align continuous_linear_map.fderiv ContinuousLinearMap.fderiv
protected theorem ContinuousLinearMap.fderivWithin (hxs : UniqueDiffWithinAt 𝕜 s x) :
fderivWithin 𝕜 e s x = e := by
rw [DifferentiableAt.fderivWithin e.differentiableAt hxs]
exact e.fderiv
#align continuous_linear_map.fderiv_within ContinuousLinearMap.fderivWithin
@[simp, fun_prop]
protected theorem ContinuousLinearMap.differentiable : Differentiable 𝕜 e := fun _ =>
e.differentiableAt
#align continuous_linear_map.differentiable ContinuousLinearMap.differentiable
@[fun_prop]
protected theorem ContinuousLinearMap.differentiableOn : DifferentiableOn 𝕜 e s :=
e.differentiable.differentiableOn
#align continuous_linear_map.differentiable_on ContinuousLinearMap.differentiableOn
theorem IsBoundedLinearMap.hasFDerivAtFilter (h : IsBoundedLinearMap 𝕜 f) :
HasFDerivAtFilter f h.toContinuousLinearMap x L :=
h.toContinuousLinearMap.hasFDerivAtFilter
#align is_bounded_linear_map.has_fderiv_at_filter IsBoundedLinearMap.hasFDerivAtFilter
@[fun_prop]
theorem IsBoundedLinearMap.hasFDerivWithinAt (h : IsBoundedLinearMap 𝕜 f) :
HasFDerivWithinAt f h.toContinuousLinearMap s x :=
h.hasFDerivAtFilter
#align is_bounded_linear_map.has_fderiv_within_at IsBoundedLinearMap.hasFDerivWithinAt
@[fun_prop]
theorem IsBoundedLinearMap.hasFDerivAt (h : IsBoundedLinearMap 𝕜 f) :
HasFDerivAt f h.toContinuousLinearMap x :=
h.hasFDerivAtFilter
#align is_bounded_linear_map.has_fderiv_at IsBoundedLinearMap.hasFDerivAt
@[fun_prop]
theorem IsBoundedLinearMap.differentiableAt (h : IsBoundedLinearMap 𝕜 f) : DifferentiableAt 𝕜 f x :=
h.hasFDerivAt.differentiableAt
#align is_bounded_linear_map.differentiable_at IsBoundedLinearMap.differentiableAt
@[fun_prop]
theorem IsBoundedLinearMap.differentiableWithinAt (h : IsBoundedLinearMap 𝕜 f) :
DifferentiableWithinAt 𝕜 f s x :=
h.differentiableAt.differentiableWithinAt
#align is_bounded_linear_map.differentiable_within_at IsBoundedLinearMap.differentiableWithinAt
theorem IsBoundedLinearMap.fderiv (h : IsBoundedLinearMap 𝕜 f) :
fderiv 𝕜 f x = h.toContinuousLinearMap :=
HasFDerivAt.fderiv h.hasFDerivAt
#align is_bounded_linear_map.fderiv IsBoundedLinearMap.fderiv
theorem IsBoundedLinearMap.fderivWithin (h : IsBoundedLinearMap 𝕜 f)
(hxs : UniqueDiffWithinAt 𝕜 s x) : fderivWithin 𝕜 f s x = h.toContinuousLinearMap := by
rw [DifferentiableAt.fderivWithin h.differentiableAt hxs]
exact h.fderiv
#align is_bounded_linear_map.fderiv_within IsBoundedLinearMap.fderivWithin
@[fun_prop]
theorem IsBoundedLinearMap.differentiable (h : IsBoundedLinearMap 𝕜 f) : Differentiable 𝕜 f :=
fun _ => h.differentiableAt
#align is_bounded_linear_map.differentiable IsBoundedLinearMap.differentiable
@[fun_prop]
theorem IsBoundedLinearMap.differentiableOn (h : IsBoundedLinearMap 𝕜 f) : DifferentiableOn 𝕜 f s :=
h.differentiable.differentiableOn
#align is_bounded_linear_map.differentiable_on IsBoundedLinearMap.differentiableOn
end ContinuousLinearMap
end