Quelle Bounded_Continuous_Function.thy Sprache: Isabelle

section \<open>Bounded Continuous Functions\<close>

theory Bounded_Continuous_Function
  imports
    Topology_Euclidean_Space
    Uniform_Limit
begin

subsection \<open>Definition\<close>

definition\<^marker>\<open>tag important\<close> "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"

typedef (overloaded) ('a, 'b) bcontfun (\<open>(\<open>notation=\<open>infix \<Rightarrow>\<^sub>C\<close>\<close>_ \<Rightarrow>\<^sub>C /_)\<close> [22, 21] 21) =
  "bcontfun::('a::topological_space \ 'b::metric_space) set"
  morphisms apply_bcontfun Bcontfun
  by (auto intro: continuous_intros simp: bounded_def bcontfun_def)

declare [[coercion "apply_bcontfun :: ('a::topological_space \\<^sub>C'b::metric_space) \ 'a \ 'b"]]

setup_lifting type_definition_bcontfun

lemma continuous_on_apply_bcontfun[intro, simp]: "continuous_on T (apply_bcontfun x)"
  and bounded_apply_bcontfun[intro, simp]: "bounded (range (apply_bcontfun x))"
  using apply_bcontfun[of x]
  by (auto simp: bcontfun_def intro: continuous_on_subset)

lemma bcontfun_eqI: "(\x. apply_bcontfun f x = apply_bcontfun g x) \ f = g"
  by transfer auto

lemma bcontfunE:
  assumes "f \ bcontfun"
  obtains g where "f = apply_bcontfun g"
  by (blast intro: apply_bcontfun_cases assms )

lemma const_bcontfun: "(\x. b) \ bcontfun"
  by (auto simp: bcontfun_def image_def)

lift_definition const_bcontfun::"'b::metric_space \ ('a::topological_space \\<^sub>C 'b)" is "\c _. c"
  by (rule const_bcontfun)

(* TODO: Generalize to uniform spaces? *)
instantiation bcontfun :: (topological_space, metric_space) metric_space
begin

lift_definition\<^marker>\<open>tag important\<close> dist_bcontfun :: "'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> 'a \<Rightarrow>\<^sub>C 'b \<Rightarrow> real"
  is "\f g. (SUP x. dist (f x) (g x))" .

definition uniformity_bcontfun :: "('a \\<^sub>C 'b \ 'a \\<^sub>C 'b) filter"
  where "uniformity_bcontfun = (INF e\{0 <..}. principal {(x, y). dist x y < e})"

definition open_bcontfun :: "('a \\<^sub>C 'b) set \ bool"
  where "open_bcontfun S = (\x\S. \\<^sub>F (x', y) in uniformity. x' = x \ y \ S)"

lemma bounded_dist_le_SUP_dist:
  "bounded (range f) \ bounded (range g) \ dist (f x) (g x) \ (SUP x. dist (f x) (g x))"
  by (auto intro!: cSUP_upper bounded_imp_bdd_above bounded_dist_comp)

lemma dist_bounded:
  fixes f g :: "'a \\<^sub>C 'b"
  shows "dist (f x) (g x) \ dist f g"
  by transfer (auto intro!: bounded_dist_le_SUP_dist simp: bcontfun_def)

lemma dist_bound:
  fixes f g :: "'a \\<^sub>C 'b"
  assumes "\x. dist (f x) (g x) \ b"
  shows "dist f g \ b"
  using assms
  by transfer (auto intro!: cSUP_least)

lemma dist_fun_lt_imp_dist_val_lt:
  fixes f g :: "'a \\<^sub>C 'b"
  assumes "dist f g < e"
  shows "dist (f x) (g x) < e"
  using dist_bounded assms by (rule le_less_trans)

instance
proof
  fix f g h :: "'a \\<^sub>C 'b"
  show "dist f g = 0 \ f = g"
  proof
    have "\x. dist (f x) (g x) \ dist f g"
      by (rule dist_bounded)
    also assume "dist f g = 0"
    finally show "f = g"
      by (auto simp: apply_bcontfun_inject[symmetric])
  qed (auto simp: dist_bcontfun_def intro!: cSup_eq)
  show "dist f g \ dist f h + dist g h"
  proof (rule dist_bound)
    fix x
    have "dist (f x) (g x) \ dist (f x) (h x) + dist (g x) (h x)"
      by (rule dist_triangle2)
    also have "dist (f x) (h x) \ dist f h"
      by (rule dist_bounded)
    also have "dist (g x) (h x) \ dist g h"
      by (rule dist_bounded)
    finally show "dist (f x) (g x) \ dist f h + dist g h"
      by simp
  qed
qed (rule open_bcontfun_def uniformity_bcontfun_def)+

end

lift_definition PiC::"'a::topological_space set \ ('a \ 'b set) \ ('a \\<^sub>C 'b::metric_space) set"
  is "\I X. Pi I X \ bcontfun"
  by auto

lemma mem_PiC_iff: "x \ PiC I X \ apply_bcontfun x \ Pi I X"
  by transfer simp

lemmas mem_PiCD = mem_PiC_iff[THEN iffD1]
  and mem_PiCI = mem_PiC_iff[THEN iffD2]

lemma tendsto_bcontfun_uniform_limit:
  fixes f::"'i \ 'a::topological_space \\<^sub>C 'b::metric_space"
  assumes "(f \ l) F"
  shows "uniform_limit UNIV f l F"
proof (rule uniform_limitI)
  fix e::real assume "e > 0"
  from tendstoD[OF assms this] have "\\<^sub>F x in F. dist (f x) l < e" .
  then show "\\<^sub>F n in F. \x\UNIV. dist ((f n) x) (l x) < e"
    by eventually_elim (auto simp: dist_fun_lt_imp_dist_val_lt)
qed

lemma uniform_limit_tendsto_bcontfun:
  fixes f::"'i \ 'a::topological_space \\<^sub>C 'b::metric_space"
    and l::"'a::topological_space \\<^sub>C 'b::metric_space"
  assumes "uniform_limit UNIV f l F"
  shows "(f \ l) F"
proof (rule tendstoI)
  fix e::real assume "e > 0"
  then have "e / 2 > 0" by simp
  from uniform_limitD[OF assms this]
  have "\\<^sub>F i in F. \x. dist (f i x) (l x) < e / 2" by simp
  then have "\\<^sub>F x in F. dist (f x) l \ e / 2"
    by eventually_elim (blast intro: dist_bound less_imp_le)
  then show "\\<^sub>F x in F. dist (f x) l < e"
    by eventually_elim (use \<open>0 < e\<close> in auto)
qed

lemma uniform_limit_bcontfunE:
  fixes f::"'i \ 'a::topological_space \\<^sub>C 'b::metric_space"
    and l::"'a::topological_space \ 'b::metric_space"
  assumes "uniform_limit UNIV f l F" "F \ bot"
  obtains l'::"'a::topological_space \<Rightarrow>\<^sub>C 'b::metric_space"
  where "l = l'" "(f \ l') F"
  by (metis (mono_tags, lifting) always_eventually apply_bcontfun apply_bcontfun_cases assms
      bcontfun_def mem_Collect_eq uniform_limit_bounded uniform_limit_tendsto_bcontfun
      uniform_limit_theorem)

lemma closed_PiC:
  fixes I :: "'a::metric_space set"
    and X :: "'a \ 'b::complete_space set"
  assumes "\i. i \ I \ closed (X i)"
  shows "closed (PiC I X)"
  unfolding closed_sequential_limits
proof safe
  fix f l
  assume seq: "\n. f n \ PiC I X" and lim: "f \ l"
  show "l \ PiC I X"
  proof (safe intro!: mem_PiCI)
    fix x assume "x \ I"
    then have "closed (X x)"
      using assms by simp
    moreover have "eventually (\i. f i x \ X x) sequentially"
      using seq \<open>x \<in> I\<close>
      by (auto intro!: eventuallyI dest!: mem_PiCD simp: Pi_iff)
    moreover note sequentially_bot
    moreover have "(\n. (f n) x) \ l x"
      using tendsto_bcontfun_uniform_limit[OF lim]
      by (rule tendsto_uniform_limitI) simp
    ultimately show "l x \ X x"
      by (rule Lim_in_closed_set)
  qed
qed

subsection \<open>Complete Space\<close>

instance\<^marker>\<open>tag important\<close> bcontfun :: (metric_space, complete_space) complete_space
proof
  fix f :: "nat \ ('a, 'b) bcontfun"
  assume "Cauchy f"  \<comment> \<open>Cauchy equals uniform convergence\<close>
  then obtain g where "uniform_limit UNIV f g sequentially"
    using uniformly_convergent_eq_cauchy[of "\_. True" f]
    unfolding Cauchy_def uniform_limit_sequentially_iff
    by (metis dist_fun_lt_imp_dist_val_lt)

  from uniform_limit_bcontfunE[OF this sequentially_bot]
  obtain l' where "g = apply_bcontfun l'" "(f \<longlonglongrightarrow> l')" by metis
  then show "convergent f"
    by (intro convergentI)
qed

subsection\<^marker>\<open>tag unimportant\<close> \<open>Supremum norm for a normed vector space\<close>

instantiation\<^marker>\<open>tag unimportant\<close> bcontfun :: (topological_space, real_normed_vector) real_vector
begin

lemma uminus_cont: "f \ bcontfun \ (\x. - f x) \ bcontfun" for f::"'a \ 'b"
  by (auto simp: bcontfun_def intro!: continuous_intros)

lemma plus_cont: "f \ bcontfun \ g \ bcontfun \ (\x. f x + g x) \ bcontfun" for f g::"'a \ 'b"
  by (auto simp: bcontfun_def intro!: continuous_intros bounded_plus_comp)

lemma minus_cont: "f \ bcontfun \ g \ bcontfun \ (\x. f x - g x) \ bcontfun" for f g::"'a \ 'b"
  by (auto simp: bcontfun_def intro!: continuous_intros bounded_minus_comp)

lemma scaleR_cont: "f \ bcontfun \ (\x. a *\<^sub>R f x) \ bcontfun" for f :: "'a \ 'b"
  by (auto simp: bcontfun_def intro!: continuous_intros bounded_scaleR_comp)

lemma bcontfun_normI: "continuous_on UNIV f \ (\x. norm (f x) \ b) \ f \ bcontfun"
  by (auto simp: bcontfun_def intro: boundedI)

lift_definition uminus_bcontfun::"('a \\<^sub>C 'b) \ 'a \\<^sub>C 'b" is "\f x. - f x"
  by (rule uminus_cont)

lift_definition plus_bcontfun::"('a \\<^sub>C 'b) \ ('a \\<^sub>C 'b) \ 'a \\<^sub>C 'b" is "\f g x. f x + g x"
  by (rule plus_cont)

lift_definition minus_bcontfun::"('a \\<^sub>C 'b) \ ('a \\<^sub>C 'b) \ 'a \\<^sub>C 'b" is "\f g x. f x - g x"
  by (rule minus_cont)

lift_definition zero_bcontfun::"'a \\<^sub>C 'b" is "\_. 0"
  by (rule const_bcontfun)

lemma const_bcontfun_0_eq_0[simp]: "const_bcontfun 0 = 0"
  by transfer simp

lift_definition scaleR_bcontfun::"real \ ('a \\<^sub>C 'b) \ 'a \\<^sub>C 'b" is "\r g x. r *\<^sub>R g x"
  by (rule scaleR_cont)

lemmas [simp] =
  const_bcontfun.rep_eq
  uminus_bcontfun.rep_eq
  plus_bcontfun.rep_eq
  minus_bcontfun.rep_eq
  zero_bcontfun.rep_eq
  scaleR_bcontfun.rep_eq

instance
  by standard (auto intro!: bcontfun_eqI simp: algebra_simps)

end

instantiation\<^marker>\<open>tag unimportant\<close> bcontfun :: (topological_space, real_normed_vector) real_normed_vector
begin

definition norm_bcontfun :: "('a, 'b) bcontfun \ real"
  where "norm_bcontfun f = dist f 0"

definition "sgn (f::('a,'b) bcontfun) = f /\<^sub>R norm f"

instance
proof
  fix a :: real
  fix f g :: "('a, 'b) bcontfun"
  show "dist f g = norm (f - g)"
    unfolding norm_bcontfun_def
    by transfer (simp add: dist_norm)
  show "norm (f + g) \ norm f + norm g"
    unfolding norm_bcontfun_def
    by transfer
      (auto intro!: cSUP_least norm_triangle_le add_mono bounded_norm_le_SUP_norm
        simp: dist_norm bcontfun_def)
  show "norm (a *\<^sub>R f) = \a\ * norm f"
    unfolding norm_bcontfun_def
    apply transfer
    by (rule trans[OF _ continuous_at_Sup_mono[symmetric]])
      (auto intro!: monoI mult_left_mono continuous_intros bounded_imp_bdd_above
        simp: bounded_norm_comp bcontfun_def image_comp)
qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)

end

lemma norm_bounded:
  fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
  shows "norm (apply_bcontfun f x) \ norm f"
  using dist_bounded[of f x 0]
  by (simp add: dist_norm)

lemma norm_bound:
  fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
  assumes "\x. norm (apply_bcontfun f x) \ b"
  shows "norm f \ b"
  using dist_bound[of f 0 b] assms
  by (simp add: dist_norm)

subsection\<^marker>\<open>tag unimportant\<close> \<open>(bounded) continuous extenstion\<close>

lemma continuous_on_cbox_bcontfunE:
  fixes f::"'a::euclidean_space \ 'b::metric_space"
  assumes "continuous_on (cbox a b) f"
  obtains g::"'a \\<^sub>C 'b" where
    "\x. x \ cbox a b \ g x = f x"
    "\x. g x = f (clamp a b x)"
proof -
  define g where "g \ ext_cont f a b"
  have "g \ bcontfun"
    using assms
    by (auto intro!: continuous_on_ext_cont simp: g_def bcontfun_def)
      (auto simp: g_def ext_cont_def
        intro!: clamp_bounded compact_imp_bounded[OF compact_continuous_image] assms)
  then obtain h where h: "g = apply_bcontfun h" by (rule bcontfunE)
  then have "h x = f x" if "x \ cbox a b" for x
    by (auto simp: h[symmetric] g_def that)
  moreover
  have "h x = f (clamp a b x)" for x
    by (auto simp: h[symmetric] g_def ext_cont_def)
  ultimately show ?thesis ..
qed

lifting_update bcontfun.lifting
lifting_forget bcontfun.lifting

end

quality93%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.