src/HOL/Analysis/Continuous_Extension.thy
author immler
Tue Jul 10 09:38:35 2018 +0200 (11 months ago)
changeset 68607 67bb59e49834
parent 68224 1f7308050349
child 69286 e4d5a07fecb6
permissions -rw-r--r--
make theorem, corollary, and proposition %important for HOL-Analysis manual
wenzelm@63992
     1
(*  Title:      HOL/Analysis/Continuous_Extension.thy
lp15@63305
     2
    Authors:    LC Paulson, based on material from HOL Light
lp15@63305
     3
*)
lp15@63305
     4
lp15@63305
     5
section \<open>Continuous extensions of functions: Urysohn's lemma, Dugundji extension theorem, Tietze\<close>
lp15@63305
     6
hoelzl@63594
     7
theory Continuous_Extension
lp15@66289
     8
imports Starlike
lp15@63305
     9
begin
lp15@63305
    10
lp15@63305
    11
subsection\<open>Partitions of unity subordinate to locally finite open coverings\<close>
lp15@63305
    12
lp15@63305
    13
text\<open>A difference from HOL Light: all summations over infinite sets equal zero,
lp15@63305
    14
   so the "support" must be made explicit in the summation below!\<close>
lp15@63305
    15
immler@68607
    16
proposition subordinate_partition_of_unity:
lp15@63305
    17
  fixes S :: "'a :: euclidean_space set"
lp15@63305
    18
  assumes "S \<subseteq> \<Union>\<C>" and opC: "\<And>T. T \<in> \<C> \<Longrightarrow> open T"
lp15@63305
    19
      and fin: "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
lp15@63305
    20
  obtains F :: "['a set, 'a] \<Rightarrow> real"
lp15@63305
    21
    where "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x \<in> S. 0 \<le> F U x)"
lp15@63305
    22
      and "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
nipkow@64267
    23
      and "\<And>x. x \<in> S \<Longrightarrow> supp_sum (\<lambda>W. F W x) \<C> = 1"
lp15@63305
    24
      and "\<And>x. x \<in> S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}"
immler@68607
    25
proof (cases "\<exists>W. W \<in> \<C> \<and> S \<subseteq> W")
lp15@63305
    26
  case True
lp15@63305
    27
    then obtain W where "W \<in> \<C>" "S \<subseteq> W" by metis
lp15@63305
    28
    then show ?thesis
lp15@63305
    29
      apply (rule_tac F = "\<lambda>V x. if V = W then 1 else 0" in that)
nipkow@64267
    30
      apply (auto simp: continuous_on_const supp_sum_def support_on_def)
lp15@63305
    31
      done
lp15@63305
    32
next
lp15@63305
    33
  case False
nipkow@64267
    34
    have nonneg: "0 \<le> supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" for x
nipkow@64267
    35
      by (simp add: supp_sum_def sum_nonneg)
lp15@63305
    36
    have sd_pos: "0 < setdist {x} (S - V)" if "V \<in> \<C>" "x \<in> S" "x \<in> V" for V x
lp15@63305
    37
    proof -
lp15@63305
    38
      have "closedin (subtopology euclidean S) (S - V)"
lp15@63305
    39
        by (simp add: Diff_Diff_Int Diff_subset closedin_def opC openin_open_Int \<open>V \<in> \<C>\<close>)
lp15@63305
    40
      with that False setdist_eq_0_closedin [of S "S-V" x] setdist_pos_le [of "{x}" "S - V"]
lp15@63305
    41
        show ?thesis
lp15@63305
    42
          by (simp add: order_class.order.order_iff_strict)
lp15@63305
    43
    qed
nipkow@64267
    44
    have ss_pos: "0 < supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>" if "x \<in> S" for x
lp15@63305
    45
    proof -
lp15@63305
    46
      obtain U where "U \<in> \<C>" "x \<in> U" using \<open>x \<in> S\<close> \<open>S \<subseteq> \<Union>\<C>\<close>
lp15@63305
    47
        by blast
lp15@63305
    48
      obtain V where "open V" "x \<in> V" "finite {U \<in> \<C>. U \<inter> V \<noteq> {}}"
lp15@63305
    49
        using \<open>x \<in> S\<close> fin by blast
lp15@63305
    50
      then have *: "finite {A \<in> \<C>. \<not> S \<subseteq> A \<and> x \<notin> closure (S - A)}"
lp15@63305
    51
        using closure_def that by (blast intro: rev_finite_subset)
lp15@63305
    52
      have "x \<notin> closure (S - U)"
lp15@63305
    53
        by (metis \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> less_irrefl sd_pos setdist_eq_0_sing_1 that)
lp15@63305
    54
      then show ?thesis
nipkow@64267
    55
        apply (simp add: setdist_eq_0_sing_1 supp_sum_def support_on_def)
nipkow@64267
    56
        apply (rule ordered_comm_monoid_add_class.sum_pos2 [OF *, of U])
lp15@63305
    57
        using \<open>U \<in> \<C>\<close> \<open>x \<in> U\<close> False
lp15@63305
    58
        apply (auto simp: setdist_pos_le sd_pos that)
lp15@63305
    59
        done
lp15@63305
    60
    qed
lp15@63305
    61
    define F where
nipkow@64267
    62
      "F \<equiv> \<lambda>W x. if x \<in> S then setdist {x} (S - W) / supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>
lp15@63305
    63
                 else 0"
lp15@63305
    64
    show ?thesis
lp15@63305
    65
    proof (rule_tac F = F in that)
lp15@63305
    66
      have "continuous_on S (F U)" if "U \<in> \<C>" for U
lp15@63305
    67
      proof -
nipkow@64267
    68
        have *: "continuous_on S (\<lambda>x. supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>)"
lp15@63305
    69
        proof (clarsimp simp add: continuous_on_eq_continuous_within)
lp15@63305
    70
          fix x assume "x \<in> S"
lp15@63305
    71
          then obtain X where "open X" and x: "x \<in> S \<inter> X" and finX: "finite {U \<in> \<C>. U \<inter> X \<noteq> {}}"
lp15@63305
    72
            using assms by blast
lp15@63305
    73
          then have OSX: "openin (subtopology euclidean S) (S \<inter> X)" by blast
lp15@63305
    74
          have sumeq: "\<And>x. x \<in> S \<inter> X \<Longrightarrow>
lp15@63305
    75
                     (\<Sum>V | V \<in> \<C> \<and> V \<inter> X \<noteq> {}. setdist {x} (S - V))
nipkow@64267
    76
                     = supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>"
nipkow@64267
    77
            apply (simp add: supp_sum_def)
nipkow@64267
    78
            apply (rule sum.mono_neutral_right [OF finX])
hoelzl@63593
    79
            apply (auto simp: setdist_eq_0_sing_1 support_on_def subset_iff)
lp15@63305
    80
            apply (meson DiffI closure_subset disjoint_iff_not_equal subsetCE)
lp15@63305
    81
            done
nipkow@64267
    82
          show "continuous (at x within S) (\<lambda>x. supp_sum (\<lambda>V. setdist {x} (S - V)) \<C>)"
lp15@63305
    83
            apply (rule continuous_transform_within_openin
nipkow@64267
    84
                     [where f = "\<lambda>x. (sum (\<lambda>V. setdist {x} (S - V)) {V \<in> \<C>. V \<inter> X \<noteq> {}})"
lp15@63305
    85
                        and S ="S \<inter> X"])
lp15@63305
    86
            apply (rule continuous_intros continuous_at_setdist continuous_at_imp_continuous_at_within OSX x)+
lp15@63305
    87
            apply (simp add: sumeq)
lp15@63305
    88
            done
lp15@63305
    89
        qed
lp15@63305
    90
        show ?thesis
lp15@63305
    91
          apply (simp add: F_def)
lp15@63305
    92
          apply (rule continuous_intros *)+
lp15@63305
    93
          using ss_pos apply force
lp15@63305
    94
          done
lp15@63305
    95
      qed
lp15@63305
    96
      moreover have "\<lbrakk>U \<in> \<C>; x \<in> S\<rbrakk> \<Longrightarrow> 0 \<le> F U x" for U x
lp15@63305
    97
        using nonneg [of x] by (simp add: F_def divide_simps setdist_pos_le)
lp15@63305
    98
      ultimately show "\<And>U. U \<in> \<C> \<Longrightarrow> continuous_on S (F U) \<and> (\<forall>x\<in>S. 0 \<le> F U x)"
lp15@63305
    99
        by metis
lp15@63305
   100
    next
lp15@63305
   101
      show "\<And>x U. \<lbrakk>U \<in> \<C>; x \<in> S; x \<notin> U\<rbrakk> \<Longrightarrow> F U x = 0"
lp15@63305
   102
        by (simp add: setdist_eq_0_sing_1 closure_def F_def)
lp15@63305
   103
    next
nipkow@64267
   104
      show "supp_sum (\<lambda>W. F W x) \<C> = 1" if "x \<in> S" for x
lp15@63305
   105
        using that ss_pos [OF that]
nipkow@64267
   106
        by (simp add: F_def divide_simps supp_sum_divide_distrib [symmetric])
lp15@63305
   107
    next
lp15@63305
   108
      show "\<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. F U x \<noteq> 0}" if "x \<in> S" for x
lp15@63305
   109
        using fin [OF that] that
lp15@63305
   110
        by (fastforce simp: setdist_eq_0_sing_1 closure_def F_def elim!: rev_finite_subset)
lp15@63305
   111
    qed
lp15@63305
   112
qed
lp15@63305
   113
lp15@63305
   114
lp15@63306
   115
subsection\<open>Urysohn's lemma (for Euclidean spaces, where the proof is easy using distances)\<close>
lp15@63305
   116
lp15@63305
   117
lemma Urysohn_both_ne:
lp15@63305
   118
  assumes US: "closedin (subtopology euclidean U) S"
lp15@63305
   119
      and UT: "closedin (subtopology euclidean U) T"
lp15@63305
   120
      and "S \<inter> T = {}" "S \<noteq> {}" "T \<noteq> {}" "a \<noteq> b"
lp15@63305
   121
  obtains f :: "'a::euclidean_space \<Rightarrow> 'b::real_normed_vector"
lp15@63305
   122
    where "continuous_on U f"
lp15@63305
   123
          "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
lp15@63305
   124
          "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
lp15@63305
   125
          "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
lp15@63305
   126
proof -
lp15@63305
   127
  have S0: "\<And>x. x \<in> U \<Longrightarrow> setdist {x} S = 0 \<longleftrightarrow> x \<in> S"
lp15@63305
   128
    using \<open>S \<noteq> {}\<close>  US setdist_eq_0_closedin  by auto
lp15@63305
   129
  have T0: "\<And>x. x \<in> U \<Longrightarrow> setdist {x} T = 0 \<longleftrightarrow> x \<in> T"
lp15@63305
   130
    using \<open>T \<noteq> {}\<close>  UT setdist_eq_0_closedin  by auto
lp15@63305
   131
  have sdpos: "0 < setdist {x} S + setdist {x} T" if "x \<in> U" for x
lp15@63305
   132
  proof -
lp15@63305
   133
    have "~ (setdist {x} S = 0 \<and> setdist {x} T = 0)"
lp15@63305
   134
      using assms by (metis IntI empty_iff setdist_eq_0_closedin that)
lp15@63305
   135
    then show ?thesis
lp15@63305
   136
      by (metis add.left_neutral add.right_neutral add_pos_pos linorder_neqE_linordered_idom not_le setdist_pos_le)
lp15@63305
   137
  qed
lp15@63305
   138
  define f where "f \<equiv> \<lambda>x. a + (setdist {x} S / (setdist {x} S + setdist {x} T)) *\<^sub>R (b - a)"
lp15@63305
   139
  show ?thesis
lp15@63305
   140
  proof (rule_tac f = f in that)
lp15@63305
   141
    show "continuous_on U f"
lp15@63305
   142
      using sdpos unfolding f_def
lp15@63305
   143
      by (intro continuous_intros | force)+
lp15@63305
   144
    show "f x \<in> closed_segment a b" if "x \<in> U" for x
lp15@63305
   145
        unfolding f_def
lp15@63305
   146
      apply (simp add: closed_segment_def)
lp15@63305
   147
      apply (rule_tac x="(setdist {x} S / (setdist {x} S + setdist {x} T))" in exI)
lp15@63305
   148
      using sdpos that apply (simp add: algebra_simps)
lp15@63305
   149
      done
lp15@63305
   150
    show "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
lp15@63305
   151
      using S0 \<open>a \<noteq> b\<close> f_def sdpos by force
lp15@63305
   152
    show "(f x = b \<longleftrightarrow> x \<in> T)" if "x \<in> U" for x
lp15@63305
   153
    proof -
lp15@63305
   154
      have "f x = b \<longleftrightarrow> (setdist {x} S / (setdist {x} S + setdist {x} T)) = 1"
lp15@63305
   155
        unfolding f_def
lp15@63305
   156
        apply (rule iffI)
lp15@63305
   157
         apply (metis  \<open>a \<noteq> b\<close> add_diff_cancel_left' eq_iff_diff_eq_0 pth_1 real_vector.scale_right_imp_eq, force)
lp15@63305
   158
        done
lp15@63305
   159
      also have "...  \<longleftrightarrow> setdist {x} T = 0 \<and> setdist {x} S \<noteq> 0"
lp15@63305
   160
        using sdpos that
lp15@63305
   161
        by (simp add: divide_simps) linarith
lp15@63305
   162
      also have "...  \<longleftrightarrow> x \<in> T"
lp15@63305
   163
        using \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>S \<inter> T = {}\<close> that
lp15@63305
   164
        by (force simp: S0 T0)
lp15@63305
   165
      finally show ?thesis .
lp15@63305
   166
    qed
lp15@63305
   167
  qed
lp15@63305
   168
qed
lp15@63305
   169
lp15@63305
   170
proposition Urysohn_local_strong:
lp15@63305
   171
  assumes US: "closedin (subtopology euclidean U) S"
lp15@63305
   172
      and UT: "closedin (subtopology euclidean U) T"
lp15@63305
   173
      and "S \<inter> T = {}" "a \<noteq> b"
lp15@63305
   174
  obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@63305
   175
    where "continuous_on U f"
lp15@63305
   176
          "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
lp15@63305
   177
          "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
lp15@63305
   178
          "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
lp15@63305
   179
proof (cases "S = {}")
lp15@63305
   180
  case True show ?thesis
lp15@63305
   181
  proof (cases "T = {}")
lp15@63305
   182
    case True show ?thesis
lp15@63305
   183
    proof (rule_tac f = "\<lambda>x. midpoint a b" in that)
lp15@63305
   184
      show "continuous_on U (\<lambda>x. midpoint a b)"
lp15@63305
   185
        by (intro continuous_intros)
lp15@63305
   186
      show "midpoint a b \<in> closed_segment a b"
lp15@63305
   187
        using csegment_midpoint_subset by blast
lp15@63305
   188
      show "(midpoint a b = a) = (x \<in> S)" for x
lp15@63305
   189
        using \<open>S = {}\<close> \<open>a \<noteq> b\<close> by simp
lp15@63305
   190
      show "(midpoint a b = b) = (x \<in> T)" for x
lp15@63305
   191
        using \<open>T = {}\<close> \<open>a \<noteq> b\<close> by simp
lp15@63305
   192
    qed
lp15@63305
   193
  next
lp15@63305
   194
    case False
lp15@63305
   195
    show ?thesis
lp15@63305
   196
    proof (cases "T = U")
lp15@63305
   197
      case True with \<open>S = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
lp15@63305
   198
        by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const)
lp15@63305
   199
    next
lp15@63305
   200
      case False
lp15@63305
   201
      with UT closedin_subset obtain c where c: "c \<in> U" "c \<notin> T"
lp15@63305
   202
        by fastforce
lp15@63305
   203
      obtain f where f: "continuous_on U f"
lp15@63305
   204
                "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment (midpoint a b) b"
lp15@63305
   205
                "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)"
lp15@63305
   206
                "\<And>x. x \<in> U \<Longrightarrow> (f x = b \<longleftrightarrow> x \<in> T)"
lp15@63305
   207
        apply (rule Urysohn_both_ne [of U "{c}" T "midpoint a b" "b"])
lp15@63305
   208
        using c \<open>T \<noteq> {}\<close> assms apply simp_all
lp15@63305
   209
        done
lp15@63305
   210
      show ?thesis
lp15@63305
   211
        apply (rule_tac f=f in that)
lp15@63305
   212
        using \<open>S = {}\<close> \<open>T \<noteq> {}\<close> f csegment_midpoint_subset notin_segment_midpoint [OF \<open>a \<noteq> b\<close>]
lp15@63305
   213
        apply force+
lp15@63305
   214
        done
lp15@63305
   215
    qed
lp15@63305
   216
  qed
lp15@63305
   217
next
lp15@63305
   218
  case False
lp15@63305
   219
  show ?thesis
lp15@63305
   220
  proof (cases "T = {}")
lp15@63305
   221
    case True show ?thesis
lp15@63305
   222
    proof (cases "S = U")
lp15@63305
   223
      case True with \<open>T = {}\<close> \<open>a \<noteq> b\<close> show ?thesis
lp15@63305
   224
        by (rule_tac f = "\<lambda>x. a" in that) (auto simp: continuous_on_const)
lp15@63305
   225
    next
lp15@63305
   226
      case False
lp15@63305
   227
      with US closedin_subset obtain c where c: "c \<in> U" "c \<notin> S"
lp15@63305
   228
        by fastforce
lp15@63305
   229
      obtain f where f: "continuous_on U f"
lp15@63305
   230
                "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a (midpoint a b)"
lp15@63305
   231
                "\<And>x. x \<in> U \<Longrightarrow> (f x = midpoint a b \<longleftrightarrow> x = c)"
lp15@63305
   232
                "\<And>x. x \<in> U \<Longrightarrow> (f x = a \<longleftrightarrow> x \<in> S)"
lp15@63305
   233
        apply (rule Urysohn_both_ne [of U S "{c}" a "midpoint a b"])
lp15@63305
   234
        using c \<open>S \<noteq> {}\<close> assms apply simp_all
lp15@63305
   235
        apply (metis midpoint_eq_endpoint)
lp15@63305
   236
        done
lp15@63305
   237
      show ?thesis
lp15@63305
   238
        apply (rule_tac f=f in that)
lp15@63305
   239
        using \<open>S \<noteq> {}\<close> \<open>T = {}\<close> f  \<open>a \<noteq> b\<close>
lp15@63305
   240
        apply simp_all
lp15@63305
   241
        apply (metis (no_types) closed_segment_commute csegment_midpoint_subset midpoint_sym subset_iff)
lp15@63305
   242
        apply (metis closed_segment_commute midpoint_sym notin_segment_midpoint)
lp15@63305
   243
        done
lp15@63305
   244
    qed
lp15@63305
   245
  next
lp15@63305
   246
    case False
lp15@63305
   247
    show ?thesis
lp15@63305
   248
      using Urysohn_both_ne [OF US UT \<open>S \<inter> T = {}\<close> \<open>S \<noteq> {}\<close> \<open>T \<noteq> {}\<close> \<open>a \<noteq> b\<close>] that
lp15@63305
   249
      by blast
lp15@63305
   250
  qed
lp15@63305
   251
qed
lp15@63305
   252
lp15@63305
   253
lemma Urysohn_local:
lp15@63305
   254
  assumes US: "closedin (subtopology euclidean U) S"
lp15@63305
   255
      and UT: "closedin (subtopology euclidean U) T"
lp15@63305
   256
      and "S \<inter> T = {}"
lp15@63305
   257
  obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@63305
   258
    where "continuous_on U f"
lp15@63305
   259
          "\<And>x. x \<in> U \<Longrightarrow> f x \<in> closed_segment a b"
lp15@63305
   260
          "\<And>x. x \<in> S \<Longrightarrow> f x = a"
lp15@63305
   261
          "\<And>x. x \<in> T \<Longrightarrow> f x = b"
lp15@63305
   262
proof (cases "a = b")
lp15@63305
   263
  case True then show ?thesis
lp15@63305
   264
    by (rule_tac f = "\<lambda>x. b" in that) (auto simp: continuous_on_const)
lp15@63305
   265
next
lp15@63305
   266
  case False
lp15@63305
   267
  then show ?thesis
lp15@63305
   268
    apply (rule Urysohn_local_strong [OF assms])
lp15@63305
   269
    apply (erule that, assumption)
lp15@63305
   270
    apply (meson US closedin_singleton closedin_trans)
lp15@63305
   271
    apply (meson UT closedin_singleton closedin_trans)
lp15@63305
   272
    done
lp15@63305
   273
qed
lp15@63305
   274
lp15@63305
   275
lemma Urysohn_strong:
lp15@63305
   276
  assumes US: "closed S"
lp15@63305
   277
      and UT: "closed T"
lp15@63305
   278
      and "S \<inter> T = {}" "a \<noteq> b"
lp15@63305
   279
  obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@63305
   280
    where "continuous_on UNIV f"
lp15@63305
   281
          "\<And>x. f x \<in> closed_segment a b"
lp15@63305
   282
          "\<And>x. f x = a \<longleftrightarrow> x \<in> S"
lp15@63305
   283
          "\<And>x. f x = b \<longleftrightarrow> x \<in> T"
lp15@66884
   284
using assms by (auto intro: Urysohn_local_strong [of UNIV S T])
lp15@63305
   285
immler@68607
   286
proposition Urysohn:
lp15@63305
   287
  assumes US: "closed S"
lp15@63305
   288
      and UT: "closed T"
lp15@63305
   289
      and "S \<inter> T = {}"
lp15@63305
   290
  obtains f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@63305
   291
    where "continuous_on UNIV f"
lp15@63305
   292
          "\<And>x. f x \<in> closed_segment a b"
lp15@63305
   293
          "\<And>x. x \<in> S \<Longrightarrow> f x = a"
lp15@63305
   294
          "\<And>x. x \<in> T \<Longrightarrow> f x = b"
immler@68607
   295
  using assms by (auto intro: Urysohn_local [of UNIV S T a b])
lp15@63305
   296
lp15@63305
   297
nipkow@67968
   298
subsection\<open>The Dugundji extension theorem and Tietze variants as corollaries\<close>
lp15@63305
   299
immler@67962
   300
text%important\<open>J. Dugundji. An extension of Tietze's theorem. Pacific J. Math. Volume 1, Number 3 (1951), 353-367.
wenzelm@68224
   301
https://projecteuclid.org/euclid.pjm/1103052106\<close>
lp15@63305
   302
immler@68607
   303
theorem Dugundji:
lp15@63305
   304
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
lp15@63305
   305
  assumes "convex C" "C \<noteq> {}"
lp15@63305
   306
      and cloin: "closedin (subtopology euclidean U) S"
lp15@63305
   307
      and contf: "continuous_on S f" and "f ` S \<subseteq> C"
lp15@63305
   308
  obtains g where "continuous_on U g" "g ` U \<subseteq> C"
lp15@63305
   309
                  "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
immler@68607
   310
proof (cases "S = {}")
lp15@63305
   311
  case True then show thesis
wenzelm@67613
   312
    apply (rule_tac g="\<lambda>x. SOME y. y \<in> C" in that)
lp15@63305
   313
      apply (rule continuous_intros)
lp15@63305
   314
     apply (meson all_not_in_conv \<open>C \<noteq> {}\<close> image_subsetI someI_ex, simp)
lp15@63305
   315
    done
lp15@63305
   316
next
lp15@63305
   317
  case False
lp15@63305
   318
  then have sd_pos: "\<And>x. \<lbrakk>x \<in> U; x \<notin> S\<rbrakk> \<Longrightarrow> 0 < setdist {x} S"
lp15@63305
   319
    using setdist_eq_0_closedin [OF cloin] le_less setdist_pos_le by fastforce
lp15@63305
   320
  define \<B> where "\<B> = {ball x (setdist {x} S / 2) |x. x \<in> U - S}"
lp15@63305
   321
  have [simp]: "\<And>T. T \<in> \<B> \<Longrightarrow> open T"
lp15@63305
   322
    by (auto simp: \<B>_def)
lp15@63305
   323
  have USS: "U - S \<subseteq> \<Union>\<B>"
lp15@63305
   324
    by (auto simp: sd_pos \<B>_def)
lp15@63305
   325
  obtain \<C> where USsub: "U - S \<subseteq> \<Union>\<C>"
lp15@63305
   326
       and nbrhd: "\<And>U. U \<in> \<C> \<Longrightarrow> open U \<and> (\<exists>T. T \<in> \<B> \<and> U \<subseteq> T)"
lp15@63305
   327
       and fin: "\<And>x. x \<in> U - S
lp15@63305
   328
                     \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U. U \<in> \<C> \<and> U \<inter> V \<noteq> {}}"
lp15@63305
   329
    using paracompact [OF USS] by auto
lp15@63305
   330
  have "\<exists>v a. v \<in> U \<and> v \<notin> S \<and> a \<in> S \<and>
lp15@63305
   331
              T \<subseteq> ball v (setdist {v} S / 2) \<and>
lp15@63305
   332
              dist v a \<le> 2 * setdist {v} S" if "T \<in> \<C>" for T
lp15@63305
   333
  proof -
lp15@63305
   334
    obtain v where v: "T \<subseteq> ball v (setdist {v} S / 2)" "v \<in> U" "v \<notin> S"
lp15@63305
   335
      using \<open>T \<in> \<C>\<close> nbrhd by (force simp: \<B>_def)
lp15@63305
   336
    then obtain a where "a \<in> S" "dist v a < 2 * setdist {v} S"
lp15@63305
   337
      using setdist_ltE [of "{v}" S "2 * setdist {v} S"]
lp15@63305
   338
      using False sd_pos by force
lp15@63305
   339
    with v show ?thesis
lp15@63305
   340
      apply (rule_tac x=v in exI)
lp15@63305
   341
      apply (rule_tac x=a in exI, auto)
lp15@63305
   342
      done
lp15@63305
   343
  qed
lp15@63305
   344
  then obtain \<V> \<A> where
lp15@63305
   345
    VA: "\<And>T. T \<in> \<C> \<Longrightarrow> \<V> T \<in> U \<and> \<V> T \<notin> S \<and> \<A> T \<in> S \<and>
lp15@63305
   346
              T \<subseteq> ball (\<V> T) (setdist {\<V> T} S / 2) \<and>
lp15@63305
   347
              dist (\<V> T) (\<A> T) \<le> 2 * setdist {\<V> T} S"
lp15@63305
   348
    by metis
lp15@63305
   349
  have sdle: "setdist {\<V> T} S \<le> 2 * setdist {v} S" if "T \<in> \<C>" "v \<in> T" for T v
lp15@63305
   350
    using setdist_Lipschitz [of "\<V> T" S v] VA [OF \<open>T \<in> \<C>\<close>] \<open>v \<in> T\<close> by auto
lp15@63305
   351
  have d6: "dist a (\<A> T) \<le> 6 * dist a v" if "T \<in> \<C>" "v \<in> T" "a \<in> S" for T v a
lp15@63305
   352
  proof -
lp15@63305
   353
    have "dist (\<V> T) v < setdist {\<V> T} S / 2"
lp15@63305
   354
      using that VA mem_ball by blast
lp15@63305
   355
    also have "... \<le> setdist {v} S"
lp15@63305
   356
      using sdle [OF \<open>T \<in> \<C>\<close> \<open>v \<in> T\<close>] by simp
lp15@63305
   357
    also have vS: "setdist {v} S \<le> dist a v"
lp15@63305
   358
      by (simp add: setdist_le_dist setdist_sym \<open>a \<in> S\<close>)
lp15@63305
   359
    finally have VTV: "dist (\<V> T) v < dist a v" .
lp15@63305
   360
    have VTS: "setdist {\<V> T} S \<le> 2 * dist a v"
lp15@63305
   361
      using sdle that vS by force
lp15@63305
   362
    have "dist a (\<A> T) \<le> dist a v + dist v (\<V> T) + dist (\<V> T) (\<A> T)"
lp15@63305
   363
      by (metis add.commute add_le_cancel_left dist_commute dist_triangle2 dist_triangle_le)
lp15@63305
   364
    also have "... \<le> dist a v + dist a v + dist (\<V> T) (\<A> T)"
lp15@63305
   365
      using VTV by (simp add: dist_commute)
lp15@63305
   366
    also have "... \<le> 2 * dist a v + 2 * setdist {\<V> T} S"
lp15@63305
   367
      using VA [OF \<open>T \<in> \<C>\<close>] by auto
lp15@63305
   368
    finally show ?thesis
lp15@63305
   369
      using VTS by linarith
lp15@63305
   370
  qed
lp15@63305
   371
  obtain H :: "['a set, 'a] \<Rightarrow> real"
lp15@63305
   372
    where Hcont: "\<And>Z. Z \<in> \<C> \<Longrightarrow> continuous_on (U-S) (H Z)"
lp15@63305
   373
      and Hge0: "\<And>Z x. \<lbrakk>Z \<in> \<C>; x \<in> U-S\<rbrakk> \<Longrightarrow> 0 \<le> H Z x"
lp15@63305
   374
      and Heq0: "\<And>x Z. \<lbrakk>Z \<in> \<C>; x \<in> U-S; x \<notin> Z\<rbrakk> \<Longrightarrow> H Z x = 0"
nipkow@64267
   375
      and H1: "\<And>x. x \<in> U-S \<Longrightarrow> supp_sum (\<lambda>W. H W x) \<C> = 1"
lp15@63305
   376
      and Hfin: "\<And>x. x \<in> U-S \<Longrightarrow> \<exists>V. open V \<and> x \<in> V \<and> finite {U \<in> \<C>. \<exists>x\<in>V. H U x \<noteq> 0}"
lp15@63305
   377
    apply (rule subordinate_partition_of_unity [OF USsub _ fin])
lp15@63305
   378
    using nbrhd by auto
nipkow@64267
   379
  define g where "g \<equiv> \<lambda>x. if x \<in> S then f x else supp_sum (\<lambda>T. H T x *\<^sub>R f(\<A> T)) \<C>"
lp15@63305
   380
  show ?thesis
lp15@63305
   381
  proof (rule that)
lp15@63305
   382
    show "continuous_on U g"
lp15@63305
   383
    proof (clarsimp simp: continuous_on_eq_continuous_within)
lp15@63305
   384
      fix a assume "a \<in> U"
lp15@63305
   385
      show "continuous (at a within U) g"
lp15@63305
   386
      proof (cases "a \<in> S")
lp15@63305
   387
        case True show ?thesis
lp15@63305
   388
        proof (clarsimp simp add: continuous_within_topological)
lp15@63305
   389
          fix W
lp15@63305
   390
          assume "open W" "g a \<in> W"
lp15@63305
   391
          then obtain e where "0 < e" and e: "ball (f a) e \<subseteq> W"
lp15@63305
   392
            using openE True g_def by auto
lp15@63305
   393
          have "continuous (at a within S) f"
lp15@63305
   394
            using True contf continuous_on_eq_continuous_within by blast
lp15@63305
   395
          then obtain d where "0 < d"
lp15@63305
   396
                        and d: "\<And>x. \<lbrakk>x \<in> S; dist x a < d\<rbrakk> \<Longrightarrow> dist (f x) (f a) < e"
lp15@63305
   397
            using continuous_within_eps_delta \<open>0 < e\<close> by force
lp15@63305
   398
          have "g y \<in> ball (f a) e" if "y \<in> U" and y: "y \<in> ball a (d / 6)" for y
lp15@63305
   399
          proof (cases "y \<in> S")
lp15@63305
   400
            case True
lp15@63305
   401
            then have "dist (f a) (f y) < e"
lp15@63305
   402
              by (metis ball_divide_subset_numeral dist_commute in_mono mem_ball y d)
lp15@63305
   403
            then show ?thesis
lp15@63305
   404
              by (simp add: True g_def)
lp15@63305
   405
          next
lp15@63305
   406
            case False
lp15@63305
   407
            have *: "dist (f (\<A> T)) (f a) < e" if "T \<in> \<C>" "H T y \<noteq> 0" for T
lp15@63305
   408
            proof -
lp15@63305
   409
              have "y \<in> T"
lp15@63305
   410
                using Heq0 that False \<open>y \<in> U\<close> by blast
lp15@63305
   411
              have "dist (\<A> T) a < d"
lp15@63305
   412
                using d6 [OF \<open>T \<in> \<C>\<close> \<open>y \<in> T\<close> \<open>a \<in> S\<close>] y
lp15@63305
   413
                by (simp add: dist_commute mult.commute)
lp15@63305
   414
              then show ?thesis
lp15@63305
   415
                using VA [OF \<open>T \<in> \<C>\<close>] by (auto simp: d)
lp15@63305
   416
            qed
nipkow@64267
   417
            have "supp_sum (\<lambda>T. H T y *\<^sub>R f (\<A> T)) \<C> \<in> ball (f a) e"
nipkow@64267
   418
              apply (rule convex_supp_sum [OF convex_ball])
lp15@63305
   419
              apply (simp_all add: False H1 Hge0 \<open>y \<in> U\<close>)
lp15@63305
   420
              by (metis dist_commute *)
lp15@63305
   421
            then show ?thesis
lp15@63305
   422
              by (simp add: False g_def)
lp15@63305
   423
          qed
lp15@63305
   424
          then show "\<exists>A. open A \<and> a \<in> A \<and> (\<forall>y\<in>U. y \<in> A \<longrightarrow> g y \<in> W)"
lp15@63305
   425
            apply (rule_tac x = "ball a (d / 6)" in exI)
lp15@63305
   426
            using e \<open>0 < d\<close> by fastforce
lp15@63305
   427
        qed
lp15@63305
   428
      next
lp15@63305
   429
        case False
lp15@63305
   430
        obtain N where N: "open N" "a \<in> N"
lp15@63305
   431
                   and finN: "finite {U \<in> \<C>. \<exists>a\<in>N. H U a \<noteq> 0}"
lp15@63305
   432
          using Hfin False \<open>a \<in> U\<close> by auto
lp15@63305
   433
        have oUS: "openin (subtopology euclidean U) (U - S)"
lp15@63305
   434
          using cloin by (simp add: openin_diff)
lp15@63305
   435
        have HcontU: "continuous (at a within U) (H T)" if "T \<in> \<C>" for T
lp15@63305
   436
          using Hcont [OF \<open>T \<in> \<C>\<close>] False  \<open>a \<in> U\<close> \<open>T \<in> \<C>\<close>
lp15@63305
   437
          apply (simp add: continuous_on_eq_continuous_within continuous_within)
lp15@63305
   438
          apply (rule Lim_transform_within_set)
lp15@63305
   439
          using oUS
lp15@63305
   440
            apply (force simp: eventually_at openin_contains_ball dist_commute dest!: bspec)+
lp15@63305
   441
          done
lp15@63305
   442
        show ?thesis
lp15@63305
   443
        proof (rule continuous_transform_within_openin [OF _ oUS])
nipkow@64267
   444
          show "continuous (at a within U) (\<lambda>x. supp_sum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C>)"
lp15@63305
   445
          proof (rule continuous_transform_within_openin)
lp15@63305
   446
            show "continuous (at a within U)
lp15@63305
   447
                    (\<lambda>x. \<Sum>T\<in>{U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T))"
lp15@63305
   448
              by (force intro: continuous_intros HcontU)+
lp15@63305
   449
          next
lp15@63305
   450
            show "openin (subtopology euclidean U) ((U - S) \<inter> N)"
lp15@63305
   451
              using N oUS openin_trans by blast
lp15@63305
   452
          next
lp15@63305
   453
            show "a \<in> (U - S) \<inter> N" using False \<open>a \<in> U\<close> N by blast
lp15@63305
   454
          next
lp15@63305
   455
            show "\<And>x. x \<in> (U - S) \<inter> N \<Longrightarrow>
lp15@63305
   456
                         (\<Sum>T \<in> {U \<in> \<C>. \<exists>x\<in>N. H U x \<noteq> 0}. H T x *\<^sub>R f (\<A> T))
nipkow@64267
   457
                         = supp_sum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C>"
nipkow@64267
   458
              by (auto simp: supp_sum_def support_on_def
nipkow@64267
   459
                       intro: sum.mono_neutral_right [OF finN])
lp15@63305
   460
          qed
lp15@63305
   461
        next
lp15@63305
   462
          show "a \<in> U - S" using False \<open>a \<in> U\<close> by blast
lp15@63305
   463
        next
nipkow@64267
   464
          show "\<And>x. x \<in> U - S \<Longrightarrow> supp_sum (\<lambda>T. H T x *\<^sub>R f (\<A> T)) \<C> = g x"
lp15@63305
   465
            by (simp add: g_def)
lp15@63305
   466
        qed
lp15@63305
   467
      qed
lp15@63305
   468
    qed
lp15@63305
   469
    show "g ` U \<subseteq> C"
lp15@63305
   470
      using \<open>f ` S \<subseteq> C\<close> VA
nipkow@64267
   471
      by (fastforce simp: g_def Hge0 intro!: convex_supp_sum [OF \<open>convex C\<close>] H1)
lp15@63305
   472
    show "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
lp15@63305
   473
      by (simp add: g_def)
lp15@63305
   474
  qed
lp15@63305
   475
qed
lp15@63305
   476
lp15@63305
   477
immler@68607
   478
corollary Tietze:
lp15@63305
   479
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
lp15@63305
   480
  assumes "continuous_on S f"
lp15@63305
   481
      and "closedin (subtopology euclidean U) S"
lp15@63305
   482
      and "0 \<le> B"
lp15@63305
   483
      and "\<And>x. x \<in> S \<Longrightarrow> norm(f x) \<le> B"
lp15@63305
   484
  obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
lp15@63305
   485
                  "\<And>x. x \<in> U \<Longrightarrow> norm(g x) \<le> B"
immler@68607
   486
  using assms
lp15@63305
   487
by (auto simp: image_subset_iff intro: Dugundji [of "cball 0 B" U S f])
lp15@63305
   488
lp15@63305
   489
corollary Tietze_closed_interval:
lp15@63305
   490
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@63305
   491
  assumes "continuous_on S f"
lp15@63305
   492
      and "closedin (subtopology euclidean U) S"
lp15@63305
   493
      and "cbox a b \<noteq> {}"
lp15@63305
   494
      and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
lp15@63305
   495
  obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
lp15@63305
   496
                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
lp15@63305
   497
apply (rule Dugundji [of "cbox a b" U S f])
lp15@63305
   498
using assms by auto
lp15@63305
   499
lp15@63305
   500
corollary Tietze_closed_interval_1:
lp15@63305
   501
  fixes f :: "'a::euclidean_space \<Rightarrow> real"
lp15@63305
   502
  assumes "continuous_on S f"
lp15@63305
   503
      and "closedin (subtopology euclidean U) S"
lp15@63305
   504
      and "a \<le> b"
lp15@63305
   505
      and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> cbox a b"
lp15@63305
   506
  obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
lp15@63305
   507
                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> cbox a b"
lp15@63305
   508
apply (rule Dugundji [of "cbox a b" U S f])
lp15@63305
   509
using assms by (auto simp: image_subset_iff)
lp15@63305
   510
lp15@63305
   511
corollary Tietze_open_interval:
lp15@63305
   512
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@63305
   513
  assumes "continuous_on S f"
lp15@63305
   514
      and "closedin (subtopology euclidean U) S"
lp15@63305
   515
      and "box a b \<noteq> {}"
lp15@63305
   516
      and "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
lp15@63305
   517
  obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
lp15@63305
   518
                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
lp15@63305
   519
apply (rule Dugundji [of "box a b" U S f])
lp15@63305
   520
using assms by auto
lp15@63305
   521
lp15@63305
   522
corollary Tietze_open_interval_1:
lp15@63305
   523
  fixes f :: "'a::euclidean_space \<Rightarrow> real"
lp15@63305
   524
  assumes "continuous_on S f"
lp15@63305
   525
      and "closedin (subtopology euclidean U) S"
lp15@63305
   526
      and "a < b"
lp15@63305
   527
      and no: "\<And>x. x \<in> S \<Longrightarrow> f x \<in> box a b"
lp15@63305
   528
  obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
lp15@63305
   529
                  "\<And>x. x \<in> U \<Longrightarrow> g x \<in> box a b"
lp15@63305
   530
apply (rule Dugundji [of "box a b" U S f])
lp15@63305
   531
using assms by (auto simp: image_subset_iff)
lp15@63305
   532
lp15@63305
   533
corollary Tietze_unbounded:
lp15@63305
   534
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::real_inner"
lp15@63305
   535
  assumes "continuous_on S f"
lp15@63305
   536
      and "closedin (subtopology euclidean U) S"
lp15@63305
   537
  obtains g where "continuous_on U g" "\<And>x. x \<in> S \<Longrightarrow> g x = f x"
lp15@63305
   538
apply (rule Dugundji [of UNIV U S f])
lp15@63305
   539
using assms by auto
lp15@63305
   540
lp15@63305
   541
end