(* Author: Sébastien Gouëzel [email protected]
Author: Johannes Hölzl (TUM) -- ported to Limsup
License: BSD
*)
theory Essential_Supremum
imports "HOL-Analysis.Analysis"
begin
lemma ae_filter_eq_bot_iff: "ae_filter M = bot \ emeasure M (space M) = 0"
by (simp add: AE_iff_measurable trivial_limit_def)
section \<open>The essential supremum\<close>
text \<open>In this paragraph, we define the essential supremum and give its basic properties. The
essential supremum of a function is its maximum value if one is allowed to throw away a set
of measure $0$. It is convenient to define it to be infinity for non-measurable functions, as
it allows for neater statements in general. This is a prerequisiste to define the space $L^\infty$.\<close>
definition esssup::"'a measure \ ('a \ 'b::{second_countable_topology, dense_linorder, linorder_topology, complete_linorder}) \ 'b"
where "esssup M f = (if f \ borel_measurable M then Limsup (ae_filter M) f else top)"
lemma esssup_non_measurable: "f \ M \\<^sub>M borel \ esssup M f = top"
by (simp add: esssup_def)
lemma esssup_eq_AE:
assumes f: "f \ M \\<^sub>M borel" shows "esssup M f = Inf {z. AE x in M. f x \ z}"
unfolding esssup_def if_P[OF f] Limsup_def
proof (intro antisym INF_greatest Inf_greatest; clarsimp)
fix y assume "AE x in M. f x \ y"
then have "(\x. f x \ y) \ {P. AE x in M. P x}"
by simp
then show "(INF P\{P. AE x in M. P x}. SUP x\Collect P. f x) \ y"
by (rule INF_lower2) (auto intro: SUP_least)
next
fix P assume P: "AE x in M. P x"
show "Inf {z. AE x in M. f x \ z} \ (SUP x\Collect P. f x)"
proof (rule Inf_lower; clarsimp)
show "AE x in M. f x \ (SUP x\Collect P. f x)"
using P by (auto elim: eventually_mono simp: SUP_upper)
qed
qed
lemma esssup_eq: "f \ M \\<^sub>M borel \ esssup M f = Inf {z. emeasure M {x \ space M. f x > z} = 0}"
by (auto simp add: esssup_eq_AE not_less[symmetric] AE_iff_measurable[OF _ refl] intro!: arg_cong[where f=Inf])
lemma esssup_zero_measure:
"emeasure M {x \ space M. f x > esssup M f} = 0"
proof (cases "esssup M f = top")
case True
then show ?thesis by auto
next
case False
then have f[measurable]: "f \ M \\<^sub>M borel" unfolding esssup_def by meson
have "esssup M f < top" using False by (auto simp: less_top)
have *: "{x \ space M. f x > z} \ null_sets M" if "z > esssup M f" for z
proof -
have "\w. w < z \ emeasure M {x \ space M. f x > w} = 0"
using \<open>z > esssup M f\<close> f by (auto simp: esssup_eq Inf_less_iff)
then obtain w where "w < z" "emeasure M {x \ space M. f x > w} = 0" by auto
then have a: "{x \ space M. f x > w} \ null_sets M" by auto
have b: "{x \ space M. f x > z} \ {x \ space M. f x > w}" using \w < z\ by auto
show ?thesis using null_sets_subset[OF a _ b] by simp
qed
obtain u::"nat \ 'b" where u: "\n. u n > esssup M f" "u \ esssup M f"
using approx_from_above_dense_linorder[OF \<open>esssup M f < top\<close>] by auto
have "{x \ space M. f x > esssup M f} = (\n. {x \ space M. f x > u n})"
using u apply auto
apply (metis (mono_tags, lifting) order_tendsto_iff eventually_mono LIMSEQ_unique)
using less_imp_le less_le_trans by blast
also have "... \ null_sets M"
using *[OF u(1)] by auto
finally show ?thesis by auto
qed
lemma esssup_AE: "AE x in M. f x \ esssup M f"
proof (cases "f \ M \\<^sub>M borel")
case True then show ?thesis
by (intro AE_I[OF _ esssup_zero_measure[of _ f]]) auto
qed (simp add: esssup_non_measurable)
lemma esssup_pos_measure:
"f \ borel_measurable M \ z < esssup M f \ emeasure M {x \ space M. f x > z} > 0"
using Inf_less_iff mem_Collect_eq not_gr_zero by (force simp: esssup_eq)
lemma esssup_I [intro]: "f \ borel_measurable M \ AE x in M. f x \ c \ esssup M f \ c"
unfolding esssup_def by (simp add: Limsup_bounded)
lemma esssup_AE_mono: "f \ borel_measurable M \ AE x in M. f x \ g x \ esssup M f \ esssup M g"
by (auto simp: esssup_def Limsup_mono)
lemma esssup_mono: "f \ borel_measurable M \ (\x. f x \ g x) \ esssup M f \ esssup M g"
by (rule esssup_AE_mono) auto
lemma esssup_AE_cong:
"f \ borel_measurable M \ g \ borel_measurable M \ AE x in M. f x = g x \ esssup M f = esssup M g"
by (auto simp: esssup_def intro!: Limsup_eq)
lemma esssup_const: "emeasure M (space M) \ 0 \ esssup M (\x. c) = c"
by (simp add: esssup_def Limsup_const ae_filter_eq_bot_iff)
lemma esssup_cmult: assumes "c > (0::real)" shows "esssup M (\x. c * f x::ereal) = c * esssup M f"
proof -
have "(\x. ereal c * f x) \ M \\<^sub>M borel \ f \ M \\<^sub>M borel"
proof (subst measurable_cong)
fix \<omega> show "f \<omega> = ereal (1/c) * (ereal c * f \<omega>)"
using \<open>0 < c\<close> by (cases "f \<omega>") auto
qed auto
then have "(\x. ereal c * f x) \ M \\<^sub>M borel \ f \ M \\<^sub>M borel"
by(safe intro!: borel_measurable_ereal_times borel_measurable_const)
with \<open>0<c\<close> show ?thesis
by (cases "ae_filter M = bot")
(auto simp: esssup_def bot_ereal_def top_ereal_def Limsup_ereal_mult_left)
qed
lemma esssup_add:
"esssup M (\x. f x + g x::ereal) \ esssup M f + esssup M g"
proof (cases "f \ borel_measurable M \ g \ borel_measurable M")
case True
then have [measurable]: "(\x. f x + g x) \ borel_measurable M" by auto
have "f x + g x \ esssup M f + esssup M g" if "f x \ esssup M f" "g x \ esssup M g" for x
using that add_mono by auto
then have "AE x in M. f x + g x \ esssup M f + esssup M g"
using esssup_AE[of f M] esssup_AE[of g M] by auto
then show ?thesis using esssup_I by auto
next
case False
then have "esssup M f + esssup M g = \" unfolding esssup_def top_ereal_def by auto
then show ?thesis by auto
qed
lemma esssup_zero_space:
"emeasure M (space M) = 0 \ f \ borel_measurable M \ esssup M f = (- \::ereal)"
by (simp add: esssup_def ae_filter_eq_bot_iff[symmetric] bot_ereal_def)
end
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
