src/HOL/Analysis/Lipschitz.thy

 section \<open>Lipschitz continuity\<close>
 theory Lipschitz
   imports Borel_Space
 begin
 
-definition lipschitz_on
+definition%important lipschitz_on
   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))"
 
 bundle lipschitz_syntax begin
-notation lipschitz_on ("_-lipschitz'_on" [1000])
+notation%important lipschitz_on ("_-lipschitz'_on" [1000])
 end
 bundle no_lipschitz_syntax begin
 no_notation lipschitz_on ("_-lipschitz'_on" [1000])
 end
 

     show ?thesis
       by (auto simp: fg)
   qed
 qed (rule lipschitz_on_nonneg[OF f])
 
-proposition lipschitz_on_concat_max:
+lemma lipschitz_on_concat_max:
   fixes a b c::real
   assumes f: "L-lipschitz_on {a .. b} f"
   assumes g: "M-lipschitz_on {b .. c} g"
   assumes fg: "f b = g b"
   shows "(max L M)-lipschitz_on {a .. c} (\<lambda>x. if x \<le> b then f x else g x)"

 qed
 
 
 subsubsection \<open>Continuity\<close>
 
-lemma lipschitz_on_uniformly_continuous:
+proposition lipschitz_on_uniformly_continuous:
   assumes "L-lipschitz_on X f"
   shows "uniformly_continuous_on X f"
   unfolding uniformly_continuous_on_def
 proof safe
   fix e::real

   show "\<exists>d>0. \<forall>x\<in>X. \<forall>x'\<in>X. dist x' x < d \<longrightarrow> dist (f x') (f x) < e"
     using lipschitz_onD[OF l] lipschitz_on_nonneg[OF assms] \<open>0 < e\<close>
     by (force intro!: exI[where x="e/(L + 1)"] simp: field_simps)
 qed
 
-lemma lipschitz_on_continuous_on:
+proposition lipschitz_on_continuous_on:
   "continuous_on X f" if "L-lipschitz_on X f"
   by (rule uniformly_continuous_imp_continuous[OF lipschitz_on_uniformly_continuous[OF that]])
 
 lemma lipschitz_on_continuous_within:
   "continuous (at x within X) f" if "L-lipschitz_on X f" "x \<in> X"
   using lipschitz_on_continuous_on[OF that(1)] that(2)
   by (auto simp: continuous_on_eq_continuous_within)
 
 subsubsection \<open>Differentiable functions\<close>
 
-lemma bounded_derivative_imp_lipschitz:
+proposition bounded_derivative_imp_lipschitz:
   assumes "\<And>x. x \<in> X \<Longrightarrow> (f has_derivative f' x) (at x within X)"
   assumes convex: "convex X"
   assumes "\<And>x. x \<in> X \<Longrightarrow> onorm (f' x) \<le> C" "0 \<le> C"
   shows "C-lipschitz_on X f"
 proof (rule lipschitz_onI)
   show "\<And>x y. x \<in> X \<Longrightarrow> y \<in> X \<Longrightarrow> dist (f x) (f y) \<le> C * dist x y"
     by (auto intro!: assms differentiable_bound[unfolded dist_norm[symmetric], OF convex])
 qed fact
 
 
-subsubsection \<open>Structural introduction rules\<close>
+subsubsection%unimportant \<open>Structural introduction rules\<close>
 
 named_theorems lipschitz_intros "structural introduction rules for Lipschitz controls"
 
 lemma lipschitz_on_compose [lipschitz_intros]:
   "(D * C)-lipschitz_on U (g o f)"

 qed
 
 
 subsection \<open>Local Lipschitz continuity (uniform for a family of functions)\<close>
 
-definition local_lipschitz::
+definition%important local_lipschitz::
   "'a::metric_space set \<Rightarrow> 'b::metric_space set \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'c::metric_space) \<Rightarrow> bool"
   where
   "local_lipschitz T X f \<equiv> \<forall>x \<in> X. \<forall>t \<in> T.
     \<exists>u>0. \<exists>L. \<forall>t \<in> cball t u \<inter> T. L-lipschitz_on (cball x u \<inter> X) (f t)"
 

   from lipschitz_boundE[of "(cball x 1 \<inter> B)"] obtain C where "C-lipschitz_on (cball x 1 \<inter> B) f" by auto
   then show ?case
     by (auto intro: exI[where x=1])
 qed
 
-lemma c1_implies_local_lipschitz:
+proposition c1_implies_local_lipschitz:
   fixes T::"real set" and X::"'a::{banach,heine_borel} set"
     and f::"real \<Rightarrow> 'a \<Rightarrow> 'a"
   assumes f': "\<And>t x. t \<in> T \<Longrightarrow> x \<in> X \<Longrightarrow> (f t has_derivative blinfun_apply (f' (t, x))) (at x)"
   assumes cont_f': "continuous_on (T \<times> X) f'"
   assumes "open T"