Quelle Essential_Supremum.thy Sprache: Isabelle

(*  Author:  Sébastien Gouëzel   sebastien.gouezel@univ-rennes1.fr
    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

quality100%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.