Theory Extended_Real_Limits

theory Extended_Real_Limits
imports Topology_Euclidean_Space Extended_Real Indicator_Function
(*  Title:      HOL/Multivariate_Analysis/Extended_Real_Limits.thy
    Author:     Johannes Hölzl, TU München
    Author:     Robert Himmelmann, TU München
    Author:     Armin Heller, TU München
    Author:     Bogdan Grechuk, University of Edinburgh
*)

header {* Limits on the Extended real number line *}

theory Extended_Real_Limits
  imports Topology_Euclidean_Space "~~/src/HOL/Library/Extended_Real" "~~/src/HOL/Library/Indicator_Function"
begin

lemma convergent_limsup_cl:
  fixes X :: "nat => 'a::{complete_linorder,linorder_topology}"
  shows "convergent X ==> limsup X = lim X"
  by (auto simp: convergent_def limI lim_imp_Limsup)

lemma lim_increasing_cl:
  assumes "!!n m. n ≥ m ==> f n ≥ f m"
  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
proof
  show "f ----> (SUP n. f n)"
    using assms
    by (intro increasing_tendsto)
       (auto simp: SUP_upper eventually_sequentially less_SUP_iff intro: less_le_trans)
qed

lemma lim_decreasing_cl:
  assumes "!!n m. n ≥ m ==> f n ≤ f m"
  obtains l where "f ----> (l::'a::{complete_linorder,linorder_topology})"
proof
  show "f ----> (INF n. f n)"
    using assms
    by (intro decreasing_tendsto)
       (auto simp: INF_lower eventually_sequentially INF_less_iff intro: le_less_trans)
qed

lemma compact_complete_linorder:
  fixes X :: "nat => 'a::{complete_linorder,linorder_topology}"
  shows "∃l r. subseq r ∧ (X o r) ----> l"
proof -
  obtain r where "subseq r" and mono: "monoseq (X o r)"
    using seq_monosub[of X]
    unfolding comp_def
    by auto
  then have "(∀n m. m ≤ n --> (X o r) m ≤ (X o r) n) ∨ (∀n m. m ≤ n --> (X o r) n ≤ (X o r) m)"
    by (auto simp add: monoseq_def)
  then obtain l where "(X o r) ----> l"
     using lim_increasing_cl[of "X o r"] lim_decreasing_cl[of "X o r"]
     by auto
  then show ?thesis
    using `subseq r` by auto
qed

lemma compact_UNIV:
  "compact (UNIV :: 'a::{complete_linorder,linorder_topology,second_countable_topology} set)"
  using compact_complete_linorder
  by (auto simp: seq_compact_eq_compact[symmetric] seq_compact_def)

lemma compact_eq_closed:
  fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
  shows "compact S <-> closed S"
  using closed_inter_compact[of S, OF _ compact_UNIV] compact_imp_closed
  by auto

lemma closed_contains_Sup_cl:
  fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
  assumes "closed S"
    and "S ≠ {}"
  shows "Sup S ∈ S"
proof -
  from compact_eq_closed[of S] compact_attains_sup[of S] assms
  obtain s where S: "s ∈ S" "∀t∈S. t ≤ s"
    by auto
  then have "Sup S = s"
    by (auto intro!: Sup_eqI)
  with S show ?thesis
    by simp
qed

lemma closed_contains_Inf_cl:
  fixes S :: "'a::{complete_linorder,linorder_topology,second_countable_topology} set"
  assumes "closed S"
    and "S ≠ {}"
  shows "Inf S ∈ S"
proof -
  from compact_eq_closed[of S] compact_attains_inf[of S] assms
  obtain s where S: "s ∈ S" "∀t∈S. s ≤ t"
    by auto
  then have "Inf S = s"
    by (auto intro!: Inf_eqI)
  with S show ?thesis
    by simp
qed

lemma ereal_dense3:
  fixes x y :: ereal
  shows "x < y ==> ∃r::rat. x < real_of_rat r ∧ real_of_rat r < y"
proof (cases x y rule: ereal2_cases, simp_all)
  fix r q :: real
  assume "r < q"
  from Rats_dense_in_real[OF this] show "∃x. r < real_of_rat x ∧ real_of_rat x < q"
    by (fastforce simp: Rats_def)
next
  fix r :: real
  show "∃x. r < real_of_rat x" "∃x. real_of_rat x < r"
    using gt_ex[of r] lt_ex[of r] Rats_dense_in_real
    by (auto simp: Rats_def)
qed

instance ereal :: second_countable_topology
proof (default, intro exI conjI)
  let ?B = "(\<Union>r∈\<rat>. {{..< r}, {r <..}} :: ereal set set)"
  show "countable ?B"
    by (auto intro: countable_rat)
  show "open = generate_topology ?B"
  proof (intro ext iffI)
    fix S :: "ereal set"
    assume "open S"
    then show "generate_topology ?B S"
      unfolding open_generated_order
    proof induct
      case (Basis b)
      then obtain e where "b = {..<e} ∨ b = {e<..}"
        by auto
      moreover have "{..<e} = \<Union>{{..<x}|x. x ∈ \<rat> ∧ x < e}" "{e<..} = \<Union>{{x<..}|x. x ∈ \<rat> ∧ e < x}"
        by (auto dest: ereal_dense3
                 simp del: ex_simps
                 simp add: ex_simps[symmetric] conj_commute Rats_def image_iff)
      ultimately show ?case
        by (auto intro: generate_topology.intros)
    qed (auto intro: generate_topology.intros)
  next
    fix S
    assume "generate_topology ?B S"
    then show "open S"
      by induct auto
  qed
qed

lemma continuous_on_ereal[intro, simp]: "continuous_on A ereal"
  unfolding continuous_on_topological open_ereal_def
  by auto

lemma continuous_at_ereal[intro, simp]: "continuous (at x) ereal"
  using continuous_on_eq_continuous_at[of UNIV]
  by auto

lemma continuous_within_ereal[intro, simp]: "x ∈ A ==> continuous (at x within A) ereal"
  using continuous_on_eq_continuous_within[of A]
  by auto

lemma ereal_open_uminus:
  fixes S :: "ereal set"
  assumes "open S"
  shows "open (uminus ` S)"
  using `open S`[unfolded open_generated_order]
proof induct
  have "range uminus = (UNIV :: ereal set)"
    by (auto simp: image_iff ereal_uminus_eq_reorder)
  then show "open (range uminus :: ereal set)"
    by simp
qed (auto simp add: image_Union image_Int)

lemma ereal_uminus_complement:
  fixes S :: "ereal set"
  shows "uminus ` (- S) = - uminus ` S"
  by (auto intro!: bij_image_Compl_eq surjI[of _ uminus] simp: bij_betw_def)

lemma ereal_closed_uminus:
  fixes S :: "ereal set"
  assumes "closed S"
  shows "closed (uminus ` S)"
  using assms
  unfolding closed_def ereal_uminus_complement[symmetric]
  by (rule ereal_open_uminus)

lemma ereal_open_closed_aux:
  fixes S :: "ereal set"
  assumes "open S"
    and "closed S"
    and S: "(-∞) ∉ S"
  shows "S = {}"
proof (rule ccontr)
  assume "¬ ?thesis"
  then have *: "Inf S ∈ S"
    by (metis assms(2) closed_contains_Inf_cl)
  {
    assume "Inf S = -∞"
    then have False
      using * assms(3) by auto
  }
  moreover
  {
    assume "Inf S = ∞"
    then have "S = {∞}"
      by (metis Inf_eq_PInfty `S ≠ {}`)
    then have False
      by (metis assms(1) not_open_singleton)
  }
  moreover
  {
    assume fin: "¦Inf S¦ ≠ ∞"
    from ereal_open_cont_interval[OF assms(1) * fin]
    obtain e where e: "e > 0" "{Inf S - e<..<Inf S + e} ⊆ S" .
    then obtain b where b: "Inf S - e < b" "b < Inf S"
      using fin ereal_between[of "Inf S" e] dense[of "Inf S - e"]
      by auto
    then have "b: {Inf S - e <..< Inf S + e}"
      using e fin ereal_between[of "Inf S" e]
      by auto
    then have "b ∈ S"
      using e by auto
    then have False
      using b by (metis complete_lattice_class.Inf_lower leD)
  }
  ultimately show False
    by auto
qed

lemma ereal_open_closed:
  fixes S :: "ereal set"
  shows "open S ∧ closed S <-> S = {} ∨ S = UNIV"
proof -
  {
    assume lhs: "open S ∧ closed S"
    {
      assume "-∞ ∉ S"
      then have "S = {}"
        using lhs ereal_open_closed_aux by auto
    }
    moreover
    {
      assume "-∞ ∈ S"
      then have "- S = {}"
        using lhs ereal_open_closed_aux[of "-S"] by auto
    }
    ultimately have "S = {} ∨ S = UNIV"
      by auto
  }
  then show ?thesis
    by auto
qed

lemma ereal_open_affinity_pos:
  fixes S :: "ereal set"
  assumes "open S"
    and m: "m ≠ ∞" "0 < m"
    and t: "¦t¦ ≠ ∞"
  shows "open ((λx. m * x + t) ` S)"
proof -
  obtain r where r[simp]: "m = ereal r"
    using m by (cases m) auto
  obtain p where p[simp]: "t = ereal p"
    using t by auto
  have "r ≠ 0" "0 < r" and m': "m ≠ ∞" "m ≠ -∞" "m ≠ 0"
    using m by auto
  from `open S` [THEN ereal_openE]
  obtain l u where T:
      "open (ereal -` S)"
      "∞ ∈ S ==> {ereal l<..} ⊆ S"
      "- ∞ ∈ S ==> {..<ereal u} ⊆ S"
    by blast
  let ?f = "(λx. m * x + t)"
  show ?thesis
    unfolding open_ereal_def
  proof (intro conjI impI exI subsetI)
    have "ereal -` ?f ` S = (λx. r * x + p) ` (ereal -` S)"
    proof safe
      fix x y
      assume "ereal y = m * x + t" "x ∈ S"
      then show "y ∈ (λx. r * x + p) ` ereal -` S"
        using `r ≠ 0` by (cases x) (auto intro!: image_eqI[of _ _ "real x"] split: split_if_asm)
    qed force
    then show "open (ereal -` ?f ` S)"
      using open_affinity[OF T(1) `r ≠ 0`]
      by (auto simp: ac_simps)
  next
    assume "∞ ∈ ?f`S"
    with `0 < r` have "∞ ∈ S"
      by auto
    fix x
    assume "x ∈ {ereal (r * l + p)<..}"
    then have [simp]: "ereal (r * l + p) < x"
      by auto
    show "x ∈ ?f`S"
    proof (rule image_eqI)
      show "x = m * ((x - t) / m) + t"
        using m t
        by (cases rule: ereal3_cases[of m x t]) auto
      have "ereal l < (x - t) / m"
        using m t
        by (simp add: ereal_less_divide_pos ereal_less_minus)
      then show "(x - t) / m ∈ S"
        using T(2)[OF `∞ ∈ S`] by auto
    qed
  next
    assume "-∞ ∈ ?f ` S"
    with `0 < r` have "-∞ ∈ S"
      by auto
    fix x assume "x ∈ {..<ereal (r * u + p)}"
    then have [simp]: "x < ereal (r * u + p)"
      by auto
    show "x ∈ ?f`S"
    proof (rule image_eqI)
      show "x = m * ((x - t) / m) + t"
        using m t
        by (cases rule: ereal3_cases[of m x t]) auto
      have "(x - t)/m < ereal u"
        using m t
        by (simp add: ereal_divide_less_pos ereal_minus_less)
      then show "(x - t)/m ∈ S"
        using T(3)[OF `-∞ ∈ S`]
        by auto
    qed
  qed
qed

lemma ereal_open_affinity:
  fixes S :: "ereal set"
  assumes "open S"
    and m: "¦m¦ ≠ ∞" "m ≠ 0"
    and t: "¦t¦ ≠ ∞"
  shows "open ((λx. m * x + t) ` S)"
proof cases
  assume "0 < m"
  then show ?thesis
    using ereal_open_affinity_pos[OF `open S` _ _ t, of m] m
    by auto
next
  assume "¬ 0 < m" then
  have "0 < -m"
    using `m ≠ 0`
    by (cases m) auto
  then have m: "-m ≠ ∞" "0 < -m"
    using `¦m¦ ≠ ∞`
    by (auto simp: ereal_uminus_eq_reorder)
  from ereal_open_affinity_pos[OF ereal_open_uminus[OF `open S`] m t] show ?thesis
    unfolding image_image by simp
qed

lemma ereal_lim_mult:
  fixes X :: "'a => ereal"
  assumes lim: "(X ---> L) net"
    and a: "¦a¦ ≠ ∞"
  shows "((λi. a * X i) ---> a * L) net"
proof cases
  assume "a ≠ 0"
  show ?thesis
  proof (rule topological_tendstoI)
    fix S
    assume "open S" and "a * L ∈ S"
    have "a * L / a = L"
      using `a ≠ 0` a
      by (cases rule: ereal2_cases[of a L]) auto
    then have L: "L ∈ ((λx. x / a) ` S)"
      using `a * L ∈ S`
      by (force simp: image_iff)
    moreover have "open ((λx. x / a) ` S)"
      using ereal_open_affinity[OF `open S`, of "inverse a" 0] `a ≠ 0` a
      by (auto simp: ereal_divide_eq ereal_inverse_eq_0 divide_ereal_def ac_simps)
    note * = lim[THEN topological_tendstoD, OF this L]
    {
      fix x
      from a `a ≠ 0` have "a * (x / a) = x"
        by (cases rule: ereal2_cases[of a x]) auto
    }
    note this[simp]
    show "eventually (λx. a * X x ∈ S) net"
      by (rule eventually_mono[OF _ *]) auto
  qed
qed auto

lemma ereal_lim_uminus:
  fixes X :: "'a => ereal"
  shows "((λi. - X i) ---> - L) net <-> (X ---> L) net"
  using ereal_lim_mult[of X L net "ereal (-1)"]
    ereal_lim_mult[of "(λi. - X i)" "-L" net "ereal (-1)"]
  by (auto simp add: algebra_simps)

lemma ereal_open_atLeast:
  fixes x :: ereal
  shows "open {x..} <-> x = -∞"
proof
  assume "x = -∞"
  then have "{x..} = UNIV"
    by auto
  then show "open {x..}"
    by auto
next
  assume "open {x..}"
  then have "open {x..} ∧ closed {x..}"
    by auto
  then have "{x..} = UNIV"
    unfolding ereal_open_closed by auto
  then show "x = -∞"
    by (simp add: bot_ereal_def atLeast_eq_UNIV_iff)
qed

lemma open_uminus_iff:
  fixes S :: "ereal set"
  shows "open (uminus ` S) <-> open S"
  using ereal_open_uminus[of S] ereal_open_uminus[of "uminus ` S"]
  by auto

lemma ereal_Liminf_uminus:
  fixes f :: "'a => ereal"
  shows "Liminf net (λx. - (f x)) = - Limsup net f"
  using ereal_Limsup_uminus[of _ "(λx. - (f x))"] by auto

lemma ereal_Lim_uminus:
  fixes f :: "'a => ereal"
  shows "(f ---> f0) net <-> ((λx. - f x) ---> - f0) net"
  using
    ereal_lim_mult[of f f0 net "- 1"]
    ereal_lim_mult[of "λx. - (f x)" "-f0" net "- 1"]
  by (auto simp: ereal_uminus_reorder)

lemma Liminf_PInfty:
  fixes f :: "'a => ereal"
  assumes "¬ trivial_limit net"
  shows "(f ---> ∞) net <-> Liminf net f = ∞"
  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
  using Liminf_le_Limsup[OF assms, of f]
  by auto

lemma Limsup_MInfty:
  fixes f :: "'a => ereal"
  assumes "¬ trivial_limit net"
  shows "(f ---> -∞) net <-> Limsup net f = -∞"
  unfolding tendsto_iff_Liminf_eq_Limsup[OF assms]
  using Liminf_le_Limsup[OF assms, of f]
  by auto

lemma convergent_ereal:
  fixes X :: "nat => 'a :: {complete_linorder,linorder_topology}"
  shows "convergent X <-> limsup X = liminf X"
  using tendsto_iff_Liminf_eq_Limsup[of sequentially]
  by (auto simp: convergent_def)

lemma limsup_le_liminf_real:
  fixes X :: "nat => real" and L :: real
  assumes 1: "limsup X ≤ L" and 2: "L ≤ liminf X"
  shows "X ----> L"
proof -
  from 1 2 have "limsup X ≤ liminf X" by auto
  hence 3: "limsup X = liminf X"  
    apply (subst eq_iff, rule conjI)
    by (rule Liminf_le_Limsup, auto)
  hence 4: "convergent (λn. ereal (X n))"
    by (subst convergent_ereal)
  hence "limsup X = lim (λn. ereal(X n))"
    by (rule convergent_limsup_cl)
  also from 1 2 3 have "limsup X = L" by auto
  finally have "lim (λn. ereal(X n)) = L" ..
  hence "(λn. ereal (X n)) ----> L"
    apply (elim subst)
    by (subst convergent_LIMSEQ_iff [symmetric], rule 4) 
  thus ?thesis by simp
qed

lemma liminf_PInfty:
  fixes X :: "nat => ereal"
  shows "X ----> ∞ <-> liminf X = ∞"
  by (metis Liminf_PInfty trivial_limit_sequentially)

lemma limsup_MInfty:
  fixes X :: "nat => ereal"
  shows "X ----> -∞ <-> limsup X = -∞"
  by (metis Limsup_MInfty trivial_limit_sequentially)

lemma ereal_lim_mono:
  fixes X Y :: "nat => 'a::linorder_topology"
  assumes "!!n. N ≤ n ==> X n ≤ Y n"
    and "X ----> x"
    and "Y ----> y"
  shows "x ≤ y"
  using assms(1) by (intro LIMSEQ_le[OF assms(2,3)]) auto

lemma incseq_le_ereal:
  fixes X :: "nat => 'a::linorder_topology"
  assumes inc: "incseq X"
    and lim: "X ----> L"
  shows "X N ≤ L"
  using inc
  by (intro ereal_lim_mono[of N, OF _ tendsto_const lim]) (simp add: incseq_def)

lemma decseq_ge_ereal:
  assumes dec: "decseq X"
    and lim: "X ----> (L::'a::linorder_topology)"
  shows "X N ≥ L"
  using dec by (intro ereal_lim_mono[of N, OF _ lim tendsto_const]) (simp add: decseq_def)

lemma bounded_abs:
  fixes a :: real
  assumes "a ≤ x"
    and "x ≤ b"
  shows "abs x ≤ max (abs a) (abs b)"
  by (metis abs_less_iff assms leI le_max_iff_disj
    less_eq_real_def less_le_not_le less_minus_iff minus_minus)

lemma ereal_Sup_lim:
  fixes a :: "'a::{complete_linorder,linorder_topology}"
  assumes "!!n. b n ∈ s"
    and "b ----> a"
  shows "a ≤ Sup s"
  by (metis Lim_bounded_ereal assms complete_lattice_class.Sup_upper)

lemma ereal_Inf_lim:
  fixes a :: "'a::{complete_linorder,linorder_topology}"
  assumes "!!n. b n ∈ s"
    and "b ----> a"
  shows "Inf s ≤ a"
  by (metis Lim_bounded2_ereal assms complete_lattice_class.Inf_lower)

lemma SUP_Lim_ereal:
  fixes X :: "nat => 'a::{complete_linorder,linorder_topology}"
  assumes inc: "incseq X"
    and l: "X ----> l"
  shows "(SUP n. X n) = l"
  using LIMSEQ_SUP[OF inc] tendsto_unique[OF trivial_limit_sequentially l]
  by simp

lemma INF_Lim_ereal:
  fixes X :: "nat => 'a::{complete_linorder,linorder_topology}"
  assumes dec: "decseq X"
    and l: "X ----> l"
  shows "(INF n. X n) = l"
  using LIMSEQ_INF[OF dec] tendsto_unique[OF trivial_limit_sequentially l]
  by simp

lemma SUP_eq_LIMSEQ:
  assumes "mono f"
  shows "(SUP n. ereal (f n)) = ereal x <-> f ----> x"
proof
  have inc: "incseq (λi. ereal (f i))"
    using `mono f` unfolding mono_def incseq_def by auto
  {
    assume "f ----> x"
    then have "(λi. ereal (f i)) ----> ereal x"
      by auto
    from SUP_Lim_ereal[OF inc this] show "(SUP n. ereal (f n)) = ereal x" .
  next
    assume "(SUP n. ereal (f n)) = ereal x"
    with LIMSEQ_SUP[OF inc] show "f ----> x" by auto
  }
qed

lemma liminf_ereal_cminus:
  fixes f :: "nat => ereal"
  assumes "c ≠ -∞"
  shows "liminf (λx. c - f x) = c - limsup f"
proof (cases c)
  case PInf
  then show ?thesis
    by (simp add: Liminf_const)
next
  case (real r)
  then show ?thesis
    unfolding liminf_SUP_INF limsup_INF_SUP
    apply (subst INF_ereal_cminus)
    apply auto
    apply (subst SUP_ereal_cminus)
    apply auto
    done
qed (insert `c ≠ -∞`, simp)


subsubsection {* Continuity *}

lemma continuous_at_of_ereal:
  fixes x0 :: ereal
  assumes "¦x0¦ ≠ ∞"
  shows "continuous (at x0) real"
proof -
  {
    fix T
    assume T: "open T" "real x0 ∈ T"
    def S  "ereal ` T"
    then have "ereal (real x0) ∈ S"
      using T by auto
    then have "x0 ∈ S"
      using assms ereal_real by auto
    moreover have "open S"
      using open_ereal S_def T by auto
    moreover have "∀y∈S. real y ∈ T"
      using S_def T by auto
    ultimately have "∃S. x0 ∈ S ∧ open S ∧ (∀y∈S. real y ∈ T)"
      by auto
  }
  then show ?thesis
    unfolding continuous_at_open by blast
qed

lemma nhds_ereal: "nhds (ereal r) = filtermap ereal (nhds r)"
  by (simp add: filtermap_nhds_open_map open_ereal continuous_at_of_ereal)

lemma at_ereal: "at (ereal r) = filtermap ereal (at r)"
  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)

lemma at_left_ereal: "at_left (ereal r) = filtermap ereal (at_left r)"
  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)

lemma at_right_ereal: "at_right (ereal r) = filtermap ereal (at_right r)"
  by (simp add: filter_eq_iff eventually_at_filter nhds_ereal eventually_filtermap)

lemma
  shows at_left_PInf: "at_left ∞ = filtermap ereal at_top"
    and at_right_MInf: "at_right (-∞) = filtermap ereal at_bot"
  unfolding filter_eq_iff eventually_filtermap eventually_at_top_dense eventually_at_bot_dense
    eventually_at_left[OF ereal_less(5)] eventually_at_right[OF ereal_less(6)]
  by (auto simp add: ereal_all_split ereal_ex_split)

lemma ereal_tendsto_simps1:
  "((f o real) ---> y) (at_left (ereal x)) <-> (f ---> y) (at_left x)"
  "((f o real) ---> y) (at_right (ereal x)) <-> (f ---> y) (at_right x)"
  "((f o real) ---> y) (at_left (∞::ereal)) <-> (f ---> y) at_top"
  "((f o real) ---> y) (at_right (-∞::ereal)) <-> (f ---> y) at_bot"
  unfolding tendsto_compose_filtermap at_left_ereal at_right_ereal at_left_PInf at_right_MInf
  by (auto simp: filtermap_filtermap filtermap_ident)

lemma ereal_tendsto_simps2:
  "((ereal o f) ---> ereal a) F <-> (f ---> a) F"
  "((ereal o f) ---> ∞) F <-> (LIM x F. f x :> at_top)"
  "((ereal o f) ---> -∞) F <-> (LIM x F. f x :> at_bot)"
  unfolding tendsto_PInfty filterlim_at_top_dense tendsto_MInfty filterlim_at_bot_dense
  using lim_ereal by (simp_all add: comp_def)

lemmas ereal_tendsto_simps = ereal_tendsto_simps1 ereal_tendsto_simps2

lemma continuous_at_iff_ereal:
  fixes f :: "'a::t2_space => real"
  shows "continuous (at x0 within s) f <-> continuous (at x0 within s) (ereal o f)"
  unfolding continuous_within comp_def lim_ereal ..

lemma continuous_on_iff_ereal:
  fixes f :: "'a::t2_space => real"
  assumes "open A"
  shows "continuous_on A f <-> continuous_on A (ereal o f)"
  unfolding continuous_on_def comp_def lim_ereal ..

lemma continuous_on_real: "continuous_on (UNIV - {∞, -∞::ereal}) real"
  using continuous_at_of_ereal continuous_on_eq_continuous_at open_image_ereal
  by auto

lemma continuous_on_iff_real:
  fixes f :: "'a::t2_space => ereal"
  assumes *: "!!x. x ∈ A ==> ¦f x¦ ≠ ∞"
  shows "continuous_on A f <-> continuous_on A (real o f)"
proof -
  have "f ` A ⊆ UNIV - {∞, -∞}"
    using assms by force
  then have *: "continuous_on (f ` A) real"
    using continuous_on_real by (simp add: continuous_on_subset)
  have **: "continuous_on ((real o f) ` A) ereal"
    using continuous_on_ereal continuous_on_subset[of "UNIV" "ereal" "(real o f) ` A"]
    by blast
  {
    assume "continuous_on A f"
    then have "continuous_on A (real o f)"
      apply (subst continuous_on_compose)
      using *
      apply auto
      done
  }
  moreover
  {
    assume "continuous_on A (real o f)"
    then have "continuous_on A (ereal o (real o f))"
      apply (subst continuous_on_compose)
      using **
      apply auto
      done
    then have "continuous_on A f"
      apply (subst continuous_on_eq[of A "ereal o (real o f)" f])
      using assms ereal_real
      apply auto
      done
  }
  ultimately show ?thesis
    by auto
qed

lemma continuous_at_const:
  fixes f :: "'a::t2_space => ereal"
  assumes "∀x. f x = C"
  shows "∀x. continuous (at x) f"
  unfolding continuous_at_open
  using assms t1_space
  by auto

lemma mono_closed_real:
  fixes S :: "real set"
  assumes mono: "∀y z. y ∈ S ∧ y ≤ z --> z ∈ S"
    and "closed S"
  shows "S = {} ∨ S = UNIV ∨ (∃a. S = {a..})"
proof -
  {
    assume "S ≠ {}"
    { assume ex: "∃B. ∀x∈S. B ≤ x"
      then have *: "∀x∈S. Inf S ≤ x"
        using cInf_lower[of _ S] ex by (metis bdd_below_def)
      then have "Inf S ∈ S"
        apply (subst closed_contains_Inf)
        using ex `S ≠ {}` `closed S`
        apply auto
        done
      then have "∀x. Inf S ≤ x <-> x ∈ S"
        using mono[rule_format, of "Inf S"] *
        by auto
      then have "S = {Inf S ..}"
        by auto
      then have "∃a. S = {a ..}"
        by auto
    }
    moreover
    {
      assume "¬ (∃B. ∀x∈S. B ≤ x)"
      then have nex: "∀B. ∃x∈S. x < B"
        by (simp add: not_le)
      {
        fix y
        obtain x where "x∈S" and "x < y"
          using nex by auto
        then have "y ∈ S"
          using mono[rule_format, of x y] by auto
      }
      then have "S = UNIV"
        by auto
    }
    ultimately have "S = UNIV ∨ (∃a. S = {a ..})"
      by blast
  }
  then show ?thesis
    by blast
qed

lemma mono_closed_ereal:
  fixes S :: "real set"
  assumes mono: "∀y z. y ∈ S ∧ y ≤ z --> z ∈ S"
    and "closed S"
  shows "∃a. S = {x. a ≤ ereal x}"
proof -
  {
    assume "S = {}"
    then have ?thesis
      apply (rule_tac x=PInfty in exI)
      apply auto
      done
  }
  moreover
  {
    assume "S = UNIV"
    then have ?thesis
      apply (rule_tac x="-∞" in exI)
      apply auto
      done
  }
  moreover
  {
    assume "∃a. S = {a ..}"
    then obtain a where "S = {a ..}"
      by auto
    then have ?thesis
      apply (rule_tac x="ereal a" in exI)
      apply auto
      done
  }
  ultimately show ?thesis
    using mono_closed_real[of S] assms by auto
qed


subsection {* Sums *}

lemma setsum_ereal[simp]: "(∑x∈A. ereal (f x)) = ereal (∑x∈A. f x)"
proof (cases "finite A")
  case True
  then show ?thesis by induct auto
next
  case False
  then show ?thesis by simp
qed

lemma setsum_Pinfty:
  fixes f :: "'a => ereal"
  shows "(∑x∈P. f x) = ∞ <-> finite P ∧ (∃i∈P. f i = ∞)"
proof safe
  assume *: "setsum f P = ∞"
  show "finite P"
  proof (rule ccontr)
    assume "infinite P"
    with * show False
      by auto
  qed
  show "∃i∈P. f i = ∞"
  proof (rule ccontr)
    assume "¬ ?thesis"
    then have "!!i. i ∈ P ==> f i ≠ ∞"
      by auto
    with `finite P` have "setsum f P ≠ ∞"
      by induct auto
    with * show False
      by auto
  qed
next
  fix i
  assume "finite P" and "i ∈ P" and "f i = ∞"
  then show "setsum f P = ∞"
  proof induct
    case (insert x A)
    show ?case using insert by (cases "x = i") auto
  qed simp
qed

lemma setsum_Inf:
  fixes f :: "'a => ereal"
  shows "¦setsum f A¦ = ∞ <-> finite A ∧ (∃i∈A. ¦f i¦ = ∞)"
proof
  assume *: "¦setsum f A¦ = ∞"
  have "finite A"
    by (rule ccontr) (insert *, auto)
  moreover have "∃i∈A. ¦f i¦ = ∞"
  proof (rule ccontr)
    assume "¬ ?thesis"
    then have "∀i∈A. ∃r. f i = ereal r"
      by auto
    from bchoice[OF this] obtain r where "∀x∈A. f x = ereal (r x)" ..
    with * show False
      by auto
  qed
  ultimately show "finite A ∧ (∃i∈A. ¦f i¦ = ∞)"
    by auto
next
  assume "finite A ∧ (∃i∈A. ¦f i¦ = ∞)"
  then obtain i where "finite A" "i ∈ A" and "¦f i¦ = ∞"
    by auto
  then show "¦setsum f A¦ = ∞"
  proof induct
    case (insert j A)
    then show ?case
      by (cases rule: ereal3_cases[of "f i" "f j" "setsum f A"]) auto
  qed simp
qed

lemma setsum_real_of_ereal:
  fixes f :: "'i => ereal"
  assumes "!!x. x ∈ S ==> ¦f x¦ ≠ ∞"
  shows "(∑x∈S. real (f x)) = real (setsum f S)"
proof -
  have "∀x∈S. ∃r. f x = ereal r"
  proof
    fix x
    assume "x ∈ S"
    from assms[OF this] show "∃r. f x = ereal r"
      by (cases "f x") auto
  qed
  from bchoice[OF this] obtain r where "∀x∈S. f x = ereal (r x)" ..
  then show ?thesis
    by simp
qed

lemma setsum_ereal_0:
  fixes f :: "'a => ereal"
  assumes "finite A"
    and "!!i. i ∈ A ==> 0 ≤ f i"
  shows "(∑x∈A. f x) = 0 <-> (∀i∈A. f i = 0)"
proof
  assume *: "(∑x∈A. f x) = 0"
  then have "(∑x∈A. f x) ≠ ∞"
    by auto
  then have "∀i∈A. ¦f i¦ ≠ ∞"
    using assms by (force simp: setsum_Pinfty)
  then have "∀i∈A. ∃r. f i = ereal r"
    by auto
  from bchoice[OF this] * assms show "∀i∈A. f i = 0"
    using setsum_nonneg_eq_0_iff[of A "λi. real (f i)"] by auto
qed (rule setsum.neutral)

lemma setsum_ereal_right_distrib:
  fixes f :: "'a => ereal"
  assumes "!!i. i ∈ A ==> 0 ≤ f i"
  shows "r * setsum f A = (∑n∈A. r * f n)"
proof cases
  assume "finite A"
  then show ?thesis using assms
    by induct (auto simp: ereal_right_distrib setsum_nonneg)
qed simp

lemma sums_ereal_positive:
  fixes f :: "nat => ereal"
  assumes "!!i. 0 ≤ f i"
  shows "f sums (SUP n. ∑i<n. f i)"
proof -
  have "incseq (λi. ∑j=0..<i. f j)"
    using ereal_add_mono[OF _ assms]
    by (auto intro!: incseq_SucI)
  from LIMSEQ_SUP[OF this]
  show ?thesis unfolding sums_def
    by (simp add: atLeast0LessThan)
qed

lemma summable_ereal_pos:
  fixes f :: "nat => ereal"
  assumes "!!i. 0 ≤ f i"
  shows "summable f"
  using sums_ereal_positive[of f, OF assms]
  unfolding summable_def
  by auto

lemma suminf_ereal_eq_SUP:
  fixes f :: "nat => ereal"
  assumes "!!i. 0 ≤ f i"
  shows "(∑x. f x) = (SUP n. ∑i<n. f i)"
  using sums_ereal_positive[of f, OF assms, THEN sums_unique]
  by simp

lemma sums_ereal: "(λx. ereal (f x)) sums ereal x <-> f sums x"
  unfolding sums_def by simp

lemma suminf_bound:
  fixes f :: "nat => ereal"
  assumes "∀N. (∑n<N. f n) ≤ x"
    and pos: "!!n. 0 ≤ f n"
  shows "suminf f ≤ x"
proof (rule Lim_bounded_ereal)
  have "summable f" using pos[THEN summable_ereal_pos] .
  then show "(λN. ∑n<N. f n) ----> suminf f"
    by (auto dest!: summable_sums simp: sums_def atLeast0LessThan)
  show "∀n≥0. setsum f {..<n} ≤ x"
    using assms by auto
qed

lemma suminf_bound_add:
  fixes f :: "nat => ereal"
  assumes "∀N. (∑n<N. f n) + y ≤ x"
    and pos: "!!n. 0 ≤ f n"
    and "y ≠ -∞"
  shows "suminf f + y ≤ x"
proof (cases y)
  case (real r)
  then have "∀N. (∑n<N. f n) ≤ x - y"
    using assms by (simp add: ereal_le_minus)
  then have "(∑ n. f n) ≤ x - y"
    using pos by (rule suminf_bound)
  then show "(∑ n. f n) + y ≤ x"
    using assms real by (simp add: ereal_le_minus)
qed (insert assms, auto)

lemma suminf_upper:
  fixes f :: "nat => ereal"
  assumes "!!n. 0 ≤ f n"
  shows "(∑n<N. f n) ≤ (∑n. f n)"
  unfolding suminf_ereal_eq_SUP [OF assms]
  by (auto intro: complete_lattice_class.SUP_upper)

lemma suminf_0_le:
  fixes f :: "nat => ereal"
  assumes "!!n. 0 ≤ f n"
  shows "0 ≤ (∑n. f n)"
  using suminf_upper[of f 0, OF assms]
  by simp

lemma suminf_le_pos:
  fixes f g :: "nat => ereal"
  assumes "!!N. f N ≤ g N"
    and "!!N. 0 ≤ f N"
  shows "suminf f ≤ suminf g"
proof (safe intro!: suminf_bound)
  fix n
  {
    fix N
    have "0 ≤ g N"
      using assms(2,1)[of N] by auto
  }
  have "setsum f {..<n} ≤ setsum g {..<n}"
    using assms by (auto intro: setsum_mono)
  also have "… ≤ suminf g"
    using `!!N. 0 ≤ g N`
    by (rule suminf_upper)
  finally show "setsum f {..<n} ≤ suminf g" .
qed (rule assms(2))

lemma suminf_half_series_ereal: "(∑n. (1/2 :: ereal) ^ Suc n) = 1"
  using sums_ereal[THEN iffD2, OF power_half_series, THEN sums_unique, symmetric]
  by (simp add: one_ereal_def)

lemma suminf_add_ereal:
  fixes f g :: "nat => ereal"
  assumes "!!i. 0 ≤ f i"
    and "!!i. 0 ≤ g i"
  shows "(∑i. f i + g i) = suminf f + suminf g"
  apply (subst (1 2 3) suminf_ereal_eq_SUP)
  unfolding setsum.distrib
  apply (intro assms ereal_add_nonneg_nonneg SUP_ereal_add_pos incseq_setsumI setsum_nonneg ballI)+
  done

lemma suminf_cmult_ereal:
  fixes f g :: "nat => ereal"
  assumes "!!i. 0 ≤ f i"
    and "0 ≤ a"
  shows "(∑i. a * f i) = a * suminf f"
  by (auto simp: setsum_ereal_right_distrib[symmetric] assms
       ereal_zero_le_0_iff setsum_nonneg suminf_ereal_eq_SUP
       intro!: SUP_ereal_cmult)

lemma suminf_PInfty:
  fixes f :: "nat => ereal"
  assumes "!!i. 0 ≤ f i"
    and "suminf f ≠ ∞"
  shows "f i ≠ ∞"
proof -
  from suminf_upper[of f "Suc i", OF assms(1)] assms(2)
  have "(∑i<Suc i. f i) ≠ ∞"
    by auto
  then show ?thesis
    unfolding setsum_Pinfty by simp
qed

lemma suminf_PInfty_fun:
  assumes "!!i. 0 ≤ f i"
    and "suminf f ≠ ∞"
  shows "∃f'. f = (λx. ereal (f' x))"
proof -
  have "∀i. ∃r. f i = ereal r"
  proof
    fix i
    show "∃r. f i = ereal r"
      using suminf_PInfty[OF assms] assms(1)[of i]
      by (cases "f i") auto
  qed
  from choice[OF this] show ?thesis
    by auto
qed

lemma summable_ereal:
  assumes "!!i. 0 ≤ f i"
    and "(∑i. ereal (f i)) ≠ ∞"
  shows "summable f"
proof -
  have "0 ≤ (∑i. ereal (f i))"
    using assms by (intro suminf_0_le) auto
  with assms obtain r where r: "(∑i. ereal (f i)) = ereal r"
    by (cases "∑i. ereal (f i)") auto
  from summable_ereal_pos[of "λx. ereal (f x)"]
  have "summable (λx. ereal (f x))"
    using assms by auto
  from summable_sums[OF this]
  have "(λx. ereal (f x)) sums (∑x. ereal (f x))"
    by auto
  then show "summable f"
    unfolding r sums_ereal summable_def ..
qed

lemma suminf_ereal:
  assumes "!!i. 0 ≤ f i"
    and "(∑i. ereal (f i)) ≠ ∞"
  shows "(∑i. ereal (f i)) = ereal (suminf f)"
proof (rule sums_unique[symmetric])
  from summable_ereal[OF assms]
  show "(λx. ereal (f x)) sums (ereal (suminf f))"
    unfolding sums_ereal
    using assms
    by (intro summable_sums summable_ereal)
qed

lemma suminf_ereal_minus:
  fixes f g :: "nat => ereal"
  assumes ord: "!!i. g i ≤ f i" "!!i. 0 ≤ g i"
    and fin: "suminf f ≠ ∞" "suminf g ≠ ∞"
  shows "(∑i. f i - g i) = suminf f - suminf g"
proof -
  {
    fix i
    have "0 ≤ f i"
      using ord[of i] by auto
  }
  moreover
  from suminf_PInfty_fun[OF `!!i. 0 ≤ f i` fin(1)] obtain f' where [simp]: "f = (λx. ereal (f' x))" ..
  from suminf_PInfty_fun[OF `!!i. 0 ≤ g i` fin(2)] obtain g' where [simp]: "g = (λx. ereal (g' x))" ..
  {
    fix i
    have "0 ≤ f i - g i"
      using ord[of i] by (auto simp: ereal_le_minus_iff)
  }
  moreover
  have "suminf (λi. f i - g i) ≤ suminf f"
    using assms by (auto intro!: suminf_le_pos simp: field_simps)
  then have "suminf (λi. f i - g i) ≠ ∞"
    using fin by auto
  ultimately show ?thesis
    using assms `!!i. 0 ≤ f i`
    apply simp
    apply (subst (1 2 3) suminf_ereal)
    apply (auto intro!: suminf_diff[symmetric] summable_ereal)
    done
qed

lemma suminf_ereal_PInf [simp]: "(∑x. ∞::ereal) = ∞"
proof -
  have "(∑i<Suc 0. ∞) ≤ (∑x. ∞::ereal)"
    by (rule suminf_upper) auto
  then show ?thesis
    by simp
qed

lemma summable_real_of_ereal:
  fixes f :: "nat => ereal"
  assumes f: "!!i. 0 ≤ f i"
    and fin: "(∑i. f i) ≠ ∞"
  shows "summable (λi. real (f i))"
proof (rule summable_def[THEN iffD2])
  have "0 ≤ (∑i. f i)"
    using assms by (auto intro: suminf_0_le)
  with fin obtain r where r: "ereal r = (∑i. f i)"
    by (cases "(∑i. f i)") auto
  {
    fix i
    have "f i ≠ ∞"
      using f by (intro suminf_PInfty[OF _ fin]) auto
    then have "¦f i¦ ≠ ∞"
      using f[of i] by auto
  }
  note fin = this
  have "(λi. ereal (real (f i))) sums (∑i. ereal (real (f i)))"
    using f
    by (auto intro!: summable_ereal_pos simp: ereal_le_real_iff zero_ereal_def)
  also have "… = ereal r"
    using fin r by (auto simp: ereal_real)
  finally show "∃r. (λi. real (f i)) sums r"
    by (auto simp: sums_ereal)
qed

lemma suminf_SUP_eq:
  fixes f :: "nat => nat => ereal"
  assumes "!!i. incseq (λn. f n i)"
    and "!!n i. 0 ≤ f n i"
  shows "(∑i. SUP n. f n i) = (SUP n. ∑i. f n i)"
proof -
  {
    fix n :: nat
    have "(∑i<n. SUP k. f k i) = (SUP k. ∑i<n. f k i)"
      using assms
      by (auto intro!: SUP_ereal_setsum [symmetric])
  }
  note * = this
  show ?thesis
    using assms
    apply (subst (1 2) suminf_ereal_eq_SUP)
    unfolding *
    apply (auto intro!: SUP_upper2)
    apply (subst SUP_commute)
    apply rule
    done
qed

lemma suminf_setsum_ereal:
  fixes f :: "_ => _ => ereal"
  assumes nonneg: "!!i a. a ∈ A ==> 0 ≤ f i a"
  shows "(∑i. ∑a∈A. f i a) = (∑a∈A. ∑i. f i a)"
proof (cases "finite A")
  case True
  then show ?thesis
    using nonneg
    by induct (simp_all add: suminf_add_ereal setsum_nonneg)
next
  case False
  then show ?thesis by simp
qed

lemma suminf_ereal_eq_0:
  fixes f :: "nat => ereal"
  assumes nneg: "!!i. 0 ≤ f i"
  shows "(∑i. f i) = 0 <-> (∀i. f i = 0)"
proof
  assume "(∑i. f i) = 0"
  {
    fix i
    assume "f i ≠ 0"
    with nneg have "0 < f i"
      by (auto simp: less_le)
    also have "f i = (∑j. if j = i then f i else 0)"
      by (subst suminf_finite[where N="{i}"]) auto
    also have "… ≤ (∑i. f i)"
      using nneg
      by (auto intro!: suminf_le_pos)
    finally have False
      using `(∑i. f i) = 0` by auto
  }
  then show "∀i. f i = 0"
    by auto
qed simp

lemma Liminf_within:
  fixes f :: "'a::metric_space => 'b::complete_lattice"
  shows "Liminf (at x within S) f = (SUP e:{0<..}. INF y:(S ∩ ball x e - {x}). f y)"
  unfolding Liminf_def eventually_at
proof (rule SUP_eq, simp_all add: Ball_def Bex_def, safe)
  fix P d
  assume "0 < d" and "∀y. y ∈ S --> y ≠ x ∧ dist y x < d --> P y"
  then have "S ∩ ball x d - {x} ⊆ {x. P x}"
    by (auto simp: zero_less_dist_iff dist_commute)
  then show "∃r>0. INFIMUM (Collect P) f ≤ INFIMUM (S ∩ ball x r - {x}) f"
    by (intro exI[of _ d] INF_mono conjI `0 < d`) auto
next
  fix d :: real
  assume "0 < d"
  then show "∃P. (∃d>0. ∀xa. xa ∈ S --> xa ≠ x ∧ dist xa x < d --> P xa) ∧
    INFIMUM (S ∩ ball x d - {x}) f ≤ INFIMUM (Collect P) f"
    by (intro exI[of _ "λy. y ∈ S ∩ ball x d - {x}"])
       (auto intro!: INF_mono exI[of _ d] simp: dist_commute)
qed

lemma Limsup_within:
  fixes f :: "'a::metric_space => 'b::complete_lattice"
  shows "Limsup (at x within S) f = (INF e:{0<..}. SUP y:(S ∩ ball x e - {x}). f y)"
  unfolding Limsup_def eventually_at
proof (rule INF_eq, simp_all add: Ball_def Bex_def, safe)
  fix P d
  assume "0 < d" and "∀y. y ∈ S --> y ≠ x ∧ dist y x < d --> P y"
  then have "S ∩ ball x d - {x} ⊆ {x. P x}"
    by (auto simp: zero_less_dist_iff dist_commute)
  then show "∃r>0. SUPREMUM (S ∩ ball x r - {x}) f ≤ SUPREMUM (Collect P) f"
    by (intro exI[of _ d] SUP_mono conjI `0 < d`) auto
next
  fix d :: real
  assume "0 < d"
  then show "∃P. (∃d>0. ∀xa. xa ∈ S --> xa ≠ x ∧ dist xa x < d --> P xa) ∧
    SUPREMUM (Collect P) f ≤ SUPREMUM (S ∩ ball x d - {x}) f"
    by (intro exI[of _ "λy. y ∈ S ∩ ball x d - {x}"])
       (auto intro!: SUP_mono exI[of _ d] simp: dist_commute)
qed

lemma Liminf_at:
  fixes f :: "'a::metric_space => 'b::complete_lattice"
  shows "Liminf (at x) f = (SUP e:{0<..}. INF y:(ball x e - {x}). f y)"
  using Liminf_within[of x UNIV f] by simp

lemma Limsup_at:
  fixes f :: "'a::metric_space => 'b::complete_lattice"
  shows "Limsup (at x) f = (INF e:{0<..}. SUP y:(ball x e - {x}). f y)"
  using Limsup_within[of x UNIV f] by simp

lemma min_Liminf_at:
  fixes f :: "'a::metric_space => 'b::complete_linorder"
  shows "min (f x) (Liminf (at x) f) = (SUP e:{0<..}. INF y:ball x e. f y)"
  unfolding inf_min[symmetric] Liminf_at
  apply (subst inf_commute)
  apply (subst SUP_inf)
  apply (intro SUP_cong[OF refl])
  apply (cut_tac A="ball x xa - {x}" and B="{x}" and M=f in INF_union)
  apply (drule sym)
  apply auto
  apply (metis INF_absorb centre_in_ball)
  done


lemma suminf_ereal_offset_le:
  fixes f :: "nat => ereal"
  assumes f: "!!i. 0 ≤ f i"
  shows "(∑i. f (i + k)) ≤ suminf f"
proof -
  have "(λn. ∑i<n. f (i + k)) ----> (∑i. f (i + k))"
    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
  moreover have "(λn. ∑i<n. f i) ----> (∑i. f i)"
    using summable_sums[OF summable_ereal_pos] by (simp add: sums_def atLeast0LessThan f)
  then have "(λn. ∑i<n + k. f i) ----> (∑i. f i)"
    by (rule LIMSEQ_ignore_initial_segment)
  ultimately show ?thesis
  proof (rule LIMSEQ_le, safe intro!: exI[of _ k])
    fix n assume "k ≤ n"
    have "(∑i<n. f (i + k)) = (∑i<n. (f o (λi. i + k)) i)"
      by simp
    also have "… = (∑i∈(λi. i + k) ` {..<n}. f i)"
      by (subst setsum.reindex) auto
    also have "… ≤ setsum f {..<n + k}"
      by (intro setsum_mono3) (auto simp: f)
    finally show "(∑i<n. f (i + k)) ≤ setsum f {..<n + k}" .
  qed
qed

lemma sums_suminf_ereal: "f sums x ==> (∑i. ereal (f i)) = ereal x"
  by (metis sums_ereal sums_unique)

lemma suminf_ereal': "summable f ==> (∑i. ereal (f i)) = ereal (∑i. f i)"
  by (metis sums_ereal sums_unique summable_def)

lemma suminf_ereal_finite: "summable f ==> (∑i. ereal (f i)) ≠ ∞"
  by (auto simp: sums_ereal[symmetric] summable_def sums_unique[symmetric])

subsection {* monoset *}

definition (in order) mono_set:
  "mono_set S <-> (∀x y. x ≤ y --> x ∈ S --> y ∈ S)"

lemma (in order) mono_greaterThan [intro, simp]: "mono_set {B<..}" unfolding mono_set by auto
lemma (in order) mono_atLeast [intro, simp]: "mono_set {B..}" unfolding mono_set by auto
lemma (in order) mono_UNIV [intro, simp]: "mono_set UNIV" unfolding mono_set by auto
lemma (in order) mono_empty [intro, simp]: "mono_set {}" unfolding mono_set by auto

lemma (in complete_linorder) mono_set_iff:
  fixes S :: "'a set"
  defines "a ≡ Inf S"
  shows "mono_set S <-> S = {a <..} ∨ S = {a..}" (is "_ = ?c")
proof
  assume "mono_set S"
  then have mono: "!!x y. x ≤ y ==> x ∈ S ==> y ∈ S"
    by (auto simp: mono_set)
  show ?c
  proof cases
    assume "a ∈ S"
    show ?c
      using mono[OF _ `a ∈ S`]
      by (auto intro: Inf_lower simp: a_def)
  next
    assume "a ∉ S"
    have "S = {a <..}"
    proof safe
      fix x assume "x ∈ S"
      then have "a ≤ x"
        unfolding a_def by (rule Inf_lower)
      then show "a < x"
        using `x ∈ S` `a ∉ S` by (cases "a = x") auto
    next
      fix x assume "a < x"
      then obtain y where "y < x" "y ∈ S"
        unfolding a_def Inf_less_iff ..
      with mono[of y x] show "x ∈ S"
        by auto
    qed
    then show ?c ..
  qed
qed auto

lemma ereal_open_mono_set:
  fixes S :: "ereal set"
  shows "open S ∧ mono_set S <-> S = UNIV ∨ S = {Inf S <..}"
  by (metis Inf_UNIV atLeast_eq_UNIV_iff ereal_open_atLeast
    ereal_open_closed mono_set_iff open_ereal_greaterThan)

lemma ereal_closed_mono_set:
  fixes S :: "ereal set"
  shows "closed S ∧ mono_set S <-> S = {} ∨ S = {Inf S ..}"
  by (metis Inf_UNIV atLeast_eq_UNIV_iff closed_ereal_atLeast
    ereal_open_closed mono_empty mono_set_iff open_ereal_greaterThan)

lemma ereal_Liminf_Sup_monoset:
  fixes f :: "'a => ereal"
  shows "Liminf net f =
    Sup {l. ∀S. open S --> mono_set S --> l ∈ S --> eventually (λx. f x ∈ S) net}"
    (is "_ = Sup ?A")
proof (safe intro!: Liminf_eqI complete_lattice_class.Sup_upper complete_lattice_class.Sup_least)
  fix P
  assume P: "eventually P net"
  fix S
  assume S: "mono_set S" "INFIMUM (Collect P) f ∈ S"
  {
    fix x
    assume "P x"
    then have "INFIMUM (Collect P) f ≤ f x"
      by (intro complete_lattice_class.INF_lower) simp
    with S have "f x ∈ S"
      by (simp add: mono_set)
  }
  with P show "eventually (λx. f x ∈ S) net"
    by (auto elim: eventually_elim1)
next
  fix y l
  assume S: "∀S. open S --> mono_set S --> l ∈ S --> eventually  (λx. f x ∈ S) net"
  assume P: "∀P. eventually P net --> INFIMUM (Collect P) f ≤ y"
  show "l ≤ y"
  proof (rule dense_le)
    fix B
    assume "B < l"
    then have "eventually (λx. f x ∈ {B <..}) net"
      by (intro S[rule_format]) auto
    then have "INFIMUM {x. B < f x} f ≤ y"
      using P by auto
    moreover have "B ≤ INFIMUM {x. B < f x} f"
      by (intro INF_greatest) auto
    ultimately show "B ≤ y"
      by simp
  qed
qed

lemma ereal_Limsup_Inf_monoset:
  fixes f :: "'a => ereal"
  shows "Limsup net f =
    Inf {l. ∀S. open S --> mono_set (uminus ` S) --> l ∈ S --> eventually (λx. f x ∈ S) net}"
    (is "_ = Inf ?A")
proof (safe intro!: Limsup_eqI complete_lattice_class.Inf_lower complete_lattice_class.Inf_greatest)
  fix P
  assume P: "eventually P net"
  fix S
  assume S: "mono_set (uminus`S)" "SUPREMUM (Collect P) f ∈ S"
  {
    fix x
    assume "P x"
    then have "f x ≤ SUPREMUM (Collect P) f"
      by (intro complete_lattice_class.SUP_upper) simp
    with S(1)[unfolded mono_set, rule_format, of "- SUPREMUM (Collect P) f" "- f x"] S(2)
    have "f x ∈ S"
      by (simp add: inj_image_mem_iff) }
  with P show "eventually (λx. f x ∈ S) net"
    by (auto elim: eventually_elim1)
next
  fix y l
  assume S: "∀S. open S --> mono_set (uminus ` S) --> l ∈ S --> eventually  (λx. f x ∈ S) net"
  assume P: "∀P. eventually P net --> y ≤ SUPREMUM (Collect P) f"
  show "y ≤ l"
  proof (rule dense_ge)
    fix B
    assume "l < B"
    then have "eventually (λx. f x ∈ {..< B}) net"
      by (intro S[rule_format]) auto
    then have "y ≤ SUPREMUM {x. f x < B} f"
      using P by auto
    moreover have "SUPREMUM {x. f x < B} f ≤ B"
      by (intro SUP_least) auto
    ultimately show "y ≤ B"
      by simp
  qed
qed

lemma liminf_bounded_open:
  fixes x :: "nat => ereal"
  shows "x0 ≤ liminf x <-> (∀S. open S --> mono_set S --> x0 ∈ S --> (∃N. ∀n≥N. x n ∈ S))"
  (is "_ <-> ?P x0")
proof
  assume "?P x0"
  then show "x0 ≤ liminf x"
    unfolding ereal_Liminf_Sup_monoset eventually_sequentially
    by (intro complete_lattice_class.Sup_upper) auto
next
  assume "x0 ≤ liminf x"
  {
    fix S :: "ereal set"
    assume om: "open S" "mono_set S" "x0 ∈ S"
    {
      assume "S = UNIV"
      then have "∃N. ∀n≥N. x n ∈ S"
        by auto
    }
    moreover
    {
      assume "S ≠ UNIV"
      then obtain B where B: "S = {B<..}"
        using om ereal_open_mono_set by auto
      then have "B < x0"
        using om by auto
      then have "∃N. ∀n≥N. x n ∈ S"
        unfolding B
        using `x0 ≤ liminf x` liminf_bounded_iff
        by auto
    }
    ultimately have "∃N. ∀n≥N. x n ∈ S"
      by auto
  }
  then show "?P x0"
    by auto
qed

subsection "Relate extended reals and the indicator function"

lemma ereal_indicator: "ereal (indicator A x) = indicator A x"
  by (auto simp: indicator_def one_ereal_def)

lemma ereal_mult_indicator: "ereal (x * indicator A y) = ereal x * indicator A y"
  by (simp split: split_indicator)

lemma ereal_indicator_mult: "ereal (indicator A y * x) = indicator A y * ereal x"
  by (simp split: split_indicator)

lemma ereal_indicator_nonneg[simp, intro]: "0 ≤ (indicator A x ::ereal)"
  unfolding indicator_def by auto

end