Theory Zeta5_Archimedean_Bound
theory Zeta5_Archimedean_Bound
imports Zeta5_Numeric_Enclosures Andreief_Identity
begin
section ‹The archimedean bound: Proposition 6.3›
text ‹Section 6 of the paper: the bound (6.11) on the weight, (6.10)
by Andreief's identity, the
one-coordinate bound (6.12), the bound (6.9) for every configuration through the logarithmic
energy of ‹ρ› and the zero-mass energy inequality, and the estimates (6.14),
(6.15) leading to
Proposition 6.3 (@{text log_FK_zeta5_bound}): ‹ln F⇩K(ζ(5)) ≤
@{text Ubar} ⋅ K⇧2 + O(K ln K)›. Lean theories
@{text Section6}, @{text Energy6}, @{text Section6b}, @{text Section6c}, @{text Config69}.›
subsection ‹(6.11) and Lemma 6.2›
text ‹(6.11): @{text "w(y) ≤ 8192(1+y)^5e^{-2πy}"}.›
lemma binomial_term_le:
fixes t :: real
assumes "0 ≤ t"
shows "real (n choose k) * t ^ k ≤ (1 + t) ^ n"
proof (cases "k ≤ n")
case True
have "(t + 1) ^ n = (∑ i ≤ n. real (n choose i) * t ^ i * 1 ^ (n - i))"
by (rule binomial_ring)
also have "… ≥ real (n choose k) * t ^ k * 1 ^ (n - k)"
by (rule member_le_sum) (use assms True in auto)
finally show ?thesis by (simp add: add.commute)
next
case False
hence "n < k" by simp
thus ?thesis using assms by (simp add: binomial_eq_0)
qed
lemma pow4_exp_bound:
fixes x :: real
assumes "0 ≤ x"
shows "x ^ 4 * exp (- x) ≤ 42"
proof -
have "exp (x / 12) ≥ 1 + x / 12" by (rule exp_ge_add_one_self)
hence "(1 + x / 12) ^ 12 ≤ exp (x / 12) ^ 12" using assms by (intro power_mono) auto
also have "exp (x / 12) ^ 12 = exp x" by (simp flip: exp_of_nat_mult)
finally have e: "(1 + x / 12) ^ 12 ≤ exp x" .
have "real (12 choose 4) * (x / 12) ^ 4 ≤ (1 + x / 12) ^ 12"
by (rule binomial_term_le) (use assms in simp)
moreover have "(12 choose 4) = (495 :: nat)"
using binomial_fact_lemma[of 4 12] by (simp add: fact_numeral)
ultimately have "495 * (x / 12) ^ 4 ≤ exp x" using e by simp
hence "x ^ 4 ≤ 20736 / 495 * exp x" by (simp add: power_divide field_simps)
also have "… ≤ 42 * exp x" by simp
finally show ?thesis by (simp add: exp_minus field_simps)
qed
theorem weight_le: "0 < y ⟹ weight y ≤ 8192 * (1 + y) ^ 5 * exp (- 2 * pi * y)"
proof -
assume y: "0 < y"
define Y where "Y = min y 1"
define s where "s = pi * Y"
have Y0: "0 < Y" "Y ≤ y" "Y ≤ 1" using y by (auto simp: Y_def)
have s0: "0 < s" and spi: "s ≤ pi" using Y0 by (auto simp: s_def)
define a where "a l = real (l + 1) ^ 4 * exp (- 2 * pi * real (l + 1) * y)" for l
define b where "b l = real (l + 1) ^ 4 * exp (- 2 * pi * real l * y)" for l
define E where "E = exp (- 2 * pi * y)"
have ab: "a l = E * b l" for l
by (simp add: a_def b_def E_def algebra_simps flip: exp_add)
have sa: "summable a" unfolding a_def by (rule weight_summable[OF y])
have ba: "b l = inverse E * a l" for l using ab[of l] by (simp add: E_def)
have sb: "summable b" unfolding ba by (rule summable_mult[OF sa])
define q where "q = exp (- s)"
have q0: "0 < q" "q < 1" using s0 by (auto simp: q_def)
define g where "g l = 42 * exp s / s ^ 4 * q ^ l" for l
have bg: "b l ≤ g l" for l
proof -
define x where "x = s * real (l + 1)"
have x0: "0 ≤ x" using s0 by (simp add: x_def)
have "Y * real l ≤ y * real l" by (rule mult_right_mono) (use Y0 in auto)
hence "exp (- 2 * pi * real l * y) ≤ exp (- 2 * s * real l)"
by (simp add: s_def algebra_simps)
hence "b l ≤ real (l + 1) ^ 4 * exp (- 2 * s * real l)" by (simp add: b_def mult_left_mono)
also have "real (l + 1) ^ 4 * exp (- 2 * s * real l) =
(x ^ 4 * exp (- x)) * exp s * q ^ l / s ^ 4"
proof -
have ql: "q ^ l = exp (real l * (- s))" unfolding q_def by (rule exp_of_nat_mult[symmetric])
have "exp (- x) * exp s * q ^ l = exp (- x + s + real l * (- s))" unfolding ql
by (simp add: mult_exp_exp algebra_simps)
also have "- x + s + real l * (- s) = - 2 * s * real l" by (simp add: x_def algebra_simps)
finally have e: "exp (- x) * exp s * q ^ l = exp (- 2 * s * real l)" .
have x4: "x ^ 4 = s ^ 4 * real (l + 1) ^ 4" by (simp add: x_def power_mult_distrib)
have "real (l + 1) ^ 4 * exp (- 2 * s * real l) =
real (l + 1) ^ 4 * (exp (- x) * exp s * q ^ l)"
by (simp only: e)
also have "… = (x ^ 4 * exp (- x)) * exp s * q ^ l / s ^ 4" unfolding x4 using s0
by simp
finally show ?thesis .
qed
also have "… ≤ 42 * exp s * q ^ l / s ^ 4"
using pow4_exp_bound[OF x0] s0 q0 by (intro divide_right_mono mult_right_mono) auto
finally show ?thesis by (simp add: g_def)
qed
have G: "g sums (42 * exp s / s ^ 4 * (1 / (1 - q)))"
unfolding g_def by (rule sums_mult) (rule geometric_sums, use q0 in simp)
have "suminf b ≤ suminf g" by (rule suminf_le[OF bg sb sums_summable[OF G]])
also have "suminf g = 42 * exp s / s ^ 4 * (1 / (1 - q))" using G by (simp add: sums_iff)
finally have Sg: "suminf b ≤ 42 * exp s / s ^ 4 * (1 / (1 - q))" .
have inv: "1 / (1 - q) ≤ (1 + s) / s"
proof -
have "1 + s ≤ exp s" by (rule exp_ge_add_one_self)
hence "q ≤ 1 / (1 + s)" using s0 by (simp add: q_def exp_minus field_simps)
hence le: "s / (1 + s) ≤ 1 - q" using s0 by (simp add: field_simps)
have "1 / (1 - q) ≤ 1 / (s / (1 + s))"
by (rule divide_left_mono[OF le]) (use q0 s0 in ‹simp_all add:
zero_less_mult_iff›)
thus ?thesis by simp
qed
have "42 * exp s / s ^ 4 * (1 / (1 - q)) ≤ 42 * exp s / s ^ 4 * ((1 + s) / s)"
using inv s0 by (intro mult_left_mono) auto
with Sg have Sb': "suminf b ≤ 42 * exp s / s ^ 4 * ((1 + s) / s)" by linarith
have s5: "s ^ 5 = s * s ^ 4" by (simp add: eval_nat_numeral)
have Sb: "suminf b ≤ 42 * exp s * (1 + s) / s ^ 5" using Sb' unfolding s5
by (simp add: field_simps)
have W: "weight y = (2 * pi) ^ 4 * y ^ 5 / 12 * E * suminf b"
proof -
have "suminf a = E * suminf b" unfolding ab by (rule suminf_mult[OF sb])
thus ?thesis unfolding weight_def a_def[symmetric] by simp
qed
have C0: "0 ≤ (2 * pi) ^ 4 * y ^ 5 / 12 * E" using y by (simp add: E_def)
have "weight y ≤ (2 * pi) ^ 4 * y ^ 5 / 12 * E * (42 * exp s * (1 + s) / s ^ 5)"
unfolding W by (rule mult_left_mono[OF Sb C0])
also have "… = 56 * pi ^ 4 * (exp s * (1 + s)) * (y / s) ^ 5 * E"
using s0 by (simp add: power_divide power_mult_distrib field_simps)
also have "… ≤ 56 * pi ^ 4 * (exp s * (1 + s)) * ((1 + y) / pi) ^ 5 * E"
proof -
have ys: "y / s ≤ (1 + y) / pi"
proof (cases "y ≤ 1")
case True
hence "s = pi * y" by (simp add: s_def Y_def)
thus ?thesis using y by (simp add: field_simps)
next
case False
hence "s = pi" by (simp add: s_def Y_def)
thus ?thesis by (simp add: divide_right_mono)
qed
have "(y / s) ^ 5 ≤ ((1 + y) / pi) ^ 5" using ys y s0 by (intro power_mono) auto
thus ?thesis using s0 by (intro mult_right_mono mult_left_mono) (auto simp: E_def)
qed
also have "… = (56 * (exp s * (1 + s)) / pi) * (1 + y) ^ 5 * E"
proof -
have p5: "pi ^ 5 = pi * pi ^ 4" by (simp add: eval_nat_numeral)
have h: "pi ^ 4 * ((1 + y) / pi) ^ 5 = (1 + y) ^ 5 / pi" unfolding power_divide p5 by simp
have "56 * pi ^ 4 * (exp s * (1 + s)) * ((1 + y) / pi) ^ 5 * E
= 56 * (exp s * (1 + s)) * (pi ^ 4 * ((1 + y) / pi) ^ 5) * E" by (simp only: mult_ac)
also have "… = 56 * (exp s * (1 + s)) * ((1 + y) ^ 5 / pi) * E" by (simp only: h)
also have "… = (56 * (exp s * (1 + s)) / pi) * (1 + y) ^ 5 * E" by simp
finally show ?thesis .
qed
also have "… ≤ 8192 * (1 + y) ^ 5 * E"
proof -
have "exp s ≤ exp 4" using spi pi_less_4 by simp
also have "exp (4 :: real) = exp 1 ^ 4" using exp_of_nat_mult[of 4 "1 :: real"] by simp
also have "… ≤ 3 ^ 4" using exp_le by (intro power_mono) auto
finally have es: "exp s ≤ 81" by simp
have s5: "1 + s ≤ 5" using spi pi_less_4 by simp
have "exp s * (1 + s) ≤ 81 * 5" using es s5 s0 by (intro mult_mono) auto
hence "56 * (exp s * (1 + s)) / pi ≤ 56 * (81 * 5) / 3"
using pi_gt3 s0 by (intro frac_le) auto
hence "56 * (exp s * (1 + s)) / pi ≤ 8192" by simp
thus ?thesis using y by (intro mult_right_mono) (auto simp: E_def)
qed
finally show "weight y ≤ 8192 * (1 + y) ^ 5 * exp (- 2 * pi * y)" by (simp add: E_def)
qed
theorem DeltaK_zeta5_integral:
assumes "40 dvd K"
shows "real_eval (DeltaK K) zeta5 = 1 / fact (hof K) *
set_lebesgue_integral (PiM {..<hof K} (λ_. lborel)) {y. ∀i<hof K. 0 < y i}
(λy. (∏ i < hof K. ∏ j ∈ {j. i < j ∧
j < hof K}. (y i ^ 2 - y j ^ 2) ^ 2) *
(∏ i < hof K. real_eval (Dm (Nof K)) (y i ^ 2) ^ 6 / real_eval (Dm K) (y i ^ 2) *
weight (y i)))"
proof -
text ‹Instead of the restricted measure on @{text "(0,∞)"} (whose product would
need
@{text "PiM"} of restricted spaces, absent from the library), apply Andreief on @{const lborel}
with the indicator of @{text "(0,∞)"} put into the first family.›
define h where "h = hof K"
define g :: "real ⇒ real" where "g =
(λy. real_eval (Dm (Nof K)) (y ^ 2) ^ 6 / real_eval (Dm K) (y ^ 2) * weight y)"
define φ :: "nat ⇒ real ⇒ real" where "φ =
(λi y. y ^ (2 * i) * indicator {0<..} y)"
define ψ :: "nat ⇒ real ⇒ real" where "ψ =
(λj y. y ^ (2 * j) * g y)"
have gy: "⋀t. real_eval (Dm (Nof K)) (t ^ 2) ^ 6 / real_eval (Dm K) (t ^ 2) * weight t = g t"
by (simp add: g_def)
have S0: "(0::nat) ∉ {1..K}"
by simp
have DK: "sqPoleProd {1..K} = Dm K"
by (simp add: Dm_def sqPoleProd_def)
have pt: "⋀m y. real_eval (Dm (Nof K) ^ 6 * pX ^ m) (y ^ 2) / real_eval (Dm K) (y ^ 2) *
weight y = (y ^ 2) ^ m * g y"
unfolding g_def real_eval_mult real_eval_power real_eval_pX
by (simp add: mult_ac)
have php: "⋀i j y. φ i y * ψ j y =
indicator {0<..} y *⇩R ((y ^ 2) ^ (i + j) * g y)"
unfolding φ_def ψ_def power_add power_mult
by (simp add: mult_ac)
have entry: "⋀i j. i < h ⟹ j < h ⟹
real_eval (GK K $$ (i, j)) zeta5 = integral⇧L lborel (λy. φ i y *
ψ j y)"
proof -
fix i j assume ij: "i < h" "j < h"
have e1: "GK K $$ (i, j) = muX {1..K} (Dm (Nof K) ^ 6 * pX ^ (i + j))"
using ij by (simp add: GK_def h_def)
show "real_eval (GK K $$ (i, j)) zeta5 =
integral⇧L lborel (λy. φ i y * ψ j y)"
unfolding e1 muX_zeta5_integral[OF finite_atLeastAtMost S0] DK pt php
set_lebesgue_integral_def
by simp
qed
have detG: "real_eval (DeltaK K) zeta5 =
Determinant.det (Matrix.mat h h (λ(i,
j). integral⇧L lborel (λy. φ i y * ψ j y)))"
proof -
have d1: "real_eval (DeltaK K) zeta5 =
Determinant.det (map_mat (λP. real_eval P zeta5) (GK K))"
unfolding DeltaK_def by (rule comm_ring_hom.hom_det[OF real_eval_hom, symmetric])
have d2: "map_mat (λP. real_eval P zeta5) (GK K) =
Matrix.mat h h (λ(i, j). integral⇧L lborel (λy. φ i y *
ψ j y))"
proof (rule eq_matI)
fix i j assume i: "i < dim_row (Matrix.mat h h (λ(i,
j). integral⇧L lborel (λy. φ i y * ψ j y)))"
and j: "j < dim_col (Matrix.mat h h (λ(i,
j). integral⇧L lborel (λy. φ i y * ψ j y)))"
show "map_mat (λP. real_eval P zeta5) (GK K) $$ (i, j) =
Matrix.mat h h (λ(i, j). integral⇧L lborel (λy. φ i y *
ψ j y)) $$ (i, j)"
using i j entry by (simp add: GK_def h_def)
next
show "dim_row (map_mat (λP. real_eval P zeta5) (GK K)) =
dim_row (Matrix.mat h h (λ(i,
j). integral⇧L lborel (λy. φ i y * ψ j y)))"
by (simp add: GK_def h_def)
next
show "dim_col (map_mat (λP. real_eval P zeta5) (GK K)) =
dim_col (Matrix.mat h h (λ(i,
j). integral⇧L lborel (λy. φ i y * ψ j y)))"
by (simp add: GK_def h_def)
qed
show ?thesis
unfolding d1 d2
by simp
qed
have integ: "⋀i j. i < h ⟹ j < h ⟹
integrable lborel (λy. φ i y * ψ j y)"
proof -
fix i j assume ij: "i < h" "j < h"
have r: "set_integrable lborel {0<..} (λy. real_eval (Dm (Nof K) ^ 6 * pX ^ (i +
j)) (y ^ 2) / real_eval (sqPoleProd {1..K}) (y ^ 2) * weight y)"
by (rule rat_integrable[OF finite_atLeastAtMost S0])
show "integrable lborel (λy. φ i y * ψ j y)"
using r[unfolded set_integrable_def DK pt]
by (simp add: php)
qed
have A: "Determinant.det (Matrix.mat h h (λ(i,
j). integral⇧L lborel (λy. φ i y * ψ j y)))
= 1 / fact h * integral⇧L (PiM {..<h} (λ_. lborel))
(λx. Determinant.det (Matrix.mat h h (λ(a,
b). φ a (x b))) * Determinant.det (Matrix.mat h h (λ(a,
b). ψ a (x b))))"
by (rule andreief[OF sigma_finite_lborel integ])
have V: "⋀y :: nat ⇒ real. Determinant.det (Matrix.mat h h (λ(a,
b). y b ^ (2 * a))) = (∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y j ^ 2 - y i ^ 2))"
proof -
fix y :: "nat ⇒ real"
have "Determinant.det (Matrix.mat h h (λ(a, b). y b ^ (2 * a))) =
Determinant.det (Matrix.mat h h (λ(a, b). (y a ^ 2) ^ b))"
using andreief_det_swap[of h "λa b. (y a ^ 2) ^ b"] by (simp add: power_mult)
also have "… = (∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y j ^ 2 - y i ^ 2))"
using det_vandermonde_jnf[of h "λa. y a ^ 2"] by simp
finally show "Determinant.det (Matrix.mat h h (λ(a, b). y b ^ (2 * a))) = (∏ i <
h. ∏ j ∈ {j. i < j ∧ j < h}. (y j ^ 2 - y i ^ 2))" .
qed
have Wphi: "⋀y. Determinant.det (Matrix.mat h h (λ(a, b). φ a (y b))) =
(∏ b < h. indicator {0<..} (y b)) * Determinant.det (Matrix.mat h h (λ(a,
b). y b ^ (2 * a)))"
unfolding φ_def
by (simp add: andreief_det_scale_cols)
have Wpsi: "⋀y. Determinant.det (Matrix.mat h h (λ(a, b). ψ a (y b))) =
(∏ b < h. g (y b)) * Determinant.det (Matrix.mat h h (λ(a, b). y b ^ (2 * a)))"
unfolding ψ_def
by (simp add: andreief_det_scale_cols)
have ind: "⋀y :: nat ⇒ real. (∏ b < h. indicator {0<..} (y b) :: real) =
indicator {y. ∀i<h. 0 < y i} y"
proof -
fix y :: "nat ⇒ real"
show "(∏ b < h. indicator {0<..} (y b) :: real) = indicator {y. ∀i<h. 0 < y i} y"
proof (cases "∀i<h. 0 < y i")
case True
then show ?thesis
by (simp add: indicator_def)
next
case False
then show ?thesis
by (auto simp: indicator_def prod_zero_iff)
qed
qed
have sq: "⋀a b :: real. (b - a) * (b - a) = (a - b) ^ 2"
by (simp add: power2_eq_square algebra_simps)
have Vsq: "⋀y :: nat ⇒ real. (∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y j ^ 2 - y i ^ 2)) * (∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y j ^ 2 - y i ^ 2))
= (∏ i < h. ∏ j ∈ {j. i < j ∧ j < h}. (y i ^ 2 - y j ^ 2) ^ 2)"
unfolding prod.distrib[symmetric] sq
by simp
have pw: "⋀y. Determinant.det (Matrix.mat h h (λ(a,
b). φ a (y b))) * Determinant.det (Matrix.mat h h (λ(a, b). ψ a (y b)))
= indicator {y. ∀i<h. 0 < y i} y *⇩R ((∏ i < h. ∏ j ∈ {j. i <
j ∧ j < h}. (y i ^ 2 - y j ^ 2) ^ 2) * (∏ i < h. g (y i)))"
unfolding Wphi Wpsi ind V Vsq[symmetric]
by (simp add: mult_ac)
have fin: "integral⇧L (PiM {..<h} (λ_. lborel)) (λx. Determinant.det
(Matrix.mat h h (λ(a, b). φ a (x b))) *
Determinant.det (Matrix.mat h h (λ(a, b). ψ a (x b))))
= set_lebesgue_integral (PiM {..<h} (λ_. lborel)) {y. ∀i<h. 0 <
y i} (λy. (∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y i ^ 2 - y j ^ 2) ^ 2) * (∏ i < h. g (y i)))"
unfolding set_lebesgue_integral_def pw
by simp
show ?thesis
unfolding h_def[symmetric] gy detG A fin
by simp
qed
subsection ‹(6.12) and the one-coordinate bound›
text ‹(6.12): @{text "0 ≤ ∑_{j≤m} log(t + (j/K)^2) -
K ∫_0^{m/K} log(t + u^2) du ≤ 2 log m + 2"}.›
lemma sum_ge_int:
"0 < t ⟹ 0 < κ ⟹
κ * integral {0..real m / κ} (λu. ln (t + u ^ 2)) ≤ (∑ j =
1..m. ln (t + (real j / κ) ^ 2))"
proof (induction m)
case 0
thus ?case by simp
next
case (Suc m)
define f where "f u = ln (t + u ^ 2)" for u :: real
have fe: "(λu. ln (t + u ^ 2)) = f" by (simp add: f_def fun_eq_iff)
have t: "0 < t" and k: "0 < κ" using Suc.prems by auto
have tp: "0 < t + u ^ 2" for u :: real using t by (simp add: add_pos_nonneg)
have cont: "continuous_on {a..b} f" for a b
unfolding f_def by (intro continuous_intros) (use tp in ‹auto simp: less_le›)
have intg: "f integrable_on {a..b}" for a b by (rule integrable_continuous_interval[OF cont])
define a where "a = real m / κ"
define b where "b = real (Suc m) / κ"
have ab: "0 ≤ a" "a ≤ b" using k by (auto simp: a_def b_def divide_right_mono)
have comb: "integral {0..a} f + integral {a..b} f = integral {0..b} f"
by (rule Henstock_Kurzweil_Integration.integral_combine[OF ab intg])
have "integral {a..b} f ≤ integral {a..b} (λ_. f b)"
proof (rule integral_le[OF intg])
show "(λ_. f b) integrable_on {a..b}"
by (rule integrable_continuous_interval) (rule continuous_on_const)
fix u assume "u ∈ {a..b}"
hence "0 ≤ u" "u ≤ b" using ab by auto
hence "u ^ 2 ≤ b ^ 2" by (intro power_mono) auto
thus "f u ≤ f b" unfolding f_def using tp by (subst ln_le_cancel_iff) auto
qed
also have "… = (b - a) * f b" using ab by simp
also have "b - a = 1 / κ" using k by (simp add: a_def b_def field_simps)
finally have le': "κ * integral {a..b} f ≤ f b" using k by (simp add: field_simps)
have IH: "κ * integral {0..a} f ≤ (∑ j = 1..m. ln (t + (real j / κ) ^ 2))"
using Suc.IH[OF t k] unfolding fe a_def .
have "κ * integral {0..b} f = κ * integral {0..a} f + κ * integral {a..b} f"
by (simp add: comb[symmetric] distrib_left)
also have "… ≤ (∑ j = 1..m. ln (t + (real j / κ) ^ 2)) + f b"
using IH le' by linarith
also have "… = (∑ j = 1..Suc m. ln (t + (real j / κ) ^ 2))"
by (simp add: b_def f_def)
finally show ?case unfolding fe b_def .
qed
lemma sum_log_le: "1 ≤ m ⟹
(∑ k = 1..m. ln (real k)) ≤ real m * ln (real m) - real m + ln (real m) + 1"
proof -
assume "1 ≤ m"
thus ?thesis
proof (induction m rule: nat_induct_at_least)
case base
show ?case
by simp
next
case (Suc m)
define A :: real where "A = ln (real m)"
define B :: real where "B = ln (real (Suc m))"
have m1: "1 ≤ real m" using Suc.hyps
by simp
have IH: "(∑ k = 1..m. ln (real k)) ≤ real m * A - real m + A + 1" using Suc.IH
unfolding A_def .
have "ln (real m / real (Suc m)) ≤ real m / real (Suc m) - 1"
using m1 ln_le_minus_one[of "real m / real (Suc m)"]
by simp
moreover have "ln (real m / real (Suc m)) = A - B" using m1 unfolding A_def B_def
by (simp add: ln_div)
moreover have "real m / real (Suc m) - 1 = - 1 / real (Suc m)" using m1
by (simp add: field_simps)
ultimately have d4a: "A - B ≤ - 1 / real (Suc m)"
by simp
have d4: "real (Suc m) * (A - B) ≤ - 1" using mult_left_mono[OF d4a, of "real (Suc m)"] m1
by simp
have f: "(∑ k = 1..Suc m. ln (real k)) = B + (∑ k = 1..m. ln (real k))"
unfolding B_def
by simp
have e: "real (Suc m) * (A - B) = real m * A + A - real (Suc m) * B"
by (simp add: algebra_simps)
have s: "real (Suc m) = real m + 1"
by simp
have "(∑ k = 1..Suc m. ln (real k)) ≤ real (Suc m) * B - real (Suc m) + B + 1"
using e f d4 IH s
by simp
thus ?case unfolding B_def .
qed
qed
lemma ln_int0: "0 < (c :: real) ⟹ ln integrable_on {0..c}"
using set_borel_integral_eq_integral(1)[OF ln_integrable_near_zero] integrable_on_Icc_iff_Ioo
by auto
lemma integral_ln_0: "0 < (b :: real) ⟹
integral {0..b} (λu. ln u) = b * ln b - b"
proof -
assume b: "0 < b"
have "integral {0..b} (λu. ln u) =
integral {0..b} (λu. (1 / 2) *⇩R ln (0 + u ^ 2))"
by (simp add: ln_realpow)
also have "… = (1 / 2) * (2 * (b * ln b - b))" using Ic_zero[OF b]
by simp
also have "… = b * ln b - b"
by simp
finally show ?thesis .
qed
text ‹Telescoping a sum of integrals over the cells
@{text "[(j-1)/κ, j/κ]"}.›
lemma tele_gen:
fixes g :: "real ⇒ real" and κ :: real
assumes k: "0 < κ" and gi: "⋀c. 0 < c ⟹ g integrable_on {0..c}"
shows "(∑ j = 1..n. integral {real (j - 1) / κ..real j / κ} g) =
integral {0..real n / κ} g"
proof (induction n)
case 0
show ?case
by simp
next
case (Suc n)
have a: "0 ≤ real n / κ" using k
by simp
have b: "real n / κ ≤ real (Suc n) / κ" using k
by (simp add: divide_right_mono)
have i: "g integrable_on {0..real (Suc n) / κ}" using gi k
by simp
have c: "integral {0..real n / κ} g + integral {real n / κ..real (Suc n) /
κ} g = integral {0..real (Suc n) / κ} g"
using Henstock_Kurzweil_Integration.integral_combine[OF a b i] .
show ?case using Suc.IH c
by simp
qed
text ‹(6.12): @{text "∑_{j≤m} log(t + (j/κ)^2) -
κ ∫_0^{m/κ} log(t + u^2) du ≤
2 log m + 2"}: on each cell @{text "[(j-1)/κ, j/κ]"},
@{text "log(t + b^2) - log(t + u^2) ≤ 2 log b - 2 log u"}.›
lemma sum_le_int:
"0 < t ⟹ 0 < κ ⟹ 1 ≤ m ⟹
(∑ j = 1..m. ln (t + (real j / κ) ^ 2)) ≤
κ * integral {0..real m / κ} (λu. ln (t + u ^ 2)) + 2 * ln (real m) +
2"
proof -
assume t: "0 < t" and k: "0 < κ" and m: "1 ≤ m"
have cell: "⋀j. 1 ≤ j ⟹
ln (t + (real j / κ) ^ 2) / κ - integral {real (j - 1) / κ..real j /
κ} (λu. ln (t + u ^ 2))
≤ integral {real (j - 1) / κ..real j / κ} (λu. 2 *
ln (real j / κ) - 2 * ln u)"
proof -
fix j :: nat assume j: "1 ≤ j"
define a where "a = real (j - 1) / κ"
define b where "b = real j / κ"
have a0: "0 ≤ a" unfolding a_def using k
by simp
have b0: "0 < b" unfolding b_def using k j
by simp
have ab: "a ≤ b" unfolding a_def b_def using k j
by (simp add: divide_right_mono)
have ba: "b - a = 1 / κ" unfolding a_def b_def using j
by (simp add: of_nat_diff diff_divide_distrib)
have tp: "0 < t + u ^ 2" for u :: real using t
by (simp add: add_pos_nonneg)
have "t + u ^ 2 ≠ 0" for u :: real using tp[of u]
by simp
hence c1: "continuous_on {a..b} (λu. ln (t + u ^ 2))"
by (fast intro: continuous_intros)
have i1: "(λu. ln (t + u ^ 2)) integrable_on {a..b}"
using integrable_continuous_interval[OF c1]
by simp
have i2: "(λu. 2 * ln b - 2 * ln u) integrable_on {a..b}"
proof -
have l: "ln integrable_on {a..b}"
using integrable_on_subinterval[OF ln_int0[OF b0], of a b] a0
by simp
show ?thesis using l
by (auto intro: Henstock_Kurzweil_Integration.integrable_diff integrable_const_ivl
integrable_on_cmult_left)
qed
have i3: "(λu. ln (t + b ^ 2) - ln (t + u ^ 2)) integrable_on {a..b}" using i1
by (auto intro: Henstock_Kurzweil_Integration.integrable_diff integrable_const_ivl)
have pw: "ln (t + b ^ 2) - ln (t + u ^ 2) ≤ 2 * ln b - 2 * ln u" if u: "0 < u" "u ≤ b"
for u
proof -
have m: "(t + b ^ 2) * u ^ 2 ≤ b ^ 2 * (t + u ^ 2)"
proof -
have "u ^ 2 ≤ b ^ 2" using u
by (simp add: power_mono)
hence "t * u ^ 2 ≤ t * b ^ 2" using t
by (simp add: mult_left_mono)
thus ?thesis
by (simp add: algebra_simps)
qed
have l: "ln ((t + b ^ 2) * u ^ 2) ≤ ln (b ^ 2 * (t + u ^ 2))"
using m u tp[of u] tp[of b] b0
by simp
have l1: "ln ((t + b ^ 2) * u ^ 2) = ln (t + b ^ 2) + 2 * ln u" using u tp[of b]
by (simp add: ln_mult ln_realpow)
have l2: "ln (b ^ 2 * (t + u ^ 2)) = 2 * ln b + ln (t + u ^ 2)" using b0 tp[of u]
by (simp add: ln_mult ln_realpow)
show ?thesis using l l1 l2
by simp
qed
have le: "integral {a<..<b} (λu. ln (t + b ^ 2) - ln (t + u ^ 2)) ≤
integral {a<..<b} (λu. 2 * ln b - 2 * ln u)"
proof (rule integral_le)
show "(λu. ln (t + b ^ 2) - ln (t + u ^ 2)) integrable_on {a<..<b}" using i3
by (simp add: integrable_on_Icc_iff_Ioo["symmetric"])
show "(λu. 2 * ln b - 2 * ln u) integrable_on {a<..<b}" using i2
by (simp add: integrable_on_Icc_iff_Ioo["symmetric"])
fix u assume "u ∈ {a<..<b}"
thus "ln (t + b ^ 2) - ln (t + u ^ 2) ≤ 2 * ln b - 2 * ln u" using pw a0
by simp
qed
have eqL: "ln (t + b ^ 2) / κ - integral {a..b} (λu. ln (t + u ^ 2)) =
integral {a<..<b} (λu. ln (t + b ^ 2) - ln (t + u ^ 2))"
proof -
have "integral {a..b} (λu. ln (t + b ^ 2) - ln (t + u ^ 2)) =
integral {a..b} (λu. ln (t + b ^ 2)) - integral {a..b} (λu. ln (t + u ^ 2))"
using i1
using Henstock_Kurzweil_Integration.integral_diff by blast
moreover have "integral {a..b} (λu. ln (t + b ^ 2)) = ln (t + b ^ 2) / κ"
using ab ba
by (simp add: content_real)
moreover have "integral {a..b} (λu. ln (t + b ^ 2) - ln (t + u ^ 2)) =
integral {a<..<b} (λu. ln (t + b ^ 2) - ln (t + u ^ 2))"
by (simp add: integral_open_interval_real)
ultimately show ?thesis
by simp
qed
have eqR: "integral {a..b} (λu. 2 * ln b - 2 * ln u) =
integral {a<..<b} (λu. 2 * ln b - 2 * ln u)"
by (simp add: integral_open_interval_real)
show "ln (t + (real j / κ) ^ 2) / κ - integral {real (j - 1) / κ..real j /
κ} (λu. ln (t + u ^ 2))
≤ integral {real (j - 1) / κ..real j / κ} (λu. 2 *
ln (real j / κ) - 2 * ln u)"
using le eqL eqR unfolding a_def b_def
by simp
qed
have fi: "(λu. ln (t + u ^ 2)) integrable_on {0..c}" for c
proof -
have "t + u ^ 2 ≠ 0" for u :: real using add_pos_nonneg[OF t zero_le_power2[of u]]
by simp
hence "continuous_on {0..c} (λu. ln (t + u ^ 2))"
by (fast intro: continuous_intros)
thus ?thesis
by (auto intro: integrable_continuous_interval)
qed
have tele: "(∑ j = 1..m. integral {real (j - 1) / κ..real j /
κ} (λu. ln (t + u ^ 2))) =
integral {0..real m / κ} (λu. ln (t + u ^ 2))"
using tele_gen[OF k fi]
by simp
have rhs: "(∑ j = 1..m. integral {real (j - 1) / κ..real j /
κ} (λu. 2 * ln (real j / κ) - 2 * ln u))
= (2 / κ) * (∑ j =
1..m. ln (real j)) - 2 * (real m / κ) * ln (real m) + 2 * real m / κ"
proof -
have li: "ln integrable_on {0..c}" if "0 < c" for c :: real using ln_int0[OF that] .
have cellR: "integral {real (j - 1) / κ..real j / κ} (λu. 2 * ln (real j /
κ) - 2 * ln u) = 2 * ln (real j / κ) / κ - 2 * integral {real (j - 1) /
κ..real j / κ} ln" if j: "1 ≤ j" for j
proof -
have jb: "0 < real j / κ" using j k
by simp
have lc: "ln integrable_on {real (j - 1) / κ..real j / κ}"
using integrable_on_subinterval[OF li[OF jb],
of "real (j - 1) / κ" "real j / κ"] k
by (simp add: divide_right_mono)
have l2: "(λu. 2 * ln u) integrable_on {real (j - 1) / κ..real j / κ}"
using lc
by (auto intro: integrable_on_cmult_left)
have d: "integral {real (j - 1) / κ..real j / κ} (λu. 2 * ln (real j /
κ) - 2 * ln u) = integral {real (j - 1) / κ..real j /
κ} (λu. 2 * ln (real j / κ)) - integral {real (j - 1) /
κ..real j / κ} (λu. 2 * ln u)"
using l2 Henstock_Kurzweil_Integration.integral_diff[OF integrable_const_ivl l2]
by simp
have c: "integral {real (j - 1) / κ..real j / κ} (λu. 2 * ln (real j /
κ)) = 2 * ln (real j / κ) / κ" using j k
by (simp add: content_real of_nat_diff diff_divide_distrib)
have e: "integral {real (j - 1) / κ..real j / κ} (λu. 2 * ln u) =
2 * integral {real (j - 1) / κ..real j / κ} ln"
using integral_mult[OF lc, of 2]
by simp
show ?thesis unfolding d c e ..
qed
have s1: "(∑ j = 1..m. integral {real (j - 1) / κ..real j /
κ} (λu. 2 * ln (real j / κ) - 2 * ln u)) = (∑ j =
1..m. 2 * ln (real j / κ) / κ) - 2 * (∑ j =
1..m. integral {real (j - 1) / κ..real j / κ} ln)"
using cellR
by (simp add: sum_subtractf sum_distrib_left)
have lnd: "ln (real j / κ) = ln (real j) - ln κ" if "1 ≤ j" for j using that k
by (simp add: ln_div)
have s2: "(∑ j = 1..m. 2 * ln (real j / κ) / κ) =
(2 / κ) * (∑ j = 1..m. ln (real j)) - 2 * real m / κ * ln κ"
proof -
have "(∑ j = 1..m. 2 * ln (real j / κ) / κ) = (∑ j =
1..m. (2 / κ) * ln (real j) - (2 / κ) * ln κ)"
proof (rule sum.cong)
fix j assume "j ∈ {1..m}"
hence j1: "1 ≤ j"
by simp
show "2 * ln (real j / κ) / κ =
(2 / κ) * ln (real j) - (2 / κ) * ln κ" using lnd[OF j1]
by (simp add: diff_divide_distrib right_diff_distrib)
next
show "{1..m} = {1..m}"
by simp
qed
also have "… = (2 / κ) * (∑ j =
1..m. ln (real j)) - 2 * real m / κ * ln κ"
by (simp add: sum_subtractf sum_distrib_left)
finally show ?thesis .
qed
have sumL: "(∑ j = 1..m. integral {real (j - 1) / κ..real j / κ} ln) =
integral {0..real m / κ} ln" using tele_gen[OF k li] .
have mk: "0 < real m / κ" using m k
by simp
have lnI: "integral {0..real m / κ} ln =
real m / κ * ln (real m / κ) - real m / κ" using integral_ln_0[OF mk] .
have lnm: "ln (real m / κ) = ln (real m) - ln κ" using m k
by (simp add: ln_div)
show ?thesis unfolding s1 s2 sumL lnI lnm
by (simp add: algebra_simps)
qed
have "(∑ j = 1..m. ln (t + (real j / κ) ^ 2)) / κ - integral {0..real m /
κ} (λu. ln (t + u ^ 2))
≤ (2 / κ) * (∑ j =
1..m. ln (real j)) - 2 * (real m / κ) * ln (real m) + 2 * real m / κ"
unfolding tele[symmetric] rhs[symmetric] sum_divide_distrib sum_subtractf[symmetric]
by (rule sum_mono) (use cell in simp)
also have "… ≤ (2 / κ) * (ln (real m) + 1)"
using sum_log_le[OF m] k by (simp add: field_simps)
finally have F: "(∑ j = 1..m. ln (t + (real j / κ) ^ 2)) / κ -
integral {0..real m / κ} (λu. ln (t + u ^ 2)) ≤
(2 / κ) * (ln (real m) + 1)" .
have "κ * ((∑ j = 1..m. ln (t + (real j / κ) ^ 2)) / κ -
integral {0..real m / κ} (λu. ln (t + u ^ 2))) ≤
κ * ((2 / κ) * (ln (real m) + 1))"
using mult_left_mono[OF F less_imp_le[OF k]] by simp
moreover have "κ * ((∑ j =
1..m. ln (t + (real j / κ) ^ 2)) / κ - integral {0..real m /
κ} (λu. ln (t + u ^ 2))) = (∑ j =
1..m. ln (t + (real j / κ) ^ 2)) - κ * integral {0..real m /
κ} (λu. ln (t + u ^ 2))"
using k by (simp add: algebra_simps)
moreover have "κ * ((2 / κ) * (ln (real m) + 1)) = 2 * ln (real m) + 2"
using k by (simp add: algebra_simps)
ultimately show ?thesis by simp
qed
text ‹The one-coordinate bound: (6.11) and (6.12) give
@{text "D_N(y^2)^6/D_K(y^2) w(y) ≤
8192 e^1^2 K^{12N+12}/K^{2K} (1+y)^5 e^{-K V((y/K)^2)}"}.›
lemma g_le:
assumes "1 ≤ N" "N ≤ K" "real N / real K = 3 / 40" "0 < y"
shows "real_eval (Dm N) (y ^ 2) ^ 6 / real_eval (Dm K) (y ^ 2) * weight y ≤
8192 * exp 12 * real K ^ (12 * N + 12) / real K ^ (2 * K) *
((1 + y) ^ 5 * exp (- real K * Vf ((y / real K) ^ 2)))"
proof -
define t where "t = (y / real K) ^ 2"
define κ where "κ = real K"
have K0: "0 < κ" using assms unfolding κ_def by simp
have t0: "0 < t" using assms unfolding t_def by simp
have Dm_exp: "⋀m. real_eval (Dm m) (y ^ 2) = κ ^ (2 * m) * exp (∑ j =
1..m. ln (t + (real j / κ) ^ 2))"
proof -
fix m
have f: "real_eval (Dm m) (y ^ 2) = (∏ j = 1..m. y ^ 2 + real j ^ 2)"
unfolding Dm_def real_eval_prod
by (simp add: real_eval_simps of_rat_power)
have each: "y ^ 2 + real j ^ 2 = κ ^ 2 * exp (ln (t + (real j / κ) ^ 2))" for j
proof -
have p: "0 < t + (real j / κ) ^ 2" using t0
by (simp add: add_pos_nonneg)
have "y ^ 2 + real j ^ 2 = κ ^ 2 * (t + (real j / κ) ^ 2)"
unfolding t_def κ_def using K0 unfolding κ_def
by (simp add: power_divide field_simps)
thus ?thesis using p
by simp
qed
have "(∏ j = 1..m. y ^ 2 + real j ^ 2) = (∏ j =
1..m. κ ^ 2 * exp (ln (t + (real j / κ) ^ 2)))" unfolding each ..
also have "… = (κ ^ 2) ^ m * exp (∑ j =
1..m. ln (t + (real j / κ) ^ 2))"
by (simp add: prod.distrib exp_sum)
also have "… = κ ^ (2 * m) * exp (∑ j =
1..m. ln (t + (real j / κ) ^ 2))"
by (simp add: power_mult)
finally show "real_eval (Dm m) (y ^ 2) = κ ^ (2 * m) * exp (∑ j =
1..m. ln (t + (real j / κ) ^ 2))" unfolding f .
qed
have lower: "κ * integral {0..real K / κ} (λu. ln (t + u ^ 2)) ≤
(∑ j = 1..K. ln (t + (real j / κ) ^ 2))"
by (rule sum_ge_int[OF t0 K0])
have upper: "(∑ j = 1..N. ln (t + (real j / κ) ^ 2)) ≤
κ * integral {0..real N / κ} (λu. ln (t + u ^ 2)) + 2 * ln (real N) + 2"
by (rule sum_le_int[OF t0 K0 assms(1)])
have V: "κ * Vf t = 2 * pi * y + κ * integral {0..1} (λu. ln (t + u ^ 2)) -
6 * κ * integral {0..3 / 40} (λu. ln (t + u ^ 2))"
unfolding Vf_def t_def κ_def
using real_sqrt_abs[of "y / real K"] assms(4) K0[unfolded κ_def]
by (simp add: algebra_simps)
have ends: "real K / κ = 1" "real N / κ = 3 / 40" using assms(3) K0
unfolding κ_def by simp_all
have w: "weight y ≤ 8192 * (1 + y) ^ 5 * exp (- 2 * pi * y)" by (rule weight_le[OF assms(4)])
have "real_eval (Dm N) (y ^ 2) ^ 6 / real_eval (Dm K) (y ^ 2) * weight y
≤ κ ^ (12 * N) / κ ^ (2 * K) * exp (6 * (κ * integral {0..3 /
40} (λu. ln (t + u ^ 2)) + 2 * ln (real N) + 2) - κ *
integral {0..1} (λu. ln (t + u ^ 2))) * (8192 * (1 + y) ^ 5 * exp (- 2 * pi *
y))"
proof -
have q: "real_eval (Dm N) (y ^ 2) ^ 6 / real_eval (Dm K) (y ^ 2) =
κ ^ (12 * N) / κ ^ (2 * K) * exp (6 * (∑ j =
1..N. ln (t + (real j / κ) ^ 2)) - (∑ j =
1..K. ln (t + (real j / κ) ^ 2)))"
unfolding Dm_exp using exp_of_nat_mult[of 6 "∑ j =
1..N. ln (t + (real j / κ) ^ 2)"]
by (simp add: power_mult_distrib exp_diff power_mult["symmetric"])
have ex: "exp (6 * (∑ j = 1..N. ln (t + (real j / κ) ^ 2)) - (∑ j =
1..K. ln (t + (real j / κ) ^ 2))) ≤
exp (6 * (κ * integral {0..3 / 40} (λu. ln (t + u ^ 2)) + 2 * ln (real N) +
2) - κ * integral {0..1} (λu. ln (t + u ^ 2)))"
using upper lower unfolding ends
by simp
have w0: "0 < weight y" by (rule weight_pos[OF assms(4)])
have c0: "0 ≤ κ ^ (12 * N) / κ ^ (2 * K)" using K0
by simp
have "real_eval (Dm N) (y ^ 2) ^ 6 / real_eval (Dm K) (y ^ 2) * weight y =
κ ^ (12 * N) / κ ^ (2 * K) * exp (6 * (∑ j =
1..N. ln (t + (real j / κ) ^ 2)) - (∑ j =
1..K. ln (t + (real j / κ) ^ 2))) * weight y"
unfolding q ..
also have "… ≤ κ ^ (12 * N) / κ ^ (2 * K) * exp (6 * (κ *
integral {0..3 / 40} (λu. ln (t + u ^ 2)) + 2 * ln (real N) + 2) - κ *
integral {0..1} (λu. ln (t + u ^ 2))) * (8192 * (1 + y) ^ 5 * exp (- 2 * pi * y))"
using mult_mono[OF mult_left_mono[OF ex c0] w] less_imp_le[OF w0] mult_nonneg_nonneg[OF c0
exp_ge_zero]
by simp
finally show ?thesis .
qed
also have "… ≤ 8192 * exp 12 * real K ^ (12 * N + 12) / real K ^ (2 * K) * ((1 +
y) ^ 5 * exp (- real K * Vf ((y / real K) ^ 2)))"
proof -
have V': "6 * (κ * integral {0..3 / 40} (λu. ln (t + u ^ 2)) + 2 * ln (real N) +
2) - κ * integral {0..1} (λu. ln (t + u ^ 2)) + (- 2 * pi * y) =
12 * ln (real N) + 12 + (- κ * Vf t)"
using V
by simp
have N0: "0 < real N" using assms(1)
by simp
have e1: "exp (6 * (κ * integral {0..3 / 40} (λu. ln (t + u ^ 2)) + 2 *
ln (real N) + 2) - κ * integral {0..1} (λu. ln (t + u ^ 2))) * exp (- 2 * pi *
y) = real N ^ 12 * exp 12 * exp (- κ * Vf t)"
proof -
have "exp (6 * (κ * integral {0..3 / 40} (λu. ln (t + u ^ 2)) + 2 *
ln (real N) + 2) - κ * integral {0..1} (λu. ln (t + u ^ 2))) * exp (- 2 *
pi * y) = exp (12 * ln (real N)) * exp 12 * exp (- κ * Vf t)"
unfolding mult_exp_exp V'
by (simp add: exp_add)
also have "exp (12 * ln (real N)) = real N ^ 12"
using N0 exp_ln[of "real N ^ 12"] ln_realpow[of "real N" 12]
by simp
finally show ?thesis .
qed
have N12: "real N ^ 12 ≤ real K ^ 12" using assms(2)
by (simp add: power_mono)
have "κ ^ (12 * N) / κ ^ (2 * K) * exp (6 * (κ * integral {0..3 /
40} (λu. ln (t + u ^ 2)) + 2 * ln (real N) + 2) - κ *
integral {0..1} (λu. ln (t + u ^ 2))) * (8192 * (1 + y) ^ 5 * exp (- 2 * pi * y))
= 8192 * exp 12 * κ ^ (12 * N) * real N ^ 12 / κ ^ (2 * K) * ((1 + y) ^ 5 *
exp (- κ * Vf t))"
using e1
by (simp add: algebra_simps)
also have "… ≤ 8192 * exp 12 * κ ^ (12 * N) * real K ^ 12 / κ ^ (2 *
K) * ((1 + y) ^ 5 * exp (- κ * Vf t))"
using N12 K0 assms(4)
by (simp add: mult_left_mono mult_right_mono divide_right_mono)
also have "… = 8192 * exp 12 * real K ^ (12 * N + 12) / real K ^ (2 * K) * ((1 + y) ^ 5 *
exp (- real K * Vf ((y / real K) ^ 2)))"
unfolding κ_def t_def
by (simp add: power_add)
finally show ?thesis .
qed
finally show ?thesis .
qed
subsection ‹(6.9) The bound for every configuration›
text ‹(6.9): for every configuration @{text "0 ≤ t_1, …, t_h"} of distinct points,
@{text "2∑_{i<j} log|t_i - t_j| - K∑V(t_i) + ∑√t_i ≤
(λM_0 - I(ρ))K^2 + (120 + √2)h + 2h log K"}.
Proof: regularise by circle measures of radius @{text "ε = 1/(4K^2)"}, apply Lemma 6.2 to
@{text "σ = K^-^1∑ω_i"} and @{text ρ},
the circle average of @{text "log|z-a|"}, the arcsine mass bound
@{text "ρ([x-r, x+r]) ≤ 40√r"}, and (6.7) (Lean: @{text Config69}).›
lemma rho_singleton: "emeasure rho {a} = 0"
using rho_Icc_le[of 0 a] by simp
text ‹The cross bound: @{text "∫ ln⇧+(ε/|x - u|) dρ(u) ≤
80 sqrt ε"}, by the layer cake over @{text "rho_Icc_le"}.›
lemma cross_bound:
fixes x e :: real
assumes e: "0 < e"
shows "(∫⇧+ u. ennreal (max 0 (ln (e / ¦x - u¦))) ∂rho) ≤
ennreal (80 * sqrt e)"
proof -
have cake: "⋀a :: real. 0 ≤ a ⟹
ennreal a = (∫⇧+ s. indicator {0..<a} s ∂lborel)"
by (simp add: emeasure_lborel_Ico)
have level: "⋀s u. 0 ≤ s ⟹ u ≠ x ⟹
(s < ln (e / ¦x - u¦)) ⟷ ¦x - u¦ < e * exp (- s)"
proof -
fix s u :: real
assume s0: "0 ≤ s" and ux: "u ≠ x"
have d0: "0 < ¦x - u¦" using ux by simp
have l1: "(s < ln (e / ¦x - u¦)) ⟷ exp s < e / ¦x - u¦"
using d0 e ln_less_cancel_iff[of "exp s" "e / ¦x - u¦"] by simp
have l2a: "e * exp (- s) = e / exp s" by (simp add: exp_minus divide_inverse)
have l2: "exp s < e / ¦x - u¦ ⟷
¦x - u¦ < e * exp (- s)" unfolding l2a
using d0 pos_less_divide_eq[of "¦x -
u¦" "exp s" e] pos_less_divide_eq[of "exp s" "¦x - u¦" e]
by (simp add: mult.commute)
show "(s < ln (e / ¦x - u¦)) ⟷ ¦x - u¦ < e * exp (- s)"
using l1 l2 by (rule trans)
qed
have swap: "(∫⇧+ u. ennreal (max 0 (ln (e / ¦x - u¦))) ∂rho)
= (∫⇧+ s. emeasure rho {u. ¦x - u¦ <
e * exp (- s)} * indicator {0..} s ∂lborel)"
proof -
define f where "f u = max 0 (ln (e / ¦x - u¦))" for u :: real
have fnn: "⋀u. 0 ≤ f u" unfolding f_def by simp
have A: "(∫⇧+ u. ennreal (f u) ∂rho) =
(∫⇧+ u. (∫⇧+ s. indicator {0..<f u} s ∂lborel)
∂rho)"
using cake[OF fnn] by simp
have "finite_measure rho" using rho_univ by (auto simp: rho_def intro: finite_measureI)
hence ps: "pair_sigma_finite rho lborel" using sigma_finite_lborel
unfolding pair_sigma_finite_def finite_measure_def by simp
have sr: "sets (rho ⨂⇩M lborel) = sets (borel ⨂⇩M borel)"
unfolding rho_def using sets_pair_measure_cong by simp
have mf0a: "(λp :: real × real. indicator {p :: real × real. 0 ≤
snd p ∧ snd p < max 0 (ln (e / ¦x - fst p¦))} p :: ennreal) ∈
borel_measurable (borel ⨂⇩M borel)"
by measurable
have mf0e: "(λp :: real × real. indicator {0..<f (fst p)} (snd p) :: ennreal) =
(λp :: real × real. indicator {p :: real × real. 0 ≤ snd p ∧
snd p < max 0 (ln (e / ¦x - fst p¦))} p :: ennreal)"
unfolding f_def by (simp add: indicator_def)
have mf0: "(λp :: real ×
real. indicator {0..<f (fst p)} (snd p) :: ennreal) ∈
borel_measurable (borel ⨂⇩M borel)" unfolding mf0e by (rule mf0a)
have mf: "(λ(u, s). indicator {0..<f u} s :: ennreal) ∈
borel_measurable (rho ⨂⇩M lborel)" unfolding split_beta'
using mf0 measurable_cong_sets[OF sr refl] by auto
have B: "(∫⇧+ u. (∫⇧+ s. indicator {0..<f u} s ∂lborel)
∂rho) = (∫⇧+ s. (∫⇧+ u. indicator {0..<f u} s
∂rho) ∂lborel)"
using pair_sigma_finite.Fubini'[OF ps mf] by simp
have C: "⋀s. (∫⇧+ u. indicator {0..<f u} s ∂rho) =
emeasure rho {u. ¦x - u¦ < e * exp (- s)} * indicator {0..} s"
proof -
fix s :: real
show "(∫⇧+ u. indicator {0..<f u} s ∂rho) =
emeasure rho {u. ¦x - u¦ < e * exp (- s)} * indicator {0..} s"
proof (cases "0 ≤ s")
case False
have z: "⋀u. (indicator {0..<f u} s :: ennreal) = 0" using False by simp
show ?thesis using False unfolding z by simp
next
case True
have ind: "⋀u. (indicator {0..<f u} s :: ennreal) = indicator ({u. ¦x - u¦ <
e * exp (- s)} - {x}) u"
proof -
fix u :: real
show "(indicator {0..<f u} s :: ennreal) = indicator ({u. ¦x - u¦ <
e * exp (- s)} - {x}) u"
proof (cases "u = x")
case True
have fx: "f u = 0" unfolding f_def True by simp
show ?thesis unfolding fx using True by simp
next
case False
have "(s < f u) ⟷ ¦x - u¦ < e * exp (- s)"
unfolding f_def using level[OF ‹0 ≤ s› False] ‹0 ≤
s› by linarith
thus ?thesis using False ‹0 ≤ s› unfolding indicator_def by simp
qed
qed
have meas2: "{u. ¦x - u¦ < e * exp (- s)} ∈ sets rho" unfolding rho_def
by simp
have null: "{x} ∈ null_sets rho" using rho_singleton[of x] unfolding rho_def by auto
have meas3: "{u. ¦x - u¦ < e * exp (- s)} - {x} ∈ sets rho" using meas2 null
by auto
show ?thesis unfolding ind using True meas3 emeasure_Diff_null_set[OF null meas2] by simp
qed
qed
have "(∫⇧+ u. ennreal (f u) ∂rho) =
(∫⇧+ s. emeasure rho {u. ¦x - u¦ <
e * exp (- s)} * indicator {0..} s ∂lborel)"
unfolding A B C ..
thus ?thesis unfolding f_def .
qed
have ball: "⋀s. emeasure rho {u. ¦x - u¦ < e * exp (- s)} ≤
ennreal (40 * sqrt (e * exp (- s)))"
proof -
fix s :: real
have r0: "0 ≤ e * exp (- s)" using e by simp
have sub: "{u. ¦x - u¦ < e * exp (- s)} ⊆
{x - e * exp (- s)..x + e * exp (- s)}" by auto
have meas: "{x - e * exp (- s)..x + e * exp (- s)} ∈ sets rho" unfolding rho_def by simp
show "emeasure rho {u. ¦x - u¦ < e * exp (- s)} ≤
ennreal (40 * sqrt (e * exp (- s)))"
using emeasure_mono[OF sub meas] rho_Icc_le[OF r0, of x] by (rule order_trans)
qed
have tail: "(∫⇧+ s. ennreal (40 * sqrt (e * exp (- s))) *
indicator {0..} s ∂lborel) = ennreal (80 * sqrt e)"
proof -
have sq: "⋀s. sqrt (e * exp (- s)) = sqrt e * exp (- s / 2)"
proof -
fix s :: real
have ee: "exp (- s) = exp (- s / 2) * exp (- s / 2)" by (simp add: exp_add["symmetric"])
show "sqrt (e * exp (- s)) = sqrt e * exp (- s / 2)" unfolding ee
using real_sqrt_mult[of e "exp (- s / 2) * exp (- s / 2)"] by simp
qed
have m: "(λs. 40 * (sqrt e * exp (- s / 2))) ∈ borel_measurable borel" by simp
have d: "⋀s. 0 ≤ s ⟹
((λs. - 80 * sqrt e * exp (- s / 2)) has_real_derivative 40 * (sqrt e * exp (- s /
2))) (at s)" by (force intro: derivative_eq_intros)
have n: "⋀s. 0 ≤ s ⟹ 0 ≤ 40 * (sqrt e * exp (- s / 2))" using e
by simp
have h1: "filterlim (λs::real. 1 / 2 * s) at_top at_top"
using filterlim_tendsto_pos_mult_at_top[OF tendsto_const _ filterlim_ident,
of "1 / 2 :: real"] by simp
have h2: "((λy::real. exp (- y)) ⤏ 0) at_top"
by (intro filterlim_compose[OF exp_at_bot] filterlim_uminus_at_bot_at_top)
have h3: "((λs::real. exp (- (1 / 2 * s))) ⤏ 0) at_top"
using filterlim_compose[OF h2 h1] by (simp add: o_def)
have l: "((λs. - 80 * sqrt e * exp (- s / 2)) ⤏ 0) at_top"
using tendsto_mult_right_zero[OF h3, of "- 80 * sqrt e"] by simp
have ftc: "(∫⇧+ s. ennreal (40 * (sqrt e * exp (- s / 2))) *
indicator {0..} s ∂lborel) = ennreal (80 * sqrt e)"
using nn_integral_FTC_atLeast[where f = "λs. 40 * (sqrt e * exp (- s / 2))" and F =
"λs. - 80 * sqrt e * exp (- s / 2)" and a = 0 and T = 0, OF m d n l] by simp
show ?thesis unfolding sq using ftc .
qed
have mono: "(∫⇧+ s. emeasure rho {u. ¦x - u¦ <
e * exp (- s)} * indicator {0..} s ∂lborel) ≤
(∫⇧+ s. ennreal (40 * sqrt (e * exp (- s))) *
indicator {0..} s ∂lborel)"
using ball by (force intro: nn_integral_mono mult_right_mono)
show ?thesis
unfolding swap using mono tail by simp
qed
text ‹Helpers for (6.9): the normalised arclength density on @{text "[0, 2π]"} and the
circle measures.›
abbreviation cden :: "real measure" where
"cden ≡ density lborel (λθ. ennreal (indicator {0..2 * pi} θ / (2 *
pi)))"
lemma cden_univ: "emeasure cden UNIV = 1"
proof -
have "emeasure cden UNIV = (∫⇧+ θ. ennreal (indicator {0..2 *
pi} θ / (2 * pi)) ∂lborel)"
by (simp add: emeasure_density)
also have "… = (∫⇧+ θ. ennreal (1 / (2 * pi)) * indicator {0..2 *
pi} θ ∂lborel)"
by (auto simp: indicator_def intro: nn_integral_cong)
also have "… = ennreal (1 / (2 * pi)) * ennreal (2 * pi)"
by (simp add: nn_integral_cmult_indicator)
also have "… = 1"
by (simp add: ennreal_mult["symmetric"])
finally show ?thesis .
qed
lemma cden_finite: "finite_measure cden"
using cden_univ by (auto intro: finite_measureI)
lemma circ_meas: "(λθ :: real. c + of_real ε * cis θ) ∈
borel_measurable borel"
by (fast intro: borel_measurable_continuous_onI continuous_intros)
lemma circ_meas': "(λθ :: real. c + of_real ε * cis θ) ∈
measurable cden borel"
using circ_meas[of c ε] by simp
lemma sets_circ: "sets (circ c ε) = sets borel"
unfolding circ_def by simp
lemma space_circ: "space (circ c ε) = UNIV"
unfolding circ_def by simp
lemma circ_univ: "emeasure (circ c ε) UNIV = 1"
unfolding circ_def using emeasure_distr[OF circ_meas'[of c ε], of UNIV] cden_univ by simp
lemma circ_finite: "finite_measure (circ c ε)"
using circ_univ[of c ε] space_circ[of c ε] by (auto intro: finite_measureI)
lemma circ_AE: "AE z in circ c ε. norm (z - c) = ¦ε¦"
proof -
have P: "{z ∈ space borel. norm (z - c) = ¦ε¦} ∈
sets (borel :: complex measure)"
by measurable
have pt: "AE θ in cden. norm (c + of_real ε * cis θ - c) =
¦ε¦"
by (simp add: norm_mult)
show ?thesis unfolding circ_def using AE_distr_iff[OF circ_meas'[of c ε] P] pt by simp
qed
lemma circ_integrable_bound:
fixes f :: "complex ⇒ real" and B :: real
assumes m: "f ∈ borel_measurable borel" and b: "⋀z. norm (z - c) =
¦ε¦ ⟹ ¦f z¦ ≤ B"
shows "integrable (circ c ε) f"
proof -
have m': "f ∈ borel_measurable (circ c ε)"
using m measurable_cong_sets[OF sets_circ[of c ε] refl]
by auto
have ae: "AE z in circ c ε. norm (f z) ≤ B" using circ_AE[of c ε] b
by (auto elim: eventually_mono)
show ?thesis using finite_measure.integrable_const_bound[OF circ_finite ae m'] .
qed
lemma cis_eq_null: "{θ :: real. cis θ = w} ∈ null_sets lborel"
proof -
have bad: "{θ. cis θ = w} ⊆
range (λn::int. Arg w + 2 * pi * of_int n)"
proof
fix θ assume th: "θ ∈ {θ. cis θ = w}"
have w0: "w ≠ 0" using th
by auto
have cw: "cis (Arg w) = w" using cis_Arg[OF w0] th
by (force simp: sgn_div_norm)
have "sin θ = sin (Arg w) ∧ cos θ = cos (Arg w)" using th cw
by (simp add: complex_eq_iff)
then obtain n :: int where "θ = Arg w + 2 * pi * n" using sin_cos_eq_iff by blast
thus "θ ∈ range (λn::int. Arg w + 2 * pi * of_int n)" by auto
qed
show ?thesis using countable_imp_null_set_lborel countable_subset[OF bad]
by fast
qed
lemma circ_log_integrable:
assumes e: "0 < ε"
shows "integrable (circ c ε) (λz. ln (norm (z - a)))"
proof -
define w where "w = (a - c) / of_real ε"
have mF: "(λz :: complex. ln (norm (z - a))) ∈ borel_measurable borel"
by simp
have mh: "(λθ. ln (norm (c + of_real ε * cis θ - a))) ∈
borel_measurable borel"
using measurable_compose[OF circ_meas[of c ε] mF] by (simp add: o_def)
have n2: "(λθ. norm (cis θ - w)) ∈ borel_measurable borel"
by (fast intro: borel_measurable_continuous_onI continuous_intros)
have mk: "(λθ. ln ε + ln (norm (cis θ - w))) ∈
borel_measurable borel" using borel_measurable_ln[OF n2]
by (auto intro: borel_measurable_add)
have pw: "ln (norm (c + of_real ε * cis θ - a)) =
ln ε + ln (norm (cis θ - w))" if nw: "cis θ ≠ w" for θ
proof -
have eq: "c + of_real ε * cis θ - a = of_real ε * (cis θ - w)"
using e unfolding w_def
by (simp add: field_simps)
show ?thesis unfolding eq norm_mult using e nw ln_mult[of ε "norm (cis θ - w)"]
by simp
qed
have ae: "AE θ ∈ einterval (min (ereal 0) (ereal (2 * pi))) (max (ereal 0) (ereal (2 *
pi))) in lborel. ln (norm (c + of_real ε * cis θ - a)) =
ln ε + ln (norm (cis θ - w))"
using AE_I'[OF cis_eq_null[of w], of "λθ. θ ∈
einterval (min (ereal 0) (ereal (2 * pi))) (max (ereal 0) (ereal (2 * pi))) ⟶
ln (norm (c + of_real ε * cis θ - a)) =
ln ε + ln (norm (cis θ - w))"] pw
by blast
have ii0: "interval_lebesgue_integrable lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln ε + ln (norm (cis θ - w)))"
using interval_lebesgue_integral_add(1)[OF interval_integral_const(1) circle_log_integrable[of
w]] .
have "interval_lebesgue_integrable lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (c + of_real ε * cis θ - a)))"
using interval_lebesgue_integrable_cong_AE[of "λθ. ln (norm (c +
of_real ε * cis θ - a))" "λθ. ln ε +
ln (norm (cis θ - w))" "ereal 0" "ereal (2 * pi)"] mh mk ae ii0 by simp
hence "set_integrable lborel {0<..<2 * pi} (λθ. ln (norm (c + of_real ε *
cis θ - a)))"
unfolding interval_lebesgue_integrable_def by simp
hence "set_integrable lborel {0..2 * pi} (λθ. ln (norm (c + of_real ε *
cis θ - a)))"
using set_integrable_discrete_difference[where X = "{0, 2 * pi}" and M = lborel and A =
"{0..2 * pi}" and B = "{0<..<2 * pi}" and f =
"λθ. ln (norm (c + of_real ε * cis θ - a))"]
by force
hence i1a: "integrable lborel (λθ. (1 / (2 * pi)) * (indicator {0..2 *
pi} θ *⇩R ln (norm (c + of_real ε * cis θ - a))))"
unfolding set_integrable_def by simp
have eqf: "(λθ. (indicator {0..2 * pi} θ / (2 * pi)) *⇩R ln (norm (c +
of_real ε * cis θ - a))) =
(λθ. (1 / (2 * pi)) * (indicator {0..2 * pi} θ *⇩R ln (norm (c +
of_real ε * cis θ - a))))"
by (simp add: fun_eq_iff)
have i1: "integrable lborel (λθ. (indicator {0..2 * pi} θ / (2 *
pi)) *⇩R ln (norm (c + of_real ε * cis θ - a)))"
unfolding eqf by (rule i1a)
have mg: "(λθ :: real. indicator {0..2 * pi} θ / (2 * pi)) ∈
borel_measurable lborel"
by simp
have i2: "integrable cden (λθ. ln (norm (c + of_real ε * cis θ -
a)))"
using integrable_density[of "λθ. ln (norm (c + of_real ε *
cis θ - a))" lborel "λθ. indicator {0..2 * pi} θ / (2 *
pi)"] mh mg i1
by simp
show ?thesis unfolding circ_def using integrable_distr_eq[OF circ_meas'[of c ε] mF] i2
by simp
qed
lemma circ_singleton:
assumes e: "0 < ε"
shows "emeasure (circ c ε) {a} = 0"
proof -
define w where "w = (a - c) / of_real ε"
have pre: "(λθ. c + of_real ε * cis θ) -` {a} ∩ space cden =
{θ. cis θ = w}"
unfolding w_def using e by (auto simp: field_simps)
have "{θ :: real. cis θ = w} ∈ sets lborel" using cis_eq_null[of w]
by (simp add: null_sets_def)
hence d1: "emeasure cden {θ. cis θ = w} =
(∫⇧+ θ. ennreal (indicator {0..2 * pi} θ / (2 * pi)) *
indicator {θ. cis θ = w} θ ∂lborel)"
by (simp add: emeasure_density)
have d2: "(∫⇧+ θ. ennreal (indicator {0..2 * pi} θ / (2 * pi)) *
indicator {θ. cis θ = w} θ ∂lborel) = 0"
by (rule nn_integral_null_set[OF cis_eq_null[of w]])
have d: "emeasure cden {θ. cis θ = w} = 0"
using d1 d2 by simp
show ?thesis unfolding circ_def using emeasure_distr[OF circ_meas'[of c ε],
of "{a}"] pre d
by simp
qed
lemma circ_neg_log:
fixes c z :: complex and ε R :: real
assumes e: "0 < ε" and hc: "norm c + ε ≤ R" and hz: "norm z ≤ R"
shows "(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂circ c ε) ≤
ennreal (2 * R - ln ε)"
proof -
define g where "g w = ln (norm (w - z))" for w :: complex
have ig: "integrable (circ c ε) g" unfolding g_def
using circ_log_integrable[OF e, of c z] .
have ipos: "integrable (circ c ε) (λw. max 0 (g w))" using ig
using integrable_max by simp
have ineg: "integrable (circ c ε) (λw. max 0 (- g w))" using ig
using integrable_max by simp
have e1: "(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂circ c ε) =
(∫⇧+ w. ennreal (max 0 (- g w)) ∂circ c ε)"
unfolding g_def by (simp add: norm_minus_commute ennreal_max_0)
have e2: "(∫⇧+ w. ennreal (max 0 (- g w)) ∂circ c ε) =
ennreal (integral⇧L (circ c ε) (λw. max 0 (- g w)))"
using nn_integral_eq_integral[OF ineg] by simp
have e3: "integral⇧L (circ c ε) (λw. max 0 (- g w)) =
integral⇧L (circ c ε) (λw. max 0 (g w)) -
integral⇧L (circ c ε) g"
proof -
have pt: "(λw. max 0 (- g w)) = (λw. max 0 (g w) - g w)"
by (simp add: fun_eq_iff max_def)
show ?thesis unfolding pt using Bochner_Integration.integral_diff[OF ipos ig] .
qed
have h1: "ln ε ≤ integral⇧L (circ c ε) g" unfolding g_def
using circ_log[OF e, of c z] e
by simp
have R0: "0 ≤ R" using hc e norm_ge_zero[of c]
by linarith
have hb: "AE w in circ c ε. max 0 (g w) ≤ 2 * R"
proof -
have pt: "max 0 (g w) ≤ 2 * R" if hw: "norm (w - c) = ¦ε¦" for w
proof -
have "norm w ≤ R" using hw hc e norm_triangle_ineq[of "w - c" c]
by simp
hence w2: "norm (w - z) ≤ 2 * R" using hz norm_triangle_ineq4[of w z]
by simp
have w3: "g w ≤ norm (w - z)" unfolding g_def
by (metis less_eq_real_def ln_0 ln_less_self norm_ge_zero)
show ?thesis using w2 w3 R0
by simp
qed
show ?thesis using circ_AE[of c ε] pt
by (auto elim: eventually_mono)
qed
have h2: "integral⇧L (circ c ε) (λw. max 0 (g w)) ≤ 2 * R"
proof -
have "integral⇧L (circ c ε) (λw. max 0 (g w)) ≤
integral⇧L (circ c ε) (λw. 2 * R)"
using integral_mono_AE[OF ipos _ hb] finite_measure.integrable_const[OF circ_finite]
by auto
also have "… = 2 * R" using circ_univ[of c ε] space_circ[of c ε]
by (simp add: measure_def)
finally show ?thesis .
qed
show ?thesis unfolding e1 e2 e3 using h1 h2
using ennreal_leI by simp
qed
text ‹Finite sums of circle measures,
realised as a push-forward of @{text "count_space I ⨂ cden"}.›
lemma csum_meas:
fixes c :: "nat ⇒ complex" and I :: "nat set"
assumes I: "countable I"
shows "(λ(i, θ). c i + of_real ε * cis θ) ∈
measurable (count_space I ⨂⇩M cden) borel"
using measurable_pair_measure_countable1[OF I, of "λ(i,
θ). c i + of_real ε * cis θ" cden borel] circ_meas'
by simp
lemma csum_nn:
fixes c :: "nat ⇒ complex" and I :: "nat set" and f :: "complex ⇒ ennreal"
assumes I: "finite I" and f: "f ∈ borel_measurable borel"
shows "(∫⇧+ z. f z ∂distr (count_space I ⨂⇩M cden) borel
(λ(i, θ). c i + of_real ε * cis θ))
= (∑ i ∈ I. ∫⇧+ z. f z ∂circ (c i) ε)"
proof -
have m: "(λ(i, θ). c i + of_real ε * cis θ) ∈
measurable (count_space I ⨂⇩M cden) borel"
using csum_meas[OF countable_finite[OF I]] .
have sf: "sigma_finite_measure cden" using cden_finite
by (simp add: finite_measure_def)
have mfp: "(λp. f ((λ(i,
θ). c i + of_real ε * cis θ) p)) ∈
borel_measurable (count_space I ⨂⇩M cden)"
using measurable_compose[OF m f] by (simp add: o_def)
have e1: "(∫⇧+ z. f z ∂distr (count_space I ⨂⇩M cden) borel
(λ(i, θ). c i + of_real ε * cis θ))
= (∫⇧+ p. f ((λ(i,
θ). c i + of_real ε *
cis θ) p) ∂(count_space I ⨂⇩M cden))"
using nn_integral_distr[OF m] f by simp
have e2: "(∫⇧+ p. f ((λ(i,
θ). c i + of_real ε *
cis θ) p) ∂(count_space I ⨂⇩M cden))
= (∫⇧+ i. (∫⇧+ θ. f (c i + of_real ε *
cis θ) ∂cden) ∂count_space I)"
using sigma_finite_measure.nn_integral_fst[OF sf mfp] by simp
have e4: "⋀i. (∫⇧+ θ. f (c i + of_real ε *
cis θ) ∂cden) = (∫⇧+ z. f z ∂circ (c i) ε)"
unfolding circ_def using nn_integral_distr[OF circ_meas'] f by simp
have e3: "(∫⇧+ i. (∫⇧+ θ. f (c i + of_real ε *
cis θ) ∂cden) ∂count_space I)
= (∑ i ∈ I. ∫⇧+ z. f z ∂circ (c i) ε)"
unfolding e4 by (rule nn_integral_count_space_finite[OF I])
show ?thesis unfolding e1 e2 e3 ..
qed
lemma csum_emeasure:
fixes c :: "nat ⇒ complex" and I :: "nat set"
assumes I: "finite I" and A: "A ∈ sets borel"
shows "emeasure (distr (count_space I ⨂⇩M cden) borel (λ(i,
θ). c i + of_real ε * cis θ)) A = (∑ i ∈
I. emeasure (circ (c i) ε) A)"
using csum_nn[OF I, where f = "indicator A" and c = c and ε = ε] A sets_circ
by simp
lemma csum_integral:
fixes c :: "nat ⇒ complex" and I :: "nat set" and f :: "complex ⇒ real"
assumes I: "finite I" and f: "f ∈ borel_measurable borel" and fi: "⋀i. i ∈
I ⟹ integrable (circ (c i) ε) f"
shows "integrable (distr (count_space I ⨂⇩M cden) borel (λ(i,
θ). c i + of_real ε * cis θ)) f"
and "integral⇧L (distr (count_space I ⨂⇩M cden) borel (λ(i,
θ). c i + of_real ε * cis θ)) f = (∑ i ∈
I. integral⇧L (circ (c i) ε) f)"
proof -
have m: "(λ(i, θ). c i + of_real ε * cis θ) ∈
measurable (count_space I ⨂⇩M cden) borel"
using csum_meas[OF countable_finite[OF I]] .
have mn: "(λz. ennreal (norm (f z))) ∈ borel_measurable borel" using f
by simp
have fin: "⋀i. i ∈ I ⟹
(∫⇧+ z. ennreal (norm (f z)) ∂circ (c i) ε) < ∞"
using fi
by (simp add: integrable_iff_bounded)
have nnD: "(∫⇧+ z. ennreal (norm (f z)) ∂distr (count_space I
⨂⇩M cden) borel (λ(i,
θ). c i + of_real ε * cis θ)) < ∞"
unfolding csum_nn[OF I mn] using fin I ennreal_sum_less_top[OF I] by simp
have "f ∈ borel_measurable (distr (count_space I ⨂⇩M cden) borel (λ(i,
θ). c i + of_real ε * cis θ))"
using f by simp
thus "integrable (distr (count_space I ⨂⇩M cden) borel (λ(i,
θ). c i + of_real ε * cis θ)) f"
using nnD by (simp add: integrable_iff_bounded)
hence iP: "integrable (count_space I ⨂⇩M cden) (λp. f ((λ(i,
θ). c i + of_real ε * cis θ) p))"
using integrable_distr_eq[OF m f] by simp
have ps: "pair_sigma_finite (count_space I) cden"
using sigma_finite_measure_count_space_finite[OF I] cden_finite
unfolding pair_sigma_finite_def by (simp add: finite_measure_def)
have e1: "integral⇧L (distr (count_space I ⨂⇩M cden) borel (λ(i,
θ). c i + of_real ε * cis θ)) f
= integral⇧L (count_space I ⨂⇩M cden) (λp. f ((λ(i,
θ). c i + of_real ε * cis θ) p))"
by (rule integral_distr[OF m f])
have e2: "integral⇧L (count_space I ⨂⇩M cden) (λp. f ((λ(i,
θ). c i + of_real ε * cis θ) p))
= (∫ i. (∫ θ. f (c i + of_real ε *
cis θ) ∂cden) ∂count_space I)"
using pair_sigma_finite.integral_fst'[OF ps iP] by simp
have e4: "⋀i. (∫ θ. f (c i + of_real ε *
cis θ) ∂cden) = integral⇧L (circ (c i) ε) f"
unfolding circ_def using integral_distr[OF circ_meas' f] by simp
have e3: "(∫ i. (∫ θ. f (c i + of_real ε *
cis θ) ∂cden) ∂count_space I)
= (∑ i ∈ I. integral⇧L (circ (c i) ε) f)"
unfolding e4 by (rule lebesgue_integral_count_space_finite[OF I])
show "integral⇧L (distr (count_space I ⨂⇩M cden) borel (λ(i,
θ). c i + of_real ε * cis θ)) f = (∑ i ∈
I. integral⇧L (circ (c i) ε) f)"
unfolding e1 e2 e3 ..
qed
text ‹A scaled measure is a density with a constant; the Bochner integral scales.›
lemma scale_density:
fixes M :: "'a measure" and r :: real
shows "scale_measure (ennreal r) M = density M (λ_. ennreal r)"
proof (rule measure_eqI)
show "sets (scale_measure (ennreal r) M) = sets (density M (λ_. ennreal r))"
by simp
fix A assume A: "A ∈ sets (scale_measure (ennreal r) M)"
show "emeasure (scale_measure (ennreal r) M) A = emeasure (density M (λ_. ennreal r)) A"
using A by (simp add: emeasure_density nn_integral_cmult_indicator)
qed
lemma scale_integral:
fixes M :: "'a measure" and f :: "'a ⇒ real" and r :: real
assumes r: "0 ≤ r" and f: "f ∈ borel_measurable M"
shows "integral⇧L (scale_measure (ennreal r) M) f = r * integral⇧L M f"
and "integrable M f ⟹ integrable (scale_measure (ennreal r) M) f"
proof -
have g: "(λ_. r) ∈ borel_measurable M"
by simp
have nn: "AE x in M. 0 ≤ r" using r
by simp
show "integral⇧L (scale_measure (ennreal r) M) f = r * integral⇧L M f"
unfolding scale_density
using integral_density[OF f g nn] by simp
show "integrable M f ⟹ integrable (scale_measure (ennreal r) M) f"
unfolding scale_density
using integrable_density[OF f g nn] by simp
qed
text ‹Facts about @{text ρ} and its image on @{text ℂ}.›
lemma rho_finite: "finite_measure rho"
using rho_univ by (auto simp: rho_def intro: finite_measureI)
lemma rhoC_meas: "(of_real :: real ⇒ complex) ∈ measurable rho borel"
unfolding rho_def by simp
lemma sets_rhoC: "sets (distr rho borel (of_real :: real ⇒ complex)) = sets borel"
by simp
lemma rhoC_finite: "finite_measure (distr rho borel (of_real :: real ⇒ complex))"
using finite_measure.finite_measure_distr[OF rho_finite rhoC_meas] .
lemma rhoC_singleton: "emeasure (distr rho borel (of_real :: real ⇒ complex)) {a} = 0"
proof -
have sub: "(of_real :: real ⇒ complex) -` {a} ∩ space rho ⊆ {Re a}"
by auto
have sm: "{Re a} ∈ sets rho" unfolding rho_def
by simp
have le: "emeasure rho ((of_real :: real ⇒ complex) -` {a} ∩ space rho) ≤
emeasure rho {Re a}"
by (rule emeasure_mono[OF sub sm])
show ?thesis using emeasure_distr[OF rhoC_meas, of "{a}"] le rho_singleton[of "Re a"]
by simp
qed
lemma rhoC_AE: "AE w in distr rho borel (of_real :: real ⇒ complex). norm w ≤ 2"
proof -
have P: "{w ∈ space borel. norm w ≤ (2 :: real)} ∈ sets (borel :: complex measure)"
by measurable
have nul: "- {0<..<2 :: real} ∈ null_sets rho" using rho_compl unfolding rho_def
by auto
have ae: "AE u in rho. norm (of_real u :: complex) ≤ 2"
using AE_I'[OF nul, of "λu. norm (of_real u :: complex) ≤ 2"]
by force
show ?thesis using AE_distr_iff[OF rhoC_meas P] ae
by simp
qed
lemma rhoC_neg_log: "(∫⇧+ w. ennreal (- ln (norm (z -
w))) ∂distr rho borel (of_real :: real ⇒ complex)) ≤ ennreal 80"
proof -
have mf: "(λw :: complex. ennreal (- ln (norm (z - w)))) ∈ borel_measurable borel"
by simp
have e1: "(∫⇧+ w. ennreal (- ln (norm (z -
w))) ∂distr rho borel (of_real :: real ⇒ complex)) =
(∫⇧+ u. ennreal (- ln (norm (z - of_real u))) ∂rho)"
using nn_integral_distr[OF rhoC_meas] mf by simp
have nul: "{Re z} ∈ null_sets rho" using rho_singleton[of "Re z"] unfolding rho_def
by auto
have ae: "AE u in rho. u ≠ Re z"
using AE_I'[OF nul, of "λu. u ≠ Re z"] by auto
have pt: "ennreal (- ln (norm (z - of_real u))) ≤
ennreal (max 0 (ln (1 / ¦Re z - u¦)))" if u: "u ≠ Re z" for u
proof -
have d0: "0 < ¦Re z - u¦" using u
by simp
have dle: "¦Re z - u¦ ≤ norm (z - of_real u)"
using abs_Re_le_cmod[of "z - of_real u"]
by simp
have l1: "- ln (norm (z - of_real u)) ≤ - ln ¦Re z - u¦"
using d0 dle ln_le_cancel_iff[of "¦Re z - u¦" "norm (z - of_real u)"]
by linarith
have l2: "- ln ¦Re z - u¦ = ln (1 / ¦Re z - u¦)" using d0
by (simp add: ln_div)
show ?thesis using l1 l2
using ennreal_leI by simp
qed
have e2: "(∫⇧+ u. ennreal (- ln (norm (z - of_real u))) ∂rho) ≤
(∫⇧+ u. ennreal (max 0 (ln (1 / ¦Re z - u¦))) ∂rho)"
using ae pt by (auto intro: nn_integral_mono_AE elim: eventually_mono)
have e3: "(∫⇧+ u. ennreal (max 0 (ln (1 / ¦Re z -
u¦))) ∂rho) ≤ ennreal 80"
using cross_bound[of 1 "Re z"] by simp
show ?thesis unfolding e1 using e2 e3 by (rule order_trans)
qed
text ‹Integrability of @{text "log|z - w|"} against a product of finite measures carried
by a ball.›
lemma ennreal_abs_ln_le:
fixes y :: real
assumes y: "0 ≤ y"
shows "ennreal ¦ln y¦ ≤ ennreal y + ennreal (- ln y)"
proof -
have "ln y ≤ y" using y
by (metis assms ln_0 ln_bound less_eq_real_def)
hence "¦ln y¦ ≤ y + max 0 (- ln y)" using y
by simp
hence "ennreal ¦ln y¦ ≤ ennreal (y + max 0 (- ln y))" by (rule ennreal_leI)
also have "… = ennreal y + ennreal (- ln y)" using y
by (simp add: ennreal_plus ennreal_max_0)
finally show ?thesis .
qed
lemma integrable_log_prod:
fixes μ ν :: "complex measure" and R C :: real
assumes fm: "finite_measure μ" and fn: "finite_measure ν" and sm: "sets μ =
sets borel" and sn: "sets ν = sets borel"
and aem: "AE z in μ. norm z ≤ R" and aen: "AE w in ν. norm w ≤ R"
and lg: "⋀z. norm z ≤ R ⟹
(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂ν) ≤ ennreal C"
shows "integrable (μ ⨂⇩M ν) (λp. ln (norm (fst p - snd p)))"
proof -
have sp: "sets (μ ⨂⇩M ν) = sets (borel ⨂⇩M borel)" using sm sn
using sets_pair_measure_cong by simp
have "(λp :: complex × complex. ln (norm (fst p - snd p))) ∈
borel_measurable (borel ⨂⇩M borel)"
by simp
hence m: "(λp. ln (norm (fst p - snd p))) ∈
borel_measurable (μ ⨂⇩M ν)" using measurable_cong_sets[OF sp refl]
by blast
have sfn: "sigma_finite_measure ν" using fn
by (simp add: finite_measure_def)
have ma: "(λp. ennreal (norm (ln (norm (fst p - snd p))))) ∈
borel_measurable (μ ⨂⇩M ν)" using m
by simp
have fub: "(∫⇧+ p. ennreal (norm (ln (norm (fst p -
snd p)))) ∂(μ ⨂⇩M ν)) =
(∫⇧+ z. (∫⇧+ w. ennreal (norm (ln (norm (z -
w)))) ∂ν) ∂μ)"
using sigma_finite_measure.nn_integral_fst[OF sfn ma] by simp
define B where "B = ennreal (2 * R) * emeasure ν (space ν) + ennreal C"
have inner: "⋀z. norm z ≤ R ⟹
(∫⇧+ w. ennreal (norm (ln (norm (z - w)))) ∂ν) ≤ B"
proof -
fix z :: complex assume hz: "norm z ≤ R"
have mw1: "(λw. ennreal (norm (z - w))) ∈ borel_measurable ν"
unfolding measurable_cong_sets[OF sn refl]
by simp
have mw2: "(λw. ennreal (- ln (norm (z - w)))) ∈ borel_measurable ν"
unfolding measurable_cong_sets[OF sn refl]
by simp
have s1: "(∫⇧+ w. ennreal (norm (ln (norm (z - w)))) ∂ν) ≤
(∫⇧+ w. ennreal (norm (z - w)) + ennreal (- ln (norm (z -
w))) ∂ν)"
using ennreal_abs_ln_le by (auto intro: nn_integral_mono)
have s2: "(∫⇧+ w. ennreal (norm (z - w)) + ennreal (- ln (norm (z -
w))) ∂ν) = (∫⇧+ w. ennreal (norm (z - w)) ∂ν) +
(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂ν)"
by (rule nn_integral_add[OF mw1 mw2])
have a: "AE w in ν. ennreal (norm (z - w)) ≤ ennreal (2 * R)"
proof -
have pt: "ennreal (norm (z - w)) ≤ ennreal (2 * R)" if w: "norm w ≤ R" for w
using w hz norm_triangle_ineq4[of z w] using ennreal_leI by simp
show ?thesis using aen pt
by (auto elim: eventually_mono)
qed
have s3: "(∫⇧+ w. ennreal (norm (z - w)) ∂ν) ≤
ennreal (2 * R) * emeasure ν (space ν)"
using nn_integral_mono_AE[OF a] by simp
show "(∫⇧+ w. ennreal (norm (ln (norm (z - w)))) ∂ν) ≤ B"
unfolding B_def using s1 s2 s3 lg[OF hz]
by (auto intro: add_mono order_trans)
qed
have outer: "(∫⇧+ z. (∫⇧+ w. ennreal (norm (ln (norm (z -
w)))) ∂ν) ∂μ) ≤ (∫⇧+ z. B ∂μ)"
using aem inner by (fast intro: nn_integral_mono_AE elim: eventually_mono)
have "B < ∞" unfolding B_def
using finite_measure.emeasure_finite[OF fn, of "space ν"]
by (simp add: ennreal_mult_less_top less_top)
hence fin: "(∫⇧+ z. B ∂μ) < ∞"
using finite_measure.emeasure_finite[OF fm, of "space μ"]
by (simp add: ennreal_mult_less_top less_top)
show ?thesis unfolding integrable_iff_bounded using m fub outer fin
by simp
qed
text ‹The sum of two measures with the Borel sets, as @{const measure_of}.›
lemma summ_sets:
fixes μ ν :: "'a::topological_space measure"
shows "sets (measure_of UNIV (sets borel) (λA. emeasure μ A + emeasure ν A)) =
sets (borel :: 'a measure)"
using sets.sigma_sets_eq[of borel] sets_measure_of[of "sets borel" UNIV] by simp
lemma summ_emeasure:
fixes μ ν :: "'a::topological_space measure"
assumes s1: "sets μ = sets borel" and s2: "sets ν = sets borel" and A: "A ∈
sets borel"
shows "emeasure (measure_of UNIV (sets borel) (λA. emeasure μ A +
emeasure ν A)) A = emeasure μ A + emeasure ν A"
proof (rule emeasure_measure_of_sigma)
show "sigma_algebra UNIV (sets borel)" using sets.sigma_algebra_axioms[of borel]
by simp
show "positive (sets borel) (λA. emeasure μ A + emeasure ν A)"
unfolding positive_def
by simp
show "countably_additive (sets borel) (λA. emeasure μ A + emeasure ν A)"
unfolding countably_additive_def
proof (intro allI impI)
fix F :: "nat ⇒ 'a set"
assume F1: "range F ⊆ sets borel" and F2: "disjoint_family F" and F3: "⋃ (range
F) ∈ sets borel"
have a1: "(∑ i. emeasure μ (F i)) = emeasure μ (⋃ (range F))"
using suminf_emeasure[of F μ] F1 F2 s1
by simp
have a2: "(∑ i. emeasure ν (F i)) = emeasure ν (⋃ (range F))"
using suminf_emeasure[of F ν] F1 F2 s2
by simp
show "(∑ i. emeasure μ (F i) + emeasure ν (F i)) =
emeasure μ (⋃ (range F)) + emeasure ν (⋃ (range F))"
unfolding a1[symmetric] a2[symmetric]
using suminf_add[of "λi. emeasure μ (F i)" "λi. emeasure ν (F i)"]
using summableI by simp
qed
show "A ∈ sets borel" by (rule A)
qed
lemma summ_nn:
fixes μ ν :: "'a::topological_space measure" and f :: "'a ⇒ ennreal"
assumes s1: "sets μ = sets borel" and s2: "sets ν = sets borel" and f: "f ∈
borel_measurable borel"
shows "(∫⇧+ z. f z ∂measure_of UNIV (sets borel) (λA. emeasure
μ A + emeasure ν A)) = (∫⇧+ z. f z ∂μ) +
(∫⇧+ z. f z ∂ν)"
proof -
define η where "η = measure_of UNIV (sets borel) (λA. emeasure μ A +
emeasure ν A)"
have sη: "sets η = sets borel" unfolding η_def by (rule summ_sets)
have mc: "⋀g :: 'a ⇒ ennreal. g ∈ borel_measurable borel ⟹
g ∈ borel_measurable η ∧ g ∈ borel_measurable μ ∧
g ∈ borel_measurable ν"
using sη s1 s2 measurable_cong_sets by simp
have "(∫⇧+ z. f z ∂η) =
(∫⇧+ z. f z ∂μ) + (∫⇧+ z. f z ∂ν)"
using f
proof induction
case (cong f g)
show ?case using cong
by (simp add: fun_eq_iff)
next
case (set A)
show ?case using set summ_emeasure[OF s1 s2 set] sη s1 s2 unfolding η_def
by simp
next
case (mult u c)
show ?case using mult mc[OF mult(2)]
by (simp add: nn_integral_cmult distrib_left)
next
case (add u v)
show ?case using add mc
by (simp add: nn_integral_add)
next
case (seq U)
have m: "⋀i. U i ∈ borel_measurable η ∧
U i ∈ borel_measurable μ ∧ U i ∈ borel_measurable ν" using seq mc
by simp
have mη: "⋀i. U i ∈ borel_measurable η" using m by blast
have mμ: "⋀i. U i ∈ borel_measurable μ" using m by blast
have mν: "⋀i. U i ∈ borel_measurable ν" using m by blast
have c1: "(∫⇧+ z. (SUP i. U i) z ∂η) =
(SUP i. ∫⇧+ z. U i z ∂η)" unfolding SUP_apply
by (rule nn_integral_monotone_convergence_SUP[OF ‹incseq U› mη])
have c2: "(∫⇧+ z. (SUP i. U i) z ∂μ) =
(SUP i. ∫⇧+ z. U i z ∂μ)" unfolding SUP_apply
by (rule nn_integral_monotone_convergence_SUP[OF ‹incseq U› mμ])
have c3: "(∫⇧+ z. (SUP i. U i) z ∂ν) =
(SUP i. ∫⇧+ z. U i z ∂ν)" unfolding SUP_apply
by (rule nn_integral_monotone_convergence_SUP[OF ‹incseq U› mν])
have i2: "incseq (λi. ∫⇧+ z. U i z ∂μ)"
using ‹incseq U› unfolding incseq_def le_fun_def
by (auto intro: nn_integral_mono)
have i3: "incseq (λi. ∫⇧+ z. U i z ∂ν)"
using ‹incseq U› unfolding incseq_def le_fun_def
by (auto intro: nn_integral_mono)
show ?case unfolding c1 c2 c3 using seq ennreal_SUP_add[OF i2 i3]
by simp
qed
thus ?thesis unfolding η_def .
qed
text ‹Logarithmic integrals against @{text ρ}.›
lemma abs_ln_max_le:
fixes e x :: real
assumes e: "0 < e" and x: "0 ≤ x"
shows "¦ln (max e x)¦ ≤ ¦ln e¦ + x"
proof (cases "x ≤ e")
case True
show ?thesis using True x
by (simp add: max_def)
next
case False
have "ln x ≤ x" using x
by (metis ln_0 ln_bound less_eq_real_def)
moreover have "ln e ≤ ln x" using e False
by simp
ultimately show ?thesis using False
using e by linarith
qed
lemma rho_AE_Ioo: "AE u in rho. 0 < u ∧ u < 2"
proof -
have nul: "- {0<..<2 :: real} ∈ null_sets rho" using rho_compl unfolding rho_def
by auto
show ?thesis using AE_I'[OF nul, of "λu. 0 < u ∧ u < 2"]
by force
qed
lemma rho_neg_log_le: "(∫⇧+ u. ennreal (- ln ¦x - u¦) ∂rho) ≤
ennreal 80"
proof -
have pt: "⋀u. ennreal (- ln ¦x - u¦) =
ennreal (max 0 (ln (1 / ¦x - u¦)))"
by (simp add: ln_div ennreal_max_0)
show ?thesis unfolding pt using cross_bound[of 1 x]
by simp
qed
lemma rho_log_integrable: "integrable rho (λu. ln ¦x - u¦)"
proof -
have m: "(λu. ln ¦x - u¦) ∈ borel_measurable rho" unfolding rho_def
by simp
have m1: "(λu. ennreal ¦x - u¦) ∈ borel_measurable rho" unfolding rho_def
by simp
have m2: "(λu. ennreal (- ln ¦x - u¦)) ∈ borel_measurable rho"
unfolding rho_def
by simp
have s1: "(∫⇧+ u. ennreal (norm (ln ¦x - u¦)) ∂rho) ≤
(∫⇧+ u. ennreal ¦x - u¦ + ennreal (- ln ¦x -
u¦) ∂rho)"
using ennreal_abs_ln_le by (auto intro: nn_integral_mono)
have s2: "(∫⇧+ u. ennreal ¦x - u¦ + ennreal (- ln ¦x -
u¦) ∂rho) = (∫⇧+ u. ennreal ¦x - u¦ ∂rho) +
(∫⇧+ u. ennreal (- ln ¦x - u¦) ∂rho)"
by (rule nn_integral_add[OF m1 m2])
have a: "AE u in rho. ennreal ¦x - u¦ ≤ ennreal (¦x¦ + 2)"
using rho_AE_Ioo
by (fastforce intro: ennreal_leI elim: eventually_mono)
have s3: "(∫⇧+ u. ennreal ¦x - u¦ ∂rho) ≤
ennreal (¦x¦ + 2) * emeasure rho (space rho)"
using nn_integral_mono_AE[OF a] by simp
have f1: "emeasure rho (space rho) < ∞"
using finite_measure.emeasure_finite[OF rho_finite, of "space rho"]
by (simp add: less_top)
have b1: "(∫⇧+ u. ennreal (norm (ln ¦x - u¦)) ∂rho) ≤
ennreal (¦x¦ + 2) * emeasure rho (space rho) + ennreal 80"
using s1 s2 s3 rho_neg_log_le[of x] by (auto intro: add_mono order_trans)
have b2: "ennreal (¦x¦ + 2) * emeasure rho (space rho) + ennreal 80 < ∞"
using f1
by (simp add: ennreal_mult_less_top less_top)
have fin: "(∫⇧+ u. ennreal (norm (ln ¦x - u¦)) ∂rho) <
∞" by (rule le_less_trans[OF b1 b2])
show ?thesis using m fin unfolding integrable_iff_bounded
by simp
qed
lemma rho_logmax_integrable:
assumes e: "0 < ε"
shows "integrable rho (λu. ln (max ε ¦x - u¦))"
proof -
have m: "(λu. ln (max ε ¦x - u¦)) ∈ borel_measurable rho"
unfolding rho_def
by simp
have pt: "norm (ln (max ε ¦x - u¦)) ≤
¦ln ε¦ + (¦x¦ + 2)" if u: "0 < u ∧ u < 2" for u
proof -
have "¦ln (max ε ¦x - u¦)¦ ≤
¦ln ε¦ + ¦x - u¦" by (rule abs_ln_max_le[OF e abs_ge_zero])
thus ?thesis using u
by (smt (verit, del_insts) real_norm_def)
qed
have ae: "AE u in rho. norm (ln (max ε ¦x - u¦)) ≤
¦ln ε¦ + (¦x¦ + 2)" using rho_AE_Ioo pt
by (auto elim: eventually_mono)
show ?thesis using finite_measure.integrable_const_bound[OF rho_finite ae m] .
qed
lemma rho_logmax_le:
assumes e: "0 < ε"
shows "integral⇧L rho (λu. ln (max ε ¦x - u¦)) ≤
logPot rho x + 80 * sqrt ε"
proof -
define g where "g u = ln (max ε ¦x - u¦) - ln ¦x - u¦" for u
have i1: "integrable rho (λu. ln (max ε ¦x - u¦))"
by (rule rho_logmax_integrable[OF e])
have i2: "integrable rho (λu. ln ¦x - u¦)" by (rule rho_log_integrable)
have ig: "integrable rho g" unfolding g_def using i1 i2
by simp
have dif: "integral⇧L rho (λu. ln (max ε ¦x - u¦)) =
logPot rho x + integral⇧L rho g"
unfolding g_def logPot_def using Bochner_Integration.integral_diff[OF i1 i2]
by simp
have nul: "{x} ∈ null_sets rho" using rho_singleton[of x] unfolding rho_def
by auto
have ane: "AE u in rho. u ≠ x" using AE_I'[OF nul, of "λu. u ≠ x"]
by auto
have gpt: "g u = max 0 (ln (ε / ¦x - u¦))" if u: "u ≠ x" for u
proof -
have d0: "0 < ¦x - u¦" using u
by simp
have ld: "ln (ε / ¦x - u¦) = ln ε - ln ¦x - u¦" using d0 e
by (simp add: ln_div)
show ?thesis
proof (cases "ε ≤ ¦x - u¦")
case True
have "ln ε ≤ ln ¦x - u¦" using True e d0
by simp
thus ?thesis unfolding g_def ld using True
by (simp add: max_def)
next
case False
have "ln ¦x - u¦ < ln ε" using False e d0
by simp
thus ?thesis unfolding g_def ld using False
by (simp add: max_def)
qed
qed
have gnn: "AE u in rho. 0 ≤ g u" using ane gpt
by (auto elim: eventually_mono)
have nnI: "ennreal (integral⇧L rho g) =
(∫⇧+ u. ennreal (g u) ∂rho)"
using nn_integral_eq_integral[OF ig gnn]
by simp
have nnE: "(∫⇧+ u. ennreal (g u) ∂rho) =
(∫⇧+ u. ennreal (max 0 (ln (ε / ¦x - u¦))) ∂rho)"
using ane gpt by (auto intro: nn_integral_cong_AE elim: eventually_mono)
have "ennreal (integral⇧L rho g) ≤ ennreal (80 * sqrt ε)" unfolding nnI nnE
by (rule cross_bound[OF e])
hence b2: "integral⇧L rho g ≤ 80 * sqrt ε" using e
by (simp add: ennreal_le_iff)
show ?thesis unfolding dif using b2
by simp
qed
text ‹The energies of a scaled sum of circle measures.›
lemma csum_scale_integral:
fixes t :: "nat ⇒ real" and h :: nat and ε r :: real and f :: "complex
⇒ real"
assumes r: "0 ≤ r" and f: "f ∈ borel_measurable borel" and fi: "⋀i. i <
h ⟹ integrable (circ (of_real (t i)) ε) f"
shows "integral⇧L (scale_measure (ennreal r) (distr (count_space {..<h} ⨂⇩M
cden) borel (λ(i, θ). of_real (t i) + of_real ε * cis θ))) f
= r * (∑ i < h. integral⇧L (circ (of_real (t i)) ε) f)"
proof -
have fi': "⋀i. i ∈ {..<h} ⟹
integrable (circ (of_real (t i)) ε) f" using fi
by simp
have fD: "f ∈ borel_measurable (distr (count_space {..<h} ⨂⇩M cden) borel
(λ(i, θ). of_real (t i) + of_real ε * cis θ))" using f
by simp
show ?thesis using scale_integral(1)[OF r fD] csum_integral(2)[OF finite_lessThan f fi']
by simp
qed
lemma csum_energy_ge:
fixes t :: "nat ⇒ real" and h :: nat and ε r :: real and S :: "complex
measure"
assumes e: "0 < ε" and inj: "inj_on t {..<h}" and r: "0 ≤ r"
and S: "S = scale_measure (ennreal r) (distr (count_space {..<h} ⨂⇩M cden) borel
(λ(i, θ). of_real (t i) + of_real ε * cis θ))"
shows "r ^ 2 * (∑ i < h. ∑ j < h. (if i =
j then ln ε else ln ¦t i - t j¦)) ≤ logEnergyC S S"
proof -
define c :: "nat ⇒ complex" where "c i = of_real (t i)" for i
define Φ :: "complex ⇒ real" where "Φ z = (∑ j <
h. ln (max ε (norm (c j - z))))" for z
have SI: "⋀f. f ∈ borel_measurable borel ⟹
(⋀i. i < h ⟹ integrable (circ (c i) ε) f) ⟹
integral⇧L S f = r * (∑ i < h. integral⇧L (circ (c i) ε) f)"
unfolding S c_def using csum_scale_integral[OF r]
by simp
have inner: "⋀z. integral⇧L S (λw. ln (norm (z - w))) = r * Φ z"
proof -
fix z :: complex
have fe: "(λw. ln (norm (z - w))) = (λw. ln (norm (w - z)))"
by (simp add: norm_minus_commute)
have mf: "(λw :: complex. ln (norm (w - z))) ∈ borel_measurable borel"
by simp
have ii: "⋀i. i < h ⟹
integrable (circ (c i) ε) (λw. ln (norm (w - z)))"
by (rule circ_log_integrable[OF e])
have cl: "⋀j. integral⇧L (circ (c j) ε) (λw. ln (norm (w - z))) =
ln (max ε (norm (c j - z)))"
by (rule circ_log[OF e])
show "integral⇧L S (λw. ln (norm (z - w))) = r * Φ z"
unfolding fe Φ_def using SI[OF mf ii] cl
by simp
qed
have mΦj: "⋀j. (λz. ln (max ε (norm (c j - z)))) ∈
borel_measurable borel"
by simp
have mΦ: "Φ ∈ borel_measurable borel" unfolding Φ_def[abs_def] using mΦj
by simp
have iΦj: "⋀i j. integrable (circ (c i) ε) (λz. ln (max ε
(norm (c j - z))))"
proof -
fix i j
show "integrable (circ (c i) ε) (λz. ln (max ε (norm (c j - z))))"
proof (rule circ_integrable_bound[where B =
"¦ln ε¦ + (norm (c j) + norm (c i) + ¦ε¦)"])
show "(λz. ln (max ε (norm (c j - z)))) ∈ borel_measurable borel"
by (rule mΦj)
fix z :: complex assume hz: "norm (z - c i) = ¦ε¦"
have b: "¦ln (max ε (norm (c j - z)))¦ ≤
¦ln ε¦ + norm (c j - z)" by (rule abs_ln_max_le[OF e norm_ge_zero])
have nz: "norm (c j - z) ≤ norm (c j) + norm (c i) + ¦ε¦"
using hz norm_triangle_ineq4[of "c j" z] norm_triangle_sub[of z "c i"]
by simp
show "¦ln (max ε (norm (c j - z)))¦ ≤
¦ln ε¦ + (norm (c j) + norm (c i) + ¦ε¦)" using b nz
by simp
qed
qed
have iΦ: "⋀i. i < h ⟹ integrable (circ (c i) ε) Φ"
unfolding Φ_def using iΦj
by simp
have outer: "logEnergyC S S = r * (r * (∑ i <
h. integral⇧L (circ (c i) ε) Φ))"
unfolding logEnergyC_def inner using SI[OF mΦ iΦ]
by simp
have split: "⋀i. integral⇧L (circ (c i) ε) Φ = (∑ j <
h. integral⇧L (circ (c i) ε) (λz. ln (max ε (norm (c j - z)))))"
unfolding Φ_def using iΦj
by simp
have trm: "⋀i j. i < h ⟹ j < h ⟹
(if i = j then ln ε else ln ¦t i - t j¦) ≤
integral⇧L (circ (c i) ε) (λz. ln (max ε (norm (c j - z))))"
proof -
fix i j assume i: "i < h" and j: "j < h"
show "(if i = j then ln ε else ln ¦t i - t j¦) ≤
integral⇧L (circ (c i) ε) (λz. ln (max ε (norm (c j - z))))"
proof (cases "i = j")
case True
have ae: "AE z in circ (c i) ε. ln (max ε (norm (c j - z))) =
ln ε" using circ_AE[of "c i" ε] True e
by (auto simp: norm_minus_commute elim: eventually_mono)
have m1: "(λz. ln (max ε (norm (c j - z)))) ∈
borel_measurable (circ (c i) ε)"
using mΦj[of j] measurable_cong_sets[OF sets_circ refl]
by blast
have ic1: "integral⇧L (circ (c i) ε) (λz. ln (max ε (norm (c j
- z)))) = integral⇧L (circ (c i) ε) (λz. ln ε)"
using integral_cong_AE[OF m1 _ ae]
by simp
have ic2: "integral⇧L (circ (c i) ε) (λz. ln ε) =
ln ε" using circ_univ[of "c i" ε] space_circ[of "c i" ε]
by (simp add: measure_def)
show ?thesis using True ic1 ic2
by auto
next
case False
have "t i ≠ t j" using inj i j False unfolding inj_on_def
by auto
hence dpos: "0 < ¦t i - t j¦"
by simp
have cne: "norm (c i - c j) = ¦t i - t j¦" unfolding c_def
by (metis norm_of_real of_real_hom.hom_minus)
have nul: "{c j} ∈ null_sets (circ (c i) ε)"
using circ_singleton[OF e, of "c i" "c j"] sets_circ[of "c i" ε]
by auto
have ane: "AE z in circ (c i) ε. z ≠ c j"
using AE_I'[OF nul, of "λz. z ≠ c j"]
by auto
have pt: "⋀z. z ≠ c j ⟹
ln (norm (z - c j)) ≤ ln (max ε (norm (c j - z)))"
by (simp add: ln_mono norm_minus_commute)
have aele: "AE z in circ (c i) ε. ln (norm (z - c j)) ≤
ln (max ε (norm (c j - z)))" using ane pt
by (auto elim: eventually_mono)
have i1: "integrable (circ (c i) ε) (λz. ln (norm (z - c j)))"
by (rule circ_log_integrable[OF e])
have mono: "integral⇧L (circ (c i) ε) (λz. ln (norm (z - c j))) ≤
integral⇧L (circ (c i) ε) (λz. ln (max ε (norm (c j - z))))"
by (rule integral_mono_AE[OF i1 iΦj aele])
have cl: "integral⇧L (circ (c i) ε) (λz. ln (norm (z - c j))) =
ln (max ε (norm (c i - c j)))" by (rule circ_log[OF e])
have lm: "ln ¦t i - t j¦ ≤ ln (max ε (norm (c i - c j)))"
unfolding cne using dpos e
by simp
show ?thesis using False mono cl lm
by simp
qed
qed
have sumle: "(∑ i < h. ∑ j < h. (if i =
j then ln ε else ln ¦t i - t j¦)) ≤ (∑ i <
h. integral⇧L (circ (c i) ε) Φ)"
unfolding split using trm
by (auto intro: sum_mono)
show ?thesis unfolding outer using sumle r mult_left_mono[OF sumle, of "r * r"]
by (simp add: power2_eq_square mult.assoc)
qed
lemma csum_cross_le:
fixes t :: "nat ⇒ real" and h :: nat and ε r :: real and S :: "complex
measure"
assumes e: "0 < ε" and e1: "ε ≤ 1" and tnn: "⋀i. i <
h ⟹ 0 ≤ t i" and r: "0 ≤ r"
and S: "S = scale_measure (ennreal r) (distr (count_space {..<h} ⨂⇩M cden) borel
(λ(i, θ). of_real (t i) + of_real ε * cis θ))"
shows "logEnergyC S (distr rho borel of_real) ≤ r * (∑ i <
h. (logPot rho (t i) + 80 * sqrt ε))"
proof -
define c :: "nat ⇒ complex" where "c i = of_real (t i)" for i
define ρC :: "complex measure" where "ρC = distr rho borel of_real"
define F :: "complex ⇒ real" where "F z =
integral⇧L ρC (λw. ln (norm (z - w)))" for z
have SI: "⋀f. f ∈ borel_measurable borel ⟹
(⋀i. i < h ⟹ integrable (circ (c i) ε) f) ⟹
integral⇧L S f = r * (∑ i < h. integral⇧L (circ (c i) ε) f)"
unfolding S c_def using csum_scale_integral[OF r]
by simp
have fr: "finite_measure ρC" unfolding ρC_def by (rule rhoC_finite)
have sr: "sets ρC = sets borel" unfolding ρC_def by (rule sets_rhoC)
have sfr: "sigma_finite_measure ρC" using fr
by (simp add: finite_measure_def)
have mp0: "(λp :: complex × complex. ln (norm (fst p - snd p))) ∈
borel_measurable (borel ⨂⇩M borel)"
by simp
have sp: "sets ((borel :: complex measure) ⨂⇩M ρC) =
sets (borel ⨂⇩M borel)" using sr
using sets_pair_measure_cong by simp
have mp: "(λ(z, w). ln (norm (z - w))) ∈
borel_measurable ((borel :: complex measure) ⨂⇩M ρC)"
unfolding split_beta' using mp0 measurable_cong_sets[OF sp refl]
by blast
have mF: "F ∈ borel_measurable borel" unfolding F_def[abs_def]
using sigma_finite_measure.borel_measurable_lebesgue_integral[OF sfr mp] .
have aeR: "AE w in ρC. norm w ≤ 2" unfolding ρC_def by (rule rhoC_AE)
have lgR: "⋀z. (∫⇧+ w. ennreal (- ln (norm (z - w))) ∂ρC) ≤
ennreal 80" unfolding ρC_def by (rule rhoC_neg_log)
have bound: "integral⇧L (circ (c i) ε) F ≤
logPot rho (t i) + 80 * sqrt ε"
and iF: "integrable (circ (c i) ε) F" if i: "i < h" for i
proof -
have ci: "norm (c i) = t i" unfolding c_def using tnn[OF i]
by simp
have aeC: "AE z in circ (c i) ε. norm z ≤ t i + 3"
proof -
have pt: "norm z ≤ t i + 3" if hz: "norm (z - c i) = ¦ε¦" for z
using hz ci e e1 norm_triangle_sub[of z "c i"]
by simp
show ?thesis using circ_AE[of "c i" ε] pt
by (auto elim: eventually_mono)
qed
have aeR': "AE w in ρC. norm w ≤ t i + 3" using aeR tnn[OF i]
by (auto elim: eventually_mono)
have Pi: "integrable (circ (c i) ε ⨂⇩M ρC) (λp. ln (norm
(fst p - snd p)))"
by (rule integrable_log_prod[OF circ_finite fr sets_circ sr aeC aeR' lgR])
have Pi': "integrable (circ (c i) ε ⨂⇩M ρC) (λ(x,
y). ln (norm (x - y)))"
unfolding split_beta' by (rule Pi)
have ps: "pair_sigma_finite (circ (c i) ε) ρC"
using circ_finite[of "c i" ε] fr
unfolding pair_sigma_finite_def by (simp add: finite_measure_def)
show "integrable (circ (c i) ε) F" unfolding F_def[abs_def]
using pair_sigma_finite.integrable_fst[OF ps Pi'] .
have s1: "integral⇧L (circ (c i) ε) F =
integral⇧L (circ (c i) ε ⨂⇩M ρC) (λ(x,
y). ln (norm (x - y)))"
unfolding F_def[abs_def] using pair_sigma_finite.integral_fst[OF ps Pi'] .
have s2: "integral⇧L (circ (c i) ε ⨂⇩M ρC) (λ(x,
y). ln (norm (x - y))) = (∫ y. (∫ x. ln (norm (x -
y)) ∂circ (c i) ε) ∂ρC)"
using pair_sigma_finite.integral_snd[OF ps Pi'] by (rule sym)
have s3: "⋀y. (∫ x. ln (norm (x - y)) ∂circ (c i) ε) =
ln (max ε (norm (c i - y)))" by (rule circ_log[OF e])
have m4: "(λy :: complex. ln (max ε (norm (c i - y)))) ∈
borel_measurable borel"
by simp
have s4: "(∫ y. ln (max ε (norm (c i - y))) ∂ρC) =
(∫ u. ln (max ε (norm (c i - of_real u))) ∂rho)"
unfolding ρC_def by (rule integral_distr[OF rhoC_meas m4])
have s5: "⋀u. norm (c i - of_real u) = ¦t i - u¦" unfolding c_def
by (metis norm_of_real of_real_hom.hom_minus)
have eqF: "integral⇧L (circ (c i) ε) F =
(∫ u. ln (max ε ¦t i - u¦) ∂rho)"
unfolding s1 s2 s3 s4 s5 ..
show "integral⇧L (circ (c i) ε) F ≤ logPot rho (t i) + 80 * sqrt ε"
unfolding eqF by (rule rho_logmax_le[OF e])
qed
have outer: "logEnergyC S ρC = r * (∑ i <
h. integral⇧L (circ (c i) ε) F)"
unfolding logEnergyC_def F_def[symmetric] using SI[OF mF iF]
by simp
have sle: "(∑ i < h. integral⇧L (circ (c i) ε) F) ≤ (∑ i <
h. (logPot rho (t i) + 80 * sqrt ε))"
using bound by (blast intro: sum_mono)
show ?thesis unfolding ρC_def[symmetric] outer using mult_left_mono[OF sle r] .
qed
theorem configuration_bound:
fixes t :: "nat ⇒ real"
assumes "40 dvd K" "0 < K" "⋀i. i < hof K ⟹
0 ≤ t i" "inj_on t {..<hof K}"
shows "2 * (∑ i < hof K. ∑ j ∈ {j. i < j ∧
j < hof K}. ln ¦t i - t j¦)
- real K * (∑ i < hof K. Vf (t i)) + (∑ i < hof K. sqrt (t i))
≤ (lam_r * of_rat M0c - logEnergy rho) * real K ^ 2
+ (120 + sqrt 2) * real (hof K) + 2 * real (hof K) * ln (real K)"
proof -
define h where "h = hof K"
define ε where "ε = (1 / (2 * real K)) ^ 2"
have e0: "0 < ε" using assms(2) unfolding ε_def by simp
have sqe: "sqrt ε = 1 / (2 * real K)" unfolding ε_def using assms(2)
by simp
have lne: "ln ε = - 2 * ln 2 - 2 * ln (real K)" unfolding ε_def using assms(2)
by (simp add: ln_realpow ln_div ln_mult)
have hK: "real h = lam_r * real K" unfolding h_def using assms(1)
by (auto elim!: dvdE simp: hof_def lam_r_def)
text ‹The regularised configuration
@{text "σ = K^-^1 ∑_i ω(t_i, ε)"} as one push-forward measure,
and @{text "ρ"} on @{text ℂ}.›
define σ where "σ = scale_measure (ennreal (1 / real K))
(distr (count_space {..<h} ⨂⇩M density lborel (λθ. ennreal
(indicator {0..2 * pi} θ / (2 * pi)))) borel
(λ(i, θ). of_real (t i) + of_real ε * cis θ))"
define ρC :: "complex measure" where "ρC = distr rho borel of_real"
have sig_univ: "emeasure σ UNIV = ennreal (real h / real K)"
proof -
have D1: "emeasure (distr (count_space {..<h} ⨂⇩M density lborel
(λθ. ennreal (indicator {0..2 * pi} θ / (2 * pi)))) borel (λ(i,
θ). of_real (t i) + of_real ε * cis θ)) UNIV = of_nat h"
using csum_emeasure[where I = "{..<h}" and A = UNIV and c =
"λi. of_real (t i)" and ε = ε] circ_univ
by simp
show ?thesis unfolding σ_def using D1
by (simp add: ennreal_of_nat_eq_real_of_nat ennreal_mult'["symmetric"])
qed
have rhoC_univ: "emeasure ρC UNIV = ennreal lam_r"
proof -
have m: "(of_real :: real ⇒ complex) ∈ measurable rho borel" unfolding rho_def
by simp
have sp: "space rho = UNIV" unfolding rho_def
by simp
show ?thesis unfolding ρC_def using emeasure_distr[OF m, of UNIV] sp rho_univ
by simp
qed
have mass: "emeasure σ UNIV = emeasure ρC UNIV" unfolding sig_univ rhoC_univ hK
using assms(2) by simp
have inj': "inj_on t {..<h}" using assms(4) unfolding h_def .
have k0: "0 ≤ 1 / real K"
by simp
have energy_sig_ge: "(1 / real K ^ 2) * ((∑ i < h. ∑ j < h. (if i =
j then ln ε else ln ¦t i - t j¦))) ≤ logEnergyC σ σ"
using csum_energy_ge[OF e0 inj' k0 σ_def] by (simp add: power_divide)
have e1c: "ε ≤ 1" unfolding ε_def using assms(2)
by (simp add: power_le_one)
have tnnc: "⋀i. i < h ⟹ 0 ≤ t i" using assms(3) unfolding h_def
by simp
have energy_cross_le: "logEnergyC σ ρC ≤ (1 / real K) * (∑ i <
h. (logPot rho (t i) + 80 * sqrt ε))"
unfolding ρC_def by (rule csum_cross_le[OF e0 e1c tnnc k0 σ_def])
have energy_rhoC: "logEnergyC ρC ρC = logEnergy rho"
proof -
have inner: "⋀z. integral⇧L ρC (λw. ln (norm (z - w))) =
integral⇧L rho (λu. ln (norm (z - of_real u)))"
unfolding ρC_def using integral_distr[OF rhoC_meas] by force
have sfr: "sigma_finite_measure rho" using rho_finite
by (simp add: finite_measure_def)
have mp0: "(λp :: complex × real. ln (norm (fst p - of_real (snd p)))) ∈
borel_measurable (borel ⨂⇩M borel)"
by simp
have sp: "sets ((borel :: complex measure) ⨂⇩M rho) =
sets (borel ⨂⇩M borel)" unfolding rho_def
using sets_pair_measure_cong by simp
have mp: "(λ(z, u). ln (norm (z - of_real u))) ∈
borel_measurable ((borel :: complex measure) ⨂⇩M rho)"
unfolding split_beta' using mp0 measurable_cong_sets[OF sp refl] by blast
have mG: "(λz :: complex. integral⇧L rho (λu. ln (norm (z -
of_real u)))) ∈ borel_measurable borel"
using sigma_finite_measure.borel_measurable_lebesgue_integral[OF sfr mp] .
have outer: "integral⇧L ρC (λz. integral⇧L rho (λu. ln (norm (z
- of_real u)))) = integral⇧L rho (λx. integral⇧L rho (λu. ln (norm
(of_real x - of_real u :: complex))))"
unfolding ρC_def by (rule integral_distr[OF rhoC_meas mG])
have pt: "⋀x u :: real. ln (norm (of_real x - of_real u :: complex)) =
ln ¦x - u¦"
by (metis norm_of_real of_real_hom.hom_minus)
show ?thesis unfolding logEnergyC_def logEnergy_def logPot_def inner outer pt ..
qed
text ‹The dominating measure @{text "η = σ + ρC"}
for Lemma 6.2 (Isabelle has no sum of measures: use @{text "sup_measure'"} or an explicit
@{text measure_of}).›
define η :: "complex measure" where "η =
measure_of UNIV (sets borel) (λA. emeasure σ A + emeasure ρC A)"
have sets_sig: "sets σ = sets borel"
unfolding σ_def by simp
have sets_rho: "sets ρC = sets borel"
unfolding ρC_def by simp
have sets_eta: "sets η = sets borel"
unfolding η_def by (rule summ_sets)
have em_eta: "⋀A. A ∈ sets borel ⟹
emeasure η A = emeasure σ A + emeasure ρC A"
unfolding η_def using summ_emeasure[OF sets_sig sets_rho] by simp
have fin: "finite_measure η"
using em_eta[of UNIV] sig_univ rhoC_univ sets_eta sets_eq_imp_space_eq[OF sets_eta]
by (auto intro: finite_measureI)
have le1: "σ ≤ η"
using le_measure[of σ η] sets_sig sets_eta em_eta by simp
have le2: "ρC ≤ η"
using le_measure[of ρC η] sets_rho sets_eta em_eta by simp
have nn_sum: "⋀f. f ∈ borel_measurable borel ⟹
(∫⇧+ z. f z ∂η) ≤
(∫⇧+ z. f z ∂σ) +
(∫⇧+ z. f z ∂ρC)"
unfolding η_def using summ_nn[OF sets_sig sets_rho] by simp
have int_eta: "integrable (η ⨂⇩M η) (λzw. ln (norm (fst zw -
snd zw)))"
proof -
define R0 :: real where "R0 = (∑ i < h. t i) + 3"
have tnn: "⋀i. i < h ⟹ 0 ≤ t i" using assms(3) unfolding h_def
by simp
have tle: "⋀i. i < h ⟹ t i ≤ (∑ j < h. t j)" using tnn
by (auto intro: member_le_sum)
have e1: "ε ≤ 1" unfolding ε_def using assms(2)
by (simp add: power_le_one)
have R3: "3 ≤ R0" unfolding R0_def using tnn
by (auto intro: sum_nonneg)
have cR: "⋀i. i < h ⟹
norm (of_real (t i) :: complex) + ε ≤ R0" unfolding R0_def using tle tnn e1
by force
have lne0: "ln ε ≤ 0" using e0 e1
by simp
define B where "B = 2 * R0 - ln ε"
have B0: "0 ≤ B" unfolding B_def using R3 lne0
by simp
define N where "N = {z :: complex. R0 < norm z}"
have Nm: "N ∈ sets borel" unfolding N_def
by (auto intro: borel_open open_Collect_less continuous_intros)
have cN: "⋀i. i < h ⟹ emeasure (circ (of_real (t i)) ε) N = 0"
proof -
fix i assume i: "i < h"
have pt: "z ∉ N" if hz: "norm (z - of_real (t i)) = ¦ε¦" for z
using hz cR[OF i] e0 norm_triangle_sub[of z "of_real (t i)"] unfolding N_def
by simp
have ae: "AE z in circ (of_real (t i)) ε. z ∉ N"
using circ_AE[of "of_real (t i)" ε] pt
by (auto elim: eventually_mono)
show "emeasure (circ (of_real (t i)) ε) N = 0"
using AE_iff_measurable[of N "circ (of_real (t i)) ε" "λz. z ∉ N"]
ae Nm sets_circ space_circ
by simp
qed
have sN: "emeasure σ N = 0" unfolding σ_def
using csum_emeasure[where I = "{..<h}" and A = N and c =
"λi. of_real (t i)" and ε = ε] Nm cN
by simp
have rN: "emeasure ρC N = 0"
proof -
have ae: "AE w in ρC. w ∉ N" using rhoC_AE R3 unfolding ρC_def N_def
by (auto elim: eventually_mono)
show ?thesis using AE_iff_measurable[of N ρC "λz. z ∉ N"] ae Nm sets_rho
sets_eq_imp_space_eq[OF sets_rho]
by simp
qed
have eN: "emeasure η N = 0" using em_eta[OF Nm] sN rN
by simp
have aeη: "AE z in η. norm z ≤ R0"
using AE_iff_measurable[of N η "λz. norm z ≤
R0"] Nm sets_eta sets_eq_imp_space_eq[OF sets_eta] eN unfolding N_def
by force
have lg: "⋀z. norm z ≤ R0 ⟹
(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂η) ≤
ennreal (real h / real K * B + 80)"
proof -
fix z :: complex assume hz: "norm z ≤ R0"
have mf: "(λw. ennreal (- ln (norm (z - w)))) ∈ borel_measurable borel"
by simp
have mfD: "(λw. ennreal (- ln (norm (z - w)))) ∈
borel_measurable (distr (count_space {..<h} ⨂⇩M density lborel
(λθ. ennreal (indicator {0..2 * pi} θ / (2 *
pi)))) borel (λ(i, θ). of_real (t i) + of_real ε * cis θ))"
using mf
by simp
have a1: "(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂η) ≤
(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂σ) +
(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂ρC)"
by (rule nn_sum[OF mf])
have a2: "(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂σ) =
ennreal (1 / real K) * (∑ i <
h. ∫⇧+ w. ennreal (- ln (norm (z -
w))) ∂circ (of_real (t i)) ε)"
unfolding σ_def using nn_integral_scale_measure[OF mfD] csum_nn[OF finite_lessThan
mf]
by simp
have a3: "(∑ i < h. ∫⇧+ w. ennreal (- ln (norm (z -
w))) ∂circ (of_real (t i)) ε) ≤ (∑ i < h. ennreal B)"
using circ_neg_log[OF e0 cR hz] unfolding B_def
by (blast intro: sum_mono)
have a4: "(∑ i < h. ennreal B) = ennreal (real h * B)" using B0
by (simp add: ennreal_of_nat_eq_real_of_nat ennreal_mult)
have a5: "ennreal (1 / real K) * ennreal (real h * B) = ennreal (real h / real K * B)"
using B0
by (simp add: ennreal_mult["symmetric"])
have a6: "(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂ρC) ≤
ennreal 80" unfolding ρC_def by (rule rhoC_neg_log)
have a7: "ennreal (real h / real K * B) + ennreal 80 = ennreal (real h / real K * B + 80)"
using B0
by (simp add: ennreal_plus)
have "(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂η) ≤
(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂σ) +
(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂ρC)"
by (rule a1)
also have "… ≤ ennreal (1 / real K) * (∑ i < h. ennreal B) + ennreal 80"
unfolding a2 using a3 a6
by (force intro: add_mono mult_left_mono)
also have "… = ennreal (real h / real K * B + 80)" unfolding a4 a5 a7 ..
finally show "(∫⇧+ w. ennreal (- ln (norm (z - w))) ∂η) ≤
ennreal (real h / real K * B + 80)" .
qed
show ?thesis by (rule integrable_log_prod[OF fin fin sets_eta sets_eta aeη aeη lg])
qed
have diag: "emeasure (η ⨂⇩M η) {zw. fst zw = snd zw} = 0"
proof -
have sfe: "sigma_finite_measure η" using fin
by (simp add: finite_measure_def)
have Dm0: "{zw :: complex × complex. fst zw = snd zw} ∈
sets (borel ⨂⇩M borel)"
proof -
have mf: "(λp :: complex × complex. fst p - snd p) ∈
borel_measurable (borel ⨂⇩M borel)"
by simp
have eq: "{p :: complex × complex. fst p = snd p} =
(λp. fst p - snd p) -` {0} ∩ space (borel ⨂⇩M borel)"
by (auto simp: space_pair_measure)
show ?thesis unfolding eq using measurable_sets[OF mf, of "{0}"]
by simp
qed
have Dm: "{zw :: complex × complex. fst zw = snd zw} ∈
sets (η ⨂⇩M η)" using Dm0 sets_pair_measure_cong[OF sets_eta sets_eta]
by simp
have e1: "emeasure (η ⨂⇩M η) {zw. fst zw = snd zw} =
(∫⇧+ z. ∫⇧+ w. indicator {zw :: complex ×
complex. fst zw = snd zw} (z, w) ∂η ∂η)"
by (rule sigma_finite_measure.emeasure_pair_measure[OF sfe Dm])
have sz: "⋀z. emeasure σ {z} = 0"
proof -
fix z :: complex
have "emeasure σ {z} = ennreal (1 / real K) * (∑ i <
h. emeasure (circ (of_real (t i)) ε) {z})" unfolding σ_def
using csum_emeasure[where I = "{..<h}" and A = "{z}" and c =
"λi. of_real (t i)" and ε = ε] by simp
thus "emeasure σ {z} = 0" using circ_singleton[OF e0]
by simp
qed
have rz: "⋀z. emeasure ρC {z} = 0" unfolding ρC_def by (rule rhoC_singleton)
have pt: "⋀z. (∫⇧+ w. indicator {zw :: complex × complex. fst zw =
snd zw} (z, w) ∂η) = 0"
proof -
fix z :: complex
have ind: "(λw. indicator {zw :: complex × complex. fst zw =
snd zw} (z, w) :: ennreal) = indicator {z}"
by (simp add: fun_eq_iff indicator_def)
show "(∫⇧+ w. indicator {zw :: complex × complex. fst zw =
snd zw} (z, w) ∂η) = 0" unfolding ind using em_eta[of "{z}"] sz rz sets_eta
by simp
qed
show ?thesis unfolding e1 pt
by simp
qed
have eta: "finite_measure η" "sets η = sets borel" "σ ≤
η" "ρC ≤ η"
"integrable (η ⨂⇩M η) (λzw. ln (norm (fst zw -
snd zw)))" "emeasure (η ⨂⇩M η) {zw. fst zw = snd zw} = 0"
by fact+
have L62: "logEnergyC σ σ - 2 * logEnergyC σ ρC +
logEnergyC ρC ρC ≤ 0"
by (rule log_energy_zero_mass_nonpos[OF eta(1) _ _ eta(2) eta(3,4) mass eta(5,6)]) (simp_all
add: σ_def ρC_def)
have fb: "⋀i. i < h ⟹
2 * logPot rho (t i) - Vf (t i) + sqrt (t i) / real K ≤ of_rat M0c + sqrt 2 / real K"
proof -
fix i assume i: "i < h"
have K40: "40 ≤ real K" using assms(1,2)
by (auto elim: dvdE)
have t0: "0 ≤ t i" using assms(3) i unfolding h_def
by simp
show "2 * logPot rho (t i) - Vf (t i) + sqrt (t i) / real K ≤ of_rat M0c + sqrt 2 / real K"
using field_bound[OF K40 t0]
by simp
qed
have pair: "(∑ i < h. ∑ j < h. (if i =
j then ln ε else ln ¦t i - t j¦)) = 2 * (∑ i < h. ∑ j ∈ {j. i <
j ∧ j < h}. ln ¦t i - t j¦) + real h * ln ε"
proof -
define L where "L i j = ln ¦t i - t j¦" for i j
have sym: "L i j = L j i" for i j unfolding L_def
by (simp add: abs_minus_commute)
have row: "(∑ j < h. (if i = j then ln ε else L i j)) =
ln ε + (∑ j ∈ {j. i < j ∧
j < h}. L i j) + (∑ j ∈ {j. j < i}. L i j)" if i: "i < h" for i
proof -
have r1: "(∑ j < h. (if i = j then ln ε else L i j)) =
ln ε + (∑ j ∈ {..<h} - {i}. L i j)" using i
by (simp add: sum.remove if_distrib sum.If_cases)
have r2: "{..<h} - {i} = {j. i < j ∧ j < h} ∪ {j. j < i}" using i
by auto
have r3: "(∑ j ∈ {j. i < j ∧
j < h} ∪ {j. j < i}. L i j) = (∑ j ∈ {j. i < j ∧
j < h}. L i j) + (∑ j ∈ {j. j < i}. L i j)"
by (auto intro: sum.union_disjoint)
show ?thesis unfolding r1 r2 r3
by simp
qed
have rows: "(∑ i < h. ∑ j < h. (if i = j then ln ε else L i j)) =
real h * ln ε + (∑ i < h. ∑ j ∈ {j. i < j ∧
j < h}. L i j) + (∑ i < h. ∑ j ∈ {j. j < i}. L i j)"
using row
by (simp add: sum.distrib)
have sw1: "(∑ i < h. ∑ j ∈ {j. j < i}. L i j) = (∑ i < h. ∑ j ∈
{j. j ∈ {..<h} ∧ j < i}. L i j)"
by (force intro: sum.cong)
have sw2: "(∑ i < h. ∑ j ∈ {j. j ∈ {..<h} ∧
j < i}. L i j) = (∑ j < h. ∑ i ∈ {i. i ∈ {..<h} ∧ j < i}. L i j)"
using sum.swap_restrict[of "{..<h}" "{..<h}" L "λi j. j < i"]
by simp
have sw3: "(∑ j < h. ∑ i ∈ {i. i ∈ {..<h} ∧
j < i}. L i j) = (∑ i < h. ∑ j ∈ {j. i < j ∧ j < h}. L i j)"
using sym by (auto simp: conj_commute intro: sum.cong)
show ?thesis using rows sw1 sw2 sw3 unfolding L_def
by linarith
qed
define S2 where "S2 = (∑ i < h. ∑ j ∈ {j. i < j ∧
j < h}. ln ¦t i - t j¦)"
define A where "A = (∑ i < h. logPot rho (t i))"
define Vs where "Vs = (∑ i < h. Vf (t i))"
define Ss where "Ss = (∑ i < h. sqrt (t i))"
define I where "I = logEnergy rho"
define κ where "κ = real K"
have k0: "0 < κ" unfolding κ_def using assms(2)
by simp
have "(∑ i < h. 2 * logPot rho (t i) - Vf (t i) + sqrt (t i) / real K) ≤ (∑ i <
h. of_rat M0c + sqrt 2 / real K)"
using fb
by (blast intro: sum_mono)
hence fbs: "2 * A - Vs + Ss / κ ≤ real h * (of_rat M0c + sqrt 2 / κ)"
unfolding A_def Vs_def Ss_def κ_def
by (simp add: sum.distrib sum_subtractf sum_distrib_left sum_divide_distrib)
have fbK: "2 * A * κ - Vs * κ + Ss ≤
real h * of_rat M0c * κ + real h * sqrt 2"
proof -
have "(2 * A - Vs + Ss / κ) * κ ≤
real h * (of_rat M0c + sqrt 2 / κ) * κ" using fbs k0
by (simp add: mult_right_mono)
thus ?thesis using k0
by (simp add: algebra_simps)
qed
have cs: "(∑ i < h. (logPot rho (t i) + 80 * sqrt ε)) =
A + real h * (40 / κ)" unfolding A_def sqe κ_def
by (simp add: sum.distrib)
have ec: "logEnergyC σ ρC ≤ (A + real h * (40 / κ)) / κ"
using energy_cross_le unfolding cs κ_def
by simp
have "(2 * S2 + real h * ln ε) / κ ^ 2 ≤ logEnergyC σ σ"
using energy_sig_ge unfolding pair S2_def κ_def
by (simp add: power2_eq_square)
hence comb: "(2 * S2 + real h * ln ε) / κ ^ 2 ≤
2 * ((A + real h * (40 / κ)) / κ) - I"
using ec L62 energy_rhoC unfolding I_def
by linarith
have combK: "2 * S2 + real h * ln ε ≤
2 * A * κ + 80 * real h - I * κ ^ 2"
proof -
have m: "(2 * S2 + real h * ln ε) / κ ^ 2 * κ ^ 2 ≤
(2 * ((A + real h * (40 / κ)) / κ) - I) * κ ^ 2"
using mult_right_mono[OF comb, of "κ ^ 2"] k0 by simp
have e1: "(2 * S2 + real h * ln ε) / κ ^ 2 * κ ^ 2 =
2 * S2 + real h * ln ε" using k0
by simp
have e2: "(2 * ((A + real h * (40 / κ)) / κ) - I) * κ ^ 2 =
2 * A * κ + 80 * real h - I * κ ^ 2"
using k0 by (simp add: power2_eq_square algebra_simps)
show ?thesis using m e1 e2
by simp
qed
have hl: "real h * ln ε = - 2 * real h * ln 2 - 2 * real h * ln κ"
unfolding lne κ_def by (simp add: algebra_simps)
have l2: "real h * ln 2 ≤ real h" using mult_left_le[of "ln 2" "real h"] ln_2_less_1
by simp
have hM: "real h * of_rat M0c * κ = lam_r * of_rat M0c * κ ^ 2"
unfolding hK κ_def
by (simp add: power2_eq_square)
have fin: "2 * S2 - κ * Vs + Ss ≤
(lam_r * of_rat M0c - I) * κ ^ 2 + (120 + sqrt 2) * real h + 2 * real h * ln κ"
proof -
have r: "(lam_r * of_rat M0c - I) * κ ^ 2 + (120 + sqrt 2) * real h + 2 * real h *
ln κ = lam_r * of_rat M0c * κ ^ 2 - I * κ ^ 2 + 120 * real h + real h *
sqrt 2 + 2 * real h * ln κ"
by (simp add: algebra_simps)
have v: "κ * Vs = Vs * κ"
by simp
have h0: "0 ≤ real h"
by simp
show ?thesis unfolding r v using fbK combK hl l2 hM h0
by simp
qed
show ?thesis using fin unfolding S2_def Vs_def Ss_def I_def κ_def h_def .
qed
subsection ‹(6.14), (6.15) and Proposition 6.3›
text ‹@{text "∫_0^∞ (1+y)^5 e^{-y/κ} dy ≤ 3872 κ^6"}
(Lean: @{text "phi_bound"}).›
lemma phi_aux:
fixes κ :: real
assumes "1 ≤ κ"
shows "set_integrable lborel {0<..} (λy. (1 + y) ^ 5 * exp (- y / κ))"
and "set_lebesgue_integral lborel {0<..} (λy. (1 + y) ^ 5 * exp (- y / κ)) ≤
3872 * κ ^ 6"
proof -
have k0: "0 < κ" using assms
by simp
have c0: "0 < 1 / κ" using k0
by simp
define g0 :: "real ⇒ real" where "g0 y = y ^ 0 * exp (- ((1 / κ) * y))" for y
define g5 :: "real ⇒ real" where "g5 y = y ^ 5 * exp (- ((1 / κ) * y))" for y
define ψ :: "real ⇒ real" where "ψ y = 32 * g0 y + 32 * g5 y" for y
have i0: "set_integrable lborel {0<..} g0" unfolding g0_def using gam_integrable[OF c0, of 0]
by simp
have i5: "set_integrable lborel {0<..} g5" unfolding g5_def using gam_integrable[OF c0, of 5]
by simp
have v0: "set_lebesgue_integral lborel {0<..} g0 = κ" unfolding g0_def
using gam[OF c0, of 0] k0
by simp
have v5: "set_lebesgue_integral lborel {0<..} g5 = 120 * κ ^ 6" unfolding g5_def
using gam[OF c0, of 5] k0
by (simp add: fact_numeral power_one_over)
have ipsi: "set_integrable lborel {0<..} ψ" unfolding ψ_def using i0 i5
by simp
have vpsi: "set_lebesgue_integral lborel {0<..} ψ = 32 * κ + 3840 * κ ^ 6"
unfolding ψ_def using i0 i5 v0 v5
by simp
have p5: "(1 + y) ^ 5 ≤ 32 * (1 + y ^ 5)" if y: "0 ≤ y" for y :: real
proof (cases "y ≤ 1")
case True
have "(1 + y) ^ 5 ≤ (2 :: real) ^ 5" using power_mono[of "1 + y" 2 5] True y
by simp
moreover have "(2 :: real) ^ 5 = 32"
by simp
moreover have "0 ≤ y ^ 5" using y
by simp
ultimately show ?thesis
by argo
next
case False
have "(1 + y) ^ 5 ≤ (2 * y) ^ 5" using power_mono[of "1 + y" "2 * y" 5] False y
by simp
also have "… = 32 * y ^ 5"
by (simp add: power_mult_distrib)
finally show ?thesis
by simp
qed
have bound: "(1 + y) ^ 5 * exp (- y / κ) ≤ ψ y" if y: "0 < y" for y
proof -
have e: "exp (- y / κ) = exp (- ((1 / κ) * y))"
by simp
have "(1 + y) ^ 5 * exp (- y / κ) ≤ 32 * (1 + y ^ 5) * exp (- y / κ)"
using p5[of y] y
by simp
also have "… = ψ y" unfolding ψ_def g0_def g5_def e
by (simp add: algebra_simps)
finally show ?thesis .
qed
have meas: "set_borel_measurable lborel {0<..} (λy. (1 + y) ^ 5 * exp (- y / κ))"
unfolding set_borel_measurable_def by simp
have nn: "0 ≤ (1 + y) ^ 5 * exp (- y / κ)" if "0 < y" for y :: real using that
by simp
have AE: "AE y in lborel. y ∈ {0<..} ⟶
norm ((1 + y) ^ 5 * exp (- y / κ)) ≤ norm (ψ y)"
using bound nn
by (force simp: AE_I2)
show I: "set_integrable lborel {0<..} (λy. (1 + y) ^ 5 * exp (- y / κ))"
using set_integrable_bound[OF ipsi meas AE] .
have k6: "κ ^ 1 ≤ κ ^ 6" using power_increasing[of 1 6 κ] assms
by simp
have "set_lebesgue_integral lborel {0<..} (λy. (1 + y) ^ 5 * exp (- y / κ)) ≤
set_lebesgue_integral lborel {0<..} ψ"
using set_integral_mono[OF I ipsi] bound
by simp
also have "… ≤ 3872 * κ ^ 6" unfolding vpsi using k6
by simp
finally show "set_lebesgue_integral lborel {0<..} (λy. (1 + y) ^ 5 * exp (- y /
κ)) ≤ 3872 * κ ^ 6" .
qed
text ‹(6.14): @{text "log Δ_K(ζ(5)) ≤
2h(h + 6N - K) log K + (λM_0 - I(ρ))K^2 + 18h log K + 160h"}.›
theorem log_DeltaK_zeta5_bound:
assumes "40 dvd K" "0 < K"
shows "ln (real_eval (DeltaK K) zeta5) ≤
2 * real (hof K) * (real (hof K) + 6 * real (Nof K) - real K) * ln (real K)
+ (lam_r * of_rat M0c - logEnergy rho) * real K ^ 2
+ 18 * real (hof K) * ln (real K) + 160 * real (hof K)"
proof -
define h where "h = hof K"
define N where "N = Nof K"
define E where "E = (lam_r * of_rat M0c - logEnergy rho) * real K ^ 2 + (120 + sqrt 2) * real h +
2 * real h * ln (real K)"
define c0 where "c0 = 8192 * exp 12 * real K ^ (12 * N + 12) / real K ^ (2 * K)"
have hN: "1 ≤ N" "N ≤ K" "real N / real K = 3 / 40" "0 < h"
proof -
obtain k where k: "K = 40 * k" using assms(1)
by auto
have k1: "1 ≤ k" using assms(2) k
by simp
have Nk: "N = 3 * k" unfolding N_def Nof_def k
by simp
have hk: "h = 37 * k" unfolding h_def hof_def k
by simp
show "1 ≤ N" using Nk k1
by simp
show "N ≤ K" using Nk k
by simp
show "real N / real K = 3 / 40" using Nk k k1
by simp
show "0 < h" using hk k1
by simp
qed
text ‹Pointwise bound of the Andreief integrand (@{text "g_le"} and (6.9) with
@{text "t_i = (y_i/K)^2"}).›
have pointwise: "⋀y. (∀i<h. 0 < y i) ⟹
(∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y i ^ 2 - y j ^ 2) ^ 2) * (∏ i <
h. real_eval (Dm N) (y i ^ 2) ^ 6 / real_eval (Dm K) (y i ^ 2) * weight (y i))
≤ (real K ^ 4) ^ (h * (h - 1) div 2) * c0 ^ h * exp E * (∏ i <
h. (1 + y i) ^ 5 * exp (- y i / real K))"
proof -
fix y :: "nat ⇒ real" assume ypos: "∀i<h. 0 < y i"
have k0: "0 < real K" using assms(2)
by simp
define t where "t i = (y i / real K) ^ 2" for i
define Q where "Q = (∏ i < h. (1 + y i) ^ 5 * exp (- y i / real K))"
have Q0: "0 ≤ Q" unfolding Q_def using ypos
by (fastforce intro: prod_nonneg)
have c00: "0 ≤ c0" unfolding c0_def
by simp
have R0: "0 ≤ (real K ^ 4) ^ (h * (h - 1) div 2) * c0 ^ h * exp E * Q" using Q0 c00
by simp
have hyt: "y i ^ 2 = real K ^ 2 * t i" for i unfolding t_def using k0
by (simp add: power_divide)
have Dpos: "0 < real_eval (Dm m) (u ^ 2)" for m u
proof -
have D: "Dm m = sqPoleProd {1..m}"
by (simp add: Dm_def sqPoleProd_def)
show ?thesis unfolding D
by (auto intro: real_eval_sqPoleProd_pos)
qed
have g0: "0 ≤ real_eval (Dm N) (u ^ 2) ^ 6 / real_eval (Dm K) (u ^ 2) * weight u"
if "0 < u" for u
using Dpos[of N u] Dpos[of K u] weight_pos[OF that]
by (simp add: divide_nonneg_pos)
show "(∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y i ^ 2 - y j ^ 2) ^ 2) * (∏ i <
h. real_eval (Dm N) (y i ^ 2) ^ 6 / real_eval (Dm K) (y i ^ 2) * weight (y i))
≤ (real K ^ 4) ^ (h * (h - 1) div 2) * c0 ^ h * exp E * (∏ i <
h. (1 + y i) ^ 5 * exp (- y i / real K))"
proof (cases "inj_on t {..<h}")
case False
obtain i j where ij: "i < h" "j < h" "t i = t j" "i ≠ j" using False
unfolding inj_on_def
by auto
obtain a b where ab: "a < b" "b < h" "t a = t b"
proof (cases "i < j")
case True
show ?thesis using that[of i j] True ij
by simp
next
case False
show ?thesis using that[of j i] False ij
by simp
qed
have "(y a ^ 2 - y b ^ 2) ^ 2 = 0" using hyt[of a] hyt[of b] ab(3)
by (simp add: hyt)
hence "(∏ j ∈ {j. a < j ∧ j < h}. (y a ^ 2 - y j ^ 2) ^ 2) = 0" using ab
by (auto simp: prod_zero_iff)
hence Z: "(∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y i ^ 2 - y j ^ 2) ^ 2) = 0" using ab
by (auto simp: prod_zero_iff)
show ?thesis unfolding Z using R0 unfolding Q_def
by (simp add: zero_le_mult_iff)
next
case True
define L where "L i j = ln ¦t i - t j¦" for i j
have hfac: "(y i ^ 2 - y j ^ 2) ^ 2 = real K ^ 4 * exp (2 * L i j)" if ij: "i < j" "j < h"
for i j
proof -
have ne: "t i ≠ t j" using True ij unfolding inj_on_def
by auto
have l: "2 * ln ¦t i - t j¦ = ln (¦t i - t j¦ ^ 2)"
using ln_realpow[of "¦t i - t j¦" 2]
by simp
have e: "exp (2 * L i j) = (t i - t j) ^ 2" unfolding L_def l using ne
by simp
have d: "real K ^ 2 * t i - real K ^ 2 * t j = real K ^ 2 * (t i - t j)"
by (simp add: algebra_simps)
show ?thesis unfolding e hyt d
by (simp add: power_mult_distrib)
qed
have card: "(∑ i<h. card {j. i < j ∧ j < h}) = h * (h - 1) div 2"
proof -
have c1: "card {j. i < j ∧ j < h} = h - Suc i" for i
proof -
have "{j. i < j ∧ j < h} = {Suc i..<h}"
by auto
thus ?thesis
by simp
qed
have "(∑ i<h. card {j. i < j ∧ j < h}) = (∑ i<h. h - Suc i)" unfolding c1 ..
also have "… = (∑ i<h. i)" using sum.nat_diff_reindex[of "λi. i" h]
by simp
also have "… = h * (h - 1) div 2"
by (simp add: Sum_Ico_nat atLeast0LessThan[symmetric])
finally show ?thesis .
qed
have hV: "(∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y i ^ 2 - y j ^ 2) ^ 2) = (real K ^ 4) ^ (h * (h - 1) div 2) * exp (2 * (∑ i <
h. ∑ j ∈ {j. i < j ∧ j < h}. L i j))"
proof -
have "(∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y i ^ 2 - y j ^ 2) ^ 2) = (∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. real K ^ 4 * exp (2 * L i j))"
using hfac
by simp
also have "… = (∏ i < h. (real K ^ 4) ^ card {j. i < j ∧
j < h} * exp (2 * (∑ j ∈ {j. i < j ∧ j < h}. L i j)))"
by (simp add: prod.distrib exp_sum sum_distrib_left)
also have "… = (real K ^ 4) ^ (∑ i<h. card {j. i < j ∧
j < h}) * exp (2 * (∑ i < h. ∑ j ∈ {j. i < j ∧ j < h}. L i j))"
by (simp add: power_sum exp_sum sum_distrib_left)
finally show ?thesis unfolding card .
qed
have hG: "(∏ i < h. real_eval (Dm N) (y i ^ 2) ^ 6 / real_eval (Dm K) (y i ^ 2) *
weight (y i)) ≤ (∏ i < h. c0 * ((1 + y i) ^ 5 * exp (- real K * Vf (t i))))"
proof (rule prod_mono)
fix i assume "i ∈ {..<h}"
hence yi: "0 < y i" using ypos
by simp
show "0 ≤ real_eval (Dm N) (y i ^ 2) ^ 6 / real_eval (Dm K) (y i ^ 2) *
weight (y i) ∧ real_eval (Dm N) (y i ^ 2) ^ 6 / real_eval (Dm K) (y i ^ 2) *
weight (y i) ≤ c0 * ((1 + y i) ^ 5 * exp (- real K * Vf (t i)))"
using g0[OF yi] g_le[OF hN(1,2,3) yi] unfolding t_def c0_def by simp
qed
have hG': "(∏ i < h. c0 * ((1 + y i) ^ 5 * exp (- real K * Vf (t i)))) =
c0 ^ h * (∏ i < h. (1 + y i) ^ 5) * exp (- real K * (∑ i < h. Vf (t i)))"
by (simp add: prod.distrib exp_sum sum_distrib_left)
have sq: "sqrt (t i) = y i / real K" if "i < h" for i unfolding t_def using ypos that k0
by auto
have tnn: "0 ≤ t i" for i unfolding t_def
by simp
have hc0: "2 * (∑ i < h. ∑ j ∈ {j. i < j ∧
j < h}. L i j) - real K * (∑ i < h. Vf (t i)) + (∑ i < h. sqrt (t i)) ≤ E"
using configuration_bound[OF assms(1,2), of t] unfolding h_def[symmetric] E_def L_def
using True tnn
by simp
have ss: "(∑ i < h. sqrt (t i)) = (∑ i < h. y i / real K)" using sq
by simp
have "2 * (∑ i < h. ∑ j ∈ {j. i < j ∧
j < h}. L i j) - real K * (∑ i < h. Vf (t i)) + (∑ i < h. y i / real K) ≤ E"
using hc0 ss
by simp
hence hexp: "exp (2 * (∑ i < h. ∑ j ∈ {j. i < j ∧
j < h}. L i j)) * exp (- real K * (∑ i < h. Vf (t i))) ≤ exp E * exp (- (∑ i <
h. y i / real K))"
unfolding mult_exp_exp by simp
have ex: "exp (- (∑ i < h. y i / real K)) = (∏ i < h. exp (- y i / real K))"
by (simp add: exp_sum[symmetric] sum_negf[symmetric])
have Qe: "Q = (∏ i < h. (1 + y i) ^ 5) * exp (- (∑ i < h. y i / real K))"
unfolding Q_def ex
by (simp add: prod.distrib)
have pp: "0 ≤ (∏ i < h. (1 + y i) ^ 5)" using ypos
by (force intro: prod_nonneg)
have Vn: "0 ≤ (real K ^ 4) ^ (h * (h - 1) div 2) * exp (2 * (∑ i < h. ∑ j ∈
{j. i < j ∧ j < h}. L i j))"
by simp
have P0: "0 ≤ (real K ^ 4) ^ (h * (h - 1) div 2) * c0 ^ h * (∏ i <
h. (1 + y i) ^ 5)" using c00 pp
by simp
have "(∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y i ^ 2 - y j ^ 2) ^ 2) * (∏ i <
h. real_eval (Dm N) (y i ^ 2) ^ 6 / real_eval (Dm K) (y i ^ 2) * weight (y i)) =
(real K ^ 4) ^ (h * (h - 1) div 2) * exp (2 * (∑ i < h. ∑ j ∈ {j. i < j ∧
j < h}. L i j)) * (∏ i < h. real_eval (Dm N) (y i ^ 2) ^ 6 /
real_eval (Dm K) (y i ^ 2) * weight (y i))"
unfolding hV ..
also have "… ≤ (real K ^ 4) ^ (h * (h - 1) div 2) * exp (2 * (∑ i <
h. ∑ j ∈ {j. i < j ∧
j < h}. L i j)) * (c0 ^ h * (∏ i < h. (1 + y i) ^ 5) * exp (- real K * (∑ i <
h. Vf (t i))))"
using mult_left_mono[OF hG[unfolded hG'] Vn] by simp
also have "… = (real K ^ 4) ^ (h * (h - 1) div 2) * c0 ^ h * (∏ i <
h. (1 + y i) ^ 5) * (exp (2 * (∑ i < h. ∑ j ∈ {j. i < j ∧
j < h}. L i j)) * exp (- real K * (∑ i < h. Vf (t i))))"
by (simp add: algebra_simps)
also have "… ≤ (real K ^ 4) ^ (h * (h - 1) div 2) * c0 ^ h * (∏ i <
h. (1 + y i) ^ 5) * (exp E * exp (- (∑ i < h. y i / real K)))"
using hexp P0
by (simp add: mult_left_mono)
also have "… = (real K ^ 4) ^ (h * (h - 1) div 2) * c0 ^ h * exp E * Q" unfolding Qe
by (simp add: algebra_simps)
finally show ?thesis unfolding Q_def .
qed
qed
have phi_bound: "set_lebesgue_integral lborel {0<..} (λy. (1 + y) ^ 5 * exp (- y /
real K)) ≤ 3872 * real K ^ 6"
using phi_aux(2)[of "real K"] assms(2) by simp
have A: "real_eval (DeltaK K) zeta5 = 1 / fact h *
set_lebesgue_integral (PiM {..<h} (λ_. lborel)) {y. ∀i<h. 0 < y i}
(λy. (∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y i ^ 2 - y j ^ 2) ^ 2) * (∏ i <
h. real_eval (Dm N) (y i ^ 2) ^ 6 / real_eval (Dm K) (y i ^ 2) * weight (y i)))"
unfolding h_def N_def by (rule DeltaK_zeta5_integral[OF assms(1)])
have B: "set_lebesgue_integral (PiM {..<h} (λ_. lborel)) {y. ∀i<h. 0 < y i}
(λy. (∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y i ^ 2 - y j ^ 2) ^ 2) * (∏ i <
h. real_eval (Dm N) (y i ^ 2) ^ 6 / real_eval (Dm K) (y i ^ 2) * weight (y i)))
≤ (real K ^ 4) ^ (h * (h - 1) div 2) * c0 ^ h * exp E * (3872 * real K ^ 6) ^ h"
proof -
define φ :: "real ⇒ real" where "φ y = (1 + y) ^ 5 * exp (- y / real K)"
for y
define ψ :: "real ⇒ real" where "ψ y = indicator {0<..} y * φ y"
for y
define C :: real where "C = (real K ^ 4) ^ (h * (h - 1) div 2) * c0 ^ h * exp E"
have c00: "0 ≤ c0" unfolding c0_def
by simp
have C0: "0 ≤ C" unfolding C_def using c00
by simp
have "set_integrable lborel {0<..} φ" unfolding φ_def
using phi_aux(1)[of "real K"] assms(2)
by simp
hence psi_int: "integrable lborel ψ" unfolding set_integrable_def ψ_def
by simp
have psi_eq: "integral⇧L lborel ψ = set_lebesgue_integral lborel {0<..} φ"
unfolding set_lebesgue_integral_def ψ_def
by simp
have psi_nn: "0 ≤ ψ y" for y unfolding ψ_def φ_def
by (simp add: indicator_def)
have int_nn: "0 ≤ integral⇧L lborel ψ" using psi_nn
by (simp add: integral_nonneg)
have int_le: "integral⇧L lborel ψ ≤ 3872 * real K ^ 6"
unfolding psi_eq φ_def using phi_bound
by simp
interpret PS: product_sigma_finite "λ_::nat. lborel :: real measure"
by (auto intro: product_sigma_finite.intro sigma_finite_lborel)
have prodint: "integrable (PiM {..<h} (λ_. lborel)) (λy. ∏ i<h. ψ (y
i))" using psi_int PS.product_integrable_prod[of "{..<h}" "λ_. ψ"]
by simp
have prodeq: "integral⇧L (PiM {..<h} (λ_. lborel)) (λy. ∏ i<h.
ψ (y i)) = integral⇧L lborel ψ ^ h"
using psi_int PS.product_integral_prod[of "{..<h}" "λ_. ψ"]
by simp
have intmaj: "integrable (PiM {..<h} (λ_. lborel)) (λy. C *
(∏ i<h. ψ (y i)))" using prodint
by simp
have nn: "0 ≤ C * (∏ i<h. ψ (y i))" for y using C0 psi_nn
by (simp add: prod_nonneg)
have maj: "indicator {y. ∀i<h. 0 < y i} y *⇩R ((∏ i < h. ∏ j ∈
{j. i < j ∧ j < h}. (y i ^ 2 - y j ^ 2) ^ 2) * (∏ i <
h. real_eval (Dm N) (y i ^ 2) ^ 6 / real_eval (Dm K) (y i ^ 2) * weight (y i))) ≤
C * (∏ i<h. ψ (y i))" for y
proof (cases "∀i<h. 0 < y i")
case True
have ps: "(∏ i<h. ψ (y i)) = (∏ i<h. (1 + y i) ^ 5 * exp (- y i / real K))"
using True unfolding ψ_def φ_def
by simp
show ?thesis unfolding ps C_def using pointwise[OF True] True
by simp
next
case False
show ?thesis using False nn[of y]
by simp
qed
have "set_lebesgue_integral (PiM {..<h} (λ_. lborel)) {y. ∀i<h. 0 <
y i} (λy. ((∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y i ^ 2 - y j ^ 2) ^ 2) * (∏ i <
h. real_eval (Dm N) (y i ^ 2) ^ 6 / real_eval (Dm K) (y i ^ 2) * weight (y i))))
≤ integral⇧L (PiM {..<h} (λ_. lborel)) (λy. C *
(∏ i<h. ψ (y i)))"
unfolding set_lebesgue_integral_def using integral_mono'[OF intmaj maj nn]
by simp
also have "… = C * integral⇧L lborel ψ ^ h" using prodeq
by simp
also have "… ≤ C * (3872 * real K ^ 6) ^ h" using int_nn int_le C0
by (meson mult_left_mono power_mono)
finally show ?thesis unfolding C_def .
qed
have pos: "0 < real_eval (DeltaK K) zeta5" by (rule Delta_zeta5_pos)
have fact1: "1 / fact h ≤ (1 :: real)"
by (simp add: divide_le_eq_1)
define I where "I = set_lebesgue_integral (PiM {..<h} (λ_. lborel)) {y. ∀i<h. 0 <
y i}
(λy. (∏ i < h. ∏ j ∈ {j. i < j ∧
j < h}. (y i ^ 2 - y j ^ 2) ^ 2) * (∏ i <
h. real_eval (Dm N) (y i ^ 2) ^ 6 / real_eval (Dm K) (y i ^ 2) * weight (y i)))"
define LK :: real where "LK = ln (real K)"
define P where "P = h * (h - 1) div 2"
define R where "R = (real K ^ 4) ^ P * c0 ^ h * exp E * (3872 * real K ^ 6) ^ h"
have A': "real_eval (DeltaK K) zeta5 = 1 / fact h * I" using A unfolding I_def .
have B': "I ≤ R" using B unfolding I_def R_def P_def .
have K1: "1 ≤ real K" using assms(2)
by simp
have c0pos: "0 < c0" unfolding c0_def using K1
by simp
have I00: "0 < 1 / fact h * I" using pos unfolding A'
by simp
have I0: "0 < I" using zero_less_mult_pos[OF I00]
by simp
have DI: "1 / fact h * I ≤ I" using mult_right_mono[OF fact1, of I] I0
by simp
have lnR: "ln (real_eval (DeltaK K) zeta5) ≤ ln R" using A' DI B' pos
by simp
have lnR_eq: "ln R = real P * (4 * LK) + real h * ln c0 + E + real h * (ln 3872 + 6 * LK)"
unfolding R_def LK_def using assms(2) c0pos
by (simp add: ln_mult ln_realpow distrib_left)
have p8192: "(8192 :: real) = 2 ^ 13"
by simp
have l8192: "ln (8192 :: real) = 13 * ln 2"
unfolding p8192 ln_realpow by simp
have lnc0: "ln c0 = 13 * ln 2 + 12 + real (12 * N + 12) * LK - real (2 * K) * LK"
unfolding c0_def LK_def using assms(2) l8192
by (simp add: ln_div ln_mult ln_realpow)
have ev: "even (h * (h - 1))"
by auto
have "P * 2 = h * (h - 1)" unfolding P_def using ev
by simp
moreover have "real (h * (h - 1)) = real h * real h - real h" using hN(4)
by (simp add: of_nat_diff algebra_simps)
ultimately have hP: "real P * 2 = real h * real h - real h"
by linarith
have e4: "real P * (4 * LK) = 2 * (real h * real h - real h) * LK"
by (simp add: hP[symmetric])
have l2: "ln 2 < (1::real)"
by (simp add: ln_2_less_1)
have p4096: "(4096 :: real) = 2 ^ 12"
by simp
have "ln 3872 ≤ ln (4096::real)"
by simp
moreover have "ln (4096::real) = 12 * ln 2"
unfolding p4096 ln_realpow by simp
ultimately have l3872: "ln 3872 ≤ 12 * ln (2::real)"
by simp
have s2: "sqrt 2 ≤ (3 / 2 :: real)" using real_le_lsqrt[where x = 2 and y = "3 / 2"]
by (simp add: power2_eq_square)
have key: "(2 * real h * (real h + 6 * real N - real K) * LK + (lam_r * of_rat M0c -
logEnergy rho) * real K ^ 2 + 18 * real h * LK + 160 * real h)
- (real P * (4 * LK) + real h * ln c0 + E + real h * (ln 3872 + 6 * LK)) =
real h * (28 - 13 * ln 2 - sqrt 2 - ln 3872)"
unfolding e4 lnc0 E_def unfolding LK_def[symmetric]
by (simp add: algebra_simps)
have nonneg: "0 ≤ real h * (28 - 13 * ln 2 - sqrt 2 - ln 3872)" using l2 l3872 s2
by simp
have "ln (real_eval (DeltaK K) zeta5) ≤
2 * real h * (real h + 6 * real N - real K) * LK + (lam_r * of_rat M0c - logEnergy rho) *
real K ^ 2 + 18 * real h * LK + 160 * real h"
using lnR lnR_eq key nonneg
by simp
thus ?thesis unfolding h_def N_def LK_def .
qed
text ‹(6.15): @{text "log S_K ≤
(2λ - 12αλ - 2λ^2)K^2 log K + C*K^2 + 6h log K + 6h"}
(factorial bounds; @{text "Stirling_Formula.ln_fact_bounds"} is available).›
theorem log_SK_bound:
assumes "40 dvd K" "0 < K"
shows "ln (of_rat (SK K)) ≤
(2 * lam_r - 12 * alpha_r * lam_r - 2 * lam_r ^ 2) * real K ^ 2 * ln (real K)
+ Cstar * real K ^ 2 + 6 * real (hof K) * ln (real K) + 6 * real (hof K)"
proof -
obtain n where K: "K = 40 * n" and n1: "1 ≤ n" using assms by (auto elim: dvdE)
have hh: "hof K = 37 * n" and hN: "Nof K = 3 * n" unfolding K hof_def Nof_def by simp_all
have ln_fact_le: "⋀m. 1 ≤ m ⟹
ln (fact m) ≤ real m * ln (real m) - real m + ln (real m) + 2"
proof -
fix m :: nat assume "1 ≤ m"
thus "ln (fact m) ≤ real m * ln (real m) - real m + ln (real m) + 2"
proof (induction m rule: nat_induct_at_least)
case base
show ?case
by simp
next
case (Suc m)
define A :: real where "A = ln (real m)"
define B :: real where "B = ln (real (Suc m))"
have m1: "1 ≤ real m" using Suc.hyps
by simp
have IH: "ln (fact m) ≤ real m * A - real m + A + 2" using Suc.IH unfolding A_def .
have d1: "ln (real m / real (Suc m)) ≤ real m / real (Suc m) - 1"
using m1 ln_le_minus_one[of "real m / real (Suc m)"]
by simp
have d2: "ln (real m / real (Suc m)) = A - B" using m1 unfolding A_def B_def
by (simp add: ln_div)
have d3: "real m / real (Suc m) - 1 = - 1 / real (Suc m)" using m1
by (simp add: field_simps)
have d4a: "A - B ≤ - 1 / real (Suc m)" using d1 d2 d3
by simp
have d4: "real (Suc m) * (A - B) ≤ - 1" using mult_left_mono[OF d4a, of "real (Suc m)"] m1
by simp
have f: "ln (fact (Suc m)) = B + ln (fact m)" unfolding B_def
by (simp add: fact_Suc ln_mult)
have e: "real (Suc m) * (A - B) = real m * A + A - real (Suc m) * B"
by (simp add: algebra_simps)
have s: "real (Suc m) = real m + 1"
by simp
have g: "ln (fact (Suc m)) ≤ real (Suc m) * B - real (Suc m) + B + 2" using e f d4 IH s
by simp
show ?case using g unfolding B_def .
qed
qed
have le_ln_fact: "⋀m. 1 ≤ m ⟹
real m * ln (real m) - real m + 1 ≤ ln (fact m)"
proof -
fix m :: nat assume "1 ≤ m"
thus "real m * ln (real m) - real m + 1 ≤ ln (fact m)"
proof (induction m rule: nat_induct_at_least)
case base
show ?case
by auto
next
case (Suc m)
define A :: real where "A = ln (real m)"
define B :: real where "B = ln (real (Suc m))"
have m1: "1 ≤ real m" using Suc.hyps
by simp
have IH: "real m * A - real m + 1 ≤ ln (fact m)" using Suc.IH unfolding A_def .
have d1: "ln (real (Suc m) / real m) ≤ real (Suc m) / real m - 1"
using m1 ln_le_minus_one[of "real (Suc m) / real m"]
by simp
have d2: "ln (real (Suc m) / real m) = B - A" using m1 unfolding A_def B_def
by (simp add: ln_div)
have d3: "real (Suc m) / real m - 1 = 1 / real m" using m1
by (simp add: field_simps)
have d4a: "B - A ≤ 1 / real m" using d1 d2 d3
by simp
have d4: "real m * (B - A) ≤ 1" using mult_left_mono[OF d4a, of "real m"] m1
by simp
have f: "ln (fact (Suc m)) = B + ln (fact m)" unfolding B_def
by (simp add: fact_Suc ln_mult)
have e: "real (Suc m) * B - real (Suc m) + 1 = real m * (B - A) + real m * A + B - real m"
by (simp add: algebra_simps)
have g: "real (Suc m) * B - real (Suc m) + 1 ≤ ln (fact (Suc m))" using e f d4 IH
by simp
show ?case using g unfolding B_def .
qed
qed
have sum_ln_fact_ge: "⋀h. 1 ≤ h ⟹
real h ^ 2 * ln (2 * real h) - 3 * real h ^ 2 / 2 - 2 * real h * ln (2 * real h) ≤
(∑ i = 1..h - 1. ln (fact (2 * i)))"
proof -
fix h :: nat assume "1 ≤ h"
thus "real h ^ 2 * ln (2 * real h) - 3 * real h ^ 2 / 2 - 2 * real h * ln (2 * real h) ≤
(∑ i = 1..h - 1. ln (fact (2 * i)))"
proof (induction h rule: nat_induct_at_least)
case base
have l2: "0 ≤ ln (2::real)"
by simp
have b1: "(real 1)⇧2 * ln (2 * real 1) - 3 * (real 1)⇧2 / 2 - 2 * real 1 * ln (2 *
real 1) = - ln (2::real) - 3 / 2"
by simp
have b2: "(∑ i = 1..1 - 1. ln (fact (2 * i))) = (0::real)" by simp
show ?case unfolding b1 b2 using l2 by linarith
next
case (Suc h)
define A :: real where "A = ln (2 * real h)"
define B :: real where "B = ln (2 * real (Suc h))"
have h1: "1 ≤ real h" using Suc.hyps
by simp
have IH: "real h ^ 2 * A - 3 * real h ^ 2 / 2 - 2 * real h * A ≤ (∑ i =
1..h - 1. ln (fact (2 * i)))"
using Suc.IH unfolding A_def .
have hf: "2 * real h * A - 2 * real h + 1 ≤ ln (fact (2 * h))"
using le_ln_fact[of "2 * h"] Suc.hyps unfolding A_def
by simp
have d1: "ln ((2 * real (Suc h)) / (2 * real h)) ≤ (2 * real (Suc h)) / (2 * real h) - 1"
using h1 ln_le_minus_one[of "(2 * real (Suc h)) / (2 * real h)"] by simp
have d2: "ln ((2 * real (Suc h)) / (2 * real h)) = B - A" using h1 unfolding A_def B_def
by (simp add: ln_div)
have d3: "(2 * real (Suc h)) / (2 * real h) - 1 = 1 / real h" using h1
by (simp add: field_simps)
have d4a: "B - A ≤ 1 / real h" using d1 d2 d3
by simp
have d4: "real h * (B - A) ≤ 1" using mult_left_mono[OF d4a, of "real h"] h1
by simp
have d6: "0 ≤ B" unfolding B_def
by simp
have hh: "real h * (real h * (B - A)) ≤ real h" using d4 h1
by (simp add: mult_left_mono)
obtain k where k: "h = Suc k" using not0_implies_Suc[of h] Suc.hyps
by auto
have split: "(∑ i = 1..Suc h - 1. ln (fact (2 * i))) = (∑ i =
1..h - 1. ln (fact (2 * i))) + ln (fact (2 * h))"
unfolding k
by simp
have e: "real (Suc h) ^ 2 * B - 3 * real (Suc h) ^ 2 / 2 - 2 * real (Suc h) * B
= real h * (real h * (B - A)) + real h ^ 2 * A - B - 3 * real h ^ 2 / 2 - 3 * real h - 3 /
2"
by (simp add: algebra_simps power2_eq_square)
have g: "real (Suc h) ^ 2 * B - 3 * real (Suc h) ^ 2 / 2 - 2 * real (Suc h) * B ≤
(∑ i = 1..Suc h - 1. ln (fact (2 * i)))"
unfolding e split
proof -
show "real h * (real h * (B - A)) + real h ^ 2 * A - B - 3 * real h ^ 2 / 2 - 3 * real h -
3 / 2 ≤ (∑ i = 1..h - 1. ln (fact (2 * i))) + ln (fact (2 * h))"
using IH hf hh d6 by simp
qed
show ?case using g unfolding B_def .
qed
qed
have SK: "ln (of_rat (SK K)) = 2 * real (hof K) * ln (fact K) + real (hof K - 1) * ln 4 - 12 *
real (hof K) * ln (fact (Nof K)) - 2 * (∑ i = 1..hof K - 1. ln (fact (2 * i)))"
proof -
have fr: "(of_rat (fact m) :: real) = fact m" for m using of_rat_of_nat_eq[of "fact m"] by simp
have q: "(of_rat (SK K) :: real) = (fact K ^ (2 * hof K) * 4 ^ (hof K - 1)) /
(fact (Nof K) ^ (12 * hof K) * (∏ i = 1..hof K - 1. fact (2 * i) ^ 2))"
unfolding SK_def by (simp add: of_rat_divide of_rat_mult of_rat_power of_rat_prod fr)
have pos: "0 < (∏ i = 1..hof K - 1. (fact (2 * i) :: real) ^ 2)" by (simp add: prod_pos)
have "ln (of_rat (SK K)) = ln ((fact K :: real) ^ (2 * hof K)) + ln ((4 :: real) ^ (hof K -
1)) - ln ((fact (Nof K) :: real) ^ (12 * hof K)) - ln (∏ i =
1..hof K - 1. (fact (2 * i) :: real) ^ 2)"
unfolding q using pos by (simp add: ln_div ln_mult)
also have "ln (∏ i = 1..hof K - 1. (fact (2 * i) :: real) ^ 2) = 2 * (∑ i =
1..hof K - 1. ln (fact (2 * i)))"
by (simp add: ln_prod ln_realpow sum_distrib_left)
finally show ?thesis by (simp add: ln_realpow)
qed
define x :: real where "x = real n"
define L :: real where "L = ln (40 * x)"
define F40 :: real where "F40 = ln (fact (40 * n))"
define F3 :: real where "F3 = ln (fact (3 * n))"
define S :: real where "S = (∑ i = 1..37 * n - 1. ln (fact (2 * i)))"
define a :: real where "a = ln (3 / 40)"
define b :: real where "b = ln (37 / 20)"
define l4 :: real where "l4 = ln 4"
have x1: "1 ≤ x" using n1 unfolding x_def by simp
have eN: "ln (3 * x) = a + L" using x1 ln_mult_pos[of "3 / 40" "40 * x"] unfolding a_def L_def
by simp
have eh: "ln (2 * (37 * x)) = b + L" using x1 ln_mult_pos[of "37 / 20" "40 * x"]
unfolding b_def L_def by simp
have hA: "F40 ≤ 40 * x * L - 40 * x + L + 2" using ln_fact_le[of "40 * n"] n1
unfolding F40_def L_def x_def by simp
have hB: "3 * x * (a + L) - 3 * x + 1 ≤ F3" using le_ln_fact[of "3 * n"] n1 eN
unfolding F3_def x_def by simp
have hC: "(37 * x) ^ 2 * (b + L) - 3 * (37 * x) ^ 2 / 2 - 2 * (37 * x) * (b + L) ≤ S"
using sum_ln_fact_ge[of "37 * n"] n1 eh unfolding S_def x_def L_def by simp
have l4u: "l4 ≤ 3" using ln_le_minus_one[of "4 :: real"] unfolding l4_def by simp
have l4l: "0 ≤ l4" unfolding l4_def by simp
have bu: "b ≤ 1" using ln_le_minus_one[of "37 / 20 :: real"] unfolding b_def by simp
have ca: "Cstar = - 2 * (37 / 40) + 12 * (3 / 40) * (37 / 40) * (1 - a) + 3 * (37 / 40) ^ 2 - 2 *
(37 / 40) ^ 2 * b"
unfolding Cstar_def lam_r_def alpha_r_def a_def b_def by simp
have key: "((2 * lam_r - 12 * alpha_r * lam_r - 2 * lam_r ^ 2) * (40 * x) ^ 2 * L + Cstar * (40 *
x) ^ 2 + 6 * (37 * x) * L + 6 * (37 * x))
- (2 * (37 * x) * F40 + (37 * x - 1) * l4 - 12 * (37 * x) * F3 - 2 * S)
= 74 * x * (40 * x * L - 40 * x + L + 2 - F40) + 444 * x * (F3 - (3 * x * (a + L) - 3 * x +
1))
+ 2 * (S - ((37 * x) ^ 2 * (b + L) - 3 * (37 * x) ^ 2 / 2 - 2 * (37 * x) * (b + L))) + (x *
(518 - 37 * l4 - 148 * b) + l4)"
unfolding ca lam_r_def alpha_r_def by (simp add: field_simps power2_eq_square)
have nn1: "0 ≤ 74 * x * (40 * x * L - 40 * x + L + 2 - F40)" using hA x1 by simp
have nn2: "0 ≤ 444 * x * (F3 - (3 * x * (a + L) - 3 * x + 1))" using hB x1 by simp
have nn3: "0 ≤ x * (518 - 37 * l4 - 148 * b)" using l4l l4u bu x1 by simp
have main: "2 * (37 * x) * F40 + (37 * x - 1) * l4 - 12 * (37 * x) * F3 - 2 * S ≤
(2 * lam_r - 12 * alpha_r * lam_r - 2 * lam_r ^ 2) * (40 * x) ^ 2 * L + Cstar * (40 * x) ^ 2 +
6 * (37 * x) * L + 6 * (37 * x)"
using key nn1 nn2 nn3 hC l4l by simp
have sub: "real (37 * n - 1) = 37 * x - 1"
using n1 unfolding x_def by simp
show ?thesis
unfolding SK unfolding hh hN unfolding K
using main sub by (simp add: x_def L_def F40_def F3_def S_def l4_def)
qed
text ‹Proposition 6.3 is at the end of this theory (it needs (6.4) from Appendix A).›
lemma real_eval_FK_eq: "real_eval (FK K) zeta5 = of_rat (SK K) * real_eval (DeltaK K) zeta5"
by (simp add: FK_def real_eval_def map_poly_smult of_rat_mult)
text ‹Proposition 6.3: @{text "0 < F_K(ζ(5))"} and
@{text "log F_K(ζ(5)) ≤ UbarK^2 + 24K log K + 200K"}.
(Needs (6.4) from Appendix A, which is therefore imported.)›
theorem log_FK_zeta5_bound:
assumes "40 dvd K" "0 < K"
shows "0 < real_eval (FK K) zeta5 ∧
ln (real_eval (FK K) zeta5) ≤
of_rat Ubar * real K ^ 2 + 24 * real K * ln (real K) + 200 * real K"
proof -
have S0: "0 < (of_rat (SK K) :: real)" using SK_pos[of K] by simp
have D0: "0 < real_eval (DeltaK K) zeta5" by (rule Delta_zeta5_pos)
have pos: "0 < real_eval (FK K) zeta5" unfolding real_eval_FK_eq using S0 D0 by simp
obtain k where k: "K = 40 * k" using assms(1) by (elim dvdE)
have hk: "real (hof K) = 37 * real k" and Nk: "real (Nof K) = 3 * real k" and Kk: "real K =
40 * real k"
unfolding k hof_def Nof_def by simp_all
define LK where "LK = ln (real K)"
have LK0: "0 ≤ LK" using assms(2) by (simp add: LK_def)
have hK: "real (hof K) ≤ real K" using hk Kk by simp
define A where "A = 2 * real (hof K) * (real (hof K) + 6 * real (Nof K) - real K) * LK"
define B where "B = (2 * lam_r - 12 * alpha_r * lam_r - 2 * lam_r ^ 2) * real K ^ 2 * LK"
have AB: "A + B = 0" unfolding A_def B_def hk Nk Kk
by (simp add: lam_r_def alpha_r_def power2_eq_square algebra_simps)
have L: "ln (real_eval (FK K) zeta5) = ln (of_rat (SK K)) + ln (real_eval (DeltaK K) zeta5)"
unfolding real_eval_FK_eq using S0 D0 by (simp add: ln_mult)
have "ln (real_eval (FK K) zeta5)
≤ (A + (lam_r * of_rat M0c - logEnergy rho) * real K ^ 2 + 18 * real (hof K) * LK + 160 *
real (hof K))
+ (B + Cstar * real K ^ 2 + 6 * real (hof K) * LK + 6 * real (hof K))"
unfolding L A_def B_def LK_def using log_DeltaK_zeta5_bound[OF assms] log_SK_bound[OF assms]
by linarith
also have "… = (A + B) + (lam_r * of_rat M0c - logEnergy rho + Cstar) * real K ^ 2
+ 24 * (real (hof K) * LK) + 166 * real (hof K)"
by (simp add: algebra_simps)
also have "… ≤ of_rat Ubar * real K ^ 2 + 24 * (real K * LK) + 200 * real K"
proof -
have e: "(lam_r * of_rat M0c - logEnergy rho + Cstar) * real K ^ 2 ≤
of_rat Ubar * real K ^ 2"
by (rule mult_right_mono[OF rho_energy_bound]) simp
have l: "real (hof K) * LK ≤ real K * LK" by (rule mult_right_mono[OF hK LK0])
have h: "166 * real (hof K) ≤ 200 * real K" using hK by simp
show ?thesis unfolding AB using e l h by linarith
qed
finally show ?thesis using pos by (simp add: LK_def mult.assoc)
qed
end