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
```