Quelle  Essential_Supremum.thy

(*  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 ‹The essential supremum›

text ‹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$.›

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 →🪙M borel ==> esssup M f = top"
  by (simp add: esssup_def)

lemma esssup_eq_AE:
  assumes f: "f ∈ M →🪙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 →🪙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 →🪙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 ‹z > esssup M f› 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 🚫› 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 ‹esssup M f 🚫›] 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 →🪙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 →🪙M borel ==> f ∈ M →🪙M borel"
  proof (subst measurable_cong)
    fix ψ show "f ψ = ereal (1/c) * (ereal c * f ψ)"
      using ‹0 🚫› by (cases "f ψ") auto
  qed auto
  then have "(λx. ereal c * f x) ∈ M →🪙M borel ⟷ f ∈ M →🪙M borel"
    by(safe intro!: borel_measurable_ereal_times borel_measurable_const)
  with ‹0🚫› 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