src/HOL/Analysis/Bounded_Continuous_Function.thy
author hoelzl
Mon Aug 08 14:13:14 2016 +0200 (2016-08-08)
changeset 63627 6ddb43c6b711
parent 63594 src/HOL/Multivariate_Analysis/Bounded_Continuous_Function.thy@bd218a9320b5
child 64267 b9a1486e79be
permissions -rw-r--r--
rename HOL-Multivariate_Analysis to HOL-Analysis.
wenzelm@60420
     1
section \<open>Bounded Continuous Functions\<close>
wenzelm@60421
     2
hoelzl@59453
     3
theory Bounded_Continuous_Function
hoelzl@63594
     4
imports Henstock_Kurzweil_Integration
hoelzl@59453
     5
begin
hoelzl@59453
     6
wenzelm@60421
     7
subsection \<open>Definition\<close>
hoelzl@59453
     8
wenzelm@60421
     9
definition bcontfun :: "('a::topological_space \<Rightarrow> 'b::metric_space) set"
wenzelm@60421
    10
  where "bcontfun = {f. continuous_on UNIV f \<and> bounded (range f)}"
hoelzl@59453
    11
wenzelm@61260
    12
typedef (overloaded) ('a, 'b) bcontfun =
wenzelm@61260
    13
    "bcontfun :: ('a::topological_space \<Rightarrow> 'b::metric_space) set"
hoelzl@59453
    14
  by (auto simp: bcontfun_def intro: continuous_intros simp: bounded_def)
hoelzl@59453
    15
hoelzl@59453
    16
lemma bcontfunE:
hoelzl@59453
    17
  assumes "f \<in> bcontfun"
hoelzl@59453
    18
  obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) u \<le> y"
hoelzl@59453
    19
  using assms unfolding bcontfun_def
hoelzl@59453
    20
  by (metis (lifting) bounded_any_center dist_commute mem_Collect_eq rangeI)
hoelzl@59453
    21
hoelzl@59453
    22
lemma bcontfunE':
hoelzl@59453
    23
  assumes "f \<in> bcontfun"
hoelzl@59453
    24
  obtains y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y"
hoelzl@59453
    25
  using assms bcontfunE
hoelzl@59453
    26
  by metis
hoelzl@59453
    27
wenzelm@60421
    28
lemma bcontfunI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) u \<le> b) \<Longrightarrow> f \<in> bcontfun"
hoelzl@59453
    29
  unfolding bcontfun_def
hoelzl@59453
    30
  by (metis (lifting, no_types) bounded_def dist_commute mem_Collect_eq rangeE)
hoelzl@59453
    31
wenzelm@60421
    32
lemma bcontfunI': "continuous_on UNIV f \<Longrightarrow> (\<And>x. dist (f x) undefined \<le> b) \<Longrightarrow> f \<in> bcontfun"
hoelzl@59453
    33
  using bcontfunI by metis
hoelzl@59453
    34
hoelzl@59453
    35
lemma continuous_on_Rep_bcontfun[intro, simp]: "continuous_on T (Rep_bcontfun x)"
hoelzl@59453
    36
  using Rep_bcontfun[of x]
hoelzl@59453
    37
  by (auto simp: bcontfun_def intro: continuous_on_subset)
hoelzl@59453
    38
hoelzl@62101
    39
(* TODO: Generalize to uniform spaces? *)
hoelzl@59453
    40
instantiation bcontfun :: (topological_space, metric_space) metric_space
hoelzl@59453
    41
begin
hoelzl@59453
    42
wenzelm@60421
    43
definition dist_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> ('a, 'b) bcontfun \<Rightarrow> real"
wenzelm@60421
    44
  where "dist_bcontfun f g = (SUP x. dist (Rep_bcontfun f x) (Rep_bcontfun g x))"
hoelzl@59453
    45
hoelzl@62101
    46
definition uniformity_bcontfun :: "(('a, 'b) bcontfun \<times> ('a, 'b) bcontfun) filter"
hoelzl@62101
    47
  where "uniformity_bcontfun = (INF e:{0 <..}. principal {(x, y). dist x y < e})"
hoelzl@62101
    48
wenzelm@60421
    49
definition open_bcontfun :: "('a, 'b) bcontfun set \<Rightarrow> bool"
hoelzl@62101
    50
  where "open_bcontfun S = (\<forall>x\<in>S. \<forall>\<^sub>F (x', y) in uniformity. x' = x \<longrightarrow> y \<in> S)"
hoelzl@59453
    51
hoelzl@59453
    52
lemma dist_bounded:
wenzelm@60421
    53
  fixes f :: "('a, 'b) bcontfun"
hoelzl@59453
    54
  shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
hoelzl@59453
    55
proof -
wenzelm@60421
    56
  have "Rep_bcontfun f \<in> bcontfun" by (rule Rep_bcontfun)
hoelzl@59453
    57
  from bcontfunE'[OF this] obtain y where y:
hoelzl@59453
    58
    "continuous_on UNIV (Rep_bcontfun f)"
hoelzl@59453
    59
    "\<And>x. dist (Rep_bcontfun f x) undefined \<le> y"
hoelzl@59453
    60
    by auto
wenzelm@60421
    61
  have "Rep_bcontfun g \<in> bcontfun" by (rule Rep_bcontfun)
hoelzl@59453
    62
  from bcontfunE'[OF this] obtain z where z:
hoelzl@59453
    63
    "continuous_on UNIV (Rep_bcontfun g)"
hoelzl@59453
    64
    "\<And>x. dist (Rep_bcontfun g x) undefined \<le> z"
hoelzl@59453
    65
    by auto
wenzelm@60421
    66
  show ?thesis
wenzelm@60421
    67
    unfolding dist_bcontfun_def
hoelzl@59453
    68
  proof (intro cSUP_upper bdd_aboveI2)
hoelzl@59453
    69
    fix x
wenzelm@60421
    70
    have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le>
wenzelm@60421
    71
      dist (Rep_bcontfun f x) undefined + dist (Rep_bcontfun g x) undefined"
hoelzl@59453
    72
      by (rule dist_triangle2)
wenzelm@60421
    73
    also have "\<dots> \<le> y + z"
wenzelm@60421
    74
      using y(2)[of x] z(2)[of x] by (rule add_mono)
hoelzl@59453
    75
    finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> y + z" .
hoelzl@59453
    76
  qed simp
hoelzl@59453
    77
qed
hoelzl@59453
    78
hoelzl@59453
    79
lemma dist_bound:
wenzelm@60421
    80
  fixes f :: "('a, 'b) bcontfun"
hoelzl@59453
    81
  assumes "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> b"
hoelzl@59453
    82
  shows "dist f g \<le> b"
hoelzl@59453
    83
  using assms by (auto simp: dist_bcontfun_def intro: cSUP_least)
hoelzl@59453
    84
hoelzl@59453
    85
lemma dist_bounded_Abs:
wenzelm@60421
    86
  fixes f g :: "'a \<Rightarrow> 'b"
hoelzl@59453
    87
  assumes "f \<in> bcontfun" "g \<in> bcontfun"
hoelzl@59453
    88
  shows "dist (f x) (g x) \<le> dist (Abs_bcontfun f) (Abs_bcontfun g)"
hoelzl@59453
    89
  by (metis Abs_bcontfun_inverse assms dist_bounded)
hoelzl@59453
    90
hoelzl@59453
    91
lemma const_bcontfun: "(\<lambda>x::'a. b::'b) \<in> bcontfun"
hoelzl@59453
    92
  by (auto intro: bcontfunI continuous_on_const)
hoelzl@59453
    93
hoelzl@59453
    94
lemma dist_fun_lt_imp_dist_val_lt:
hoelzl@59453
    95
  assumes "dist f g < e"
hoelzl@59453
    96
  shows "dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
hoelzl@59453
    97
  using dist_bounded assms by (rule le_less_trans)
hoelzl@59453
    98
hoelzl@59453
    99
lemma dist_val_lt_imp_dist_fun_le:
hoelzl@59453
   100
  assumes "\<forall>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) < e"
hoelzl@59453
   101
  shows "dist f g \<le> e"
wenzelm@60421
   102
  unfolding dist_bcontfun_def
hoelzl@59453
   103
proof (intro cSUP_least)
hoelzl@59453
   104
  fix x
hoelzl@59453
   105
  show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> e"
hoelzl@59453
   106
    using assms[THEN spec[where x=x]] by (simp add: dist_norm)
wenzelm@60421
   107
qed simp
hoelzl@59453
   108
hoelzl@59453
   109
instance
hoelzl@59453
   110
proof
wenzelm@60421
   111
  fix f g h :: "('a, 'b) bcontfun"
hoelzl@59453
   112
  show "dist f g = 0 \<longleftrightarrow> f = g"
hoelzl@59453
   113
  proof
wenzelm@60421
   114
    have "\<And>x. dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f g"
wenzelm@60421
   115
      by (rule dist_bounded)
hoelzl@59453
   116
    also assume "dist f g = 0"
wenzelm@60421
   117
    finally show "f = g"
wenzelm@60421
   118
      by (auto simp: Rep_bcontfun_inject[symmetric] Abs_bcontfun_inverse)
haftmann@62343
   119
  qed (auto simp: dist_bcontfun_def intro!: cSup_eq)
hoelzl@59453
   120
  show "dist f g \<le> dist f h + dist g h"
hoelzl@59453
   121
  proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
hoelzl@59453
   122
    fix x
hoelzl@59453
   123
    have "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le>
hoelzl@59453
   124
      dist (Rep_bcontfun f x) (Rep_bcontfun h x) + dist (Rep_bcontfun g x) (Rep_bcontfun h x)"
hoelzl@59453
   125
      by (rule dist_triangle2)
wenzelm@60421
   126
    also have "dist (Rep_bcontfun f x) (Rep_bcontfun h x) \<le> dist f h"
wenzelm@60421
   127
      by (rule dist_bounded)
wenzelm@60421
   128
    also have "dist (Rep_bcontfun g x) (Rep_bcontfun h x) \<le> dist g h"
wenzelm@60421
   129
      by (rule dist_bounded)
wenzelm@60421
   130
    finally show "dist (Rep_bcontfun f x) (Rep_bcontfun g x) \<le> dist f h + dist g h"
wenzelm@60421
   131
      by simp
hoelzl@59453
   132
  qed
hoelzl@62101
   133
qed (rule open_bcontfun_def uniformity_bcontfun_def)+
wenzelm@60421
   134
hoelzl@59453
   135
end
hoelzl@59453
   136
hoelzl@59453
   137
lemma closed_Pi_bcontfun:
wenzelm@60421
   138
  fixes I :: "'a::metric_space set"
wenzelm@60421
   139
    and X :: "'a \<Rightarrow> 'b::complete_space set"
hoelzl@59453
   140
  assumes "\<And>i. i \<in> I \<Longrightarrow> closed (X i)"
hoelzl@59453
   141
  shows "closed (Abs_bcontfun ` (Pi I X \<inter> bcontfun))"
hoelzl@59453
   142
  unfolding closed_sequential_limits
hoelzl@59453
   143
proof safe
hoelzl@59453
   144
  fix f l
wenzelm@61969
   145
  assume seq: "\<forall>n. f n \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)" and lim: "f \<longlonglongrightarrow> l"
hoelzl@59453
   146
  have lim_fun: "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (Rep_bcontfun l x) < e"
hoelzl@59453
   147
    using LIMSEQ_imp_Cauchy[OF lim, simplified Cauchy_def] metric_LIMSEQ_D[OF lim]
wenzelm@60421
   148
    by (intro uniformly_cauchy_imp_uniformly_convergent[where P="\<lambda>_. True", simplified])
hoelzl@59453
   149
      (metis dist_fun_lt_imp_dist_val_lt)+
hoelzl@59453
   150
  show "l \<in> Abs_bcontfun ` (Pi I X \<inter> bcontfun)"
hoelzl@59453
   151
  proof (rule, safe)
hoelzl@59453
   152
    fix x assume "x \<in> I"
wenzelm@60421
   153
    then have "closed (X x)"
wenzelm@60421
   154
      using assms by simp
hoelzl@59453
   155
    moreover have "eventually (\<lambda>xa. Rep_bcontfun (f xa) x \<in> X x) sequentially"
hoelzl@59453
   156
    proof (rule always_eventually, safe)
hoelzl@59453
   157
      fix i
wenzelm@60420
   158
      from seq[THEN spec, of i] \<open>x \<in> I\<close>
hoelzl@59453
   159
      show "Rep_bcontfun (f i) x \<in> X x"
hoelzl@59453
   160
        by (auto simp: Abs_bcontfun_inverse)
hoelzl@59453
   161
    qed
hoelzl@59453
   162
    moreover note sequentially_bot
wenzelm@61969
   163
    moreover have "(\<lambda>n. Rep_bcontfun (f n) x) \<longlonglongrightarrow> Rep_bcontfun l x"
hoelzl@59453
   164
      using lim_fun by (blast intro!: metric_LIMSEQ_I)
hoelzl@59453
   165
    ultimately show "Rep_bcontfun l x \<in> X x"
hoelzl@59453
   166
      by (rule Lim_in_closed_set)
hoelzl@59453
   167
  qed (auto simp: Rep_bcontfun Rep_bcontfun_inverse)
hoelzl@59453
   168
qed
hoelzl@59453
   169
wenzelm@60421
   170
wenzelm@60420
   171
subsection \<open>Complete Space\<close>
hoelzl@59453
   172
hoelzl@59453
   173
instance bcontfun :: (metric_space, complete_space) complete_space
hoelzl@59453
   174
proof
wenzelm@60421
   175
  fix f :: "nat \<Rightarrow> ('a, 'b) bcontfun"
wenzelm@61808
   176
  assume "Cauchy f"  \<comment> \<open>Cauchy equals uniform convergence\<close>
hoelzl@59453
   177
  then obtain g where limit_function:
hoelzl@59453
   178
    "\<forall>e>0. \<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e"
hoelzl@59453
   179
    using uniformly_convergent_eq_cauchy[of "\<lambda>_. True"
hoelzl@59453
   180
      "\<lambda>n. Rep_bcontfun (f n)"]
wenzelm@60421
   181
    unfolding Cauchy_def
wenzelm@60421
   182
    by (metis dist_fun_lt_imp_dist_val_lt)
hoelzl@59453
   183
wenzelm@61808
   184
  then obtain N where fg_dist:  \<comment> \<open>for an upper bound on @{term g}\<close>
hoelzl@59453
   185
    "\<forall>n\<ge>N. \<forall>x. dist (g x) ( Rep_bcontfun (f n) x) < 1"
hoelzl@59453
   186
    by (force simp add: dist_commute)
hoelzl@59453
   187
  from bcontfunE'[OF Rep_bcontfun, of "f N"] obtain b where
wenzelm@60421
   188
    f_bound: "\<forall>x. dist (Rep_bcontfun (f N) x) undefined \<le> b"
wenzelm@60421
   189
    by force
wenzelm@61808
   190
  have "g \<in> bcontfun"  \<comment> \<open>The limit function is bounded and continuous\<close>
hoelzl@59453
   191
  proof (intro bcontfunI)
hoelzl@59453
   192
    show "continuous_on UNIV g"
hoelzl@59453
   193
      using bcontfunE[OF Rep_bcontfun] limit_function
wenzelm@60421
   194
      by (intro continuous_uniform_limit[where f="\<lambda>n. Rep_bcontfun (f n)" and F="sequentially"])
wenzelm@60421
   195
        (auto simp add: eventually_sequentially trivial_limit_def dist_norm)
hoelzl@59453
   196
  next
hoelzl@59453
   197
    fix x
hoelzl@59453
   198
    from fg_dist have "dist (g x) (Rep_bcontfun (f N) x) < 1"
hoelzl@59453
   199
      by (simp add: dist_norm norm_minus_commute)
hoelzl@59453
   200
    with dist_triangle[of "g x" undefined "Rep_bcontfun (f N) x"]
hoelzl@59453
   201
    show "dist (g x) undefined \<le> 1 + b" using f_bound[THEN spec, of x]
hoelzl@59453
   202
      by simp
hoelzl@59453
   203
  qed
hoelzl@59453
   204
  show "convergent f"
lp15@60017
   205
  proof (rule convergentI, subst lim_sequentially, safe)
wenzelm@61808
   206
    \<comment> \<open>The limit function converges according to its norm\<close>
wenzelm@60421
   207
    fix e :: real
wenzelm@60421
   208
    assume "e > 0"
wenzelm@60421
   209
    then have "e/2 > 0" by simp
hoelzl@59453
   210
    with limit_function[THEN spec, of"e/2"]
hoelzl@59453
   211
    have "\<exists>N. \<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e/2"
hoelzl@59453
   212
      by simp
hoelzl@59453
   213
    then obtain N where N: "\<forall>n\<ge>N. \<forall>x. dist (Rep_bcontfun (f n) x) (g x) < e / 2" by auto
hoelzl@59453
   214
    show "\<exists>N. \<forall>n\<ge>N. dist (f n) (Abs_bcontfun g) < e"
hoelzl@59453
   215
    proof (rule, safe)
hoelzl@59453
   216
      fix n
hoelzl@59453
   217
      assume "N \<le> n"
hoelzl@59453
   218
      with N show "dist (f n) (Abs_bcontfun g) < e"
hoelzl@59453
   219
        using dist_val_lt_imp_dist_fun_le[of
hoelzl@59453
   220
          "f n" "Abs_bcontfun g" "e/2"]
wenzelm@60420
   221
          Abs_bcontfun_inverse[OF \<open>g \<in> bcontfun\<close>] \<open>e > 0\<close> by simp
hoelzl@59453
   222
    qed
hoelzl@59453
   223
  qed
hoelzl@59453
   224
qed
hoelzl@59453
   225
wenzelm@60421
   226
wenzelm@60421
   227
subsection \<open>Supremum norm for a normed vector space\<close>
hoelzl@59453
   228
hoelzl@59453
   229
instantiation bcontfun :: (topological_space, real_normed_vector) real_vector
hoelzl@59453
   230
begin
hoelzl@59453
   231
hoelzl@59453
   232
definition "-f = Abs_bcontfun (\<lambda>x. -(Rep_bcontfun f x))"
hoelzl@59453
   233
hoelzl@59453
   234
definition "f + g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x + Rep_bcontfun g x)"
hoelzl@59453
   235
hoelzl@59453
   236
definition "f - g = Abs_bcontfun (\<lambda>x. Rep_bcontfun f x - Rep_bcontfun g x)"
hoelzl@59453
   237
hoelzl@59453
   238
definition "0 = Abs_bcontfun (\<lambda>x. 0)"
hoelzl@59453
   239
hoelzl@59453
   240
definition "scaleR r f = Abs_bcontfun (\<lambda>x. r *\<^sub>R Rep_bcontfun f x)"
hoelzl@59453
   241
hoelzl@59453
   242
lemma plus_cont:
wenzelm@60421
   243
  fixes f g :: "'a \<Rightarrow> 'b"
wenzelm@60421
   244
  assumes f: "f \<in> bcontfun"
wenzelm@60421
   245
    and g: "g \<in> bcontfun"
hoelzl@59453
   246
  shows "(\<lambda>x. f x + g x) \<in> bcontfun"
hoelzl@59453
   247
proof -
hoelzl@59453
   248
  from bcontfunE'[OF f] obtain y where "continuous_on UNIV f" "\<And>x. dist (f x) undefined \<le> y"
hoelzl@59453
   249
    by auto
hoelzl@59453
   250
  moreover
hoelzl@59453
   251
  from bcontfunE'[OF g] obtain z where "continuous_on UNIV g" "\<And>x. dist (g x) undefined \<le> z"
hoelzl@59453
   252
    by auto
hoelzl@59453
   253
  ultimately show ?thesis
hoelzl@59453
   254
  proof (intro bcontfunI)
hoelzl@59453
   255
    fix x
wenzelm@60421
   256
    have "dist (f x + g x) 0 = dist (f x + g x) (0 + 0)"
wenzelm@60421
   257
      by simp
wenzelm@60421
   258
    also have "\<dots> \<le> dist (f x) 0 + dist (g x) 0"
wenzelm@60421
   259
      by (rule dist_triangle_add)
hoelzl@59453
   260
    also have "\<dots> \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0"
hoelzl@59453
   261
      unfolding zero_bcontfun_def using assms
lp15@62379
   262
      by (metis add_mono const_bcontfun dist_bounded_Abs)
wenzelm@60421
   263
    finally show "dist (f x + g x) 0 \<le> dist (Abs_bcontfun f) 0 + dist (Abs_bcontfun g) 0" .
hoelzl@59453
   264
  qed (simp add: continuous_on_add)
hoelzl@59453
   265
qed
hoelzl@59453
   266
hoelzl@59453
   267
lemma Rep_bcontfun_plus[simp]: "Rep_bcontfun (f + g) x = Rep_bcontfun f x + Rep_bcontfun g x"
hoelzl@59453
   268
  by (simp add: plus_bcontfun_def Abs_bcontfun_inverse plus_cont Rep_bcontfun)
hoelzl@59453
   269
hoelzl@59453
   270
lemma uminus_cont:
wenzelm@60421
   271
  fixes f :: "'a \<Rightarrow> 'b"
hoelzl@59453
   272
  assumes "f \<in> bcontfun"
hoelzl@59453
   273
  shows "(\<lambda>x. - f x) \<in> bcontfun"
hoelzl@59453
   274
proof -
wenzelm@60421
   275
  from bcontfunE[OF assms, of 0] obtain y
wenzelm@60421
   276
    where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
hoelzl@59453
   277
    by auto
wenzelm@60421
   278
  then show ?thesis
hoelzl@59453
   279
  proof (intro bcontfunI)
hoelzl@59453
   280
    fix x
hoelzl@59453
   281
    assume "\<And>x. dist (f x) 0 \<le> y"
wenzelm@60421
   282
    then show "dist (- f x) 0 \<le> y"
wenzelm@60421
   283
      by (subst dist_minus[symmetric]) simp
hoelzl@59453
   284
  qed (simp add: continuous_on_minus)
hoelzl@59453
   285
qed
hoelzl@59453
   286
wenzelm@60421
   287
lemma Rep_bcontfun_uminus[simp]: "Rep_bcontfun (- f) x = - Rep_bcontfun f x"
hoelzl@59453
   288
  by (simp add: uminus_bcontfun_def Abs_bcontfun_inverse uminus_cont Rep_bcontfun)
hoelzl@59453
   289
hoelzl@59453
   290
lemma minus_cont:
wenzelm@60421
   291
  fixes f g :: "'a \<Rightarrow> 'b"
wenzelm@60421
   292
  assumes f: "f \<in> bcontfun"
wenzelm@60421
   293
    and g: "g \<in> bcontfun"
hoelzl@59453
   294
  shows "(\<lambda>x. f x - g x) \<in> bcontfun"
wenzelm@60421
   295
  using plus_cont [of f "- g"] assms
wenzelm@60421
   296
  by (simp add: uminus_cont fun_Compl_def)
hoelzl@59453
   297
wenzelm@60421
   298
lemma Rep_bcontfun_minus[simp]: "Rep_bcontfun (f - g) x = Rep_bcontfun f x - Rep_bcontfun g x"
hoelzl@59453
   299
  by (simp add: minus_bcontfun_def Abs_bcontfun_inverse minus_cont Rep_bcontfun)
hoelzl@59453
   300
hoelzl@59453
   301
lemma scaleR_cont:
wenzelm@60421
   302
  fixes a :: real
wenzelm@60421
   303
    and f :: "'a \<Rightarrow> 'b"
hoelzl@59453
   304
  assumes "f \<in> bcontfun"
hoelzl@59453
   305
  shows " (\<lambda>x. a *\<^sub>R f x) \<in> bcontfun"
hoelzl@59453
   306
proof -
wenzelm@60421
   307
  from bcontfunE[OF assms, of 0] obtain y
wenzelm@60421
   308
    where "continuous_on UNIV f" "\<And>x. dist (f x) 0 \<le> y"
hoelzl@59453
   309
    by auto
wenzelm@60421
   310
  then show ?thesis
hoelzl@59453
   311
  proof (intro bcontfunI)
wenzelm@60421
   312
    fix x
wenzelm@60421
   313
    assume "\<And>x. dist (f x) 0 \<le> y"
wenzelm@61945
   314
    then show "dist (a *\<^sub>R f x) 0 \<le> \<bar>a\<bar> * y"
haftmann@59554
   315
      by (metis norm_cmul_rule_thm norm_conv_dist)
hoelzl@59453
   316
  qed (simp add: continuous_intros)
hoelzl@59453
   317
qed
hoelzl@59453
   318
wenzelm@60421
   319
lemma Rep_bcontfun_scaleR[simp]: "Rep_bcontfun (a *\<^sub>R g) x = a *\<^sub>R Rep_bcontfun g x"
hoelzl@59453
   320
  by (simp add: scaleR_bcontfun_def Abs_bcontfun_inverse scaleR_cont Rep_bcontfun)
hoelzl@59453
   321
hoelzl@59453
   322
instance
wenzelm@61169
   323
  by standard
wenzelm@60421
   324
    (simp_all add: plus_bcontfun_def zero_bcontfun_def minus_bcontfun_def scaleR_bcontfun_def
wenzelm@60421
   325
      Abs_bcontfun_inverse Rep_bcontfun_inverse Rep_bcontfun algebra_simps
wenzelm@60421
   326
      plus_cont const_bcontfun minus_cont scaleR_cont)
wenzelm@60421
   327
hoelzl@59453
   328
end
hoelzl@59453
   329
hoelzl@59453
   330
instantiation bcontfun :: (topological_space, real_normed_vector) real_normed_vector
hoelzl@59453
   331
begin
hoelzl@59453
   332
wenzelm@60421
   333
definition norm_bcontfun :: "('a, 'b) bcontfun \<Rightarrow> real"
wenzelm@60421
   334
  where "norm_bcontfun f = dist f 0"
hoelzl@59453
   335
hoelzl@59453
   336
definition "sgn (f::('a,'b) bcontfun) = f /\<^sub>R norm f"
hoelzl@59453
   337
hoelzl@59453
   338
instance
hoelzl@59453
   339
proof
wenzelm@60421
   340
  fix a :: real
wenzelm@60421
   341
  fix f g :: "('a, 'b) bcontfun"
hoelzl@59453
   342
  show "dist f g = norm (f - g)"
hoelzl@59453
   343
    by (simp add: norm_bcontfun_def dist_bcontfun_def zero_bcontfun_def
lp15@62379
   344
      Abs_bcontfun_inverse const_bcontfun dist_norm)
hoelzl@59453
   345
  show "norm (f + g) \<le> norm f + norm g"
hoelzl@59453
   346
    unfolding norm_bcontfun_def
hoelzl@59453
   347
  proof (subst dist_bcontfun_def, safe intro!: cSUP_least)
hoelzl@59453
   348
    fix x
hoelzl@59453
   349
    have "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le>
hoelzl@59453
   350
      dist (Rep_bcontfun f x) 0 + dist (Rep_bcontfun g x) 0"
hoelzl@59453
   351
      by (metis (hide_lams, no_types) Rep_bcontfun_minus Rep_bcontfun_plus diff_0_right dist_norm
hoelzl@59453
   352
        le_less_linear less_irrefl norm_triangle_lt)
hoelzl@59453
   353
    also have "dist (Rep_bcontfun f x) 0 \<le> dist f 0"
hoelzl@59453
   354
      using dist_bounded[of f x 0]
hoelzl@59453
   355
      by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
hoelzl@59453
   356
    also have "dist (Rep_bcontfun g x) 0 \<le> dist g 0" using dist_bounded[of g x 0]
hoelzl@59453
   357
      by (simp add: Abs_bcontfun_inverse const_bcontfun zero_bcontfun_def)
hoelzl@59453
   358
    finally show "dist (Rep_bcontfun (f + g) x) (Rep_bcontfun 0 x) \<le> dist f 0 + dist g 0" by simp
hoelzl@59453
   359
  qed
hoelzl@59453
   360
  show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
hoelzl@59453
   361
  proof -
hoelzl@59453
   362
    have "\<bar>a\<bar> * Sup (range (\<lambda>x. dist (Rep_bcontfun f x) 0)) =
hoelzl@59453
   363
      (SUP i:range (\<lambda>x. dist (Rep_bcontfun f x) 0). \<bar>a\<bar> * i)"
hoelzl@59453
   364
    proof (intro continuous_at_Sup_mono bdd_aboveI2)
hoelzl@59453
   365
      fix x
hoelzl@59453
   366
      show "dist (Rep_bcontfun f x) 0 \<le> norm f" using dist_bounded[of f x 0]
lp15@62379
   367
        by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
hoelzl@59453
   368
          const_bcontfun)
hoelzl@59453
   369
    qed (auto intro!: monoI mult_left_mono continuous_intros)
hoelzl@59453
   370
    moreover
wenzelm@60421
   371
    have "range (\<lambda>x. dist (Rep_bcontfun (a *\<^sub>R f) x) 0) =
hoelzl@59453
   372
      (\<lambda>x. \<bar>a\<bar> * x) ` (range (\<lambda>x. dist (Rep_bcontfun f x) 0))"
lp15@62379
   373
      by auto
hoelzl@59453
   374
    ultimately
hoelzl@59453
   375
    show "norm (a *\<^sub>R f) = \<bar>a\<bar> * norm f"
lp15@62379
   376
      by (simp add: norm_bcontfun_def dist_bcontfun_def Abs_bcontfun_inverse
lp15@62379
   377
        zero_bcontfun_def const_bcontfun image_image)
hoelzl@59453
   378
  qed
hoelzl@59453
   379
qed (auto simp: norm_bcontfun_def sgn_bcontfun_def)
hoelzl@59453
   380
hoelzl@59453
   381
end
hoelzl@59453
   382
wenzelm@60421
   383
lemma bcontfun_normI: "continuous_on UNIV f \<Longrightarrow> (\<And>x. norm (f x) \<le> b) \<Longrightarrow> f \<in> bcontfun"
lp15@62379
   384
  by (metis bcontfunI dist_0_norm dist_commute)
hoelzl@59453
   385
hoelzl@59453
   386
lemma norm_bounded:
wenzelm@60421
   387
  fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
hoelzl@59453
   388
  shows "norm (Rep_bcontfun f x) \<le> norm f"
hoelzl@59453
   389
  using dist_bounded[of f x 0]
lp15@62379
   390
  by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def
hoelzl@59453
   391
    const_bcontfun)
hoelzl@59453
   392
hoelzl@59453
   393
lemma norm_bound:
wenzelm@60421
   394
  fixes f :: "('a::topological_space, 'b::real_normed_vector) bcontfun"
hoelzl@59453
   395
  assumes "\<And>x. norm (Rep_bcontfun f x) \<le> b"
hoelzl@59453
   396
  shows "norm f \<le> b"
hoelzl@59453
   397
  using dist_bound[of f 0 b] assms
lp15@62379
   398
  by (simp add: norm_bcontfun_def Abs_bcontfun_inverse zero_bcontfun_def const_bcontfun)
hoelzl@59453
   399
hoelzl@59453
   400
wenzelm@60421
   401
subsection \<open>Continuously Extended Functions\<close>
wenzelm@60421
   402
wenzelm@60421
   403
definition clamp :: "'a::euclidean_space \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'a" where
hoelzl@59453
   404
  "clamp a b x = (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i)"
hoelzl@59453
   405
wenzelm@60421
   406
definition ext_cont :: "('a::euclidean_space \<Rightarrow> 'b::real_normed_vector) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> ('a, 'b) bcontfun"
hoelzl@59453
   407
  where "ext_cont f a b = Abs_bcontfun ((\<lambda>x. f (clamp a b x)))"
hoelzl@59453
   408
hoelzl@59453
   409
lemma ext_cont_def':
hoelzl@59453
   410
  "ext_cont f a b = Abs_bcontfun (\<lambda>x.
hoelzl@59453
   411
    f (\<Sum>i\<in>Basis. (if x\<bullet>i < a\<bullet>i then a\<bullet>i else if x\<bullet>i \<le> b\<bullet>i then x\<bullet>i else b\<bullet>i) *\<^sub>R i))"
wenzelm@60421
   412
  unfolding ext_cont_def clamp_def ..
hoelzl@59453
   413
hoelzl@59453
   414
lemma clamp_in_interval:
hoelzl@59453
   415
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
hoelzl@59453
   416
  shows "clamp a b x \<in> cbox a b"
hoelzl@59453
   417
  unfolding clamp_def
hoelzl@59453
   418
  using box_ne_empty(1)[of a b] assms by (auto simp: cbox_def)
hoelzl@59453
   419
hoelzl@59453
   420
lemma dist_clamps_le_dist_args:
wenzelm@60421
   421
  fixes x :: "'a::euclidean_space"
hoelzl@59453
   422
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
hoelzl@59453
   423
  shows "dist (clamp a b y) (clamp a b x) \<le> dist y x"
hoelzl@59453
   424
proof -
wenzelm@60421
   425
  from box_ne_empty(1)[of a b] assms have "(\<forall>i\<in>Basis. a \<bullet> i \<le> b \<bullet> i)"
wenzelm@60421
   426
    by (simp add: cbox_def)
wenzelm@60421
   427
  then have "(\<Sum>i\<in>Basis. (dist (clamp a b y \<bullet> i) (clamp a b x \<bullet> i))\<^sup>2) \<le>
wenzelm@60421
   428
    (\<Sum>i\<in>Basis. (dist (y \<bullet> i) (x \<bullet> i))\<^sup>2)"
wenzelm@60421
   429
    by (auto intro!: setsum_mono simp: clamp_def dist_real_def abs_le_square_iff[symmetric])
wenzelm@60421
   430
  then show ?thesis
wenzelm@60421
   431
    by (auto intro: real_sqrt_le_mono
wenzelm@60421
   432
      simp: euclidean_dist_l2[where y=x] euclidean_dist_l2[where y="clamp a b x"] setL2_def)
hoelzl@59453
   433
qed
hoelzl@59453
   434
hoelzl@59453
   435
lemma clamp_continuous_at:
wenzelm@60421
   436
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
wenzelm@60421
   437
    and x :: 'a
hoelzl@59453
   438
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
wenzelm@60421
   439
    and f_cont: "continuous_on (cbox a b) f"
hoelzl@59453
   440
  shows "continuous (at x) (\<lambda>x. f (clamp a b x))"
wenzelm@60421
   441
  unfolding continuous_at_eps_delta
wenzelm@60421
   442
proof safe
wenzelm@60421
   443
  fix x :: 'a
wenzelm@60421
   444
  fix e :: real
wenzelm@60421
   445
  assume "e > 0"
wenzelm@60421
   446
  moreover have "clamp a b x \<in> cbox a b"
wenzelm@60421
   447
    by (simp add: clamp_in_interval assms)
wenzelm@60421
   448
  moreover note f_cont[simplified continuous_on_iff]
hoelzl@59453
   449
  ultimately
hoelzl@59453
   450
  obtain d where d: "0 < d"
hoelzl@59453
   451
    "\<And>x'. x' \<in> cbox a b \<Longrightarrow> dist x' (clamp a b x) < d \<Longrightarrow> dist (f x') (f (clamp a b x)) < e"
hoelzl@59453
   452
    by force
hoelzl@59453
   453
  show "\<exists>d>0. \<forall>x'. dist x' x < d \<longrightarrow>
hoelzl@59453
   454
    dist (f (clamp a b x')) (f (clamp a b x)) < e"
hoelzl@59453
   455
    by (auto intro!: d clamp_in_interval assms dist_clamps_le_dist_args[THEN le_less_trans])
hoelzl@59453
   456
qed
hoelzl@59453
   457
hoelzl@59453
   458
lemma clamp_continuous_on:
wenzelm@60421
   459
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::metric_space"
hoelzl@59453
   460
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
wenzelm@60421
   461
    and f_cont: "continuous_on (cbox a b) f"
hoelzl@59453
   462
  shows "continuous_on UNIV (\<lambda>x. f (clamp a b x))"
hoelzl@59453
   463
  using assms
hoelzl@59453
   464
  by (auto intro: continuous_at_imp_continuous_on clamp_continuous_at)
hoelzl@59453
   465
hoelzl@59453
   466
lemma clamp_bcontfun:
wenzelm@60421
   467
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
hoelzl@59453
   468
  assumes "\<And>i. i \<in> Basis \<Longrightarrow> a \<bullet> i \<le> b \<bullet> i"
wenzelm@60421
   469
    and continuous: "continuous_on (cbox a b) f"
hoelzl@59453
   470
  shows "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
hoelzl@59453
   471
proof -
wenzelm@60421
   472
  have "bounded (f ` (cbox a b))"
wenzelm@60421
   473
    by (rule compact_continuous_image[OF continuous compact_cbox[of a b], THEN compact_imp_bounded])
wenzelm@60421
   474
  then obtain c where f_bound: "\<forall>x\<in>f ` cbox a b. norm x \<le> c"
wenzelm@60421
   475
    by (auto simp add: bounded_pos)
hoelzl@59453
   476
  show "(\<lambda>x. f (clamp a b x)) \<in> bcontfun"
hoelzl@59453
   477
  proof (intro bcontfun_normI)
hoelzl@59453
   478
    fix x
wenzelm@60421
   479
    show "norm (f (clamp a b x)) \<le> c"
wenzelm@60421
   480
      using clamp_in_interval[OF assms(1), of x] f_bound
wenzelm@60421
   481
      by (simp add: ext_cont_def)
hoelzl@59453
   482
  qed (simp add: clamp_continuous_on assms)
hoelzl@59453
   483
qed
hoelzl@59453
   484
hoelzl@59453
   485
lemma integral_clamp:
hoelzl@59453
   486
  "integral {t0::real..clamp t0 t1 x} f =
hoelzl@59453
   487
    (if x < t0 then 0 else if x \<le> t1 then integral {t0..x} f else integral {t0..t1} f)"
hoelzl@59453
   488
  by (auto simp: clamp_def)
hoelzl@59453
   489
hoelzl@59453
   490
hoelzl@59453
   491
declare [[coercion Rep_bcontfun]]
hoelzl@59453
   492
hoelzl@59453
   493
lemma ext_cont_cancel[simp]:
wenzelm@60421
   494
  fixes x a b :: "'a::euclidean_space"
hoelzl@59453
   495
  assumes x: "x \<in> cbox a b"
wenzelm@60421
   496
    and "continuous_on (cbox a b) f"
hoelzl@59453
   497
  shows "ext_cont f a b x = f x"
hoelzl@59453
   498
  using assms
hoelzl@59453
   499
  unfolding ext_cont_def
hoelzl@59453
   500
proof (subst Abs_bcontfun_inverse[OF clamp_bcontfun])
hoelzl@59453
   501
  show "f (clamp a b x) = f x"
hoelzl@59453
   502
    using x unfolding clamp_def mem_box
hoelzl@59453
   503
    by (intro arg_cong[where f=f] euclidean_eqI[where 'a='a]) (simp add: not_less)
hoelzl@59453
   504
qed (auto simp: cbox_def)
hoelzl@59453
   505
hoelzl@59453
   506
lemma ext_cont_cong:
hoelzl@59453
   507
  assumes "t0 = s0"
wenzelm@60421
   508
    and "t1 = s1"
wenzelm@60421
   509
    and "\<And>t. t \<in> (cbox t0 t1) \<Longrightarrow> f t = g t"
wenzelm@60421
   510
    and "continuous_on (cbox t0 t1) f"
wenzelm@60421
   511
    and "continuous_on (cbox s0 s1) g"
wenzelm@60421
   512
    and ord: "\<And>i. i \<in> Basis \<Longrightarrow> t0 \<bullet> i \<le> t1 \<bullet> i"
hoelzl@59453
   513
  shows "ext_cont f t0 t1 = ext_cont g s0 s1"
hoelzl@59453
   514
  unfolding assms ext_cont_def
hoelzl@59453
   515
  using assms clamp_in_interval[OF ord]
hoelzl@59453
   516
  by (subst Rep_bcontfun_inject[symmetric]) simp
hoelzl@59453
   517
hoelzl@59453
   518
end