Theory Wooley_Elementary_Discrete_Inequality

(*Session: Wooley_Elementary_Discrete_Inequality
  Title: Wooley's Discrete Inequality
  Author: Angeliki Koutsoukou-Argyraki 
  Affiliation: Royal Holloway, University of London
  Date: 1 October 2024.*)

section‹Wooley's Discrete Inequality›

theory Wooley_Elementary_Discrete_Inequality 
  imports "HOL-Library.Quadratic_Discriminant" "HOL-Real_Asymp.Real_Asymp"

begin

text‹This is a formalisation of the proof of an inequality by Trevor D. Wooley attesting that when 
$\lambda > 0$, $$\min_{r \in \mathbb{N}}(r + \lambda/r) \leq \sqrt{4 \lambda +1}$$
with equality if and only if $\lambda = m(m-1)$ for some positive integer $m$.
The source is the note "An Elementary Discrete Inequality" available on Wooley's webpage 
\cite{Wooley_notes_inequality}:
\url{https://www.math.purdue.edu/~twooley/publ/20230410discineq.pdf}.›


subsection‹General elementary technical lemmas›

lemma obtains_nat_in_interval: 
  fixes x::real assumes "x0"
  obtains c::nat where "c  {x<.. x+1}" 
proof
  show "natx+1  {x<..x + 1}"
    using assms by force
qed

lemma obtains_nat_in_interval_greater_leq: 
  fixes x::real assumes "x0"
  obtains c::nat where "c >x" and "c  x+1" 
  by (meson assms greaterThanAtMost_iff obtains_nat_in_interval)

lemma obtains_nat_in_interval_half: 
  fixes x::real assumes "x1/2"
  obtains c::nat where "c > x - (1/2)" and "c  x+1/2" 
  using assms  obtains_nat_in_interval_greater_leq [of "x-1/2"]
  by (smt (verit) field_sum_of_halves)


subsection‹Trivial case, where we minimise over all positive real values of $r$›

theorem elementary_ineq_Wooley_real:
  fixes l::real and g::"real  real" 
  assumes "l>0" and " r  R. g r = r+(l/r)"
    and "R={r::real. r>0}" 
  shows "( r  R. g r   2* sqrt(l))  ( r  R. g (sqrt(l))  g r)"
proof-
  have " r  R. 2 * sqrt(l)+ (sqrt(r) - (sqrt(l)/sqrt(r)))^2 = r+(l/r)"
    using  assms   by (simp add: power_divide power2_diff)
  moreover
  have " r  R. 2 * sqrt(l)+ (sqrt(r) - (sqrt(l)/sqrt(r)))^2  2 *(sqrt(l))"
    using assms by auto
  ultimately have " r  R. r+(l/r)  2*sqrt(l)" by simp
  moreover
  have "g (sqrt(l)) = 2 *sqrt(l)" using assms by (simp add: real_div_sqrt)
  ultimately show  ?thesis using assms by auto
qed


subsection‹Main result: Inequality for the discrete version›

theorem elementary_discrete_ineq_Wooley:
  fixes l::real and g::"nat  real"
  assumes "l>0" and "R = {r::nat. r>0}" and " r  R. g r = r+ (l/r)"
  shows "(INF r  R. g r)  sqrt(4*l+1)"

proof-

  text‹We will first show the inequality for a specific choice of $r_u \in R$. Then the assertion of 
the theorem will be simply shown by transitivity.›

  define x::real where "x = sqrt(l+1/4)"
  with assms have "x>1/2"  
    by (smt (verit, best) real_sqrt_divide real_sqrt_four real_sqrt_less_iff real_sqrt_one)

  obtain r_u::nat where "r_u >x -1/2" and "r_u  x+1/2" 
    using obtains_nat_in_interval_half x>1/2 by (metis less_eq_real_def)
  have "r_u  R" using assms 1 / 2 < x x - 1 / 2 < real r_u by auto
  have ru_gt: "r_u > sqrt(l+1/4)-1/2" using r_u >x -1/2 x =sqrt(l+1/4) by blast
  have ru_le: "r_u  sqrt(l+1/4)+1/2" using r_u  x +1/2 x =sqrt(l+1/4) by blast

  text‹Proving the following auxiliary statement is the key part of the whole proof.›

  have auxiliary: "¦r_u - (l/r_u)¦  1"
  proof-
    define δ::real where "δ  = r_u - sqrt(l+1/4)" 
    with assms ru_gt δ_def ru_le 
    have δ: "δ > -1/2" "δ  1/2"
      by auto

    have a: "¦r_u - l/r_u¦ = ¦ ((sqrt(l+1/4) + δ)^2 -l)/(sqrt(l+1/4) + δ)¦" 
      using δ_def
      by (smt (verit, ccfv_SIG) 1 / 2 < x x - 1 / 2 < real r_u 
          add_divide_distrib nonzero_mult_div_cancel_right power2_eq_square)

    have b:"¦ ((sqrt(l+1/4) + δ)^2 -l)/(sqrt(l+1/4) + δ)¦ =  
¦2* δ +( ((1/4) - δ2)/(sqrt(l+1/4) + δ ))¦" 
    proof-
      have "¦((sqrt(l+1/4) + δ)^2 -l)/(sqrt(l+1/4) + δ) ¦ = 
 ¦(1/4 + 2*(sqrt(l+1/4))* δ+ δ2)/(sqrt(l+1/4) + δ) ¦"
        by (smt (verit, best) assms(1) divide_nonneg_nonneg power2_sum real_sqrt_pow2)
      also have " =  ¦ ( 2* δ* (sqrt(l+1/4))+ 2* δ2 + 1/4 -δ2 )/(sqrt(l+1/4) + δ)¦"
        by (smt (verit) power2_sum)
      also have " =  ¦ ( 2* δ* (sqrt(l+1/4)+ δ) + 1/4 -δ2 )/(sqrt(l+1/4) + δ)¦"
        by (smt (verit, ccfv_SIG) power2_diff power2_sum)
      also have " =  ¦ ( 2* δ* (sqrt(l+1/4)+ δ))/(sqrt(l+1/4) + δ) 
+ ((1/4 -δ2 )/(sqrt(l+1/4) + δ)) ¦ "
        by (metis add_diff_eq add_divide_distrib)
      also have  " = ¦ 2* δ + ((1/4 -δ2 )/(sqrt(l+1/4) + δ)) ¦  "
        using δ = real r_u - sqrt (l + 1 / 4) r_u  R assms by force
      finally show ?thesis .
    qed

    show ?thesis
      text‹We distinguish the cases $\delta > 0$ and $\delta \leq 0$:›
    proof (cases "δ > 0")
      case True
      define t::real where "t = 1/2 - δ"
      have c: "0  2* δ +(( 1/4 - δ2)/(sqrt(l+1/4) + δ ))"
      proof-
        have "δ2  1/4" using  δ  δ > 0
          by (metis less_eq_real_def plus_or_minus_sqrt real_sqrt_divide real_sqrt_four real_sqrt_le_iff real_sqrt_one real_sqrt_power) 
        then have "1/4 -δ2  0" 
          by simp
        then show ?thesis using δ > 0 assms by simp
      qed

      have d: "2* δ +( (1/4 - δ2)/(sqrt(l+1/4) + δ ))  1 -2*t + ((t-t2)/ (1-t))"
      proof-
        have "δ = 1/2 - t" using  t_def by simp
        then have "2* δ +( (1/4 - δ2)/(sqrt(l+1/4) + δ )) = 
                   2*(1/2 - t ) +( (1/4 - ( 1/2 - t)^2)/(sqrt(l+1/4) + 1/2 - t ))" 
          by simp
        also have  "  = 1 - 2*t + ( (1/4 - ( 1/4 -2*(1/2)* t+ t2))/(sqrt(l+1/4) + 1/2 - t ))"
          by (simp add: power2_diff power_divide)
        also have " =  1 - 2*t + ((t- t2)/(sqrt(l+1/4) + 1/2 - t )) " by simp
        also have "  1 -2*t + ((t-t2)/ (1-t))" 
        proof-
          have "sqrt(l+1/4) + 1/2  1"
            using 1/2 < x x_def by linarith
          then have *: "sqrt(l+1/4) + 1/2 -t   1 -t" by simp
          have "1-t  0 "  using t = 1/2 - δ δ >0 by linarith
          have "sqrt(l+1/4) + 1/2 -t  0" 
            using δ_def t = 1/2 - δ  δ >0 assms(1) by force
          then have "(1/(sqrt(l+1/4) + 1/2 - t )) (1/ (1-t))" 
            using * 1-t  0 by (smt (verit) True δ = 1/2 - t frac_le le_divide_eq_1_pos)
          have "t-t2 0" using  δ = 1/2 - t δ >0
            by (smt (verit, best) δ  1 / 2 field_sum_of_halves le_add_same_cancel1 nat_1_add_1 
                power_decreasing_iff
                power_one_right real_sqrt_pow2_iff real_sqrt_zero zero_less_one_class.zero_le_one)
          then have "((t-t2) /(sqrt(l+1/4) + 1/2 - t )) ((t-t2)/ (1-t))" 
            by (smt (verit) "*" True t = 1/2 - δ frac_le le_divide_eq_1_pos)
          then show ?thesis by force
        qed
        finally show ?thesis .
      qed

      have e: "1 -2*t + ((t-t2)/ (1-t))  1"
      proof-
        have "1 -2*t + ((t-t2)/ (1-t)) =  1-2*t + ((1-t)*t /(1-t))" by algebra
        also have " =  1- t"
          using c d by fastforce
        finally show ?thesis
          using δ t_def by linarith 
      qed

      show ?thesis using a b c d e by linarith

    next
      case False
      define t::real where "t = 1/2 + δ"
      then have "δ = t-1/2"by simp
      have "δ  0" using False by auto

      have "-( 2* δ +( ((1/4) - δ2)/(sqrt(l+1/4) + δ ))) = 
- ( 2* (t-1/2) +( ((1/4) - (t-1/2)^2)/(sqrt(l+1/4) + t - 1/2 )))"
        using  δ = t-1/2  by auto

      also have " =-( 2*t- 1 +( (  t-t2)/(sqrt(l+1/4) + t - 1/2 )))" 
        by (simp add: power2_diff power_divide)

      finally have ***: "-( 2* δ +( ((1/4) - δ2)/(sqrt(l+1/4) + δ ))) = 
-( 2*t- 1 +( (  t-t2)/(sqrt(l+1/4) + t - 1/2 )))" .

      have c:"-( 2* δ +( ((1/4) - δ2)/(sqrt(l+1/4) + δ )))  1 -2*t - ((t-t2)/ (sqrt(l+1/4)))"
      proof-
        have  c1: "sqrt(l+1/4) + t - 1/2  sqrt(l+1/4)"  
          using δ = t - 1 / 2 δ  0 by simp

        have "(sqrt(l+1/4) + t - 1/2)  0"  "sqrt(l+1/4)  0"
          using assms δ_def δ = t - 1/2 r_u  R by auto
        then
        have c2: "(t-t2)/(sqrt(l+1/4) + t - 1/2) (t-t2)/ sqrt(l+1/4)"  
          using c1 assms 
          by (smt (verit, best) δ_def ru_gt t = 1/2 + δ 
              field_sum_of_halves frac_le le_add_same_cancel1 nat_1_add_1 of_nat_0_le_iff 
              power_decreasing_iff power_one_right zero_less_one_class.zero_le_one)

        have c3: "- (t-t2)/(sqrt(l+1/4) + t - 1/2)  - (t-t2)/ sqrt(l+1/4)"  
          using c2  by linarith
        show ?thesis using *** c3 by linarith

      qed

      have d: "1 -2*t - ((t-t2)/ (sqrt(l+1/4)))  1"  
      proof-
        have *: "t >0" using δ > -1/2  t = 1/2 + δ by simp
        have **: "t  1" using  δ  0 t = 1/2 + δ by simp
        show ?thesis using * **
          by (smt (verit) assms(1) divide_nonneg_nonneg mult_le_cancel_right2 power2_eq_square real_sqrt_ge_0_iff)
      qed

      have e: "-( 2* δ +( ((1/4) - δ2)/(sqrt(l+1/4) + δ )))  1 -2*t - ((t-t2)/t)  "
      proof-
        have "-( 2* δ +( ((1/4) - δ2)/(sqrt(l+1/4) + δ ))) 
= -( 2*t- 1 +((t-t2)/(sqrt(l+1/4) + t - 1/2)))"
          using *** by simp

        have "( (  t-t2)/(sqrt(l+1/4) + t - 1/2 ))  (t-t2)/ t"
        proof-
          have : "(sqrt(l+1/4) + t - 1/2 )   t" using assms
            by (smt (verit, best) one_power2 power_divide real_sqrt_four real_sqrt_pow2 sqrt_le_D)
          moreover have "t >0" using δ > -1/2  t = 1/2 + δ by simp
          ultimately have "(sqrt(l+1/4) + t - 1/2 ) >0" 
            by auto
          show ?thesis using  (sqrt(l+1/4) + t - 1/2 ) >0 
              0 < t 
            by (smt (verit, best) δ  0 t = 1/2 + δ 
                frac_le le_add_same_cancel1 le_divide_eq_1_pos nat_1_add_1 power_decreasing_iff 
                power_one_right zero_less_one_class.zero_le_one)
        qed
        with *** show ?thesis by linarith

      qed
      have f: "1 -2*t - ((t-t2)/t)  -1/2" 
      proof-
        have "t >0" using δ > -1/2  t = 1/2 + δ by simp
        then have "1 -2*t - ((t-t2)/t) = 1-2*t -(1 -t)" 
          by (metis divide_diff_eq_iff less_irrefl one_eq_divide_iff power2_eq_square)
        also have " = -t" by auto
        finally show ?thesis 
          using δ  0 t = 1/2 + δ  by linarith
      qed
      show ?thesis using a b c d e f by linarith
    qed
  qed

  text‹The next step is to show that by the statement named "auxiliary" shown above, we can 
directly show the desired inequality for the specific $r_u \in R$:›

  have "(r_u - l/r_u)^2 1" 
    using auxiliary abs_square_le_1 by blast
  then have "(r_u^2 - 2*r_u* (l/r_u) + l^2/r_u^2 1)" 
    using power2_diff power_divide assms
    by (smt (verit) mult_2 of_nat_add of_nat_eq_of_nat_power_cancel_iff)
  then have "r_u^2 - 2*l + l^2/r_u^2 1" using assms r_u  R by force
  then have "r_u^2 + 2*l + l^2/r_u^2  ( 4*l+1)" by argo
  then have "r_u^2 + 2*r_u*(l/r_u) + l^2/r_u^2  ( 4*l+1)" using assms by simp
  then have "(r_u+ (l/r_u))^2  ( 4*l+1)"
    by (smt (verit, best) mult_2 of_nat_add of_nat_power_eq_of_nat_cancel_iff power2_sum 
        power_divide)
  then have "(r_u+ (l/r_u))  sqrt(4*l+1)" using real_le_rsqrt by blast
  moreover
  text‹The following shows that it is enough that we showed the inequality for the specific 
$r_u \in R$, as the statement of the theorem will then simply hold by transitivity.›

  have "(INF r  R. g r)  g r_u " 
  proof-
    have "bdd_below (g ` R)" unfolding bdd_below_def 
      using  assms image_iff 
      by (metis add_increasing assms(1) divide_nonneg_nonneg image_iff less_eq_real_def
          of_nat_0_le_iff)
    show ?thesis
      by (simp add: bdd_below (g ` R) r_u  R cINF_lower)
  qed
  ultimately show ?thesis using assms r_u  R by force
qed

subsection‹Special case: Equality for the discrete version›

text‹We will now show a special case of the main result where equality holds instead of inequality.› 

text‹We will need to make use of the following technical lemma, which will be used so as to 
guarantee that there exists a $p \in R$ for which the INF of $g(r)$ equals to $g(p)$. To this end, 
we will show that here the infimum INF can be identified with the minimum Min by restricting to a 
finite set. As the operator Min in Isabelle is used for finite sets and $R$ is infinite, we
used INF in the original formulation, however here Min and INF can be identified.›

text‹The following technical lemma is by Larry Paulson:›

lemma restrict_to_min:
  fixes l::real and g::"nat  real"
  assumes "l>0" and R_def: "R={r::nat. r>0}" and g_def: " r. g r = r + (l/r)"
  obtains F where "finite F" "F  R" "(INF r  R. g r) = Min (g ` F)" "F  {}"

proof -
  have ge0: "g r  0" for r
    using l>0 R_def g_def  by (auto simp: g_def) 
  then have bdd: "bdd_below (g ` R)"
    by (auto simp add: g_def R_def bdd_below_def)
  have "F n in sequentially. g 1 < g n"
    by (simp add: g_def) real_asymp
  then obtain N where "N>0" and N: "r. rN  g 1 < g r"
    by (metis Suc_leD eventually_sequentially less_Suc_eq_0_disj) 
  define F where "F = R  {..N}"
  have F: "finite F" "F  R"
    by (auto simp add: F_def)
  have "F  {}"
    using F_def R_def 0 < N by blast
  have "(INF r  R. g r) = (INF r  F. g r)"
  proof (intro order.antisym cInf_mono bdd)
    show "bdd_below (g ` F)"
      by (meson ge0 bdd_belowI2)
  next
    fix b
    assume "b  g ` R"
    then show "ag ` F. a  b"
      unfolding image_iff F_def R_def Bex_def
      by (metis N linorder_not_less IntI atMost_iff mem_Collect_eq nle_le zero_less_one)
  qed (use FR 0 < N in auto simp: R_def F_def)
  also have " = Min (g ` F)"
    using F  {} by (simp add: finite F cInf_eq_Min)
  finally have "(INF r  R. g r) = Min (g ` F)" .
  with F show thesis
    using that F  {} by blast
qed

text‹We will make use of the following calculation, which is convenient to formulate separately as
a lemma.›

lemma elementary_discrete_ineq_Wooley_quadratic_eq_sol:
  fixes l::real and g::"nat  real" 
  assumes "l>0" and " r. g r =r+ (l/r)" and "g r = sqrt(4*l+1)" 
  shows "(r = 1/2 + (1/2)* sqrt( 4*l +1))  (r = - 1/2 + (1/2)* sqrt(4*l +1))"
proof-
  have eq0: "r^2 - r*(sqrt( 4*l+1 )) + l = 0"  
  proof-
    have "r*( r + l/r) = r*(sqrt(4*l+1))" using assms by simp
    then have  "r^2 + r*(l/r) = r*(sqrt(4*l+1))"  
      by (simp add: distrib_left power2_eq_square)
    then show ?thesis
      by (smt (verit, ccfv_threshold) assms divide_eq_eq mult.commute real_sqrt_gt_1_iff)
  qed

  text‹Solving the above quadratic equation gives the following two roots:›

  have roots:"(r = 1/2 + (1/2)*sqrt( 4*l +1))(r = - 1/2 + (1/2)*sqrt(4*l+1))"
  proof-
    define a::real where "a = 1"
    define b::real where "b = - sqrt(4*l+1)"
    define c::real where "c = l"
    have "a*r^2 + b* r + c =0" using eq0 by (simp add: mult.commute a_def b_def c_def)
    then have A: "(r = (-b + sqrt( discrim a  b c))/ 2*a)  (r = (-b -sqrt( discrim a  b c))/ 2*a)"
      using discriminant_iff[of a r] a_def by simp
    have "discrim a b c = b^2 -4*a*c" 
      using discrim_def by simp
    then have B: "(r = (-b + sqrt(b^2 -4*a*c))/ 2*a)  (r = (-b -sqrt(b^2 -4*a*c))/ 2*a)"
      using A by auto
    then have C: "(r = (-b + sqrt(b^2 -4*c))/ 2)  (r = (-b -sqrt(b^2 -4*c))/ 2)"
      using a_def by simp
    have "b^2 -4*c = 1" using b_def c_def assms(1) by auto
    then have "(r = (-b + 1)/ 2)  (r = (-b - 1)/ 2)"
      using C by auto
    then show ?thesis using b_def by auto
  qed
  show ?thesis using roots by simp
qed


text‹The special case with equality involves a double implication (iff), and we start by showing 
one direction.›

theorem elementary_discrete_ineq_Wooley_special_case_1:
  fixes l::real and g::"nat  real" assumes "l>0" and "R={r::nat. r>0}" and " r. g r = r + (l/r)"
    and "(INF r  R. g r) = sqrt(4*l+1)"
  shows " m::nat. l =m*(m-1)"

proof-
  have " p  R. (INF r  R. g r) = g p"
  proof-
    obtain F where *:(INF r  R. g r) = Min (g ` F) and finite F and F  R F  {}
      using assms restrict_to_min by metis 
    then obtain p::nat where "  Min (g ` F)  = g p " "p  R"
      by (smt (verit) Min_in finite_imageI image_iff image_is_empty subsetD)
    with * show ?thesis by metis
  qed
  with assms
  obtain r_u::nat where "g r_u = sqrt(4*l+1)" and "r_u  R" 
    by metis
  then have ru: "(r_u + (l/r_u)) = sqrt( 4*l+1 )" 
    using assms by auto

  have "(r_u =  1/2 + (1/2)* sqrt( 4*l +1))  (l = r_u^2 - r_u)" 
  proof-
    assume "r_u =  1/2 + (1/2)* (sqrt( 4*l +1))"
    then have "2* r_u = 1 + sqrt( 4*l +1)" by simp
    then have "(2* real(r_u) -1)^2 = ( 4*l +1)" using assms by auto
    then have "(2*real(r_u))^2 -2*(2*real( r_u)) +1 = ( 4*l +1)" 
      by (simp add: power2_diff)
    then have "4*real(r_u)^2-4*(r_u) = 4*l" by fastforce
    then show "(l = r_u^2 - r_u )"  
      by (simp add: of_nat_diff power2_eq_square)
  qed
  moreover
  have "(r_u = - 1/2 + (1/2)* sqrt( 4*l +1)) (l =r_u^2 + r_u)"
  proof-
    assume "r_u = - 1/2 + (1/2)* sqrt(4*l +1)"    
    then have "2 * r_u +1 =  sqrt(4*l+1)" by simp
    then have "(2*r_u +1)^2 = (4*l+1)" using assms by auto
    then have "4*(r_u)^2 +4*r_u +1 = 4*l+1" 
      by (simp add: power2_eq_square)
    then show " (l =r_u^2 + r_u )"
      by (simp add: of_nat_diff power2_eq_square)
  qed
  moreover
  have "(r_u =  1/2 + (1/2)* sqrt( 4*l +1))  (r_u = - 1/2 + (1/2)* sqrt(4*l +1))"
    using assms ru elementary_discrete_ineq_Wooley_quadratic_eq_sol
      assms by auto
  ultimately have "(l =r_u^2 + r_u)  (l = r_u^2 - r_u)" 
    by blast
  then show ?thesis 
    by (metis add_implies_diff distrib_left mult.commute mult.right_neutral power2_eq_square right_diff_distrib')

  text‹(Interestingly, the above use of metis finished the proof in a simple step guaranteeing the 
existence of a witness with the desired property).›

qed


text‹Now we show the other direction.›

theorem elementary_discrete_ineq_Wooley_special_case_2:
  fixes l::real and g::"nat  real"
  assumes "l>0"  and  "R={r::nat. r>0}" and " r. g r =r+ (l/r)" and " m::nat. l =m*(m-1)"
  shows "(INF r  R. g r) = sqrt(4*l+1)"

proof-    

  obtain r_u::nat where "(l =r_u^2 + r_u)" using assms 
    by (metis add.commute add_cancel_left_right mult_eq_if power2_eq_square)
  then have "sqrt( 4*l +1)= sqrt(4*r_u^2 +4* r_u +1)" by simp
  moreover have "4*r_u^2 +4* r_u +1 =(2*r_u +1)^2"
    by (simp add: Groups.mult_ac(2) distrib_left power2_eq_square)
  ultimately have 4: "sqrt( 4*l +1)= sqrt((2*r_u +1)^2)" by metis
  then have ru: "r_u  = -1/2 + 1/2*sqrt( 4*l +1)" by (simp add: add_divide_distrib)

  text‹To prove the conclusion of the theorem, we will follow a proof by contradiction.›

  show ?thesis
  proof (rule ccontr)
    assume "Inf (g ` R)  sqrt (4 * l + 1)"
    then have inf: "(INF r  R. g r) < sqrt(4*l+1)"
      using assms less_eq_real_def elementary_discrete_ineq_Wooley by blast

    have " p  R. (INF r  R. g r) = g p" 
    proof-
      obtain F where *:(INF r  R. g r) = Min (g ` F) and finite F F  R F  {}
        using assms restrict_to_min by metis 
      then obtain p::nat where "Min (g ` F)  = g p " "p  R"
        by (meson Min_in finite_imageI imageE image_is_empty subsetD)
      with * show ?thesis by metis
    qed

    obtain p::nat where "p  R" and "(INF r  R. g r) = g p" using assms 
         p  R.  (INF r  R. g r) = g p by blast
    then have "(p+ l/p < sqrt( 4*l+1))"
      using inf assms(3) by auto 

    have "p*(p+ l/p) < p*(sqrt( 4*l+1))" 
      using p  R (p+ l/p < sqrt( 4*l+1)) assms by simp
    then have  "p^2 - p*(sqrt( 4*l+1))+ l<0"  
      by (smt (verit) p  R assms(2) distrib_left mem_Collect_eq nonzero_mult_div_cancel_left 
          of_nat_0_less_iff of_nat_mult power2_eq_square times_divide_eq_right)

    text‹We now need to find the possible values of this hypothetical $p \in R$, i.e. the roots of the 
above quadratic inequality. (These will be in-between the roots of the corresponding quadratic 
equation which were given in lemma @{thm elementary_discrete_ineq_Wooley_quadratic_eq_sol}). 
Here we show that the roots of the quadratic inequality lie in the following interval via a direct 
calculation:›

    have p: "(p < (sqrt(4*l+1) + 1) / 2)  (p >(sqrt(4*l+1) - 1) / 2)"
    proof-
      have "p^2 - p*(sqrt(4*l+1))+ l +1/4 < 1/4" 
        using p^2 - p*(sqrt(4*l+1))+ l<0 by simp
      moreover
      have "- (2*(p* sqrt(4*l +1))/2) + (4* l +1)/4 = - p*(sqrt(4*l+1))+ l +1/4"
        by force
      ultimately have ***: "p^2 - (2*(p* sqrt(4*l +1))/2) + (4* l +1)/4  <1/4" 
        by linarith
      have ****: "(p -(sqrt(4*l +1))/2)^2 = p^2 -2 * p* (sqrt(4*l +1))/2+ ( (sqrt(4*l +1))/2)^2" 
        by (simp add: power2_diff)
      then have "p^2 -2 * p* (sqrt(4*l+1))/2+ ((sqrt(4*l +1))/2)^2 = p^2 -2 * p* (sqrt(4*l +1))/2+ (4*l +1)/4"
        by (smt (verit) assms(1) power_divide real_sqrt_four real_sqrt_pow2)
      then have "(p -(sqrt(4*l +1))/2)^2 <1/4" using *** **** by linarith
      then have "¦(p -(sqrt(4*l +1))/2) ¦ <1/2" 
        by (metis real_sqrt_abs real_sqrt_divide real_sqrt_four real_sqrt_less_mono real_sqrt_one)
      then have "((p -(sqrt(4*l +1))/2) ) <1/2"  "((p -(sqrt(4*l +1))/2) ) > -1/2" by linarith+
      then show ?thesis 
        by force
    qed

    text‹So $p$ lies in an interval of length strictly less than 1 between two positive integers, but 
this means that $p$ cannot be a positive integer, which yields the desired contradiction, thus 
completing the proof:›

    obtain A::nat where A: "real A = - 1/2 + (1/2)* sqrt(4*l +1)"
      using ru by blast
    then show False
      using "4" p by fastforce
  qed
qed



text‹Finally, for convenience and completeness, we state the special case where equality holds 
formulated with the double implication and moreover including the values for which the INF (i.e.
minimum here as we have seen) is attained as previously calculated.›

theorem elementary_discrete_ineq_Wooley_special_case_iff:
  fixes l::real and g::"nat  real" 
  assumes "l>0" and "R={r::nat. r>0}" and " r. g r = r+ (l/r)"
  shows "((INF r  R. g r) = sqrt(4*l+1))  ( m::nat. l =m*(m-1))" 
    and 
    "g p =sqrt(4*l+1)  (p = 1/2 + (1/2)* sqrt( 4*l +1))  (p = -1/2 + (1/2)* sqrt(4*l +1))"
  using assms elementary_discrete_ineq_Wooley_special_case_1
    elementary_discrete_ineq_Wooley_special_case_2 
  apply blast
  using assms(1) assms(3) elementary_discrete_ineq_Wooley_quadratic_eq_sol restrict_to_min
  by auto

end