equal
deleted
inserted
replaced
4 *) |
4 *) |
5 section \<open>Lipschitz Continuity\<close> |
5 section \<open>Lipschitz Continuity\<close> |
6 |
6 |
7 theory Lipschitz |
7 theory Lipschitz |
8 imports |
8 imports |
9 Derivative |
9 Derivative Abstract_Metric_Spaces |
10 begin |
10 begin |
11 |
11 |
12 definition\<^marker>\<open>tag important\<close> lipschitz_on |
12 definition\<^marker>\<open>tag important\<close> lipschitz_on |
13 where "lipschitz_on C U f \<longleftrightarrow> (0 \<le> C \<and> (\<forall>x \<in> U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y))" |
13 where "lipschitz_on C U f \<longleftrightarrow> (0 \<le> C \<and> (\<forall>x \<in> U. \<forall>y\<in>U. dist (f x) (f y) \<le> C * dist x y))" |
14 |
14 |
115 have "lipschitz_on (max L M) {a .. b} f" "lipschitz_on (max L M) {b .. c} g" |
115 have "lipschitz_on (max L M) {a .. b} f" "lipschitz_on (max L M) {b .. c} g" |
116 by (auto intro!: lipschitz_on_mono[OF f order_refl] lipschitz_on_mono[OF g order_refl]) |
116 by (auto intro!: lipschitz_on_mono[OF f order_refl] lipschitz_on_mono[OF g order_refl]) |
117 from lipschitz_on_concat[OF this fg] show ?thesis . |
117 from lipschitz_on_concat[OF this fg] show ?thesis . |
118 qed |
118 qed |
119 |
119 |
|
120 text \<open>Equivalence between "abstract" and "type class" Lipschitz notions, |
|
121 for all types in the metric space class\<close> |
|
122 lemma Lipschitz_map_euclidean [simp]: |
|
123 "Lipschitz_continuous_map euclidean_metric euclidean_metric f |
|
124 \<longleftrightarrow> (\<exists>B. lipschitz_on B UNIV f)" (is "?lhs \<longleftrightarrow> ?rhs") |
|
125 proof |
|
126 show "?lhs \<Longrightarrow> ?rhs" |
|
127 by (force simp add: Lipschitz_continuous_map_pos lipschitz_on_def less_le_not_le) |
|
128 show "?rhs \<Longrightarrow> ?lhs" |
|
129 by (metis Lipschitz_continuous_map_def lipschitz_onD mdist_euclidean_metric mspace_euclidean_metric top_greatest) |
|
130 qed |
120 |
131 |
121 subsubsection \<open>Continuity\<close> |
132 subsubsection \<open>Continuity\<close> |
122 |
133 |
123 proposition lipschitz_on_uniformly_continuous: |
134 proposition lipschitz_on_uniformly_continuous: |
124 assumes "L-lipschitz_on X f" |
135 assumes "L-lipschitz_on X f" |