src/HOL/Analysis/Bounded_Continuous_Function.thy
author wenzelm
Mon Mar 25 17:21:26 2019 +0100 (2 months ago)
changeset 69981 3dced198b9ec
parent 69861 62e47f06d22c
child 70136 f03a01a18c6e
permissions -rw-r--r--
more strict AFP properties;
     1 section \<open>Bounded Continuous Functions\<close>
     2 
     3 theory Bounded_Continuous_Function
     4   imports
     5     Henstock_Kurzweil_Integration
     6 begin
     7 
     8 subsection \<open>Definition\<close>
     9 
    10 definition%important "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
    11 
    12 typedef (overloaded) ('a, 'b) bcontfun ("(_ \<Rightarrow>\<^sub>C /_)" [22, 21] 21) =
    13   "bcontfun::('a::topological_space \<Rightarrow> 'b::metric_space) set"
    14   morphisms apply_bcontfun Bcontfun
    15   by (auto intro: continuous_intros simp: bounded_def bcontfun_def)
    16 
    17 declare [[coercion "apply_bcontfun :: ('a::topological_space \<Rightarrow>\<^sub>C'b::metric_space) \<Rightarrow> 'a \<Rightarrow> 'b"]]
    18 
    19 setup_lifting type_definition_bcontfun
    20 
    21 lemma continuous_on_apply_bcontfun[intro, simp]: "continuous_on T (apply_bcontfun x)"
    22   and bounded_apply_bcontfun[intro, simp]: "bounded (range (apply_bcontfun x))"
    23   using apply_bcontfun[of x]
    24   by (auto simp: bcontfun_def intro: continuous_on_subset)
    25 
    26 lemma bcontfun_eqI: "(\<And>x. apply_bcontfun f x = apply_bcontfun g x) \<Longrightarrow> f = g"
    27   by transfer auto
    28 
    29 lemma bcontfunE:
    30   assumes "f \<in> bcontfun"
    31   obtains g where "f = apply_bcontfun g"
    32   by (blast intro: apply_bcontfun_cases assms )
    33 
    34 lemma const_bcontfun: "(\<lambda>x. b) \<in> bcontfun"
    35   by (auto simp: bcontfun_def continuous_on_const image_def)
    36 
    37 lift_definition const_bcontfun::"'b::metric_space \<Rightarrow> ('a::topological_space \<Rightarrow>\<^sub>C 'b)" is "\<lambda>c _. c"
    38   by (rule const_bcontfun)
    39 
    40 (* TODO: Generalize to uniform spaces? *)
    41 instantiation bcontfun :: (topological_space, metric_space) metric_space
    42 begin
    43 
    44 lift_definition%important dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real"
    45   is "\<lambda>f g. (SUP x. dist (f x) (g x))" .
    46 
    47 definition uniformity_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b \<times> 'a \<Rightarrow>\<^sub>C 'b) filter"
    48   where "uniformity_bcontfun = (INF e\<in>{0 <..}. principal {(x, y). dist x y < e})"
    49 
    50 definition open_bcontfun :: "('a \<Rightarrow>\<^sub>C 'b) set \<Rightarrow> bool"
    51   where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
    52 
    53 lemma bounded_dist_le_SUP_dist:
    54   "bounded (range f) \<Longrightarrow> bounded (range g) \<Longrightarrow> dist (f x) (g x) \<le> (SUP x. dist (f x) (g x))"
    55   by (auto intro!: cSUP_upper bounded_imp_bdd_above bounded_dist_comp)
    56 
    57 lemma dist_bounded:
    58   fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
    59   shows "dist (f x) (g x) \<le> dist f g"
    60   by transfer (auto intro!: bounded_dist_le_SUP_dist simp: bcontfun_def)
    61 
    62 lemma dist_bound:
    63   fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
    64   assumes "\<And>x. dist (f x) (g x) \<le> b"
    65   shows "dist f g \<le> b"
    66   using assms
    67   by transfer (auto intro!: cSUP_least)
    68 
    69 lemma dist_fun_lt_imp_dist_val_lt:
    70   fixes f g :: "'a \<Rightarrow>\<^sub>C 'b"
    71   assumes "dist f g < e"
    72   shows "dist (f x) (g x) < e"
    73   using dist_bounded assms by (rule le_less_trans)
    74 
    75 instance
    76 proof
    77   fix f g h :: "'a \<Rightarrow>\<^sub>C 'b"
    78   show "dist f g = 0 \<longleftrightarrow> f = g"
    79   proof
    80     have "\<And>x. dist (f x) (g x) \<le> dist f g"
    81       by (rule dist_bounded)
    82     also assume "dist f g = 0"
    83     finally show "f = g"
    84       by (auto simp: apply_bcontfun_inject[symmetric])
    85   qed (auto simp: dist_bcontfun_def intro!: cSup_eq)
    86   show "dist f g \<le> dist f h + dist g h"
    87   proof (rule dist_bound)
    88     fix x
    89     have "dist (f x) (g x) \<le> dist (f x) (h x) + dist (g x) (h x)"
    90       by (rule dist_triangle2)
    91     also have "dist (f x) (h x) \<le> dist f h"
    92       by (rule dist_bounded)
    93     also have "dist (g x) (h x) \<le> dist g h"
    94       by (rule dist_bounded)
    95     finally show "dist (f x) (g x) \<le> dist f h + dist g h"
    96       by simp
    97   qed
    98 qed (rule open_bcontfun_def uniformity_bcontfun_def)+
    99 
   100 end
   101 
   102 lift_definition PiC::"'a::topological_space set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b::metric_space) set"
   103   is "\<lambda>I X. Pi I X \<inter> bcontfun"
   104   by auto
   105 
   106 lemma mem_PiC_iff: "x \<in> PiC I X \<longleftrightarrow> apply_bcontfun x \<in> Pi I X"
   107   by transfer simp
   108 
   109 lemmas mem_PiCD = mem_PiC_iff[THEN iffD1]
   110   and mem_PiCI = mem_PiC_iff[THEN iffD2]
   111 
   112 lemma tendsto_bcontfun_uniform_limit:
   113   fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
   114   assumes "(f \<longlongrightarrow> l) F"
   115   shows "uniform_limit UNIV f l F"
   116 proof (rule uniform_limitI)
   117   fix e::real assume "e > 0"
   118   from tendstoD[OF assms this] have "\<forall>\<^sub>F x in F. dist (f x) l < e" .
   119   then show "\<forall>\<^sub>F n in F. \<forall>x\<in>UNIV. dist ((f n) x) (l x) < e"
   120     by eventually_elim (auto simp: dist_fun_lt_imp_dist_val_lt)
   121 qed
   122 
   123 lemma uniform_limit_tendsto_bcontfun:
   124   fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
   125     and l::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
   126   assumes "uniform_limit UNIV f l F"
   127   shows "(f \<longlongrightarrow> l) F"
   128 proof (rule tendstoI)
   129   fix e::real assume "e > 0"
   130   then have "e / 2 > 0" by simp
   131   from uniform_limitD[OF assms this]
   132   have "\<forall>\<^sub>F i in F. \<forall>x. dist (f i x) (l x) < e / 2" by simp
   133   then have "\<forall>\<^sub>F x in F. dist (f x) l \<le> e / 2"
   134     by eventually_elim (blast intro: dist_bound less_imp_le)
   135   then show "\<forall>\<^sub>F x in F. dist (f x) l < e"
   136     by eventually_elim (use \<open>0 < e\<close> in auto)
   137 qed
   138 
   139 lemma uniform_limit_bcontfunE:
   140   fixes f::"'i \<Rightarrow> 'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
   141     and l::"'a::topological_space \<Rightarrow> 'b::metric_space"
   142   assumes "uniform_limit UNIV f l F" "F \<noteq> bot"
   143   obtains l'::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
   144   where "l = l'" "(f \<longlongrightarrow> l') F"
   145   by (metis (mono_tags, lifting) always_eventually apply_bcontfun apply_bcontfun_cases assms
   146       bcontfun_def mem_Collect_eq uniform_limit_bounded uniform_limit_tendsto_bcontfun
   147       uniform_limit_theorem)
   148 
   149 lemma closed_PiC:
   150   fixes I :: "'a::metric_space set"
   151     and X :: "'a \<Rightarrow> 'b::complete_space set"
   152   assumes "\<And>i. i \<in> I \<Longrightarrow> closed (X i)"
   153   shows "closed (PiC I X)"
   154   unfolding closed_sequential_limits
   155 proof safe
   156   fix f l
   157   assume seq: "\<forall>n. f n \<in> PiC I X" and lim: "f \<longlonglongrightarrow> l"
   158   show "l \<in> PiC I X"
   159   proof (safe intro!: mem_PiCI)
   160     fix x assume "x \<in> I"
   161     then have "closed (X x)"
   162       using assms by simp
   163     moreover have "eventually (\<lambda>i. f i x \<in> X x) sequentially"
   164       using seq \<open>x \<in> I\<close>
   165       by (auto intro!: eventuallyI dest!: mem_PiCD simp: Pi_iff)
   166     moreover note sequentially_bot
   167     moreover have "(\<lambda>n. (f n) x) \<longlonglongrightarrow> l x"
   168       using tendsto_bcontfun_uniform_limit[OF lim]
   169       by (rule tendsto_uniform_limitI) simp
   170     ultimately show "l x \<in> X x"
   171       by (rule Lim_in_closed_set)
   172   qed
   173 qed
   174 
   175 
   176 subsection \<open>Complete Space\<close>
   177 
   178 instance%important bcontfun :: (metric_space, complete_space) complete_space
   179 proof%unimportant
   180   fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun"
   181   assume "Cauchy f"  \<comment> \<open>Cauchy equals uniform convergence\<close>
   182   then obtain g where "uniform_limit UNIV f g sequentially"
   183     using uniformly_convergent_eq_cauchy[of "\<lambda>_. True" f]
   184     unfolding Cauchy_def uniform_limit_sequentially_iff
   185     by (metis dist_fun_lt_imp_dist_val_lt)
   186 
   187   from uniform_limit_bcontfunE[OF this sequentially_bot]
   188   obtain l' where "g = apply_bcontfun l'" "(f \<longlonglongrightarrow> l')" by metis
   189   then show "convergent f"
   190     by (intro convergentI)
   191 qed
   192 
   193 
   194 subsection%unimportant \<open>Supremum norm for a normed vector space\<close>
   195 
   196 instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_vector
   197 begin
   198 
   199 lemma uminus_cont: "f \<in> bcontfun \<Longrightarrow> (\<lambda>x. - f x) \<in> bcontfun" for f::"'a \<Rightarrow> 'b"
   200   by (auto simp: bcontfun_def intro!: continuous_intros)
   201 
   202 lemma plus_cont: "f \<in> bcontfun \<Longrightarrow> g \<in> bcontfun \<Longrightarrow> (\<lambda>x. f x + g x) \<in> bcontfun" for f g::"'a \<Rightarrow> 'b"
   203   by (auto simp: bcontfun_def intro!: continuous_intros bounded_plus_comp)
   204 
   205 lemma minus_cont: "f \<in> bcontfun \<Longrightarrow> g \<in> bcontfun \<Longrightarrow> (\<lambda>x. f x - g x) \<in> bcontfun" for f g::"'a \<Rightarrow> 'b"
   206   by (auto simp: bcontfun_def intro!: continuous_intros bounded_minus_comp)
   207 
   208 lemma scaleR_cont: "f \<in> bcontfun \<Longrightarrow> (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun" for f :: "'a \<Rightarrow> 'b"
   209   by (auto simp: bcontfun_def intro!: continuous_intros bounded_scaleR_comp)
   210 
   211 lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
   212   by (auto simp: bcontfun_def intro: boundedI)
   213 
   214 lift_definition uminus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>f x. - f x"
   215   by (rule uminus_cont)
   216 
   217 lift_definition plus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>f g x. f x + g x"
   218   by (rule plus_cont)
   219 
   220 lift_definition minus_bcontfun::"('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>f g x. f x - g x"
   221   by (rule minus_cont)
   222 
   223 lift_definition zero_bcontfun::"'a \<Rightarrow>\<^sub>C 'b" is "\<lambda>_. 0"
   224   by (rule const_bcontfun)
   225 
   226 lemma const_bcontfun_0_eq_0[simp]: "const_bcontfun 0 = 0"
   227   by transfer simp
   228 
   229 lift_definition scaleR_bcontfun::"real \<Rightarrow> ('a \<Rightarrow>\<^sub>C 'b) \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b"  is "\<lambda>r g x. r *\<^sub>R g x"
   230   by (rule scaleR_cont)
   231 
   232 lemmas [simp] =
   233   const_bcontfun.rep_eq
   234   uminus_bcontfun.rep_eq
   235   plus_bcontfun.rep_eq
   236   minus_bcontfun.rep_eq
   237   zero_bcontfun.rep_eq
   238   scaleR_bcontfun.rep_eq
   239 
   240 
   241 instance
   242   by standard (auto intro!: bcontfun_eqI simp: algebra_simps)
   243 
   244 end
   245 
   246 lemma bounded_norm_le_SUP_norm:
   247   "bounded (range f) \<Longrightarrow> norm (f x) \<le> (SUP x. norm (f x))"
   248   by (auto intro!: cSUP_upper bounded_imp_bdd_above simp: bounded_norm_comp)
   249 
   250 instantiation%unimportant bcontfun :: (topological_space, real_normed_vector) real_normed_vector
   251 begin
   252 
   253 definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real"
   254   where "norm_bcontfun f = dist f 0"
   255 
   256 definition "sgn (f::('a,'b) bcontfun) = f /\<^sub>R norm f"
   257 
   258 instance
   259 proof
   260   fix a :: real
   261   fix f g :: "('a, 'b) bcontfun"
   262   show "dist f g = norm (f - g)"
   263     unfolding norm_bcontfun_def
   264     by transfer (simp add: dist_norm)
   265   show "norm (f + g) \<le> norm f + norm g"
   266     unfolding norm_bcontfun_def
   267     by transfer
   268       (auto intro!: cSUP_least norm_triangle_le add_mono bounded_norm_le_SUP_norm
   269         simp: dist_norm bcontfun_def)
   270   show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
   271     unfolding norm_bcontfun_def
   272     apply transfer
   273     by (rule trans[OF _ continuous_at_Sup_mono[symmetric]])
   274       (auto intro!: monoI mult_left_mono continuous_intros bounded_imp_bdd_above
   275         simp: bounded_norm_comp bcontfun_def image_comp)
   276 qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
   277 
   278 end
   279 
   280 lemma norm_bounded:
   281   fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
   282   shows "norm (apply_bcontfun f x) \<le> norm f"
   283   using dist_bounded[of f x 0]
   284   by (simp add: dist_norm)
   285 
   286 lemma norm_bound:
   287   fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
   288   assumes "\<And>x. norm (apply_bcontfun f x) \<le> b"
   289   shows "norm f \<le> b"
   290   using dist_bound[of f 0 b] assms
   291   by (simp add: dist_norm)
   292 
   293 subsection%unimportant \<open>(bounded) continuous extenstion\<close>
   294 
   295 lemma integral_clamp:
   296   "integral {t0::real..clamp t0 t1 x} f =
   297     (if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)"
   298   by (auto simp: clamp_def)
   299 
   300 lemma continuous_on_interval_bcontfunE:
   301   fixes f::"'a::ordered_euclidean_space \<Rightarrow> 'b::metric_space"
   302   assumes "continuous_on {a .. b} f"
   303   obtains g::"'a \<Rightarrow>\<^sub>C 'b" where
   304     "\<And>x. a \<le> x \<Longrightarrow> x \<le> b \<Longrightarrow> g x = f x"
   305     "\<And>x. g x = f (clamp a b x)"
   306 proof -
   307   define g where "g \<equiv> ext_cont f a b"
   308   have "g \<in> bcontfun"
   309     using assms
   310     by (auto intro!: continuous_on_ext_cont simp: g_def cbox_interval bcontfun_def)
   311       (auto simp: g_def ext_cont_def cbox_interval
   312         intro!: compact_interval clamp_bounded compact_imp_bounded[OF compact_continuous_image] assms)
   313   then obtain h where h: "g = apply_bcontfun h" by (rule bcontfunE)
   314   then have "h x = f x" if "a \<le> x" "x \<le> b" for x
   315     by (auto simp: h[symmetric] g_def cbox_interval that)
   316   moreover
   317   have "h x = f (clamp a b x)" for x
   318     by (auto simp: h[symmetric] g_def ext_cont_def)
   319   ultimately show ?thesis ..
   320 qed
   321 
   322 lifting_update bcontfun.lifting
   323 lifting_forget bcontfun.lifting
   324 
   325 end