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