139 apply (drule local.tendsto) |
139 apply (drule local.tendsto) |
140 apply (simp add: local.scaleR local.diff local.add local.zero) |
140 apply (simp add: local.scaleR local.diff local.add local.zero) |
141 done |
141 done |
142 |
142 |
143 lemmas scaleR_right_has_derivative = |
143 lemmas scaleR_right_has_derivative = |
144 bounded_linear.has_derivative [OF bounded_linear_scaleR_right, standard] |
144 bounded_linear.has_derivative [OF bounded_linear_scaleR_right] |
145 |
145 |
146 lemmas scaleR_left_has_derivative = |
146 lemmas scaleR_left_has_derivative = |
147 bounded_linear.has_derivative [OF bounded_linear_scaleR_left, standard] |
147 bounded_linear.has_derivative [OF bounded_linear_scaleR_left] |
148 |
148 |
149 lemmas inner_right_has_derivative = |
149 lemmas inner_right_has_derivative = |
150 bounded_linear.has_derivative [OF bounded_linear_inner_right, standard] |
150 bounded_linear.has_derivative [OF bounded_linear_inner_right] |
151 |
151 |
152 lemmas inner_left_has_derivative = |
152 lemmas inner_left_has_derivative = |
153 bounded_linear.has_derivative [OF bounded_linear_inner_left, standard] |
153 bounded_linear.has_derivative [OF bounded_linear_inner_left] |
154 |
154 |
155 lemmas mult_right_has_derivative = |
155 lemmas mult_right_has_derivative = |
156 bounded_linear.has_derivative [OF bounded_linear_mult_right, standard] |
156 bounded_linear.has_derivative [OF bounded_linear_mult_right] |
157 |
157 |
158 lemmas mult_left_has_derivative = |
158 lemmas mult_left_has_derivative = |
159 bounded_linear.has_derivative [OF bounded_linear_mult_left, standard] |
159 bounded_linear.has_derivative [OF bounded_linear_mult_left] |
160 |
160 |
161 lemmas euclidean_component_has_derivative = |
161 lemmas euclidean_component_has_derivative = |
162 bounded_linear.has_derivative [OF bounded_linear_euclidean_component] |
162 bounded_linear.has_derivative [OF bounded_linear_euclidean_component] |
163 |
163 |
164 lemma has_derivative_neg: |
164 lemma has_derivative_neg: |