Theory Relation_of_PNTs

theory Relation_of_PNTs
imports
  "PNT_Remainder_Library"
begin
unbundle pnt_syntax
unbundle prime_counting_syntax

section ‹Implication relation of many forms of prime number theorem›

definition rem_est :: "real ⇒ real ⇒ real ⇒ _" where
"rem_est c m n ≡ O(λ x. x * exp (-c * ln x powr m * ln (ln x) powr n))"

definition Li :: "real ⇒ real" where "Li x ≡ integral {2..x} (λx. 1 / ln x)"
definition PNT_1 where "PNT_1 c m n ≡ ((λx. π x - Li x) ∈ rem_est c m n)"
definition PNT_2 where "PNT_2 c m n ≡ ((λx. θ x - x) ∈ rem_est c m n)"
definition PNT_3 where "PNT_3 c m n ≡ ((λx. ψ x - x) ∈ rem_est c m n)"

lemma rem_est_compare_powr:
  fixes c m n :: real
  assumes h: "0 < m" "m < 1"
  shows "(λx. x powr (2 / 3)) ∈ rem_est c m n"
  unfolding rem_est_def using assms
  by (cases c "0 :: real" rule: linorder_cases; real_asymp)

lemma PNT_3_imp_PNT_2:
  fixes c m n :: real
  assumes h: "0 < m" "m < 1" and "PNT_3 c m n"
  shows "PNT_2 c m n"
proof -
  have 1: "(λ x. ψ x - x) ∈ rem_est c m n"
    using assms(3) unfolding PNT_3_def by auto
  have "(λx. ψ x - θ x) ∈ O(λx. ln x * sqrt x)" by (rule ψ_minus_θ_bigo)
  moreover have "(λx. ln x * sqrt x) ∈ O(λx. x powr (2 / 3))" by real_asymp
  ultimately have 2: "(λx. ψ x - θ x) ∈ rem_est c m n"
    using rem_est_compare_powr [OF h, of c n] unfolding rem_est_def
    by (blast intro: landau_o.big.trans)
  have "(λx. ψ x - x - (ψ x - θ x)) ∈ rem_est c m n"
    using 1 2 unfolding rem_est_def by (rule sum_in_bigo)
  thus ?thesis unfolding PNT_2_def by simp
qed

definition r1 where "r1 x ≡ π x - Li x" for x
definition r2 where "r2 x ≡ θ x - x" for x

lemma pi_represent_by_theta:
  fixes x :: real
  assumes "2 ≤ x"
  shows "π x = θ x / (ln x) + integral {2..x} (λt. θ t / (t * (ln t)2))"
proof -
  note integral_unique [OF π_conv_θ_integral]
  with assms show ?thesis by auto
qed

lemma Li_integrate_by_part:
  fixes x :: real
  assumes "2 ≤ x"
  shows
  "(λx. 1 / (ln x)2) integrable_on {2..x}"
  "Li x = x / (ln x) - 2 / (ln 2) + integral {2..x} (λt. 1 / (ln t)2)"
proof -
  have "(λx. x * (- 1 / (x * (ln x)2))) integrable_on {2..x}"
    by (rule integrable_continuous_interval)
       ((rule continuous_intros)+, auto)
  hence "(λx. - (if x = 0 then 0 else 1 / (ln x)2)) integrable_on {2..x}"
    by simp
  moreover have "((λt. 1 / ln t) has_vector_derivative -1 / (t * (ln t)2)) (at t)"
    when Ht: "2 ≤ t" for t
  proof -
    define a where "a ≡ (0 * ln t - 1 * (1 / t))/(ln t * ln t)"
    have "DERIV (λt. 1 / (ln t)) t :> a"
    unfolding a_def
    proof (rule derivative_intros DERIV_ln_divide)+
      from Ht show "0 < t" by linarith
      note ln_gt_zero and Ht thus "ln t ≠ 0" by auto
    qed
    also have "a = -1 / (t * (ln t)2)"
      unfolding a_def by (simp add: power2_eq_square)
    finally have "DERIV (λt. 1 / (ln t)) t :> -1 / (t * (ln t)2)" by auto
    thus ?thesis
      by (subst has_real_derivative_iff_has_vector_derivative [symmetric])
  qed
  ultimately have "((λx. 1 * (1 / ln x)) has_integral
    x * (1 / ln x) - 2 * (1 / ln 2) - integral {2..x} (λx. x * (-1 / (x * (ln x)2))))
    {2..x}"
    using ‹2 ≤ x› by (intro integration_by_part') auto
  note 3 = this [simplified]
  have "((λx. 1 / ln x) has_integral (x / ln x - 2 / ln 2 + integral {2..x} (λx. 1 / (ln x)2))) {2..x}"
  proof -
    define a where "a t ≡ if t = 0 then 0 else 1 / (ln t)2" for t :: real
    have "⋀t :: real. t ∈ {2..x} ⟹ a t = 1 / (ln t)2"
      unfolding a_def by auto
    hence 4: "integral {2..x} a = integral {2..x} (λx. 1 / (ln x)2)" by (rule integral_cong)
    from 3 show ?thesis
      by (subst (asm) 4 [unfolded a_def])
  qed
  thus "Li x = x / ln x - 2 / ln 2 + integral {2..x} (λt. 1 / (ln t)2)" unfolding Li_def by auto
  show "(λx. 1 / (ln x)2) integrable_on {2..x}"
    by (rule integrable_continuous_interval)
       ((rule continuous_intros)+, auto)
qed

lemma θ_integrable:
  fixes x :: "real"
  assumes "2 ≤ x"
  shows "(λt. θ t / (t * (ln t)2)) integrable_on {2..x}"
by (rule π_conv_θ_integral [THEN has_integral_integrable], rule assms)

lemma r1_represent_by_r2:
  fixes x :: real
  assumes Hx: "2 ≤ x"
  shows "(λt. r2 t / (t * (ln t)2)) integrable_on {2..x}" (is ?P)
    "r1 x = r2 x / (ln x) + 2 / ln 2 + integral {2..x} (λt. r2 t / (t * (ln t)2))" (is ?Q)
proof -
  have 0: "⋀t. t ∈ {2..x} ⟹ (θ t - t) / (t * (ln t)2) = θ t / (t * (ln t)2) - 1 / (ln t)2"
    by (subst diff_divide_distrib, auto)
  note integrables = θ_integrable Li_integrate_by_part(1)
  let ?D = "integral {2..x} (λt. θ t / (t * (ln t)2)) -
    integral {2..x} (λt. 1 / (ln t)2)"
  have "((λt. θ t / (t * (ln t)2) - 1 / (ln t)2) has_integral
    ?D) {2..x}"
  unfolding r2_def by
    (rule has_integral_diff)
    (rule integrables [THEN integrable_integral], rule Hx)+
  hence 0: "((λt. r2 t / (t * (ln t)2)) has_integral
    ?D) {2..x}"
  unfolding r2_def by (subst has_integral_cong [OF 0])
  thus ?P by (rule has_integral_integrable)
  note 1 = 0 [THEN integral_unique]
  have 2: "r2 x / ln x = θ x / ln x - x / ln x"
    unfolding r2_def by (rule diff_divide_distrib)
  from pi_represent_by_theta and Li_integrate_by_part(2) and assms
  have "π x - Li x = θ x / ln x
    + integral {2..x} (λt. θ t / (t * (ln t)2))
    - (x / ln x - 2 / ln 2 + integral {2..x} (λt. 1 / (ln t)2))"
    by auto
  also have "… = r2 x / ln x + 2 / ln 2
    + integral {2..x} (λt. r2 t / (t * (ln t)2))"
    by (subst 2, subst 1) auto
  finally show ?Q unfolding r1_def by auto
qed

lemma exp_integral_asymp:
  fixes f f' :: "real ⇒ real"
  assumes cf: "continuous_on {a..} f"
      and der: "⋀x. a < x ⟹ DERIV f x :> f' x"
      and td: "((λx. x * f' x) ⤏ 0) at_top"
      and f_ln: "f ∈ o(ln)"
  shows "(λx. integral {a..x} (λt. exp (-f t))) ∼[at_top] (λx. x * exp(-f x))"
proof (rule asymp_equivI', rule lhospital_at_top_at_top)
  have cont_exp: "continuous_on {a..} (λt. exp (- f t))"
    using cf by (intro continuous_intros)
  show "∀F x in at_top. ((λx. integral {a..x} (λt. exp (- f t)))
    has_real_derivative exp (- f x)) (at x)" (is "eventually ?P ?F")
  proof (rule eventually_at_top_linorderI')
    fix x assume 1: "a < x"
    hence 2: "a ≤ x" by linarith
    have 3: "(at x within {a..x+1}) = (at x)"
      by (rule at_within_interior) (auto intro: 1)
    show "?P x"
      by (subst 3 [symmetric], rule integral_has_real_derivative)
         (rule continuous_on_subset [OF cont_exp], auto intro: 2)
  qed
  have "∀F x in at_top. ((λx. x * exp (- f x))
    has_real_derivative 1 * exp (- f x) + exp (- f x) * (- f' x) * x) (at x)"
    (is "eventually ?P ?F")
  proof (rule eventually_at_top_linorderI')
    fix x assume 1: "a < x"
    hence 2: "(at x within {a<..}) = (at x)" by (auto intro: at_within_open)
    show "?P x"
      by (subst 2 [symmetric], intro derivative_intros)
         (subst 2, rule der, rule 1)
  qed
  moreover have
    "1 * exp (- f x) + exp (- f x) * (- f' x) * x
    = exp (- f x) * (1 - x * f' x)" for x :: real
    by (simp add: field_simps)
  ultimately show "∀F x in at_top.
       ((λx. x * exp (- f x))
    has_real_derivative exp (- f x) * (1 - x * f' x)) (at x)" by auto
  show "LIM x at_top. x * exp (- f x) :> at_top"
    using f_ln by (rule smallo_ln_diverge_1)
  have "((λx. 1 / (1 - x * f' x)) ⤏ 1 / (1 - 0)) at_top"
    by ((rule tendsto_intros)+, rule td, linarith)
  thus "((λx. exp (- f x) / (exp (- f x) * (1 - x * f' x))) ⤏ 1) at_top" by auto
  have "((λx. 1 - x * f' x) ⤏ 1 - 0) at_top"
    by ((rule tendsto_intros)+, rule td)
  hence 0: "((λx. 1 - x * f' x) ⤏ 1) at_top" by simp
  hence "∀F x in at_top. 0 < 1 - x * f' x"
    by (rule order_tendstoD) linarith
  moreover have "∀F x in at_top. 0 < 1 - x * f' x ⟶ exp (- f x) * (1 - x * f' x) ≠ 0" by auto
  ultimately show "∀F x in at_top. exp (- f x) * (1 - x * f' x) ≠ 0"
    by (rule eventually_rev_mp)
qed

lemma x_mul_exp_larger_than_const:
  fixes c :: real and g :: "real ⇒ real"
  assumes g_ln: "g ∈ o(ln)"
  shows "(λx. c) ∈ O(λx. x * exp(-g x))"
proof -
  have "LIM x at_top. x * exp (- g x) :> at_top"
    using g_ln by (rule smallo_ln_diverge_1)
  hence "∀F x in at_top. 1 ≤ x * exp (- g x)"
    using filterlim_at_top by fast
  hence "∀F x in at_top. ∥c∥ * 1 ≤ ∥c∥ * ∥x * exp (- g x)∥"
    by (rule eventually_rev_mp)
       (auto simp del: mult_1_right
             intro!: eventuallyI mult_left_mono)
  thus "(λx. c :: real) ∈ O(λx. x * exp (- g x))" by auto
qed

lemma integral_bigo_exp':
  fixes a :: real and f g g' :: "real ⇒ real"
  assumes f_bound: "f ∈ O(λx. exp(-g x))"
    and Hf:   "⋀x. a ≤ x ⟹ f integrable_on {a..x}"
    and Hf':  "⋀x. a ≤ x ⟹ (λx. ¦f x¦) integrable_on {a..x}"
    and Hg:   "continuous_on {a..} g"
    and der:  "⋀x. a < x ⟹ DERIV g x :> g' x"
    and td:   "((λx. x * g' x) ⤏ 0) at_top"
    and g_ln: "g ∈ o(ln)"
  shows "(λx. integral{a..x} f) ∈ O(λx. x * exp(-g x))"
proof -
  have "⋀y. continuous_on {a..y} g"
    by (rule continuous_on_subset, rule Hg) auto
  hence "⋀y. (λx. exp(-g x)) integrable_on {a..y}"
    by (intro integrable_continuous_interval)
       (rule continuous_intros)+
  hence "⋀y. (λx. ¦exp(-g x)¦) integrable_on {a..y}" by simp
  hence "(λx. integral{a..x} f) ∈ O(λx. 1 + integral{a..x} (λx. ¦exp(-g x)¦))"
    using assms by (intro integral_bigo)
  hence "(λx. integral{a..x} f) ∈ O(λx. 1 + integral{a..x} (λx. exp(-g x)))" by simp
  also have "(λx. 1 + integral{a..x} (λx. exp(-g x))) ∈ O(λx. x * exp(-g x))"
  proof (rule sum_in_bigo)
    show "(λx. 1 :: real) ∈ O(λx. x * exp (- g x))"
      by (intro x_mul_exp_larger_than_const g_ln)
    show "(λx. integral {a..x} (λx. exp (- g x))) ∈ O(λx. x * exp (- g x))"
      by (rule asymp_equiv_imp_bigo, rule exp_integral_asymp, auto intro: assms)
  qed
  finally show ?thesis .
qed

lemma integral_bigo_exp:
  fixes a b :: real and f g g' :: "real ⇒ real"
  assumes le: "a ≤ b"
    and f_bound: "f ∈ O(λx. exp(-g x))"
    and Hf:  "⋀x. a ≤ x ⟹ f integrable_on {a..x}"
    and Hf': "⋀x. b ≤ x ⟹ (λx. ¦f x¦) integrable_on {b..x}"
    and Hg:  "continuous_on {b..} g"
    and der: "⋀x. b < x ⟹ DERIV g x :> g' x"
    and td:  "((λx. x * g' x) ⤏ 0) at_top"
    and g_ln:"g ∈ o(ln)"
  shows "(λx. integral {a..x} f) ∈ O(λx. x * exp(-g x))"
proof -
  have "(λx. integral {a..b} f) ∈ O(λx. x * exp(-g x))"
    by (intro x_mul_exp_larger_than_const g_ln)
  moreover have "(λx. integral {b..x} f) ∈ O(λx. x * exp(-g x))"
    by (intro integral_bigo_exp' [where ?g' = g']
              f_bound Hf Hf' Hg der td g_ln)
       (use le Hf integrable_cut' in auto)
  ultimately have "(λx. integral {a..b} f + integral {b..x} f) ∈ O(λx. x * exp(-g x))"
    by (rule sum_in_bigo)
  moreover have "integral {a..x} f = integral {a..b} f + integral {b..x} f" when "b ≤ x" for x
    by (subst eq_commute, rule Henstock_Kurzweil_Integration.integral_combine)
       (insert le that, auto intro: Hf)
  hence "∀F x in at_top. integral {a..x} f = integral {a..b} f + integral {b..x} f"
    by (rule eventually_at_top_linorderI)
  ultimately show ?thesis
    by (simp add: landau_o.big.in_cong)
qed

lemma integrate_r2_estimate:
  fixes c m n :: real
  assumes hm: "0 < m" "m < 1"
    and h: "r2 ∈ rem_est c m n"
  shows "(λx. integral {2..x} (λt. r2 t / (t * (ln t)2))) ∈ rem_est c m n"
unfolding rem_est_def
proof (subst mult.assoc,
       subst minus_mult_left [symmetric],
       rule integral_bigo_exp)
  show "(2 :: real) ≤ 3" by auto
  show "(λx. c * (ln x powr m * ln (ln x) powr n)) ∈ o(ln)"
    using hm by real_asymp
  have "ln x ≠ 1" when "3 ≤ x" for x :: real
    using ln_when_ge_3 [of x] that by auto
  thus "continuous_on {3..} (λx. c * (ln x powr m * ln (ln x) powr n))"
    by (intro continuous_intros) auto
  show "(λt. r2 t / (t * (ln t)2)) integrable_on {2..x}"
    if "2 ≤ x" for x using that by (rule r1_represent_by_r2(1))
  define g where "g x ≡
    c * (m * ln x powr (m - 1) * (1 / x * 1) * ln (ln x) powr n
       + n * ln (ln x) powr (n - 1) * (1 / ln x * (1 / x)) * ln x powr m)"
    for x
  show "((λx. c * (ln x powr m * ln (ln x) powr n)) has_real_derivative g x) (at x)"
    if "3 < x" for x
  proof -
    have *: "at x within {3<..} = at x"
      by (rule at_within_open) (auto intro: that)
    moreover have
      "((λx. c * (ln x powr m * ln (ln x) powr n)) has_real_derivative g x)
       (at x within {3<..})"
    unfolding g_def using that
    by (intro derivative_intros DERIV_mult DERIV_cmult)
       (auto intro: ln_when_ge_3 DERIV_ln_divide simp add: *)
    ultimately show ?thesis by auto
  qed
  show "((λx. x * g x) ⤏ 0) at_top"
    unfolding g_def using hm by real_asymp
  have nz: "∀F t :: real in at_top. t * (ln t)2 ≠ 0"
  proof (rule eventually_at_top_linorderI')
    fix x :: real assume "1 < x"
    thus "x * (ln x)2 ≠ 0" by auto
  qed
  define h where "h x ≡ exp (- c * ln x powr m * ln (ln x) powr n)" for x
  have "(λt. r2 t / (t * (ln t)2)) ∈ O(λx. (x * h x) / (x * (ln x)2))"
    by (rule landau_o.big.divide_right, rule nz)
       (unfold h_def, fold rem_est_def, rule h)
  also have "(λx. (x * h x) / (x * (ln x)2)) ∈ O(λx. h x)"
  proof -
    have "(λx :: real. 1 / (ln x)2) ∈ O(λx. 1)" by real_asymp
    hence "(λx. h x * (1 / (ln x)2)) ∈ O(λx. h x * 1)"
      by (rule landau_o.big.mult_left)
    thus ?thesis
      by (auto simp add: field_simps intro!: landau_o.big.ev_eq_trans2)
  qed
  finally show "(λt. r2 t / (t * (ln t)2))
    ∈ O(λx. exp (- (c * (ln x powr m * ln (ln x) powr n))))"
    unfolding h_def by (simp add: algebra_simps)
  have "(λx. r2 x / (x * (ln x)2)) absolutely_integrable_on {2..x}"
    if *:"2 ≤ x" for x
  proof (rule set_integrableI_bounded)
    show "{2..x} ∈ sets lebesgue" by auto
    show "emeasure lebesgue {2..x} < ∞" using * by auto
    have "(λt. r2 t / (t * (ln t)2) * indicator {2..x} t) ∈ borel_measurable lebesgue"
      using * by (intro integrable_integral
        [THEN has_integral_implies_lebesgue_measurable_real])
        (rule r1_represent_by_r2(1))
    thus "(λt. indicat_real {2..x} t *R (r2 t / (t * (ln t)2))) ∈ borel_measurable lebesgue"
      by (simp add: mult_ac)
    let ?C = "(ln 4 + 1) / (ln 2)2 :: real"
    show "AE t∈{2..x} in lebesgue. ∥r2 t / (t * (ln t)2)∥ ≤ ?C"
    proof (rule AE_I2, safe)
      fix t assume "t ∈ {2..x}"
      hence h: "1 ≤ t" "2 ≤ t" by auto
      hence "0 ≤ θ t ∧ θ t < ln 4 * t" by (auto intro: θ_upper_bound)
      hence *:"¦θ t¦ ≤ ln 4 * t" by auto
      have "1 ≤ ln t / ln 2" using h by auto
      hence "1 ≤ (ln t / ln 2)2" by auto
      also have "… = (ln t)2 / (ln 2)2" unfolding power2_eq_square by auto
      finally have "1 ≤ (ln t)2 / (ln 2)2" .
      hence "¦r2 t¦ ≤ ¦θ t¦ + ¦t¦" unfolding r2_def by auto
      also have "… ≤ ln 4 * t + 1 * t" using h * by auto
      also have "… = (ln 4 + 1) * t" by (simp add: algebra_simps)
      also have "… ≤ (ln 4 + 1) * t * ((ln t)2 / (ln 2)2)"
        by (auto simp add: field_simps)
           (rule add_mono; rule rev_mp[OF h(2)], auto)
      finally have *:"¦r2 t¦ ≤ ?C * (t * (ln t)2)" by auto
      thus "∥r2 t / (t * (ln t)2)∥ ≤ ?C"
        using h * by (auto simp add: field_simps)
    qed
  qed
  hence "⋀x. 2 ≤ x ⟹ (λx. ¦r2 x / (x * (ln x)2)¦) integrable_on {2..x}"
    by (fold real_norm_def)
       (rule absolutely_integrable_on_def [THEN iffD1, THEN conjunct2])
  thus "⋀x. 3 ≤ x ⟹ (λx. ¦r2 x / (x * (ln x)2)¦) integrable_on {3..x}"
    using ‹2 ≤ 3› integrable_cut' by blast
qed

lemma r2_div_ln_estimate:
  fixes c m n :: real
  assumes hm: "0 < m" "m < 1"
    and h: "r2 ∈ rem_est c m n"
  shows "(λx. r2 x / (ln x) + 2 / ln 2) ∈ rem_est c m n"
proof -
  have "(λx. r2 x / ln x) ∈ O(r2)"
  proof (intro bigoI eventually_at_top_linorderI)
    fix x :: real assume 1:"exp 1 ≤ x"
    have 2:"(0 :: real) < exp 1" by simp
    hence 3:"0 < x" using 1 by linarith
    have 4: "0 ≤ ¦r2 x¦" by auto
    have "(1 :: real) = ln (exp 1)" by simp
    also have "… ≤ ln x" using 1 2 3 by (subst ln_le_cancel_iff)
    finally have "1 ≤ ln x" .
    thus "∥r2 x / ln x∥ ≤ 1 * ∥r2 x∥"
      by (auto simp add: field_simps, subst mult_le_cancel_right1, auto)
  qed
  with h have 1: "(λx. r2 x / ln x) ∈ rem_est c m n"
    unfolding rem_est_def using landau_o.big_trans by blast
  moreover have "(λx :: real. 2 / ln 2) ∈ O(λx. x powr (2 / 3))"
    by real_asymp
  hence "(λx :: real. 2 / ln 2) ∈ rem_est c m n"
    using rem_est_compare_powr [OF hm, of c n]
    unfolding rem_est_def by (rule landau_o.big.trans)
  ultimately show ?thesis
    unfolding rem_est_def by (rule sum_in_bigo)
qed

lemma PNT_2_imp_PNT_1:
  fixes l :: real
  assumes h: "0 < m" "m < 1" and "PNT_2 c m n"
  shows "PNT_1 c m n"
proof -
  from assms(3) have h': "r2 ∈ rem_est c m n"
    unfolding PNT_2_def r2_def by auto
  let ?a = "λx. r2 x / ln x + 2 / ln 2"
  let ?b = "λx. integral {2..x} (λt. r2 t / (t * (ln t)2))"
  have 1: "∀F x in at_top. π x - Li x = ?a x + ?b x"
    by (rule eventually_at_top_linorderI, fold r1_def)
       (rule r1_represent_by_r2(2), blast)
  have 2: "(λx. ?a x + ?b x) ∈ rem_est c m n"
    by (unfold rem_est_def, (rule sum_in_bigo; fold rem_est_def))
       (intro r2_div_ln_estimate integrate_r2_estimate h h')+
  from landau_o.big.in_cong [OF 1] and 2 show ?thesis
    unfolding PNT_1_def rem_est_def by blast
qed

theorem PNT_3_imp_PNT_1:
  fixes l :: real
  assumes h : "0 < m" "m < 1" and "PNT_3 c m n"
  shows "PNT_1 c m n"
  by (intro PNT_2_imp_PNT_1 PNT_3_imp_PNT_2 assms)

hide_const (open) r1 r2
unbundle no prime_counting_syntax and no pnt_syntax

end