Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/Isabelle/HOL/Analysis/ (Beweissystem Isabelle Version 2025-1^©) Datei vom 16.11.2025 mit Größe 82 kB

Quelle Extended_Real_Limits.thy Sprache: Isabelle

(*  Title:      HOL/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 \<open>Limits on the Extended Real Number Line\<close> (* TO FIX: perhaps put all Nonstandard Analysis related
topics together? *)

theory Extended_Real_Limits
imports
  Topology_Euclidean_Space
  "HOL-Library.Extended_Real"
  "HOL-Library.Extended_Nonnegative_Real"
  "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\<^marker>\<open>tag unimportant\<close> enat :: second_countable_topology
proof
  show "\B::enat set set. countable B \ open = generate_topology B"
  proof (intro exI conjI)
    show "countable (range lessThan \ range greaterThan::enat set set)"
      by auto
  qed (simp add: open_enat_def)
qed

instance\<^marker>\<open>tag unimportant\<close> 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 = {.. b = {e<..}"
        by auto
      moreover have "{..{{.. \ \ 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 \<open>This is a copy from \<open>ereal :: second_countable_topology\<close>. Maybe find a common super class of
topological spaces where the rational numbers are densely embedded ?\<close>
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 = {.. b = {e<..}"
        by auto
      moreover have "{..{{.. \ \ 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 \<open>S \<noteq> {}\<close>)
    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<.. 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"
  using ereal_open_closed_aux open_closed by auto

lemma ereal_open_atLeast:
  fixes x :: ereal
  shows "open {x..} \ x = -\"
  by (metis atLeast_eq_UNIV_iff bot_ereal_def closed_atLeast ereal_open_closed not_Ici_eq_empty)

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"
        by (meson \<open>S \<noteq> {}\<close> assms(2) bdd_belowI closed_contains_Inf)
      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 -
  consider "S = {} \ S = UNIV" | "(\a. S = {a..})"
    using assms(2) mono mono_closed_real by blast
  then show ?thesis
  proof cases
    case 1
    then show ?thesis
      by (meson PInfty_neq_ereal(1) UNIV_eq_I bot.extremum empty_Collect_eq ereal_infty_less_eq(1) mem_Collect_eq)
  next
    case 2
    then show ?thesis
      by (metis atLeast_iff ereal_less_eq(3) mem_Collect_eq subsetI subset_antisym)
  qed
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: dist_commute)
  then show "\r>0. Inf (f ` (Collect P)) \ Inf (f ` (S \ ball x r - {x}))"
    by (intro exI[of _ d] INF_mono conjI \<open>0 < d\<close>) auto
next
  fix d :: real
  assume "0 < d"
  then show "\P. (\d>0. \xa. xa \ S \ xa \ x \ dist xa x < d \ P xa) \
    Inf (f ` (S \<inter> ball x d - {x})) \<le> Inf (f ` (Collect P))"
    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: dist_commute)
  then show "\r>0. Sup (f ` (S \ ball x r - {x})) \ Sup (f ` (Collect P))"
    by (intro exI[of _ d] SUP_mono conjI \<open>0 < d\<close>) auto
next
  fix d :: real
  assume "0 < d"
  then show "\P. (\d>0. \xa. xa \ S \ xa \ x \ dist xa x < d \ P xa) \
    Sup (f ` (Collect P)) \<le> Sup (f ` (S \<inter> ball x d - {x}))"
    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)"
  apply (simp add: inf_min [symmetric] Liminf_at inf_commute [of "f x"] SUP_inf)
  apply (metis (no_types, lifting) INF_insert centre_in_ball greaterThan_iff image_cong inf_commute insert_Diff)
  done

subsection \<open>Extended-Real.thy\<close> (*FIX ME change title *)

lemma sum_constant_ereal:
  fixes a::ereal
  shows "(\i\I. a) = a * card I"
proof (induction I rule: infinite_finite_induct)
  case (insert i I)
  then show ?case
    by (simp add: ereal_right_distrib flip: plus_ereal.simps)
qed auto

lemma real_lim_then_eventually_real:
  assumes "(u \ ereal l) F"
  shows "eventually (\n. u n = ereal(real_of_ereal(u n))) F"
proof -
  have "ereal l \ {-\<..<(\::ereal)}" by simp
  moreover have "open {-\<..<(\::ereal)}" by simp
  ultimately have "eventually (\n. u n \ {-\<..<(\::ereal)}) F" using assms tendsto_def by blast
  moreover have "\x. x \ {-\<..<(\::ereal)} \ x = ereal(real_of_ereal x)" using ereal_real by auto
  ultimately show ?thesis by (metis (mono_tags, lifting) eventually_mono)
qed

lemma ereal_Inf_cmult:
  assumes "c>(0::real)"
  shows "Inf {ereal c * x |x. P x} = ereal c * Inf {x. P x}"
proof -
  have "bij ((*) (ereal c))"
    apply (rule bij_betw_byWitness[of _ "\x. (x::ereal) / c"], auto simp: assms ereal_mult_divide)
    using assms ereal_divide_eq by auto
  then have "ereal c * Inf {x. P x} = Inf ((*) (ereal c) ` {x. P x})"
    by (simp add: assms ereal_mult_left_mono less_imp_le mono_def mono_bij_Inf)
  then show ?thesis
    by (simp add: setcompr_eq_image)
qed

subsubsection\<^marker>\<open>tag important\<close> \<open>Continuity of addition\<close>

text \<open>The next few lemmas remove an unnecessary assumption in \<open>tendsto_add_ereal\<close>, culminating
in \<open>tendsto_add_ereal_general\<close> which essentially says that the addition
is continuous on ereal times ereal, except at \<open>(-\<infinity>, \<infinity>)\<close> and \<open>(\<infinity>, -\<infinity>)\<close>.
It is much more convenient in many situations, see for instance the proof of
\<open>tendsto_sum_ereal\<close> below.\<close>

lemma tendsto_add_ereal_PInf:
  fixes y :: ereal
  assumes y: "y \ -\"
  assumes f: "(f \ \) F" and g: "(g \ y) F"
  shows "((\x. f x + g x) \ \) F"
proof -
  have "\C. eventually (\x. g x > ereal C) F"
  proof (cases y)
    case (real r)
    have "y > y-1" using y real by (simp add: ereal_between(1))
    then have "eventually (\x. g x > y - 1) F" using g y order_tendsto_iff by auto
    moreover have "y-1 = ereal(real_of_ereal(y-1))"
      by (metis real ereal_eq_1(1) ereal_minus(1) real_of_ereal.simps(1))
    ultimately have "eventually (\x. g x > ereal(real_of_ereal(y - 1))) F" by simp
    then show ?thesis by auto
  next
    case (PInf)
    have "eventually (\x. g x > ereal 0) F" using g PInf by (simp add: tendsto_PInfty)
    then show ?thesis by auto
  qed (simp add: y)
  then obtain C::real where ge: "eventually (\x. g x > ereal C) F" by auto

  {
    fix M::real
    have "eventually (\x. f x > ereal(M - C)) F" using f by (simp add: tendsto_PInfty)
    then have "eventually (\x. (f x > ereal (M-C)) \ (g x > ereal C)) F"
      by (auto simp: ge eventually_conj_iff)
    moreover have "\x. ((f x > ereal (M-C)) \ (g x > ereal C)) \ (f x + g x > ereal M)"
      using ereal_add_strict_mono2 by fastforce
    ultimately have "eventually (\x. f x + g x > ereal M) F" using eventually_mono by force
  }
  then show ?thesis by (simp add: tendsto_PInfty)
qed

text\<open>One would like to deduce the next lemma from the previous one, but the fact
that \<open>- (x + y)\<close> is in general different from \<open>(- x) + (- y)\<close> in ereal creates difficulties,
so it is more efficient to copy the previous proof.\<close>

lemma tendsto_add_ereal_MInf:
  fixes y :: ereal
  assumes y: "y \ \"
  assumes f: "(f \ -\) F" and g: "(g \ y) F"
  shows "((\x. f x + g x) \ -\) F"
proof -
  have "\C. eventually (\x. g x < ereal C) F"
  proof (cases y)
    case (real r)
    have "y < y+1" using y real by (simp add: ereal_between(1))
    then have "eventually (\x. g x < y + 1) F" using g y order_tendsto_iff by force
    moreover have "y+1 = ereal(real_of_ereal (y+1))" by (simp add: real)
    ultimately have "eventually (\x. g x < ereal(real_of_ereal(y + 1))) F" by simp
    then show ?thesis by auto
  next
    case (MInf)
    have "eventually (\x. g x < ereal 0) F" using g MInf by (simp add: tendsto_MInfty)
    then show ?thesis by auto
  qed (simp add: y)
  then obtain C::real where ge: "eventually (\x. g x < ereal C) F" by auto

  {
    fix M::real
    have "eventually (\x. f x < ereal(M - C)) F" using f by (simp add: tendsto_MInfty)
    then have "eventually (\x. (f x < ereal (M- C)) \ (g x < ereal C)) F"
      by (auto simp: ge eventually_conj_iff)
    moreover have "\x. ((f x < ereal (M-C)) \ (g x < ereal C)) \ (f x + g x < ereal M)"
      using ereal_add_strict_mono2 by fastforce
    ultimately have "eventually (\x. f x + g x < ereal M) F" using eventually_mono by force
  }
  then show ?thesis by (simp add: tendsto_MInfty)
qed

lemma tendsto_add_ereal_general1:
  fixes x y :: ereal
  assumes y: "\y\ \ \"
  assumes f: "(f \ x) F" and g: "(g \ y) F"
  shows "((\x. f x + g x) \ x + y) F"
proof (cases x)
  case (real r)
  have a: "\x\ \ \" by (simp add: real)
  show ?thesis by (rule tendsto_add_ereal[OF a, OF y, OF f, OF g])
next
  case PInf
  then show ?thesis using tendsto_add_ereal_PInf assms by force
next
  case MInf
  then show ?thesis using tendsto_add_ereal_MInf assms
    by (metis abs_ereal.simps(3) ereal_MInfty_eq_plus)
qed

lemma tendsto_add_ereal_general2:
  fixes x y :: ereal
  assumes x: "\x\ \ \"
      and f: "(f \ x) F" and g: "(g \ y) F"
  shows "((\x. f x + g x) \ x + y) F"
proof -
  have "((\x. g x + f x) \ x + y) F"
    by (metis (full_types) add.commute f g tendsto_add_ereal_general1 x)
  moreover have "\x. g x + f x = f x + g x" using add.commute by auto
  ultimately show ?thesis by simp
qed

text \<open>The next lemma says that the addition is continuous on \<open>ereal\<close>, except at
the pairs \<open>(-\<infinity>, \<infinity>)\<close> and \<open>(\<infinity>, -\<infinity>)\<close>.\<close>

lemma tendsto_add_ereal_general [tendsto_intros]:
  fixes x y :: ereal
  assumes "\((x=\ \ y=-\) \ (x=-\ \ y=\))"
      and f: "(f \ x) F" and g: "(g \ y) F"
  shows "((\x. f x + g x) \ x + y) F"
proof (cases x)
  case (real r)
  show ?thesis
    using real assms
    by (intro tendsto_add_ereal_general2; auto)
next
  case (PInf)
  then have "y \ -\" using assms by simp
  then show ?thesis using tendsto_add_ereal_PInf PInf assms by auto
next
  case (MInf)
  then have "y \ \" using assms by simp
  then show ?thesis
    by (metis ereal_MInfty_eq_plus tendsto_add_ereal_MInf MInf f g)
qed

subsubsection\<^marker>\<open>tag important\<close> \<open>Continuity of multiplication\<close>

text \<open>In the same way as for addition, we prove that the multiplication is continuous on
ereal times ereal, except at \<open>(\<infinity>, 0)\<close> and \<open>(-\<infinity>, 0)\<close> and \<open>(0, \<infinity>)\<close> and \<open>(0, -\<infinity>)\<close>,
starting with specific situations.\<close>

lemma tendsto_mult_real_ereal:
  assumes "(u \ ereal l) F" "(v \ ereal m) F"
  shows "((\n. u n * v n) \ ereal l * ereal m) F"
proof -
  have ureal: "eventually (\n. u n = ereal(real_of_ereal(u n))) F" by (rule real_lim_then_eventually_real[OF assms(1)])
  then have "((\n. ereal(real_of_ereal(u n))) \ ereal l) F" using assms by auto
  then have limu: "((\n. real_of_ereal(u n)) \ l) F" by auto
  have vreal: "eventually (\n. v n = ereal(real_of_ereal(v n))) F" by (rule real_lim_then_eventually_real[OF assms(2)])
  then have "((\n. ereal(real_of_ereal(v n))) \ ereal m) F" using assms by auto
  then have limv: "((\n. real_of_ereal(v n)) \ m) F" by auto

  {
    fix n assume "u n = ereal(real_of_ereal(u n))" "v n = ereal(real_of_ereal(v n))"
    then have "ereal(real_of_ereal(u n) * real_of_ereal(v n)) = u n * v n"
      by (metis times_ereal.simps(1))
  }
  then have *: "eventually (\n. ereal(real_of_ereal(u n) * real_of_ereal(v n)) = u n * v n) F"
    using eventually_elim2[OF ureal vreal] by auto

  have "((\n. real_of_ereal(u n) * real_of_ereal(v n)) \ l * m) F"
    using tendsto_mult[OF limu limv] by auto
  then have "((\n. ereal(real_of_ereal(u n)) * real_of_ereal(v n)) \ ereal(l * m)) F"
    by auto
  then show ?thesis using * filterlim_cong by fastforce
qed

lemma tendsto_mult_ereal_PInf:
  fixes f g::"_ \ ereal"
  assumes "(f \ l) F" "l>0" "(g \ \) F"
  shows "((\x. f x * g x) \ \) F"
proof -
  obtain a::real where "0 < ereal a" "a < l"
    using assms(2) using ereal_dense2 by blast
  have *: "eventually (\x. f x > a) F"
    using \<open>a < l\<close> assms(1) by (simp add: order_tendsto_iff)
  {
    fix K::real
    define M where "M = max K 1"
    then have "M > 0" by simp
    then have "ereal(M/a) > 0" using \<open>ereal a > 0\<close> by simp
    then have "\x. ((f x > a) \ (g x > M/a)) \ (f x * g x > ereal a * ereal(M/a))"
      using ereal_mult_mono_strict'[where ?c = "M/a", OF \0 < ereal a\] by auto
    moreover have "ereal a * ereal(M/a) = M" using \<open>ereal a > 0\<close> by simp
    ultimately have "\x. ((f x > a) \ (g x > M/a)) \ (f x * g x > M)" by simp
    moreover have "M \ K" unfolding M_def by simp
    ultimately have Imp: "\x. ((f x > a) \ (g x > M/a)) \ (f x * g x > K)"
      using ereal_less_eq(3) le_less_trans by blast

    have "eventually (\x. g x > M/a) F" using assms(3) by (simp add: tendsto_PInfty)
    then have "eventually (\x. (f x > a) \ (g x > M/a)) F"
      using * by (auto simp: eventually_conj_iff)
    then have "eventually (\x. f x * g x > K) F" using eventually_mono Imp by force
  }
  then show ?thesis by (auto simp: tendsto_PInfty)
qed

lemma tendsto_mult_ereal_pos:
  fixes f g::"_ \ ereal"
  assumes "(f \ l) F" "(g \ m) F" "l>0" "m>0"
  shows "((\x. f x * g x) \ l * m) F"
proof (cases)
  assume *: "l = \ \ m = \"
  then show ?thesis
  proof (cases)
    assume "m = \"
    then show ?thesis using tendsto_mult_ereal_PInf assms by auto
  next
    assume "\(m = \)"
    then have "l = \" using * by simp
    then have "((\x. g x * f x) \ l * m) F" using tendsto_mult_ereal_PInf assms by auto
    moreover have "\x. g x * f x = f x * g x" using mult.commute by auto
    ultimately show ?thesis by simp
  qed
next
  assume "\(l = \ \ m = \)"
  then have "l < \" "m < \" by auto
  then obtain lr mr where "l = ereal lr" "m = ereal mr"
    using \<open>l>0\<close> \<open>m>0\<close> by (metis ereal_cases ereal_less(6) not_less_iff_gr_or_eq)
  then show ?thesis using tendsto_mult_real_ereal assms by auto
qed

text \<open>We reduce the general situation to the positive case by multiplying by suitable signs.
Unfortunately, as ereal is not a ring, all the neat sign lemmas are not available there. We
give the bare minimum we need.\<close>

lemma ereal_sgn_abs:
  fixes l::ereal
  shows "sgn(l) * l = abs(l)"
    by (cases l, auto simp: sgn_if ereal_less_uminus_reorder)

lemma sgn_squared_ereal:
  assumes "l \ (0::ereal)"
  shows "sgn(l) * sgn(l) = 1"
  using assms by (cases l, auto simp: one_ereal_def sgn_if)

lemma tendsto_mult_ereal [tendsto_intros]:
  fixes f g::"_ \ ereal"
  assumes "(f \ l) F" "(g \ m) F" "\((l=0 \ abs(m) = \) \ (m=0 \ abs(l) = \))"
  shows "((\x. f x * g x) \ l * m) F"
proof (cases)
  assume "l=0 \ m=0"
  then have "abs(l) \ \" "abs(m) \ \" using assms(3) by auto
  then obtain lr mr where "l = ereal lr" "m = ereal mr" by auto
  then show ?thesis using tendsto_mult_real_ereal assms by auto
next
  have sgn_finite: "\a::ereal. abs(sgn a) \ \"
    by (metis MInfty_neq_ereal(2) PInfty_neq_ereal(2) abs_eq_infinity_cases ereal_times(1) ereal_times(3) ereal_uminus_eq_reorder sgn_ereal.elims)
  then have sgn_finite2: "\a b::ereal. abs(sgn a * sgn b) \ \"
    by (metis abs_eq_infinity_cases abs_ereal.simps(2) abs_ereal.simps(3) ereal_mult_eq_MInfty ereal_mult_eq_PInfty)
  assume "\(l=0 \ m=0)"
  then have "l \ 0" "m \ 0" by auto
  then have "abs(l) > 0" "abs(m) > 0"
    by (metis abs_ereal_ge0 abs_ereal_less0 abs_ereal_pos ereal_uminus_uminus ereal_uminus_zero less_le not_less)+
  then have "sgn(l) * l > 0" "sgn(m) * m > 0" using ereal_sgn_abs by auto
  moreover have "((\x. sgn(l) * f x) \ (sgn(l) * l)) F"
    by (rule tendsto_cmult_ereal, auto simp: sgn_finite assms(1))
  moreover have "((\x. sgn(m) * g x) \ (sgn(m) * m)) F"
    by (rule tendsto_cmult_ereal, auto simp: sgn_finite assms(2))
  ultimately have *: "((\x. (sgn(l) * f x) * (sgn(m) * g x)) \ (sgn(l) * l) * (sgn(m) * m)) F"
    using tendsto_mult_ereal_pos by force
  have "((\x. (sgn(l) * sgn(m)) * ((sgn(l) * f x) * (sgn(m) * g x))) \ (sgn(l) * sgn(m)) * ((sgn(l) * l) * (sgn(m) * m))) F"
    by (rule tendsto_cmult_ereal, auto simp: sgn_finite2 *)
  moreover have "\x. (sgn(l) * sgn(m)) * ((sgn(l) * f x) * (sgn(m) * g x)) = f x * g x"
    by (metis mult.left_neutral sgn_squared_ereal[OF \<open>l \<noteq> 0\<close>] sgn_squared_ereal[OF \<open>m \<noteq> 0\<close>] mult.assoc mult.commute)
  moreover have "(sgn(l) * sgn(m)) * ((sgn(l) * l) * (sgn(m) * m)) = l * m"
    by (metis mult.left_neutral sgn_squared_ereal[OF \<open>l \<noteq> 0\<close>] sgn_squared_ereal[OF \<open>m \<noteq> 0\<close>] mult.assoc mult.commute)
  ultimately show ?thesis by auto
qed

lemma tendsto_cmult_ereal_general [tendsto_intros]:
  fixes f::"_ \ ereal" and c::ereal
  assumes "(f \ l) F" "\ (l=0 \ abs(c) = \)"
  shows "((\x. c * f x) \ c * l) F"
by (cases "c = 0", auto simp: assms tendsto_mult_ereal)

subsubsection\<^marker>\<open>tag important\<close> \<open>Continuity of division\<close>

lemma tendsto_inverse_ereal_PInf:
  fixes u::"_ \ ereal"
  assumes "(u \ \) F"
  shows "((\x. 1/ u x) \ 0) F"
proof -
  {
    fix e::real assume "e>0"
    have "1/e < \" by auto
    then have "eventually (\n. u n > 1/e) F" using assms(1) by (simp add: tendsto_PInfty)
    moreover
    {
      fix z::ereal assume "z>1/e"
      then have "z>0" using \<open>e>0\<close> using less_le_trans not_le by fastforce
      then have "1/z \ 0" by auto
      moreover have "1/z < e"
      proof (cases z)
        case (real r)
        then show ?thesis
          using \<open>0 < e\<close> \<open>0 < z\<close> \<open>ereal (1 / e) < z\<close> divide_less_eq ereal_divide_less_pos by fastforce
      qed (use \<open>0 < e\<close> \<open>0 < z\<close> in auto)
      ultimately have "1/z \ 0" "1/z < e" by auto
    }
    ultimately have "eventually (\n. 1/u nn. 1/u n\0) F" by (auto simp: eventually_mono)
  } note * = this
  show ?thesis
  proof (subst order_tendsto_iff, auto)
    fix a::ereal assume "a<0"
    then show "eventually (\n. 1/u n > a) F" using *(2) eventually_mono less_le_trans linordered_field_no_ub by fastforce
  next
    fix a::ereal assume "a>0"
    then obtain e::real where "e>0" "a>e" using ereal_dense2 ereal_less(2) by blast
    then have "eventually (\n. 1/u n < e) F" using *(1) by auto
    then show "eventually (\n. 1/u n < a) F" using \a>e\ by (metis (mono_tags, lifting) eventually_mono less_trans)
  qed
qed

text \<open>The next lemma deserves to exist by itself, as it is so common and useful.\<close>

lemma tendsto_inverse_real [tendsto_intros]:
  fixes u::"_ \ real"
  shows "(u \ l) F \ l \ 0 \ ((\x. 1/ u x) \ 1/l) F"
  using tendsto_inverse unfolding inverse_eq_divide .

lemma tendsto_inverse_ereal [tendsto_intros]:
  fixes u::"_ \ ereal"
  assumes "(u \ l) F" "l \ 0"
  shows "((\x. 1/ u x) \ 1/l) F"
proof (cases l)
  case (real r)
  then have "r \ 0" using assms(2) by auto
  then have "1/l = ereal(1/r)" using real by (simp add: one_ereal_def)
  define v where "v = (\n. real_of_ereal(u n))"
  have ureal: "eventually (\n. u n = ereal(v n)) F" unfolding v_def using real_lim_then_eventually_real assms(1) real by auto
  then have "((\n. ereal(v n)) \ ereal r) F" using assms real v_def by auto
  then have *: "((\n. v n) \ r) F" by auto
  then have "((\n. 1/v n) \ 1/r) F" using \r \ 0\ tendsto_inverse_real by auto
  then have lim: "((\n. ereal(1/v n)) \ 1/l) F" using \1/l = ereal(1/r)\ by auto

  have "r \ -{0}" "open (-{(0::real)})" using \r \ 0\ by auto
  then have "eventually (\n. v n \ -{0}) F" using * using topological_tendstoD by blast
  then have "eventually (\n. v n \ 0) F" by auto
  moreover
  {
    fix n assume H: "v n \ 0" "u n = ereal(v n)"
    then have "ereal(1/v n) = 1/ereal(v n)" by (simp add: one_ereal_def)
    then have "ereal(1/v n) = 1/u n" using H(2) by simp
  }
  ultimately have "eventually (\n. ereal(1/v n) = 1/u n) F" using ureal eventually_elim2 by force
  with Lim_transform_eventually[OF lim this] show ?thesis by simp
next
  case (PInf)
  then have "1/l = 0" by auto
  then show ?thesis using tendsto_inverse_ereal_PInf assms PInf by auto
next
  case (MInf)
  then have "1/l = 0" by auto
  have "1/z = -1/ -z" if "z < 0" for z::ereal
    apply (cases z) using divide_ereal_def \<open> z < 0 \<close> by auto
  moreover have "eventually (\n. u n < 0) F" by (metis (no_types) MInf assms(1) tendsto_MInfty zero_ereal_def)
  ultimately have *: "eventually (\n. -1/-u n = 1/u n) F" by (simp add: eventually_mono)

  define v where "v = (\n. - u n)"
  have "(v \ \) F" unfolding v_def using MInf assms(1) tendsto_uminus_ereal by fastforce
  then have "((\n. 1/v n) \ 0) F" using tendsto_inverse_ereal_PInf by auto
  then have "((\n. -1/v n) \ 0) F" using tendsto_uminus_ereal by fastforce
  then show ?thesis unfolding v_def using Lim_transform_eventually[OF _ *] \<open> 1/l = 0 \<close> by auto
qed

lemma tendsto_divide_ereal [tendsto_intros]:
  fixes f g::"_ \ ereal"
  assumes "(f \ l) F" "(g \ m) F" "m \ 0" "\(abs(l) = \ \ abs(m) = \)"
  shows "((\x. f x / g x) \ l / m) F"
proof -
  define h where "h = (\x. 1/ g x)"
  have *: "(h \ 1/m) F" unfolding h_def using assms(2) assms(3) tendsto_inverse_ereal by auto
  have "((\x. f x * h x) \ l * (1/m)) F"
    apply (rule tendsto_mult_ereal[OF assms(1) *]) using assms(3) assms(4) by (auto simp: divide_ereal_def)
  moreover have "f x * h x = f x / g x" for x unfolding h_def by (simp add: divide_ereal_def)
  moreover have "l * (1/m) = l/m" by (simp add: divide_ereal_def)
  ultimately show ?thesis unfolding h_def using Lim_transform_eventually by auto
qed

subsubsection \<open>Further limits\<close>

text \<open>The assumptions of @{thm tendsto_diff_ereal} are too strong, we weaken them here.\<close>

lemma tendsto_diff_ereal_general [tendsto_intros]:
  fixes u v::"'a \ ereal"
  assumes "(u \ l) F" "(v \ m) F" "\((l = \ \ m = \) \ (l = -\ \ m = -\))"
  shows "((\n. u n - v n) \ l - m) F"
proof -
  have "\ = l \ ((\a. u a + - v a) \ l + - m) F"
      by (metis (no_types) assms ereal_uminus_uminus tendsto_add_ereal_general tendsto_uminus_ereal)
  then have "((\n. u n + (-v n)) \ l + (-m)) F"
    by (simp add: assms ereal_uminus_eq_reorder tendsto_add_ereal_general)
  then show ?thesis
    by (simp add: minus_ereal_def)
qed

lemma id_nat_ereal_tendsto_PInf [tendsto_intros]:
  "(\ n::nat. real n) \ \"
by (simp add: filterlim_real_sequentially tendsto_PInfty_eq_at_top)

lemma tendsto_at_top_pseudo_inverse [tendsto_intros]:
  fixes u::"nat \ nat"
  assumes "LIM n sequentially. u n :> at_top"
  shows "LIM n sequentially. Inf {N. u N \ n} :> at_top"
proof -
  {
    fix C::nat
    define M where "M = Max {u n| n. n \ C}+1"
    {
      fix n assume "n \ M"
      have "eventually (\N. u N \ n) sequentially" using assms
        by (simp add: filterlim_at_top)
      then have *: "{N. u N \ n} \ {}" by force

      have "N > C" if "u N \ n" for N
      proof (rule ccontr)
        assume "\(N > C)"
        then have "u N \ Max {u n| n. n \ C}"
          using Max_ge by (simp add: setcompr_eq_image not_less)
        then show False using \<open>u N \<ge> n\<close> \<open>n \<ge> M\<close> unfolding M_def by auto
      qed
      then have **: "{N. u N \ n} \ {C..}" by fastforce
      have "Inf {N. u N \ n} \ C"
        by (metis "*" "**" Inf_nat_def1 atLeast_iff subset_eq)
    }
    then have "eventually (\n. Inf {N. u N \ n} \ C) sequentially"
      using eventually_sequentially by auto
  }
  then show ?thesis using filterlim_at_top by auto
qed

lemma pseudo_inverse_finite_set:
  fixes u::"nat \ nat"
  assumes "LIM n sequentially. u n :> at_top"
  shows "finite {N. u N \ n}"
proof -
  fix n
  have "eventually (\N. u N \ n+1) sequentially" using assms
    by (simp add: filterlim_at_top)
  then obtain N1 where N1: "\N. N \ N1 \ u N \ n + 1"
    using eventually_sequentially by auto
  have "{N. u N \ n} \ {..
    by (metis (no_types, lifting) N1 Suc_eq_plus1 lessThan_iff less_le_not_le mem_Collect_eq nle_le not_less_eq_eq subset_eq)
  then show "finite {N. u N \ n}" by (simp add: finite_subset)
qed

lemma tendsto_at_top_pseudo_inverse2 [tendsto_intros]:
  fixes u::"nat \ nat"
  assumes "LIM n sequentially. u n :> at_top"
  shows "LIM n sequentially. Max {N. u N \ n} :> at_top"
proof -
  {
    fix N0::nat
    have "N0 \ Max {N. u N \ n}" if "n \ u N0" for n
      by (simp add: assms pseudo_inverse_finite_set that)
    then have "eventually (\n. N0 \ Max {N. u N \ n}) sequentially"
      using eventually_sequentially by blast
  }
  then show ?thesis using filterlim_at_top by auto
qed

lemma ereal_truncation_top [tendsto_intros]:
  fixes x::ereal
  shows "(\n::nat. min x n) \ x"
proof (cases x)
  case (real r)
  then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
  then have "min x n = x" if "n \ K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
  then have "eventually (\n. min x n = x) sequentially" using eventually_at_top_linorder by blast
  then show ?thesis by (simp add: tendsto_eventually)
next
  case (PInf)
  then have "min x n = n" for n::nat by (auto simp: min_def)
  then show ?thesis using id_nat_ereal_tendsto_PInf PInf by auto
next
  case (MInf)
  then have "min x n = x" for n::nat by (auto simp: min_def)
  then show ?thesis by auto
qed

lemma ereal_truncation_real_top [tendsto_intros]:
  fixes x::ereal
  assumes "x \ - \"
  shows "(\n::nat. real_of_ereal(min x n)) \ x"
proof (cases x)
  case (real r)
  then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
  then have "min x n = x" if "n \ K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
  then have "real_of_ereal(min x n) = r" if "n \ K" for n using real that by auto
  then have "eventually (\n. real_of_ereal(min x n) = r) sequentially" using eventually_at_top_linorder by blast
  then have "(\n. real_of_ereal(min x n)) \ r" by (simp add: tendsto_eventually)
  then show ?thesis using real by auto
next
  case (PInf)
  then have "real_of_ereal(min x n) = n" for n::nat by (auto simp: min_def)
  then show ?thesis using id_nat_ereal_tendsto_PInf PInf by auto
qed (simp add: assms)

lemma ereal_truncation_bottom [tendsto_intros]:
  fixes x::ereal
  shows "(\n::nat. max x (- real n)) \ x"
proof (cases x)
  case (real r)
  then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
  then have "max x (-real n) = x" if "n \ K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
  then have "eventually (\n. max x (-real n) = x) sequentially" using eventually_at_top_linorder by blast
  then show ?thesis by (simp add: tendsto_eventually)
next
  case (MInf)
  then have "max x (-real n) = (-1)* ereal(real n)" for n::nat by (auto simp: max_def)
  moreover have "(\n. (-1)* ereal(real n)) \ -\"
    using tendsto_cmult_ereal[of "-1", OF _ id_nat_ereal_tendsto_PInf] by (simp add: one_ereal_def)
  ultimately show ?thesis using MInf by auto
next
  case (PInf)
  then have "max x (-real n) = x" for n::nat by (auto simp: max_def)
  then show ?thesis by auto
qed

lemma ereal_truncation_real_bottom [tendsto_intros]:
  fixes x::ereal
  assumes "x \ \"
  shows "(\n::nat. real_of_ereal(max x (- real n))) \ x"
proof (cases x)
  case (real r)
  then obtain K::nat where "K>0" "K > abs(r)" using reals_Archimedean2 gr0I by auto
  then have "max x (-real n) = x" if "n \ K" for n apply (subst real, subst real, auto) using that eq_iff by fastforce
  then have "real_of_ereal(max x (-real n)) = r" if "n \ K" for n using real that by auto
  then have "eventually (\n. real_of_ereal(max x (-real n)) = r) sequentially" using eventually_at_top_linorder by blast
  then have "(\n. real_of_ereal(max x (-real n))) \ r" by (simp add: tendsto_eventually)
  then show ?thesis using real by auto
next
  case (MInf)
  then have "real_of_ereal(max x (-real n)) = (-1)* ereal(real n)" for n::nat by (auto simp: max_def)
  moreover have "(\n. (-1)* ereal(real n)) \ -\"
    using tendsto_cmult_ereal[of "-1", OF _ id_nat_ereal_tendsto_PInf] by (simp add: one_ereal_def)
  ultimately show ?thesis using MInf by auto
qed (simp add: assms)

text \<open>the next one is copied from \<open>tendsto_sum\<close>.\<close>
lemma tendsto_sum_ereal [tendsto_intros]:
  fixes f :: "'a \ 'b \ ereal"
  assumes "\i. i \ S \ (f i \ a i) F"
          "\i. abs(a i) \ \"
  shows "((\x. \i\S. f i x) \ (\i\S. a i)) F"
proof (cases "finite S")
  assume "finite S" then show ?thesis using assms
    by (induct, simp, simp add: tendsto_add_ereal_general2 assms)
qed(simp)

lemma continuous_ereal_abs:
  "continuous_on (UNIV::ereal set) abs"
proof -
  have "continuous_on ({..0} \ {(0::ereal)..}) abs"
  proof (intro continuous_on_closed_Un continuous_intros)
    show "continuous_on {..0::ereal} abs"
      by (metis abs_ereal_ge0 abs_ereal_less0 continuous_on_eq antisym_conv1 atMost_iff continuous_uminus_ereal ereal_uminus_zero)
    show "continuous_on {0::ereal..} abs"
      by (metis abs_ereal_ge0 atLeast_iff continuous_on_eq continuous_on_id)
  qed
  moreover have "(UNIV::ereal set) = {..0} \ {(0::ereal)..}" by auto
  ultimately show ?thesis by auto
qed

lemmas continuous_on_compose_ereal_abs[continuous_intros] =
  continuous_on_compose2[OF continuous_ereal_abs _ subset_UNIV]

lemma tendsto_abs_ereal [tendsto_intros]:
  assumes "(u \ (l::ereal)) F"
  shows "((\n. abs(u n)) \ abs l) F"
using continuous_ereal_abs assms by (metis UNIV_I continuous_on tendsto_compose)

lemma ereal_minus_real_tendsto_MInf [tendsto_intros]:
  "(\x. ereal (- real x)) \ - \"
by (subst uminus_ereal.simps(1)[symmetric], intro tendsto_intros)

subsection \<open>Extended-Nonnegative-Real.thy\<close> (*FIX title *)

lemma tendsto_diff_ennreal_general [tendsto_intros]:
  fixes u v::"'a \ ennreal"
  assumes "(u \ l) F" "(v \ m) F" "\(l = \ \ m = \)"
  shows "((\n. u n - v n) \ l - m) F"
proof -
  have "((\n. e2ennreal(enn2ereal(u n) - enn2ereal(v n))) \ e2ennreal(enn2ereal l - enn2ereal m)) F"
    by (intro tendsto_intros) (use assms in auto)
  then show ?thesis by auto
qed

lemma tendsto_mult_ennreal [tendsto_intros]:
  fixes l m::ennreal
  assumes "(u \ l) F" "(v \ m) F" "\((l = 0 \ m = \) \ (l = \ \ m = 0))"
  shows "((\n. u n * v n) \ l * m) F"
proof -
  have "((\n. e2ennreal(enn2ereal (u n) * enn2ereal (v n))) \ e2ennreal(enn2ereal l * enn2ereal m)) F"
    by (intro tendsto_intros) (use assms enn2ereal_inject zero_ennreal.rep_eq in fastforce)+
  moreover have "e2ennreal(enn2ereal (u n) * enn2ereal (v n)) = u n * v n" for n
    by (subst times_ennreal.abs_eq[symmetric], auto simp: eq_onp_same_args)
  moreover have "e2ennreal(enn2ereal l * enn2ereal m) = l * m"
    by (subst times_ennreal.abs_eq[symmetric], auto simp: eq_onp_same_args)
  ultimately show ?thesis
    by auto
qed

subsection \<open>monoset\<close> (*FIX ME title *)

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 _ \<open>a \<in> S\<close>]
      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 \<open>x \<in> S\<close> \<open>a \<notin> S\<close> 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. \<forall>S. open S \<longrightarrow> mono_set S \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> 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" "Inf (f ` (Collect P)) \ S"
  {
    fix x
    assume "P x"
    then have "Inf (f ` (Collect P)) \ 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 \ Inf (f ` (Collect P)) \ 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 "Inf (f ` {x. B < f x}) \ y"
      using P by auto
    moreover have "B \ Inf (f ` {x. B < f x})"
      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. \<forall>S. open S \<longrightarrow> mono_set (uminus ` S) \<longrightarrow> l \<in> S \<longrightarrow> eventually (\<lambda>x. f x \<in> 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)" "Sup (f ` (Collect P)) \ S"
  {
    fix x
    assume "P x"
    then have "f x \ Sup (f ` (Collect P))"
      by (intro complete_lattice_class.SUP_upper) simp
    with S(1)[unfolded mono_set, rule_format, of "- Sup (f ` (Collect P))" "- 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 \ Sup (f ` (Collect P))"
  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 \ Sup (f ` {x. f x < B})"
      using P by auto
    moreover have "Sup (f ` {x. f x < B}) \ 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"
    then have "\N. \n\N. x n \ S"
        by (metis \<open>x0 \<le> liminf x\<close> ereal_open_mono_set greaterThan_iff liminf_bounded_iff om UNIV_I)
  }
  then show "?P x0"
    by auto
qed

lemma limsup_finite_then_bounded:
  fixes u::"nat \ real"
  assumes "limsup u < \"
  shows "\C. \n. u n \ C"
proof -
  obtain C where C: "limsup u < C" "C < \" using assms ereal_dense2 by blast
  then have "C = ereal(real_of_ereal C)" using ereal_real by force
  have "eventually (\n. u n < C) sequentially"
    using SUP_lessD eventually_mono C(1)
    by (fastforce simp: INF_less_iff Limsup_def)
  then obtain N where N: "\n. n \ N \ u n < C" using eventually_sequentially by auto
  define D where "D = max (real_of_ereal C) (Max {u n |n. n \ N})"
  have "\n. u n \ D"
  proof -
    fix n show "u n \ D"
    proof (cases)
      assume *: "n \ N"
      have "u n \ Max {u n |n. n \ N}" by (rule Max_ge, auto simp: *)
      then show "u n \ D" unfolding D_def by linarith
    next
      assume "\(n \ N)"
      then have "n \ N" by simp
      then have "u n < C" using N by auto
      then have "u n < real_of_ereal C" using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
      then show "u n \ D" unfolding D_def by linarith
    qed
  qed
  then show ?thesis by blast
qed

lemma liminf_finite_then_bounded_below:
  fixes u::"nat \ real"
  assumes "liminf u > -\"
  shows "\C. \n. u n \ C"
proof -
  obtain C where C: "liminf u > C" "C > -\" using assms using ereal_dense2 by blast
  then have "C = ereal(real_of_ereal C)" using ereal_real by force
  have "eventually (\n. u n > C) sequentially"
    using eventually_elim2 less_INF_D C(1)
    by (fastforce simp: less_SUP_iff Liminf_def)
  then obtain N where N: "\n. n \ N \ u n > C" using eventually_sequentially by auto
  define D where "D = min (real_of_ereal C) (Min {u n |n. n \ N})"
  have "\n. u n \ D"
  proof -
    fix n show "u n \ D"
    proof (cases)
      assume *: "n \ N"
      have "u n \ Min {u n |n. n \ N}" by (rule Min_le, auto simp: *)
      then show "u n \ D" unfolding D_def by linarith
    next
      assume "\(n \ N)"
      then have "n \ N" by simp
      then have "u n > C" using N by auto
      then have "u n > real_of_ereal C"
        using \<open>C = ereal(real_of_ereal C)\<close> less_ereal.simps(1) by fastforce
      then show "u n \ D" unfolding D_def by linarith
    qed
  qed
  then show ?thesis by blast
qed

lemma liminf_upper_bound:
  fixes u:: "nat \ ereal"
  assumes "liminf u < l"
  shows "\N>k. u N < l"
by (metis assms gt_ex less_le_trans liminf_bounded_iff not_less)

lemma limsup_shift:
  "limsup (\n. u (n+1)) = limsup u"
proof -
  have "(SUP m\{n+1..}. u m) = (SUP m\{n..}. u (m + 1))" for n
    by (rule SUP_eq) (use Suc_le_D in auto)
  then have a: "(INF n. SUP m\{n..}. u (m + 1)) = (INF n. (SUP m\{n+1..}. u m))" by auto
  have b: "(INF n. (SUP m\{n+1..}. u m)) = (INF n\{1..}. (SUP m\{n..}. u m))"
    by (rule INF_eq) (use Suc_le_D in auto)
  have "(INF n\{1..}. v n) = (INF n. v n)" if "decseq v" for v::"nat \ 'a"
    by (rule INF_eq) (use \<open>decseq v\<close> decseq_Suc_iff in auto)
  moreover have "decseq (\n. (SUP m\{n..}. u m))" by (simp add: SUP_subset_mono decseq_def)
  ultimately have c: "(INF n\{1..}. (SUP m\{n..}. u m)) = (INF n. (SUP m\{n..}. u m))" by simp
  have "(INF n. Sup (u ` {n..})) = (INF n. SUP m\{n..}. u (m + 1))" using a b c by simp
  then show ?thesis by (auto cong: limsup_INF_SUP)
qed

lemma limsup_shift_k:
  "limsup (\n. u (n+k)) = limsup u"
proof (induction k)
  case (Suc k)
  have "limsup (\n. u (n+k+1)) = limsup (\n. u (n+k))" using limsup_shift[where ?u="\n. u(n+k)"] by simp
  then show ?case using Suc.IH by simp
qed (auto)

lemma liminf_shift:
  "liminf (\n. u (n+1)) = liminf u"
proof -
  have "(INF m\{n+1..}. u m) = (INF m\{n..}. u (m + 1))" for n
    by (rule INF_eq) (use Suc_le_D in auto)
  then have a: "(SUP n. INF m\{n..}. u (m + 1)) = (SUP n. (INF m\{n+1..}. u m))" by auto
  have b: "(SUP n. (INF m\{n+1..}. u m)) = (SUP n\{1..}. (INF m\{n..}. u m))"
    by (rule SUP_eq) (use Suc_le_D in auto)
  have "(SUP n\{1..}. v n) = (SUP n. v n)" if "incseq v" for v::"nat \ 'a"
    by (rule SUP_eq) (use \<open>incseq v\<close> incseq_Suc_iff in auto)
  moreover have "incseq (\n. (INF m\{n..}. u m))" by (simp add: INF_superset_mono mono_def)
  ultimately have c: "(SUP n\{1..}. (INF m\{n..}. u m)) = (SUP n. (INF m\{n..}. u m))" by simp
  have "(SUP n. Inf (u ` {n..})) = (SUP n. INF m\{n..}. u (m + 1))" using a b c by simp
  then show ?thesis by (auto cong: liminf_SUP_INF)
qed

lemma liminf_shift_k:
  "liminf (\n. u (n+k)) = liminf u"
proof (induction k)
  case (Suc k)
  have "liminf (\n. u (n+k+1)) = liminf (\n. u (n+k))"
    using liminf_shift[where ?u="\n. u(n+k)"] by simp
  then show ?case using Suc.IH by simp
qed (auto)

lemma Limsup_obtain:
  fixes u::"_ \ 'a :: complete_linorder"
  assumes "Limsup F u > c"
  shows "\i. u i > c"
proof -
  have "(INF P\{P. eventually P F}. SUP x\{x. P x}. u x) > c" using assms by (simp add: Limsup_def)
  then show ?thesis by (metis eventually_True mem_Collect_eq less_INF_D less_SUP_iff)
qed

text \<open>The next lemma is extremely useful, as it often makes it possible to reduce statements
about limsups to statements about limits.\<close>

lemma limsup_subseq_lim:
  fixes u::"nat \ 'a :: {complete_linorder, linorder_topology}"
  shows "\r::nat\nat. strict_mono r \ (u o r) \ limsup u"
proof (cases)
  assume "\n. \p>n. \m\p. u m \ u p"
  then have "\r. \n. (\m\r n. u m \ u (r n)) \ r n < r (Suc n)"
    by (intro dependent_nat_choice) (auto simp: conj_commute)
  then obtain r :: "nat \ nat" where "strict_mono r" and mono: "\n m. r n \ m \ u m \ u (r n)"
    by (auto simp: strict_mono_Suc_iff)
  define umax where "umax = (\n. (SUP m\{n..}. u m))"
  have "decseq umax" unfolding umax_def by (simp add: SUP_subset_mono antimono_def)
  then have "umax \ limsup u" unfolding umax_def by (metis LIMSEQ_INF limsup_INF_SUP)
  then have *: "(umax o r) \ limsup u" by (simp add: LIMSEQ_subseq_LIMSEQ \strict_mono r\)
  have "\n. umax(r n) = u(r n)" unfolding umax_def using mono
    by (metis SUP_le_iff antisym atLeast_def mem_Collect_eq order_refl)
  then have "umax o r = u o r" unfolding o_def by simp
  then have "(u o r) \ limsup u" using * by simp
  then show ?thesis using \<open>strict_mono r\<close> by blast
next
  assume "\ (\n. \p>n. (\m\p. u m \ u p))"
  then obtain N where N: "\p. p > N \ \m>p. u p < u m" by (force simp: not_le le_less)
  have "\r. \n. N < r n \ r n < r (Suc n) \ (\i\ {N<..r (Suc n)}. u i \ u (r (Suc n)))"
  proof (rule dependent_nat_choice)
    fix x assume "N < x"
    then have a: "finite {N<..x}" "{N<..x} \ {}" by simp_all
    have "Max {u i |i. i \ {N<..x}} \ {u i |i. i \ {N<..x}}" apply (rule Max_in) using a by (auto)
    then obtain p where "p \ {N<..x}" and upmax: "u p = Max{u i |i. i \ {N<..x}}" by auto
    define U where "U = {m. m > p \ u p < u m}"
    have "U \ {}" unfolding U_def using N[of p] \p \ {N<..x}\ by auto
    define y where "y = Inf U"
    then have "y \ U" using \U \ {}\ by (simp add: Inf_nat_def1)
    have a: "\i. i \ {N<..x} \ u i \ u p"
    proof -
      fix i assume "i \ {N<..x}"
      then have "u i \ {u i |i. i \ {N<..x}}" by blast
      then show "u i \ u p" using upmax by simp
    qed
    moreover have "u p < u y" using \<open>y \<in> U\<close> U_def by auto
    ultimately have "y \ {N<..x}" using not_le by blast
    moreover have "y > N" using \<open>y \<in> U\<close> U_def \<open>p \<in> {N<..x}\<close> by auto
    ultimately have "y > x" by auto

    have "\i. i \ {N<..y} \ u i \ u y"
    proof -
      fix i assume "i \ {N<..y}" show "u i \ u y"
      proof (cases)
        assume "i = y"
        then show ?thesis by simp
      next
        assume "\(i=y)"
        then have i:"i \ {N<..i \ {N<..y}\ by simp
        have "u i \ u p"
        proof (cases)
          assume "i \ x"
          then have "i \ {N<..x}" using i by simp
          then show ?thesis using a by simp
        next
          assume "\(i \ x)"
          then have "i > x" by simp
          then have *: "i > p" using \<open>p \<in> {N<..x}\<close> by simp
          have "i < Inf U" using i y_def by simp
          then have "i \ U" using Inf_nat_def not_less_Least by auto
          then show ?thesis using U_def * by auto
        qed
        then show "u i \ u y" using \u p < u y\ by auto
      qed
    qed
    then have "N < y \ x < y \ (\i\{N<..y}. u i \ u y)" using \y > x\ \y > N\ by auto
    then show "\y>N. x < y \ (\i\{N<..y}. u i \ u y)" by auto
  qed (auto)
  then obtain r where r: "\n. N < r n \ r n < r (Suc n) \ (\i\ {N<..r (Suc n)}. u i \ u (r (Suc n)))" by auto
  have "strict_mono r" using r by (auto simp: strict_mono_Suc_iff)
  have "incseq (u o r)" unfolding o_def using r by (simp add: incseq_SucI order.strict_implies_order)
  then have "(u o r) \ (SUP n. (u o r) n)" using LIMSEQ_SUP by blast
  then have "limsup (u o r) = (SUP n. (u o r) n)" by (simp add: lim_imp_Limsup)
  moreover have "limsup (u o r) \ limsup u" using \strict_mono r\ by (simp add: limsup_subseq_mono)
  ultimately have "(SUP n. (u o r) n) \ limsup u" by simp

  {
    fix i assume i: "i \ {N<..}"
    obtain n where "i < r (Suc n)" using \<open>strict_mono r\<close> using Suc_le_eq seq_suble by blast
    then have "i \ {N<..r(Suc n)}" using i by simp
    then have "u i \ u (r(Suc n))" using r by simp
    then have "u i \ (SUP n. (u o r) n)" unfolding o_def by (meson SUP_upper2 UNIV_I)
  }
  then have "(SUP i\{N<..}. u i) \ (SUP n. (u o r) n)" using SUP_least by blast
  then have "limsup u \ (SUP n. (u o r) n)" unfolding Limsup_def
    by (metis (mono_tags, lifting) INF_lower2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
  then have "limsup u = (SUP n. (u o r) n)" using \<open>(SUP n. (u o r) n) \<le> limsup u\<close> by simp
  then have "(u o r) \ limsup u" using \(u o r) \ (SUP n. (u o r) n)\ by simp
  then show ?thesis using \<open>strict_mono r\<close> by auto
qed

lemma liminf_subseq_lim:
  fixes u::"nat \ 'a :: {complete_linorder, linorder_topology}"
  shows "\r::nat\nat. strict_mono r \ (u o r) \ liminf u"
proof (cases)
  assume "\n. \p>n. \m\p. u m \ u p"
  then have "\r. \n. (\m\r n. u m \ u (r n)) \ r n < r (Suc n)"
    by (intro dependent_nat_choice) (auto simp: conj_commute)
  then obtain r :: "nat \ nat" where "strict_mono r" and mono: "\n m. r n \ m \ u m \ u (r n)"
    by (auto simp: strict_mono_Suc_iff)
  define umin where "umin = (\n. (INF m\{n..}. u m))"
  have "incseq umin" unfolding umin_def by (simp add: INF_superset_mono incseq_def)
  then have "umin \ liminf u" unfolding umin_def by (metis LIMSEQ_SUP liminf_SUP_INF)
  then have *: "(umin o r) \ liminf u" by (simp add: LIMSEQ_subseq_LIMSEQ \strict_mono r\)
  have "\n. umin(r n) = u(r n)" unfolding umin_def using mono
    by (metis le_INF_iff antisym atLeast_def mem_Collect_eq order_refl)
  then have "umin o r = u o r" unfolding o_def by simp
  then have "(u o r) \ liminf u" using * by simp
  then show ?thesis using \<open>strict_mono r\<close> by blast
next
  assume "\ (\n. \p>n. (\m\p. u m \ u p))"
  then obtain N where N: "\p. p > N \ \m>p. u p > u m" by (force simp: not_le le_less)
  have "\r. \n. N < r n \ r n < r (Suc n) \ (\i\ {N<..r (Suc n)}. u i \ u (r (Suc n)))"
  proof (rule dependent_nat_choice)
    fix x assume "N < x"
    then have a: "finite {N<..x}" "{N<..x} \ {}" by simp_all
    have "Min {u i |i. i \ {N<..x}} \ {u i |i. i \ {N<..x}}" apply (rule Min_in) using a by (auto)
    then obtain p where "p \ {N<..x}" and upmin: "u p = Min{u i |i. i \ {N<..x}}" by auto
    define U where "U = {m. m > p \ u p > u m}"
    have "U \ {}" unfolding U_def using N[of p] \p \ {N<..x}\ by auto
    define y where "y = Inf U"
    then have "y \ U" using \U \ {}\ by (simp add: Inf_nat_def1)
    have a: "\i. i \ {N<..x} \ u i \ u p"
    proof -
      fix i assume "i \ {N<..x}"
      then have "u i \ {u i |i. i \ {N<..x}}" by blast
      then show "u i \ u p" using upmin by simp
    qed
    moreover have "u p > u y" using \<open>y \<in> U\<close> U_def by auto
    ultimately have "y \ {N<..x}" using not_le by blast
    moreover have "y > N" using \<open>y \<in> U\<close> U_def \<open>p \<in> {N<..x}\<close> by auto
    ultimately have "y > x" by auto

    have "\i. i \ {N<..y} \ u i \ u y"
    proof -
      fix i assume "i \ {N<..y}" show "u i \ u y"
      proof (cases)
        assume "i = y"
        then show ?thesis by simp
      next
        assume "\(i=y)"
        then have i:"i \ {N<..i \ {N<..y}\ by simp
        have "u i \ u p"
        proof (cases)
          assume "i \ x"
          then show ?thesis using a \<open>i \<in> {N<..y}\<close> by force
        next
          assume "\(i \ x)"
          then have "i > x" by simp
          then have *: "i > p" using \<open>p \<in> {N<..x}\<close> by simp
          have "i < Inf U" using i y_def by simp
          then have "i \ U" using Inf_nat_def not_less_Least by auto
          then show ?thesis using U_def * by auto
        qed
        then show "u i \ u y" using \u p > u y\ by auto
      qed
    qed
    then have "N < y \ x < y \ (\i\{N<..y}. u i \ u y)" using \y > x\ \y > N\ by auto
    then show "\y>N. x < y \ (\i\{N<..y}. u i \ u y)" by auto
  qed (auto)
  then obtain r :: "nat \ nat"
    where r: "\n. N < r n \ r n < r (Suc n) \ (\i\ {N<..r (Suc n)}. u i \ u (r (Suc n)))" by auto
  have "strict_mono r" using r by (auto simp: strict_mono_Suc_iff)
  have "decseq (u o r)" unfolding o_def using r by (simp add: decseq_SucI order.strict_implies_order)
  then have "(u o r) \ (INF n. (u o r) n)" using LIMSEQ_INF by blast
  then have "liminf (u o r) = (INF n. (u o r) n)" by (simp add: lim_imp_Liminf)
  moreover have "liminf (u o r) \ liminf u" using \strict_mono r\ by (simp add: liminf_subseq_mono)
  ultimately have "(INF n. (u o r) n) \ liminf u" by simp

  {
    fix i assume i: "i \ {N<..}"
    obtain n where "i < r (Suc n)" using \<open>strict_mono r\<close> using Suc_le_eq seq_suble by blast
    then have "i \ {N<..r(Suc n)}" using i by simp
    then have "u i \ u (r(Suc n))" using r by simp
    then have "u i \ (INF n. (u o r) n)" unfolding o_def by (meson INF_lower2 UNIV_I)
  }
  then have "(INF i\{N<..}. u i) \ (INF n. (u o r) n)" using INF_greatest by blast
  then have "liminf u \ (INF n. (u o r) n)" unfolding Liminf_def
    by (metis (mono_tags, lifting) SUP_upper2 atLeast_Suc_greaterThan atLeast_def eventually_ge_at_top mem_Collect_eq)
  then have "liminf u = (INF n. (u o r) n)" using \<open>(INF n. (u o r) n) \<ge> liminf u\<close> by simp
  then have "(u o r) \ liminf u" using \(u o r) \ (INF n. (u o r) n)\ by simp
  then show ?thesis using \<open>strict_mono r\<close> by auto
qed

text \<open>The following statement about limsups is reduced to a statement about limits using
subsequences thanks to \<open>limsup_subseq_lim\<close>. The statement for limits follows for instance from
\<open>tendsto_add_ereal_general\<close>.\<close>

lemma ereal_limsup_add_mono:
  fixes u v::"nat \ ereal"
--> --------------------

--> maximum size reached

--> --------------------

quality98%

¤ Dauer der Verarbeitung: 0.33 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.