src/HOL/Analysis/Change_Of_Vars.thy
author paulson <lp15@cam.ac.uk>
Wed Apr 18 21:12:50 2018 +0100 (16 months ago)
changeset 68001 0a2a1b6507c1
parent 67999 1b05f74f2e5f
child 68017 e99f9b3962bf
child 68072 493b818e8e10
permissions -rw-r--r--
correction of TeX errors and other oversights
lp15@67998
     1
theory Change_Of_Vars
lp15@67999
     2
  imports Vitali_Covering_Theorem Determinants
lp15@67998
     3
lp15@67998
     4
begin
lp15@67998
     5
lp15@67998
     6
subsection\<open>Induction on matrix row operations\<close>
lp15@67998
     7
lp15@67998
     8
lemma induct_matrix_row_operations:
lp15@67999
     9
  fixes P :: "real^'n^'n \<Rightarrow> bool"
lp15@67998
    10
  assumes zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
lp15@67998
    11
    and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
lp15@67998
    12
    and swap_cols: "\<And>A m n. \<lbrakk>P A; m \<noteq> n\<rbrakk> \<Longrightarrow> P(\<chi> i j. A $ i $ Fun.swap m n id j)"
lp15@67998
    13
    and row_op: "\<And>A m n c. \<lbrakk>P A; m \<noteq> n\<rbrakk>
lp15@67998
    14
                   \<Longrightarrow> P(\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)"
lp15@67998
    15
  shows "P A"
lp15@67998
    16
proof -
lp15@67998
    17
  have "P A" if "(\<And>i j. \<lbrakk>j \<in> -K;  i \<noteq> j\<rbrakk> \<Longrightarrow> A$i$j = 0)" for A K
lp15@67998
    18
  proof -
lp15@67998
    19
    have "finite K"
lp15@67998
    20
      by simp
lp15@67998
    21
    then show ?thesis using that
lp15@67998
    22
    proof (induction arbitrary: A rule: finite_induct)
lp15@67998
    23
      case empty
lp15@67998
    24
      with diagonal show ?case
lp15@67998
    25
        by simp
lp15@67998
    26
    next
lp15@67998
    27
      case (insert k K)
lp15@67998
    28
      note insertK = insert
lp15@67998
    29
      have "P A" if kk: "A$k$k \<noteq> 0"
lp15@67998
    30
        and 0: "\<And>i j. \<lbrakk>j \<in> - insert k K; i \<noteq> j\<rbrakk> \<Longrightarrow> A$i$j = 0"
lp15@67998
    31
               "\<And>i. \<lbrakk>i \<in> -L; i \<noteq> k\<rbrakk> \<Longrightarrow> A$i$k = 0" for A L
lp15@67998
    32
      proof -
lp15@67998
    33
        have "finite L"
lp15@67998
    34
          by simp
lp15@67998
    35
        then show ?thesis using 0 kk
lp15@67998
    36
        proof (induction arbitrary: A rule: finite_induct)
lp15@67998
    37
          case (empty B)
lp15@67998
    38
          show ?case
lp15@67998
    39
          proof (rule insertK)
lp15@67998
    40
            fix i j
lp15@67998
    41
            assume "i \<in> - K" "j \<noteq> i"
lp15@67998
    42
            show "B $ j $ i = 0"
lp15@67998
    43
              using \<open>j \<noteq> i\<close> \<open>i \<in> - K\<close> empty
lp15@67998
    44
              by (metis ComplD ComplI Compl_eq_Diff_UNIV Diff_empty UNIV_I insert_iff)
lp15@67998
    45
          qed
lp15@67998
    46
        next
lp15@67998
    47
          case (insert l L B)
lp15@67998
    48
          show ?case
lp15@67998
    49
          proof (cases "k = l")
lp15@67998
    50
            case True
lp15@67998
    51
            with insert show ?thesis
lp15@67998
    52
              by auto
lp15@67998
    53
          next
lp15@67998
    54
            case False
lp15@67998
    55
            let ?C = "\<chi> i. if i = l then row l B - (B $ l $ k / B $ k $ k) *\<^sub>R row k B else row i B"
lp15@67998
    56
            have 1: "\<lbrakk>j \<in> - insert k K; i \<noteq> j\<rbrakk> \<Longrightarrow> ?C $ i $ j = 0" for j i
lp15@67998
    57
              by (auto simp: insert.prems(1) row_def)
lp15@67998
    58
            have 2: "?C $ i $ k = 0"
lp15@67998
    59
              if "i \<in> - L" "i \<noteq> k" for i
lp15@67998
    60
            proof (cases "i=l")
lp15@67998
    61
              case True
lp15@67998
    62
              with that insert.prems show ?thesis
lp15@67998
    63
                by (simp add: row_def)
lp15@67998
    64
            next
lp15@67998
    65
              case False
lp15@67998
    66
              with that show ?thesis
lp15@67998
    67
                by (simp add: insert.prems(2) row_def)
lp15@67998
    68
            qed
lp15@67998
    69
            have 3: "?C $ k $ k \<noteq> 0"
lp15@67998
    70
              by (auto simp: insert.prems row_def \<open>k \<noteq> l\<close>)
lp15@67998
    71
            have PC: "P ?C"
lp15@67998
    72
              using insert.IH [OF 1 2 3] by auto
lp15@67998
    73
            have eqB: "(\<chi> i. if i = l then row l ?C + (B $ l $ k / B $ k $ k) *\<^sub>R row k ?C else row i ?C) = B"
lp15@67998
    74
              using \<open>k \<noteq> l\<close> by (simp add: vec_eq_iff row_def)
lp15@67998
    75
            show ?thesis
lp15@67998
    76
              using row_op [OF PC, of l k, where c = "B$l$k / B$k$k"] eqB \<open>k \<noteq> l\<close>
lp15@67998
    77
              by (simp add: cong: if_cong)
lp15@67998
    78
          qed
lp15@67998
    79
        qed
lp15@67998
    80
      qed
lp15@67998
    81
      then have nonzero_hyp: "P A"
lp15@67998
    82
        if kk: "A$k$k \<noteq> 0" and zeroes: "\<And>i j. j \<in> - insert k K \<and> i\<noteq>j \<Longrightarrow> A$i$j = 0" for A
lp15@67998
    83
        by (auto simp: intro!: kk zeroes)
lp15@67998
    84
      show ?case
lp15@67998
    85
      proof (cases "row k A = 0")
lp15@67998
    86
        case True
lp15@67998
    87
        with zero_row show ?thesis by auto
lp15@67998
    88
      next
lp15@67998
    89
        case False
lp15@67998
    90
        then obtain l where l: "A$k$l \<noteq> 0"
lp15@67998
    91
          by (auto simp: row_def zero_vec_def vec_eq_iff)
lp15@67998
    92
        show ?thesis
lp15@67998
    93
        proof (cases "k = l")
lp15@67998
    94
          case True
lp15@67998
    95
          with l nonzero_hyp insert.prems show ?thesis
lp15@67998
    96
            by blast
lp15@67998
    97
        next
lp15@67998
    98
          case False
lp15@67998
    99
          have *: "A $ i $ Fun.swap k l id j = 0" if "j \<noteq> k" "j \<notin> K" "i \<noteq> j" for i j
lp15@67998
   100
            using False l insert.prems that
lp15@67998
   101
            by (auto simp: swap_def insert split: if_split_asm)
lp15@67998
   102
          have "P (\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j)"
lp15@67998
   103
            by (rule swap_cols [OF nonzero_hyp False]) (auto simp: l *)
lp15@67998
   104
          moreover
lp15@67998
   105
          have "(\<chi> i j. (\<chi> i j. A $ i $ Fun.swap k l id j) $ i $ Fun.swap k l id j) = A"
lp15@67998
   106
            by (metis (no_types, lifting) id_apply o_apply swap_id_idempotent vec_lambda_unique vec_lambda_unique)
lp15@67998
   107
          ultimately show ?thesis
lp15@67998
   108
            by simp
lp15@67998
   109
        qed
lp15@67998
   110
      qed
lp15@67998
   111
    qed
lp15@67998
   112
  qed
lp15@67998
   113
  then show ?thesis
lp15@67998
   114
    by blast
lp15@67998
   115
qed
lp15@67998
   116
lp15@67998
   117
lemma induct_matrix_elementary:
lp15@67999
   118
  fixes P :: "real^'n^'n \<Rightarrow> bool"
lp15@67998
   119
  assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
lp15@67998
   120
    and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
lp15@67998
   121
    and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
lp15@67998
   122
    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
lp15@67998
   123
    and idplus: "\<And>m n c. m \<noteq> n \<Longrightarrow> P(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))"
lp15@67998
   124
  shows "P A"
lp15@67998
   125
proof -
lp15@67998
   126
  have swap: "P (\<chi> i j. A $ i $ Fun.swap m n id j)"  (is "P ?C")
lp15@67998
   127
    if "P A" "m \<noteq> n" for A m n
lp15@67998
   128
  proof -
lp15@67998
   129
    have "A ** (\<chi> i j. mat 1 $ i $ Fun.swap m n id j) = ?C"
lp15@67998
   130
      by (simp add: matrix_matrix_mult_def mat_def vec_eq_iff if_distrib sum.delta_remove)
lp15@67998
   131
    then show ?thesis
lp15@67998
   132
      using mult swap1 that by metis
lp15@67998
   133
  qed
lp15@67998
   134
  have row: "P (\<chi> i. if i = m then row m A + c *\<^sub>R row n A else row i A)"  (is "P ?C")
lp15@67998
   135
    if "P A" "m \<noteq> n" for A m n c
lp15@67998
   136
  proof -
lp15@67998
   137
    let ?B = "\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j)"
lp15@67998
   138
    have "?B ** A = ?C"
lp15@67998
   139
      using \<open>m \<noteq> n\<close> unfolding matrix_matrix_mult_def row_def of_bool_def
lp15@67998
   140
      by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
lp15@67998
   141
    then show ?thesis
lp15@67998
   142
      by (rule subst) (auto simp: that mult idplus)
lp15@67998
   143
  qed
lp15@67998
   144
  show ?thesis
lp15@67998
   145
    by (rule induct_matrix_row_operations [OF zero_row diagonal swap row])
lp15@67998
   146
qed
lp15@67998
   147
lp15@67998
   148
lemma induct_matrix_elementary_alt:
lp15@67999
   149
  fixes P :: "real^'n^'n \<Rightarrow> bool"
lp15@67998
   150
  assumes mult: "\<And>A B. \<lbrakk>P A; P B\<rbrakk> \<Longrightarrow> P(A ** B)"
lp15@67998
   151
    and zero_row: "\<And>A i. row i A = 0 \<Longrightarrow> P A"
lp15@67998
   152
    and diagonal: "\<And>A. (\<And>i j. i \<noteq> j \<Longrightarrow> A$i$j = 0) \<Longrightarrow> P A"
lp15@67998
   153
    and swap1: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
lp15@67998
   154
    and idplus: "\<And>m n. m \<noteq> n \<Longrightarrow> P(\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j))"
lp15@67998
   155
  shows "P A"
lp15@67998
   156
proof -
lp15@67998
   157
  have *: "P (\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j))"
lp15@67998
   158
    if "m \<noteq> n" for m n c
lp15@67998
   159
  proof (cases "c = 0")
lp15@67998
   160
    case True
lp15@67998
   161
    with diagonal show ?thesis by auto
lp15@67998
   162
  next
lp15@67998
   163
    case False
lp15@67998
   164
    then have eq: "(\<chi> i j. if i = m \<and> j = n then c else of_bool (i = j)) =
lp15@67998
   165
                      (\<chi> i j. if i = j then (if j = n then inverse c else 1) else 0) **
lp15@67998
   166
                      (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)) **
lp15@67998
   167
                      (\<chi> i j. if i = j then if j = n then c else 1 else 0)"
lp15@67998
   168
      using \<open>m \<noteq> n\<close>
lp15@67998
   169
      apply (simp add: matrix_matrix_mult_def vec_eq_iff of_bool_def if_distrib [of "\<lambda>x. y * x" for y] cong: if_cong)
lp15@67998
   170
      apply (simp add: if_if_eq_conj sum.neutral conj_commute cong: conj_cong)
lp15@67998
   171
      done
lp15@67998
   172
    show ?thesis
lp15@67998
   173
      apply (subst eq)
lp15@67998
   174
      apply (intro mult idplus that)
lp15@67998
   175
       apply (auto intro: diagonal)
lp15@67998
   176
      done
lp15@67998
   177
  qed
lp15@67998
   178
  show ?thesis
lp15@67998
   179
    by (rule induct_matrix_elementary) (auto intro: assms *)
lp15@67998
   180
qed
lp15@67998
   181
lp15@67998
   182
lemma induct_linear_elementary:
lp15@67998
   183
  fixes f :: "real^'n \<Rightarrow> real^'n"
lp15@67998
   184
  assumes "linear f"
lp15@67998
   185
    and comp: "\<And>f g. \<lbrakk>linear f; linear g; P f; P g\<rbrakk> \<Longrightarrow> P(f \<circ> g)"
lp15@67998
   186
    and zeroes: "\<And>f i. \<lbrakk>linear f; \<And>x. (f x) $ i = 0\<rbrakk> \<Longrightarrow> P f"
lp15@67998
   187
    and const: "\<And>c. P(\<lambda>x. \<chi> i. c i * x$i)"
lp15@67998
   188
    and swap: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. x $ Fun.swap m n id i)"
lp15@67998
   189
    and idplus: "\<And>m n::'n. m \<noteq> n \<Longrightarrow> P(\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i)"
lp15@67998
   190
  shows "P f"
lp15@67998
   191
proof -
lp15@67998
   192
  have "P (( *v) A)" for A
lp15@67998
   193
  proof (rule induct_matrix_elementary_alt)
lp15@67998
   194
    fix A B
lp15@67998
   195
    assume "P (( *v) A)" and "P (( *v) B)"
lp15@67998
   196
    then show "P (( *v) (A ** B))"
lp15@67998
   197
      by (metis (no_types, lifting) comp linear_compose matrix_compose matrix_eq matrix_vector_mul matrix_vector_mul_linear)
lp15@67998
   198
  next
lp15@67999
   199
    fix A :: "real^'n^'n" and i
lp15@67998
   200
    assume "row i A = 0"
lp15@67998
   201
    then show "P (( *v) A)"
lp15@67998
   202
      by (metis inner_zero_left matrix_vector_mul_component matrix_vector_mul_linear row_def vec_eq_iff vec_lambda_beta zeroes)
lp15@67998
   203
  next
lp15@67999
   204
    fix A :: "real^'n^'n"
lp15@67998
   205
    assume 0: "\<And>i j. i \<noteq> j \<Longrightarrow> A $ i $ j = 0"
lp15@67999
   206
    have "A $ i $ i * x $ i = (\<Sum>j\<in>UNIV. A $ i $ j * x $ j)" for x and i :: "'n"
lp15@67998
   207
      by (simp add: 0 comm_monoid_add_class.sum.remove [where x=i])
lp15@67998
   208
    then have "(\<lambda>x. \<chi> i. A $ i $ i * x $ i) = (( *v) A)"
lp15@67998
   209
      by (auto simp: 0 matrix_vector_mult_def)
lp15@67998
   210
    then show "P (( *v) A)"
lp15@67998
   211
      using const [of "\<lambda>i. A $ i $ i"] by simp
lp15@67998
   212
  next
lp15@67998
   213
    fix m n :: "'n"
lp15@67998
   214
    assume "m \<noteq> n"
lp15@67998
   215
    have eq: "(\<Sum>j\<in>UNIV. if i = Fun.swap m n id j then x $ j else 0) =
lp15@67998
   216
              (\<Sum>j\<in>UNIV. if j = Fun.swap m n id i then x $ j else 0)"
lp15@67999
   217
      for i and x :: "real^'n"
lp15@67998
   218
      unfolding swap_def by (rule sum.cong) auto
lp15@67998
   219
    have "(\<lambda>x::real^'n. \<chi> i. x $ Fun.swap m n id i) = (( *v) (\<chi> i j. if i = Fun.swap m n id j then 1 else 0))"
lp15@67998
   220
      by (auto simp: mat_def matrix_vector_mult_def eq if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
lp15@67998
   221
    with swap [OF \<open>m \<noteq> n\<close>] show "P (( *v) (\<chi> i j. mat 1 $ i $ Fun.swap m n id j))"
lp15@67998
   222
      by (simp add: mat_def matrix_vector_mult_def)
lp15@67998
   223
  next
lp15@67998
   224
    fix m n :: "'n"
lp15@67998
   225
    assume "m \<noteq> n"
lp15@67999
   226
    then have "x $ m + x $ n = (\<Sum>j\<in>UNIV. of_bool (j = n \<or> m = j) * x $ j)" for x :: "real^'n"
lp15@67998
   227
      by (auto simp: of_bool_def if_distrib [of "\<lambda>x. x * y" for y] sum.remove cong: if_cong)
lp15@67998
   228
    then have "(\<lambda>x::real^'n. \<chi> i. if i = m then x $ m + x $ n else x $ i) =
lp15@67998
   229
               (( *v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
lp15@67998
   230
      unfolding matrix_vector_mult_def of_bool_def
lp15@67998
   231
      by (auto simp: vec_eq_iff if_distrib [of "\<lambda>x. x * y" for y] cong: if_cong)
lp15@67998
   232
    then show "P (( *v) (\<chi> i j. of_bool (i = m \<and> j = n \<or> i = j)))"
lp15@67998
   233
      using idplus [OF \<open>m \<noteq> n\<close>] by simp
lp15@67998
   234
  qed
lp15@67998
   235
  then show ?thesis
lp15@67998
   236
    by (metis \<open>linear f\<close> matrix_vector_mul)
lp15@67998
   237
qed
lp15@67998
   238
lp15@67998
   239
lp15@67998
   240
proposition
lp15@67998
   241
  fixes a :: "real^'n"
lp15@67998
   242
  assumes "m \<noteq> n" and ab_ne: "cbox a b \<noteq> {}" and an: "0 \<le> a$n"
lp15@67998
   243
  shows measurable_shear_interval: "(\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i) ` (cbox a b) \<in> lmeasurable"
lp15@67998
   244
       (is  "?f ` _ \<in> _")
lp15@67998
   245
   and measure_shear_interval: "measure lebesgue ((\<lambda>x. \<chi> i. if i = m then x$m + x$n else x$i) ` cbox a b)
lp15@67998
   246
               = measure lebesgue (cbox a b)" (is "?Q")
lp15@67998
   247
proof -
lp15@67998
   248
  have lin: "linear ?f"
lp15@67998
   249
    by (force simp: plus_vec_def scaleR_vec_def algebra_simps intro: linearI)
lp15@67998
   250
  show fab: "?f ` cbox a b \<in> lmeasurable"
lp15@67998
   251
    by (simp add: lin measurable_linear_image_interval)
lp15@67998
   252
  let ?c = "\<chi> i. if i = m then b$m + b$n else b$i"
lp15@67998
   253
  let ?mn = "axis m 1 - axis n (1::real)"
lp15@67998
   254
  have eq1: "measure lebesgue (cbox a ?c)
lp15@67998
   255
            = measure lebesgue (?f ` cbox a b)
lp15@67998
   256
            + measure lebesgue (cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a$m})
lp15@67998
   257
            + measure lebesgue (cbox a ?c \<inter> {x. ?mn \<bullet> x \<ge> b$m})"
lp15@67998
   258
  proof (rule measure_Un3_negligible)
lp15@67998
   259
    show "cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a$m} \<in> lmeasurable" "cbox a ?c \<inter> {x. ?mn \<bullet> x \<ge> b$m} \<in> lmeasurable"
lp15@67998
   260
      by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurable_convex)
lp15@67998
   261
    have "negligible {x. ?mn \<bullet> x = a$m}"
lp15@67998
   262
      by (metis \<open>m \<noteq> n\<close> axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
lp15@67998
   263
    moreover have "?f ` cbox a b \<inter> (cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a $ m}) \<subseteq> {x. ?mn \<bullet> x = a$m}"
lp15@67998
   264
      using \<open>m \<noteq> n\<close> antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis')
lp15@67998
   265
    ultimately show "negligible ((?f ` cbox a b) \<inter> (cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a $ m}))"
lp15@67998
   266
      by (rule negligible_subset)
lp15@67998
   267
    have "negligible {x. ?mn \<bullet> x = b$m}"
lp15@67998
   268
      by (metis \<open>m \<noteq> n\<close> axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
lp15@67998
   269
    moreover have "(?f ` cbox a b) \<inter> (cbox a ?c \<inter> {x. ?mn \<bullet> x \<ge> b$m}) \<subseteq> {x. ?mn \<bullet> x = b$m}"
lp15@67998
   270
      using \<open>m \<noteq> n\<close> antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis')
lp15@67998
   271
    ultimately show "negligible (?f ` cbox a b \<inter> (cbox a ?c \<inter> {x. ?mn \<bullet> x \<ge> b$m}))"
lp15@67998
   272
      by (rule negligible_subset)
lp15@67998
   273
    have "negligible {x. ?mn \<bullet> x = b$m}"
lp15@67998
   274
      by (metis \<open>m \<noteq> n\<close> axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
lp15@67998
   275
    moreover have "(cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a $ m} \<inter> (cbox a ?c \<inter> {x. ?mn \<bullet> x \<ge> b$m})) \<subseteq> {x. ?mn \<bullet> x = b$m}"
lp15@67998
   276
      using \<open>m \<noteq> n\<close> ab_ne
lp15@67998
   277
      apply (auto simp: algebra_simps mem_box_cart inner_axis')
lp15@67998
   278
      apply (drule_tac x=m in spec)+
lp15@67998
   279
      apply simp
lp15@67998
   280
      done
lp15@67998
   281
    ultimately show "negligible (cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a $ m} \<inter> (cbox a ?c \<inter> {x. ?mn \<bullet> x \<ge> b$m}))"
lp15@67998
   282
      by (rule negligible_subset)
lp15@67998
   283
    show "?f ` cbox a b \<union> cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a $ m} \<union> cbox a ?c \<inter> {x. ?mn \<bullet> x \<ge> b$m} = cbox a ?c" (is "?lhs = _")
lp15@67998
   284
    proof
lp15@67998
   285
      show "?lhs \<subseteq> cbox a ?c"
lp15@67998
   286
        by (auto simp: mem_box_cart add_mono) (meson add_increasing2 an order_trans)
lp15@67998
   287
      show "cbox a ?c \<subseteq> ?lhs"
lp15@67998
   288
        apply (auto simp: algebra_simps image_iff inner_axis' lambda_add_Galois [OF \<open>m \<noteq> n\<close>])
lp15@67998
   289
        apply (auto simp: mem_box_cart split: if_split_asm)
lp15@67998
   290
        done
lp15@67998
   291
    qed
lp15@67998
   292
  qed (fact fab)
lp15@67998
   293
  let ?d = "\<chi> i. if i = m then a $ m - b $ m else 0"
lp15@67998
   294
  have eq2: "measure lebesgue (cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a $ m}) + measure lebesgue (cbox a ?c \<inter> {x. ?mn \<bullet> x \<ge> b$m})
lp15@67998
   295
           = measure lebesgue (cbox a (\<chi> i. if i = m then a $ m + b $ n else b $ i))"
lp15@67998
   296
  proof (rule measure_translate_add[of "cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a$m}" "cbox a ?c \<inter> {x. ?mn \<bullet> x \<ge> b$m}"
lp15@67998
   297
     "(\<chi> i. if i = m then a$m - b$m else 0)" "cbox a (\<chi> i. if i = m then a$m + b$n else b$i)"])
lp15@67998
   298
    show "(cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a$m}) \<in> lmeasurable"
lp15@67998
   299
      "cbox a ?c \<inter> {x. ?mn \<bullet> x \<ge> b$m} \<in> lmeasurable"
lp15@67998
   300
      by (auto simp: convex_Int convex_halfspace_le convex_halfspace_ge bounded_Int measurable_convex)
lp15@67998
   301
    have "\<And>x. \<lbrakk>x $ n + a $ m \<le> x $ m\<rbrakk>
lp15@67998
   302
         \<Longrightarrow> x \<in> (+) (\<chi> i. if i = m then a $ m - b $ m else 0) ` {x. x $ n + b $ m \<le> x $ m}"
lp15@67998
   303
      using \<open>m \<noteq> n\<close>
lp15@67998
   304
      by (rule_tac x="x - (\<chi> i. if i = m then a$m - b$m else 0)" in image_eqI)
lp15@67998
   305
         (simp_all add: mem_box_cart)
lp15@67998
   306
    then have imeq: "(+) ?d ` {x. b $ m \<le> ?mn \<bullet> x} = {x. a $ m \<le> ?mn \<bullet> x}"
lp15@67998
   307
      using \<open>m \<noteq> n\<close> by (auto simp: mem_box_cart inner_axis' algebra_simps)
lp15@67998
   308
    have "\<And>x. \<lbrakk>0 \<le> a $ n; x $ n + a $ m \<le> x $ m;
lp15@67998
   309
                \<forall>i. i \<noteq> m \<longrightarrow> a $ i \<le> x $ i \<and> x $ i \<le> b $ i\<rbrakk>
lp15@67998
   310
         \<Longrightarrow> a $ m \<le> x $ m"
lp15@67998
   311
      using \<open>m \<noteq> n\<close>  by force
lp15@67998
   312
    then have "(+) ?d ` (cbox a ?c \<inter> {x. b $ m \<le> ?mn \<bullet> x})
lp15@67998
   313
            = cbox a (\<chi> i. if i = m then a $ m + b $ n else b $ i) \<inter> {x. a $ m \<le> ?mn \<bullet> x}"
lp15@67998
   314
      using an ab_ne
lp15@67998
   315
      apply (simp add: cbox_translation [symmetric] translation_Int interval_ne_empty_cart imeq)
lp15@67998
   316
      apply (auto simp: mem_box_cart inner_axis' algebra_simps if_distrib all_if_distrib)
lp15@67998
   317
      by (metis (full_types) add_mono mult_2_right)
lp15@67998
   318
    then show "cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a $ m} \<union>
lp15@67998
   319
          (+) ?d ` (cbox a ?c \<inter> {x. b $ m \<le> ?mn \<bullet> x}) =
lp15@67998
   320
          cbox a (\<chi> i. if i = m then a $ m + b $ n else b $ i)"  (is "?lhs = ?rhs")
lp15@67998
   321
      using an \<open>m \<noteq> n\<close>
lp15@67998
   322
      apply (auto simp: mem_box_cart inner_axis' algebra_simps if_distrib all_if_distrib, force)
lp15@67998
   323
        apply (drule_tac x=n in spec)+
lp15@67998
   324
      by (meson ab_ne add_mono_thms_linordered_semiring(3) dual_order.trans interval_ne_empty_cart(1))
lp15@67998
   325
    have "negligible{x. ?mn \<bullet> x = a$m}"
lp15@67998
   326
      by (metis \<open>m \<noteq> n\<close> axis_index_axis eq_iff_diff_eq_0 negligible_hyperplane)
lp15@67998
   327
    moreover have "(cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a $ m} \<inter>
lp15@67998
   328
                                 (+) ?d ` (cbox a ?c \<inter> {x. b $ m \<le> ?mn \<bullet> x})) \<subseteq> {x. ?mn \<bullet> x = a$m}"
lp15@67998
   329
      using \<open>m \<noteq> n\<close> antisym_conv by (fastforce simp: algebra_simps mem_box_cart inner_axis')
lp15@67998
   330
    ultimately show "negligible (cbox a ?c \<inter> {x. ?mn \<bullet> x \<le> a $ m} \<inter>
lp15@67998
   331
                                 (+) ?d ` (cbox a ?c \<inter> {x. b $ m \<le> ?mn \<bullet> x}))"
lp15@67998
   332
      by (rule negligible_subset)
lp15@67998
   333
  qed
lp15@67998
   334
  have ac_ne: "cbox a ?c \<noteq> {}"
lp15@67998
   335
    using ab_ne an
lp15@67998
   336
    by (clarsimp simp: interval_eq_empty_cart) (meson add_less_same_cancel1 le_less_linear less_le_trans)
lp15@67998
   337
  have ax_ne: "cbox a (\<chi> i. if i = m then a $ m + b $ n else b $ i) \<noteq> {}"
lp15@67998
   338
    using ab_ne an
lp15@67998
   339
    by (clarsimp simp: interval_eq_empty_cart) (meson add_less_same_cancel1 le_less_linear less_le_trans)
lp15@67998
   340
  have eq3: "measure lebesgue (cbox a ?c) = measure lebesgue (cbox a (\<chi> i. if i = m then a$m + b$n else b$i)) + measure lebesgue (cbox a b)"
lp15@67998
   341
    by (simp add: content_cbox_if_cart ab_ne ac_ne ax_ne algebra_simps prod.delta_remove
lp15@67998
   342
             if_distrib [of "\<lambda>u. u - z" for z] prod.remove)
lp15@67998
   343
  show ?Q
lp15@67998
   344
    using eq1 eq2 eq3
lp15@67998
   345
    by (simp add: algebra_simps)
lp15@67998
   346
qed
lp15@67998
   347
lp15@67998
   348
lp15@67998
   349
proposition
lp15@67998
   350
  fixes S :: "(real^'n) set"
lp15@67998
   351
  assumes "S \<in> lmeasurable"
lp15@67998
   352
  shows measurable_stretch: "((\<lambda>x. \<chi> k. m k * x$k) ` S) \<in> lmeasurable" (is  "?f ` S \<in> _")
lp15@67998
   353
    and measure_stretch: "measure lebesgue ((\<lambda>x. \<chi> k. m k * x$k) ` S) = \<bar>prod m UNIV\<bar> * measure lebesgue S"
lp15@67998
   354
    (is "?MEQ")
lp15@67998
   355
proof -
lp15@67998
   356
  have "(?f ` S) \<in> lmeasurable \<and> ?MEQ"
lp15@67998
   357
  proof (cases "\<forall>k. m k \<noteq> 0")
lp15@67998
   358
    case True
lp15@67998
   359
    have m0: "0 < \<bar>prod m UNIV\<bar>"
lp15@67998
   360
      using True by simp
lp15@67998
   361
    have "(indicat_real (?f ` S) has_integral \<bar>prod m UNIV\<bar> * measure lebesgue S) UNIV"
lp15@67998
   362
    proof (clarsimp simp add: has_integral_alt [where i=UNIV])
lp15@67998
   363
      fix e :: "real"
lp15@67998
   364
      assume "e > 0"
lp15@67998
   365
      have "(indicat_real S has_integral (measure lebesgue S)) UNIV"
lp15@67998
   366
        using assms lmeasurable_iff_has_integral by blast
lp15@67998
   367
      then obtain B where "B>0"
lp15@67998
   368
        and B: "\<And>a b. ball 0 B \<subseteq> cbox a b \<Longrightarrow>
lp15@67998
   369
                        \<exists>z. (indicat_real S has_integral z) (cbox a b) \<and>
lp15@67998
   370
                            \<bar>z - measure lebesgue S\<bar> < e / \<bar>prod m UNIV\<bar>"
lp15@67998
   371
        by (simp add: has_integral_alt [where i=UNIV]) (metis (full_types) divide_pos_pos m0  m0 \<open>e > 0\<close>)
lp15@67998
   372
      show "\<exists>B>0. \<forall>a b. ball 0 B \<subseteq> cbox a b \<longrightarrow>
lp15@67998
   373
                  (\<exists>z. (indicat_real (?f ` S) has_integral z) (cbox a b) \<and>
lp15@67998
   374
                       \<bar>z - \<bar>prod m UNIV\<bar> * measure lebesgue S\<bar> < e)"
lp15@67998
   375
      proof (intro exI conjI allI)
lp15@67998
   376
        let ?C = "Max (range (\<lambda>k. \<bar>m k\<bar>)) * B"
lp15@67998
   377
        show "?C > 0"
lp15@67998
   378
          using True \<open>B > 0\<close> by (simp add: Max_gr_iff)
lp15@67998
   379
        show "ball 0 ?C \<subseteq> cbox u v \<longrightarrow>
lp15@67998
   380
                  (\<exists>z. (indicat_real (?f ` S) has_integral z) (cbox u v) \<and>
lp15@67998
   381
                       \<bar>z - \<bar>prod m UNIV\<bar> * measure lebesgue S\<bar> < e)" for u v
lp15@67998
   382
        proof
lp15@67998
   383
          assume uv: "ball 0 ?C \<subseteq> cbox u v"
lp15@67998
   384
          with \<open>?C > 0\<close> have cbox_ne: "cbox u v \<noteq> {}"
lp15@67998
   385
            using centre_in_ball by blast
lp15@67998
   386
          let ?\<alpha> = "\<lambda>k. u$k / m k"
lp15@67998
   387
          let ?\<beta> = "\<lambda>k. v$k / m k"
lp15@67998
   388
          have invm0: "\<And>k. inverse (m k) \<noteq> 0"
lp15@67998
   389
            using True by auto
lp15@67998
   390
          have "ball 0 B \<subseteq> (\<lambda>x. \<chi> k. x $ k / m k) ` ball 0 ?C"
lp15@67998
   391
          proof clarsimp
lp15@67999
   392
            fix x :: "real^'n"
lp15@67998
   393
            assume x: "norm x < B"
lp15@67998
   394
            have [simp]: "\<bar>Max (range (\<lambda>k. \<bar>m k\<bar>))\<bar> = Max (range (\<lambda>k. \<bar>m k\<bar>))"
lp15@67998
   395
              by (meson Max_ge abs_ge_zero abs_of_nonneg finite finite_imageI order_trans rangeI)
lp15@67998
   396
            have "norm (\<chi> k. m k * x $ k) \<le> norm (Max (range (\<lambda>k. \<bar>m k\<bar>)) *\<^sub>R x)"
lp15@67998
   397
              by (rule norm_le_componentwise_cart) (auto simp: abs_mult intro: mult_right_mono)
lp15@67998
   398
            also have "\<dots> < ?C"
lp15@67998
   399
              using x by simp (metis \<open>B > 0\<close> \<open>?C > 0\<close> mult.commute real_mult_less_iff1 zero_less_mult_pos)
lp15@67998
   400
            finally have "norm (\<chi> k. m k * x $ k) < ?C" .
lp15@67998
   401
            then show "x \<in> (\<lambda>x. \<chi> k. x $ k / m k) ` ball 0 ?C"
lp15@67998
   402
              using stretch_Galois [of "inverse \<circ> m"] True by (auto simp: image_iff field_simps)
lp15@67998
   403
          qed
lp15@67998
   404
          then have Bsub: "ball 0 B \<subseteq> cbox (\<chi> k. min (?\<alpha> k) (?\<beta> k)) (\<chi> k. max (?\<alpha> k) (?\<beta> k))"
lp15@67998
   405
            using cbox_ne uv image_stretch_interval_cart [of "inverse \<circ> m" u v, symmetric]
lp15@67998
   406
            by (force simp: field_simps)
lp15@67998
   407
          obtain z where zint: "(indicat_real S has_integral z) (cbox (\<chi> k. min (?\<alpha> k) (?\<beta> k)) (\<chi> k. max (?\<alpha> k) (?\<beta> k)))"
lp15@67998
   408
                   and zless: "\<bar>z - measure lebesgue S\<bar> < e / \<bar>prod m UNIV\<bar>"
lp15@67998
   409
            using B [OF Bsub] by blast
lp15@67998
   410
          have ind: "indicat_real (?f ` S) = (\<lambda>x. indicator S (\<chi> k. x$k / m k))"
lp15@67998
   411
            using True stretch_Galois [of m] by (force simp: indicator_def)
lp15@67998
   412
          show "\<exists>z. (indicat_real (?f ` S) has_integral z) (cbox u v) \<and>
lp15@67998
   413
                       \<bar>z - \<bar>prod m UNIV\<bar> * measure lebesgue S\<bar> < e"
lp15@67998
   414
          proof (simp add: ind, intro conjI exI)
lp15@67998
   415
            have "((\<lambda>x. indicat_real S (\<chi> k. x $ k/ m k)) has_integral z *\<^sub>R \<bar>prod m UNIV\<bar>)
lp15@67998
   416
                ((\<lambda>x. \<chi> k. x $ k * m k) ` cbox (\<chi> k. min (?\<alpha> k) (?\<beta> k)) (\<chi> k. max (?\<alpha> k) (?\<beta> k)))"
lp15@67998
   417
              using True has_integral_stretch_cart [OF zint, of "inverse \<circ> m"]
lp15@67998
   418
              by (simp add: field_simps prod_dividef)
lp15@67998
   419
            moreover have "((\<lambda>x. \<chi> k. x $ k * m k) ` cbox (\<chi> k. min (?\<alpha> k) (?\<beta> k)) (\<chi> k. max (?\<alpha> k) (?\<beta> k))) = cbox u v"
lp15@67998
   420
              using True image_stretch_interval_cart [of "inverse \<circ> m" u v, symmetric]
lp15@67998
   421
                image_stretch_interval_cart [of "\<lambda>k. 1" u v, symmetric] \<open>cbox u v \<noteq> {}\<close>
lp15@67998
   422
              by (simp add: field_simps image_comp o_def)
lp15@67998
   423
            ultimately show "((\<lambda>x. indicat_real S (\<chi> k. x $ k/ m k)) has_integral z *\<^sub>R \<bar>prod m UNIV\<bar>) (cbox u v)"
lp15@67998
   424
              by simp
lp15@67998
   425
            have "\<bar>z *\<^sub>R \<bar>prod m UNIV\<bar> - \<bar>prod m UNIV\<bar> * measure lebesgue S\<bar>
lp15@67998
   426
                 = \<bar>prod m UNIV\<bar> * \<bar>z - measure lebesgue S\<bar>"
lp15@67998
   427
              by (metis (no_types, hide_lams) abs_abs abs_scaleR mult.commute real_scaleR_def right_diff_distrib')
lp15@67998
   428
            also have "\<dots> < e"
lp15@67998
   429
              using zless True by (simp add: field_simps)
lp15@67998
   430
            finally show "\<bar>z *\<^sub>R \<bar>prod m UNIV\<bar> - \<bar>prod m UNIV\<bar> * measure lebesgue S\<bar> < e" .
lp15@67998
   431
          qed
lp15@67998
   432
        qed
lp15@67998
   433
      qed
lp15@67998
   434
    qed
lp15@67998
   435
    then show ?thesis
lp15@67998
   436
      by (auto simp: has_integral_integrable integral_unique lmeasure_integral_UNIV measurable_integrable)
lp15@67998
   437
  next
lp15@67998
   438
    case False
lp15@67998
   439
    then obtain k where "m k = 0" and prm: "prod m UNIV = 0"
lp15@67998
   440
      by auto
lp15@67998
   441
    have nfS: "negligible (?f ` S)"
lp15@67998
   442
      by (rule negligible_subset [OF negligible_standard_hyperplane_cart]) (use \<open>m k = 0\<close> in auto)
lp15@67998
   443
    then have "(?f ` S) \<in> lmeasurable"
lp15@67998
   444
      by (simp add: negligible_iff_measure)
lp15@67998
   445
    with nfS show ?thesis
lp15@67998
   446
      by (simp add: prm negligible_iff_measure0)
lp15@67998
   447
  qed
lp15@67998
   448
  then show "(?f ` S) \<in> lmeasurable" ?MEQ
lp15@67998
   449
    by metis+
lp15@67998
   450
qed
lp15@67998
   451
lp15@67998
   452
lp15@67998
   453
proposition
lp15@67998
   454
 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
lp15@67998
   455
  assumes "linear f" "S \<in> lmeasurable"
lp15@67998
   456
  shows measurable_linear_image: "(f ` S) \<in> lmeasurable"
lp15@67998
   457
    and measure_linear_image: "measure lebesgue (f ` S) = \<bar>det (matrix f)\<bar> * measure lebesgue S" (is "?Q f S")
lp15@67998
   458
proof -
lp15@67998
   459
  have "\<forall>S \<in> lmeasurable. (f ` S) \<in> lmeasurable \<and> ?Q f S"
lp15@67998
   460
  proof (rule induct_linear_elementary [OF \<open>linear f\<close>]; intro ballI)
lp15@67998
   461
    fix f g and S :: "(real,'n) vec set"
lp15@67998
   462
    assume "linear f" and "linear g"
lp15@67998
   463
      and f [rule_format]: "\<forall>S \<in> lmeasurable. f ` S \<in> lmeasurable \<and> ?Q f S"
lp15@67998
   464
      and g [rule_format]: "\<forall>S \<in> lmeasurable. g ` S \<in> lmeasurable \<and> ?Q g S"
lp15@67998
   465
      and S: "S \<in> lmeasurable"
lp15@67998
   466
    then have gS: "g ` S \<in> lmeasurable"
lp15@67998
   467
      by blast
lp15@67998
   468
    show "(f \<circ> g) ` S \<in> lmeasurable \<and> ?Q (f \<circ> g) S"
lp15@67998
   469
      using f [OF gS] g [OF S] matrix_compose [OF \<open>linear g\<close> \<open>linear f\<close>]
lp15@67998
   470
      by (simp add: o_def image_comp abs_mult det_mul)
lp15@67998
   471
  next
lp15@67999
   472
    fix f :: "real^'n::_ \<Rightarrow> real^'n::_" and i and S :: "(real^'n::_) set"
lp15@67998
   473
    assume "linear f" and 0: "\<And>x. f x $ i = 0" and "S \<in> lmeasurable"
lp15@67998
   474
    then have "\<not> inj f"
lp15@67998
   475
      by (metis (full_types) linear_injective_imp_surjective one_neq_zero surjE vec_component)
lp15@67998
   476
    have detf: "det (matrix f) = 0"
lp15@67998
   477
      by (metis "0" \<open>linear f\<close> invertible_det_nz invertible_right_inverse matrix_right_invertible_surjective matrix_vector_mul surjE vec_component)
lp15@67998
   478
    show "f ` S \<in> lmeasurable \<and> ?Q f S"
lp15@67998
   479
    proof
lp15@67998
   480
      show "f ` S \<in> lmeasurable"
lp15@67998
   481
        using lmeasurable_iff_indicator_has_integral \<open>linear f\<close> \<open>\<not> inj f\<close> negligible_UNIV negligible_linear_singular_image by blast
lp15@67998
   482
      have "measure lebesgue (f ` S) = 0"
lp15@67998
   483
        by (meson \<open>\<not> inj f\<close> \<open>linear f\<close> negligible_imp_measure0 negligible_linear_singular_image)
lp15@67998
   484
      also have "\<dots> = \<bar>det (matrix f)\<bar> * measure lebesgue S"
lp15@67998
   485
        by (simp add: detf)
lp15@67998
   486
      finally show "?Q f S" .
lp15@67998
   487
    qed
lp15@67998
   488
  next
lp15@67999
   489
    fix c and S :: "(real^'n::_) set"
lp15@67998
   490
    assume "S \<in> lmeasurable"
lp15@67998
   491
    show "(\<lambda>a. \<chi> i. c i * a $ i) ` S \<in> lmeasurable \<and> ?Q (\<lambda>a. \<chi> i. c i * a $ i) S"
lp15@67998
   492
    proof
lp15@67998
   493
      show "(\<lambda>a. \<chi> i. c i * a $ i) ` S \<in> lmeasurable"
lp15@67998
   494
        by (simp add: \<open>S \<in> lmeasurable\<close> measurable_stretch)
lp15@67998
   495
      show "?Q (\<lambda>a. \<chi> i. c i * a $ i) S"
lp15@67998
   496
        by (simp add: measure_stretch [OF \<open>S \<in> lmeasurable\<close>, of c] axis_def matrix_def det_diagonal)
lp15@67998
   497
    qed
lp15@67998
   498
  next
lp15@67998
   499
    fix m :: "'n" and n :: "'n" and S :: "(real, 'n) vec set"
lp15@67998
   500
    assume "m \<noteq> n" and "S \<in> lmeasurable"
lp15@67998
   501
    let ?h = "\<lambda>v::(real, 'n) vec. \<chi> i. v $ Fun.swap m n id i"
lp15@67998
   502
    have lin: "linear ?h"
lp15@67998
   503
      by (simp add: plus_vec_def scaleR_vec_def linearI)
lp15@67998
   504
    have meq: "measure lebesgue ((\<lambda>v::(real, 'n) vec. \<chi> i. v $ Fun.swap m n id i) ` cbox a b)
lp15@67998
   505
             = measure lebesgue (cbox a b)" for a b
lp15@67998
   506
    proof (cases "cbox a b = {}")
lp15@67998
   507
      case True then show ?thesis
lp15@67998
   508
        by simp
lp15@67998
   509
    next
lp15@67998
   510
      case False
lp15@67998
   511
      then have him: "?h ` (cbox a b) \<noteq> {}"
lp15@67998
   512
        by blast
lp15@67998
   513
      have eq: "?h ` (cbox a b) = cbox (?h a) (?h b)"
lp15@67998
   514
        by (auto simp: image_iff lambda_swap_Galois mem_box_cart) (metis swap_id_eq)+
lp15@67998
   515
      show ?thesis
lp15@67998
   516
        using him prod.permute [OF permutes_swap_id, where S=UNIV and g="\<lambda>i. (b - a)$i", symmetric]
lp15@67998
   517
        by (simp add: eq content_cbox_cart False)
lp15@67998
   518
    qed
lp15@67998
   519
    have "(\<chi> i j. if Fun.swap m n id i = j then 1 else 0) = (\<chi> i j. if j = Fun.swap m n id i then 1 else (0::real))"
lp15@67998
   520
      by (auto intro!: Cart_lambda_cong)
lp15@67998
   521
    then have "matrix ?h = transpose(\<chi> i j. mat 1 $ i $ Fun.swap m n id j)"
lp15@67998
   522
      by (auto simp: matrix_eq transpose_def axis_def mat_def matrix_def)
lp15@67998
   523
    then have 1: "\<bar>det (matrix ?h)\<bar> = 1"
lp15@67998
   524
      by (simp add: det_permute_columns permutes_swap_id sign_swap_id abs_mult)
lp15@67998
   525
    show "?h ` S \<in> lmeasurable \<and> ?Q ?h S"
lp15@67998
   526
    proof
lp15@67998
   527
      show "?h ` S \<in> lmeasurable" "?Q ?h S"
lp15@67998
   528
        using measure_linear_sufficient [OF lin \<open>S \<in> lmeasurable\<close>] meq 1 by force+
lp15@67998
   529
    qed
lp15@67998
   530
  next
lp15@67999
   531
    fix m n :: "'n" and S :: "(real, 'n) vec set"
lp15@67998
   532
    assume "m \<noteq> n" and "S \<in> lmeasurable"
lp15@67998
   533
    let ?h = "\<lambda>v::(real, 'n) vec. \<chi> i. if i = m then v $ m + v $ n else v $ i"
lp15@67998
   534
    have lin: "linear ?h"
lp15@67998
   535
      by (auto simp: algebra_simps plus_vec_def scaleR_vec_def vec_eq_iff intro: linearI)
lp15@67998
   536
    consider "m < n" | " n < m"
lp15@67998
   537
      using \<open>m \<noteq> n\<close> less_linear by blast
lp15@67998
   538
    then have 1: "det(matrix ?h) = 1"
lp15@67998
   539
    proof cases
lp15@67998
   540
      assume "m < n"
lp15@67998
   541
      have *: "matrix ?h $ i $ j = (0::real)" if "j < i" for i j :: 'n
lp15@67998
   542
      proof -
lp15@67998
   543
        have "axis j 1 = (\<chi> n. if n = j then 1 else (0::real))"
lp15@67998
   544
          using axis_def by blast
lp15@67998
   545
        then have "(\<chi> p q. if p = m then axis q 1 $ m + axis q 1 $ n else axis q 1 $ p) $ i $ j = (0::real)"
lp15@67998
   546
          using \<open>j < i\<close> axis_def \<open>m < n\<close> by auto
lp15@67998
   547
        with \<open>m < n\<close> show ?thesis
lp15@67998
   548
          by (auto simp: matrix_def axis_def cong: if_cong)
lp15@67998
   549
      qed
lp15@67998
   550
      show ?thesis
lp15@67998
   551
        using \<open>m \<noteq> n\<close> by (subst det_upperdiagonal [OF *]) (auto simp: matrix_def axis_def cong: if_cong)
lp15@67998
   552
    next
lp15@67998
   553
      assume "n < m"
lp15@67998
   554
      have *: "matrix ?h $ i $ j = (0::real)" if "j > i" for i j :: 'n
lp15@67998
   555
      proof -
lp15@67998
   556
        have "axis j 1 = (\<chi> n. if n = j then 1 else (0::real))"
lp15@67998
   557
          using axis_def by blast
lp15@67998
   558
        then have "(\<chi> p q. if p = m then axis q 1 $ m + axis q 1 $ n else axis q 1 $ p) $ i $ j = (0::real)"
lp15@67998
   559
          using \<open>j > i\<close> axis_def \<open>m > n\<close> by auto
lp15@67998
   560
        with \<open>m > n\<close> show ?thesis
lp15@67998
   561
          by (auto simp: matrix_def axis_def cong: if_cong)
lp15@67998
   562
      qed
lp15@67998
   563
      show ?thesis
lp15@67998
   564
        using \<open>m \<noteq> n\<close>
lp15@67998
   565
        by (subst det_lowerdiagonal [OF *]) (auto simp: matrix_def axis_def cong: if_cong)
lp15@67998
   566
    qed
lp15@67998
   567
    have meq: "measure lebesgue (?h ` (cbox a b)) = measure lebesgue (cbox a b)" for a b
lp15@67998
   568
    proof (cases "cbox a b = {}")
lp15@67998
   569
      case True then show ?thesis by simp
lp15@67998
   570
    next
lp15@67998
   571
      case False
lp15@67998
   572
      then have ne: "(+) (\<chi> i. if i = n then - a $ n else 0) ` cbox a b \<noteq> {}"
lp15@67998
   573
        by auto
lp15@67998
   574
      let ?v = "\<chi> i. if i = n then - a $ n else 0"
lp15@67998
   575
      have "?h ` cbox a b
lp15@67998
   576
            = (+) (\<chi> i. if i = m \<or> i = n then a $ n else 0) ` ?h ` (+) ?v ` (cbox a b)"
lp15@67998
   577
        using \<open>m \<noteq> n\<close> unfolding image_comp o_def by (force simp: vec_eq_iff)
lp15@67998
   578
      then have "measure lebesgue (?h ` (cbox a b))
lp15@67998
   579
               = measure lebesgue ((\<lambda>v. \<chi> i. if i = m then v $ m + v $ n else v $ i) `
lp15@67998
   580
                                   (+) ?v ` cbox a b)"
lp15@67998
   581
        by (rule ssubst) (rule measure_translation)
lp15@67998
   582
      also have "\<dots> = measure lebesgue ((\<lambda>v. \<chi> i. if i = m then v $ m + v $ n else v $ i) ` cbox (?v +a) (?v + b))"
lp15@67998
   583
        by (metis (no_types, lifting) cbox_translation)
lp15@67998
   584
      also have "\<dots> = measure lebesgue ((+) (\<chi> i. if i = n then - a $ n else 0) ` cbox a b)"
lp15@67998
   585
        apply (subst measure_shear_interval)
lp15@67998
   586
        using \<open>m \<noteq> n\<close> ne apply auto
lp15@67998
   587
        apply (simp add: cbox_translation)
lp15@67998
   588
        by (metis cbox_borel cbox_translation measure_completion sets_lborel)
lp15@67998
   589
      also have "\<dots> = measure lebesgue (cbox a b)"
lp15@67998
   590
        by (rule measure_translation)
lp15@67998
   591
        finally show ?thesis .
lp15@67998
   592
      qed
lp15@67998
   593
    show "?h ` S \<in> lmeasurable \<and> ?Q ?h S"
lp15@67998
   594
      using measure_linear_sufficient [OF lin \<open>S \<in> lmeasurable\<close>] meq 1 by force
lp15@67998
   595
  qed
lp15@67998
   596
  with assms show "(f ` S) \<in> lmeasurable" "?Q f S"
lp15@67998
   597
    by metis+
lp15@67998
   598
qed
lp15@67998
   599
lp15@67998
   600
lp15@67998
   601
lemma
lp15@67998
   602
 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
lp15@67998
   603
  assumes f: "orthogonal_transformation f" and S: "S \<in> lmeasurable"
lp15@67998
   604
  shows measurable_orthogonal_image: "f ` S \<in> lmeasurable"
lp15@67998
   605
    and measure_orthogonal_image: "measure lebesgue (f ` S) = measure lebesgue S"
lp15@67998
   606
proof -
lp15@67998
   607
  have "linear f"
lp15@67998
   608
    by (simp add: f orthogonal_transformation_linear)
lp15@67998
   609
  then show "f ` S \<in> lmeasurable"
lp15@67998
   610
    by (metis S measurable_linear_image)
lp15@67998
   611
  show "measure lebesgue (f ` S) = measure lebesgue S"
lp15@67998
   612
    by (simp add: measure_linear_image \<open>linear f\<close> S f)
lp15@67998
   613
qed
lp15@67998
   614
lp15@67998
   615
subsection\<open>@{text F_sigma} and @{text G_delta} sets.\<close>
lp15@67998
   616
lp15@67998
   617
(*https://en.wikipedia.org/wiki/F\<sigma>_set*)
lp15@67998
   618
inductive fsigma :: "'a::topological_space set \<Rightarrow> bool" where
lp15@67998
   619
  "(\<And>n::nat. closed (F n)) \<Longrightarrow> fsigma (UNION UNIV F)"
lp15@67998
   620
lp15@67998
   621
inductive gdelta :: "'a::topological_space set \<Rightarrow> bool" where
lp15@67998
   622
  "(\<And>n::nat. open (F n)) \<Longrightarrow> gdelta (INTER UNIV F)"
lp15@67998
   623
lp15@67998
   624
lemma fsigma_Union_compact:
lp15@67998
   625
  fixes S :: "'a::{real_normed_vector,heine_borel} set"
lp15@67998
   626
  shows "fsigma S \<longleftrightarrow> (\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = UNION UNIV F)"
lp15@67998
   627
proof safe
lp15@67998
   628
  assume "fsigma S"
lp15@67998
   629
  then obtain F :: "nat \<Rightarrow> 'a set" where F: "range F \<subseteq> Collect closed" "S = UNION UNIV F"
lp15@67998
   630
    by (meson fsigma.cases image_subsetI mem_Collect_eq)
lp15@67998
   631
  then have "\<exists>D::nat \<Rightarrow> 'a set. range D \<subseteq> Collect compact \<and> UNION UNIV D = F i" for i
lp15@67998
   632
    using closed_Union_compact_subsets [of "F i"]
lp15@67998
   633
    by (metis image_subsetI mem_Collect_eq range_subsetD)
lp15@67998
   634
  then obtain D :: "nat \<Rightarrow> nat \<Rightarrow> 'a set"
lp15@67998
   635
    where D: "\<And>i. range (D i) \<subseteq> Collect compact \<and> UNION UNIV (D i) = F i"
lp15@67998
   636
    by metis
lp15@67998
   637
  let ?DD = "\<lambda>n. (\<lambda>(i,j). D i j) (prod_decode n)"
lp15@67998
   638
  show "\<exists>F::nat \<Rightarrow> 'a set. range F \<subseteq> Collect compact \<and> S = UNION UNIV F"
lp15@67998
   639
  proof (intro exI conjI)
lp15@67998
   640
    show "range ?DD \<subseteq> Collect compact"
lp15@67998
   641
      using D by clarsimp (metis mem_Collect_eq rangeI split_conv subsetCE surj_pair)
lp15@67998
   642
    show "S = UNION UNIV ?DD"
lp15@67998
   643
    proof
lp15@67998
   644
      show "S \<subseteq> UNION UNIV ?DD"
lp15@67998
   645
        using D F
lp15@67998
   646
        by clarsimp (metis UN_iff old.prod.case prod_decode_inverse prod_encode_eq)
lp15@67998
   647
      show "UNION UNIV ?DD \<subseteq> S"
lp15@67998
   648
        using D F  by fastforce
lp15@67998
   649
    qed
lp15@67998
   650
  qed
lp15@67998
   651
next
lp15@67998
   652
  fix F :: "nat \<Rightarrow> 'a set"
lp15@67998
   653
  assume "range F \<subseteq> Collect compact" and "S = UNION UNIV F"
lp15@67998
   654
  then show "fsigma (UNION UNIV F)"
lp15@67998
   655
    by (simp add: compact_imp_closed fsigma.intros image_subset_iff)
lp15@67998
   656
qed
lp15@67998
   657
lp15@67998
   658
lemma gdelta_imp_fsigma: "gdelta S \<Longrightarrow> fsigma (- S)"
lp15@67998
   659
proof (induction rule: gdelta.induct)
lp15@67998
   660
  case (1 F)
lp15@67998
   661
  have "- INTER UNIV F = (\<Union>i. -(F i))"
lp15@67998
   662
    by auto
lp15@67998
   663
  then show ?case
lp15@67998
   664
    by (simp add: fsigma.intros closed_Compl 1)
lp15@67998
   665
qed
lp15@67998
   666
lp15@67998
   667
lemma fsigma_imp_gdelta: "fsigma S \<Longrightarrow> gdelta (- S)"
lp15@67998
   668
proof (induction rule: fsigma.induct)
lp15@67998
   669
  case (1 F)
lp15@67998
   670
  have "- UNION UNIV F = (\<Inter>i. -(F i))"
lp15@67998
   671
    by auto
lp15@67998
   672
  then show ?case
lp15@67998
   673
    by (simp add: 1 gdelta.intros open_closed)
lp15@67998
   674
qed
lp15@67998
   675
lp15@67998
   676
lemma gdelta_complement: "gdelta(- S) \<longleftrightarrow> fsigma S"
lp15@67998
   677
  using fsigma_imp_gdelta gdelta_imp_fsigma by force
lp15@67998
   678
lp15@67998
   679
text\<open>A Lebesgue set is almost an @{text F_sigma} or @{text G_delta}.\<close>
lp15@67998
   680
lemma lebesgue_set_almost_fsigma:
lp15@67998
   681
  assumes "S \<in> sets lebesgue"
lp15@67998
   682
  obtains C T where "fsigma C" "negligible T" "C \<union> T = S" "disjnt C T"
lp15@67998
   683
proof -
lp15@67998
   684
  { fix n::nat
lp15@67998
   685
    have "\<exists>T. closed T \<and> T \<subseteq> S \<and> S - T \<in> lmeasurable \<and> measure lebesgue (S-T) < 1 / Suc n"
lp15@67998
   686
      using sets_lebesgue_inner_closed [OF assms]
lp15@67998
   687
      by (metis divide_pos_pos less_numeral_extra(1) of_nat_0_less_iff zero_less_Suc)
lp15@67998
   688
  }
lp15@67998
   689
  then obtain F where F: "\<And>n::nat. closed (F n) \<and> F n \<subseteq> S \<and> S - F n \<in> lmeasurable \<and> measure lebesgue (S - F n) < 1 / Suc n"
lp15@67998
   690
    by metis
lp15@67998
   691
  let ?C = "UNION UNIV F"
lp15@67998
   692
  show thesis
lp15@67998
   693
  proof
lp15@67998
   694
    show "fsigma ?C"
lp15@67998
   695
      using F by (simp add: fsigma.intros)
lp15@67998
   696
    show "negligible (S - ?C)"
lp15@67998
   697
    proof (clarsimp simp add: negligible_outer_le)
lp15@67998
   698
      fix e :: "real"
lp15@67998
   699
      assume "0 < e"
lp15@67998
   700
      then obtain n where n: "1 / Suc n < e"
lp15@67998
   701
        using nat_approx_posE by metis
lp15@67998
   702
      show "\<exists>T. S - (\<Union>x. F x) \<subseteq> T \<and> T \<in> lmeasurable \<and> measure lebesgue T \<le> e"
lp15@67998
   703
      proof (intro exI conjI)
lp15@67998
   704
        show "measure lebesgue (S - F n) \<le> e"
lp15@67998
   705
          by (meson F n less_trans not_le order.asym)
lp15@67998
   706
      qed (use F in auto)
lp15@67998
   707
    qed
lp15@67998
   708
    show "?C \<union> (S - ?C) = S"
lp15@67998
   709
      using F by blast
lp15@67998
   710
    show "disjnt ?C (S - ?C)"
lp15@67998
   711
      by (auto simp: disjnt_def)
lp15@67998
   712
  qed
lp15@67998
   713
qed
lp15@67998
   714
lp15@67998
   715
lemma lebesgue_set_almost_gdelta:
lp15@67998
   716
  assumes "S \<in> sets lebesgue"
lp15@67998
   717
  obtains C T where "gdelta C" "negligible T" "S \<union> T = C" "disjnt S T"
lp15@67998
   718
proof -
lp15@67998
   719
  have "-S \<in> sets lebesgue"
lp15@67998
   720
    using assms Compl_in_sets_lebesgue by blast
lp15@67998
   721
  then obtain C T where C: "fsigma C" "negligible T" "C \<union> T = -S" "disjnt C T"
lp15@67998
   722
    using lebesgue_set_almost_fsigma by metis
lp15@67998
   723
  show thesis
lp15@67998
   724
  proof
lp15@67998
   725
    show "gdelta (-C)"
lp15@67998
   726
      by (simp add: \<open>fsigma C\<close> fsigma_imp_gdelta)
lp15@67998
   727
    show "S \<union> T = -C" "disjnt S T"
lp15@67998
   728
      using C by (auto simp: disjnt_def)
lp15@67998
   729
  qed (use C in auto)
lp15@67998
   730
qed
lp15@67998
   731
lp15@67998
   732
lp15@67998
   733
proposition measure_semicontinuous_with_hausdist_explicit:
lp15@67998
   734
  assumes "bounded S" and neg: "negligible(frontier S)" and "e > 0"
lp15@67998
   735
  obtains d where "d > 0"
lp15@67998
   736
                  "\<And>T. \<lbrakk>T \<in> lmeasurable; \<And>y. y \<in> T \<Longrightarrow> \<exists>x. x \<in> S \<and> dist x y < d\<rbrakk>
lp15@67998
   737
                        \<Longrightarrow> measure lebesgue T < measure lebesgue S + e"
lp15@67998
   738
proof (cases "S = {}")
lp15@67998
   739
  case True
lp15@67998
   740
  with that \<open>e > 0\<close> show ?thesis by force
lp15@67998
   741
next
lp15@67998
   742
  case False
lp15@67998
   743
  then have frS: "frontier S \<noteq> {}"
lp15@67998
   744
    using \<open>bounded S\<close> frontier_eq_empty not_bounded_UNIV by blast
lp15@67998
   745
  have "S \<in> lmeasurable"
lp15@67998
   746
    by (simp add: \<open>bounded S\<close> measurable_Jordan neg)
lp15@67998
   747
  have null: "(frontier S) \<in> null_sets lebesgue"
lp15@67998
   748
    by (metis neg negligible_iff_null_sets)
lp15@67998
   749
  have "frontier S \<in> lmeasurable" and mS0: "measure lebesgue (frontier S) = 0"
lp15@67998
   750
    using neg negligible_imp_measurable negligible_iff_measure by blast+
lp15@67998
   751
  with \<open>e > 0\<close> lmeasurable_outer_open
lp15@67998
   752
  obtain U where "open U"
lp15@67998
   753
    and U: "frontier S \<subseteq> U" "U - frontier S \<in> lmeasurable" "measure lebesgue (U - frontier S) < e"
lp15@67998
   754
    by (metis fmeasurableD)
lp15@67998
   755
  with null have "U \<in> lmeasurable"
lp15@67998
   756
    by (metis borel_open measurable_Diff_null_set sets_completionI_sets sets_lborel)
lp15@67998
   757
  have "measure lebesgue (U - frontier S) = measure lebesgue U"
lp15@67998
   758
    using mS0 by (simp add: \<open>U \<in> lmeasurable\<close> fmeasurableD measure_Diff_null_set null)
lp15@67998
   759
  with U have mU: "measure lebesgue U < e"
lp15@67998
   760
    by simp
lp15@67998
   761
  show ?thesis
lp15@67998
   762
  proof
lp15@67998
   763
    have "U \<noteq> UNIV"
lp15@67998
   764
      using \<open>U \<in> lmeasurable\<close> by auto
lp15@67998
   765
    then have "- U \<noteq> {}"
lp15@67998
   766
      by blast
lp15@67998
   767
    with \<open>open U\<close> \<open>frontier S \<subseteq> U\<close> show "setdist (frontier S) (- U) > 0"
lp15@67998
   768
      by (auto simp: \<open>bounded S\<close> open_closed compact_frontier_bounded setdist_gt_0_compact_closed frS)
lp15@67998
   769
    fix T
lp15@67998
   770
    assume "T \<in> lmeasurable"
lp15@67998
   771
      and T: "\<And>t. t \<in> T \<Longrightarrow> \<exists>y. y \<in> S \<and> dist y t < setdist (frontier S) (- U)"
lp15@67998
   772
    then have "measure lebesgue T - measure lebesgue S \<le> measure lebesgue (T - S)"
lp15@67998
   773
      by (simp add: \<open>S \<in> lmeasurable\<close> measure_diff_le_measure_setdiff)
lp15@67998
   774
    also have "\<dots>  \<le> measure lebesgue U"
lp15@67998
   775
    proof -
lp15@67998
   776
      have "T - S \<subseteq> U"
lp15@67998
   777
      proof clarify
lp15@67998
   778
        fix x
lp15@67998
   779
        assume "x \<in> T" and "x \<notin> S"
lp15@67998
   780
        then obtain y where "y \<in> S" and y: "dist y x < setdist (frontier S) (- U)"
lp15@67998
   781
          using T by blast
lp15@67998
   782
        have "closed_segment x y \<inter> frontier S \<noteq> {}"
lp15@67998
   783
          using connected_Int_frontier \<open>x \<notin> S\<close> \<open>y \<in> S\<close> by blast
lp15@67998
   784
        then obtain z where z: "z \<in> closed_segment x y" "z \<in> frontier S"
lp15@67998
   785
          by auto
lp15@67998
   786
        with y have "dist z x < setdist(frontier S) (- U)"
lp15@67998
   787
          by (auto simp: dist_commute dest!: dist_in_closed_segment)
lp15@67998
   788
        with z have False if "x \<in> -U"
lp15@67998
   789
          using setdist_le_dist [OF \<open>z \<in> frontier S\<close> that] by auto
lp15@67998
   790
        then show "x \<in> U"
lp15@67998
   791
          by blast
lp15@67998
   792
      qed
lp15@67998
   793
      then show ?thesis
lp15@67998
   794
        by (simp add: \<open>S \<in> lmeasurable\<close> \<open>T \<in> lmeasurable\<close> \<open>U \<in> lmeasurable\<close> fmeasurableD measure_mono_fmeasurable sets.Diff)
lp15@67998
   795
    qed
lp15@67998
   796
    finally have "measure lebesgue T - measure lebesgue S \<le> measure lebesgue U" .
lp15@67998
   797
    with mU show "measure lebesgue T < measure lebesgue S + e"
lp15@67998
   798
      by linarith
lp15@67998
   799
  qed
lp15@67998
   800
qed
lp15@67998
   801
lp15@67998
   802
proposition lebesgue_regular_inner:
lp15@67998
   803
 assumes "S \<in> sets lebesgue"
lp15@67998
   804
 obtains K C where "negligible K" "\<And>n::nat. compact(C n)" "S = (\<Union>n. C n) \<union> K"
lp15@67998
   805
proof -
lp15@67998
   806
  have "\<exists>T. closed T \<and> T \<subseteq> S \<and> (S - T) \<in> lmeasurable \<and> measure lebesgue (S - T) < (1/2)^n" for n
lp15@67998
   807
    using sets_lebesgue_inner_closed assms
lp15@67998
   808
    by (metis sets_lebesgue_inner_closed zero_less_divide_1_iff zero_less_numeral zero_less_power)
lp15@67998
   809
  then obtain C where clo: "\<And>n. closed (C n)" and subS: "\<And>n. C n \<subseteq> S"
lp15@67998
   810
    and mea: "\<And>n. (S - C n) \<in> lmeasurable"
lp15@67998
   811
    and less: "\<And>n. measure lebesgue (S - C n) < (1/2)^n"
lp15@67998
   812
    by metis
lp15@67998
   813
  have "\<exists>F. (\<forall>n::nat. compact(F n)) \<and> (\<Union>n. F n) = C m" for m::nat
lp15@67998
   814
    by (metis clo closed_Union_compact_subsets)
lp15@67998
   815
  then obtain D :: "[nat,nat] \<Rightarrow> 'a set" where D: "\<And>m n. compact(D m n)" "\<And>m. (\<Union>n. D m n) = C m"
lp15@67998
   816
    by metis
lp15@67998
   817
  let ?C = "from_nat_into (\<Union>m. range (D m))"
lp15@67998
   818
  have "countable (\<Union>m. range (D m))"
lp15@67998
   819
    by blast
lp15@67998
   820
  have "range (from_nat_into (\<Union>m. range (D m))) = (\<Union>m. range (D m))"
lp15@67998
   821
    using range_from_nat_into by simp
lp15@67998
   822
  then have CD: "\<exists>m n. ?C k = D m n"  for k
lp15@67998
   823
    by (metis (mono_tags, lifting) UN_iff rangeE range_eqI)
lp15@67998
   824
  show thesis
lp15@67998
   825
  proof
lp15@67998
   826
    show "negligible (S - (\<Union>n. C n))"
lp15@67998
   827
    proof (clarsimp simp: negligible_outer_le)
lp15@67998
   828
      fix e :: "real"
lp15@67998
   829
      assume "e > 0"
lp15@67998
   830
      then obtain n where n: "(1/2)^n < e"
lp15@67998
   831
        using real_arch_pow_inv [of e "1/2"] by auto
lp15@67998
   832
      show "\<exists>T. S - (\<Union>n. C n) \<subseteq> T \<and> T \<in> lmeasurable \<and> measure lebesgue T \<le> e"
lp15@67998
   833
      proof (intro exI conjI)
lp15@67998
   834
        show "S - (\<Union>n. C n) \<subseteq> S - C n"
lp15@67998
   835
          by blast
lp15@67998
   836
        show "S - C n \<in> lmeasurable"
lp15@67998
   837
          by (simp add: mea)
lp15@67998
   838
        show "measure lebesgue (S - C n) \<le> e"
lp15@67998
   839
          using less [of n] n by simp
lp15@67998
   840
      qed
lp15@67998
   841
    qed
lp15@67998
   842
    show "compact (?C n)" for n
lp15@67998
   843
      using CD D by metis
lp15@67998
   844
    show "S = (\<Union>n. ?C n) \<union> (S - (\<Union>n. C n))" (is "_ = ?rhs")
lp15@67998
   845
    proof
lp15@67998
   846
      show "S \<subseteq> ?rhs"
lp15@67998
   847
        using D by fastforce
lp15@67998
   848
      show "?rhs \<subseteq> S"
lp15@67998
   849
        using subS D CD by auto (metis Sup_upper range_eqI subsetCE)
lp15@67998
   850
    qed
lp15@67998
   851
  qed
lp15@67998
   852
qed
lp15@67998
   853
lp15@67998
   854
lp15@67998
   855
lemma sets_lebesgue_continuous_image:
lp15@67998
   856
  assumes T: "T \<in> sets lebesgue" and contf: "continuous_on S f"
lp15@67998
   857
    and negim: "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible(f ` T)" and "T \<subseteq> S"
lp15@67998
   858
 shows "f ` T \<in> sets lebesgue"
lp15@67998
   859
proof -
lp15@67998
   860
  obtain K C where "negligible K" and com: "\<And>n::nat. compact(C n)" and Teq: "T = (\<Union>n. C n) \<union> K"
lp15@67998
   861
    using lebesgue_regular_inner [OF T] by metis
lp15@67998
   862
  then have comf: "\<And>n::nat. compact(f ` C n)"
lp15@67998
   863
    by (metis Un_subset_iff Union_upper \<open>T \<subseteq> S\<close> compact_continuous_image contf continuous_on_subset rangeI)
lp15@67998
   864
  have "((\<Union>n. f ` C n) \<union> f ` K) \<in> sets lebesgue"
lp15@67998
   865
  proof (rule sets.Un)
lp15@67998
   866
    have "K \<subseteq> S"
lp15@67998
   867
      using Teq \<open>T \<subseteq> S\<close> by blast
lp15@67998
   868
    show "(\<Union>n. f ` C n) \<in> sets lebesgue"
lp15@67998
   869
    proof (rule sets.countable_Union)
lp15@67998
   870
      show "range (\<lambda>n. f ` C n) \<subseteq> sets lebesgue"
lp15@67998
   871
        using borel_compact comf by (auto simp: borel_compact)
lp15@67998
   872
    qed auto
lp15@67998
   873
    show "f ` K \<in> sets lebesgue"
lp15@67998
   874
      by (simp add: \<open>K \<subseteq> S\<close> \<open>negligible K\<close> negim negligible_imp_sets)
lp15@67998
   875
  qed
lp15@67998
   876
  then show ?thesis
lp15@67998
   877
    by (simp add: Teq image_Un image_Union)
lp15@67998
   878
qed
lp15@67998
   879
lp15@67998
   880
lemma differentiable_image_in_sets_lebesgue:
lp15@67998
   881
  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
lp15@67998
   882
  assumes S: "S \<in> sets lebesgue" and dim: "DIM('m) \<le> DIM('n)" and f: "f differentiable_on S"
lp15@67998
   883
  shows "f`S \<in> sets lebesgue"
lp15@67998
   884
proof (rule sets_lebesgue_continuous_image [OF S])
lp15@67998
   885
  show "continuous_on S f"
lp15@67998
   886
    by (meson differentiable_imp_continuous_on f)
lp15@67998
   887
  show "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible (f ` T)"
lp15@67998
   888
    using differentiable_on_subset f
lp15@67998
   889
    by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim])
lp15@67998
   890
qed auto
lp15@67998
   891
lp15@67998
   892
lemma sets_lebesgue_on_continuous_image:
lp15@67998
   893
  assumes S: "S \<in> sets lebesgue" and X: "X \<in> sets (lebesgue_on S)" and contf: "continuous_on S f"
lp15@67998
   894
    and negim: "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible(f ` T)"
lp15@67998
   895
  shows "f ` X \<in> sets (lebesgue_on (f ` S))"
lp15@67998
   896
proof -
lp15@67998
   897
  have "X \<subseteq> S"
lp15@67998
   898
    by (metis S X sets.Int_space_eq2 sets_restrict_space_iff)
lp15@67998
   899
  moreover have "f ` S \<in> sets lebesgue"
lp15@67998
   900
    using S contf negim sets_lebesgue_continuous_image by blast
lp15@67998
   901
  moreover have "f ` X \<in> sets lebesgue"
lp15@67998
   902
    by (metis S X contf negim sets_lebesgue_continuous_image sets_restrict_space_iff space_restrict_space space_restrict_space2)
lp15@67998
   903
  ultimately show ?thesis
lp15@67998
   904
    by (auto simp: sets_restrict_space_iff)
lp15@67998
   905
qed
lp15@67998
   906
lp15@67998
   907
lemma differentiable_image_in_sets_lebesgue_on:
lp15@67998
   908
  fixes f :: "'m::euclidean_space \<Rightarrow> 'n::euclidean_space"
lp15@67998
   909
  assumes S: "S \<in> sets lebesgue" and X: "X \<in> sets (lebesgue_on S)" and dim: "DIM('m) \<le> DIM('n)"
lp15@67998
   910
       and f: "f differentiable_on S"
lp15@67998
   911
     shows "f ` X \<in> sets (lebesgue_on (f`S))"
lp15@67998
   912
proof (rule sets_lebesgue_on_continuous_image [OF S X])
lp15@67998
   913
  show "continuous_on S f"
lp15@67998
   914
    by (meson differentiable_imp_continuous_on f)
lp15@67998
   915
  show "\<And>T. \<lbrakk>negligible T; T \<subseteq> S\<rbrakk> \<Longrightarrow> negligible (f ` T)"
lp15@67998
   916
    using differentiable_on_subset f
lp15@67998
   917
    by (auto simp: intro!: negligible_differentiable_image_negligible [OF dim])
lp15@67998
   918
qed
lp15@67998
   919
lp15@67998
   920
lp15@67998
   921
proposition
lp15@67998
   922
 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
lp15@67998
   923
  assumes S: "S \<in> lmeasurable"
lp15@67998
   924
  and deriv: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
lp15@67998
   925
  and int: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S"
lp15@67998
   926
  and bounded: "\<And>x. x \<in> S \<Longrightarrow> \<bar>det (matrix (f' x))\<bar> \<le> B"
lp15@67998
   927
  shows measurable_bounded_differentiable_image:
lp15@67998
   928
       "f ` S \<in> lmeasurable"
lp15@67998
   929
    and measure_bounded_differentiable_image:
lp15@67998
   930
       "measure lebesgue (f ` S) \<le> B * measure lebesgue S" (is "?M")
lp15@67998
   931
proof -
lp15@67998
   932
  have "f ` S \<in> lmeasurable \<and> measure lebesgue (f ` S) \<le> B * measure lebesgue S"
lp15@67998
   933
  proof (cases "B < 0")
lp15@67998
   934
    case True
lp15@67998
   935
    then have "S = {}"
lp15@67998
   936
      by (meson abs_ge_zero bounded empty_iff equalityI less_le_trans linorder_not_less subsetI)
lp15@67998
   937
    then show ?thesis
lp15@67998
   938
      by auto
lp15@67998
   939
  next
lp15@67998
   940
    case False
lp15@67998
   941
    then have "B \<ge> 0"
lp15@67998
   942
      by arith
lp15@67998
   943
    let ?\<mu> = "measure lebesgue"
lp15@67998
   944
    have f_diff: "f differentiable_on S"
lp15@67998
   945
      using deriv by (auto simp: differentiable_on_def differentiable_def)
lp15@67998
   946
    have eps: "f ` S \<in> lmeasurable" "?\<mu> (f ` S) \<le> (B+e) * ?\<mu> S" (is "?ME")
lp15@67998
   947
              if "e > 0" for e
lp15@67998
   948
    proof -
lp15@67998
   949
      have eps_d: "f ` S \<in> lmeasurable"  "?\<mu> (f ` S) \<le> (B+e) * (?\<mu> S + d)" (is "?MD")
lp15@67998
   950
                  if "d > 0" for d
lp15@67998
   951
      proof -
lp15@67998
   952
        obtain T where "open T" "S \<subseteq> T" and TS: "(T-S) \<in> lmeasurable" and "?\<mu> (T-S) < d"
lp15@67998
   953
          using S \<open>d > 0\<close> lmeasurable_outer_open by blast
lp15@67998
   954
        with S have "T \<in> lmeasurable" and Tless: "?\<mu> T < ?\<mu> S + d"
lp15@67998
   955
          by (auto simp: measurable_measure_Diff dest!: fmeasurable_Diff_D)
lp15@67998
   956
        have "\<exists>r. 0 < r \<and> r < d \<and> ball x r \<subseteq> T \<and> f ` (S \<inter> ball x r) \<in> lmeasurable \<and>
lp15@67998
   957
                  ?\<mu> (f ` (S \<inter> ball x r)) \<le> (B + e) * ?\<mu> (ball x r)"
lp15@67998
   958
          if "x \<in> S" "d > 0" for x d
lp15@67998
   959
        proof -
lp15@67998
   960
          have lin: "linear (f' x)"
lp15@67998
   961
            and lim0: "((\<lambda>y. (f y - (f x + f' x (y - x))) /\<^sub>R norm(y - x)) \<longlongrightarrow> 0) (at x within S)"
lp15@67998
   962
            using deriv \<open>x \<in> S\<close> by (auto simp: has_derivative_within bounded_linear.linear field_simps)
lp15@67998
   963
          have bo: "bounded (f' x ` ball 0 1)"
lp15@67998
   964
            by (simp add: bounded_linear_image linear_linear lin)
lp15@67998
   965
          have neg: "negligible (frontier (f' x ` ball 0 1))"
lp15@67998
   966
            using deriv has_derivative_linear \<open>x \<in> S\<close>
lp15@67998
   967
            by (auto intro!: negligible_convex_frontier [OF convex_linear_image])
lp15@67998
   968
          have 0: "0 < e * unit_ball_vol (real CARD('n))"
lp15@67998
   969
            using  \<open>e > 0\<close> by simp
lp15@67998
   970
          obtain k where "k > 0" and k:
lp15@67998
   971
                  "\<And>U. \<lbrakk>U \<in> lmeasurable; \<And>y. y \<in> U \<Longrightarrow> \<exists>z. z \<in> f' x ` ball 0 1 \<and> dist z y < k\<rbrakk>
lp15@67998
   972
                        \<Longrightarrow> ?\<mu> U < ?\<mu> (f' x ` ball 0 1) + e * unit_ball_vol (CARD('n))"
lp15@67998
   973
            using measure_semicontinuous_with_hausdist_explicit [OF bo neg 0] by blast
lp15@67998
   974
          obtain l where "l > 0" and l: "ball x l \<subseteq> T"
lp15@67998
   975
            using \<open>x \<in> S\<close> \<open>open T\<close> \<open>S \<subseteq> T\<close> openE by blast
lp15@67998
   976
          obtain \<zeta> where "0 < \<zeta>"
lp15@67998
   977
            and \<zeta>: "\<And>y. \<lbrakk>y \<in> S; y \<noteq> x; dist y x < \<zeta>\<rbrakk>
lp15@67998
   978
                        \<Longrightarrow> norm (f y - (f x + f' x (y - x))) / norm (y - x) < k"
lp15@67998
   979
            using lim0 \<open>k > 0\<close> by (force simp: Lim_within field_simps)
lp15@67998
   980
          define r where "r \<equiv> min (min l (\<zeta>/2)) (min 1 (d/2))"
lp15@67998
   981
          show ?thesis
lp15@67998
   982
          proof (intro exI conjI)
lp15@67998
   983
            show "r > 0" "r < d"
lp15@67998
   984
              using \<open>l > 0\<close> \<open>\<zeta> > 0\<close> \<open>d > 0\<close> by (auto simp: r_def)
lp15@67998
   985
            have "r \<le> l"
lp15@67998
   986
              by (auto simp: r_def)
lp15@67998
   987
            with l show "ball x r \<subseteq> T"
lp15@67998
   988
              by auto
lp15@67998
   989
            have ex_lessK: "\<exists>x' \<in> ball 0 1. dist (f' x x') ((f y - f x) /\<^sub>R r) < k"
lp15@67998
   990
              if "y \<in> S" and "dist x y < r" for y
lp15@67998
   991
            proof (cases "y = x")
lp15@67998
   992
              case True
lp15@67998
   993
              with lin linear_0 \<open>k > 0\<close> that show ?thesis
lp15@67998
   994
                by (rule_tac x=0 in bexI) (auto simp: linear_0)
lp15@67998
   995
            next
lp15@67998
   996
              case False
lp15@67998
   997
              then show ?thesis
lp15@67998
   998
              proof (rule_tac x="(y - x) /\<^sub>R r" in bexI)
lp15@67998
   999
                have "f' x ((y - x) /\<^sub>R r) = f' x (y - x) /\<^sub>R r"
lp15@67998
  1000
                  by (simp add: lin linear_cmul)
lp15@67998
  1001
                then have "dist (f' x ((y - x) /\<^sub>R r)) ((f y - f x) /\<^sub>R r) = norm (f' x (y - x) /\<^sub>R r - (f y - f x) /\<^sub>R r)"
lp15@67998
  1002
                  by (simp add: dist_norm)
lp15@67998
  1003
                also have "\<dots> = norm (f' x (y - x) - (f y - f x)) / r"
lp15@67998
  1004
                  using \<open>r > 0\<close> by (simp add: real_vector.scale_right_diff_distrib [symmetric] divide_simps)
lp15@67998
  1005
                also have "\<dots> \<le> norm (f y - (f x + f' x (y - x))) / norm (y - x)"
lp15@67998
  1006
                  using that \<open>r > 0\<close> False by (simp add: algebra_simps divide_simps dist_norm norm_minus_commute mult_right_mono)
lp15@67998
  1007
                also have "\<dots> < k"
lp15@67998
  1008
                  using that \<open>0 < \<zeta>\<close> by (simp add: dist_commute r_def  \<zeta> [OF \<open>y \<in> S\<close> False])
lp15@67998
  1009
                finally show "dist (f' x ((y - x) /\<^sub>R r)) ((f y - f x) /\<^sub>R r) < k" .
lp15@67998
  1010
                show "(y - x) /\<^sub>R r \<in> ball 0 1"
lp15@67998
  1011
                  using that \<open>r > 0\<close> by (simp add: dist_norm divide_simps norm_minus_commute)
lp15@67998
  1012
              qed
lp15@67998
  1013
            qed
lp15@67998
  1014
            let ?rfs = "(\<lambda>x. x /\<^sub>R r) ` (+) (- f x) ` f ` (S \<inter> ball x r)"
lp15@67998
  1015
            have rfs_mble: "?rfs \<in> lmeasurable"
lp15@67998
  1016
            proof (rule bounded_set_imp_lmeasurable)
lp15@67998
  1017
              have "f differentiable_on S \<inter> ball x r"
lp15@67998
  1018
                using f_diff by (auto simp: fmeasurableD differentiable_on_subset)
lp15@67998
  1019
              with S show "?rfs \<in> sets lebesgue"
lp15@67998
  1020
                by (auto simp: sets.Int intro!: lebesgue_sets_translation differentiable_image_in_sets_lebesgue)
lp15@67998
  1021
              let ?B = "(\<lambda>(x, y). x + y) ` (f' x ` ball 0 1 \<times> ball 0 k)"
lp15@67998
  1022
              have "bounded ?B"
lp15@67998
  1023
                by (simp add: bounded_plus [OF bo])
lp15@67998
  1024
              moreover have "?rfs \<subseteq> ?B"
lp15@67998
  1025
                apply (auto simp: dist_norm image_iff dest!: ex_lessK)
lp15@67998
  1026
                by (metis (no_types, hide_lams) add.commute diff_add_cancel dist_0_norm dist_commute dist_norm mem_ball)
lp15@67998
  1027
              ultimately show "bounded (?rfs)"
lp15@67998
  1028
                by (rule bounded_subset)
lp15@67998
  1029
            qed
lp15@67998
  1030
            then have "(\<lambda>x. r *\<^sub>R x) ` ?rfs \<in> lmeasurable"
lp15@67998
  1031
              by (simp add: measurable_linear_image)
lp15@67998
  1032
            with \<open>r > 0\<close> have "(+) (- f x) ` f ` (S \<inter> ball x r) \<in> lmeasurable"
lp15@67998
  1033
              by (simp add: image_comp o_def)
lp15@67998
  1034
            then have "(+) (f x) ` (+) (- f x) ` f ` (S \<inter> ball x r) \<in> lmeasurable"
lp15@67998
  1035
              using  measurable_translation by blast
lp15@67998
  1036
            then show fsb: "f ` (S \<inter> ball x r) \<in> lmeasurable"
lp15@67998
  1037
              by (simp add: image_comp o_def)
lp15@67998
  1038
            have "?\<mu> (f ` (S \<inter> ball x r)) = ?\<mu> (?rfs) * r ^ CARD('n)"
lp15@67998
  1039
              using \<open>r > 0\<close> by (simp add: measure_translation measure_linear_image measurable_translation fsb field_simps)
lp15@67998
  1040
            also have "\<dots> \<le> (\<bar>det (matrix (f' x))\<bar> * unit_ball_vol (CARD('n)) + e * unit_ball_vol (CARD('n))) * r ^ CARD('n)"
lp15@67998
  1041
            proof -
lp15@67998
  1042
              have "?\<mu> (?rfs) < ?\<mu> (f' x ` ball 0 1) + e * unit_ball_vol (CARD('n))"
lp15@67998
  1043
                using rfs_mble by (force intro: k dest!: ex_lessK)
lp15@67998
  1044
              then have "?\<mu> (?rfs) < \<bar>det (matrix (f' x))\<bar> * unit_ball_vol (CARD('n)) + e * unit_ball_vol (CARD('n))"
lp15@67998
  1045
                by (simp add: lin measure_linear_image [of "f' x"] content_ball)
lp15@67998
  1046
              with \<open>r > 0\<close> show ?thesis
lp15@67998
  1047
                by auto
lp15@67998
  1048
            qed
lp15@67998
  1049
            also have "\<dots> \<le> (B + e) * ?\<mu> (ball x r)"
lp15@67998
  1050
              using bounded [OF \<open>x \<in> S\<close>] \<open>r > 0\<close> by (simp add: content_ball algebra_simps)
lp15@67998
  1051
            finally show "?\<mu> (f ` (S \<inter> ball x r)) \<le> (B + e) * ?\<mu> (ball x r)" .
lp15@67998
  1052
          qed
lp15@67998
  1053
        qed
lp15@67998
  1054
        then obtain r where
lp15@67998
  1055
          r0d: "\<And>x d. \<lbrakk>x \<in> S; d > 0\<rbrakk> \<Longrightarrow> 0 < r x d \<and> r x d < d"
lp15@67998
  1056
          and rT: "\<And>x d. \<lbrakk>x \<in> S; d > 0\<rbrakk> \<Longrightarrow> ball x (r x d) \<subseteq> T"
lp15@67998
  1057
          and r: "\<And>x d. \<lbrakk>x \<in> S; d > 0\<rbrakk> \<Longrightarrow>
lp15@67998
  1058
                  (f ` (S \<inter> ball x (r x d))) \<in> lmeasurable \<and>
lp15@67998
  1059
                  ?\<mu> (f ` (S \<inter> ball x (r x d))) \<le> (B + e) * ?\<mu> (ball x (r x d))"
lp15@67998
  1060
          by metis
lp15@67998
  1061
        obtain C where "countable C" and Csub: "C \<subseteq> {(x,r x t) |x t. x \<in> S \<and> 0 < t}"
lp15@67998
  1062
          and pwC: "pairwise (\<lambda>i j. disjnt (ball (fst i) (snd i)) (ball (fst j) (snd j))) C"
lp15@67998
  1063
          and negC: "negligible(S - (\<Union>i \<in> C. ball (fst i) (snd i)))"
lp15@67998
  1064
          apply (rule Vitali_covering_theorem_balls [of S "{(x,r x t) |x t. x \<in> S \<and> 0 < t}" fst snd])
lp15@67998
  1065
           apply auto
lp15@67998
  1066
          by (metis dist_eq_0_iff r0d)
lp15@67998
  1067
        let ?UB = "(\<Union>(x,s) \<in> C. ball x s)"
lp15@67998
  1068
        have eq: "f ` (S \<inter> ?UB) = (\<Union>(x,s) \<in> C. f ` (S \<inter> ball x s))"
lp15@67998
  1069
          by auto
lp15@67998
  1070
        have mle: "?\<mu> (\<Union>(x,s) \<in> K. f ` (S \<inter> ball x s)) \<le> (B + e) * (?\<mu> S + d)"  (is "?l \<le> ?r")
lp15@67998
  1071
          if "K \<subseteq> C" and "finite K" for K
lp15@67998
  1072
        proof -
lp15@67998
  1073
          have gt0: "b > 0" if "(a, b) \<in> K" for a b
lp15@67998
  1074
            using Csub that \<open>K \<subseteq> C\<close> r0d by auto
lp15@67998
  1075
          have inj: "inj_on (\<lambda>(x, y). ball x y) K"
lp15@67998
  1076
            by (force simp: inj_on_def ball_eq_ball_iff dest: gt0)
lp15@67998
  1077
          have disjnt: "disjoint ((\<lambda>(x, y). ball x y) ` K)"
lp15@67998
  1078
            using pwC that
lp15@67998
  1079
            apply (clarsimp simp: pairwise_def case_prod_unfold ball_eq_ball_iff)
lp15@67998
  1080
            by (metis subsetD fst_conv snd_conv)
lp15@67998
  1081
          have "?l \<le> (\<Sum>i\<in>K. ?\<mu> (case i of (x, s) \<Rightarrow> f ` (S \<inter> ball x s)))"
lp15@67998
  1082
          proof (rule measure_UNION_le [OF \<open>finite K\<close>], clarify)
lp15@67998
  1083
            fix x r
lp15@67998
  1084
            assume "(x,r) \<in> K"
lp15@67998
  1085
            then have "x \<in> S"
lp15@67998
  1086
              using Csub \<open>K \<subseteq> C\<close> by auto
lp15@67998
  1087
            show "f ` (S \<inter> ball x r) \<in> sets lebesgue"
lp15@67998
  1088
              by (meson Int_lower1 S differentiable_on_subset f_diff fmeasurableD lmeasurable_ball order_refl sets.Int differentiable_image_in_sets_lebesgue)
lp15@67998
  1089
          qed
lp15@67998
  1090
          also have "\<dots> \<le> (\<Sum>(x,s) \<in> K. (B + e) * ?\<mu> (ball x s))"
lp15@67998
  1091
            apply (rule sum_mono)
lp15@67998
  1092
            using Csub r \<open>K \<subseteq> C\<close> by auto
lp15@67998
  1093
          also have "\<dots> = (B + e) * (\<Sum>(x,s) \<in> K. ?\<mu> (ball x s))"
lp15@67998
  1094
            by (simp add: prod.case_distrib sum_distrib_left)
lp15@67998
  1095
          also have "\<dots> = (B + e) * sum ?\<mu> ((\<lambda>(x, y). ball x y) ` K)"
lp15@67998
  1096
            using \<open>B \<ge> 0\<close> \<open>e > 0\<close> by (simp add: inj sum.reindex prod.case_distrib)
lp15@67998
  1097
          also have "\<dots> = (B + e) * ?\<mu> (\<Union>(x,s) \<in> K. ball x s)"
lp15@67998
  1098
            using \<open>B \<ge> 0\<close> \<open>e > 0\<close> that
lp15@67998
  1099
            by (subst measure_Union') (auto simp: disjnt measure_Union')
lp15@67998
  1100
          also have "\<dots> \<le> (B + e) * ?\<mu> T"
lp15@67998
  1101
            using \<open>B \<ge> 0\<close> \<open>e > 0\<close> that apply simp
lp15@67998
  1102
            apply (rule measure_mono_fmeasurable [OF _ _ \<open>T \<in> lmeasurable\<close>])
lp15@67998
  1103
            using Csub rT by force+
lp15@67998
  1104
          also have "\<dots> \<le> (B + e) * (?\<mu> S + d)"
lp15@67998
  1105
            using \<open>B \<ge> 0\<close> \<open>e > 0\<close> Tless by simp
lp15@67998
  1106
          finally show ?thesis .
lp15@67998
  1107
        qed
lp15@67998
  1108
        have fSUB_mble: "(f ` (S \<inter> ?UB)) \<in> lmeasurable"
lp15@67998
  1109
          unfolding eq using Csub r False \<open>e > 0\<close> that
lp15@67998
  1110
          by (auto simp: intro!: fmeasurable_UN_bound [OF \<open>countable C\<close> _ mle])
lp15@67998
  1111
        have fSUB_meas: "?\<mu> (f ` (S \<inter> ?UB)) \<le> (B + e) * (?\<mu> S + d)"  (is "?MUB")
lp15@67998
  1112
          unfolding eq using Csub r False \<open>e > 0\<close> that
lp15@67998
  1113
          by (auto simp: intro!: measure_UN_bound [OF \<open>countable C\<close> _ mle])
lp15@67998
  1114
        have neg: "negligible ((f ` (S \<inter> ?UB) - f ` S) \<union> (f ` S - f ` (S \<inter> ?UB)))"
lp15@67998
  1115
        proof (rule negligible_subset [OF negligible_differentiable_image_negligible [OF order_refl negC, where f=f]])
lp15@67998
  1116
          show "f differentiable_on S - (\<Union>i\<in>C. ball (fst i) (snd i))"
lp15@67998
  1117
            by (meson DiffE differentiable_on_subset subsetI f_diff)
lp15@67998
  1118
        qed force
lp15@67998
  1119
        show "f ` S \<in> lmeasurable"
lp15@67998
  1120
          by (rule lmeasurable_negligible_symdiff [OF fSUB_mble neg])
lp15@67998
  1121
        show ?MD
lp15@67998
  1122
          using fSUB_meas measure_negligible_symdiff [OF fSUB_mble neg] by simp
lp15@67998
  1123
      qed
lp15@67998
  1124
      show "f ` S \<in> lmeasurable"
lp15@67998
  1125
        using eps_d [of 1] by simp
lp15@67998
  1126
      show ?ME
lp15@67998
  1127
      proof (rule field_le_epsilon)
lp15@67998
  1128
        fix \<delta> :: real
lp15@67998
  1129
        assume "0 < \<delta>"
lp15@67998
  1130
        then show "?\<mu> (f ` S) \<le> (B + e) * ?\<mu> S + \<delta>"
lp15@67998
  1131
          using eps_d [of "\<delta> / (B+e)"] \<open>e > 0\<close> \<open>B \<ge> 0\<close> by (auto simp: divide_simps mult_ac)
lp15@67998
  1132
      qed
lp15@67998
  1133
    qed
lp15@67998
  1134
    show ?thesis
lp15@67998
  1135
    proof (cases "?\<mu> S = 0")
lp15@67998
  1136
      case True
lp15@67998
  1137
      with eps have "?\<mu> (f ` S) = 0"
lp15@67998
  1138
        by (metis mult_zero_right not_le zero_less_measure_iff)
lp15@67998
  1139
      then show ?thesis
lp15@67998
  1140
        using eps [of 1] by (simp add: True)
lp15@67998
  1141
    next
lp15@67998
  1142
      case False
lp15@67998
  1143
      have "?\<mu> (f ` S) \<le> B * ?\<mu> S"
lp15@67998
  1144
      proof (rule field_le_epsilon)
lp15@67998
  1145
        fix e :: real
lp15@67998
  1146
        assume "e > 0"
lp15@67998
  1147
        then show "?\<mu> (f ` S) \<le> B * ?\<mu> S + e"
lp15@67998
  1148
          using eps [of "e / ?\<mu> S"] False by (auto simp: algebra_simps zero_less_measure_iff)
lp15@67998
  1149
      qed
lp15@67998
  1150
      with eps [of 1] show ?thesis by auto
lp15@67998
  1151
    qed
lp15@67998
  1152
  qed
lp15@67998
  1153
  then show "f ` S \<in> lmeasurable" ?M by blast+
lp15@67998
  1154
qed
lp15@67998
  1155
lp15@67998
  1156
lemma
lp15@67998
  1157
 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
lp15@67998
  1158
  assumes S: "S \<in> lmeasurable"
lp15@67998
  1159
    and deriv: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
lp15@67998
  1160
    and int: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S"
lp15@67998
  1161
  shows m_diff_image_weak: "f ` S \<in> lmeasurable \<and> measure lebesgue (f ` S) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)"
lp15@67998
  1162
proof -
lp15@67998
  1163
  let ?\<mu> = "measure lebesgue"
lp15@67998
  1164
  have aint_S: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) absolutely_integrable_on S"
lp15@67998
  1165
    using int unfolding absolutely_integrable_on_def by auto
lp15@67998
  1166
  define m where "m \<equiv> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)"
lp15@67998
  1167
  have *: "f ` S \<in> lmeasurable" "?\<mu> (f ` S) \<le> m + e * ?\<mu> S"
lp15@67998
  1168
    if "e > 0" for e
lp15@67998
  1169
  proof -
lp15@67998
  1170
    define T where "T \<equiv> \<lambda>n. {x \<in> S. n * e \<le> \<bar>det (matrix (f' x))\<bar> \<and>
lp15@67998
  1171
                                     \<bar>det (matrix (f' x))\<bar> < (Suc n) * e}"
lp15@67998
  1172
    have meas_t: "T n \<in> lmeasurable" for n
lp15@67998
  1173
    proof -
lp15@67998
  1174
      have *: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) \<in> borel_measurable (lebesgue_on S)"
lp15@67998
  1175
        using aint_S by (simp add: S borel_measurable_restrict_space_iff fmeasurableD set_integrable_def)
lp15@67998
  1176
      have [intro]: "x \<in> sets (lebesgue_on S) \<Longrightarrow> x \<in> sets lebesgue" for x
lp15@67998
  1177
        using S sets_restrict_space_subset by blast
lp15@67998
  1178
      have "{x \<in> S. real n * e \<le> \<bar>det (matrix (f' x))\<bar>} \<in> sets lebesgue"
lp15@67998
  1179
        using * by (auto simp: borel_measurable_iff_halfspace_ge space_restrict_space)
lp15@67998
  1180
      then have 1: "{x \<in> S. real n * e \<le> \<bar>det (matrix (f' x))\<bar>} \<in> lmeasurable"
lp15@67998
  1181
        using S by (simp add: fmeasurableI2)
lp15@67998
  1182
      have "{x \<in> S. \<bar>det (matrix (f' x))\<bar> < (1 + real n) * e} \<in> sets lebesgue"
lp15@67998
  1183
        using * by (auto simp: borel_measurable_iff_halfspace_less space_restrict_space)
lp15@67998
  1184
      then have 2: "{x \<in> S. \<bar>det (matrix (f' x))\<bar> < (1 + real n) * e} \<in> lmeasurable"
lp15@67998
  1185
        using S by (simp add: fmeasurableI2)
lp15@67998
  1186
      show ?thesis
lp15@67998
  1187
        using fmeasurable.Int [OF 1 2] by (simp add: T_def Int_def cong: conj_cong)
lp15@67998
  1188
    qed
lp15@67998
  1189
    have aint_T: "\<And>k. (\<lambda>x. \<bar>det (matrix (f' x))\<bar>) absolutely_integrable_on T k"
lp15@67998
  1190
      using set_integrable_subset [OF aint_S] meas_t T_def by blast
lp15@67998
  1191
    have Seq: "S = (\<Union>n. T n)"
lp15@67998
  1192
      apply (auto simp: T_def)
lp15@67998
  1193
      apply (rule_tac x="nat(floor(abs(det(matrix(f' x))) / e))" in exI)
lp15@67998
  1194
      using that apply auto
lp15@67998
  1195
      using of_int_floor_le pos_le_divide_eq apply blast
lp15@67998
  1196
      by (metis add.commute pos_divide_less_eq real_of_int_floor_add_one_gt)
lp15@67998
  1197
    have meas_ft: "f ` T n \<in> lmeasurable" for n
lp15@67998
  1198
    proof (rule measurable_bounded_differentiable_image)
lp15@67998
  1199
      show "T n \<in> lmeasurable"
lp15@67998
  1200
        by (simp add: meas_t)
lp15@67998
  1201
    next
lp15@67998
  1202
      fix x :: "(real,'n) vec"
lp15@67998
  1203
      assume "x \<in> T n"
lp15@67998
  1204
      show "(f has_derivative f' x) (at x within T n)"
lp15@67998
  1205
        by (metis (no_types, lifting) \<open>x \<in> T n\<close> deriv has_derivative_within_subset mem_Collect_eq subsetI T_def)
lp15@67998
  1206
      show "\<bar>det (matrix (f' x))\<bar> \<le> (Suc n) * e"
lp15@67998
  1207
        using \<open>x \<in> T n\<close> T_def by auto
lp15@67998
  1208
    next
lp15@67998
  1209
      show "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on T n"
lp15@67998
  1210
        using aint_T absolutely_integrable_on_def by blast
lp15@67998
  1211
    qed
lp15@67998
  1212
    have disT: "disjoint (range T)"
lp15@67998
  1213
      unfolding disjoint_def
lp15@67998
  1214
    proof clarsimp
lp15@67998
  1215
      show "T m \<inter> T n = {}" if "T m \<noteq> T n" for m n
lp15@67998
  1216
        using that
lp15@67998
  1217
      proof (induction m n rule: linorder_less_wlog)
lp15@67998
  1218
        case (less m n)
lp15@67998
  1219
        with \<open>e > 0\<close> show ?case
lp15@67998
  1220
          unfolding T_def
lp15@67998
  1221
          proof (clarsimp simp add: Collect_conj_eq [symmetric])
lp15@67998
  1222
            fix x
lp15@67998
  1223
            assume "e > 0"  "m < n"  "n * e \<le> \<bar>det (matrix (f' x))\<bar>"  "\<bar>det (matrix (f' x))\<bar> < (1 + real m) * e"
lp15@67998
  1224
            then have "n < 1 + real m"
lp15@67998
  1225
              by (metis (no_types, hide_lams) less_le_trans mult.commute not_le real_mult_le_cancel_iff2)
lp15@67998
  1226
            then show "False"
lp15@67998
  1227
              using less.hyps by linarith
lp15@67998
  1228
          qed
lp15@67998
  1229
      qed auto
lp15@67998
  1230
    qed
lp15@67998
  1231
    have injT: "inj_on T ({n. T n \<noteq> {}})"
lp15@67998
  1232
      unfolding inj_on_def
lp15@67998
  1233
    proof clarsimp
lp15@67998
  1234
      show "m = n" if "T m = T n" "T n \<noteq> {}" for m n
lp15@67998
  1235
        using that
lp15@67998
  1236
      proof (induction m n rule: linorder_less_wlog)
lp15@67998
  1237
        case (less m n)
lp15@67998
  1238
        have False if "T n \<subseteq> T m" "x \<in> T n" for x
lp15@67998
  1239
          using \<open>e > 0\<close> \<open>m < n\<close> that
lp15@67998
  1240
          apply (auto simp: T_def  mult.commute intro: less_le_trans dest!: subsetD)
lp15@67998
  1241
          by (metis add.commute less_le_trans nat_less_real_le not_le real_mult_le_cancel_iff2)
lp15@67998
  1242
        then show ?case
lp15@67998
  1243
          using less.prems by blast
lp15@67998
  1244
      qed auto
lp15@67998
  1245
    qed
lp15@67998
  1246
    have sum_eq_Tim: "(\<Sum>k\<le>n. f (T k)) = sum f (T ` {..n})" if "f {} = 0" for f :: "_ \<Rightarrow> real" and n
lp15@67998
  1247
    proof (subst sum.reindex_nontrivial)
lp15@67998
  1248
      fix i j  assume "i \<in> {..n}" "j \<in> {..n}" "i \<noteq> j" "T i = T j"
lp15@67998
  1249
      with that  injT [unfolded inj_on_def] show "f (T i) = 0"
lp15@67998
  1250
        by simp metis
lp15@67998
  1251
    qed (use atMost_atLeast0 in auto)
lp15@67998
  1252
    let ?B = "m + e * ?\<mu> S"
lp15@67998
  1253
    have "(\<Sum>k\<le>n. ?\<mu> (f ` T k)) \<le> ?B" for n
lp15@67998
  1254
    proof -
lp15@67998
  1255
      have "(\<Sum>k\<le>n. ?\<mu> (f ` T k)) \<le> (\<Sum>k\<le>n. ((k+1) * e) * ?\<mu>(T k))"
lp15@67998
  1256
      proof (rule sum_mono [OF measure_bounded_differentiable_image])
lp15@67998
  1257
        show "(f has_derivative f' x) (at x within T k)" if "x \<in> T k" for k x
lp15@67998
  1258
          using that unfolding T_def by (blast intro: deriv has_derivative_within_subset)
lp15@67998
  1259
        show "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on T k" for k
lp15@67998
  1260
          using absolutely_integrable_on_def aint_T by blast
lp15@67998
  1261
        show "\<bar>det (matrix (f' x))\<bar> \<le> real (k + 1) * e" if "x \<in> T k" for k x
lp15@67998
  1262
          using T_def that by auto
lp15@67998
  1263
      qed (use meas_t in auto)
lp15@67998
  1264
      also have "\<dots> \<le> (\<Sum>k\<le>n. (k * e) * ?\<mu>(T k)) + (\<Sum>k\<le>n. e * ?\<mu>(T k))"
lp15@67998
  1265
        by (simp add: algebra_simps sum.distrib)
lp15@67998
  1266
      also have "\<dots> \<le> ?B"
lp15@67998
  1267
      proof (rule add_mono)
lp15@67998
  1268
        have "(\<Sum>k\<le>n. real k * e * ?\<mu> (T k)) = (\<Sum>k\<le>n. integral (T k) (\<lambda>x. k * e))"
lp15@67998
  1269
          by (simp add: lmeasure_integral [OF meas_t]
lp15@67998
  1270
                        integral_mult_right [symmetric] integral_mult_left [symmetric]
lp15@67998
  1271
                   del: integral_mult_right integral_mult_left)
lp15@67998
  1272
        also have "\<dots> \<le> (\<Sum>k\<le>n. integral (T k) (\<lambda>x.  (abs (det (matrix (f' x))))))"
lp15@67998
  1273
        proof (rule sum_mono)
lp15@67998
  1274
          fix k
lp15@67998
  1275
          assume "k \<in> {..n}"
lp15@67998
  1276
          show "integral (T k) (\<lambda>x. k * e) \<le> integral (T k) (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)"
lp15@67998
  1277
          proof (rule integral_le [OF integrable_on_const [OF meas_t]])
lp15@67998
  1278
            show "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on T k"
lp15@67998
  1279
              using absolutely_integrable_on_def aint_T by blast
lp15@67998
  1280
          next
lp15@67998
  1281
            fix x assume "x \<in> T k"
lp15@67998
  1282
            show "k * e \<le> \<bar>det (matrix (f' x))\<bar>"
lp15@67998
  1283
              using \<open>x \<in> T k\<close> T_def by blast
lp15@67998
  1284
          qed
lp15@67998
  1285
        qed
lp15@67998
  1286
        also have "\<dots> = sum (\<lambda>T. integral T (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)) (T ` {..n})"
lp15@67998
  1287
          by (auto intro: sum_eq_Tim)
lp15@67998
  1288
        also have "\<dots> = integral (\<Union>k\<le>n. T k) (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)"
lp15@67998
  1289
        proof (rule integral_unique [OF has_integral_Union, symmetric])
lp15@67998
  1290
          fix S  assume "S \<in> T ` {..n}"
lp15@67998
  1291
          then show "((\<lambda>x. \<bar>det (matrix (f' x))\<bar>) has_integral integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)) S"
lp15@67998
  1292
          using absolutely_integrable_on_def aint_T by blast
lp15@67998
  1293
        next
lp15@67998
  1294
          show "pairwise (\<lambda>S S'. negligible (S \<inter> S')) (T ` {..n})"
lp15@67998
  1295
            using disT unfolding disjnt_iff by (auto simp: pairwise_def intro!: empty_imp_negligible)
lp15@67998
  1296
        qed auto
lp15@67998
  1297
        also have "\<dots> \<le> m"
lp15@67998
  1298
          unfolding m_def
lp15@67998
  1299
        proof (rule integral_subset_le)
lp15@67998
  1300
          have "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) absolutely_integrable_on (\<Union>k\<le>n. T k)"
lp15@67998
  1301
            apply (rule set_integrable_subset [OF aint_S])
lp15@67998
  1302
             apply (intro measurable meas_t fmeasurableD)
lp15@67998
  1303
            apply (force simp: Seq)
lp15@67998
  1304
            done
lp15@67998
  1305
          then show "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on (\<Union>k\<le>n. T k)"
lp15@67998
  1306
            using absolutely_integrable_on_def by blast
lp15@67998
  1307
        qed (use Seq int in auto)
lp15@67998
  1308
        finally show "(\<Sum>k\<le>n. real k * e * ?\<mu> (T k)) \<le> m" .
lp15@67998
  1309
      next
lp15@67998
  1310
        have "(\<Sum>k\<le>n. ?\<mu> (T k)) = sum ?\<mu> (T ` {..n})"
lp15@67998
  1311
          by (auto intro: sum_eq_Tim)
lp15@67998
  1312
        also have "\<dots> = ?\<mu> (\<Union>k\<le>n. T k)"
lp15@67998
  1313
          using S disT by (auto simp: pairwise_def meas_t intro: measure_Union' [symmetric])
lp15@67998
  1314
        also have "\<dots> \<le> ?\<mu> S"
lp15@67998
  1315
          using S by (auto simp: Seq intro: meas_t fmeasurableD measure_mono_fmeasurable)
lp15@67998
  1316
        finally have "(\<Sum>k\<le>n. ?\<mu> (T k)) \<le> ?\<mu> S" .
lp15@67998
  1317
        then show "(\<Sum>k\<le>n. e * ?\<mu> (T k)) \<le> e * ?\<mu> S"
lp15@67998
  1318
          by (metis less_eq_real_def ordered_comm_semiring_class.comm_mult_left_mono sum_distrib_left that)
lp15@67998
  1319
      qed
lp15@67998
  1320
      finally show "(\<Sum>k\<le>n. ?\<mu> (f ` T k)) \<le> ?B" .
lp15@67998
  1321
    qed
lp15@67998
  1322
    moreover have "measure lebesgue (\<Union>k\<le>n. f ` T k) \<le> (\<Sum>k\<le>n. ?\<mu> (f ` T k))" for n
lp15@67998
  1323
      by (simp add: fmeasurableD meas_ft measure_UNION_le)
lp15@67998
  1324
    ultimately have B_ge_m: "?\<mu> (\<Union>k\<le>n. (f ` T k)) \<le> ?B" for n
lp15@67998
  1325
      by (meson order_trans)
lp15@67998
  1326
    have "(\<Union>n. f ` T n) \<in> lmeasurable"
lp15@67998
  1327
      by (rule fmeasurable_countable_Union [OF meas_ft B_ge_m])
lp15@67998
  1328
    moreover have "?\<mu> (\<Union>n. f ` T n) \<le> m + e * ?\<mu> S"
lp15@67998
  1329
      by (rule measure_countable_Union_le [OF meas_ft B_ge_m])
lp15@67998
  1330
    ultimately show "f ` S \<in> lmeasurable" "?\<mu> (f ` S) \<le> m + e * ?\<mu> S"
lp15@67998
  1331
      by (auto simp: Seq image_Union)
lp15@67998
  1332
  qed
lp15@67998
  1333
  show ?thesis
lp15@67998
  1334
  proof
lp15@67998
  1335
    show "f ` S \<in> lmeasurable"
lp15@67998
  1336
      using * linordered_field_no_ub by blast
lp15@67998
  1337
    let ?x = "m - ?\<mu> (f ` S)"
lp15@67998
  1338
    have False if "?\<mu> (f ` S) > integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)"
lp15@67998
  1339
    proof -
lp15@67998
  1340
      have ml: "m < ?\<mu> (f ` S)"
lp15@67998
  1341
        using m_def that by blast
lp15@67998
  1342
      then have "?\<mu> S \<noteq> 0"
lp15@67998
  1343
        using "*"(2) bgauge_existence_lemma by fastforce
lp15@67998
  1344
      with ml have 0: "0 < - (m - ?\<mu> (f ` S))/2 / ?\<mu> S"
lp15@67998
  1345
        using that zero_less_measure_iff by force
lp15@67998
  1346
      then show ?thesis
lp15@67998
  1347
        using * [OF 0] that by (auto simp: divide_simps m_def split: if_split_asm)
lp15@67998
  1348
    qed
lp15@67998
  1349
    then show "?\<mu> (f ` S) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)"
lp15@67998
  1350
      by fastforce
lp15@67998
  1351
  qed
lp15@67998
  1352
qed
lp15@67998
  1353
lp15@67998
  1354
lp15@67998
  1355
theorem
lp15@67998
  1356
 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
lp15@67998
  1357
  assumes S: "S \<in> sets lebesgue"
lp15@67998
  1358
    and deriv: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
lp15@67998
  1359
    and int: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on S"
lp15@67998
  1360
  shows measurable_differentiable_image: "f ` S \<in> lmeasurable"
lp15@67998
  1361
    and measure_differentiable_image:
lp15@67998
  1362
       "measure lebesgue (f ` S) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" (is "?M")
lp15@67998
  1363
proof -
lp15@67998
  1364
  let ?I = "\<lambda>n::nat. cbox (vec (-n)) (vec n) \<inter> S"
lp15@67998
  1365
  let ?\<mu> = "measure lebesgue"
lp15@67998
  1366
  have "x \<in> cbox (vec (- real (nat \<lceil>norm x\<rceil>))) (vec (real (nat \<lceil>norm x\<rceil>)))" for x :: "real^'n::_"
lp15@67998
  1367
    apply (auto simp: mem_box_cart)
lp15@67998
  1368
    apply (metis abs_le_iff component_le_norm_cart minus_le_iff of_nat_ceiling order.trans)
lp15@67998
  1369
    by (meson abs_le_D1 norm_bound_component_le_cart real_nat_ceiling_ge)
lp15@67998
  1370
  then have Seq: "S = (\<Union>n. ?I n)"
lp15@67998
  1371
    by auto
lp15@67998
  1372
  have fIn: "f ` ?I n \<in> lmeasurable"
lp15@67998
  1373
       and mfIn: "?\<mu> (f ` ?I n) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" (is ?MN) for n
lp15@67998
  1374
  proof -
lp15@67998
  1375
    have In: "?I n \<in> lmeasurable"
lp15@67998
  1376
      by (simp add: S bounded_Int bounded_set_imp_lmeasurable sets.Int)
lp15@67998
  1377
    moreover have "\<And>x. x \<in> ?I n \<Longrightarrow> (f has_derivative f' x) (at x within ?I n)"
lp15@67998
  1378
      by (meson Int_iff deriv has_derivative_within_subset subsetI)
lp15@67998
  1379
    moreover have int_In: "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) integrable_on ?I n"
lp15@67998
  1380
    proof -
lp15@67998
  1381
      have "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) absolutely_integrable_on S"
lp15@67998
  1382
        using int absolutely_integrable_integrable_bound by force
lp15@67998
  1383
      then have "(\<lambda>x. \<bar>det (matrix (f' x))\<bar>) absolutely_integrable_on ?I n"
lp15@67998
  1384
        by (metis (no_types) Int_lower1 In fmeasurableD inf_commute set_integrable_subset)
lp15@67998
  1385
      then show ?thesis
lp15@67998
  1386
        using absolutely_integrable_on_def by blast
lp15@67998
  1387
    qed
lp15@67998
  1388
    ultimately have "f ` ?I n \<in> lmeasurable" "?\<mu> (f ` ?I n) \<le> integral (?I n) (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)"
lp15@67998
  1389
      using m_diff_image_weak by metis+
lp15@67998
  1390
    moreover have "integral (?I n) (\<lambda>x. \<bar>det (matrix (f' x))\<bar>) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)"
lp15@67998
  1391
      by (simp add: int_In int integral_subset_le)
lp15@67998
  1392
    ultimately show "f ` ?I n \<in> lmeasurable" ?MN
lp15@67998
  1393
      by auto
lp15@67998
  1394
  qed
lp15@67998
  1395
  have "?I k \<subseteq> ?I n" if "k \<le> n" for k n
lp15@67998
  1396
    by (rule Int_mono) (use that in \<open>auto simp: subset_interval_imp_cart\<close>)
lp15@67998
  1397
  then have "(\<Union>k\<le>n. f ` ?I k) = f ` ?I n" for n
lp15@67998
  1398
    by (fastforce simp add:)
lp15@67998
  1399
  with mfIn have "?\<mu> (\<Union>k\<le>n. f ` ?I k) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)" for n
lp15@67998
  1400
    by simp
lp15@67998
  1401
  then have "(\<Union>n. f ` ?I n) \<in> lmeasurable" "?\<mu> (\<Union>n. f ` ?I n) \<le> integral S (\<lambda>x. \<bar>det (matrix (f' x))\<bar>)"
lp15@67998
  1402
    by (rule fmeasurable_countable_Union [OF fIn] measure_countable_Union_le [OF fIn])+
lp15@67998
  1403
  then show "f ` S \<in> lmeasurable" ?M
lp15@67998
  1404
    by (metis Seq image_UN)+
lp15@67998
  1405
qed
lp15@67998
  1406
lp15@67998
  1407
lp15@67998
  1408
lemma borel_measurable_simple_function_limit_increasing:
lp15@67998
  1409
  fixes f :: "'a::euclidean_space \<Rightarrow> real"
lp15@67998
  1410
  shows "(f \<in> borel_measurable lebesgue \<and> (\<forall>x. 0 \<le> f x)) \<longleftrightarrow>
lp15@67998
  1411
         (\<exists>g. (\<forall>n x. 0 \<le> g n x \<and> g n x \<le> f x) \<and> (\<forall>n x. g n x \<le> (g(Suc n) x)) \<and>
lp15@67998
  1412
              (\<forall>n. g n \<in> borel_measurable lebesgue) \<and> (\<forall>n. finite(range (g n))) \<and>
lp15@67998
  1413
              (\<forall>x. (\<lambda>n. g n x) \<longlonglongrightarrow> f x))"
lp15@67998
  1414
         (is "?lhs = ?rhs")
lp15@67998
  1415
proof
lp15@67998
  1416
  assume f: ?lhs
lp15@67998
  1417
  have leb_f: "{x. a \<le> f x \<and> f x < b} \<in> sets lebesgue" for a b
lp15@67998
  1418
  proof -
lp15@67998
  1419
    have "{x. a \<le> f x \<and> f x < b} = {x. f x < b} - {x. f x < a}"
lp15@67998
  1420
      by auto
lp15@67998
  1421
    also have "\<dots> \<in> sets lebesgue"
lp15@67998
  1422
      using borel_measurable_vimage_halfspace_component_lt [of f UNIV] f by auto
lp15@67998
  1423
    finally show ?thesis .
lp15@67998
  1424
  qed
lp15@67998
  1425
  have "g n x \<le> f x"
lp15@67998
  1426
        if inc_g: "\<And>n x. 0 \<le> g n x \<and> g n x \<le> g (Suc n) x"
lp15@67998
  1427
           and meas_g: "\<And>n. g n \<in> borel_measurable lebesgue"
lp15@67998
  1428
           and fin: "\<And>n. finite(range (g n))" and lim: "\<And>x. (\<lambda>n. g n x) \<longlonglongrightarrow> f x" for g n x
lp15@67998
  1429
  proof -
lp15@67998
  1430
    have "\<exists>r>0. \<forall>N. \<exists>n\<ge>N. dist (g n x) (f x) \<ge> r" if "g n x > f x"
lp15@67998
  1431
    proof -
lp15@67998
  1432
      have g: "g n x \<le> g (N + n) x" for N
lp15@67998
  1433
        by (rule transitive_stepwise_le) (use inc_g in auto)
lp15@67998
  1434
      have "\<exists>na\<ge>N. g n x - f x \<le> dist (g na x) (f x)" for N
lp15@67998
  1435
        apply (rule_tac x="N+n" in exI)
lp15@67998
  1436
        using g [of N] by (auto simp: dist_norm)
lp15@67998
  1437
      with that show ?thesis
lp15@67998
  1438
        using diff_gt_0_iff_gt by blast
lp15@67998
  1439
    qed
lp15@67998
  1440
    with lim show ?thesis
lp15@67998
  1441
      apply (auto simp: lim_sequentially)
lp15@67998
  1442
      by (meson less_le_not_le not_le_imp_less)
lp15@67998
  1443
  qed
lp15@67998
  1444
  moreover
lp15@67998
  1445
  let ?\<Omega> = "\<lambda>n k. indicator {y. k/2^n \<le> f y \<and> f y < (k+1)/2^n}"
lp15@67998
  1446
  let ?g = "\<lambda>n x. (\<Sum>k::real | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n). k/2^n * ?\<Omega> n k x)"
lp15@67998
  1447
  have "\<exists>g. (\<forall>n x. 0 \<le> g n x \<and> g n x \<le> (g(Suc n) x)) \<and>
lp15@67998
  1448
             (\<forall>n. g n \<in> borel_measurable lebesgue) \<and> (\<forall>n. finite(range (g n))) \<and>(\<forall>x. (\<lambda>n. g n x) \<longlonglongrightarrow> f x)"
lp15@67998
  1449
  proof (intro exI allI conjI)
lp15@67998
  1450
    show "0 \<le> ?g n x" for n x
lp15@67998
  1451
    proof (clarify intro!: ordered_comm_monoid_add_class.sum_nonneg)
lp15@67998
  1452
      fix k::real
lp15@67998
  1453
      assume "k \<in> \<int>" and k: "\<bar>k\<bar> \<le> 2 ^ (2*n)"
lp15@67998
  1454
      show "0 \<le> k/2^n * ?\<Omega> n k x"
lp15@67998
  1455
        using f \<open>k \<in> \<int>\<close> apply (auto simp: indicator_def divide_simps Ints_def)
lp15@67998
  1456
        apply (drule spec [where x=x])
lp15@67998
  1457
        using zero_le_power [of "2::real" n] mult_nonneg_nonneg [of "f x" "2^n"]
lp15@67998
  1458
        by linarith
lp15@67998
  1459
    qed
lp15@67998
  1460
    show "?g n x \<le> ?g (Suc n) x" for n x
lp15@67998
  1461
    proof -
lp15@67998
  1462
      have "?g n x =
lp15@67998
  1463
            (\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n).
lp15@67998
  1464
              k/2^n * (indicator {y. k/2^n \<le> f y \<and> f y < (k+1/2)/2^n} x +
lp15@67998
  1465
              indicator {y. (k+1/2)/2^n \<le> f y \<and> f y < (k+1)/2^n} x))"
lp15@67998
  1466
        by (rule sum.cong [OF refl]) (simp add: indicator_def divide_simps)
lp15@67998
  1467
      also have "\<dots> = (\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n). k/2^n * indicator {y. k/2^n \<le> f y \<and> f y < (k+1/2)/2^n} x) +
lp15@67998
  1468
                       (\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n). k/2^n * indicator {y. (k+1/2)/2^n \<le> f y \<and> f y < (k+1)/2^n} x)"
lp15@67998
  1469
        by (simp add:  comm_monoid_add_class.sum.distrib algebra_simps)
lp15@67998
  1470
      also have "\<dots> = (\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n). (2 * k)/2 ^ Suc n * indicator {y. (2 * k)/2 ^ Suc n \<le> f y \<and> f y < (2 * k+1)/2 ^ Suc n} x) +
lp15@67998
  1471
                       (\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n). (2 * k)/2 ^ Suc n * indicator {y. (2 * k+1)/2 ^ Suc n \<le> f y \<and> f y < ((2 * k+1) + 1)/2 ^ Suc n} x)"
lp15@67998
  1472
        by (force simp: field_simps indicator_def intro: sum.cong)
lp15@67998
  1473
      also have "\<dots> \<le> (\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2 * Suc n). k/2 ^ Suc n * (indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x))"
lp15@67998
  1474
                (is "?a + _ \<le> ?b")
lp15@67998
  1475
      proof -
lp15@67998
  1476
        have *: "\<lbrakk>sum f I \<le> sum h I; a + sum h I \<le> b\<rbrakk> \<Longrightarrow> a + sum f I \<le> b" for I a b f and h :: "real\<Rightarrow>real"
lp15@67998
  1477
          by linarith
lp15@67998
  1478
        let ?h = "\<lambda>k. (2*k+1)/2 ^ Suc n *
lp15@67998
  1479
                      (indicator {y. (2 * k+1)/2 ^ Suc n \<le> f y \<and> f y < ((2*k+1) + 1)/2 ^ Suc n} x)"
lp15@67998
  1480
        show ?thesis
lp15@67998
  1481
        proof (rule *)
lp15@67998
  1482
          show "(\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n).
lp15@67998
  1483
                  2 * k/2 ^ Suc n * indicator {y. (2 * k+1)/2 ^ Suc n \<le> f y \<and> f y < (2 * k+1 + 1)/2 ^ Suc n} x)
lp15@67998
  1484
                \<le> sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}"
lp15@67998
  1485
            by (rule sum_mono) (simp add: indicator_def divide_simps)
lp15@67998
  1486
        next
lp15@67998
  1487
          have \<alpha>: "?a = (\<Sum>k \<in> ( *)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
lp15@67998
  1488
                         k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)"
lp15@67998
  1489
            by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex)
lp15@67998
  1490
          have \<beta>: "sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}
lp15@67998
  1491
                   = (\<Sum>k \<in> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
lp15@67998
  1492
                      k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)"
lp15@67998
  1493
            by (auto simp: inj_on_def field_simps comm_monoid_add_class.sum.reindex)
lp15@67998
  1494
          have 0: "( *) 2 ` {k \<in> \<int>. P k} \<inter> (\<lambda>x. 2 * x + 1) ` {k \<in> \<int>. P k} = {}" for P :: "real \<Rightarrow> bool"
lp15@67998
  1495
          proof -
lp15@67998
  1496
            have "2 * i \<noteq> 2 * j + 1" for i j :: int by arith
lp15@67998
  1497
            thus ?thesis
lp15@67998
  1498
              unfolding Ints_def by auto (use of_int_eq_iff in fastforce)
lp15@67998
  1499
          qed
lp15@67998
  1500
          have "?a + sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}
lp15@67998
  1501
                = (\<Sum>k \<in> ( *)2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}.
lp15@67998
  1502
                  k/2 ^ Suc n * indicator {y. k/2 ^ Suc n \<le> f y \<and> f y < (k+1)/2 ^ Suc n} x)"
lp15@67998
  1503
            unfolding \<alpha> \<beta>
lp15@67998
  1504
            using finite_abs_int_segment [of "2 ^ (2*n)"]
lp15@67998
  1505
            by (subst sum_Un) (auto simp: 0)
lp15@67998
  1506
          also have "\<dots> \<le> ?b"
lp15@67998
  1507
          proof (rule sum_mono2)
lp15@67998
  1508
            show "finite {k::real. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)}"
lp15@67998
  1509
              by (rule finite_abs_int_segment)
lp15@67998
  1510
            show "( *) 2 ` {k::real. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2^(2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2^(2*n)} \<subseteq> {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)}"
lp15@67998
  1511
              apply auto
lp15@67998
  1512
              using one_le_power [of "2::real" "2*n"]  by linarith
lp15@67998
  1513
            have *: "\<lbrakk>x \<in> (S \<union> T) - U; \<And>x. x \<in> S \<Longrightarrow> x \<in> U; \<And>x. x \<in> T \<Longrightarrow> x \<in> U\<rbrakk> \<Longrightarrow> P x" for S T U P
lp15@67998
  1514
              by blast
lp15@67998
  1515
            have "0 \<le> b" if "b \<in> \<int>" "f x * (2 * 2^n) < b + 1" for b
lp15@67998
  1516
            proof -
lp15@67998
  1517
              have "0 \<le> f x * (2 * 2^n)"
lp15@67998
  1518
                by (simp add: f)
lp15@67998
  1519
              also have "\<dots> < b+1"
lp15@67998
  1520
                by (simp add: that)
lp15@67998
  1521
              finally show "0 \<le> b"
lp15@67998
  1522
                using \<open>b \<in> \<int>\<close> by (auto simp: elim!: Ints_cases)
lp15@67998
  1523
            qed
lp15@67998
  1524
            then show "0 \<le> b/2 ^ Suc n * indicator {y. b/2 ^ Suc n \<le> f y \<and> f y < (b + 1)/2 ^ Suc n} x"
lp15@67998
  1525
                  if "b \<in> {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2 * Suc n)} -
lp15@67998
  1526
                          (( *) 2 ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<union> (\<lambda>x. 2*x + 1) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)})" for b
lp15@67998
  1527
              using that by (simp add: indicator_def divide_simps)
lp15@67998
  1528
          qed
lp15@67998
  1529
          finally show "?a + sum ?h {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)} \<le> ?b" .
lp15@67998
  1530
        qed
lp15@67998
  1531
      qed
lp15@67998
  1532
      finally show ?thesis .
lp15@67998
  1533
    qed
lp15@67998
  1534
    show "?g n \<in> borel_measurable lebesgue" for n
lp15@67998
  1535
      apply (intro borel_measurable_indicator borel_measurable_times borel_measurable_sum)
lp15@67998
  1536
      using leb_f sets_restrict_UNIV by auto
lp15@67998
  1537
    show "finite (range (?g n))" for n
lp15@67998
  1538
    proof -
lp15@67998
  1539
      have "(\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n). k/2^n * ?\<Omega> n k x)
lp15@67998
  1540
              \<in> (\<lambda>k. k/2^n) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)}" for x
lp15@67998
  1541
      proof (cases "\<exists>k. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n) \<and> k/2^n \<le> f x \<and> f x < (k+1)/2^n")
lp15@67998
  1542
        case True
lp15@67998
  1543
        then show ?thesis
lp15@67998
  1544
          by (blast intro: indicator_sum_eq)
lp15@67998
  1545
      next
lp15@67998
  1546
        case False
lp15@67998
  1547
        then have "(\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n). k/2^n * ?\<Omega> n k x) = 0"
lp15@67998
  1548
          by auto
lp15@67998
  1549
        then show ?thesis by force
lp15@67998
  1550
      qed
lp15@67998
  1551
      then have "range (?g n) \<subseteq> ((\<lambda>k. (k/2^n)) ` {k. k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n)})"
lp15@67998
  1552
        by auto
lp15@67998
  1553
      moreover have "finite ((\<lambda>k::real. (k/2^n)) ` {k \<in> \<int>. \<bar>k\<bar> \<le> 2 ^ (2*n)})"
lp15@67998
  1554
        by (intro finite_imageI finite_abs_int_segment)
lp15@67998
  1555
      ultimately show ?thesis
lp15@67998
  1556
        by (rule finite_subset)
lp15@67998
  1557
    qed
lp15@67998
  1558
    show "(\<lambda>n. ?g n x) \<longlonglongrightarrow> f x" for x
lp15@67998
  1559
    proof (clarsimp simp add: lim_sequentially)
lp15@67998
  1560
      fix e::real
lp15@67998
  1561
      assume "e > 0"
lp15@67998
  1562
      obtain N1 where N1: "2 ^ N1 > abs(f x)"
lp15@67998
  1563
        using real_arch_pow by fastforce
lp15@67998
  1564
      obtain N2 where N2: "(1/2) ^ N2 < e"
lp15@67998
  1565
        using real_arch_pow_inv \<open>e > 0\<close> by fastforce
lp15@67998
  1566
      have "dist (\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n). k/2^n * ?\<Omega> n k x) (f x) < e" if "N1 + N2 \<le> n" for n
lp15@67998
  1567
      proof -
lp15@67998
  1568
        let ?m = "real_of_int \<lfloor>2^n * f x\<rfloor>"
lp15@67998
  1569
        have "\<bar>?m\<bar> \<le> 2^n * 2^N1"
lp15@67998
  1570
          using N1 apply (simp add: f)
lp15@67998
  1571
          by (meson floor_mono le_floor_iff less_le_not_le mult_le_cancel_left_pos zero_less_numeral zero_less_power)
lp15@67998
  1572
        also have "\<dots> \<le> 2 ^ (2*n)"
lp15@67998
  1573
          by (metis that add_leD1 add_le_cancel_left mult.commute mult_2_right one_less_numeral_iff
lp15@67998
  1574
                    power_add power_increasing_iff semiring_norm(76))
lp15@67998
  1575
        finally have m_le: "\<bar>?m\<bar> \<le> 2 ^ (2*n)" .
lp15@67998
  1576
        have "?m/2^n \<le> f x" "f x < (?m + 1)/2^n"
lp15@67998
  1577
          by (auto simp: mult.commute pos_divide_le_eq mult_imp_less_div_pos)
lp15@67998
  1578
        then have eq: "dist (\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n). k/2^n * ?\<Omega> n k x) (f x)
lp15@67998
  1579
                     = dist (?m/2^n) (f x)"
lp15@67998
  1580
          by (subst indicator_sum_eq [of ?m]) (auto simp: m_le)
lp15@67998
  1581
        have "\<bar>2^n\<bar> * \<bar>?m/2^n - f x\<bar> = \<bar>2^n * (?m/2^n - f x)\<bar>"
lp15@67998
  1582
          by (simp add: abs_mult)
lp15@67998
  1583
        also have "\<dots> < 2 ^ N2 * e"
lp15@67998
  1584
          using N2 by (simp add: divide_simps mult.commute) linarith
lp15@67998
  1585
        also have "\<dots> \<le> \<bar>2^n\<bar> * e"
lp15@67998
  1586
          using that \<open>e > 0\<close> by auto
lp15@67998
  1587
        finally have "dist (?m/2^n) (f x) < e"
lp15@67998
  1588
          by (simp add: dist_norm)
lp15@67998
  1589
        then show ?thesis
lp15@67998
  1590
          using eq by linarith
lp15@67998
  1591
      qed
lp15@67998
  1592
      then show "\<exists>no. \<forall>n\<ge>no. dist (\<Sum>k | k \<in> \<int> \<and> \<bar>k\<bar> \<le> 2 ^ (2*n). k * ?\<Omega> n k x/2^n) (f x) < e"
lp15@67998
  1593
        by force
lp15@67998
  1594
    qed
lp15@67998
  1595
  qed
lp15@67998
  1596
  ultimately show ?rhs
lp15@67998
  1597
    by metis
lp15@67998
  1598
next
lp15@67998
  1599
  assume RHS: ?rhs
lp15@67998
  1600
  with borel_measurable_simple_function_limit [of f UNIV, unfolded borel_measurable_UNIV_eq]
lp15@67998
  1601
  show ?lhs
lp15@67998
  1602
    by (blast intro: order_trans)
lp15@67998
  1603
qed
lp15@67998
  1604
lp15@67998
  1605
subsection\<open>Borel measurable Jacobian determinant\<close>
lp15@67998
  1606
lp15@67998
  1607
lemma lemma_partial_derivatives0:
lp15@67998
  1608
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@67998
  1609
  assumes "linear f" and lim0: "((\<lambda>x. f x /\<^sub>R norm x) \<longlongrightarrow> 0) (at 0 within S)"
lp15@67998
  1610
    and lb: "\<And>v. v \<noteq> 0 \<Longrightarrow> (\<exists>k>0. \<forall>e>0. \<exists>x. x \<in> S - {0} \<and> norm x < e \<and> k * norm x \<le> \<bar>v \<bullet> x\<bar>)"
lp15@67998
  1611
  shows "f x = 0"
lp15@67998
  1612
proof -
lp15@67998
  1613
  have "dim {x. f x = 0} \<le> DIM('a)"
lp15@67998
  1614
    using dim_subset_UNIV by blast
lp15@67998
  1615
  moreover have False if less: "dim {x. f x = 0} < DIM('a)"
lp15@67998
  1616
  proof -
lp15@67998
  1617
    obtain d where "d \<noteq> 0" and d: "\<And>y. f y = 0 \<Longrightarrow> d \<bullet> y = 0"
lp15@67998
  1618
      using orthogonal_to_subspace_exists [OF less] orthogonal_def
lp15@67998
  1619
      by (metis (mono_tags, lifting) mem_Collect_eq span_clauses(1))
lp15@67998
  1620
    then obtain k where "k > 0"
lp15@67998
  1621
      and k: "\<And>e. e > 0 \<Longrightarrow> \<exists>y. y \<in> S - {0} \<and> norm y < e \<and> k * norm y \<le> \<bar>d \<bullet> y\<bar>"
lp15@67998
  1622
      using lb by blast
lp15@67998
  1623
    have "\<exists>h. \<forall>n. ((h n \<in> S \<and> h n \<noteq> 0 \<and> k * norm (h n) \<le> \<bar>d \<bullet> h n\<bar>) \<and> norm (h n) < 1 / real (Suc n)) \<and>
lp15@67998
  1624
               norm (h (Suc n)) < norm (h n)"
lp15@67998
  1625
    proof (rule dependent_nat_choice)
lp15@67998
  1626
      show "\<exists>y. (y \<in> S \<and> y \<noteq> 0 \<and> k * norm y \<le> \<bar>d \<bullet> y\<bar>) \<and> norm y < 1 / real (Suc 0)"
lp15@67998
  1627
        by simp (metis DiffE insertCI k not_less not_one_le_zero)
lp15@67998
  1628
    qed (use k [of "min (norm x) (1/(Suc n + 1))" for x n] in auto)
lp15@67998
  1629
    then obtain \<alpha> where \<alpha>: "\<And>n. \<alpha> n \<in> S - {0}" and kd: "\<And>n. k * norm(\<alpha> n) \<le> \<bar>d \<bullet> \<alpha> n\<bar>"
lp15@67998
  1630
         and norm_lt: "\<And>n. norm(\<alpha> n) < 1/(Suc n)"
lp15@67998
  1631
      by force
lp15@67998
  1632
    let ?\<beta> = "\<lambda>n. \<alpha> n /\<^sub>R norm (\<alpha> n)"
lp15@67998
  1633
    have com: "\<And>g. (\<forall>n. g n \<in> sphere (0::'a) 1)
lp15@67998
  1634
              \<Longrightarrow> \<exists>l \<in> sphere 0 1. \<exists>\<rho>::nat\<Rightarrow>nat. strict_mono \<rho> \<and> (g \<circ> \<rho>) \<longlonglongrightarrow> l"
lp15@67998
  1635
      using compact_sphere compact_def by metis
lp15@67998
  1636
    moreover have "\<forall>n. ?\<beta> n \<in> sphere 0 1"
lp15@67998
  1637
      using \<alpha> by auto
lp15@67998
  1638
    ultimately obtain l::'a and \<rho>::"nat\<Rightarrow>nat"
lp15@67998
  1639
       where l: "l \<in> sphere 0 1" and "strict_mono \<rho>" and to_l: "(?\<beta> \<circ> \<rho>) \<longlonglongrightarrow> l"
lp15@67998
  1640
      by meson
lp15@67998
  1641
    moreover have "continuous (at l) (\<lambda>x. (\<bar>d \<bullet> x\<bar> - k))"
lp15@67998
  1642
      by (intro continuous_intros)
lp15@67998
  1643
    ultimately have lim_dl: "((\<lambda>x. (\<bar>d \<bullet> x\<bar> - k)) \<circ> (?\<beta> \<circ> \<rho>)) \<longlonglongrightarrow> (\<bar>d \<bullet> l\<bar> - k)"
lp15@67998
  1644
      by (meson continuous_imp_tendsto)
lp15@67998
  1645
    have "\<forall>\<^sub>F i in sequentially. 0 \<le> ((\<lambda>x. \<bar>d \<bullet> x\<bar> - k) \<circ> ((\<lambda>n. \<alpha> n /\<^sub>R norm (\<alpha> n)) \<circ> \<rho>)) i"
lp15@67998
  1646
      using \<alpha> kd by (auto simp: divide_simps)
lp15@67998
  1647
    then have "k \<le> \<bar>d \<bullet> l\<bar>"
lp15@67998
  1648
      using tendsto_lowerbound [OF lim_dl, of 0] by auto
lp15@67998
  1649
    moreover have "d \<bullet> l = 0"
lp15@67998
  1650
    proof (rule d)
lp15@67998
  1651
      show "f l = 0"
lp15@67998
  1652
      proof (rule LIMSEQ_unique [of "f \<circ> ?\<beta> \<circ> \<rho>"])
lp15@67998
  1653
        have "isCont f l"
lp15@67998
  1654
          using \<open>linear f\<close> linear_continuous_at linear_conv_bounded_linear by blast
lp15@67998
  1655
        then show "(f \<circ> (\<lambda>n. \<alpha> n /\<^sub>R norm (\<alpha> n)) \<circ> \<rho>) \<longlonglongrightarrow> f l"
lp15@67998
  1656
          unfolding comp_assoc
lp15@67998
  1657
          using to_l continuous_imp_tendsto by blast
lp15@67998
  1658
        have "\<alpha> \<longlonglongrightarrow> 0"
lp15@67998
  1659
          using norm_lt LIMSEQ_norm_0 by metis
lp15@67998
  1660
        with \<open>strict_mono \<rho>\<close> have "(\<alpha> \<circ> \<rho>) \<longlonglongrightarrow> 0"
lp15@67998
  1661
          by (metis LIMSEQ_subseq_LIMSEQ)
lp15@67998
  1662
        with lim0 \<alpha> have "((\<lambda>x. f x /\<^sub>R norm x) \<circ> (\<alpha> \<circ> \<rho>)) \<longlonglongrightarrow> 0"
lp15@67998
  1663
          by (force simp: tendsto_at_iff_sequentially)
lp15@67998
  1664
        then show "(f \<circ> (\<lambda>n. \<alpha> n /\<^sub>R norm (\<alpha> n)) \<circ> \<rho>) \<longlonglongrightarrow> 0"
lp15@67998
  1665
          by (simp add: o_def linear_cmul \<open>linear f\<close>)
lp15@67998
  1666
      qed
lp15@67998
  1667
    qed
lp15@67998
  1668
    ultimately show False
lp15@67998
  1669
      using \<open>k > 0\<close> by auto
lp15@67998
  1670
  qed
lp15@67998
  1671
  ultimately have dim: "dim {x. f x = 0} = DIM('a)"
lp15@67998
  1672
    by force
lp15@67998
  1673
  then show ?thesis
lp15@67998
  1674
    by (metis (mono_tags, lifting) UNIV_I assms(1) dim_eq_full linear_eq_0_span mem_Collect_eq)
lp15@67998
  1675
qed
lp15@67998
  1676
lp15@67998
  1677
lemma lemma_partial_derivatives:
lp15@67998
  1678
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@67998
  1679
  assumes "linear f" and lim: "((\<lambda>x. f (x - a) /\<^sub>R norm (x - a)) \<longlongrightarrow> 0) (at a within S)"
lp15@67998
  1680
    and lb: "\<And>v. v \<noteq> 0 \<Longrightarrow> (\<exists>k>0.  \<forall>e>0. \<exists>x \<in> S - {a}. norm(a - x) < e \<and> k * norm(a - x) \<le> \<bar>v \<bullet> (x - a)\<bar>)"
lp15@67998
  1681
  shows "f x = 0"
lp15@67998
  1682
proof -
lp15@67998
  1683
  have "((\<lambda>x. f x /\<^sub>R norm x) \<longlongrightarrow> 0) (at 0 within (\<lambda>x. x-a) ` S)"
lp15@67998
  1684
    using lim by (simp add: Lim_within dist_norm)
lp15@67998
  1685
  then show ?thesis
lp15@67998
  1686
  proof (rule lemma_partial_derivatives0 [OF \<open>linear f\<close>])
lp15@67998
  1687
    fix v :: "'a"
lp15@67998
  1688
    assume v: "v \<noteq> 0"
lp15@67998
  1689
    show "\<exists>k>0. \<forall>e>0. \<exists>x. x \<in> (\<lambda>x. x - a) ` S - {0} \<and> norm x < e \<and> k * norm x \<le> \<bar>v \<bullet> x\<bar>"
lp15@67998
  1690
      using lb [OF v] by (force simp:  norm_minus_commute)
lp15@67998
  1691
  qed
lp15@67998
  1692
qed
lp15@67998
  1693
lp15@67998
  1694
lp15@67998
  1695
proposition borel_measurable_partial_derivatives:
lp15@67998
  1696
  fixes f :: "real^'m::{finite,wellorder} \<Rightarrow> real^'n"
lp15@67998
  1697
  assumes S: "S \<in> sets lebesgue"
lp15@67998
  1698
    and f: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
lp15@67998
  1699
  shows "(\<lambda>x. (matrix(f' x)$m$n)) \<in> borel_measurable (lebesgue_on S)"
lp15@67998
  1700
proof -
lp15@67998
  1701
  have contf: "continuous_on S f"
lp15@67998
  1702
    using continuous_on_eq_continuous_within f has_derivative_continuous by blast
lp15@67998
  1703
  have "{x \<in> S.  (matrix (f' x)$m$n) \<le> b} \<in> sets lebesgue" for b
lp15@67998
  1704
  proof (rule sets_negligible_symdiff)
lp15@67998
  1705
    let ?T = "{x \<in> S. \<forall>e>0. \<exists>d>0. \<exists>A. A$m$n < b \<and> (\<forall>i j. A$i$j \<in> \<rat>) \<and>
lp15@67998
  1706
                       (\<forall>y \<in> S. norm(y - x) < d \<longrightarrow> norm(f y - f x - A *v (y - x)) \<le> e * norm(y - x))}"
lp15@67998
  1707
    let ?U = "S \<inter>
lp15@67998
  1708
              (\<Inter>e \<in> {e \<in> \<rat>. e > 0}.
lp15@67998
  1709
                \<Union>A \<in> {A. A$m$n < b \<and> (\<forall>i j. A$i$j \<in> \<rat>)}.
lp15@67998
  1710
                  \<Union>d \<in> {d \<in> \<rat>. 0 < d}.
lp15@67998
  1711
                     S \<inter> (\<Inter>y \<in> S. {x \<in> S. norm(y - x) < d \<longrightarrow> norm(f y - f x - A *v (y - x)) \<le> e * norm(y - x)}))"
lp15@67998
  1712
    have "?T = ?U"
lp15@67998
  1713
    proof (intro set_eqI iffI)
lp15@67998
  1714
      fix x
lp15@67998
  1715
      assume xT: "x \<in> ?T"
lp15@67998
  1716
      then show "x \<in> ?U"
lp15@67998
  1717
      proof (clarsimp simp add:)
lp15@67998
  1718
        fix q :: real
lp15@67998
  1719
        assume "q \<in> \<rat>" "q > 0"
lp15@67998
  1720
        then obtain d A where "d > 0" and A: "A $ m $ n < b" "\<And>i j. A $ i $ j \<in> \<rat>"
lp15@67998
  1721
          "\<And>y. \<lbrakk>y\<in>S;  norm (y - x) < d\<rbrakk> \<Longrightarrow> norm (f y - f x - A *v (y - x)) \<le> q * norm (y - x)"
lp15@67998
  1722
          using xT by auto
lp15@67998
  1723
        then obtain \<delta> where "d > \<delta>" "\<delta> > 0" "\<delta> \<in> \<rat>"
lp15@67998
  1724
          using Rats_dense_in_real by blast
lp15@67998
  1725
        with A show "\<exists>A. A $ m $ n < b \<and> (\<forall>i j. A $ i $ j \<in> \<rat>) \<and>
lp15@67998
  1726
                         (\<exists>s. s \<in> \<rat> \<and> 0 < s \<and> (\<forall>y\<in>S. norm (y - x) < s \<longrightarrow> norm (f y - f x - A *v (y - x)) \<le> q * norm (y - x)))"
lp15@67998
  1727
          by force
lp15@67998
  1728
      qed
lp15@67998
  1729
    next
lp15@67998
  1730
      fix x
lp15@67998
  1731
      assume xU: "x \<in> ?U"
lp15@67998
  1732
      then show "x \<in> ?T"
lp15@67998
  1733
      proof clarsimp
lp15@67998
  1734
        fix e :: "real"
lp15@67998
  1735
        assume "e > 0"
lp15@67998
  1736
        then obtain \<epsilon> where \<epsilon>: "e > \<epsilon>" "\<epsilon> > 0" "\<epsilon> \<in> \<rat>"
lp15@67998
  1737
          using Rats_dense_in_real by blast
lp15@67998
  1738
        with xU obtain A r where "x \<in> S" and Ar: "A $ m $ n < b" "\<forall>i j. A $ i $ j \<in> \<rat>" "r \<in> \<rat>" "r > 0"
lp15@67998
  1739
          and "\<forall>y\<in>S. norm (y - x) < r \<longrightarrow> norm (f y - f x - A *v (y - x)) \<le> \<epsilon> * norm (y - x)"
lp15@67998
  1740
          by (auto simp: split: if_split_asm)
lp15@67998
  1741
        then have "\<forall>y\<in>S. norm (y - x) < r \<longrightarrow> norm (f y - f x - A *v (y - x)) \<le> e * norm (y - x)"
lp15@67998
  1742
          by (meson \<open>e > \<epsilon>\<close> less_eq_real_def mult_right_mono norm_ge_zero order_trans)
lp15@67998
  1743
        then show "\<exists>d>0. \<exists>A. A $ m $ n < b \<and> (\<forall>i j. A $ i $ j \<in> \<rat>) \<and> (\<forall>y\<in>S. norm (y - x) < d \<longrightarrow> norm (f y - f x - A *v (y - x)) \<le> e * norm (y - x))"
lp15@67998
  1744
          using \<open>x \<in> S\<close> Ar by blast
lp15@67998
  1745
      qed
lp15@67998
  1746
    qed
lp15@67998
  1747
    moreover have "?U \<in> sets lebesgue"
lp15@67998
  1748
    proof -
lp15@67998
  1749
      have coQ: "countable {e \<in> \<rat>. 0 < e}"
lp15@67998
  1750
        using countable_Collect countable_rat by blast
lp15@67998
  1751
      have ne: "{e \<in> \<rat>. (0::real) < e} \<noteq> {}"
lp15@67998
  1752
        using zero_less_one Rats_1 by blast
lp15@67998
  1753
      have coA: "countable {A. A $ m $ n < b \<and> (\<forall>i j. A $ i $ j \<in> \<rat>)}"
lp15@67998
  1754
      proof (rule countable_subset)
lp15@67998
  1755
        show "countable {A. \<forall>i j. A $ i $ j \<in> \<rat>}"
lp15@67998
  1756
          using countable_vector [OF countable_vector, of "\<lambda>i j. \<rat>"] by (simp add: countable_rat)
lp15@67998
  1757
      qed blast
lp15@67998
  1758
      have *: "\<lbrakk>U \<noteq> {} \<Longrightarrow> closedin (subtopology euclidean S) (S \<inter> \<Inter> U)\<rbrakk>
lp15@67998
  1759
               \<Longrightarrow> closedin (subtopology euclidean S) (S \<inter> \<Inter> U)" for U
lp15@67998
  1760
        by fastforce
lp15@67998
  1761
      have eq: "{x::(real,'m)vec. P x \<and> (Q x \<longrightarrow> R x)} = {x. P x \<and> \<not> Q x} \<union> {x. P x \<and> R x}" for P Q R
lp15@67998
  1762
        by auto
lp15@67998
  1763
      have sets: "S \<inter> (\<Inter>y\<in>S. {x \<in> S. norm (y - x) < d \<longrightarrow> norm (f y - f x - A *v (y - x)) \<le> e * norm (y - x)})
lp15@67998
  1764
                  \<in> sets lebesgue" for e A d
lp15@67998
  1765
      proof -
lp15@67998
  1766
        have clo: "closedin (subtopology euclidean S)
lp15@67998
  1767
                     {x \<in> S. norm (y - x) < d \<longrightarrow> norm (f y - f x - A *v (y - x)) \<le> e * norm (y - x)}"
lp15@67998
  1768
          for y
lp15@67998
  1769
        proof -
lp15@67998
  1770
          have cont1: "continuous_on S (\<lambda>x. norm (y - x))"
lp15@67998
  1771
          and  cont2: "continuous_on S (\<lambda>x. e * norm (y - x) - norm (f y - f x - (A *v y - A *v x)))"
lp15@67998
  1772
            by (force intro: contf continuous_intros)+
lp15@67998
  1773
          have clo1: "closedin (subtopology euclidean S) {x \<in> S. d \<le> norm (y - x)}"
lp15@67998
  1774
            using continuous_closedin_preimage [OF cont1, of "{d..}"] by (simp add: vimage_def Int_def)
lp15@67998
  1775
          have clo2: "closedin (subtopology euclidean S)
lp15@67998
  1776
                       {x \<in> S. norm (f y - f x - (A *v y - A *v x)) \<le> e * norm (y - x)}"
lp15@67998
  1777
            using continuous_closedin_preimage [OF cont2, of "{0..}"] by (simp add: vimage_def Int_def)
lp15@67998
  1778
          show ?thesis
lp15@67998
  1779
            by (auto simp: eq not_less matrix_vector_mult_diff_distrib intro: clo1 clo2)
lp15@67998
  1780
        qed
lp15@67998
  1781
        show ?thesis
lp15@67998
  1782
          by (rule lebesgue_closedin [of S]) (force intro: * S clo)+
lp15@67998
  1783
      qed
lp15@67998
  1784
      show ?thesis
lp15@67998
  1785
        by (intro sets sets.Int S sets.countable_UN'' sets.countable_INT'' coQ coA) auto
lp15@67998
  1786
    qed
lp15@67998
  1787
    ultimately show "?T \<in> sets lebesgue"
lp15@67998
  1788
      by simp
lp15@67998
  1789
    let ?M = "(?T - {x \<in> S. matrix (f' x) $ m $ n \<le> b} \<union> ({x \<in> S. matrix (f' x) $ m $ n \<le> b} - ?T))"
lp15@67998
  1790
    let ?\<Theta> = "\<lambda>x v. \<forall>\<xi>>0. \<exists>e>0. \<forall>y \<in> S-{x}. norm (x - y) < e \<longrightarrow> \<bar>v \<bullet> (y - x)\<bar> < \<xi> * norm (x - y)"
lp15@67998
  1791
    have nN: "negligible {x \<in> S. \<exists>v\<noteq>0. ?\<Theta> x v}"
lp15@67998
  1792
      unfolding negligible_eq_zero_density
lp15@67998
  1793
    proof clarsimp
lp15@67998
  1794
      fix x v and r e :: "real"
lp15@67998
  1795
      assume "x \<in> S" "v \<noteq> 0" "r > 0" "e > 0"
lp15@67998
  1796
      and Theta [rule_format]: "?\<Theta> x v"
lp15@67998
  1797
      moreover have "(norm v * e / 2) / CARD('m) ^ CARD('m) > 0"
lp15@67998
  1798
        by (simp add: \<open>v \<noteq> 0\<close> \<open>e > 0\<close>)
lp15@67998
  1799
      ultimately obtain d where "d > 0"
lp15@67998
  1800
         and dless: "\<And>y. \<lbrakk>y \<in> S - {x}; norm (x - y) < d\<rbrakk> \<Longrightarrow>
lp15@67998
  1801
                        \<bar>v \<bullet> (y - x)\<bar> < ((norm v * e / 2) / CARD('m) ^ CARD('m)) * norm (x - y)"
lp15@67998
  1802
        by metis
lp15@67998
  1803
      let ?W = "ball x (min d r) \<inter> {y. \<bar>v \<bullet> (y - x)\<bar> < (norm v * e/2 * min d r) / CARD('m) ^ CARD('m)}"
lp15@67998
  1804
      have "open {x. \<bar>v \<bullet> (x - a)\<bar> < b}" for a b
lp15@67998
  1805
        by (intro open_Collect_less continuous_intros)
lp15@67998
  1806
      show "\<exists>d>0. d \<le> r \<and>
lp15@67998
  1807
            (\<exists>U. {x' \<in> S. \<exists>v\<noteq>0. ?\<Theta> x' v} \<inter> ball x d \<subseteq> U \<and>
lp15@67998
  1808
                 U \<in> lmeasurable \<and> measure lebesgue U < e * content (ball x d))"
lp15@67998
  1809
      proof (intro exI conjI)
lp15@67998
  1810
        show "0 < min d r" "min d r \<le> r"
lp15@67998
  1811
          using \<open>r > 0\<close> \<open>d > 0\<close> by auto
lp15@67998
  1812
        show "{x' \<in> S. \<exists>v. v \<noteq> 0 \<and> (\<forall>\<xi>>0. \<exists>e>0. \<forall>z\<in>S - {x'}. norm (x' - z) < e \<longrightarrow> \<bar>v \<bullet> (z - x')\<bar> < \<xi> * norm (x' - z))} \<inter> ball x (min d r) \<subseteq> ?W"
lp15@67998
  1813
          proof (clarsimp simp: dist_norm norm_minus_commute)
lp15@68001
  1814
            fix y w
lp15@67998
  1815
            assume "y \<in> S" "w \<noteq> 0"
lp15@67998
  1816
              and less [rule_format]:
lp15@67998
  1817
                    "\<forall>\<xi>>0. \<exists>e>0. \<forall>z\<in>S - {y}. norm (y - z) < e \<longrightarrow> \<bar>w \<bullet> (z - y)\<bar> < \<xi> * norm (y - z)"
lp15@67998
  1818
              and d: "norm (y - x) < d" and r: "norm (y - x) < r"
lp15@67998
  1819
            show "\<bar>v \<bullet> (y - x)\<bar> < norm v * e * min d r / (2 * real CARD('m) ^ CARD('m))"
lp15@67998
  1820
            proof (cases "y = x")
lp15@67998
  1821
              case True
lp15@67998
  1822
              with \<open>r > 0\<close> \<open>d > 0\<close> \<open>e > 0\<close> \<open>v \<noteq> 0\<close> show ?thesis
lp15@67998
  1823
                by simp
lp15@67998
  1824
            next
lp15@67998
  1825
              case False
lp15@67998
  1826
              have "\<bar>v \<bullet> (y - x)\<bar> < norm v * e / 2 / real (CARD('m) ^ CARD('m)) * norm (x - y)"
lp15@67998
  1827
                apply (rule dless)
lp15@67998
  1828
                using False \<open>y \<in> S\<close> d by (auto simp: norm_minus_commute)
lp15@67998
  1829
              also have "\<dots> \<le> norm v * e * min d r / (2 * real CARD('m) ^ CARD('m))"
lp15@67998
  1830
                using d r \<open>e > 0\<close> by (simp add: field_simps norm_minus_commute mult_left_mono)
lp15@67998
  1831
              finally show ?thesis .
lp15@67998
  1832
            qed
lp15@67998
  1833
          qed
lp15@67998
  1834
          show "?W \<in> lmeasurable"
lp15@67998
  1835
            by (simp add: fmeasurable_Int_fmeasurable borel_open)
lp15@67998
  1836
          obtain k::'m where True
lp15@67998
  1837
            by metis
lp15@67998
  1838
          obtain T where T: "orthogonal_transformation T" and v: "v = T(norm v *\<^sub>R axis k (1::real))"
lp15@67998
  1839
            using rotation_rightward_line by metis
lp15@67998
  1840
          define b where "b \<equiv> norm v"
lp15@67998
  1841
          have "b > 0"
lp15@67998
  1842
            using \<open>v \<noteq> 0\<close> by (auto simp: b_def)
lp15@67998
  1843
          obtain eqb: "inv T v = b *\<^sub>R axis k (1::real)" and "inj T" "bij T" and invT: "orthogonal_transformation (inv T)"
lp15@67998
  1844
            by (metis UNIV_I b_def  T v bij_betw_inv_into_left orthogonal_transformation_inj orthogonal_transformation_bij orthogonal_transformation_inv)
lp15@67998
  1845
          let ?v = "\<chi> i. min d r / CARD('m)"
lp15@67998
  1846
          let ?v' = "\<chi> i. if i = k then (e/2 * min d r) / CARD('m) ^ CARD('m) else min d r"
lp15@67998
  1847
          let ?x' = "inv T x"
lp15@67998
  1848
          let ?W' = "(ball ?x' (min d r) \<inter> {y. \<bar>(y - ?x')$k\<bar> < e * min d r / (2 * CARD('m) ^ CARD('m))})"
lp15@67998
  1849
          have abs: "x - e \<le> y \<and> y \<le> x + e \<longleftrightarrow> abs(y - x) \<le> e" for x y e::real
lp15@67998
  1850
            by auto
lp15@67998
  1851
          have "?W = T ` ?W'"
lp15@67998
  1852
          proof -
lp15@67998
  1853
            have 1: "T ` (ball (inv T x) (min d r)) = ball x (min d r)"
lp15@67998
  1854
              by (simp add: T image_orthogonal_transformation_ball orthogonal_transformation_surj surj_f_inv_f)
lp15@67998
  1855
            have 2: "{y. \<bar>v \<bullet> (y - x)\<bar> < b * e * min d r / (2 * real CARD('m) ^ CARD('m))} =
lp15@67998
  1856
                      T ` {y. \<bar>y $ k - ?x' $ k\<bar> < e * min d r / (2 * real CARD('m) ^ CARD('m))}"
lp15@67998
  1857
            proof -
lp15@67998
  1858
              have *: "\<bar>T (b *\<^sub>R axis k 1) \<bullet> (y - x)\<bar> = b * \<bar>inv T y $ k - ?x' $ k\<bar>" for y
lp15@67998
  1859
              proof -
lp15@67998
  1860
                have "\<bar>T (b *\<^sub>R axis k 1) \<bullet> (y - x)\<bar> = \<bar>(b *\<^sub>R axis k 1) \<bullet> inv T (y - x)\<bar>"
lp15@67998
  1861
                  by (metis (no_types, hide_lams) b_def eqb invT orthogonal_transformation_def v)
lp15@67998
  1862
                also have "\<dots> = b * \<bar>(axis k 1) \<bullet> inv T (y - x)\<bar>"
lp15@67998
  1863
                  using \<open>b > 0\<close> by (simp add: abs_mult)
lp15@67998
  1864
                also have "\<dots> = b * \<bar>inv T y $ k - ?x' $ k\<bar>"
lp15@67998
  1865
                  using orthogonal_transformation_linear [OF invT]
lp15@67998
  1866
                  by (simp add: inner_axis' linear_diff)
lp15@67998
  1867
                finally show ?thesis
lp15@67998
  1868
                  by simp
lp15@67998
  1869
              qed
lp15@67998
  1870
              show ?thesis
lp15@67998
  1871
                using v b_def [symmetric]
lp15@67998
  1872
                using \<open>b > 0\<close> by (simp add: * bij_image_Collect_eq [OF \<open>bij T\<close>] mult_less_cancel_left_pos times_divide_eq_right [symmetric] del: times_divide_eq_right)
lp15@67998
  1873
            qed
lp15@67998
  1874
            show ?thesis
lp15@67998
  1875
              using \<open>b > 0\<close> by (simp add: image_Int \<open>inj T\<close> 1 2 b_def [symmetric])
lp15@67998
  1876
          qed
lp15@67998
  1877
          moreover have "?W' \<in> lmeasurable"
lp15@67998
  1878
            by (auto intro: fmeasurable_Int_fmeasurable)
lp15@67998
  1879
          ultimately have "measure lebesgue ?W = measure lebesgue ?W'"
lp15@67998
  1880
            by (metis measure_orthogonal_image T)
lp15@67998
  1881
          also have "\<dots> \<le> measure lebesgue (cbox (?x' - ?v') (?x' + ?v'))"
lp15@67998
  1882
          proof (rule measure_mono_fmeasurable)
lp15@67998
  1883
            show "?W' \<subseteq> cbox (?x' - ?v') (?x' + ?v')"
lp15@67998
  1884
              apply (clarsimp simp add: mem_box_cart abs dist_norm norm_minus_commute simp del: min_less_iff_conj min.bounded_iff)
lp15@67998
  1885
              by (metis component_le_norm_cart less_eq_real_def le_less_trans vector_minus_component)
lp15@67998
  1886
          qed auto
lp15@67998
  1887
          also have "\<dots> \<le> e/2 * measure lebesgue (cbox (?x' - ?v) (?x' + ?v))"
lp15@67998
  1888
          proof -
lp15@67998
  1889
            have "cbox (?x' - ?v) (?x' + ?v) \<noteq> {}"
lp15@67998
  1890
              using \<open>r > 0\<close> \<open>d > 0\<close> by (auto simp: interval_eq_empty_cart divide_less_0_iff)
lp15@67998
  1891
            with \<open>r > 0\<close> \<open>d > 0\<close> \<open>e > 0\<close> show ?thesis
lp15@67998
  1892
              apply (simp add: content_cbox_if_cart mem_box_cart)
lp15@67998
  1893
              apply (auto simp: prod_nonneg)
lp15@67998
  1894
              apply (simp add: abs if_distrib prod.delta_remove prod_constant field_simps power_diff split: if_split_asm)
lp15@67998
  1895
              done
lp15@67998
  1896
          qed
lp15@67998
  1897
          also have "\<dots> \<le> e/2 * measure lebesgue (cball ?x' (min d r))"
lp15@67998
  1898
          proof (rule mult_left_mono [OF measure_mono_fmeasurable])
lp15@67998
  1899
            have *: "norm (?x' - y) \<le> min d r"
lp15@67998
  1900
              if y: "\<And>i. \<bar>?x' $ i - y $ i\<bar> \<le> min d r / real CARD('m)" for y
lp15@67998
  1901
            proof -
lp15@67998
  1902
              have "norm (?x' - y) \<le> (\<Sum>i\<in>UNIV. \<bar>(?x' - y) $ i\<bar>)"
lp15@67998
  1903
                by (rule norm_le_l1_cart)
lp15@67998
  1904
              also have "\<dots> \<le> real CARD('m) * (min d r / real CARD('m))"
lp15@67998
  1905
                by (rule sum_bounded_above) (use y in auto)
lp15@67998
  1906
              finally show ?thesis
lp15@67998
  1907
                by simp
lp15@67998
  1908
            qed
lp15@67998
  1909
            show "cbox (?x' - ?v) (?x' + ?v) \<subseteq> cball ?x' (min d r)"
lp15@67998
  1910
              apply (clarsimp simp only: mem_box_cart dist_norm mem_cball intro!: *)
lp15@67998
  1911
              by (simp add: abs_diff_le_iff abs_minus_commute)
lp15@67998
  1912
          qed (use \<open>e > 0\<close> in auto)
lp15@67998
  1913
          also have "\<dots> < e * content (cball ?x' (min d r))"
lp15@67998
  1914
            using \<open>r > 0\<close> \<open>d > 0\<close> \<open>e > 0\<close> by auto
lp15@67998
  1915
          also have "\<dots> = e * content (ball x (min d r))"
lp15@67998
  1916
            using \<open>r > 0\<close> \<open>d > 0\<close> by (simp add: content_cball content_ball)
lp15@67998
  1917
          finally show "measure lebesgue ?W < e * content (ball x (min d r))" .
lp15@67998
  1918
      qed
lp15@67998
  1919
    qed
lp15@67998
  1920
    have *: "(\<And>x. (x \<notin> S) \<Longrightarrow> (x \<in> T \<longleftrightarrow> x \<in> U)) \<Longrightarrow> (T - U) \<union> (U - T) \<subseteq> S" for S T U :: "(real,'m) vec set"
lp15@67998
  1921
      by blast
lp15@67998
  1922
    have MN: "?M \<subseteq> {x \<in> S. \<exists>v\<noteq>0. ?\<Theta> x v}"
lp15@67998
  1923
    proof (rule *)
lp15@67998
  1924
      fix x
lp15@67998
  1925
      assume x: "x \<notin> {x \<in> S. \<exists>v\<noteq>0. ?\<Theta> x v}"
lp15@67998
  1926
      show "(x \<in> ?T) \<longleftrightarrow> (x \<in> {x \<in> S. matrix (f' x) $ m $ n \<le> b})"
lp15@67998
  1927
      proof (cases "x \<in> S")
lp15@67998
  1928
        case True
lp15@67998
  1929
        then have x: "\<not> ?\<Theta> x v" if "v \<noteq> 0" for v
lp15@67998
  1930
          using x that by force
lp15@67998
  1931
        show ?thesis
lp15@67998
  1932
        proof (rule iffI; clarsimp)
lp15@67998
  1933
          assume b: "\<forall>e>0. \<exists>d>0. \<exists>A. A $ m $ n < b \<and> (\<forall>i j. A $ i $ j \<in> \<rat>) \<and>
lp15@67998
  1934
                                    (\<forall>y\<in>S. norm (y - x) < d \<longrightarrow> norm (f y - f x - A *v (y - x)) \<le> e * norm (y - x))"
lp15@67998
  1935
                     (is "\<forall>e>0. \<exists>d>0. \<exists>A. ?\<Phi> e d A")
lp15@67998
  1936
          then have "\<forall>k. \<exists>d>0. \<exists>A. ?\<Phi> (1 / Suc k) d A"
lp15@67998
  1937
            by (metis (no_types, hide_lams) less_Suc_eq_0_disj of_nat_0_less_iff zero_less_divide_1_iff)
lp15@67998
  1938
          then obtain \<delta> A where \<delta>: "\<And>k. \<delta> k > 0"
lp15@67998
  1939
                           and Ab: "\<And>k. A k $ m $ n < b"
lp15@67998
  1940
                           and A: "\<And>k y. \<lbrakk>y \<in> S; norm (y - x) < \<delta> k\<rbrakk> \<Longrightarrow>
lp15@67998
  1941
                                          norm (f y - f x - A k *v (y - x)) \<le> 1/(Suc k) * norm (y - x)"
lp15@67998
  1942
            by metis
lp15@67998
  1943
          have "\<forall>i j. \<exists>a. (\<lambda>n. A n $ i $ j) \<longlonglongrightarrow> a"
lp15@67998
  1944
          proof (intro allI)
lp15@67998
  1945
            fix i j
lp15@67998
  1946
            have vax: "(A n *v axis j 1) $ i = A n $ i $ j" for n
lp15@67998
  1947
              by (metis cart_eq_inner_axis matrix_vector_mul_component)
lp15@67998
  1948
            let ?CA = "{x. Cauchy (\<lambda>n. (A n) *v x)}"
lp15@67998
  1949
            have "subspace ?CA"
lp15@67998
  1950
              unfolding subspace_def convergent_eq_Cauchy [symmetric]
lp15@67998
  1951
                by (force simp: algebra_simps intro: tendsto_intros)
lp15@67998
  1952
            then have CA_eq: "?CA = span ?CA"
lp15@67998
  1953
              by (metis span_eq)
lp15@67998
  1954
            also have "\<dots> = UNIV"
lp15@67998
  1955
            proof -
lp15@67998
  1956
              have "dim ?CA \<le> CARD('m)"
lp15@67998
  1957
                by (rule dim_subset_UNIV_cart)
lp15@67998
  1958
              moreover have "False" if less: "dim ?CA < CARD('m)"
lp15@67998
  1959
              proof -
lp15@67998
  1960
                obtain d where "d \<noteq> 0" and d: "\<And>y. y \<in> span ?CA \<Longrightarrow> orthogonal d y"
lp15@67998
  1961
                  using less by (force intro: orthogonal_to_subspace_exists [of ?CA])
lp15@67998
  1962
                with x [OF \<open>d \<noteq> 0\<close>] obtain \<xi> where "\<xi> > 0"
lp15@67998
  1963
                  and \<xi>: "\<And>e. e > 0 \<Longrightarrow> \<exists>y \<in> S - {x}. norm (x - y) < e \<and> \<xi> * norm (x - y) \<le> \<bar>d \<bullet> (y - x)\<bar>"
lp15@67998
  1964
                  by (fastforce simp: not_le Bex_def)
lp15@67998
  1965
                obtain \<gamma> z where \<gamma>Sx: "\<And>i. \<gamma> i \<in> S - {x}"
lp15@67998
  1966
                           and \<gamma>le:   "\<And>i. \<xi> * norm(\<gamma> i - x) \<le> \<bar>d \<bullet> (\<gamma> i - x)\<bar>"
lp15@67998
  1967
                           and \<gamma>x:    "\<gamma> \<longlonglongrightarrow> x"
lp15@67998
  1968
                           and z:     "(\<lambda>n. (\<gamma> n - x) /\<^sub>R norm (\<gamma> n - x)) \<longlonglongrightarrow> z"
lp15@67998
  1969
                proof -
lp15@67998
  1970
                  have "\<exists>\<gamma>. (\<forall>i. (\<gamma> i \<in> S - {x} \<and>
lp15@67998
  1971
                                  \<xi> * norm(\<gamma> i - x) \<le> \<bar>d \<bullet> (\<gamma> i - x)\<bar> \<and> norm(\<gamma> i - x) < 1/Suc i) \<and>
lp15@67998
  1972
                                 norm(\<gamma>(Suc i) - x) < norm(\<gamma> i - x))"
lp15@67998
  1973
                  proof (rule dependent_nat_choice)
lp15@67998
  1974
                    show "\<exists>y. y \<in> S - {x} \<and> \<xi> * norm (y - x) \<le> \<bar>d \<bullet> (y - x)\<bar> \<and> norm (y - x) < 1 / Suc 0"
lp15@67998
  1975
                      using \<xi> [of 1] by (auto simp: dist_norm norm_minus_commute)
lp15@67998
  1976
                  next
lp15@67998
  1977
                    fix y i
lp15@67998
  1978
                    assume "y \<in> S - {x} \<and> \<xi> * norm (y - x) \<le> \<bar>d \<bullet> (y - x)\<bar> \<and> norm (y - x) < 1/Suc i"
lp15@67998
  1979
                    then have "min (norm(y - x)) (1/((Suc i) + 1)) > 0"
lp15@67998
  1980
                      by auto
lp15@67998
  1981
                    then obtain y' where "y' \<in> S - {x}" and y': "norm (x - y') < min (norm (y - x)) (1/((Suc i) + 1))"
lp15@67998
  1982
                                         "\<xi> * norm (x - y') \<le> \<bar>d \<bullet> (y' - x)\<bar>"
lp15@67998
  1983
                      using \<xi> by metis
lp15@67998
  1984
                    with \<xi> show "\<exists>y'. (y' \<in> S - {x} \<and> \<xi> * norm (y' - x) \<le> \<bar>d \<bullet> (y' - x)\<bar> \<and>
lp15@67998
  1985
                              norm (y' - x) < 1/(Suc (Suc i))) \<and> norm (y' - x) < norm (y - x)"
lp15@67998
  1986
                      by (auto simp: dist_norm norm_minus_commute)
lp15@67998
  1987
                  qed
lp15@67998
  1988
                  then obtain \<gamma> where
lp15@67998
  1989
                        \<gamma>Sx: "\<And>i. \<gamma> i \<in> S - {x}"
lp15@67998
  1990
                        and \<gamma>le: "\<And>i. \<xi> * norm(\<gamma> i - x) \<le> \<bar>d \<bullet> (\<gamma> i - x)\<bar>"
lp15@67998
  1991
                        and \<gamma>conv: "\<And>i. norm(\<gamma> i - x) < 1/(Suc i)"
lp15@67998
  1992
                    by blast
lp15@67998
  1993
                  let ?f = "\<lambda>i. (\<gamma> i - x) /\<^sub>R norm (\<gamma> i - x)"
lp15@67998
  1994
                  have "?f i \<in> sphere 0 1" for i
lp15@67998
  1995
                    using \<gamma>Sx by auto
lp15@67998
  1996
                  then obtain l \<rho> where "l \<in> sphere 0 1" "strict_mono \<rho>" and l: "(?f \<circ> \<rho>) \<longlonglongrightarrow> l"
lp15@67998
  1997
                    using compact_sphere [of "0::(real,'m) vec" 1]  unfolding compact_def by meson
lp15@67998
  1998
                  show thesis
lp15@67998
  1999
                  proof
lp15@67998
  2000
                    show "(\<gamma> \<circ> \<rho>) i \<in> S - {x}" "\<xi> * norm ((\<gamma> \<circ> \<rho>) i - x) \<le> \<bar>d \<bullet> ((\<gamma> \<circ> \<rho>) i - x)\<bar>" for i
lp15@67998
  2001
                      using \<gamma>Sx \<gamma>le by auto
lp15@67998
  2002
                    have "\<gamma> \<longlonglongrightarrow> x"
lp15@67998
  2003
                    proof (clarsimp simp add: LIMSEQ_def dist_norm)
lp15@67998
  2004
                      fix r :: "real"
lp15@67998
  2005
                      assume "r > 0"
lp15@67998
  2006
                      with real_arch_invD obtain no where "no \<noteq> 0" "real no > 1/r"
lp15@67998
  2007
                        by (metis divide_less_0_1_iff not_less_iff_gr_or_eq of_nat_0_eq_iff reals_Archimedean2)
lp15@67998
  2008
                      with \<gamma>conv show "\<exists>no. \<forall>n\<ge>no. norm (\<gamma> n - x) < r"
lp15@67998
  2009
                        by (metis \<open>r > 0\<close> add.commute divide_inverse inverse_inverse_eq inverse_less_imp_less less_trans mult.left_neutral nat_le_real_less of_nat_Suc)
lp15@67998
  2010
                    qed
lp15@67998
  2011
                    with \<open>strict_mono \<rho>\<close> show "(\<gamma> \<circ> \<rho>) \<longlonglongrightarrow> x"
lp15@67998
  2012
                      by (metis LIMSEQ_subseq_LIMSEQ)
lp15@67998
  2013
                    show "(\<lambda>n. ((\<gamma> \<circ> \<rho>) n - x) /\<^sub>R norm ((\<gamma> \<circ> \<rho>) n - x)) \<longlonglongrightarrow> l"
lp15@67998
  2014
                      using l by (auto simp: o_def)
lp15@67998
  2015
                  qed
lp15@67998
  2016
                qed
lp15@67998
  2017
                have "isCont (\<lambda>x. (\<bar>d \<bullet> x\<bar> - \<xi>)) z"
lp15@67998
  2018
                  by (intro continuous_intros)
lp15@67998
  2019
                from isCont_tendsto_compose [OF this z]
lp15@67998
  2020
                have lim: "(\<lambda>y. \<bar>d \<bullet> ((\<gamma> y - x) /\<^sub>R norm (\<gamma> y - x))\<bar> - \<xi>) \<longlonglongrightarrow> \<bar>d \<bullet> z\<bar> - \<xi>"
lp15@67998
  2021
                  by auto
lp15@67998
  2022
                moreover have "\<forall>\<^sub>F i in sequentially. 0 \<le> \<bar>d \<bullet> ((\<gamma> i - x) /\<^sub>R norm (\<gamma> i - x))\<bar> - \<xi>"
lp15@67998
  2023
                proof (rule eventuallyI)
lp15@67998
  2024
                  fix n
lp15@67998
  2025
                  show "0 \<le> \<bar>d \<bullet> ((\<gamma> n - x) /\<^sub>R norm (\<gamma> n - x))\<bar> - \<xi>"
lp15@67998
  2026
                  using \<gamma>le [of n] \<gamma>Sx by (auto simp: abs_mult divide_simps)
lp15@67998
  2027
                qed
lp15@67998
  2028
                ultimately have "\<xi> \<le> \<bar>d \<bullet> z\<bar>"
lp15@67998
  2029
                  using tendsto_lowerbound [where a=0] by fastforce
lp15@67998
  2030
                have "Cauchy (\<lambda>n. (A n) *v z)"
lp15@67998
  2031
                proof (clarsimp simp add: Cauchy_def)
lp15@67998
  2032
                  fix \<epsilon> :: "real"
lp15@67998
  2033
                  assume "0 < \<epsilon>"
lp15@67998
  2034
                  then obtain N::nat where "N > 0" and N: "\<epsilon>/2 > 1/N"
lp15@67998
  2035
                    by (metis half_gt_zero inverse_eq_divide neq0_conv real_arch_inverse)
lp15@67998
  2036
                  show "\<exists>M. \<forall>m\<ge>M. \<forall>n\<ge>M. dist (A m *v z) (A n *v z) < \<epsilon>"
lp15@67998
  2037
                  proof (intro exI allI impI)
lp15@67998
  2038
                    fix i j
lp15@67998
  2039
                    assume ij: "N \<le> i" "N \<le> j"
lp15@67998
  2040
                    let ?V = "\<lambda>i k. A i *v ((\<gamma> k - x) /\<^sub>R norm (\<gamma> k - x))"
lp15@67998
  2041
                    have "\<forall>\<^sub>F k in sequentially. dist (\<gamma> k) x < min (\<delta> i) (\<delta> j)"
lp15@67998
  2042
                      using \<gamma>x [unfolded tendsto_iff] by (meson min_less_iff_conj \<delta>)
lp15@67998
  2043
                    then have even: "\<forall>\<^sub>F k in sequentially. norm (?V i k - ?V j k) - 2 / N \<le> 0"
lp15@67998
  2044
                    proof (rule eventually_mono, clarsimp)
lp15@67998
  2045
                      fix p
lp15@67998
  2046
                      assume p: "dist (\<gamma> p) x < \<delta> i" "dist (\<gamma> p) x < \<delta> j"
lp15@67998
  2047
                      let ?C = "\<lambda>k. f (\<gamma> p) - f x - A k *v (\<gamma> p - x)"
lp15@67998
  2048
                      have "norm ((A i - A j) *v (\<gamma> p - x)) = norm (?C j - ?C i)"
lp15@67998
  2049
                        by (simp add: algebra_simps)
lp15@67998
  2050
                      also have "\<dots> \<le> norm (?C j) + norm (?C i)"
lp15@67998
  2051
                        using norm_triangle_ineq4 by blast
lp15@67998
  2052
                      also have "\<dots> \<le> 1/(Suc j) * norm (\<gamma> p - x) + 1/(Suc i) * norm (\<gamma> p - x)"
lp15@67998
  2053
                        by (metis A Diff_iff \<gamma>Sx dist_norm p add_mono)
lp15@67998
  2054
                      also have "\<dots> \<le> 1/N * norm (\<gamma> p - x) + 1/N * norm (\<gamma> p - x)"
lp15@67998
  2055
                        apply (intro add_mono mult_right_mono)
lp15@67998
  2056
                        using ij \<open>N > 0\<close> by (auto simp: field_simps)
lp15@67998
  2057
                      also have "\<dots> = 2 / N * norm (\<gamma> p - x)"
lp15@67998
  2058
                        by simp
lp15@67998
  2059
                      finally have no_le: "norm ((A i - A j) *v (\<gamma> p - x)) \<le> 2 / N * norm (\<gamma> p - x)" .
lp15@67998
  2060
                      have "norm (?V i p - ?V j p) =
lp15@67998
  2061
                            norm ((A i - A j) *v ((\<gamma> p - x) /\<^sub>R norm (\<gamma> p - x)))"
lp15@67998
  2062
                        by (simp add: algebra_simps)
lp15@67998
  2063
                      also have "\<dots> = norm ((A i - A j) *v (\<gamma> p - x)) / norm (\<gamma> p - x)"
lp15@67998
  2064
                        by (simp add: divide_inverse matrix_vector_mult_scaleR)
lp15@67998
  2065
                      also have "\<dots> \<le> 2 / N"
lp15@67998
  2066
                        using no_le by (auto simp: divide_simps)
lp15@67998
  2067
                      finally show "norm (?V i p - ?V j p) \<le> 2 / N" .
lp15@67998
  2068
                    qed
lp15@67998
  2069
                    have "isCont (\<lambda>w. (norm(A i *v w - A j *v w) - 2 / N)) z"
lp15@67998
  2070
                      by (intro continuous_intros)
lp15@67998
  2071
                    from isCont_tendsto_compose [OF this z]
lp15@67998
  2072
                    have lim: "(\<lambda>w. norm (A i *v ((\<gamma> w - x) /\<^sub>R norm (\<gamma> w - x)) -
lp15@67998
  2073
                                    A j *v ((\<gamma> w - x) /\<^sub>R norm (\<gamma> w - x))) - 2 / N)
lp15@67998
  2074
                               \<longlonglongrightarrow> norm (A i *v z - A j *v z) - 2 / N"
lp15@67998
  2075
                      by auto
lp15@67998
  2076
                    have "dist (A i *v z) (A j *v z) \<le> 2 / N"
lp15@67998
  2077
                      using tendsto_upperbound [OF lim even] by (auto simp: dist_norm)
lp15@67998
  2078
                    with N show "dist (A i *v z) (A j *v z) < \<epsilon>"
lp15@67998
  2079
                      by linarith
lp15@67998
  2080
                  qed
lp15@67998
  2081
                qed
lp15@67998
  2082
                then have "d \<bullet> z = 0"
lp15@67998
  2083
                  using CA_eq d orthogonal_def by auto
lp15@67998
  2084
                then show False
lp15@67998
  2085
                  using \<open>0 < \<xi>\<close> \<open>\<xi> \<le> \<bar>d \<bullet> z\<bar>\<close> by auto
lp15@67998
  2086
              qed
lp15@67998
  2087
              ultimately show ?thesis
lp15@67998
  2088
                using dim_eq_full by fastforce
lp15@67998
  2089
            qed
lp15@67998
  2090
            finally have "?CA = UNIV" .
lp15@67998
  2091
            then have "Cauchy (\<lambda>n. (A n) *v axis j 1)"
lp15@67998
  2092
              by auto
lp15@67998
  2093
            then obtain L where "(\<lambda>n. A n *v axis j 1) \<longlonglongrightarrow> L"
lp15@67998
  2094
              by (auto simp: Cauchy_convergent_iff convergent_def)
lp15@67998
  2095
            then have "(\<lambda>x. (A x *v axis j 1) $ i) \<longlonglongrightarrow> L $ i"
lp15@67998
  2096
              by (rule tendsto_vec_nth)
lp15@67998
  2097
            then show "\<exists>a. (\<lambda>n. A n $ i $ j) \<longlonglongrightarrow> a"
lp15@67998
  2098
              by (force simp: vax)
lp15@67998
  2099
          qed
lp15@67998
  2100
          then obtain B where B: "\<And>i j. (\<lambda>n. A n $ i $ j) \<longlonglongrightarrow> B $ i $ j"
lp15@67998
  2101
            by (auto simp: lambda_skolem)
lp15@67998
  2102
          have lin_df: "linear (f' x)"
lp15@67998
  2103
               and lim_df: "((\<lambda>y. (1 / norm (y - x)) *\<^sub>R (f y - (f x + f' x (y - x)))) \<longlongrightarrow> 0) (at x within S)"
lp15@67998
  2104
            using \<open>x \<in> S\<close> assms by (auto simp: has_derivative_within linear_linear)
lp15@67998
  2105
          moreover have "(matrix (f' x) - B) *v w = 0" for w
lp15@67998
  2106
          proof (rule lemma_partial_derivatives [of "( *v) (matrix (f' x) - B)"])
lp15@67998
  2107
            show "linear (( *v) (matrix (f' x) - B))"
lp15@67998
  2108
              by (rule matrix_vector_mul_linear)
lp15@67998
  2109
            have "((\<lambda>y. ((f x + f' x (y - x)) - f y) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within S)"
lp15@67998
  2110
              using tendsto_minus [OF lim_df] by (simp add: algebra_simps divide_simps)
lp15@67998
  2111
            then show "((\<lambda>y. (matrix (f' x) - B) *v (y - x) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0) (at x within S)"
lp15@67998
  2112
            proof (rule Lim_transform)
lp15@67998
  2113
              have "((\<lambda>y. ((f y + B *v x - (f x + B *v y)) /\<^sub>R norm (y - x))) \<longlongrightarrow> 0) (at x within S)"
lp15@67998
  2114
              proof (clarsimp simp add: Lim_within dist_norm)
lp15@67998
  2115
                fix e :: "real"
lp15@67998
  2116
                assume "e > 0"
lp15@67998
  2117
                then obtain q::nat where "q \<noteq> 0" and qe2: "1/q < e/2"
lp15@67998
  2118
                  by (metis divide_pos_pos inverse_eq_divide real_arch_inverse zero_less_numeral)
lp15@67998
  2119
                let ?g = "\<lambda>p. sum  (\<lambda>i. sum (\<lambda>j. abs((A p - B)$i$j)) UNIV) UNIV"
lp15@67998
  2120
                have "(\<lambda>k. onorm (\<lambda>y. (A k - B) *v y)) \<longlonglongrightarrow> 0"
lp15@67998
  2121
                proof (rule Lim_null_comparison)
lp15@67998
  2122
                  show "\<forall>\<^sub>F k in sequentially. norm (onorm (\<lambda>y. (A k - B) *v y)) \<le> ?g k"
lp15@67998
  2123
                  proof (rule eventually_sequentiallyI)
lp15@67998
  2124
                    fix k :: "nat"
lp15@67998
  2125
                    assume "0 \<le> k"
lp15@67998
  2126
                    have "0 \<le> onorm (( *v) (A k - B))"
lp15@67998
  2127
                      by (simp add: linear_linear onorm_pos_le matrix_vector_mul_linear)
lp15@67998
  2128
                    then show "norm (onorm (( *v) (A k - B))) \<le> (\<Sum>i\<in>UNIV. \<Sum>j\<in>UNIV. \<bar>(A k - B) $ i $ j\<bar>)"
lp15@67998
  2129
                      by (simp add: onorm_le_matrix_component_sum del: vector_minus_component)
lp15@67998
  2130
                  qed
lp15@67998
  2131
                next
lp15@67998
  2132
                  show "?g \<longlonglongrightarrow> 0"
lp15@67998
  2133
                    using B Lim_null tendsto_rabs_zero_iff by (fastforce intro!: tendsto_null_sum)
lp15@67998
  2134
                qed
lp15@67998
  2135
                with \<open>e > 0\<close> obtain p where "\<And>n. n \<ge> p \<Longrightarrow> \<bar>onorm (( *v) (A n - B))\<bar> < e/2"
lp15@67998
  2136
                  unfolding lim_sequentially by (metis diff_zero dist_real_def divide_pos_pos zero_less_numeral)
lp15@67998
  2137
                then have pqe2: "\<bar>onorm (( *v) (A (p + q) - B))\<bar> < e/2" (*17 [`abs (onorm (\y. A (p + q) ** y - B ** y)) < e / &2`]*)
lp15@67998
  2138
                  using le_add1 by blast
lp15@67998
  2139
                show "\<exists>d>0. \<forall>y\<in>S. y \<noteq> x \<and> norm (y - x) < d \<longrightarrow>
lp15@67998
  2140
                           inverse (norm (y - x)) * norm (f y + B *v x - (f x + B *v y)) < e"
lp15@67998
  2141
                proof (intro exI, safe)
lp15@67998
  2142
                  show "0 < \<delta>(p + q)"
lp15@67998
  2143
                    by (simp add: \<delta>)
lp15@67998
  2144
                next
lp15@67998
  2145
                  fix y
lp15@67998
  2146
                  assume y: "y \<in> S" "norm (y - x) < \<delta>(p + q)" and "y \<noteq> x"
lp15@67998
  2147
                  have *: "\<lbrakk>norm(b - c) < e - d; norm(y - x - b) \<le> d\<rbrakk> \<Longrightarrow> norm(y - x - c) < e"
lp15@67998
  2148
                    for b c d e x and y:: "real^'n"
lp15@67998
  2149
                    using norm_triangle_ineq2 [of "y - x - c" "y - x - b"] by simp
lp15@67998
  2150
                  have "norm (f y - f x - B *v (y - x)) < e * norm (y - x)"
lp15@67998
  2151
                  proof (rule *)
lp15@67998
  2152
                    show "norm (f y - f x - A (p + q) *v (y - x)) \<le> norm (y - x) / (Suc (p + q))"
lp15@67998
  2153
                      using A [OF y] by simp
lp15@67998
  2154
                    have "norm (A (p + q) *v (y - x) - B *v (y - x)) \<le> onorm(\<lambda>x. (A(p + q) - B) *v x) * norm(y - x)"
lp15@67998
  2155
                      by (metis linear_linear matrix_vector_mul_linear matrix_vector_mult_diff_rdistrib onorm)
lp15@67998
  2156
                    also have "\<dots> < (e/2) * norm (y - x)"
lp15@67998
  2157
                      using \<open>y \<noteq> x\<close> pqe2 by auto
lp15@67998
  2158
                    also have "\<dots> \<le> (e - 1 / (Suc (p + q))) * norm (y - x)"
lp15@67998
  2159
                    proof (rule mult_right_mono)
lp15@67998
  2160
                      have "1 / Suc (p + q) \<le> 1 / q"
lp15@67998
  2161
                        using \<open>q \<noteq> 0\<close> by (auto simp: divide_simps)
lp15@67998
  2162
                      also have "\<dots> < e/2"
lp15@67998
  2163
                        using qe2 by auto
lp15@67998
  2164
                      finally show "e / 2 \<le> e - 1 / real (Suc (p + q))"
lp15@67998
  2165
                        by linarith
lp15@67998
  2166
                    qed auto
lp15@67998
  2167
                    finally show "norm (A (p + q) *v (y - x) - B *v (y - x)) < e * norm (y - x) - norm (y - x) / real (Suc (p + q))"
lp15@67998
  2168
                      by (simp add: algebra_simps)
lp15@67998
  2169
                  qed
lp15@67998
  2170
                  then show "inverse (norm (y - x)) * norm (f y + B *v x - (f x + B *v y)) < e"
lp15@67998
  2171
                    using \<open>y \<noteq> x\<close> by (simp add: divide_simps algebra_simps)
lp15@67998
  2172
                qed
lp15@67998
  2173
              qed
lp15@67998
  2174
              then show "((\<lambda>y. (matrix (f' x) - B) *v (y - x) /\<^sub>R
lp15@67998
  2175
                           norm (y - x) - (f x + f' x (y - x) - f y) /\<^sub>R norm (y - x)) \<longlongrightarrow> 0)
lp15@67998
  2176
                          (at x within S)"
lp15@67998
  2177
                by (simp add: algebra_simps lin_df linear_diff matrix_vector_mul_linear)
lp15@67998
  2178
            qed
lp15@67998
  2179
          qed (use x in \<open>simp; auto simp: not_less\<close>)
lp15@67998
  2180
          ultimately have "f' x = ( *v) B"
lp15@67998
  2181
            by (force simp: algebra_simps)
lp15@67998
  2182
          show "matrix (f' x) $ m $ n \<le> b"
lp15@67998
  2183
          proof (rule tendsto_upperbound [of "\<lambda>i. (A i $ m $ n)" _ sequentially])
lp15@67998
  2184
            show "(\<lambda>i. A i $ m $ n) \<longlonglongrightarrow> matrix (f' x) $ m $ n"
lp15@67998
  2185
              by (simp add: B \<open>f' x = ( *v) B\<close>)
lp15@67998
  2186
            show "\<forall>\<^sub>F i in sequentially. A i $ m $ n \<le> b"
lp15@67998
  2187
              by (simp add: Ab less_eq_real_def)
lp15@67998
  2188
          qed auto
lp15@67998
  2189
        next
lp15@67998
  2190
          fix e :: "real"
lp15@67998
  2191
          assume "x \<in> S" and b: "matrix (f' x) $ m $ n \<le> b" and "e > 0"
lp15@67998
  2192
          then obtain d where "d>0"
lp15@67998
  2193
            and d: "\<And>y. y\<in>S \<Longrightarrow> 0 < dist y x \<and> dist y x < d \<longrightarrow> norm (f y - f x - f' x (y - x)) / (norm (y - x))
lp15@67998
  2194
                  < e/2"
lp15@67998
  2195
            using f [OF \<open>x \<in> S\<close>] unfolding Deriv.has_derivative_at_within Lim_within
lp15@67998
  2196
            by (auto simp: field_simps dest: spec [of _ "e/2"])
lp15@67998
  2197
          let ?A = "matrix(f' x) - (\<chi> i j. if i = m \<and> j = n then e / 4 else 0)"
lp15@67998
  2198
          obtain B where BRats: "\<And>i j. B$i$j \<in> \<rat>" and Bo_e6: "onorm(( *v) (?A - B)) < e/6"
lp15@67998
  2199
            using matrix_rational_approximation \<open>e > 0\<close>
lp15@67998
  2200
            by (metis zero_less_divide_iff zero_less_numeral)
lp15@67998
  2201
          show "\<exists>d>0. \<exists>A. A $ m $ n < b \<and> (\<forall>i j. A $ i $ j \<in> \<rat>) \<and>
lp15@67998
  2202
                (\<forall>y\<in>S. norm (y - x) < d \<longrightarrow> norm (f y - f x - A *v (y - x)) \<le> e * norm (y - x))"
lp15@67998
  2203
          proof (intro exI conjI ballI allI impI)
lp15@67998
  2204
            show "d>0"
lp15@67998
  2205
              by (rule \<open>d>0\<close>)
lp15@67998
  2206
            show "B $ m $ n < b"
lp15@67998
  2207
            proof -
lp15@67998
  2208
              have "\<bar>matrix (( *v) (?A - B)) $ m $ n\<bar> \<le> onorm (( *v) (?A - B))"
lp15@67998
  2209
                using component_le_onorm [OF matrix_vector_mul_linear, of _ m n] by metis
lp15@67998
  2210
              then show ?thesis
lp15@67998
  2211
                using b Bo_e6 by simp
lp15@67998
  2212
            qed
lp15@67998
  2213
            show "B $ i $ j \<in> \<rat>" for i j
lp15@67998
  2214
              using BRats by auto
lp15@67998
  2215
            show "norm (f y - f x - B *v (y - x)) \<le> e * norm (y - x)"
lp15@67998
  2216
              if "y \<in> S" and y: "norm (y - x) < d" for y
lp15@67998
  2217
            proof (cases "y = x")
lp15@67998
  2218
              case True then show ?thesis
lp15@67998
  2219
                by simp
lp15@67998
  2220
            next
lp15@67998
  2221
              case False
lp15@67998
  2222
              have *: "norm(d' - d) \<le> e/2 \<Longrightarrow> norm(y - (x + d')) < e/2 \<Longrightarrow> norm(y - x - d) \<le> e" for d d' e and x y::"real^'n"
lp15@67998
  2223
                using norm_triangle_le [of "d' - d" "y - (x + d')"] by simp
lp15@67998
  2224
              show ?thesis
lp15@67998
  2225
              proof (rule *)
lp15@67998
  2226
                have split246: "\<lbrakk>norm y \<le> e / 6; norm(x - y) \<le> e / 4\<rbrakk> \<Longrightarrow> norm x \<le> e/2" if "e > 0" for e and x y :: "real^'n"
lp15@67998
  2227
                  using norm_triangle_le [of y "x-y" "e/2"] \<open>e > 0\<close> by simp
lp15@67998
  2228
                have "linear (f' x)"
lp15@67998
  2229
                  using True f has_derivative_linear by blast
lp15@67998
  2230
                then have "norm (f' x (y - x) - B *v (y - x)) = norm ((matrix (f' x) - B) *v (y - x))"
lp15@67998
  2231
                  by (metis matrix_vector_mul matrix_vector_mult_diff_rdistrib)
lp15@67998
  2232
                also have "\<dots> \<le> (e * norm (y - x)) / 2"
lp15@67998
  2233
                proof (rule split246)
lp15@67998
  2234
                  have "norm ((?A - B) *v (y - x)) / norm (y - x) \<le> onorm(\<lambda>x. (?A - B) *v x)"
lp15@67998
  2235
                    by (simp add: le_onorm linear_linear matrix_vector_mul_linear)
lp15@67998
  2236
                  also have  "\<dots> < e/6"
lp15@67998
  2237
                    by (rule Bo_e6)
lp15@67998
  2238
                  finally have "norm ((?A - B) *v (y - x)) / norm (y - x) < e / 6" .
lp15@67998
  2239
                  then show "norm ((?A - B) *v (y - x)) \<le> e * norm (y - x) / 6"
lp15@67998
  2240
                    by (simp add: divide_simps False)
lp15@67998
  2241
                  have "norm ((matrix (f' x) - B) *v (y - x) - ((?A - B) *v (y - x))) = norm ((\<chi> i j. if i = m \<and> j = n then e / 4 else 0) *v (y - x))"
lp15@67998
  2242
                    by (simp add: algebra_simps)
lp15@67998
  2243
                  also have "\<dots> = norm((e/4) *\<^sub>R (y - x)$n *\<^sub>R axis m (1::real))"
lp15@67998
  2244
                  proof -
lp15@67998
  2245
                    have "(\<Sum>j\<in>UNIV. (if i = m \<and> j = n then e / 4 else 0) * (y $ j - x $ j)) * 4 = e * (y $ n - x $ n) * axis m 1 $ i" for i
lp15@67998
  2246
                    proof (cases "i=m")
lp15@67998
  2247
                      case True then show ?thesis
lp15@67998
  2248
                        by (auto simp: if_distrib [of "\<lambda>z. z * _"] cong: if_cong)
lp15@67998
  2249
                    next
lp15@67998
  2250
                      case False then show ?thesis
lp15@67998
  2251
                        by (simp add: axis_def)
lp15@67998
  2252
                    qed
lp15@67998
  2253
                    then have "(\<chi> i j. if i = m \<and> j = n then e / 4 else 0) *v (y - x) = (e/4) *\<^sub>R (y - x)$n *\<^sub>R axis m (1::real)"
lp15@67998
  2254
                      by (auto simp: vec_eq_iff matrix_vector_mult_def)
lp15@67998
  2255
                    then show ?thesis
lp15@67998
  2256
                      by metis
lp15@67998
  2257
                  qed
lp15@67998
  2258
                  also have "\<dots> \<le> e * norm (y - x) / 4"
lp15@67998
  2259
                    using \<open>e > 0\<close> apply (simp add: norm_mult abs_mult)
lp15@67998
  2260
                    by (metis component_le_norm_cart vector_minus_component)
lp15@67998
  2261
                  finally show "norm ((matrix (f' x) - B) *v (y - x) - ((?A - B) *v (y - x))) \<le> e * norm (y - x) / 4" .
lp15@67998
  2262
                  show "0 < e * norm (y - x)"
lp15@67998
  2263
                    by (simp add: False \<open>e > 0\<close>)
lp15@67998
  2264
                qed
lp15@67998
  2265
                finally show "norm (f' x (y - x) - B *v (y - x)) \<le> (e * norm (y - x)) / 2" .
lp15@67998
  2266
                show "norm (f y - (f x + f' x (y - x))) < (e * norm (y - x)) / 2"
lp15@67998
  2267
                  using False d [OF \<open>y \<in> S\<close>] y by (simp add: dist_norm field_simps)
lp15@67998
  2268
              qed
lp15@67998
  2269
            qed
lp15@67998
  2270
          qed
lp15@67998
  2271
        qed
lp15@67998
  2272
      qed auto
lp15@67998
  2273
    qed
lp15@67998
  2274
    show "negligible ?M"
lp15@67998
  2275
      using negligible_subset [OF nN MN] .
lp15@67998
  2276
  qed
lp15@67998
  2277
  then show ?thesis
lp15@67998
  2278
    by (simp add: borel_measurable_vimage_halfspace_component_le sets_restrict_space_iff assms)
lp15@67998
  2279
qed
lp15@67998
  2280
lp15@67998
  2281
lp15@67998
  2282
theorem borel_measurable_det_Jacobian:
lp15@67998
  2283
 fixes f :: "real^'n::{finite,wellorder} \<Rightarrow> real^'n::_"
lp15@67998
  2284
  assumes S: "S \<in> sets lebesgue" and f: "\<And>x. x \<in> S \<Longrightarrow> (f has_derivative f' x) (at x within S)"
lp15@67998
  2285
  shows "(\<lambda>x. det(matrix(f' x))) \<in> borel_measurable (lebesgue_on S)"
lp15@67998
  2286
  unfolding det_def
lp15@67998
  2287
  by (intro measurable) (auto intro: f borel_measurable_partial_derivatives [OF S])
lp15@67998
  2288
lp15@68001
  2289
text\<open>The localisation wrt S uses the same argument for many similar results.\<close>
lp15@68001
  2290
(*See HOL Light's MEASURABLE_ON_LEBESGUE_MEASURABLE_PREIMAGE_BOREL, etc.*)
lp15@67998
  2291
lemma borel_measurable_lebesgue_on_preimage_borel:
lp15@67998
  2292
  fixes f :: "'a::euclidean_space \<Rightarrow> 'b::euclidean_space"
lp15@67998
  2293
  assumes "S \<in> sets lebesgue"
lp15@67998
  2294
  shows "f \<in> borel_measurable (lebesgue_on S) \<longleftrightarrow>
lp15@67998
  2295
         (\<forall>T. T \<in> sets borel \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets lebesgue)"
lp15@67998
  2296
proof -
lp15@67998
  2297
  have "{x. (if x \<in> S then f x else 0) \<in> T} \<in> sets lebesgue \<longleftrightarrow> {x \<in> S. f x \<in> T} \<in> sets lebesgue"
lp15@67998
  2298
         if "T \<in> sets borel" for T
lp15@67998
  2299
    proof (cases "0 \<in> T")
lp15@67998
  2300
      case True
lp15@67998
  2301
      then have "{x \<in> S. f x \<in> T} = {x. (if x \<in> S then f x else 0) \<in> T} \<inter> S"
lp15@67998
  2302
                "{x. (if x \<in> S then f x else 0) \<in> T} = {x \<in> S. f x \<in> T} \<union> -S"
lp15@67998
  2303
        by auto
lp15@67998
  2304
      then show ?thesis
lp15@67998
  2305
        by (metis (no_types, lifting) Compl_in_sets_lebesgue assms sets.Int sets.Un)
lp15@67998
  2306
    next
lp15@67998
  2307
      case False
lp15@67998
  2308
      then have "{x. (if x \<in> S then f x else 0) \<in> T} = {x \<in> S. f x \<in> T}"
lp15@67998
  2309
        by auto
lp15@67998
  2310
      then show ?thesis
lp15@67998
  2311
        by auto
lp15@67998
  2312
    qed
lp15@67998
  2313
    then show ?thesis
lp15@67998
  2314
      unfolding borel_measurable_lebesgue_preimage_borel borel_measurable_UNIV [OF assms, symmetric]
lp15@67998
  2315
      by blast
lp15@67998
  2316
qed
lp15@67998
  2317
lp15@67998
  2318
lemma sets_lebesgue_almost_borel:
lp15@67998
  2319
  assumes "S \<in> sets lebesgue"
lp15@67998
  2320
  obtains B N where "B \<in> sets borel" "negligible N" "B \<union> N = S"
lp15@67998
  2321
proof -
lp15@67998
  2322
  obtain T N N' where "S = T \<union> N" "N \<subseteq> N'" "N' \<in> null_sets lborel" "T \<in> sets borel"
lp15@67998
  2323
    using sets_completionE [OF assms] by auto
lp15@67998
  2324
  then show thesis
lp15@67998
  2325
    by (metis negligible_iff_null_sets negligible_subset null_sets_completionI that)
lp15@67998
  2326
qed
lp15@67998
  2327
lp15@67998
  2328
lemma double_lebesgue_sets:
lp15@67998
  2329
 assumes S: "S \<in> sets lebesgue" and T: "T \<in> sets lebesgue" and fim: "f ` S \<subseteq> T"
lp15@67998
  2330
 shows "(\<forall>U. U \<in> sets lebesgue \<and> U \<subseteq> T \<longrightarrow> {x \<in> S. f x \<in> U} \<in> sets lebesgue) \<longleftrightarrow>
lp15@67998
  2331
          f \<in> borel_measurable (lebesgue_on S) \<and>
lp15@67998
  2332
          (\<forall>U. negligible U \<and> U \<subseteq> T \<longrightarrow> {x \<in> S. f x \<in> U} \<in> sets lebesgue)"
lp15@67998
  2333
         (is "?lhs \<longleftrightarrow> _ \<and> ?rhs")
lp15@67998
  2334
  unfolding borel_measurable_lebesgue_on_preimage_borel [OF S]
lp15@67998
  2335
proof (intro iffI allI conjI impI, safe)
lp15@67998
  2336
  fix V :: "'b set"
lp15@67998
  2337
  assume *: "\<forall>U. U \<in> sets lebesgue \<and> U \<subseteq> T \<longrightarrow> {x \<in> S. f x \<in> U} \<in> sets lebesgue"
lp15@67998
  2338
    and "V \<in> sets borel"
lp15@67998
  2339
  then have V: "V \<in> sets lebesgue"
lp15@67998
  2340
    by simp
lp15@67998
  2341
  have "{x \<in> S. f x \<in> V} = {x \<in> S. f x \<in> T \<inter> V}"
lp15@67998
  2342
    using fim by blast
lp15@67998
  2343
  also have "{x \<in> S. f x \<in> T \<inter> V} \<in> sets lebesgue"
lp15@67998
  2344
    using T V * le_inf_iff by blast
lp15@67998
  2345
  finally show "{x \<in> S. f x \<in> V} \<in> sets lebesgue" .
lp15@67998
  2346
next
lp15@67998
  2347
  fix U :: "'b set"
lp15@67998
  2348
  assume "\<forall>U. U \<in> sets lebesgue \<and> U \<subseteq> T \<longrightarrow> {x \<in> S. f x \<in> U} \<in> sets lebesgue"
lp15@67998
  2349
         "negligible U" "U \<subseteq> T"
lp15@67998
  2350
  then show "{x \<in> S. f x \<in> U} \<in> sets lebesgue"
lp15@67998
  2351
    using negligible_imp_sets by blast
lp15@67998
  2352
next
lp15@67998
  2353
  fix U :: "'b set"
lp15@67998
  2354
  assume 1 [rule_format]: "(\<forall>T. T \<in> sets borel \<longrightarrow> {x \<in> S. f x \<in> T} \<in> sets lebesgue)"
lp15@67998
  2355
     and 2 [rule_format]: "\<forall>U. negligible U \<and> U \<subseteq> T \<longrightarrow> {x \<in> S. f x \<in> U} \<in> sets lebesgue"
lp15@67998
  2356
     and "U \<in> sets lebesgue" "U \<subseteq> T"
lp15@67998
  2357
  then obtain C N where C: "C \<in> sets borel \<and> negligible N \<and> C \<union> N = U"
lp15@67998
  2358
    using sets_lebesgue_almost_borel
lp15@67998
  2359
    by metis
lp15@67998
  2360
  then have "{x \<in> S. f x \<in> C} \<in> sets lebesgue"
lp15@67998
  2361
    by (blast intro: 1)
lp15@67998
  2362
  moreover have "{x \<in> S. f x \<in> N} \<in> sets lebesgue"
lp15@67998
  2363
    using C \<open>U \<subseteq> T\<close> by (blast intro: 2)
lp15@67998
  2364
  moreover have "{x \<in> S. f x \<in> C \<union> N} = {x \<in> S. f x \<in> C} \<union> {x \<in> S. f x \<in> N}"
lp15@67998
  2365
    by auto
lp15@67998
  2366
  ultimately show "{x \<in> S. f x \<in> U} \<in> sets lebesgue"
lp15@67998
  2367
    using C by auto
lp15@67998
  2368
qed
lp15@67998
  2369
lp15@67998
  2370
lp15@67998
  2371
subsection\<open>Simplest case of Sard's theorem (we don't need continuity of derivative)\<close>
lp15@67998
  2372
lp15@67998
  2373
lemma Sard_lemma00:
lp15@67998
  2374
  fixes P :: "'b::euclidean_space set"
lp15@67998
  2375
  assumes "a \<ge> 0" and a: "a *\<^sub>R i \<noteq> 0" and i: "i \<in> Basis"
lp15@67998
  2376
    and P: "P \<subseteq> {x. a *\<^sub>R i \<bullet> x = 0}"
lp15@67998
  2377
    and "0 \<le> m" "0 \<le> e"
lp15@67998
  2378
 obtains S where "S \<in> lmeasurable"
lp15@67998
  2379
            and "{z. norm z \<le> m \<and> (\<exists>t \<in> P. norm(z - t) \<le> e)} \<subseteq> S"
lp15@67998
  2380
            and "measure lebesgue S \<le> (2 * e) * (2 * m) ^ (DIM('b) - 1)"
lp15@67998
  2381
proof -
lp15@67998
  2382
  have "a > 0"
lp15@67998
  2383
    using assms by simp
lp15@67998
  2384
  let ?v = "(\<Sum>j\<in>Basis. (if j = i then e else m) *\<^sub>R j)"
lp15@67998
  2385
  show thesis
lp15@67998
  2386
  proof
lp15@67998
  2387
    have "- e \<le> x \<bullet> i" "x \<bullet> i \<le> e"
lp15@67998
  2388
      if "t \<in> P" "norm (x - t) \<le> e" for x t
lp15@67998
  2389
      using \<open>a > 0\<close> that Basis_le_norm [of i "x-t"] P i
lp15@67998
  2390
      by (auto simp: inner_commute algebra_simps)
lp15@67998
  2391
    moreover have "- m \<le> x \<bullet> j" "x \<bullet> j \<le> m"
lp15@67998
  2392
      if "norm x \<le> m" "t \<in> P" "norm (x - t) \<le> e" "j \<in> Basis" and "j \<noteq> i"
lp15@67998
  2393
      for x t j
lp15@67998
  2394
      using that Basis_le_norm [of j x] by auto
lp15@67998
  2395
    ultimately
lp15@67998
  2396
    show "{z. norm z \<le> m \<and> (\<exists>t\<in>P. norm (z - t) \<le> e)} \<subseteq> cbox (-?v) ?v"
lp15@67998
  2397
      by (auto simp: mem_box)
lp15@67998
  2398
    have *: "\<forall>k\<in>Basis. - ?v \<bullet> k \<le> ?v \<bullet> k"
lp15@67998
  2399
      using \<open>0 \<le> m\<close> \<open>0 \<le> e\<close> by (auto simp: inner_Basis)
lp15@67998
  2400
    have 2: "2 ^ DIM('b) = 2 * 2 ^ (DIM('b) - Suc 0)"
lp15@67998
  2401
      by (metis DIM_positive Suc_pred power_Suc)
lp15@67998
  2402
    show "measure lebesgue (cbox (-?v) ?v) \<le> 2 * e * (2 * m) ^ (DIM('b) - 1)"
lp15@67998
  2403
      using \<open>i \<in> Basis\<close>
lp15@67998
  2404
      by (simp add: content_cbox [OF *] prod.distrib prod.If_cases Diff_eq [symmetric] 2)
lp15@67998
  2405
  qed blast
lp15@67998
  2406
qed
lp15@67998
  2407
lp15@68001
  2408
text\<open>As above, but reorienting the vector (HOL Light's @text{GEOM\_BASIS\_MULTIPLE\_TAC})\<close>
lp15@67998
  2409
lemma Sard_lemma0:
lp15@67998
  2410
  fixes P :: "(real^'n::{finite,wellorder}) set"
lp15@67998
  2411
  assumes "a \<noteq> 0"
lp15@67998
  2412
    and P: "P \<subseteq> {x. a \<bullet> x = 0}" and "0 \<le> m" "0 \<le> e"
lp15@67998
  2413
  obtains S where "S \<in> lmeasurable"
lp15@67998
  2414
    and "{z. norm z \<le> m \<and> (\<exists>t \<in> P. norm(z - t) \<le> e)} \<subseteq> S"
lp15@67998
  2415
    and "measure lebesgue S \<le> (2 * e) * (2 * m) ^ (CARD('n) - 1)"
lp15@67998
  2416
proof -
lp15@67998
  2417
  obtain T and k::'n where T: "orthogonal_transformation T" and a: "a = T (norm a *\<^sub>R axis k (1::real))"
lp15@67998
  2418
    using rotation_rightward_line by metis
lp15@67998
  2419
  have Tinv [simp]: "T (inv T x) = x" for x
lp15@67998
  2420
    by (simp add: T orthogonal_transformation_surj surj_f_inv_f)
lp15@67998
  2421
  obtain S where S: "S \<in> lmeasurable"
lp15@67998
  2422
    and subS: "{z. norm z \<le> m \<and> (\<exists>t \<in> T-`P. norm(z - t) \<le> e)} \<subseteq> S"
lp15@67998
  2423
    and mS: "measure lebesgue S \<le> (2 * e) * (2 * m) ^ (CARD('n) - 1)"
lp15@67998
  2424
  proof (rule Sard_lemma00 [of "norm a" "axis k (1::real)" "T-`P" m e])
lp15@67998
  2425
    have "norm a *\<^sub>R axis k 1 \<bullet> x = 0" if "T x \<in> P" for x
lp15@67998
  2426
    proof -
lp15@67998
  2427
      have "a \<bullet> T x = 0"
lp15@67998
  2428
        using P that by blast
lp15@67998
  2429
      then show ?thesis
lp15@67998
  2430
        by (metis (no_types, lifting) T a orthogonal_orthogonal_transformation orthogonal_def)
lp15@67998
  2431
    qed
lp15@67998
  2432
    then show "T -` P \<subseteq> {x. norm a *\<^sub>R axis k 1 \<bullet> x = 0}"
lp15@67998
  2433
      by auto
lp15@67998
  2434
  qed (use assms T in auto)
lp15@67998
  2435
  show thesis
lp15@67998
  2436
  proof
lp15@67998
  2437
    show "T ` S \<in> lmeasurable"
lp15@67998
  2438
      using S measurable_orthogonal_image T by blast
lp15@67998
  2439
    have "{z. norm z \<le> m \<and> (\<exists>t\<in>P. norm (z - t) \<le> e)} \<subseteq> T ` {z. norm z \<le> m \<and> (\<exists>t\<in>T -` P. norm (z - t) \<le> e)}"
lp15@67998
  2440
    proof clarsimp
lp15@67998
  2441
      fix x t