Theory Extended_Real_Limits

theory Extended_Real_Limits
imports Topology_Euclidean_Space Extended_Nonnegative_Real
(*  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
*)

section ‹Limits on the Extended real number line›

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

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_Int_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

instance ereal :: second_countable_topology
proof (standard, intro exI conjI)
  let ?B = "(⋃r∈ℚ. {{..< 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} = ⋃{{..<x}|x. x ∈ ℚ ∧ x < e}" "{e<..} = ⋃{{x<..}|x. x ∈ ℚ ∧ 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

text ‹This is a copy from ‹ereal :: second_countable_topology›. Maybe find a common super class of
topological spaces where the rational numbers are densely embedded ?›
instance ennreal :: second_countable_topology
proof (standard, intro exI conjI)
  let ?B = "(⋃r∈ℚ. {{..< r}, {r <..}} :: ennreal set set)"
  show "countable ?B"
    by (auto intro: countable_rat)
  show "open = generate_topology ?B"
  proof (intro ext iffI)
    fix S :: "ennreal 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} = ⋃{{..<x}|x. x ∈ ℚ ∧ x < e}" "{e<..} = ⋃{{x<..}|x. x ∈ ℚ ∧ e < x}"
        by (auto dest: ennreal_rat_dense
                 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 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_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 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

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

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_mono)
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_mono)
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_le_0: "(indicator S x::ereal) ≤ 0 ⟷ x ∉ S"
  by (auto split: split_indicator simp: one_ereal_def)

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

lemma indicator_inter_arith_ereal: "indicator A x * indicator B x = (indicator (A ∩ B) x :: ereal)"
  by (simp split: split_indicator)

end