src/HOL/Probability/Essential_Supremum.thy
author nipkow
Wed, 11 Jul 2018 11:16:26 +0200
changeset 68751 640386ab99f3
parent 67226 ec32cdaab97b
child 69260 0a9688695a1b
permissions -rw-r--r--
updated to renaming
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
     1
(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
     2
    Author:  Johannes Hölzl (TUM) -- ported to Limsup
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
     3
    License: BSD
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
     4
*)
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
     5
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
     6
theory Essential_Supremum
66453
cc19f7ca2ed6 session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents: 64333
diff changeset
     7
imports "HOL-Analysis.Analysis"
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
     8
begin
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
     9
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    10
lemma ae_filter_eq_bot_iff: "ae_filter M = bot \<longleftrightarrow> emeasure M (space M) = 0"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    11
  by (simp add: AE_iff_measurable trivial_limit_def)
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    12
67226
ec32cdaab97b isabelle update_cartouches -c -t;
wenzelm
parents: 66453
diff changeset
    13
section \<open>The essential supremum\<close>
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    14
67226
ec32cdaab97b isabelle update_cartouches -c -t;
wenzelm
parents: 66453
diff changeset
    15
text \<open>In this paragraph, we define the essential supremum and give its basic properties. The
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    16
essential supremum of a function is its maximum value if one is allowed to throw away a set
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    17
of measure $0$. It is convenient to define it to be infinity for non-measurable functions, as
67226
ec32cdaab97b isabelle update_cartouches -c -t;
wenzelm
parents: 66453
diff changeset
    18
it allows for neater statements in general. This is a prerequisiste to define the space $L^\infty$.\<close>
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    19
64319
a33bbac43359 HOL-Probability: generalize type of essential supremum
hoelzl
parents: 64293
diff changeset
    20
definition esssup::"'a measure \<Rightarrow> ('a \<Rightarrow> 'b::{second_countable_topology, dense_linorder, linorder_topology, complete_linorder}) \<Rightarrow> 'b"
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    21
  where "esssup M f = (if f \<in> borel_measurable M then Limsup (ae_filter M) f else top)"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    22
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    23
lemma esssup_non_measurable: "f \<notin> M \<rightarrow>\<^sub>M borel \<Longrightarrow> esssup M f = top"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    24
  by (simp add: esssup_def)
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    25
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    26
lemma esssup_eq_AE:
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    27
  assumes f: "f \<in> M \<rightarrow>\<^sub>M borel" shows "esssup M f = Inf {z. AE x in M. f x \<le> z}"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    28
  unfolding esssup_def if_P[OF f] Limsup_def
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    29
proof (intro antisym INF_greatest Inf_greatest; clarsimp)
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    30
  fix y assume "AE x in M. f x \<le> y"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    31
  then have "(\<lambda>x. f x \<le> y) \<in> {P. AE x in M. P x}"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    32
    by simp
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    33
  then show "(INF P:{P. AE x in M. P x}. SUP x:Collect P. f x) \<le> y"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    34
    by (rule INF_lower2) (auto intro: SUP_least)
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    35
next
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    36
  fix P assume P: "AE x in M. P x"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    37
  show "Inf {z. AE x in M. f x \<le> z} \<le> (SUP x:Collect P. f x)"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    38
  proof (rule Inf_lower; clarsimp)
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    39
    show "AE x in M. f x \<le> (SUP x:Collect P. f x)"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    40
      using P by (auto elim: eventually_mono simp: SUP_upper)
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    41
  qed
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    42
qed
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    43
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    44
lemma esssup_eq: "f \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> esssup M f = Inf {z. emeasure M {x \<in> space M. f x > z} = 0}"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    45
  by (auto simp add: esssup_eq_AE not_less[symmetric] AE_iff_measurable[OF _ refl] intro!: arg_cong[where f=Inf])
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    46
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    47
lemma esssup_zero_measure:
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    48
  "emeasure M {x \<in> space M. f x > esssup M f} = 0"
64319
a33bbac43359 HOL-Probability: generalize type of essential supremum
hoelzl
parents: 64293
diff changeset
    49
proof (cases "esssup M f = top")
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    50
  case True
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    51
  then show ?thesis by auto
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    52
next
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    53
  case False
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    54
  then have f[measurable]: "f \<in> M \<rightarrow>\<^sub>M borel" unfolding esssup_def by meson
64319
a33bbac43359 HOL-Probability: generalize type of essential supremum
hoelzl
parents: 64293
diff changeset
    55
  have "esssup M f < top" using False by (auto simp: less_top)
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    56
  have *: "{x \<in> space M. f x > z} \<in> null_sets M" if "z > esssup M f" for z
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    57
  proof -
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    58
    have "\<exists>w. w < z \<and> emeasure M {x \<in> space M. f x > w} = 0"
67226
ec32cdaab97b isabelle update_cartouches -c -t;
wenzelm
parents: 66453
diff changeset
    59
      using \<open>z > esssup M f\<close> f by (auto simp: esssup_eq Inf_less_iff)
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    60
    then obtain w where "w < z" "emeasure M {x \<in> space M. f x > w} = 0" by auto
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    61
    then have a: "{x \<in> space M. f x > w} \<in> null_sets M" by auto
67226
ec32cdaab97b isabelle update_cartouches -c -t;
wenzelm
parents: 66453
diff changeset
    62
    have b: "{x \<in> space M. f x > z} \<subseteq> {x \<in> space M. f x > w}" using \<open>w < z\<close> by auto
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    63
    show ?thesis using null_sets_subset[OF a _ b] by simp
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    64
  qed
64319
a33bbac43359 HOL-Probability: generalize type of essential supremum
hoelzl
parents: 64293
diff changeset
    65
  obtain u::"nat \<Rightarrow> 'b" where u: "\<And>n. u n > esssup M f" "u \<longlonglongrightarrow> esssup M f"
67226
ec32cdaab97b isabelle update_cartouches -c -t;
wenzelm
parents: 66453
diff changeset
    66
    using approx_from_above_dense_linorder[OF \<open>esssup M f < top\<close>] by auto
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    67
  have "{x \<in> space M. f x > esssup M f} = (\<Union>n. {x \<in> space M. f x > u n})"
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    68
    using u apply auto
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    69
    apply (metis (mono_tags, lifting) order_tendsto_iff eventually_mono LIMSEQ_unique)
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    70
    using less_imp_le less_le_trans by blast
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    71
  also have "... \<in> null_sets M"
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    72
    using *[OF u(1)] by auto
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    73
  finally show ?thesis by auto
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    74
qed
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    75
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    76
lemma esssup_AE: "AE x in M. f x \<le> esssup M f"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    77
proof (cases "f \<in> M \<rightarrow>\<^sub>M borel")
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    78
  case True then show ?thesis
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    79
    by (intro AE_I[OF _ esssup_zero_measure[of _ f]]) auto
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    80
qed (simp add: esssup_non_measurable)
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    81
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    82
lemma esssup_pos_measure:
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    83
  "f \<in> borel_measurable M \<Longrightarrow> z < esssup M f \<Longrightarrow> emeasure M {x \<in> space M. f x > z} > 0"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    84
  using Inf_less_iff mem_Collect_eq not_gr_zero by (force simp: esssup_eq)
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    85
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    86
lemma esssup_I [intro]: "f \<in> borel_measurable M \<Longrightarrow> AE x in M. f x \<le> c \<Longrightarrow> esssup M f \<le> c"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    87
  unfolding esssup_def by (simp add: Limsup_bounded)
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    88
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    89
lemma esssup_AE_mono: "f \<in> borel_measurable M \<Longrightarrow> AE x in M. f x \<le> g x \<Longrightarrow> esssup M f \<le> esssup M g"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    90
  by (auto simp: esssup_def Limsup_mono)
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    91
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    92
lemma esssup_mono: "f \<in> borel_measurable M \<Longrightarrow> (\<And>x. f x \<le> g x) \<Longrightarrow> esssup M f \<le> esssup M g"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    93
  by (rule esssup_AE_mono) auto
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    94
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    95
lemma esssup_AE_cong:
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    96
  "f \<in> borel_measurable M \<Longrightarrow> g \<in> borel_measurable M \<Longrightarrow> AE x in M. f x = g x \<Longrightarrow> esssup M f = esssup M g"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    97
  by (auto simp: esssup_def intro!: Limsup_eq)
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
    98
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
    99
lemma esssup_const: "emeasure M (space M) \<noteq> 0 \<Longrightarrow> esssup M (\<lambda>x. c) = c"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   100
  by (simp add: esssup_def Limsup_const ae_filter_eq_bot_iff)
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   101
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   102
lemma esssup_cmult: assumes "c > (0::real)" shows "esssup M (\<lambda>x. c * f x::ereal) = c * esssup M f"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   103
proof -
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   104
  have "(\<lambda>x. ereal c * f x) \<in> M \<rightarrow>\<^sub>M borel \<Longrightarrow> f \<in> M \<rightarrow>\<^sub>M borel"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   105
  proof (subst measurable_cong)
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   106
    fix \<omega> show "f \<omega> = ereal (1/c) * (ereal c * f \<omega>)"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   107
      using \<open>0 < c\<close> by (cases "f \<omega>") auto
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   108
  qed auto
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   109
  then have "(\<lambda>x. ereal c * f x) \<in> M \<rightarrow>\<^sub>M borel \<longleftrightarrow> f \<in> M \<rightarrow>\<^sub>M borel"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   110
    by(safe intro!: borel_measurable_ereal_times borel_measurable_const)
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   111
  with \<open>0<c\<close> show ?thesis
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   112
    by (cases "ae_filter M = bot")
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   113
       (auto simp: esssup_def bot_ereal_def top_ereal_def Limsup_ereal_mult_left)
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   114
qed
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   115
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   116
lemma esssup_add:
64319
a33bbac43359 HOL-Probability: generalize type of essential supremum
hoelzl
parents: 64293
diff changeset
   117
  "esssup M (\<lambda>x. f x + g x::ereal) \<le> esssup M f + esssup M g"
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   118
proof (cases "f \<in> borel_measurable M \<and> g \<in> borel_measurable M")
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   119
  case True
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   120
  then have [measurable]: "(\<lambda>x. f x + g x) \<in> borel_measurable M" by auto
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   121
  have "f x + g x \<le> esssup M f + esssup M g" if "f x \<le> esssup M f" "g x \<le> esssup M g" for x
68751
640386ab99f3 updated to renaming
nipkow
parents: 67226
diff changeset
   122
    using that add_mono by auto
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   123
  then have "AE x in M. f x + g x \<le> esssup M f + esssup M g"
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   124
    using esssup_AE[of f M] esssup_AE[of g M] by auto
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   125
  then show ?thesis using esssup_I by auto
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   126
next
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   127
  case False
64319
a33bbac43359 HOL-Probability: generalize type of essential supremum
hoelzl
parents: 64293
diff changeset
   128
  then have "esssup M f + esssup M g = \<infinity>" unfolding esssup_def top_ereal_def by auto
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   129
  then show ?thesis by auto
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   130
qed
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   131
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   132
lemma esssup_zero_space:
64333
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   133
  "emeasure M (space M) = 0 \<Longrightarrow> f \<in> borel_measurable M \<Longrightarrow> esssup M f = (- \<infinity>::ereal)"
692a1b317316 HOL-Probability: Essential Supremum as Limsup over ae_filter
hoelzl
parents: 64319
diff changeset
   134
  by (simp add: esssup_def ae_filter_eq_bot_iff[symmetric] bot_ereal_def)
64293
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   135
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   136
end
256298544491 add missing file Essential_Supremum.thy
hoelzl
parents:
diff changeset
   137