Theory Lambert_W

(*
  File:    Lambert_W.thy
  Author:  Manuel Eberl, TU München

  Definition and basic properties of the two real-valued branches of the Lambert W function,
*)
section ‹The Lambert $W$ Function on the reals›
theory Lambert_W
imports
  Complex_Main
  "HOL-Library.FuncSet"
  "HOL-Real_Asymp.Real_Asymp"
begin

(*<*)
text ‹Some lemmas about asymptotic equivalence:›

lemma asymp_equiv_sandwich':
  fixes f :: "'a ⇒ real"
  assumes "⋀c'. c' ∈ {l<..<c} ⟹ eventually (λx. f x ≥ c' * g x) F"
  assumes "⋀c'. c' ∈ {c<..<u} ⟹ eventually (λx. f x ≤ c' * g x) F"
  assumes "l < c" "c < u" and [simp]: "c ≠ 0"
  shows   "f ∼[F] (λx. c * g x)"
proof -
  have "(λx. f x - c * g x) ∈ o[F](g)"
  proof (rule landau_o.smallI)
    fix e :: real assume e: "e > 0"
    define C1 where "C1 = min (c + e) ((c + u) / 2)"
    have C1: "C1 ∈ {c<..<u}" "C1 - c ≤ e"
      using e assms by (auto simp: C1_def min_def)
    define C2 where "C2 = max (c - e) ((c + l) / 2)"
    have C2: "C2 ∈ {l<..<c}" "c - C2 ≤ e"
      using e assms by (auto simp: C2_def max_def field_simps)

    show "eventually (λx. norm (f x - c * g x) ≤ e * norm (g x)) F"
      using assms(2)[OF C1(1)] assms(1)[OF C2(1)]
    proof eventually_elim
      case (elim x)
      show ?case
      proof (cases "f x ≥ c * g x")
        case True
        hence "norm (f x - c * g x) = f x - c * g x"
          by simp
        also have "… ≤ (C1 - c) * g x"
          using elim by (simp add: algebra_simps)
        also have "… ≤ (C1 - c) * norm (g x)"
          using C1 by (intro mult_left_mono) auto
        also have "… ≤ e * norm (g x)"
          using C1 elim by (intro mult_right_mono) auto
        finally show ?thesis using elim by simp
      next
        case False
        hence "norm (f x - c * g x) = c * g x - f x"
          by simp
        also have "… ≤ (c - C2) * g x"
          using elim by (simp add: algebra_simps)
        also have "… ≤ (c - C2) * norm (g x)"
          using C2 by (intro mult_left_mono) auto
        also have "… ≤ e * norm (g x)"
          using C2 elim by (intro mult_right_mono) auto
        finally show ?thesis using elim by simp
      qed
    qed
  qed
  also have "g ∈ O[F](λx. c * g x)"
    by simp
  finally show ?thesis
    unfolding asymp_equiv_altdef by blast
qed

lemma asymp_equiv_sandwich'':
  fixes f :: "'a ⇒ real"
  assumes "⋀c'. c' ∈ {l<..<1} ⟹ eventually (λx. f x ≥ c' * g x) F"
  assumes "⋀c'. c' ∈ {1<..<u} ⟹ eventually (λx. f x ≤ c' * g x) F"
  assumes "l < 1" "1 < u"
  shows   "f ∼[F] (g)"
  using asymp_equiv_sandwich'[of l 1 g f F u] assms by simp
(*>*)

subsection ‹Properties of the function $x\mapsto x e^{x}$›

lemma exp_times_self_gt:
  assumes "x ≠ -1"
  shows   "x * exp x > -exp (-1::real)"
proof -
  define f where "f = (λx::real. x * exp x)"
  define f' where "f' = (λx::real. (x + 1) * exp x)"
  have "(f has_field_derivative f' x) (at x)" for x
    by (auto simp: f_def f'_def intro!: derivative_eq_intros simp: algebra_simps)
  define l r where "l = min x (-1)" and "r = max x (-1)"

  have "∃z. z > l ∧ z < r ∧ f r - f l = (r - l) * f' z"
    unfolding f_def f'_def l_def r_def using assms
    by (intro MVT2) (auto intro!: derivative_eq_intros simp: algebra_simps)
  then obtain z where z: "z ∈ {l<..<r}" "f r - f l = (r - l) * f' z"
    by auto
  from z have "f x = f (-1) + (x + 1) * f' z"
    using assms by (cases "x ≥ -1") (auto simp: l_def r_def max_def min_def algebra_simps)
  moreover have "sgn ((x + 1) * f' z) = 1"
    using z assms
    by (cases x "(-1) :: real" rule: linorder_cases; cases z "(-1) :: real" rule: linorder_cases)
       (auto simp: f'_def sgn_mult l_def r_def)
  hence "(x + 1) * f' z > 0" using sgn_greater by fastforce
  ultimately show ?thesis by (simp add: f_def)
qed

lemma exp_times_self_ge: "x * exp x ≥ -exp (-1::real)"
  using exp_times_self_gt[of x] by (cases "x = -1") auto

lemma exp_times_self_strict_mono:
  assumes "x ≥ -1" "x < (y :: real)"
  shows   "x * exp x < y * exp y"
  using assms(2)
proof (rule DERIV_pos_imp_increasing_open)
  fix t assume t: "x < t" "t < y"
  have "((λx. x * exp x) has_real_derivative (t + 1) * exp t) (at t)"
    by (auto intro!: derivative_eq_intros simp: algebra_simps)
  moreover have "(t + 1) * exp t > 0"
    using t assms by (intro mult_pos_pos) auto
  ultimately show "∃y. ((λa. a * exp a) has_real_derivative y) (at t) ∧ 0 < y" by blast
qed (auto intro!: continuous_intros)

lemma exp_times_self_strict_antimono:
  assumes "y ≤ -1" "x < (y :: real)"
  shows   "x * exp x > y * exp y"
proof -
  have "-x * exp x < -y * exp y"
    using assms(2)
  proof (rule DERIV_pos_imp_increasing_open)
    fix t assume t: "x < t" "t < y"
    have "((λx. -x * exp x) has_real_derivative (-(t + 1)) * exp t) (at t)"
      by (auto intro!: derivative_eq_intros simp: algebra_simps)
    moreover have "(-(t + 1)) * exp t > 0"
      using t assms by (intro mult_pos_pos) auto
    ultimately show "∃y. ((λa. -a * exp a) has_real_derivative y) (at t) ∧ 0 < y" by blast
  qed (auto intro!: continuous_intros)
  thus ?thesis by simp
qed

lemma exp_times_self_mono:
  assumes "x ≥ -1" "x ≤ (y :: real)"
  shows   "x * exp x ≤ y * exp y"
  using exp_times_self_strict_mono[of x y] assms by (cases "x = y") auto

lemma exp_times_self_antimono:
  assumes "y ≤ -1" "x ≤ (y :: real)"
  shows   "x * exp x ≥ y * exp y"
  using exp_times_self_strict_antimono[of y x] assms by (cases "x = y") auto

lemma exp_times_self_inj: "inj_on (λx::real. x * exp x) {-1..}"
proof
  fix x y :: real
  assume "x ∈ {-1..}" "y ∈ {-1..}" "x * exp x = y * exp y"
  thus "x = y"
    using exp_times_self_strict_mono[of x y] exp_times_self_strict_mono[of y x]
    by (cases x y rule: linorder_cases) auto
qed

lemma exp_times_self_inj': "inj_on (λx::real. x * exp x) {..-1}"
proof
  fix x y :: real
  assume "x ∈ {..-1}" "y ∈ {..-1}" "x * exp x = y * exp y"
  thus "x = y"
    using exp_times_self_strict_antimono[of x y] exp_times_self_strict_antimono[of y x]
    by (cases x y rule: linorder_cases) auto
qed


subsection ‹Definition›

text ‹
  The following are the two branches $W_0(x)$ and $W_{-1}(x)$ of the Lambert $W$ function on the
  real numbers. These are the inverse functions of the function $x\mapsto xe^x$, i.\,e.\ 
  we have $W(x)e^{W(x)} = x$ for both branches wherever they are defined. The two branches
  meet at the point $x = -\frac{1}{e}$.

  $W_0(x)$ is the principal branch, whose domain is $[-\frac{1}{e}; \infty)$ and whose
  range is $[-1; \infty)$.
  $W_{-1}(x)$ has the domain $[-\frac{1}{e}; 0)$ and the range $(-\infty;-1]$.
  Figure~\ref{fig:lambertw} shows plots of these two branches for illustration.
›

text ‹
\definecolor{myblue}{HTML}{3869b1}
\definecolor{myred}{HTML}{cc2428}
\begin{figure}
\begin{center}
\begin{tikzpicture}
  \begin{axis}[
          xmin=-0.5, xmax=6.6, ymin=-3.8, ymax=1.5, axis lines=middle, ytick = {-3, -2, -1, 1}, xtick = {1,...,10}, yticklabel pos = right,
          yticklabel style={right,xshift=1mm},
          extra x tick style={tick label style={above,yshift=1mm}},
          extra x ticks={-0.367879441},
          extra x tick labels={$-\frac{1}{e}$},
          width=\textwidth, height=0.8\textwidth,
          xlabel={$x$}, tick style={thin,black}
  ] 
  \addplot [color=black, line width=0.5pt, densely dashed, mark=none,domain=-5:0,samples=200] ({-exp(-1)}, {x}); 
  \addplot [color=myblue, line width=1pt, mark=none,domain=-1:1.5,samples=200] ({x*exp(x)}, {x}); 
  \addplot [color=myred, line width=1pt, mark=none,domain=-5:-1,samples=200] ({x*exp(x)}, {x}); 
  \end{axis}
\end{tikzpicture}
\end{center}
\caption{The two real branches of the Lambert $W$ function: $W_0$ (blue) and $W_{-1}$ (red).}
\label{fig:lambertw}
\end{figure}
›

definition Lambert_W :: "real ⇒ real" where
  "Lambert_W x = (if x < -exp(-1) then -1 else (THE w. w ≥ -1 ∧ w * exp w = x))"

definition Lambert_W' :: "real ⇒ real" where
  "Lambert_W' x = (if x ∈ {-exp(-1)..<0} then (THE w. w ≤ -1 ∧ w * exp w = x) else -1)"

lemma Lambert_W_ex1:
  assumes "(x::real) ≥ -exp (-1)"
  shows   "∃!w. w ≥ -1 ∧ w * exp w = x"
proof (rule ex_ex1I)
  have "filterlim (λw::real. w * exp w) at_top at_top"
    by real_asymp
  hence "eventually (λw. w * exp w ≥ x) at_top"
    by (auto simp: filterlim_at_top)
  hence "eventually (λw. w ≥ 0 ∧ w * exp w ≥ x) at_top"
    by (intro eventually_conj eventually_ge_at_top)
  then obtain w' where w': "w' * exp w' ≥ x" "w' ≥ 0"
    by (auto simp: eventually_at_top_linorder)
  from w' assms have "∃w. -1 ≤ w ∧ w ≤ w' ∧ w * exp w = x"
    by (intro IVT' continuous_intros) auto
  thus "∃w. w ≥ -1 ∧ w * exp w = x" by blast
next
  fix w w' :: real
  assume ww': "w ≥ -1 ∧ w * exp w = x" "w' ≥ -1 ∧ w' * exp w' = x"
  hence "w * exp w = w' * exp w'" by simp
  thus "w = w'"
    using exp_times_self_strict_mono[of w w'] exp_times_self_strict_mono[of w' w] ww'
    by (cases w w' rule: linorder_cases) auto
qed

lemma Lambert_W'_ex1:
  assumes "(x::real) ∈ {-exp (-1)..<0}"
  shows   "∃!w. w ≤ -1 ∧ w * exp w = x"
proof (rule ex_ex1I)
  have "eventually (λw. x ≤ w * exp w) at_bot"
    using assms by real_asymp
  hence "eventually (λw. w ≤ -1 ∧ w * exp w ≥ x) at_bot"
    by (intro eventually_conj eventually_le_at_bot)
  then obtain w' where w': "w' * exp w' ≥ x" "w' ≤ -1"
    by (auto simp: eventually_at_bot_linorder)

  from w' assms have "∃w. w' ≤ w ∧ w ≤ -1 ∧ w * exp w = x"
    by (intro IVT2' continuous_intros) auto
  thus "∃w. w ≤ -1 ∧ w * exp w = x" by blast
next
  fix w w' :: real
  assume ww': "w ≤ -1 ∧ w * exp w = x" "w' ≤ -1 ∧ w' * exp w' = x"
  hence "w * exp w = w' * exp w'" by simp
  thus "w = w'"
    using exp_times_self_strict_antimono[of w w'] exp_times_self_strict_antimono[of w' w] ww'
    by (cases w w' rule: linorder_cases) auto
qed

lemma Lambert_W_times_exp_self: 
  assumes "x ≥ -exp (-1)"
  shows   "Lambert_W x * exp (Lambert_W x) = x"
  using theI'[OF Lambert_W_ex1[OF assms]] assms by (auto simp: Lambert_W_def)

lemma Lambert_W_times_exp_self':
  assumes "x ≥ -exp (-1)"
  shows   "exp (Lambert_W x) * Lambert_W x = x"
  using Lambert_W_times_exp_self[of x] assms by (simp add: mult_ac)

lemma Lambert_W'_times_exp_self: 
  assumes "x ∈ {-exp (-1)..<0}"
  shows   "Lambert_W' x * exp (Lambert_W' x) = x"
  using theI'[OF Lambert_W'_ex1[OF assms]] assms by (auto simp: Lambert_W'_def)

lemma Lambert_W'_times_exp_self':
  assumes "x ∈ {-exp (-1)..<0}"
  shows   "exp (Lambert_W' x) * Lambert_W' x = x"
  using Lambert_W'_times_exp_self[of x] assms by (simp add: mult_ac)

lemma Lambert_W_ge: "Lambert_W x ≥ -1"
  using theI'[OF Lambert_W_ex1[of x]] by (auto simp: Lambert_W_def)

lemma Lambert_W'_le: "Lambert_W' x ≤ -1"
  using theI'[OF Lambert_W'_ex1[of x]] by (auto simp: Lambert_W'_def)

lemma Lambert_W_eqI:
  assumes "w ≥ -1" "w * exp w = x"
  shows   "Lambert_W x = w"
proof -
  from assms exp_times_self_ge[of w] have "x ≥ -exp (-1)"
    by (cases "x ≥ -exp (-1)") auto
  from Lambert_W_ex1[OF this] Lambert_W_times_exp_self[OF this] Lambert_W_ge[of x] assms
    show ?thesis by metis
  qed

lemma Lambert_W'_eqI:
  assumes "w ≤ -1" "w * exp w = x"
  shows   "Lambert_W' x = w"
proof -
  from assms exp_times_self_ge[of w] have "x ≥ -exp (-1)"
    by (cases "x ≥ -exp (-1)") auto
  moreover from assms have "w * exp w < 0"
    by (intro mult_neg_pos) auto
  ultimately have "x ∈ {-exp (-1)..<0}"
    using assms by auto

  from Lambert_W'_ex1[OF this(1)] Lambert_W'_times_exp_self[OF this(1)] Lambert_W'_le assms
    show ?thesis by metis
  qed

text ‹
  $W_0(x)$ and $W_{-1}(x)$ together fully cover all solutions of $we^w = x$:
›
lemma exp_times_self_eqD:
  assumes "w * exp w = x"
  shows   "x ≥ -exp (-1)" and "w = Lambert_W x ∨ x < 0 ∧ w = Lambert_W' x"
proof -
  from assms show "x ≥ -exp (-1)"
    using exp_times_self_ge[of w] by auto
  show "w = Lambert_W x ∨ x < 0 ∧ w = Lambert_W' x"
  proof (cases "w ≥ -1")
    case True
    hence "Lambert_W x = w"
      using assms by (intro Lambert_W_eqI) auto
    thus ?thesis by auto
  next
    case False
    from False have "w * exp w < 0"
      by (intro mult_neg_pos) auto
    from False have "Lambert_W' x = w"
      using assms by (intro Lambert_W'_eqI) auto
    thus ?thesis using assms ‹w * exp w < 0› by auto
  qed
qed

theorem exp_times_self_eq_iff:
  "w * exp w = x ⟷ x ≥ -exp (-1) ∧ (w = Lambert_W x ∨ x < 0 ∧ w = Lambert_W' x)"
  using exp_times_self_eqD[of w x]
  by (auto simp: Lambert_W_times_exp_self Lambert_W'_times_exp_self)

lemma Lambert_W_exp_times_self [simp]: "x ≥ -1 ⟹ Lambert_W (x * exp x) = x"
  by (rule Lambert_W_eqI) auto

lemma Lambert_W_exp_times_self' [simp]: "x ≥ -1 ⟹ Lambert_W (exp x * x) = x"
  by (rule Lambert_W_eqI) auto

lemma Lambert_W'_exp_times_self [simp]: "x ≤ -1 ⟹ Lambert_W' (x * exp x) = x"
  by (rule Lambert_W'_eqI) auto

lemma Lambert_W'_exp_times_self' [simp]: "x ≤ -1 ⟹ Lambert_W' (exp x * x) = x"
  by (rule Lambert_W'_eqI) auto

lemma Lambert_W_times_ln_self:
  assumes "x ≥ exp (-1)"
  shows   "Lambert_W (x * ln x) = ln x"
proof -
  have "0 < exp (-1 :: real)"
    by simp
  also note ‹… ≤ x›
  finally have "x > 0" .
  from assms have "ln (exp (-1)) ≤ ln x"
    using ‹x > 0› by (subst ln_le_cancel_iff) auto
  hence "Lambert_W (exp (ln x) * ln x) = ln x"
    by (subst Lambert_W_exp_times_self') auto
  thus ?thesis using ‹x > 0› by simp
qed

lemma Lambert_W_times_ln_self':
  assumes "x ≥ exp (-1)"
  shows   "Lambert_W (ln x  * x) = ln x"
  using Lambert_W_times_ln_self[OF assms] by (simp add: mult.commute)

lemma Lambert_W_eq_minus_exp_minus1 [simp]: "Lambert_W (-exp (-1)) = -1"
  by (rule Lambert_W_eqI) auto

lemma Lambert_W'_eq_minus_exp_minus1 [simp]: "Lambert_W' (-exp (-1)) = -1"
  by (rule Lambert_W'_eqI) auto

lemma Lambert_W_0 [simp]: "Lambert_W 0 = 0"
  by (rule Lambert_W_eqI) auto


subsection ‹Monotonicity properties›

lemma Lambert_W_strict_mono:
  assumes "x ≥ -exp(-1)" "x < y"
  shows   "Lambert_W x < Lambert_W y"
proof (rule ccontr)
  assume "¬(Lambert_W x < Lambert_W y)"
  hence "Lambert_W x * exp (Lambert_W x) ≥ Lambert_W y * exp (Lambert_W y)"
    by (intro exp_times_self_mono) (auto simp: Lambert_W_ge)
  hence "x ≥ y"
    using assms by (simp add: Lambert_W_times_exp_self)
  with assms show False by simp
qed

lemma Lambert_W_mono:
  assumes "x ≥ -exp(-1)" "x ≤ y"
  shows   "Lambert_W x ≤ Lambert_W y"
  using Lambert_W_strict_mono[of x y] assms by (cases "x = y") auto

lemma Lambert_W_eq_iff [simp]:
  "x ≥ -exp(-1) ⟹ y ≥ -exp(-1) ⟹ Lambert_W x = Lambert_W y ⟷ x = y"
  using Lambert_W_strict_mono[of x y] Lambert_W_strict_mono[of y x]
  by (cases x y rule: linorder_cases) auto

lemma Lambert_W_le_iff [simp]:
  "x ≥ -exp(-1) ⟹ y ≥ -exp(-1) ⟹ Lambert_W x ≤ Lambert_W y ⟷ x ≤ y"
  using Lambert_W_strict_mono[of x y] Lambert_W_strict_mono[of y x]
  by (cases x y rule: linorder_cases) auto

lemma Lambert_W_less_iff [simp]:
  "x ≥ -exp(-1) ⟹ y ≥ -exp(-1) ⟹ Lambert_W x < Lambert_W y ⟷ x < y"
  using Lambert_W_strict_mono[of x y] Lambert_W_strict_mono[of y x]
  by (cases x y rule: linorder_cases) auto

lemma Lambert_W_le_minus_one:
  assumes "x ≤ -exp(-1)"
  shows   "Lambert_W x = -1"
proof (cases "x = -exp(-1)")
  case False
  thus ?thesis using assms
    by (auto simp: Lambert_W_def)
qed auto

lemma Lambert_W_pos_iff [simp]: "Lambert_W x > 0 ⟷ x > 0"
proof (cases "x ≥ -exp (-1)")
  case True
  thus ?thesis
    using Lambert_W_less_iff[of 0 x] by (simp del: Lambert_W_less_iff)
next
  case False
  hence "x < - exp(-1)" by auto
  also have "… ≤ 0" by simp
  finally show ?thesis using False
    by (auto simp: Lambert_W_le_minus_one)
qed

lemma Lambert_W_eq_0_iff [simp]: "Lambert_W x = 0 ⟷ x = 0"
  using Lambert_W_eq_iff[of x 0]
  by (cases "x ≥ -exp (-1)") (auto simp: Lambert_W_le_minus_one simp del: Lambert_W_eq_iff)

lemma Lambert_W_nonneg_iff [simp]: "Lambert_W x ≥ 0 ⟷ x ≥ 0"
  using Lambert_W_pos_iff[of x]
  by (cases "x = 0") (auto simp del: Lambert_W_pos_iff)

lemma Lambert_W_neg_iff [simp]: "Lambert_W x < 0 ⟷ x < 0"
  using Lambert_W_nonneg_iff[of x] by (auto simp del: Lambert_W_nonneg_iff)

lemma Lambert_W_nonpos_iff [simp]: "Lambert_W x ≤ 0 ⟷ x ≤ 0"
  using Lambert_W_pos_iff[of x] by (auto simp del: Lambert_W_pos_iff)

lemma Lambert_W_geI:
  assumes "y * exp y ≤ x"
  shows   "Lambert_W x ≥ y"
proof (cases "y ≥ -1")
  case False
  hence "y ≤ -1" by simp
  also have "-1 ≤ Lambert_W x" by (rule Lambert_W_ge)
  finally show ?thesis .
next
  case True
  have "Lambert_W x ≥ Lambert_W (y * exp y)"
    using assms exp_times_self_ge[of y] by (intro Lambert_W_mono) auto
  thus ?thesis using assms True by simp
qed

lemma Lambert_W_gtI:
  assumes "y * exp y < x"
  shows   "Lambert_W x > y"
proof (cases "y ≥ -1")
  case False
  hence "y < -1" by simp
  also have "-1 ≤ Lambert_W x" by (rule Lambert_W_ge)
  finally show ?thesis .
next
  case True
  have "Lambert_W x > Lambert_W (y * exp y)"
    using assms exp_times_self_ge[of y] by (intro Lambert_W_strict_mono) auto
  thus ?thesis using assms True by simp
qed

lemma Lambert_W_leI:
  assumes "y * exp y ≥ x" "y ≥ -1" "x ≥ -exp (-1)"
  shows   "Lambert_W x ≤ y"
proof -
  have "Lambert_W x ≤ Lambert_W (y * exp y)"
    using assms exp_times_self_ge[of y] by (intro Lambert_W_mono) auto
  thus ?thesis using assms by simp
qed

lemma Lambert_W_lessI:
  assumes "y * exp y > x" "y ≥ -1" "x ≥ -exp (-1)"
  shows   "Lambert_W x < y"
proof -
  have "Lambert_W x < Lambert_W (y * exp y)"
    using assms exp_times_self_ge[of y] by (intro Lambert_W_strict_mono) auto
  thus ?thesis using assms by simp
qed



lemma Lambert_W'_strict_antimono:
  assumes "-exp (-1) ≤ x" "x < y" "y < 0"
  shows   "Lambert_W' x > Lambert_W' y"
proof (rule ccontr)
  assume "¬(Lambert_W' x > Lambert_W' y)"
  hence "Lambert_W' x * exp (Lambert_W' x) ≥ Lambert_W' y * exp (Lambert_W' y)"
    using assms by (intro exp_times_self_antimono Lambert_W'_le) auto
  hence "x ≥ y"
    using assms by (simp add: Lambert_W'_times_exp_self)
  with assms show False by simp
qed

lemma Lambert_W'_antimono:
  assumes "x ≥ -exp(-1)" "x ≤ y" "y < 0"
  shows   "Lambert_W' x ≥ Lambert_W' y"
  using Lambert_W'_strict_antimono[of x y] assms by (cases "x = y") auto

lemma Lambert_W'_eq_iff [simp]:
  "x ∈ {-exp(-1)..<0} ⟹ y ∈ {-exp(-1)..<0} ⟹ Lambert_W' x = Lambert_W' y ⟷ x = y"
  using Lambert_W'_strict_antimono[of x y] Lambert_W'_strict_antimono[of y x]
  by (cases x y rule: linorder_cases) auto

lemma Lambert_W'_le_iff [simp]:
  "x ∈ {-exp(-1)..<0} ⟹ y ∈ {-exp(-1)..<0} ⟹ Lambert_W' x ≤ Lambert_W' y ⟷ x ≥ y"
  using Lambert_W'_strict_antimono[of x y] Lambert_W'_strict_antimono[of y x]
  by (cases x y rule: linorder_cases) auto

lemma Lambert_W'_less_iff [simp]:
  "x ∈ {-exp(-1)..<0} ⟹ y ∈ {-exp(-1)..<0} ⟹ Lambert_W' x < Lambert_W' y ⟷ x > y"
  using Lambert_W'_strict_antimono[of x y] Lambert_W'_strict_antimono[of y x]
  by (cases x y rule: linorder_cases) auto

lemma Lambert_W'_le_minus_one:
  assumes "x ≤ -exp(-1)"
  shows   "Lambert_W' x = -1"
proof (cases "x = -exp(-1)")
  case False
  thus ?thesis using assms
    by (auto simp: Lambert_W'_def)
qed auto

lemma Lambert_W'_ge_zero: "x ≥ 0 ⟹ Lambert_W' x = -1"
  by (simp add: Lambert_W'_def)

lemma Lambert_W'_neg: "Lambert_W' x < 0"
  by (rule le_less_trans[OF Lambert_W'_le]) auto

lemma Lambert_W'_nz [simp]: "Lambert_W' x ≠ 0"
  using Lambert_W'_neg[of x] by simp

lemma Lambert_W'_geI:
  assumes "y * exp y ≥ x" "y ≤ -1" "x ≥ -exp(-1)"
  shows   "Lambert_W' x ≥ y"
proof -
  from assms have "y * exp y < 0"
    by (intro mult_neg_pos) auto
  hence "Lambert_W' x ≥ Lambert_W' (y * exp y)"
    using assms exp_times_self_ge[of y] by (intro Lambert_W'_antimono) auto
  thus ?thesis using assms by simp
qed

lemma Lambert_W'_gtI:
  assumes "y * exp y > x" "y ≤ -1" "x ≥ -exp(-1)"
  shows   "Lambert_W' x ≥ y"
proof -
  from assms have "y * exp y < 0"
    by (intro mult_neg_pos) auto
  hence "Lambert_W' x > Lambert_W' (y * exp y)"
    using assms exp_times_self_ge[of y] by (intro Lambert_W'_strict_antimono) auto
  thus ?thesis using assms by simp
qed

lemma Lambert_W'_leI:
  assumes "y * exp y ≤ x" "x < 0"
  shows   "Lambert_W' x ≤ y"
proof (cases "y ≤ -1")
  case True
  have "Lambert_W' x ≤ Lambert_W' (y * exp y)"
    using assms exp_times_self_ge[of y] by (intro Lambert_W'_antimono) auto
  thus ?thesis using assms True by simp
next
  case False
  have "Lambert_W' x ≤ -1"
    by (rule Lambert_W'_le)
  also have "… < y"
    using False by simp
  finally show ?thesis by simp
qed

lemma Lambert_W'_lessI:
  assumes "y * exp y < x" "x < 0"
  shows   "Lambert_W' x < y"
proof (cases "y ≤ -1")
  case True
  have "Lambert_W' x < Lambert_W' (y * exp y)"
    using assms exp_times_self_ge[of y] by (intro Lambert_W'_strict_antimono) auto
  thus ?thesis using assms True by simp
next
  case False
  have "Lambert_W' x ≤ -1"
    by (rule Lambert_W'_le)
  also have "… < y"
    using False by simp
  finally show ?thesis by simp
qed


lemma bij_betw_exp_times_self_atLeastAtMost:
  fixes a b :: real
  assumes "a ≥ -1" "a ≤ b"
  shows   "bij_betw (λx. x * exp x) {a..b} {a * exp a..b * exp b}"
  unfolding bij_betw_def
proof
  show "inj_on (λx. x * exp x) {a..b}"
    by (rule inj_on_subset[OF exp_times_self_inj]) (use assms in auto)
next
  show "(λx. x * exp x) ` {a..b} = {a * exp a..b * exp b}"
  proof safe
    fix x assume "x ∈ {a..b}"
    thus "x * exp x ∈ {a * exp a..b * exp b}"
      using assms by (auto intro!: exp_times_self_mono)
  next
    fix x assume x: "x ∈ {a * exp a..b * exp b}"
    have "(-1) * exp (-1) ≤ a * exp a"
      using assms by (intro exp_times_self_mono) auto
    also have "… ≤ x" using x by simp
    finally have "x ≥ -exp (-1)" by simp

    have "Lambert_W x ∈ {a..b}"
      using x ‹x ≥ -exp (-1)› assms by (auto intro!: Lambert_W_geI Lambert_W_leI)
    moreover have "Lambert_W x * exp (Lambert_W x) = x"
      using ‹x ≥ -exp (-1)› by (simp add: Lambert_W_times_exp_self)
    ultimately show "x ∈ (λx. x * exp x) ` {a..b}"
      unfolding image_iff by metis
  qed
qed

lemma bij_betw_exp_times_self_atLeastAtMost':
  fixes a b :: real
  assumes "a ≤ b" "b ≤ -1"
  shows   "bij_betw (λx. x * exp x) {a..b} {b * exp b..a * exp a}"
  unfolding bij_betw_def
proof
  show "inj_on (λx. x * exp x) {a..b}"
    by (rule inj_on_subset[OF exp_times_self_inj']) (use assms in auto)
next
  show "(λx. x * exp x) ` {a..b} = {b * exp b..a * exp a}"
  proof safe
    fix x assume "x ∈ {a..b}"
    thus "x * exp x ∈ {b * exp b..a * exp a}"
      using assms by (auto intro!: exp_times_self_antimono)
  next
    fix x assume x: "x ∈ {b * exp b..a * exp a}"
    from assms have "a * exp a < 0"
      by (intro mult_neg_pos) auto
    with x have "x < 0" by auto
    have "(-1) * exp (-1) ≤ b * exp b"
      using assms by (intro exp_times_self_antimono) auto
    also have "… ≤ x" using x by simp
    finally have "x ≥ -exp (-1)" by simp

    have "Lambert_W' x ∈ {a..b}"
      using x ‹x ≥ -exp (-1)› ‹x < 0› assms 
      by (auto intro!: Lambert_W'_geI Lambert_W'_leI)
    moreover have "Lambert_W' x * exp (Lambert_W' x) = x"
      using ‹x ≥ -exp (-1)› ‹x < 0› by (auto simp: Lambert_W'_times_exp_self)
    ultimately show "x ∈ (λx. x * exp x) ` {a..b}"
      unfolding image_iff by metis
  qed
qed

lemma bij_betw_exp_times_self_atLeast:
  fixes a :: real
  assumes "a ≥ -1"
  shows   "bij_betw (λx. x * exp x) {a..} {a * exp a..}"
  unfolding bij_betw_def
proof
  show "inj_on (λx. x * exp x) {a..}"
    by (rule inj_on_subset[OF exp_times_self_inj]) (use assms in auto)
next
  show "(λx. x * exp x) ` {a..} = {a * exp a..}"
  proof safe
    fix x assume "x ≥ a"
    thus "x * exp x ≥ a * exp a"
      using assms by (auto intro!: exp_times_self_mono)
  next
    fix x assume x: "x ≥ a * exp a"
    have "(-1) * exp (-1) ≤ a * exp a"
      using assms by (intro exp_times_self_mono) auto
    also have "… ≤ x" using x by simp
    finally have "x ≥ -exp (-1)" by simp

    have "Lambert_W x ∈ {a..}"
      using x ‹x ≥ -exp (-1)› assms by (auto intro!: Lambert_W_geI Lambert_W_leI)
    moreover have "Lambert_W x * exp (Lambert_W x) = x"
      using ‹x ≥ -exp (-1)› by (simp add: Lambert_W_times_exp_self)
    ultimately show "x ∈ (λx. x * exp x) ` {a..}"
      unfolding image_iff by metis
  qed
qed


subsection ‹Basic identities and bounds›

lemma Lambert_W_2_ln_2 [simp]: "Lambert_W (2 * ln 2) = ln 2"
proof -
  have "-1 ≤ (0 :: real)"
    by simp
  also have "… ≤ ln 2"
    by simp
  finally have "-1 ≤ (ln 2 :: real)" .
  thus ?thesis
    by (intro Lambert_W_eqI) auto
qed

lemma Lambert_W_exp_1 [simp]: "Lambert_W (exp 1) = 1"
  by (rule Lambert_W_eqI) auto

lemma Lambert_W_neg_ln_over_self:
  assumes "x ∈ {exp (-1)..exp 1}"
  shows   "Lambert_W (-ln x / x) = -ln x"
proof -
  have "0 < (exp (-1) :: real)"
    by simp
  also have "… ≤ x"
    using assms by simp
  finally have "x > 0" .
  from ‹x > 0› assms have "ln x ≤ ln (exp 1)"
    by (subst ln_le_cancel_iff) auto
  also have "ln (exp 1) = (1 :: real)"
    by simp
  finally have "ln x ≤ 1" .
  show ?thesis
    using assms ‹x > 0› ‹ln x ≤ 1›
    by (intro Lambert_W_eqI) (auto simp: exp_minus field_simps)
qed

lemma Lambert_W'_neg_ln_over_self:
  assumes "x ≥ exp 1"
  shows   "Lambert_W' (-ln x / x) = -ln x"
proof (rule Lambert_W'_eqI)
  have "0 < (exp 1 :: real)"
    by simp
  also have "… ≤ x"
    by fact
  finally have "x > 0" .
  from assms ‹x > 0› have "ln x ≥ ln (exp 1)"
    by (subst ln_le_cancel_iff) auto
  thus "-ln x ≤ -1" by simp
  show "-ln x * exp (-ln x) = -ln x / x"
    using ‹x > 0› by (simp add: field_simps exp_minus)
qed

lemma exp_Lambert_W: "x ≥ -exp (-1) ⟹ x ≠ 0 ⟹ exp (Lambert_W x) = x / Lambert_W x"
  using Lambert_W_times_exp_self[of x] by (auto simp add: divide_simps mult_ac)

lemma exp_Lambert_W': "x ∈ {-exp (-1)..<0} ⟹ exp (Lambert_W' x) = x / Lambert_W' x"
  using Lambert_W'_times_exp_self[of x] by (auto simp add: divide_simps mult_ac)

lemma ln_Lambert_W:
  assumes "x > 0"
  shows   "ln (Lambert_W x) = ln x - Lambert_W x"
proof -
  have "-exp (-1) ≤ (0 :: real)"
    by simp
  also have "… < x" by fact
  finally have x: "x > -exp(-1)" .

  have "exp (ln (Lambert_W x)) = exp (ln x - Lambert_W x)"
    using assms x by (subst exp_diff) (auto simp: exp_Lambert_W)
  thus ?thesis by (subst (asm) exp_inj_iff)
qed

lemma ln_minus_Lambert_W':
  assumes "x ∈ {-exp (-1)..<0}"
  shows   "ln (-Lambert_W' x) = ln (-x) - Lambert_W' x"
proof -
  have "exp (ln (-x) - Lambert_W' x) = -Lambert_W' x"
    using assms by (simp add: exp_diff exp_Lambert_W')
  also have "… = exp (ln (-Lambert_W' x))"
    using Lambert_W'_neg[of x] by simp
  finally show ?thesis by simp
qed

lemma Lambert_W_plus_Lambert_W_eq:
  assumes "x > 0" "y > 0"
  shows   "Lambert_W x + Lambert_W y = Lambert_W (x * y * (1 / Lambert_W x + 1 / Lambert_W y))"
proof (rule sym, rule Lambert_W_eqI)
  have "x > -exp(-1)" "y > -exp (-1)"
    by (rule less_trans[OF _ assms(1)] less_trans[OF _ assms(2)], simp)+
  with assms show "(Lambert_W x + Lambert_W y) * exp (Lambert_W x + Lambert_W y) =
                     x * y * (1 / Lambert_W x + 1 / Lambert_W y)"
    by (auto simp: field_simps exp_add exp_Lambert_W)
  have "-1 ≤ (0 :: real)"
    by simp
  also from assms have "… ≤ Lambert_W x + Lambert_W y"
    by (intro add_nonneg_nonneg) auto
  finally show "… ≥ -1" .
qed

lemma Lambert_W'_plus_Lambert_W'_eq:
  assumes "x ∈ {-exp(-1)..<0}" "y ∈ {-exp(-1)..<0}"
  shows   "Lambert_W' x + Lambert_W' y = Lambert_W' (x * y * (1 / Lambert_W' x + 1 / Lambert_W' y))"
proof (rule sym, rule Lambert_W'_eqI)
  from assms show "(Lambert_W' x + Lambert_W' y) * exp (Lambert_W' x + Lambert_W' y) =
                     x * y * (1 / Lambert_W' x + 1 / Lambert_W' y)"
    by (auto simp: field_simps exp_add exp_Lambert_W')
  have "Lambert_W' x + Lambert_W' y ≤ -1 + -1"
    by (intro add_mono Lambert_W'_le)
  also have "… ≤ -1" by simp
  finally show "Lambert_W' x + Lambert_W' y ≤ -1" .
qed

lemma Lambert_W_gt_ln_minus_ln_ln:
  assumes "x > exp 1"
  shows   "Lambert_W x > ln x - ln (ln x)"
proof (rule Lambert_W_gtI)
  have "x > 1"
    by (rule less_trans[OF _ assms]) auto
  have "ln x > ln (exp 1)"
    by (subst ln_less_cancel_iff) (use ‹x > 1› assms in auto)
  thus "(ln x - ln (ln x)) * exp (ln x - ln (ln x)) < x"
    using assms ‹x > 1› by (simp add: exp_diff field_simps)
qed

lemma Lambert_W_less_ln:
  assumes "x > exp 1"
  shows   "Lambert_W x < ln x"
proof (rule Lambert_W_lessI)
  have "x > 0"
    by (rule less_trans[OF _ assms]) auto
  have "ln x > ln (exp 1)"
    by (subst ln_less_cancel_iff) (use ‹x > 0› assms in auto)
  thus "x < ln x * exp (ln x)"
    using ‹x > 0› by simp
  show "ln x ≥ -1"
    by (rule less_imp_le[OF le_less_trans[OF _ ‹ln x > _›]]) auto
  show "x ≥ -exp (-1)"
    by (rule less_imp_le[OF le_less_trans[OF _ ‹x > 0›]]) auto
qed


subsection ‹Limits, continuity, and differentiability›

lemma filterlim_Lambert_W_at_top [tendsto_intros]: "filterlim Lambert_W at_top at_top"
  unfolding filterlim_at_top
proof
  fix C :: real
  have "eventually (λx. x ≥ C * exp C) at_top"
    by (rule eventually_ge_at_top)
  thus "eventually (λx. Lambert_W x ≥ C) at_top"
  proof eventually_elim
    case (elim x)
    thus ?case
      by (intro Lambert_W_geI) auto
  qed
qed

lemma filterlim_Lambert_W_at_left_0 [tendsto_intros]:
  "filterlim Lambert_W' at_bot (at_left 0)"
  unfolding filterlim_at_bot
proof
  fix C :: real
  define C' where "C' = min C (-1)"
  have "C' < 0" "C' ≤ C"
    by (simp_all add: C'_def)
  have "C' * exp C' < 0"
    using ‹C' < 0› by (intro mult_neg_pos) auto
  hence "eventually (λx. x ≥ C' * exp C') (at_left 0)"
    by real_asymp
  moreover have "eventually (λx::real. x < 0) (at_left 0)"
    by real_asymp
  ultimately show "eventually (λx. Lambert_W' x ≤ C) (at_left 0)"
  proof eventually_elim
    case (elim x)
    hence "Lambert_W' x ≤ C'"
      by (intro Lambert_W'_leI) auto
    also have "… ≤ C" by fact
    finally show ?case .
  qed
qed

lemma continuous_on_Lambert_W [continuous_intros]: "continuous_on {-exp (-1)..} Lambert_W"
proof -
  have *: "continuous_on {-exp (-1)..b * exp b} Lambert_W" if "b ≥ 0" for b
  proof -
    have "continuous_on ((λx. x * exp x) ` {-1..b}) Lambert_W"
      by (rule continuous_on_inv) (auto intro!: continuous_intros)
    also have "(λx. x * exp x) ` {-1..b} = {-exp (-1)..b * exp b}"
      using bij_betw_exp_times_self_atLeastAtMost[of "-1" b] ‹b ≥ 0›
      by (simp add: bij_betw_def)
    finally show ?thesis .
  qed

  have "continuous (at x) Lambert_W" if "x ≥ 0" for x
  proof -
    have x: "-exp (-1) < x"
      by (rule less_le_trans[OF _ that]) auto
    
    define b where "b = Lambert_W x + 1"
    have "b ≥ 0"
      using Lambert_W_ge[of x] by (simp add: b_def)
    have "x = Lambert_W x * exp (Lambert_W x)"
      using that x by (subst Lambert_W_times_exp_self) auto
    also have "… < b * exp b"
      by (intro exp_times_self_strict_mono) (auto simp: b_def Lambert_W_ge)
    finally have "b * exp b > x" .
    have "continuous_on {-exp(-1)<..<b * exp b} Lambert_W"
      by (rule continuous_on_subset[OF *[of b]]) (use ‹b ≥ 0› in auto)
    moreover have "x ∈ {-exp(-1)<..<b * exp b}"
      using ‹b * exp b > x› x by auto
    ultimately show "continuous (at x) Lambert_W"
      by (subst (asm) continuous_on_eq_continuous_at) auto
  qed
  hence "continuous_on {0..} Lambert_W"
    by (intro continuous_at_imp_continuous_on) auto
  moreover have "continuous_on {-exp (-1)..0} Lambert_W"
    using *[of 0] by simp
  ultimately have "continuous_on ({-exp (-1)..0} ∪ {0..}) Lambert_W"
    by (intro continuous_on_closed_Un) auto
  also have "{-exp (-1)..0} ∪ {0..} = {-exp (-1::real)..}"
    using order.trans[of "-exp (-1)::real" 0] by auto
  finally show ?thesis .
qed

lemma continuous_on_Lambert_W_alt [continuous_intros]:
  assumes "continuous_on A f" "⋀x. x ∈ A ⟹ f x ≥ -exp (-1)"
  shows   "continuous_on A (λx. Lambert_W (f x))"
  using continuous_on_compose2[OF continuous_on_Lambert_W assms(1)] assms by auto

lemma continuous_on_Lambert_W' [continuous_intros]: "continuous_on {-exp (-1)..<0} Lambert_W'"
proof -
  have *: "continuous_on {-exp (-1)..-b * exp (-b)} Lambert_W'" if "b ≥ 1" for b
  proof -
    have "continuous_on ((λx. x * exp x) ` {-b..-1}) Lambert_W'"
      by (intro continuous_on_inv ballI) (auto intro!: continuous_intros)
    also have "(λx. x * exp x) ` {-b..-1} = {-exp (-1)..-b * exp (-b)}"
      using bij_betw_exp_times_self_atLeastAtMost'[of "-b" "-1"] that
      by (simp add: bij_betw_def)
    finally show ?thesis .
  qed

  have "continuous (at x) Lambert_W'" if "x > -exp (-1)" "x < 0" for x
  proof - 
    define b where "b = Lambert_W x + 1"
    have "eventually (λb. -b * exp (-b) > x) at_top"
      using that by real_asymp
    hence "eventually (λb. b ≥ 1 ∧ -b * exp (-b) > x) at_top"
      by (intro eventually_conj eventually_ge_at_top)
    then obtain b where b: "b ≥ 1" "-b * exp (-b) > x"
      by (auto simp: eventually_at_top_linorder)

    have "continuous_on {-exp(-1)<..<-b * exp (-b)} Lambert_W'"
      by (rule continuous_on_subset[OF *[of b]]) (use ‹b ≥ 1› in auto)
    moreover have "x ∈ {-exp(-1)<..<-b * exp (-b)}"
      using b that by auto
    ultimately show "continuous (at x) Lambert_W'"
      by (subst (asm) continuous_on_eq_continuous_at) auto
  qed
  hence **: "continuous_on {-exp (-1)<..<0} Lambert_W'"
    by (intro continuous_at_imp_continuous_on) auto

  show ?thesis
    unfolding continuous_on_def
  proof
    fix x :: real assume x: "x ∈ {-exp(-1)..<0}"
    show "(Lambert_W' ⤏ Lambert_W' x) (at x within {-exp(-1)..<0})"
    proof (cases "x = -exp(-1)")
      case False
      hence "isCont Lambert_W' x"
        using x ** by (auto simp: continuous_on_eq_continuous_at)
      thus ?thesis
        using continuous_at filterlim_within_subset by blast
    next
      case True
      define a :: real where "a = -2 * exp (-2)"
      have a: "a > -exp (-1)"
        using exp_times_self_strict_antimono[of "-1" "-2"] by (auto simp: a_def)
      from True have "x ∈ {-exp (-1)..<a}"
        using a by (auto simp: a_def)
      have "continuous_on {-exp (-1)..<a} Lambert_W'"
        unfolding a_def by (rule continuous_on_subset[OF *[of 2]]) auto
      hence "(Lambert_W' ⤏ Lambert_W' x) (at x within {-exp (-1)..<a})"
        using ‹x ∈ {-exp (-1)..<a}› by (auto simp: continuous_on_def)
      also have "at x within {-exp (-1)..<a} = at_right x"
        using a by (intro at_within_nhd[of _ "{..<a}"]) (auto simp: True)
      also have "… = at x within {-exp (-1)..<0}"
        using a by (intro at_within_nhd[of _ "{..<0}"]) (auto simp: True)
      finally show ?thesis .
    qed
  qed
qed

lemma continuous_on_Lambert_W'_alt [continuous_intros]:
  assumes "continuous_on A f" "⋀x. x ∈ A ⟹ f x ∈ {-exp (-1)..<0}"
  shows   "continuous_on A (λx. Lambert_W' (f x))"
  using continuous_on_compose2[OF continuous_on_Lambert_W' assms(1)] assms
  by (auto simp: subset_iff)


lemma tendsto_Lambert_W_1:
  assumes "(f ⤏ L) F" "eventually (λx. f x ≥ -exp (-1)) F"
  shows   "((λx. Lambert_W (f x)) ⤏ Lambert_W L) F"
proof (cases "F = bot")
  case [simp]: False
  from tendsto_lowerbound[OF assms] have "L ≥ -exp (-1)" by simp
  thus ?thesis
    using continuous_on_tendsto_compose[OF continuous_on_Lambert_W assms(1)] assms(2) by simp
qed auto

lemma tendsto_Lambert_W_2:
  assumes "(f ⤏ L) F" "L > -exp (-1)"
  shows   "((λx. Lambert_W (f x)) ⤏ Lambert_W L) F"
  using order_tendstoD(1)[OF assms] assms
  by (intro tendsto_Lambert_W_1) (auto elim: eventually_mono)

lemma tendsto_Lambert_W [tendsto_intros]:
  assumes "(f ⤏ L) F" "eventually (λx. f x ≥ -exp (-1)) F ∨ L > -exp (-1)"
  shows   "((λx. Lambert_W (f x)) ⤏ Lambert_W L) F"
  using assms(2)
proof
  assume "L > -exp (-1)"
  from order_tendstoD(1)[OF assms(1) this] assms(1) show ?thesis
    by (intro tendsto_Lambert_W_1) (auto elim: eventually_mono)  
qed (use tendsto_Lambert_W_1[OF assms(1)] in auto)

lemma tendsto_Lambert_W'_1:
  assumes "(f ⤏ L) F" "eventually (λx. f x ≥ -exp (-1)) F" "L < 0"
  shows   "((λx. Lambert_W' (f x)) ⤏ Lambert_W' L) F"
proof (cases "F = bot")
  case [simp]: False
  from tendsto_lowerbound[OF assms(1,2)] have L_ge: "L ≥ -exp (-1)" by simp
  from order_tendstoD(2)[OF assms(1,3)] have ev: "eventually (λx. f x < 0) F"
    by auto
  with assms(2) have "eventually (λx. f x ∈ {-exp (-1)..<0}) F"
    by eventually_elim auto
  thus ?thesis using L_ge assms(3)
    by (intro continuous_on_tendsto_compose[OF continuous_on_Lambert_W' assms(1)]) auto
qed auto

lemma tendsto_Lambert_W'_2:
  assumes "(f ⤏ L) F" "L > -exp (-1)" "L < 0"
  shows   "((λx. Lambert_W' (f x)) ⤏ Lambert_W' L) F"
  using order_tendstoD(1)[OF assms(1,2)] assms
  by (intro tendsto_Lambert_W'_1) (auto elim: eventually_mono)

lemma tendsto_Lambert_W' [tendsto_intros]:
  assumes "(f ⤏ L) F" "eventually (λx. f x ≥ -exp (-1)) F ∨ L > -exp (-1)" "L < 0"
  shows   "((λx. Lambert_W' (f x)) ⤏ Lambert_W' L) F"
  using assms(2)
proof
  assume "L > -exp (-1)"
  from order_tendstoD(1)[OF assms(1) this] assms(1,3) show ?thesis
    by (intro tendsto_Lambert_W'_1) (auto elim: eventually_mono)  
qed (use tendsto_Lambert_W'_1[OF assms(1) _ assms(3)] in auto)


lemma continuous_Lambert_W [continuous_intros]:
  assumes "continuous F f" "f (Lim F (λx. x)) > -exp (-1) ∨ eventually (λx. f x ≥ -exp (-1)) F"
  shows   "continuous F (λx. Lambert_W (f x))"
  using assms unfolding continuous_def by (intro tendsto_Lambert_W) auto

lemma continuous_Lambert_W' [continuous_intros]:
  assumes "continuous F f" "f (Lim F (λx. x)) > -exp (-1) ∨ eventually (λx. f x ≥ -exp (-1)) F"
          "f (Lim F (λx. x)) < 0"
  shows   "continuous F (λx. Lambert_W' (f x))"
  using assms unfolding continuous_def by (intro tendsto_Lambert_W') auto


lemma has_field_derivative_Lambert_W [derivative_intros]:
  assumes x: "x > -exp (-1)"
  shows   "(Lambert_W has_real_derivative inverse (x + exp (Lambert_W x))) (at x within A)"
proof -
  write Lambert_W (‹W›)
  from x have "W x > W (-exp (-1))"
    by (subst Lambert_W_less_iff) auto
  hence "W x > -1" by simp

  note [derivative_intros] = DERIV_inverse_function[where g = Lambert_W]
  have "((λx. x * exp x) has_real_derivative (1 + W x) * exp (W x)) (at (W x))"
    by (auto intro!: derivative_eq_intros simp: algebra_simps)
  hence "(W has_real_derivative inverse ((1 + W x) * exp (W x))) (at x)"
    by (rule DERIV_inverse_function[where a = "-exp (-1)" and b = "x + 1"])
       (use x ‹W x > -1› in ‹auto simp: Lambert_W_times_exp_self Lim_ident_at
                                  intro!: continuous_intros›)
  also have "(1 + W x) * exp (W x) = x + exp (W x)"
    using x by (simp add: algebra_simps Lambert_W_times_exp_self)
  finally show ?thesis by (rule has_field_derivative_at_within)
qed

lemma has_field_derivative_Lambert_W_gen [derivative_intros]:
  assumes "(f has_real_derivative f') (at x within A)" "f x > -exp (-1)"
  shows   "((λx. Lambert_W (f x)) has_real_derivative
             (f' / (f x + exp (Lambert_W (f x))))) (at x within A)"
  using DERIV_chain2[OF has_field_derivative_Lambert_W[OF assms(2)] assms(1)]
  by (simp add: field_simps)

lemma has_field_derivative_Lambert_W' [derivative_intros]:
  assumes x: "x ∈ {-exp (-1)<..<0}"
  shows   "(Lambert_W' has_real_derivative inverse (x + exp (Lambert_W' x))) (at x within A)"
proof -
  write Lambert_W' (‹W›)
  from x have "W x < W (-exp (-1))"
    by (subst Lambert_W'_less_iff) auto
  hence "W x < -1" by simp

  note [derivative_intros] = DERIV_inverse_function[where g = Lambert_W]
  have "((λx. x * exp x) has_real_derivative (1 + W x) * exp (W x)) (at (W x))"
    by (auto intro!: derivative_eq_intros simp: algebra_simps)
  hence "(W has_real_derivative inverse ((1 + W x) * exp (W x))) (at x)"
    by (rule DERIV_inverse_function[where a = "-exp (-1)" and b = "0"])
       (use x ‹W x < -1› in ‹auto simp: Lambert_W'_times_exp_self Lim_ident_at
                                        intro!: continuous_intros›)
  also have "(1 + W x) * exp (W x) = x + exp (W x)"
    using x by (simp add: algebra_simps Lambert_W'_times_exp_self)
  finally show ?thesis by (rule has_field_derivative_at_within)
qed

lemma has_field_derivative_Lambert_W'_gen [derivative_intros]:
  assumes "(f has_real_derivative f') (at x within A)" "f x ∈ {-exp (-1)<..<0}"
  shows   "((λx. Lambert_W' (f x)) has_real_derivative
             (f' / (f x + exp (Lambert_W' (f x))))) (at x within A)"
  using DERIV_chain2[OF has_field_derivative_Lambert_W'[OF assms(2)] assms(1)]
  by (simp add: field_simps)


subsection ‹Asymptotic expansion›

text ‹
  Lastly, we prove some more detailed asymptotic expansions of $W$ and $W'$ at their
  singularities. First, we show that:
  \begin{align*}
    W(x) &= \log x - \log\log x + o(\log\log x) &&\text{for}\ x\to\infty\\
    W'(x) &= \log (-x) - \log (-\log (-x)) + o(\log (-\log (-x))) &&\text{for}\ x\to 0^{-}
  \end{align*}
›
theorem Lambert_W_asymp_equiv_at_top:
  "(λx. Lambert_W x - ln x) ∼[at_top] (λx. -ln (ln x))"
proof -
  have "(λx. Lambert_W x - ln x) ∼[at_top] (λx. (-1) * ln (ln x))"
  proof (rule asymp_equiv_sandwich')
    fix c' :: real assume c': "c' ∈ {-2<..<-1}"
    have "eventually (λx. (ln x + c' * ln (ln x)) * exp (ln x + c' * ln (ln x)) ≤ x) at_top"
         "eventually (λx. ln x + c' * ln (ln x) ≥ -1) at_top"
      using c' by real_asymp+
    thus "eventually (λx. Lambert_W x - ln x ≥ c' * ln (ln x)) at_top"
    proof eventually_elim
      case (elim x)
      hence "Lambert_W x ≥ ln x + c' * ln (ln x)"
        by (intro Lambert_W_geI)
      thus ?case by simp
    qed
  next
    fix c' :: real assume c': "c' ∈ {-1<..<0}"
    have "eventually (λx. (ln x + c' * ln (ln x)) * exp (ln x + c' * ln (ln x)) ≥ x) at_top"
         "eventually (λx. ln x + c' * ln (ln x) ≥ -1) at_top"
      using c' by real_asymp+
    thus "eventually (λx. Lambert_W x - ln x ≤ c' * ln (ln x)) at_top"
      using eventually_ge_at_top[of "-exp (-1)"]
    proof eventually_elim
      case (elim x)
      hence "Lambert_W x ≤ ln x + c' * ln (ln x)"
        by (intro Lambert_W_leI)
      thus ?case by simp
    qed
  qed auto
  thus ?thesis by simp
qed

lemma Lambert_W_asymp_equiv_at_top' [asymp_equiv_intros]:
  "Lambert_W ∼[at_top] ln"
proof -
  have "(λx. Lambert_W x - ln x) ∈ Θ(λx. -ln (ln x))"
    by (intro asymp_equiv_imp_bigtheta Lambert_W_asymp_equiv_at_top)
  also have "(λx::real. -ln (ln x)) ∈ o(ln)"
    by real_asymp
  finally show ?thesis by (simp add: asymp_equiv_altdef)
qed

theorem Lambert_W'_asymp_equiv_at_left_0:
  "(λx. Lambert_W' x - ln (-x)) ∼[at_left 0] (λx. -ln (-ln (-x)))"
proof -
  have "(λx. Lambert_W' x - ln (-x)) ∼[at_left 0] (λx. (-1) * ln (-ln (-x)))"
  proof (rule asymp_equiv_sandwich')
    fix c' :: real assume c': "c' ∈ {-2<..<-1}"
    have "eventually (λx. x ≤ (ln (-x) + c' * ln (-ln (-x))) * exp (ln (-x) + c' * ln (-ln (-x)))) (at_left 0)"
         "eventually (λx::real. ln (-x) + c' * ln (-ln (-x)) ≤ -1) (at_left 0)"
         "eventually (λx::real. -exp (-1) ≤ x) (at_left 0)"
      using c' by real_asymp+
    thus "eventually (λx. Lambert_W' x - ln (-x) ≥ c' * ln (-ln (-x))) (at_left 0)"
    proof eventually_elim
      case (elim x)
      hence "Lambert_W' x ≥ ln (-x) + c' * ln (-ln (-x))"
        by (intro Lambert_W'_geI)
      thus ?case by simp
    qed
  next
    fix c' :: real assume c': "c' ∈ {-1<..<0}"
    have "eventually (λx. x ≥ (ln (-x) + c' * ln (-ln (-x))) * exp (ln (-x) + c' * ln (-ln (-x)))) (at_left 0)"
      using c' by real_asymp
    moreover have "eventually (λx::real. x < 0) (at_left 0)"
      by (auto simp: eventually_at intro: exI[of _ 1])
    ultimately show "eventually (λx. Lambert_W' x - ln (-x) ≤ c' * ln (-ln (-x))) (at_left 0)"
    proof eventually_elim
      case (elim x)
      hence "Lambert_W' x ≤ ln (-x) + c' * ln (-ln (-x))"
        by (intro Lambert_W'_leI)
      thus ?case by simp
    qed
  qed auto
  thus ?thesis by simp
qed

lemma Lambert_W'_asymp_equiv'_at_left_0 [asymp_equiv_intros]:
  "Lambert_W' ∼[at_left 0] (λx. ln (-x))"
proof -
  have "(λx. Lambert_W' x - ln (-x)) ∈ Θ[at_left 0](λx. -ln (-ln (-x)))"
    by (intro asymp_equiv_imp_bigtheta Lambert_W'_asymp_equiv_at_left_0)
  also have "(λx::real. -ln (-ln (-x))) ∈ o[at_left 0](λx. ln (-x))"
    by real_asymp
  finally show ?thesis by (simp add: asymp_equiv_altdef)
qed


text ‹
  Next, we look at the branching point $a := \tfrac{1}{e}$. Here, the asymptotic behaviour
  is as follows:
  \begin{align*}
    W(x) &= -1 + \sqrt{2e}(x - a)^{\frac{1}{2}} - \tfrac{2}{3}e(x-a) + o(x-a) &&\text{for} x\to a^+\\
    W'(x) &= -1 - \sqrt{2e}(x - a)^{\frac{1}{2}} - \tfrac{2}{3}e(x-a) + o(x-a) &&\text{for} x\to a^+
  \end{align*}
›
lemma sqrt_sqrt_mult:
  assumes "x ≥ (0 :: real)"
  shows   "sqrt x * (sqrt x * y) = x * y"
  using assms by (subst mult.assoc [symmetric]) auto

theorem Lambert_W_asymp_equiv_at_right_minus_exp_minus1:
  defines "e ≡ exp 1"
  defines "a ≡ -exp (-1)"
  defines "C1 ≡ sqrt (2 * exp 1)"
  defines "f ≡ (λx. -1 + C1 * sqrt (x - a))"
  shows   "(λx. Lambert_W x - f x) ∼[at_right a] (λx. -2/3 * e * (x - a))"
proof -
  define C :: "real ⇒ real" where "C = (λc. sqrt (2/e)/3 * (2*e+3*c))"
  have asymp_equiv: "(λx. (f x + c * (x - a)) * exp (f x + c * (x - a)) - x)
                       ∼[at_right a] (λx. C c * (x - a) powr (3/2))" if "c ≠ -2/3 * e" for c
  proof -
    from that have "C c ≠ 0"
      by (auto simp: C_def e_def)
    have "(λx. (f x + c * (x - a)) * exp (f x + c * (x - a)) - x - C c * (x - a) powr (3/2))
            ∈ o[at_right a](λx. (x - a) powr (3/2))"
      unfolding f_def a_def C_def C1_def e_def
      by (real_asymp simp: field_simps real_sqrt_mult real_sqrt_divide sqrt_sqrt_mult
                           exp_minus simp flip: sqrt_def)
    thus ?thesis
      using ‹C c ≠ 0› by (intro smallo_imp_asymp_equiv) auto
  qed
      
  show ?thesis
  proof (rule asymp_equiv_sandwich')
    fix c' :: real assume c': "c' ∈ {-e<..<-2/3*e}"
    hence neq: "c' ≠ -2/3 * e" by auto
    from c' have neg: "C c' < 0" unfolding C_def by (auto intro!: mult_pos_neg)
    hence "eventually (λx. C c' * (x - a) powr (3 / 2) < 0) (at_right a)"
      by real_asymp
    hence "eventually (λx. (f x + c' * (x - a)) * exp (f x + c' * (x - a)) - x < 0) (at_right a)"
      using asymp_equiv_eventually_neg_iff[OF asymp_equiv[OF neq]]
      by eventually_elim (use neg in auto)
    thus "eventually (λx. Lambert_W x - f x ≥ c' * (x - a)) (at_right a)"
    proof eventually_elim
      case (elim x)
      hence "Lambert_W x ≥ f x + c' * (x - a)"
        by (intro Lambert_W_geI) auto
      thus ?case by simp
    qed
  next
    fix c' :: real assume c': "c' ∈ {-2/3*e<..<0}"
    hence neq: "c' ≠ -2/3 * e" by auto
    from c' have pos: "C c' > 0" unfolding C_def by auto
    hence "eventually (λx. C c' * (x - a) powr (3 / 2) > 0) (at_right a)"
      by real_asymp
    hence "eventually (λx. (f x + c' * (x - a)) * exp (f x + c' * (x - a)) - x > 0) (at_right a)"
      using asymp_equiv_eventually_pos_iff[OF asymp_equiv[OF neq]]
      by eventually_elim (use pos in auto)
    moreover have "eventually (λx. - 1 ≤ f x + c' * (x - a)) (at_right a)"
                  "eventually (λx. x > a) (at_right a)"
      unfolding a_def f_def C1_def c' by real_asymp+
    ultimately show "eventually (λx. Lambert_W x - f x ≤ c' * (x - a)) (at_right a)"
    proof eventually_elim
      case (elim x)
      hence "Lambert_W x ≤ f x + c' * (x - a)"
        by (intro Lambert_W_leI) (auto simp: a_def)
      thus ?case by simp
    qed
  qed (auto simp: e_def)
qed

theorem Lambert_W'_asymp_equiv_at_right_minus_exp_minus1:
  defines "e ≡ exp 1"
  defines "a ≡ -exp (-1)"
  defines "C1 ≡ sqrt (2 * exp 1)"
  defines "f ≡ (λx. -1 - C1 * sqrt (x - a))"
  shows   "(λx. Lambert_W' x - f x) ∼[at_right a] (λx. -2/3 * e * (x - a))"
proof -
  define C :: "real ⇒ real" where "C = (λc. -sqrt (2/e)/3 * (2*e+3*c))"

  have asymp_equiv: "(λx. (f x + c * (x - a)) * exp (f x + c * (x - a)) - x)
                       ∼[at_right a] (λx. C c * (x - a) powr (3/2))" if "c ≠ -2/3 * e" for c
  proof -
    from that have "C c ≠ 0"
      by (auto simp: C_def e_def)
    have "(λx. (f x + c * (x - a)) * exp (f x + c * (x - a)) - x - C c * (x - a) powr (3/2))
            ∈ o[at_right a](λx. (x - a) powr (3/2))"
      unfolding f_def a_def C_def C1_def e_def
      by (real_asymp simp: field_simps real_sqrt_mult real_sqrt_divide sqrt_sqrt_mult
                           exp_minus simp flip: sqrt_def)
    thus ?thesis
      using ‹C c ≠ 0› by (intro smallo_imp_asymp_equiv) auto
  qed
      
  show ?thesis
  proof (rule asymp_equiv_sandwich')
    fix c' :: real assume c': "c' ∈ {-e<..<-2/3*e}"
    hence neq: "c' ≠ -2/3 * e" by auto
    from c' have pos: "C c' > 0" unfolding C_def by (auto intro!: mult_pos_neg)
    hence "eventually (λx. C c' * (x - a) powr (3 / 2) > 0) (at_right a)"
      by real_asymp
    hence "eventually (λx. (f x + c' * (x - a)) * exp (f x + c' * (x - a)) - x > 0) (at_right a)"
      using asymp_equiv_eventually_pos_iff[OF asymp_equiv[OF neq]]
      by eventually_elim (use pos in auto)
    moreover have "eventually (λx. x > a) (at_right a)"
                  "eventually (λx. f x + c' * (x - a) ≤ -1) (at_right a)"
      unfolding a_def f_def C1_def c' by real_asymp+
    ultimately show "eventually (λx. Lambert_W' x - f x ≥ c' * (x - a)) (at_right a)"
    proof eventually_elim
      case (elim x)
      hence "Lambert_W' x ≥ f x + c' * (x - a)"
        by (intro Lambert_W'_geI) (auto simp: a_def)
      thus ?case by simp
    qed
  next
    fix c' :: real assume c': "c' ∈ {-2/3*e<..<0}"
    hence neq: "c' ≠ -2/3 * e" by auto
    from c' have neg: "C c' < 0" unfolding C_def by auto
    hence "eventually (λx. C c' * (x - a) powr (3 / 2) < 0) (at_right a)"
      by real_asymp
    hence "eventually (λx. (f x + c' * (x - a)) * exp (f x + c' * (x - a)) - x < 0) (at_right a)"
      using asymp_equiv_eventually_neg_iff[OF asymp_equiv[OF neq]]
      by eventually_elim (use neg in auto)
    moreover have "eventually (λx. x < 0) (at_right a)"
      unfolding a_def by real_asymp
    ultimately show "eventually (λx. Lambert_W' x - f x ≤ c' * (x - a)) (at_right a)"
    proof eventually_elim
      case (elim x)
      hence "Lambert_W' x ≤ f x + c' * (x - a)"
        by (intro Lambert_W'_leI) auto
      thus ?case by simp
    qed
  qed (auto simp: e_def)
qed


text ‹
  Lastly, just for fun, we derive a slightly more accurate expansion of $W_0(x)$ for $x\to\infty$:
›
theorem Lambert_W_asymp_equiv_at_top'':
  "(λx. Lambert_W x - ln x + ln (ln x)) ∼[at_top] (λx. ln (ln x) / ln x)"
proof -
  have "(λx. Lambert_W x - ln x + ln (ln x)) ∼[at_top] (λx. 1 * (ln (ln x) / ln x))"
  proof (rule asymp_equiv_sandwich')
    fix c' :: real assume c': "c' ∈ {0<..<1}"
    define a where "a = (λx::real. ln x - ln (ln x) + c' * (ln (ln x) / ln x))"
    have "eventually (λx. a x * exp (a x) ≤ x) at_top"
      using c' unfolding a_def by real_asymp+
    thus "eventually (λx. Lambert_W x - ln x + ln (ln x) ≥ c' * (ln (ln x) / ln x)) at_top"
    proof eventually_elim
      case (elim x)
      hence "Lambert_W x ≥ a x"
        by (intro Lambert_W_geI)
      thus ?case by (simp add: a_def)
    qed
  next
    fix c' :: real assume c': "c' ∈ {1<..<2}"
    define a where "a = (λx::real. ln x - ln (ln x) + c' * (ln (ln x) / ln x))"
    have "eventually (λx. a x * exp (a x) ≥ x) at_top"
         "eventually (λx. a x ≥ -1) at_top"
      using c' unfolding a_def by real_asymp+
    thus "eventually (λx. Lambert_W x - ln x + ln (ln x) ≤ c' * (ln (ln x) / ln x)) at_top"
      using eventually_ge_at_top[of "-exp (-1)"]
    proof eventually_elim
      case (elim x)
      hence "Lambert_W x ≤ a x"
        by (intro Lambert_W_leI)
      thus ?case by (simp add: a_def)
    qed
  qed auto
  thus ?thesis by simp
qed

end