Read about our upcoming Code of Conduct on this issue

SG_Library_Complement.thy 59.7 KB
Newer Older
 Lawrence Paulson committed Dec 07, 2015 1 (* Author: Sébastien Gouëzel sebastien.gouezel@univ-rennes1.fr  Lawrence Paulson committed Dec 01, 2015 2 3 4  License: BSD *)  sgouezel committed Mar 14, 2018 5 6 section \SG Libary complements\  hoelzl committed Jun 21, 2016 7 theory SG_Library_Complement  wenzelm committed Nov 03, 2017 8  imports "HOL-Probability.Probability"  Lawrence Paulson committed Dec 01, 2015 9 10 begin  sgouezel committed Mar 20, 2017 11 text \In this file are included many statements that were useful to me, but belong rather  Lawrence Paulson committed Dec 01, 2015 12 13 14 15 naturally to existing theories. In a perfect world, some of these statements would get included into these files. I tried to indicate to which of these classical theories the statements could be added.  sgouezel committed Mar 20, 2017 16 \  Lawrence Paulson committed Dec 01, 2015 17   sgouezel committed Mar 20, 2017 18 subsection \Basic logic\  Lawrence Paulson committed Dec 01, 2015 19   sgouezel committed Mar 20, 2017 20 text \This one is certainly available, but I could not locate it...\  Lawrence Paulson committed Dec 01, 2015 21 lemma equiv_neg:  sgouezel committed Aug 20, 2016 22  "\ P \ Q; \P \ \Q \ \ (P\Q)"  Lawrence Paulson committed Dec 01, 2015 23 24 25 by blast  sgouezel committed Mar 20, 2017 26 subsection \Basic set theory\  Lawrence Paulson committed Dec 01, 2015 27   sgouezel committed Mar 14, 2018 28 29 30 31 lemma compl_compl_eq_id [simp]: "UNIV - (UNIV - s) = s" by auto  Lawrence Paulson committed Dec 01, 2015 32 33 34 abbreviation sym_diff :: "'a set \ 'a set \ 'a set" (infixl "\" 70) where "sym_diff A B \ ((A - B) \ (B-A))"  sgouezel committed Mar 20, 2017 35 36 text \Not sure the next lemmas are useful, as they are proved solely by auto, so they could be reproved automatically whenever necessary.\  Lawrence Paulson committed Dec 01, 2015 37 38 39 40 41 42 43 44 45 46  lemma sym_diff_inc: "A \ C \ A \ B \ B \ C" by auto lemma sym_diff_vimage [simp]: "f-(A \ B) = (f-A) \ (f-B)" by auto  sgouezel committed Mar 20, 2017 47 subsection \Set-Interval.thy\  Lawrence Paulson committed Dec 01, 2015 48   sgouezel committed Mar 17, 2018 49 text \The next two lemmas belong naturally to \verb+Set_Interval.thy+, next to  Lawrence Paulson committed Dec 01, 2015 50 \verb+UN_le_add_shift+. They are not trivially equivalent to the corresponding lemmas  sgouezel committed Mar 20, 2017 51 with large inequalities, due to the difference when $n = 0$.\  Lawrence Paulson committed Dec 01, 2015 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68  lemma UN_le_eq_Un0_strict: "(\ii\{1.. M 0" (is "?A = ?B") proof show "?A \ ?B" proof fix x assume "x \ ?A" then obtain i where i: "i M i" by auto show "x \ ?B" proof(cases i) case 0 with i show ?thesis by simp next case (Suc j) with i show ?thesis by auto qed qed qed (auto)  sgouezel committed Mar 20, 2017 69 text \I use repeatedly this one, but I could not find it directly\  Lawrence Paulson committed Dec 01, 2015 70 71 72 73 74  lemma union_insert_0: "(\n::nat. A n) = A 0 \ (\n\{1..}. A n)" by (metis UN_insert Un_insert_left sup_bot.left_neutral One_nat_def atLeast_0 atLeast_Suc_greaterThan ivl_disj_un_singleton(1))  Lawrence Paulson committed Apr 10, 2019 75 text \Next one could be close to \verb+sum.nat_group+\  sgouezel committed Jan 20, 2016 76   nipkow committed Oct 17, 2016 77 lemma sum_arith_progression:  sgouezel committed Jan 20, 2016 78 79 80  "(\r<(N::nat). (\ijr j \ {i*N..riiri j \ {i*N..jMiscellanous basic results\  Lawrence Paulson committed Dec 01, 2015 94   sgouezel committed Sep 30, 2016 95 lemma ind_from_1 [case_names 1 Suc, consumes 1]:  sgouezel committed Jan 20, 2016 96 97  assumes "n > 0" assumes "P 1"  sgouezel committed Sep 30, 2016 98  and "\n. n > 0 \ P n \ P (Suc n)"  sgouezel committed Jan 20, 2016 99 100 101 102  shows "P n" proof - have "(n = 0) \ P n" proof (induction n)  sgouezel committed Aug 20, 2016 103  case 0 then show ?case by auto  sgouezel committed Jan 20, 2016 104 105  next case (Suc k)  sgouezel committed Sep 30, 2016 106 107 108  consider "Suc k = 1" | "Suc k > 1" by linarith then show ?case apply (cases) using assms Suc.IH by auto  sgouezel committed Jan 20, 2016 109  qed  sgouezel committed Mar 20, 2017 110  then show ?thesis using \n > 0\ by auto  sgouezel committed Jan 20, 2016 111 112 qed  sgouezel committed Mar 17, 2018 113 text \This lemma is certainly available somewhere, but I couldn't  sgouezel committed Mar 20, 2017 114 locate it\  Lawrence Paulson committed Dec 01, 2015 115 116 117  lemma tends_to_real_e: fixes u::"nat \ real"  Lawrence Paulson committed Sep 18, 2019 118  assumes "u \ l" "e>0"  sgouezel committed Sep 30, 2016 119  shows "\N. \n>N. abs(u n -l) < e"  Lawrence Paulson committed Sep 18, 2019 120  by (metis assms dist_real_def le_less lim_sequentially)  Lawrence Paulson committed Dec 01, 2015 121 122  lemma nat_mod_cong:  sgouezel committed Mar 20, 2017 123  assumes "a = b+(c::nat)"  Lawrence Paulson committed Dec 01, 2015 124 125 126 127  "a mod n = b mod n" shows "c mod n = 0" proof - let ?k = "a mod n"  haftmann committed Oct 16, 2016 128 129  obtain a1 where "a = a1*n + ?k" by (metis div_mult_mod_eq) moreover obtain b1 where "b = b1*n + ?k" using assms(2) by (metis div_mult_mod_eq)  Lawrence Paulson committed Dec 01, 2015 130 131 132 133 134  ultimately have "a1 * n + ?k = b1 * n + ?k + c" using assms(1) by arith then have "c = (a1 - b1) * n" by (simp add: diff_mult_distrib) then show ?thesis by simp qed  sgouezel committed Mar 14, 2018 135 136 137 lemma funpow_add': "(f ^^ (m + n)) x = (f ^^ m) ((f ^^ n) x)" by (simp add: funpow_add)  sgouezel committed Mar 20, 2017 138 139 text \The next two lemmas are not directly equivalent, since $f$ might not be injective.\  Lawrence Paulson committed Dec 01, 2015 140 141 142 143 144  lemma abs_Max_sum: fixes A::"real set" assumes "finite A" "A \ {}" shows "abs(Max A) \ (\a\A. abs(a))"  Lawrence Paulson committed Sep 18, 2019 145  by (simp add: assms member_le_sum)  Lawrence Paulson committed Dec 01, 2015 146 147 148 149 150 151 152  lemma abs_Max_sum2: fixes f::"_ \ real" assumes "finite A" "A \ {}" shows "abs(Max (fA)) \ (\a\A. abs(f a))" using assms by (induct rule: finite_ne_induct, auto)  sgouezel committed Mar 20, 2017 153 subsection \Conditionally-Complete-Lattices.thy\  Lawrence Paulson committed Dec 01, 2015 154   sgouezel committed Mar 20, 2017 155 156 157 158 159 lemma mono_cInf: fixes f :: "'a::conditionally_complete_lattice \ 'b::conditionally_complete_lattice" assumes "mono f" "A \ {}" "bdd_below A" shows "f(Inf A) \ Inf (fA)" using assms by (simp add: cINF_greatest cInf_lower monoD)  sgouezel committed Sep 30, 2016 160   sgouezel committed Mar 20, 2017 161 162 163 164 165 166 167 168 169 170 171 172 173 174 lemma mono_bij_cInf: fixes f :: "'a::conditionally_complete_linorder \ 'b::conditionally_complete_linorder" assumes "mono f" "bij f" "A \ {}" "bdd_below A" shows "f (Inf A) = Inf (fA)" proof - have "(inv f) (Inf (fA)) \ Inf ((inv f)(fA))" apply (rule cInf_greatest, auto simp add: assms(3)) using mono_inv[OF assms(1) assms(2)] assms by (simp add: mono_def bdd_below_image_mono cInf_lower) then have "Inf (fA) \ f (Inf ((inv f)(fA)))" by (metis (no_types, lifting) assms(1) assms(2) mono_def bij_inv_eq_iff) also have "... = f(Inf A)" using assms by (simp add: bij_is_inj) finally show ?thesis using mono_cInf[OF assms(1) assms(3) assms(4)] by auto qed  Lawrence Paulson committed Dec 01, 2015 175   sgouezel committed Mar 20, 2017 176 177 subsection \Topological-spaces.thy\  sgouezel committed Mar 14, 2018 178 179 180 181 182 183 184 185 186 187 188 189 190 191 lemma open_less_abs [simp]: "open {x. (C::real) < abs x}" proof - have *: "{x. C < abs x} = abs-{C<..}" by auto show ?thesis unfolding * by (auto intro!: continuous_intros) qed lemma closed_le_abs [simp]: "closed {x. (C::real) \ abs x}" proof - have *: "{x. C \ \x\} = abs-{C..}" by auto show ?thesis unfolding * by (auto intro!: continuous_intros) qed  sgouezel committed Mar 20, 2017 192 text \The next statements come from the same statements for true subsequences\  Lawrence Paulson committed Dec 01, 2015 193 194  lemma eventually_weak_subseq:  sgouezel committed Aug 20, 2016 195 196 197  fixes u::"nat \ nat" assumes "(\n. real(u n)) \ \" "eventually P sequentially" shows "eventually (\n. P (u n)) sequentially"  Lawrence Paulson committed Dec 01, 2015 198 199 200 201 proof - obtain N where *: "\n\N. P n" using assms(2) unfolding eventually_sequentially by auto obtain M where "\m\M. ereal(u m) \ N" using assms(1) by (meson Lim_PInfty) then have "\m. m \ M \ u m \ N" by auto  sgouezel committed Mar 20, 2017 202  then have "\m. m \ M \ P(u m)" using \\n\N. P n\ by simp  Lawrence Paulson committed Dec 01, 2015 203 204 205 206  then show ?thesis unfolding eventually_sequentially by auto qed lemma filterlim_weak_subseq:  sgouezel committed Aug 20, 2016 207 208 209  fixes u::"nat \ nat" assumes "(\n. real(u n)) \ \" shows "LIM n sequentially. u n:> at_top"  Lawrence Paulson committed Dec 01, 2015 210 211 212 213 unfolding filterlim_iff by (metis assms eventually_weak_subseq) lemma limit_along_weak_subseq: fixes u::"nat \ nat" and v::"nat \ _"  wenzelm committed Dec 29, 2015 214 215  assumes "(\n. real(u n)) \ \" "v \ l" shows "(\ n. v(u n)) \ l"  Lawrence Paulson committed Dec 01, 2015 216 217 using filterlim_compose[of v, OF _ filterlim_weak_subseq] assms by auto  sgouezel committed Mar 14, 2018 218 219 220 221 222 223 224 225 226 227 228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 lemma frontier_indist_le: assumes "x \ frontier {y. infdist y S \ r}" shows "infdist x S = r" proof - have "infdist x S = r" if H: "\e>0. (\y. infdist y S \ r \ dist x y < e) \ (\z. \ infdist z S \ r \ dist x z < e)" proof - have "infdist x S < r + e" if "e > 0" for e proof - obtain y where "infdist y S \ r" "dist x y < e" using H \e > 0\ by blast then show ?thesis by (metis add.commute add_mono_thms_linordered_field(3) infdist_triangle le_less_trans) qed then have A: "infdist x S \ r" by (meson field_le_epsilon order.order_iff_strict) have "r < infdist x S + e" if "e > 0" for e proof - obtain y where "$$infdist y S \ r)" "dist x y < e" using H \e > 0\ by blast then have "r < infdist y S" by auto also have "... \ infdist x S + dist y x" by (rule infdist_triangle) finally show ?thesis using \dist x y < e\ by (simp add: dist_commute) qed then have B: "r \ infdist x S" by (meson field_le_epsilon order.order_iff_strict) show ?thesis using A B by auto qed then show ?thesis using assms unfolding frontier_straddle by auto qed subsection \Limits\  sgouezel committed Jan 05, 2016 253   sgouezel committed Mar 20, 2017 254 255 256 text \The next lemmas are not very natural, but I needed them several times\ lemma tendsto_shift_1_over_n [tendsto_intros]:  sgouezel committed Jan 20, 2016 257 258 259 260 261 262 263 264 265  fixes f::"nat \ real" assumes "(\n. f n / n) \ l" shows "(\n. f (n+k) / n) \ l" proof - have "(1+k*(1/n))* (f(n+k)/(n+k)) = f(n+k)/n" if "n>0" for n using that by (auto simp add: divide_simps) with eventually_mono[OF eventually_gt_at_top[of "0::nat"] this] have "eventually (\n.(1+k*(1/n))* (f(n+k)/(n+k)) = f(n+k)/n) sequentially" by auto moreover have "(\n. (1+k*(1/n))* (f(n+k)/(n+k))) \ (1+real k*0) * l"  sgouezel committed Mar 20, 2017 266  by (intro tendsto_intros LIMSEQ_ignore_initial_segment assms)  sgouezel committed Jan 20, 2016 267 268 269  ultimately show ?thesis using Lim_transform_eventually by auto qed  sgouezel committed Mar 20, 2017 270 lemma tendsto_shift_1_over_n' [tendsto_intros]:  sgouezel committed Jan 20, 2016 271 272 273 274 275 276 277 278 279  fixes f::"nat \ real" assumes "(\n. f n / n) \ l" shows "(\n. f (n-k) / n) \ l" proof - have "(1-k*(1/(n+k)))* (f n/ n) = f n/(n+k)" if "n>0" for n using that by (auto simp add: divide_simps) with eventually_mono[OF eventually_gt_at_top[of "0::nat"] this] have "eventually (\n. (1-k*(1/(n+k)))* (f n/ n) = f n/(n+k)) sequentially" by auto moreover have "(\n. (1-k*(1/(n+k)))* (f n/ n)) \ (1-real k*0) * l"  sgouezel committed Mar 20, 2017 280  by (intro tendsto_intros assms LIMSEQ_ignore_initial_segment)  sgouezel committed Jan 20, 2016 281 282 283  ultimately have "(\n. f n / (n+k)) \ l" using Lim_transform_eventually by auto then have a: "(\n. f(n-k)/(n-k+k)) \ l" using seq_offset_neg by auto  sgouezel committed Aug 20, 2016 284 285  have "f(n-k)/(n-k+k) = f(n-k)/n" if "n>k" for n using that by auto  sgouezel committed Feb 24, 2016 286 287  with eventually_mono[OF eventually_gt_at_top[of k] this] have "eventually (\n. f(n-k)/(n-k+k) = f(n-k)/n) sequentially"  sgouezel committed Aug 20, 2016 288  by auto  Lawrence Paulson committed Aug 15, 2019 289  with Lim_transform_eventually[OF a this]  sgouezel committed Feb 24, 2016 290  show ?thesis by auto  sgouezel committed Jan 20, 2016 291 qed  sgouezel committed Jan 05, 2016 292   sgouezel committed Mar 14, 2018 293 declare LIMSEQ_realpow_zero [tendsto_intros]  sgouezel committed Mar 20, 2017 294 295  subsection \Topology-Euclidean-Space\  Lawrence Paulson committed Dec 01, 2015 296   sgouezel committed Mar 20, 2017 297 298 text \A (more usable) variation around \verb+continuous_on_closure_sequentially+. The assumption that the spaces are metric spaces is definitely too strong, but sufficient for most applications.\  sgouezel committed Sep 30, 2016 299 300 301 302 303 304 305 306 307 308  lemma continuous_on_closure_sequentially': fixes f::"'a::metric_space \ 'b::metric_space" assumes "continuous_on (closure C) f" "\(n::nat). u n \ C" "u \ l" shows "(\n. f (u n)) \ f l" proof - have "l \ closure C" unfolding closure_sequential using assms by auto then show ?thesis  sgouezel committed Mar 20, 2017 309  using \continuous_on (closure C) f\ unfolding comp_def continuous_on_closure_sequentially  sgouezel committed Sep 30, 2016 310 311 312 313  using assms by auto qed  sgouezel committed Mar 20, 2017 314 subsection \Convexity\  sgouezel committed Sep 30, 2016 315 316 317 318 319 320 321 322 323 324 325 326 327 328 329 330 331  lemma convex_on_mean_ineq: fixes f::"real \ real" assumes "convex_on A f" "x \ A" "y \ A" shows "f ((x+y)/2) \ (f x + f y) / 2" using convex_onD[OF assms(1), of "1/2" x y] using assms by (auto simp add: divide_simps) lemma convex_on_closure: assumes "convex (C::'a::real_normed_vector set)" "convex_on C f" "continuous_on (closure C) f" shows "convex_on (closure C) f" proof (rule convex_onI) fix x y::'a and t::real assume "x \ closure C" "y \ closure C" "0 < t" "t < 1" obtain u v::"nat \ 'a" where *: "\n. u n \ C" "u \ x" "\n. v n \ C" "v \ y"  sgouezel committed Mar 20, 2017 332  using \x \ closure C\ \y \ closure C\ unfolding closure_sequential by blast  sgouezel committed Sep 30, 2016 333 334  define w where "w = (\n. (1-t) *\<^sub>R (u n) + t *\<^sub>R (v n))" have "w n \ C" for n  sgouezel committed Mar 20, 2017 335  using \0 < t\ \t< 1\ convexD[OF \convex C\ *(1)[of n] *(3)[of n]] unfolding w_def by auto  sgouezel committed Sep 30, 2016 336  have "w \ ((1-t) *\<^sub>R x + t *\<^sub>R y)"  sgouezel committed Mar 20, 2017 337  unfolding w_def using *(2) *(4) by (intro tendsto_intros)  sgouezel committed Sep 30, 2016 338 339  have *: "f(w n) \ (1-t) * f(u n) + t * f (v n)" for n  sgouezel committed Mar 20, 2017 340  using *(1) *(3) \convex_on C f\ \0 \t<1\ less_imp_le unfolding w_def  Lawrence Paulson committed Oct 06, 2020 341  convex_on_alt by (simp add: add.commute)  sgouezel committed Sep 30, 2016 342  have i: "(\n. f (w n)) \ f ((1-t) *\<^sub>R x + t *\<^sub>R y)"  sgouezel committed Mar 20, 2017 343  by (rule continuous_on_closure_sequentially'[OF assms(3) \\n. w n \ C\ \w \ ((1-t) *\<^sub>R x + t *\<^sub>R y)\])  sgouezel committed Sep 30, 2016 344  have ii: "(\n. (1-t) * f(u n) + t * f (v n)) \ (1-t) * f x + t * f y"  sgouezel committed Mar 20, 2017 345 346 347  apply (intro tendsto_intros) apply (rule continuous_on_closure_sequentially'[OF assms(3) \\n. u n \ C\ \u \ x\]) apply (rule continuous_on_closure_sequentially'[OF assms(3) \\n. v n \ C\ \v \ y\])  sgouezel committed Sep 30, 2016 348 349 350 351 352  done show "f ((1 - t) *\<^sub>R x + t *\<^sub>R y) \ (1 - t) * f x + t * f y" apply (rule LIMSEQ_le[OF i ii]) using * by auto qed  sgouezel committed Mar 20, 2017 353 lemma convex_on_norm [simp]:  sgouezel committed Sep 30, 2016 354 355 356 357 358 359 360 361 362 363 364 365 366 367 368 369 370 371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394  "convex_on UNIV (\(x::'a::real_normed_vector). norm x)" using convex_on_dist[of UNIV "0::'a"] by auto lemma continuous_abs_powr [continuous_intros]: assumes "p > 0" shows "continuous_on UNIV (\(x::real). \x\ powr p)" apply (rule continuous_on_powr') using assms by (auto intro: continuous_intros) lemma continuous_mult_sgn [continuous_intros]: fixes f::"real \ real" assumes "continuous_on UNIV f" "f 0 = 0" shows "continuous_on UNIV (\x. sgn x * f x)" proof - have *: "continuous_on {0..} (\x. sgn x * f x)" apply (subst continuous_on_cong[of "{0..}" "{0..}" _ f], auto simp add: sgn_real_def assms(2)) by (rule continuous_on_subset[OF assms(1)], auto) have **: "continuous_on {..0} (\x. sgn x * f x)" apply (subst continuous_on_cong[of "{..0}" "{..0}" _ "\x. -f x"], auto simp add: sgn_real_def assms(2)) by (rule continuous_on_subset[of UNIV], auto simp add: assms intro!: continuous_intros) show ?thesis using continuous_on_closed_Un[OF _ _ * **] apply (auto intro: continuous_intros) using continuous_on_subset by fastforce qed lemma DERIV_abs_powr [derivative_intros]: assumes "p > (1::real)" shows "DERIV (\x. \x\ powr p) x :> p * sgn x * \x\ powr (p - 1)" proof - consider "x = 0" | "x>0" | "x < 0" by linarith then show ?thesis proof (cases) case 1 have "continuous_on UNIV (\x. sgn x * \x\ powr (p - 1))" by (auto simp add: assms intro!:continuous_intros) then have "(\h. sgn h * \h\ powr (p-1)) \0\ (\h. sgn h * \h\ powr (p-1)) 0" using continuous_on_def by blast moreover have "\h\ powr p / h = sgn h * \h\ powr (p-1)" for h proof - have "\h\ powr p / h = sgn h * \h\ powr p / \h\" by (auto simp add: algebra_simps divide_simps sgn_real_def) also have "... = sgn h * \h\ powr (p-1)"  sgouezel committed Mar 20, 2017 395  using assms apply (cases "h = 0") apply (auto)  sgouezel committed Mar 14, 2018 396  by (metis abs_ge_zero powr_diff [symmetric] powr_one_gt_zero_iff times_divide_eq_right)  sgouezel committed Sep 30, 2016 397 398 399  finally show ?thesis by simp qed ultimately have "(\h. \h\ powr p / h) \0\ 0" by auto  sgouezel committed Mar 20, 2017 400  then show ?thesis unfolding DERIV_def by (auto simp add: \x = 0$$  sgouezel committed Sep 30, 2016 401 402 403  next case 2 have *: "\\<^sub>F y in nhds x. \y\ powr p = y powr p"  sgouezel committed Mar 20, 2017 404  unfolding eventually_nhds apply (rule exI[of _ "{0<..}"]) using \x > 0\ by auto  sgouezel committed Sep 30, 2016 405 406  show ?thesis apply (subst DERIV_cong_ev[of _ x _ "(\x. x powr p)" _ "p * x powr (p-1)"])  sgouezel committed Mar 20, 2017 407  using \x > 0\ by (auto simp add: * has_real_derivative_powr)  sgouezel committed Sep 30, 2016 408 409 410  next case 3 have *: "\\<^sub>F y in nhds x. \y\ powr p = (-y) powr p"  sgouezel committed Mar 20, 2017 411  unfolding eventually_nhds apply (rule exI[of _ "{..<0}"]) using \x < 0\ by auto  sgouezel committed Sep 30, 2016 412 413  show ?thesis apply (subst DERIV_cong_ev[of _ x _ "(\x. (-x) powr p)" _ "p * (- x) powr (p - real 1) * - 1"])  sgouezel committed Mar 20, 2017 414 415  using \x < 0\ apply (simp, simp add: *, simp) apply (rule DERIV_fun_powr[of "\y. -y" "-1" "x" p]) using \x < 0\ by (auto simp add: derivative_intros)  sgouezel committed Sep 30, 2016 416 417 418 419 420 421  qed qed lemma convex_abs_powr: assumes "p \ 1" shows "convex_on UNIV (\x::real. \x\ powr p)"  sgouezel committed Mar 20, 2017 422 proof (cases "p = 1")  sgouezel committed Sep 30, 2016 423 424 425 426 427 428 429 430 431 432  case True have "convex_on UNIV (\x::real. norm x)" by (rule convex_on_norm) moreover have "\x\ powr p = norm x" for x using True by auto ultimately show ?thesis by simp next case False then have "p > 1" using assms by auto define g where "g = (\x::real. p * sgn x * \x\ powr (p - 1))" have *: "DERIV (\x. \x\ powr p) x :> g x" for x  sgouezel committed Mar 20, 2017 433  unfolding g_def using \p>1\ by (intro derivative_intros)  sgouezel committed Sep 30, 2016 434 435  have **: "g x \ g y" if "x \ y" for x y proof -  sgouezel committed Mar 20, 2017 436  consider "x \ 0 \ y \ 0" | "x \ 0 \ y \ 0" | "x < 0 \ y > 0" using \x \ y\ by linarith  sgouezel committed Sep 30, 2016 437 438 439  then show ?thesis proof (cases) case 1  sgouezel committed Mar 20, 2017 440  then show ?thesis unfolding g_def sgn_real_def using \p>1\ \x \ y\ by (auto simp add: powr_mono2)  sgouezel committed Sep 30, 2016 441 442  next case 2  sgouezel committed Mar 20, 2017 443  then show ?thesis unfolding g_def sgn_real_def using \p>1\ \x \ y\ by (auto simp add: powr_mono2)  sgouezel committed Sep 30, 2016 444 445  next case 3  sgouezel committed Mar 20, 2017 446  then have "g x \ 0" "0 \ g y" unfolding g_def using \p > 1\ by auto  sgouezel committed Sep 30, 2016 447 448 449 450 451 452 453 454 455 456 457 458  then show ?thesis by simp qed qed show ?thesis apply (rule convex_on_realI[of _ _ g]) using * ** by auto qed lemma convex_powr: assumes "p \ 1" shows "convex_on {0..} (\x::real. x powr p)" proof - have "convex_on {0..} (\x::real. \x\ powr p)"  sgouezel committed Mar 20, 2017 459  using convex_abs_powr[OF \p \ 1\] convex_on_subset by auto  sgouezel committed Sep 30, 2016 460 461 462 463 464 465 466 467 468 469 470  moreover have "\x\ powr p = x powr p" if "x \ {0..}" for x using that by auto ultimately show ?thesis by (simp add: convex_on_def) qed lemma convex_powr': assumes "p > 0" "p \ 1" shows "convex_on {0..} (\x::real. - (x powr p))" proof - have "convex_on {0<..} (\x::real. - (x powr p))" apply (rule convex_on_realI[of _ _ "\x. -p * x powr (p-1)"]) apply (auto intro!:derivative_intros simp add: has_real_derivative_powr)  sgouezel committed Mar 20, 2017 471  using \p > 0\ \p \ 1\ by (auto simp add: algebra_simps divide_simps powr_mono2')  sgouezel committed Sep 30, 2016 472  moreover have "continuous_on {0..} (\x::real. - (x powr p))"  sgouezel committed Mar 20, 2017 473  by (rule continuous_on_minus, rule continuous_on_powr', auto simp add: \p > 0\ intro!: continuous_intros)  sgouezel committed Sep 30, 2016 474 475 476 477 478 479 480 481 482 483 484 485 486  moreover have "{(0::real)..} = closure {0<..}" "convex {(0::real)<..}" by auto ultimately show ?thesis using convex_on_closure by metis qed lemma convex_fx_plus_fy_ineq: fixes f::"real \ real" assumes "convex_on {0..} f" "x \ 0" "y \ 0" "f 0 = 0" shows "f x + f y \ f (x+y)" proof - have *: "f a + f b \ f (a+b)" if "a \ 0" "b \ a" for a b proof (cases "a = 0") case False  sgouezel committed Mar 20, 2017 487  then have "a > 0" "b > 0" using \b \ a\ \a \ 0\ by auto  sgouezel committed Sep 30, 2016 488  have "(f 0 - f a) / (0 - a) \ (f 0 - f (a+b))/ (0 - (a+b))"  sgouezel committed Mar 20, 2017 489  apply (rule convex_on_diff[OF \convex_on {0..} f\]) using \a > 0\ \b > 0\ by auto  sgouezel committed Sep 30, 2016 490  also have "... \ (f b - f (a+b)) / (b - (a+b))"  sgouezel committed Mar 20, 2017 491  apply (rule convex_on_diff[OF \convex_on {0..} f\]) using \a > 0\ \b > 0\ by auto  sgouezel committed Sep 30, 2016 492  finally show ?thesis  sgouezel committed Mar 20, 2017 493 494  using \a > 0\ \b > 0\ \f 0 = 0\ by (auto simp add: divide_simps algebra_simps) qed (simp add: \f 0 = 0\)  sgouezel committed Sep 30, 2016 495  then show ?thesis  sgouezel committed Mar 20, 2017 496  using \x \ 0\ \y \ 0\ by (metis add.commute le_less not_le)  sgouezel committed Sep 30, 2016 497 498 499 500 501 502 qed lemma x_plus_y_p_le_xp_plus_yp: fixes p x y::real assumes "p > 0" "p \ 1" "x \ 0" "y \ 0" shows "(x + y) powr p \ x powr p + y powr p"  sgouezel committed Mar 20, 2017 503 using convex_fx_plus_fy_ineq[OF convex_powr'[OF \p > 0\ \p \ 1\] \x \ 0\ \y \ 0\] by auto  Lawrence Paulson committed Dec 01, 2015 504 505   sgouezel committed Mar 20, 2017 506 subsection \Nonnegative-extended-real.thy\  sgouezel committed Sep 30, 2016 507   sgouezel committed Mar 14, 2018 508 509 510 511 512 513 514 515 516 517 518 519 520 lemma x_plus_top_ennreal [simp]: "x + \ = (\::ennreal)" by simp lemma ennreal_ge_nat_imp_PInf: fixes x::ennreal assumes "\N. x \ of_nat N" shows "x = \" using assms apply (cases x, auto) by (meson not_less reals_Archimedean2) lemma ennreal_archimedean: assumes "x \ (\::ennreal)" shows "\n::nat. x \ n"  Lawrence Paulson committed Sep 18, 2019 521  using assms ennreal_ge_nat_imp_PInf linear by blast  sgouezel committed Mar 14, 2018 522   sgouezel committed Sep 30, 2016 523 524 525 526 527 528 529 530 531 532 533 534 535 536 lemma e2ennreal_mult: fixes a b::ereal assumes "a \ 0" shows "e2ennreal(a * b) = e2ennreal a * e2ennreal b" by (metis assms e2ennreal_neg eq_onp_same_args ereal_mult_le_0_iff linear times_ennreal.abs_eq) lemma e2ennreal_mult': fixes a b::ereal assumes "b \ 0" shows "e2ennreal(a * b) = e2ennreal a * e2ennreal b" using e2ennreal_mult[OF assms, of a] by (simp add: mult.commute) lemma SUP_real_ennreal: assumes "A \ {}" "bdd_above (fA)"  haftmann committed Nov 08, 2018 537  shows "(SUP a\A. ennreal (f a)) = ennreal(SUP a\A. f a)"  sgouezel committed Sep 30, 2016 538 539 540 apply (rule antisym, simp add: SUP_least assms(2) cSUP_upper ennreal_leI) by (metis assms(1) ennreal_SUP ennreal_less_top le_less)  sgouezel committed Mar 20, 2017 541 542 543 544 545 546 lemma e2ennreal_Liminf: "F \ bot \ e2ennreal (Liminf F f) = Liminf F (\n. e2ennreal (f n))" by (rule Liminf_compose_continuous_mono[symmetric]) (auto simp: mono_def e2ennreal_mono continuous_on_e2ennreal) lemma e2ennreal_eq_infty[simp]: "0 \ x \ e2ennreal x = top \ x = \"  sgouezel committed Mar 14, 2018 547  by (cases x) (auto)  sgouezel committed Mar 20, 2017 548   sgouezel committed Sep 30, 2016 549 550 551 552 553 554 555 556 557 558 559 560 561 562 lemma ennreal_Inf_cmult: assumes "c>(0::real)" shows "Inf {ennreal c * x |x. P x} = ennreal c * Inf {x. P x}" proof - have "(\x::ennreal. c * x) (Inf {x::ennreal. P x}) = Inf ((\x::ennreal. c * x){x::ennreal. P x})" apply (rule mono_bij_Inf) apply (simp add: monoI mult_left_mono) apply (rule bij_betw_byWitness[of _ "\x. (x::ennreal) / c"], auto simp add: assms) apply (metis assms ennreal_lessI ennreal_neq_top mult.commute mult_divide_eq_ennreal not_less_zero) apply (metis assms divide_ennreal_def ennreal_less_zero_iff ennreal_neq_top less_irrefl mult.assoc mult.left_commute mult_divide_eq_ennreal) done then show ?thesis by (simp only: setcompr_eq_image[symmetric]) qed  hoelzl committed Apr 14, 2016 563 564 565 566 567 568 569 570 571 572 573 lemma continuous_on_const_minus_ennreal: fixes f :: "'a :: topological_space \ ennreal" shows "continuous_on A f \ continuous_on A (\x. a - f x)" including ennreal.lifting proof (transfer fixing: A; clarsimp) fix f :: "'a \ ereal" and a :: "ereal" assume "0 \ a" "\x. 0 \ f x" and f: "continuous_on A f" then show "continuous_on A (\x. max 0 (a - f x))" proof cases assume "\r. a = ereal r" with f show ?thesis by (auto simp: continuous_on_def minus_ereal_def ereal_Lim_uminus[symmetric]  sgouezel committed Aug 20, 2016 574  intro!: tendsto_add_ereal_general tendsto_max)  hoelzl committed Apr 14, 2016 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589  next assume "\r. a = ereal r" with \0 \ a\ have "a = \" by (cases a) auto then show ?thesis by (simp add: continuous_on_const) qed qed lemma const_minus_Liminf_ennreal: fixes a :: ennreal shows "F \ bot \ a - Liminf F f = Limsup F (\x. a - f x)" by (intro Limsup_compose_continuous_antimono[symmetric]) (auto simp: antimono_def ennreal_mono_minus continuous_on_id continuous_on_const_minus_ennreal)  sgouezel committed Sep 30, 2016 590 591 592 593 594 595 596 lemma tendsto_cmult_ennreal [tendsto_intros]: fixes c l::ennreal assumes "\(c = \ \ l = 0)" "(f \ l) F" shows "((\x. c * f x) \ c * l) F" by (cases "c = 0", insert assms, auto intro!: tendsto_intros)  sgouezel committed Aug 20, 2016 597   sgouezel committed Mar 14, 2018 598 subsection \Indicator-Function.thy\  sgouezel committed Aug 20, 2016 599   sgouezel committed Mar 20, 2017 600 text \There is something weird with \verb+sum_mult_indicator+: it is defined both  sgouezel committed Aug 20, 2016 601 in Indicator.thy and BochnerIntegration.thy, with a different meaning. I am surprised  sgouezel committed Mar 20, 2017 602 there is no name collision... Here, I am using the version from BochnerIntegration.\  sgouezel committed Aug 20, 2016 603   nipkow committed Oct 17, 2016 604 lemma sum_indicator_eq_card2:  sgouezel committed Aug 20, 2016 605 606  assumes "finite I" shows "(\i\I. (indicator (P i) x)::nat) = card {i\I. x \ P i}"  nipkow committed Oct 17, 2016 607 608 using sum_mult_indicator [OF assms, of "\y. 1::nat" P "\y. x"] unfolding card_eq_sum by auto  sgouezel committed Aug 20, 2016 609   sgouezel committed Mar 14, 2018 610 611 612 613 614 615 616 617 618 619 620 621 622 lemma disjoint_family_indicator_le_1: assumes "disjoint_family_on A I" shows "(\ i\ I. indicator (A i) x) \ (1::'a:: {comm_monoid_add,zero_less_one})" proof (cases "finite I") case True then have *: "(\ i\ I. indicator (A i) x) = ((indicator (\i\I. A i) x)::'a)" by (simp add: indicator_UN_disjoint[OF True assms(1), of x]) show ?thesis unfolding * unfolding indicator_def by (simp add: order_less_imp_le) next case False then show ?thesis by (simp add: order_less_imp_le) qed  sgouezel committed Aug 20, 2016 623   sgouezel committed Mar 20, 2017 624 subsection \sigma-algebra.thy\  Lawrence Paulson committed Dec 01, 2015 625 626 627 628 629 630 631 632 633 634 635 636 637  lemma algebra_intersection: assumes "algebra \ A" "algebra \ B" shows "algebra \ (A \ B)" apply (subst algebra_iff_Un) using assms by (auto simp add: algebra_iff_Un) lemma sigma_algebra_intersection: assumes "sigma_algebra \ A" "sigma_algebra \ B" shows "sigma_algebra \ (A \ B)" apply (subst sigma_algebra_iff) using assms by (auto simp add: sigma_algebra_iff algebra_intersection)  sgouezel committed Mar 20, 2017 638 639 640 641 642 lemma subalgebra_M_M [simp]: "subalgebra M M" by (simp add: subalgebra_def) text \The next one is \verb+disjoint_family_Suc+ with inclusions reversed.\  Lawrence Paulson committed Dec 01, 2015 643 644 645 646 647  lemma disjoint_family_Suc2: assumes Suc: "\n. A (Suc n) \ A n" shows "disjoint_family (\i. A i - A (Suc i))" proof -  sgouezel committed Sep 30, 2016 648 649 650 651 652 653 654 655 656  have "A (m+n) \ A n" for m n proof (induct m) case 0 show ?case by simp next case (Suc m) then show ?case by (metis Suc_eq_plus1 assms add.commute add.left_commute subset_trans) qed then have "A m \ A n" if "m > n" for m n by (metis that add.commute le_add_diff_inverse nat_less_le)  sgouezel committed Aug 20, 2016 657  then show ?thesis  Lawrence Paulson committed Dec 07, 2015 658  by (auto simp add: disjoint_family_on_def)  Lawrence Paulson committed Dec 10, 2015 659  (metis insert_absorb insert_subset le_SucE le_antisym not_le_imp_less)  Lawrence Paulson committed Dec 01, 2015 660 661 662 qed  sgouezel committed Mar 20, 2017 663 subsection \Measure-Space.thy\  Lawrence Paulson committed Dec 01, 2015 664   nipkow committed Oct 17, 2016 665 lemma AE_equal_sum:  Lawrence Paulson committed Dec 01, 2015 666 667 668 669 670 671 672 673  assumes "\i. AE x in M. f i x = g i x" shows "AE x in M. (\i\I. f i x) = (\i\I. g i x)" proof (cases) assume "finite I" have "\A. A \ null_sets M \ (\x\ (space M - A). f i x = g i x)" for i using assms(1)[of i] by (metis (mono_tags, lifting) AE_E3) then obtain A where A: "\i. A i \ null_sets M \ (\x\ (space M -A i). f i x = g i x)" by metis  sgouezel committed Aug 20, 2016 674  define B where "B = (\i\I. A i)"  sgouezel committed Mar 20, 2017 675  have "B \ null_sets M" using \finite I\ A B_def by blast  hoelzl committed Oct 17, 2016 676  then have "AE x in M. x \ space M - B" by (simp add: AE_not_in)  Lawrence Paulson committed Dec 01, 2015 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692  moreover { fix x assume "x \ space M - B" then have "\i. i \ I \ f i x = g i x" unfolding B_def using A by auto then have "(\i\I. f i x) = (\i\I. g i x)" by auto } ultimately show ?thesis by auto qed (simp) lemma emeasure_pos_unionE: assumes "\ (N::nat). A N \ sets M" "emeasure M (\N. A N) > 0" shows "\N. emeasure M (A N) > 0" proof (rule ccontr) assume "\(\N. emeasure M (A N) > 0)" then have "\N. A N \ null_sets M"  hoelzl committed Apr 14, 2016 693  using assms(1) by auto  Lawrence Paulson committed Dec 01, 2015 694 695 696 697  then have "(\N. A N) \ null_sets M" by auto then show False using assms(2) by auto qed  sgouezel committed Apr 04, 2016 698 699 700 lemma (in prob_space) emeasure_intersection: fixes e::"nat \ real" assumes [measurable]: "\n. U n \ sets M"  sgouezel committed Aug 20, 2016 701 702 703  and [simp]: "\n. 0 \ e n" "summable e" and ge: "\n. emeasure M (U n) \ 1 - (e n)" shows "emeasure M (\n. U n) \ 1 - (\n. e n)"  sgouezel committed Apr 04, 2016 704 proof -  sgouezel committed Aug 20, 2016 705  define V where "V = (\n. space M - (U n))"  sgouezel committed Apr 04, 2016 706 707 708  have [measurable]: "V n \ sets M" for n unfolding V_def by auto have *: "emeasure M (V n) \ e n" for n  hoelzl committed Apr 14, 2016 709  unfolding V_def using ge[of n] by (simp add: emeasure_eq_measure prob_compl ennreal_leI)  sgouezel committed Apr 04, 2016 710 711  have "emeasure M (\n. V n) \ (\n. emeasure M (V n))" by (rule emeasure_subadditive_countably, auto)  hoelzl committed Apr 14, 2016 712 713 714 715  also have "... \ (\n. ennreal (e n))" using * by (intro suminf_le) auto also have "... = ennreal (\n. e n)" by (intro suminf_ennreal_eq) auto  sgouezel committed Apr 04, 2016 716 717  finally have "emeasure M (\n. V n) \ suminf e" by simp then have "1 - suminf e \ emeasure M (space M - (\n. V n))"  hoelzl committed Apr 14, 2016 718  by (simp add: emeasure_eq_measure prob_compl suminf_nonneg)  sgouezel committed Apr 04, 2016 719  also have "... \ emeasure M (\n. U n)"  hoelzl committed Apr 14, 2016 720  by (rule emeasure_mono) (auto simp: V_def)  sgouezel committed Apr 04, 2016 721 722 723  finally show ?thesis by simp qed  Lawrence Paulson committed Dec 01, 2015 724 725 726 727 728 729 730 lemma null_sym_diff_transitive: assumes "A \ B \ null_sets M" "B \ C \ null_sets M" and [measurable]: "A \ sets M" "C \ sets M" shows "A \ C \ null_sets M" proof - have "A \ B \ B \ C \ null_sets M" using assms(1) assms(2) by auto moreover have "A \ C \ A \ B \ B \ C" by auto  hoelzl committed Oct 18, 2016 731  ultimately show ?thesis by (meson null_sets_subset assms(3) assms(4) sets.Diff sets.Un)  Lawrence Paulson committed Dec 01, 2015 732 733 734 735 736 737 738 qed lemma Delta_null_of_null_is_null: assumes "B \ sets M" "A \ B \ null_sets M" "A \ null_sets M" shows "B \ null_sets M" proof - have "B \ A \ (A \ B)" by auto  hoelzl committed Oct 18, 2016 739  then show ?thesis using assms by (meson null_sets.Un null_sets_subset)  Lawrence Paulson committed Dec 01, 2015 740 741 742 743 744 745 746 qed lemma Delta_null_same_emeasure: assumes "A \ B \ null_sets M" and [measurable]: "A \ sets M" "B \ sets M" shows "emeasure M A = emeasure M B" proof - have "A = (A \ B) \ (A-B)" by blast  hoelzl committed Oct 18, 2016 747  moreover have "A-B \ null_sets M" using assms null_sets_subset by blast  Lawrence Paulson committed Dec 01, 2015 748 749 750  ultimately have a: "emeasure M A = emeasure M (A \ B)" using emeasure_Un_null_set by (metis assms(2) assms(3) sets.Int) have "B = (A \ B) \ (B-A)" by blast  hoelzl committed Oct 18, 2016 751  moreover have "B-A \ null_sets M" using assms null_sets_subset by blast  Lawrence Paulson committed Dec 01, 2015 752 753 754 755 756 757  ultimately have "emeasure M B = emeasure M (A \ B)" using emeasure_Un_null_set by (metis assms(2) assms(3) sets.Int) then show ?thesis using a by auto qed lemma AE_upper_bound_inf_ereal: fixes F G::"'a \ ereal"  hoelzl committed Apr 14, 2016 758  assumes "\e. (e::real) > 0 \ AE x in M. F x \ G x + e"  Lawrence Paulson committed Dec 01, 2015 759 760  shows "AE x in M. F x \ G x" proof -  hoelzl committed Apr 14, 2016 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777  have "AE x in M. \n::nat. F x \ G x + ereal (1 / Suc n)" using assms by (auto simp: AE_all_countable) then show ?thesis proof (eventually_elim) fix x assume x: "\n::nat. F x \ G x + ereal (1 / Suc n)" show "F x \ G x" proof (intro ereal_le_epsilon2[of _ "G x"] allI impI) fix e :: real assume "0 < e" then obtain n where n: "1 / Suc n < e" by (blast elim: nat_approx_posE) have "F x \ G x + 1 / Suc n" using x by simp also have "\ \ G x + e" using n by (intro add_mono ennreal_leI) auto finally show "F x \ G x + ereal e" . qed qed  Lawrence Paulson committed Dec 01, 2015 778 779 qed  sgouezel committed Mar 14, 2018 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820  text \Egorov theorem asserts that, if a sequence of functions converges almost everywhere to a limit, then the convergence is uniform on a subset of close to full measure. The first step in the proof is the following lemma, often useful by itself, asserting the same result for predicates: if a property $P_n x$ is eventually true for almost every $x$, then there exists $N$ such that $P_n x$ is true for all $n\geq N$ and all $x$ in a set of close to full measure. \ lemma (in finite_measure) Egorov_lemma: assumes [measurable]: "\n. (P n) \ measurable M (count_space UNIV)" and "AE x in M. eventually (\n. P n x) sequentially" "epsilon > 0" shows "\U N. U \ sets M \ (\n \ N. \x \ U. P n x) \ emeasure M (space M - U) < epsilon" proof - define K where "K = (\n. {x \ space M. \k\n. \(P k x)})" have [measurable]: "K n \ sets M" for n unfolding K_def by auto have "x \ (\n. K n)" if "eventually (\n. P n x) sequentially" for x unfolding K_def using that unfolding K_def eventually_sequentially by auto then have "AE x in M. x \ (\n. K n)" using assms by auto then have Z: "0 = emeasure M (\n. K n)" using AE_iff_measurable[of "(\n. K n)" M "\x. x \ (\n. K n)"] unfolding K_def by auto have *: "(\n. emeasure M (K n)) \ 0" unfolding Z apply (rule Lim_emeasure_decseq) using order_trans by (auto simp add: K_def decseq_def) have "eventually (\n. emeasure M (K n) < epsilon) sequentially" by (rule order_tendstoD(2)[OF * \epsilon > 0\]) then obtain N where N: "\n. n \ N \ emeasure M (K n) < epsilon" unfolding eventually_sequentially by auto define U where "U = space M - K N" have A [measurable]: "U \ sets M" unfolding U_def by auto have "space M - U = K N" unfolding U_def K_def by auto then have B: "emeasure M (space M - U) < epsilon" using N by auto have "\n \ N. \x \ U. P n x" unfolding U_def K_def by auto then show ?thesis using A B by blast qed text \The next lemma asserts that, in an uncountable family of disjoint sets, then there is one set with zero measure (and in fact uncountably many). It is often applied to the boundaries of $r$-neighborhoods of a given set, to show that one could choose $r$ for which this boundary has  sgouezel committed Mar 17, 2018 821 zero measure (this shows up often in relation with weak convergence).\  sgouezel committed Mar 14, 2018 822 823 824 825 826 827 828 829 830 831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848 849 850 851 852 853 854 855 856 857 858 859 860 861 862 863 864 865 866 867  lemma (in finite_measure) uncountable_disjoint_family_then_exists_zero_measure: assumes [measurable]: "\i. i \ I \ A i \ sets M" and "uncountable I" "disjoint_family_on A I" shows "\i\I. measure M (A i) = 0" proof - define f where "f = (\(r::real). {i \ I. measure M (A i) > r})" have *: "finite (f r)" if "r > 0" for r proof - obtain N::nat where N: "measure M (space M)/r \ N" using real_arch_simple by blast have "finite (f r) \ card (f r) \ N" proof (rule finite_if_finite_subsets_card_bdd) fix G assume G: "G \ f r" "finite G" then have "G \ I" unfolding f_def by auto have "card G * r = (\i \ G. r)" by auto also have "... \ (\i \ G. measure M (A i))" apply (rule sum_mono) using G unfolding f_def by auto also have "... = measure M (\i\G. A i)" apply (rule finite_measure_finite_Union[symmetric]) using \finite G\ \G \ I\ \disjoint_family_on A I\ disjoint_family_on_mono by auto also have "... \ measure M (space M)" by (simp add: bounded_measure) finally have "card G \ measure M (space M)/r" using \r > 0\ by (simp add: divide_simps) then show "card G \ N" using N by auto qed then show ?thesis by simp qed have "countable (\n. f (((1::real)/2)^n))" by (rule countable_UN, auto intro!: countable_finite *) then have "I - (\n. f (((1::real)/2)^n)) \ {}" using assms(2) by (metis countable_empty uncountable_minus_countable) then obtain i where "i \ I" "i \ (\n. f ((1/2)^n))" by auto then have "measure M (A i) \ (1 / 2) ^ n" for n unfolding f_def using linorder_not_le by auto moreover have "(\n. ((1::real) / 2) ^ n) \ 0" by (intro tendsto_intros, auto) ultimately have "measure M (A i) \ 0" using LIMSEQ_le_const by force then have "measure M (A i) = 0" by (simp add: measure_le_0_iff) then show ?thesis using \i \ I\ by auto qed  sgouezel committed Mar 20, 2017 868 869 870 871 872 873 874 875 876 877 878 879 880 text \The next statements are useful measurability statements.\ lemma measurable_Inf [measurable]: assumes [measurable]: "\(n::nat). P n \ measurable M (count_space UNIV)" shows "(\x. Inf {n. P n x}) \ measurable M (count_space UNIV)" (is "?f \ _") proof - define A where "A = (\n. (P n)-{True} \ space M - (\m space M))" have A_meas [measurable]: "A n \ sets M" for n unfolding A_def by measurable define B where "B = (\n. if n = 0 then (space M - (\n. A n)) else A (n-1))" show ?thesis proof (rule measurable_piecewise_restrict2[of B]) show "B n \ sets M" for n unfolding B_def by simp show "space M = (\n. B n)"  haftmann committed Jan 31, 2019 881  unfolding B_def using sets.sets_into_space [OF A_meas] by auto  sgouezel committed Mar 20, 2017 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906 907 908  have *: "?f x = n" if "x \ A n" for x n apply (rule cInf_eq_minimum) using that unfolding A_def by auto moreover have **: "?f x = (Inf ({}::nat set))" if "x \ space M - (\n. A n)" for x proof - have "\(P n x)" for n apply (induction n rule: nat_less_induct) using that unfolding A_def by auto then show ?thesis by simp qed ultimately have "\c. \x \ B n. ?f x = c" for n apply (cases "n = 0") unfolding B_def by auto then show "\h \ measurable M (count_space UNIV). \x \ B n. ?f x = h x" for n by fastforce qed qed lemma measurable_T_iter [measurable]: fixes f::"'a \ nat" assumes [measurable]: "T \ measurable M M" "f \ measurable M (count_space UNIV)" shows "(\x. (T^^(f x)) x) \ measurable M M" proof - have [measurable]: "(T^^n) \ measurable M M" for n::nat by (induction n, auto) show ?thesis by (rule measurable_compose_countable, auto) qed  sgouezel committed Mar 14, 2018 909 910 lemma measurable_infdist [measurable]: "(\x. infdist x S) \ borel_measurable borel"  Lawrence Paulson committed Jul 17, 2019 911 by (rule borel_measurable_continuous_onI, intro continuous_intros)  sgouezel committed Mar 14, 2018 912 913 914 915 916 917 918 919 920 921 922 923 924 925 926 927 928 929 930 931 932  text \The next lemma shows that, in a sigma finite measure space, sets with large measure can be approximated by sets with large but finite measure.\ lemma (in sigma_finite_measure) approx_with_finite_emeasure: assumes W_meas: "W \ sets M" and W_inf: "emeasure M W > C" obtains Z where "Z \ sets M" "Z \ W" "emeasure M Z < \" "emeasure M Z > C" proof (cases "emeasure M W = \") case True obtain r where r: "C = ennreal r" using W_inf by (cases C, auto) obtain Z where "Z \ sets M" "Z \ W" "emeasure M Z < \" "emeasure M Z > C" unfolding r using approx_PInf_emeasure_with_finite[OF W_meas True, of r] by auto then show ?thesis using that by blast next case False then have "W \ sets M" "W \ W" "emeasure M W < \" "emeasure M W > C" using assms apply auto using top.not_eq_extremum by blast then show ?thesis using that by blast qed  sgouezel committed Mar 20, 2017 933 subsection \Nonnegative-Lebesgue-Integration.thy\  Lawrence Paulson committed Dec 01, 2015 934   sgouezel committed Mar 17, 2018 935 text \The next lemma is a variant of \verb+nn_integral_density+,  sgouezel committed Mar 20, 2017 936 with the density on the right instead of the left, as seems more common.\  Lawrence Paulson committed Dec 01, 2015 937 938  lemma nn_integral_densityR:  sgouezel committed Mar 14, 2018 939  assumes [measurable]: "f \ borel_measurable F" "g \ borel_measurable F"  Lawrence Paulson committed Dec 01, 2015 940 941 942 943  shows "(\\<^sup>+ x. f x * g x \F) = (\\<^sup>+ x. f x \(density F g))" proof - have "(\\<^sup>+ x. f x * g x \F) = (\\<^sup>+ x. g x * f x \F)" by (simp add: mult.commute) also have "... = (\\<^sup>+ x. f x \(density F g))"  sgouezel committed Feb 24, 2016 944  by (rule nn_integral_density[symmetric], simp_all add: assms)  Lawrence Paulson committed Dec 01, 2015 945 946 947  finally show ?thesis by simp qed  hoelzl committed Apr 14, 2016 948 949 950 lemma not_AE_zero_int_ennreal_E: fixes f::"'a \ ennreal" assumes "(\\<^sup>+x. f x \M) > 0"  sgouezel committed Aug 20, 2016 951 952  and [measurable]: "f \ borel_measurable M" shows "\A\sets M. \e::real>0. emeasure M A > 0 \ (\x \ A. f x \ e)"  hoelzl committed Apr 14, 2016 953 proof (rule not_AE_zero_ennreal_E, auto simp add: assms)  Lawrence Paulson committed Dec 01, 2015 954 955 956  assume *: "AE x in M. f x = 0" have "(\\<^sup>+x. f x \M) = (\\<^sup>+x. 0 \M)" by (rule nn_integral_cong_AE, simp add: *) then have "(\\<^sup>+x. f x \M) = 0" by simp  hoelzl committed Apr 14, 2016 957  then show False using assms by simp  Lawrence Paulson committed Dec 01, 2015 958 959 960 qed lemma (in finite_measure) nn_integral_bounded_eq_bound_then_AE:  sgouezel committed Aug 20, 2016 961 962  assumes "AE x in M. f x \ ennreal c" "(\\<^sup>+x. f x \M) = c * emeasure M (space M)" and [measurable]: "f \ borel_measurable M"  Lawrence Paulson committed Dec 01, 2015 963 964 965  shows "AE x in M. f x = c" proof (cases) assume "emeasure M (space M) = 0"  sgouezel committed Sep 30, 2016 966  then show ?thesis by (rule emeasure_0_AE)  Lawrence Paulson committed Dec 01, 2015 967 next  hoelzl committed Apr 14, 2016 968 969  assume "emeasure M (space M) \ 0" have fin: "AE x in M. f x \ top" using assms by (auto simp: top_unique)  sgouezel committed Aug 20, 2016 970  define g where "g = (\x. c - f x)"  Lawrence Paulson committed Dec 01, 2015 971 972  have [measurable]: "g \ borel_measurable M" unfolding g_def by auto have "(\\<^sup>+x. g x \M) = (\\<^sup>+x. c \M) - (\\<^sup>+x. f x \M)"  hoelzl committed Apr 14, 2016 973 974 975 976 977  unfolding g_def by (rule nn_integral_diff, auto simp add: assms ennreal_mult_eq_top_iff) also have "\ = 0" using assms(2) by (auto simp: ennreal_mult_eq_top_iff) finally have "AE x in M. g x = 0" by (subst nn_integral_0_iff_AE[symmetric]) auto then have "AE x in M. c \ f x" unfolding g_def using fin by (auto simp: ennreal_minus_eq_0)  Lawrence Paulson committed Dec 01, 2015 978 979 980 981  then show ?thesis using assms(1) by auto qed  sgouezel committed Mar 14, 2018 982 983 984 985 986 987 988 989 990 991 992 993 994 995 996 997 998 999 1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015 1016 1017 1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 lemma null_sets_density: assumes [measurable]: "h \ borel_measurable M" and "AE x in M. h x \ 0" shows "null_sets (density M h) = null_sets M" proof - have *: "A \ sets M \ (AE x\A in M. h x = 0) \ A \ null_sets M" for A proof (auto) assume "A \ sets M" "AE x\A in M. h x = 0" then show "A \ null_sets M" unfolding AE_iff_null_sets[OF \A \ sets M\] using assms(2) by auto next assume "A \ null_sets M" then show "AE x\A in M. h x = 0" by (metis (mono_tags, lifting) AE_not_in eventually_mono) qed show ?thesis apply (rule set_eqI) unfolding null_sets_density_iff[OF \h \ borel_measurable M\] using * by auto qed text \The next proposition asserts that, if a function $h$ is integrable, then its integral on any set with small enough measure is small. The good conceptual proof is by considering the distribution of the function $h$ on $\mathbb{R}$ and looking at its tails. However, there is a less conceptual but more direct proof, based on dominated convergence and a proof by contradiction. This is the proof we give below.\ proposition integrable_small_integral_on_small_sets: fixes h::"'a \ real" assumes [measurable]: "integrable M h" and "delta > 0" shows "\epsilon>(0::real). \U \ sets M. emeasure M U < epsilon \ abs (\x\U. h x \M) < delta" proof (rule ccontr) assume H: "\ (\epsilon>0. \U\sets M. emeasure M U < ennreal epsilon \ abs(set_lebesgue_integral M U h) < delta)" have "\f. \epsilon\{0<..}. f epsilon \sets M \ emeasure M (f epsilon) < ennreal epsilon \ \(abs(set_lebesgue_integral M (f epsilon) h) < delta)" apply (rule bchoice) using H by auto then obtain f::"real \ 'a set" where f: "\epsilon. epsilon > 0 \ f epsilon \sets M" "\epsilon. epsilon > 0 \ emeasure M (f epsilon) < ennreal epsilon" "\epsilon. epsilon > 0 \ \(abs(set_lebesgue_integral M (f epsilon) h) < delta)" by blast define A where "A = (\n::nat. f ((1/2)^n))" have [measurable]: "A n \ sets M" for n unfolding A_def using f(1) by auto have *: "emeasure M (A n) < ennreal ((1/2)^n)" for n unfolding A_def using f(2) by auto have Large: "\(abs(set_lebesgue_integral M (A n) h) < delta)" for n unfolding A_def using f(3) by auto have S: "summable (\n. Sigma_Algebra.measure M (A n))" apply (rule summable_comparison_test'[of "\n. (1/2)^n" 0]) apply (rule summable_geometric, auto) apply (subst ennreal_le_iff[symmetric], simp) using less_imp_le[OF *] by (metis * emeasure_eq_ennreal_measure top.extremum_strict) have "AE x in M. eventually (\n. x \ space M - A n) sequentially" apply (rule borel_cantelli_AE1, auto simp add: S) by (metis * top.extremum_strict top.not_eq_extremum) moreover have "(\n. indicator (A n) x * h x) \ 0" if "eventually (\n. x \ space M - A n) sequentially" for x proof - have "eventually (\n. indicator (A n) x * h x = 0) sequentially" apply (rule eventually_mono[OF that]) unfolding indicator_def by auto then show ?thesis  Lawrence Paulson committed Jul 17, 2019 1046  unfolding eventually_sequentially using lim_explicit by force  sgouezel committed Mar 14, 2018 1047 1048 1049 1050 1051 1052 1053 1054 1055 1056 1057 1058  qed ultimately have A: "AE x in M. ((\n. indicator (A n) x * h x) \ 0)" by auto have I: "integrable M (\x. abs(h x))" using \integrable M h\ by auto have L: "(\n. abs (\x. indicator (A n) x * h x \M)) \ abs (\x. 0 \M)" apply (intro tendsto_intros) apply (rule integral_dominated_convergence[OF _ _ I A]) unfolding indicator_def by auto have "eventually (\n. abs (\x. indicator (A n) x * h x \M) < delta) sequentially" apply (rule order_tendstoD[OF L]) using \delta > 0\ by auto then show False  Lawrence Paulson committed Apr 13, 2018 1059  using Large by (auto simp: set_lebesgue_integral_def)  sgouezel committed Mar 14, 2018 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072 1073 1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 qed text \We also give the version for nonnegative ennreal valued functions. It follows from the previous one.\ proposition small_nn_integral_on_small_sets: fixes h::"'a \ ennreal" assumes [measurable]: "h \ borel_measurable M" and "delta > (0::real)" "(\\<^sup>+x. h x \M) \ \" shows "\epsilon>(0::real). \U \ sets M. emeasure M U < epsilon \ (\\<^sup>+x\U. h x \M) < delta" proof - define f where "f = (\x. enn2real(h x))" have "AE x in M. h x \ \" using assms by (metis nn_integral_PInf_AE) then have *: "AE x in M. ennreal (f x) = h x" unfolding f_def using ennreal_enn2real_if by auto have **: "(\\<^sup>+x. ennreal (f x) \M) \ \" using nn_integral_cong_AE[OF *] assms by auto have [measurable]: "f \ borel_measurable M" unfolding f_def by auto have "integrable M f" apply (rule integrableI_nonneg) using assms * f_def ** apply auto using top.not_eq_extremum by blast obtain epsilon::real where H: "epsilon > 0" "\U. U \ sets M \ emeasure M U < epsilon \ abs(\x\U. f x \M) < delta" using integrable_small_integral_on_small_sets[OF \integrable M f\ \delta > 0\] by blast have "(\\<^sup>+x\U. h x \M) < delta" if [measurable]: "U \ sets M" "emeasure M U < epsilon" for U proof - have "(\\<^sup>+x. indicator U x * h x \M) = (\\<^sup>+x. ennreal(indicator U x * f x) \M)" apply (rule nn_integral_cong_AE) using * unfolding indicator_def by auto also have "... = ennreal (\x. indicator U x * f x \M)" apply (rule nn_integral_eq_integral) apply (rule Bochner_Integration.integrable_bound[OF \integrable M f\]) unfolding indicator_def f_def by auto also have "... < ennreal delta"  Lawrence Paulson committed Apr 13, 2018 1093  apply (rule ennreal_lessI) using H(2)[OF that] by (auto simp: set_lebesgue_integral_def)  sgouezel committed Mar 14, 2018 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108  finally show ?thesis by (auto simp add: mult.commute) qed then show ?thesis using \epsilon > 0\ by auto qed subsection \Probability-measure.thy\ text \The next lemmas ensure that, if sets have a probability close to $1$, then their intersection also does.\ lemma (in prob_space) sum_measure_le_measure_inter: assumes "A \ sets M" "B \ sets M" shows "prob A + prob B \ 1 + prob (A \ B)" proof - have "prob A + prob B = prob (A \ B) + prob (A \ B)"  Lawrence Paulson committed Sep 18, 2019 1109  by (simp add: assms fmeasurable_eq_sets measure_Un3)  sgouezel committed Mar 14, 2018 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125  also have "... \ 1 + prob (A \ B)" by auto finally show ?thesis by simp qed lemma (in prob_space) sum_measure_le_measure_inter3: assumes [measurable]: "A \ sets M" "B \ sets M" "C \ sets M" shows "prob A + prob B + prob C \ 2 + prob (A \ B \ C)" using sum_measure_le_measure_inter[of B C] sum_measure_le_measure_inter[of A "B \ C"] by (auto simp add: inf_assoc) lemma (in prob_space) sum_measure_le_measure_Inter: assumes [measurable]: "finite I" "I \ {}" "\i. i \ I \ A i \ sets M" shows "(\i\I. prob (A i)) \ real(card I) - 1 + prob (\i\I. A i)" using assms proof (induct I rule: finite_ne_induct) fix x F assume H: "finite F" "F \ {}" "x \ F"  haftmann committed Nov 18, 2018 1126  "((\i. i \ F \ A i \ events) \ (\i\F. prob (A i)) \ real (card F) - 1 + prob (\(A  F)))"  sgouezel committed Mar 14, 2018 1127 1128 1129 1130  and [measurable]: "(\i. i \ insert x F \ A i \ events)" have "(\x\F. A x) \ events" using \finite F\ \F \ {}\ by auto have "(\i\insert x F. prob (A i)) = (\i\F. prob (A i)) + prob (A x)" using H(1) H(3) by auto  haftmann committed Nov 18, 2018 1131  also have "... \ real (card F)-1 + prob (\(A  F)) + prob (A x)"  sgouezel committed Mar 14, 2018 1132  using H(4) by auto  haftmann committed Nov 18, 2018 1133  also have "... \ real (card F) + prob ((\(A  F)) \ A x)"  sgouezel committed Mar 14, 2018 1134  using sum_measure_le_measure_inter[OF \(\x\F. A x) \ events\, of "A x"] by auto  haftmann committed Nov 18, 2018 1135  also have "... = real (card (insert x F)) - 1 + prob (\(A  (insert x F)))"  sgouezel committed Mar 14, 2018 1136  using H(1) H(2) unfolding card_insert_disjoint[OF \finite F\ \x \ F\] by (simp add: inf_commute)  haftmann committed Nov 18, 2018 1137  finally show "(\i\insert x F. prob (A i)) \ real (card (insert x F)) - 1 + prob (\(A  (insert x F)))"  sgouezel committed Mar 14, 2018 1138 1139 1140 1141 1142 1143 1144 1145 1146 1147 1148 1149 1150 1151 1152 1153 1154 1155 1156 1157 1158 1159 1160 1161 1162 1163 1164 1165 1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184 1185 1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204 1205 1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246 1247 1248 1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263 1264 1265 1266 1267 1268 1269 1270 1271 1272 1273 1274 1275 1276 1277 1278 1279 1280 1281 1282 1283 1284 1285 1286 1287 1288 1289 1290 1291 1292 1293 1294 1295 1296 1297 1298 1299 1300 1301 1302 1303 1304 1305 1306 1307 1308 1309 1310 1311 1312 1313 1314 1315 1316 1317 1318 1319  by simp qed (auto) text \A random variable gives a small mass to small neighborhoods of infinity.\ lemma (in prob_space) random_variable_small_tails: assumes "alpha > 0" and [measurable]: "f \ borel_measurable M" shows "\(C::real). prob {x \ space M. abs(f x) \ C} < alpha \ C \ K" proof - have *: "(\(n::nat). {x\space M. abs(f x) \ n}) = {}" apply auto by (metis real_arch_simple add.right_neutral add_mono_thms_linordered_field(4) not_less zero_less_one) have **: "(\n. prob {x \ space M. abs(f x) \ n}) \ prob (\(n::nat). {x \ space M. abs(f x) \ n})" by (rule finite_Lim_measure_decseq, auto simp add: decseq_def) have "eventually (\n. prob {x \ space M. abs(f x) \ n} < alpha) sequentially" apply (rule order_tendstoD[OF _ \alpha > 0\]) using ** unfolding * by auto then obtain N::nat where N: "\n::nat. n \ N \ prob {x \ space M. abs(f x) \ n} < alpha" unfolding eventually_sequentially by blast have "\n::nat. n \ N \ n \ K" by (meson le_cases of_nat_le_iff order.trans real_arch_simple) then obtain n::nat where n: "n \ N" "n \ K" by blast show ?thesis apply (rule exI[of _ "of_nat n"]) using N n by auto qed subsection \Distribution-functions.thy\ text \There is a locale called \verb+finite_borel_measure+ in \verb+distribution-functions.thy+. However, it only deals with real measures, and real weak convergence. I will not need the weak convergence in more general settings, but still it seems more natural to me to do the proofs in the natural settings. Let me introduce the locale \verb+finite_borel_measure'+ for this, although it would be better to rename the locale in the library file.\ locale finite_borel_measure' = finite_measure M for M :: "('a::metric_space) measure" + assumes M_is_borel [simp, measurable_cong]: "sets M = sets borel" begin lemma space_eq_univ [simp]: "space M = UNIV" using M_is_borel[THEN sets_eq_imp_space_eq] by simp lemma measurable_finite_borel [simp]: "f \ borel_measurable borel \ f \ borel_measurable M" by (rule borel_measurable_subalgebra[where N = borel]) auto text \Any closed set can be slightly enlarged to obtain a set whose boundary has $0$ measure.\ lemma approx_closed_set_with_set_zero_measure_boundary: assumes "closed S" "epsilon > 0" "S \ {}" shows "\r. r < epsilon \ r > 0 \ measure M {x. infdist x S = r} = 0 \ measure M {x. infdist x S \ r} < measure M S + epsilon" proof - have [measurable]: "S \ sets M" using \closed S\ by auto define T where "T = (\r. {x. infdist x S \ r})" have [measurable]: "T r \ sets borel" for r unfolding T_def by measurable have *: "(\n. T ((1/2)^n)) = S" unfolding T_def proof (auto) fix x assume *: "\n. infdist x S \ (1 / 2) ^n" have "infdist x S \ 0" apply (rule LIMSEQ_le_const[of "\n. (1/2)^n"], intro tendsto_intros) using * by auto then show "x \ S" using assms infdist_pos_not_in_closed by fastforce qed have A: "((1::real)/2)^n \ (1/2)^m" if "m \ n" for m n::nat using that by (simp add: power_decreasing) have "(\n. measure M (T ((1/2)^n))) \ measure M S" unfolding *[symmetric] apply (rule finite_Lim_measure_decseq, auto simp add: T_def decseq_def) using A order.trans by blast then have B: "eventually (\n. measure M (T ((1/2)^n)) < measure M S + epsilon) sequentially" apply (rule order_tendstoD) using \epsilon > 0\ by simp have C: "eventually (\n. (1/2)^n < epsilon) sequentially" by (rule order_tendstoD[OF _ \epsilon > 0\], intro tendsto_intros, auto) obtain n where n: "(1/2)^n < epsilon" "measure M (T ((1/2)^n)) < measure M S + epsilon" using eventually_conj[OF B C] unfolding eventually_sequentially by auto have "\r\{0<..<(1/2)^n}. measure M {x. infdist x S = r} = 0" apply (rule uncountable_disjoint_family_then_exists_zero_measure, auto simp add: disjoint_family_on_def) using uncountable_open_interval by fastforce then obtain r where r: "r\{0<..<(1/2)^n}" "measure M {x. infdist x S = r} = 0" by blast then have r2: "r > 0" "r < epsilon" using n by auto have "measure M {x. infdist x S \ r} \ measure M {x. infdist x S \ (1/2)^n}" apply (rule finite_measure_mono) using r by auto then have "measure M {x. infdist x S \ r} < measure M S + epsilon" using n(2) unfolding T_def by auto then show ?thesis using r(2) r2 by auto qed end (* of locale finite_borel_measure'*) sublocale finite_borel_measure \ finite_borel_measure' by (standard, simp add: M_is_borel) subsection \Weak-convergence.thy\ text \Since weak convergence is not implemented as a topology, the fact that the convergence of a sequence implies the convergence of a subsequence is not automatic. We prove it in the lemma below..\ lemma weak_conv_m_subseq: assumes "weak_conv_m M_seq M" "strict_mono r" shows "weak_conv_m (\n. M_seq (r n)) M" using assms LIMSEQ_subseq_LIMSEQ unfolding weak_conv_m_def weak_conv_def comp_def by auto context fixes \ :: "nat \ real measure" and M :: "real measure" assumes \: "\n. real_distribution (\ n)" assumes M: "real_distribution M" assumes \_to_M: "weak_conv_m \ M" begin text \The measure of a closed set behaves upper semicontinuously with respect to weak convergence: if $\mu_n \to \mu$, then $\limsup \mu_n(F) \leq \mu(F)$ (and the inequality can be strict, think of the situation where $\mu$ is a Dirac mass at $0$ and $F = \{0\}$, but $\mu_n$ has a density so that $\mu_n(\{0\}) = 0$).\ lemma closed_set_weak_conv_usc: assumes "closed S" "measure M S < l" shows "eventually (\n. measure (\ n) S < l) sequentially" proof (cases "S = {}") case True then show ?thesis using \measure M S < l\ by auto next case False interpret real_distribution M using M by simp define epsilon where "epsilon = l - measure M S" have "epsilon > 0" unfolding epsilon_def using assms(2) by auto obtain r where r: "r > 0" "r < epsilon" "measure M {x. infdist x S = r} = 0" "measure M {x. infdist x S \ r} < measure M S + epsilon" using approx_closed_set_with_set_zero_measure_boundary[OF \closed S\ \epsilon > 0\ \S \ {}\] by blast define T where "T = {x. infdist x S \ r}" have [measurable]: "T \ sets borel" unfolding T_def by auto have "S \ T" unfolding T_def using \closed S\ \r > 0\ by auto have "measure M T < l" using r(4) unfolding T_def epsilon_def by auto have "measure M (frontier T) \ measure M {x. infdist x S = r}" apply (rule finite_measure_mono) unfolding T_def using frontier_indist_le by auto then have "measure M (frontier T) = 0" using \measure M {x. infdist x S = r} = 0\ by (auto simp add: measure_le_0_iff) then have "(\n. measure (\ n) T) \ measure M T" using \_to_M by (simp add: \ emeasure_eq_measure real_distribution_axioms weak_conv_imp_continuity_set_conv) then have *: "eventually (\n. measure (\ n) T < l) sequentially" apply (rule order_tendstoD) using \measure M T < l\ by simp have **: "measure (\ n) S \ measure (\ n) T" for n apply (rule finite_measure.finite_measure_mono) using \ apply (simp add: finite_borel_measure.axioms(1) real_distribution.finite_borel_measure_M) using \S \ T\ apply simp by (simp add: \ real_distribution.events_eq_borel) show ?thesis apply (rule eventually_mono[OF *]) using ** le_less_trans by auto qed text \In the same way, the measure of an open set behaves lower semicontinuously with respect to weak convergence: if $\mu_n \to \mu$, then $\liminf \mu_n(U) \geq \mu(U)$ (and the inequality can be strict). This follows from the same statement for closed sets by passing to the complement.\ lemma open_set_weak_conv_lsc: assumes "open S" "measure M S > l" shows "eventually (\n. measure (\ n) S > l) sequentially" proof - interpret real_distribution M using M by auto have [measurable]: "S \ events" using assms(1) by auto have "eventually (\n. measure (\ n) (UNIV - S) < 1 - l) sequentially" apply (rule closed_set_weak_conv_usc) using assms prob_compl[of S] by auto moreover have "measure (\ n) (UNIV - S) = 1 - measure (\ n) S" for n proof - interpret mu: real_distribution "\ n" using \ by auto have "S \ mu.events" using assms(1) by auto then show ?thesis using mu.prob_compl[of S] by auto qed ultimately show ?thesis by auto qed end (*of context weak_conv_m*) end (*of SG_Library_Complement.thy*)