Theory Log_Sine_Integral
theory Log_Sine_Integral
imports Interval_Integral_Substitutions "HOL-Complex_Analysis.Complex_Analysis"
begin
section ‹The log-sine integral and circle averages of ‹ln |z - a|››
text ‹Jordan's inequality ‹sin θ ≥
2θ/π› on ‹[0, π/2]›,
integrability of ‹ln› near ‹0›, the classical
‹∫⇩0⇧π ln (sin θ) dθ =
-π ln 2›, and the circle average ‹∫⇩0⇧2⇧π ln
|e⇧i⇧θ - a| dθ = 2π ln (max 1 |a|)›
for every complex ‹a›, including the singular case ‹|a| = 1›; the same
for the normalised
arclength measure @{text circ} on a circle of radius ‹ε› about
‹c›. This is the layer of
Jensen's formula that HOL-Complex\_Analysis lacks.›
text ‹Jordan's inequality @{text "sin θ ≥ 2θ/π"} on
@{text "[0, π/2]"}: @{text "sin"} is concave there
(@{text "sin'' = - sin ≤ 0"}) and the chord through @{text "(0, 0)"} and
@{text "(π/2, 1)"} lies below it.›
lemma sin_ge_two_over_pi:
assumes "0 ≤ θ" "θ ≤ pi / 2"
shows "2 * θ / pi ≤ sin θ"
proof -
have c1: "convex {0..pi / 2 :: real}"
by blast
have c2: "⋀x. DERIV sin x :> cos x"
by (blast intro: DERIV_sin)
have c3: "⋀x. DERIV cos x :> - sin x"
by (fast intro: DERIV_cos)
have c4: "⋀x. x ∈ {0..pi / 2} ⟹ - sin x ≤ 0"
using sin_ge_zero by simp
have conc: "concave_on {0..pi / 2} sin"
using f''_le0_imp_concave[OF c1 c2 c3 c4] by fastforce
show ?thesis
using concave_onD_Icc'[OF conc, of θ] assms
by (simp add: field_simps)
qed
text ‹@{text "ln"} is integrable near @{text 0}:
@{text "∫_0^c (- ln u) du = c - c ln c < ∞"}.›
lemma ln_integrable_near_zero:
assumes "0 < c"
shows "set_integrable lborel {0<..<c} (λu :: real. ln u)"
proof -
define F where "F u = u * ln c - u * ln u + u" for u :: real
define f where "f u = ln c - ln u" for u :: real
have D: "DERIV F x :> f x" if "0 < x" for x
unfolding F_def[abs_def] f_def using that
by (intro derivative_eq_intros) auto
have contf: "isCont f x" if "0 < x" for x
unfolding f_def using that
by (fastforce intro: continuous_intros)
have nonneg: "AE x in lborel. ereal 0 < ereal x ⟶
ereal x < ereal c ⟶ 0 ≤ f x"
unfolding f_def
by fastforce
have lim0: "((F ∘ real_of_ereal) ⤏ 0) (at_right (ereal 0))"
unfolding ereal_tendsto_simps F_def
by real_asymp
have limc: "((F ∘ real_of_ereal) ⤏ F c) (at_left (ereal c))"
unfolding ereal_tendsto_simps F_def using assms
by (fast intro: tendsto_intros)
note FTC = interval_integral_FTC_nonneg[of "ereal 0" "ereal c" F f, OF _ _ _ nonneg lim0 limc]
have "set_integrable lborel {0<..<c} (λu :: real. ln c)"
using interval_integral_const(1)[of 0 c "ln c"] assms
unfolding interval_lebesgue_integrable_def
by auto
moreover have "set_integrable lborel {0<..<c} f"
using FTC(1) assms D contf
by auto
ultimately have "set_integrable lborel {0<..<c} (λu. ln c - f u)"
by (rule set_integral_diff(1))
thus ?thesis unfolding f_def
by simp
qed
text ‹The classical @{text "∫_0^π log sin θ dθ = -π log 2"};
first the integrability.›
lemma ln_sin_integrable: "interval_lebesgue_integrable lborel (ereal 0) (ereal pi)
(λθ. ln (sin θ))"
proof -
have meas: "(λθ :: real. ln (sin θ)) ∈ borel_measurable borel"
by simp
have lower: "ln (2 * θ / pi) ≤ ln (sin θ)" if "θ ∈ {0<..<pi / 2}"
for θ
using sin_ge_two_over_pi[of θ] sin_gt_zero[of θ] pi_gt_zero ln_le_cancel_iff[of "2
* θ / pi" "sin θ"]
using that
by simp
have upper: "ln (sin θ) ≤ 0" if "θ ∈ {0<..<pi}" for θ
using sin_le_one[of θ] sin_gt_zero[of θ]
using that
by (simp add: ln_le_zero_iff)
have bound: "norm (ln (sin θ)) ≤ norm (ln θ) + norm (ln (2 / pi))"
if th: "θ ∈ {0<..<pi / 2}" for θ
proof -
have e0: "2 * θ / pi = θ * (2 / pi)"
by simp
have "ln (2 * θ / pi) = ln θ + ln (2 / pi)"
using th pi_gt_zero ln_mult[of θ "2 / pi"] unfolding e0
by simp
moreover have "ln (2 * θ / pi) ≤ ln (sin θ)" using lower th by blast
moreover have "ln (sin θ) ≤ 0" using upper th pi_gt_zero by auto
ultimately show ?thesis unfolding real_norm_def
by linarith
qed
have i1: "set_integrable lborel {0<..<pi / 2} (λθ. norm (ln θ))"
using set_integrable_abs[OF ln_integrable_near_zero[OF pi_half_gt_zero]] unfolding real_norm_def
by simp
have i2: "set_integrable lborel {0<..<pi / 2} (λθ :: real. norm (ln (2 / pi)))"
using interval_integral_const(1)[of 0 "pi / 2" "norm (ln (2 / pi))"] pi_gt_zero
unfolding interval_lebesgue_integrable_def
by simp
have int_ln: "set_integrable lborel {0<..<pi / 2} (λθ. norm (ln θ) +
norm (ln (2 / pi)))"
using set_integral_add(1)[OF i1 i2] by simp
have sb: "set_borel_measurable lborel {0<..<pi / 2} (λθ. ln (sin θ))"
unfolding set_borel_measurable_def using meas
by simp
have ae: "AE x in lborel. x ∈ {0<..<pi / 2} ⟶
norm (ln (sin x)) ≤ norm (norm (ln x) + norm (ln (2 / pi)))" using bound
by (auto intro: AE_I2)
have int_half: "set_integrable lborel {0<..<pi / 2} (λθ. ln (sin θ))"
using set_integrable_bound[OF int_ln sb ae] by simp
have "interval_lebesgue_integrable lborel (ereal 0) (ereal (pi /
2)) (λθ. ln (sin θ))" using int_half
unfolding interval_lebesgue_integrable_def
by simp
hence "interval_lebesgue_integrable lborel (ereal (pi - pi / 2)) (ereal (pi -
0)) (λx. ln (sin (pi - x)))"
using LBINT_reflect_int[of 0 "pi / 2" "(λθ. ln (sin θ))" pi]
by simp
hence int_upper: "set_integrable lborel {pi / 2<..<pi} (λθ. ln (sin θ))"
unfolding interval_lebesgue_integrable_def
by simp
have split: "einterval (ereal 0) (ereal pi) =
{0<..<pi / 2} ∪ {pi / 2<..<pi} ∪ {pi / 2}"
using pi_gt_zero
by auto
have m1a: "{0<..<pi / 2} ∈ sets lborel"
by simp
have m1b: "{pi / 2<..<pi} ∈ sets lborel"
by simp
note m1 = m1a m1b
have u1: "set_integrable lborel ({0<..<pi / 2} ∪ {pi /
2<..<pi}) (λθ. ln (sin θ))" using set_integrable_Un[OF int_half int_upper]
using m1
by blast
have "set_integrable lborel ({0<..<pi / 2} ∪ {pi / 2<..<pi} ∪ {pi /
2}) (λθ. ln (sin θ))"
using set_integrable_discrete_difference[where X="{pi / 2}" and A="{0<..<pi / 2} ∪ {pi /
2<..<pi}" and B="{0<..<pi / 2} ∪ {pi / 2<..<pi} ∪ {pi /
2}" and M=lborel and f="(λθ. ln (sin θ))"] u1
by auto
moreover have "ereal 0 ≤ ereal pi" using pi_gt_zero by simp
ultimately show ?thesis unfolding interval_lebesgue_integrable_def unfolding split[symmetric]
by simp
qed
lemma ln_sin_integrable_half: "interval_lebesgue_integrable lborel (ereal 0) (ereal (pi /
2)) (λθ. ln (sin θ))"
proof -
have a: "set_integrable lborel {0<..<pi} (λθ. ln (sin θ))"
using ln_sin_integrable pi_gt_zero unfolding interval_lebesgue_integrable_def
by simp
have "set_integrable lborel {0<..<pi / 2} (λθ. ln (sin θ))"
using set_integrable_subset[OF a, of "{0<..<pi / 2}"]
by fastforce
thus ?thesis unfolding interval_lebesgue_integrable_def
by simp
qed
lemma ln_cos_integrable_half: "interval_lebesgue_integrable lborel (ereal 0) (ereal (pi /
2)) (λu. ln (cos u))"
proof -
have e: "(λx. ln (sin (pi / 2 - x))) = (λx. ln (cos x))"
by (simp add: cos_sin_eq)
show ?thesis using LBINT_reflect_int[of 0 "pi / 2" "λθ. ln (sin θ)" "pi /
2"] ln_sin_integrable_half unfolding e
by simp
qed
lemma ln_sin_integral: "interval_lebesgue_integral lborel (ereal 0) (ereal pi) (λθ.
ln (sin θ)) = - pi * ln 2"
proof -
define I where "I = interval_lebesgue_integral lborel (ereal 0) (ereal pi) (λθ. ln
(sin θ))"
have "interval_lebesgue_integral lborel (ereal (0)) (ereal (pi /
2)) (λθ. ln (sin θ)) + interval_lebesgue_integral lborel (ereal (pi /
2)) (ereal (pi)) (λθ. ln (sin θ)) = I" unfolding I_def
using interval_integral_sum[of "ereal 0" "ereal (pi /
2)" "ereal pi" "(λθ. ln (sin θ))"] ln_sin_integrable
by simp
moreover have "interval_lebesgue_integral lborel (ereal (pi /
2)) (ereal (pi)) (λθ. ln (sin θ)) =
interval_lebesgue_integral lborel (ereal (0)) (ereal (pi /
2)) (λθ. ln (sin θ))"
using LBINT_reflect[of "pi / 2" pi "(λθ. ln (sin θ))" pi]
by simp
ultimately have half: "I = 2 * interval_lebesgue_integral lborel (ereal 0) (ereal (pi /
2)) (λθ. ln (sin θ))"
by linarith
have p: "0 ≤ pi" using pi_gt_zero by simp
have pw: "ln (sin (0 + 2 * x)) = ln 2 + ln (sin x) + ln (cos x)" if x: "0 < x" "x < pi / 2" for x
proof -
have sx: "0 < sin x" using x sin_gt_zero[of x]
by simp
have cx: "0 < cos x" using x cos_gt_zero_pi[of x]
by simp
have e2: "sin (0 + 2 * x) = 2 * (sin x * cos x)" using sin_double[of x]
by simp
show ?thesis unfolding e2 using sx cx ln_mult[of 2 "sin x * cos x"] ln_mult[of "sin x" "cos x"]
by simp
qed
have "I = 2 * interval_lebesgue_integral lborel (ereal (0)) (ereal (pi /
2)) (λx. ln (sin (0 + 2 * x)))"
using LBINT_affine[of 2 0 pi "λθ. ln (sin θ)" 0, OF _ p] unfolding I_def
by simp
moreover have "interval_lebesgue_integral lborel (ereal (0)) (ereal (pi /
2)) (λx. ln (sin (0 + 2 * x))) =
interval_lebesgue_integral lborel (ereal (0)) (ereal (pi / 2)) (λx. ln 2 + ln (sin x) +
ln (cos x))" using pw pi_gt_zero
by (auto intro: interval_integral_cong)
moreover have "interval_lebesgue_integral lborel (ereal (0)) (ereal (pi / 2)) (λx. ln 2 +
ln (sin x) + ln (cos x)) = pi / 2 * ln 2 +
interval_lebesgue_integral lborel (ereal (0)) (ereal (pi / 2)) (λu. ln (sin u)) +
interval_lebesgue_integral lborel (ereal (0)) (ereal (pi / 2)) (λu. ln (cos u))"
using ln_sin_integrable_half ln_cos_integrable_half
by simp
ultimately have doubling: "I = pi * ln 2 + 2 *
interval_lebesgue_integral lborel (ereal 0) (ereal (pi / 2)) (λu. ln (sin u))
+ 2 * interval_lebesgue_integral lborel (ereal 0) (ereal (pi /
2)) (λu. ln (cos u))"
by linarith
have e: "(λx. ln (cos (pi / 2 - x))) = (λx. ln (sin x))"
by (simp add: cos_diff)
have cos_eq: "interval_lebesgue_integral lborel (ereal 0) (ereal (pi /
2)) (λu. ln (cos u)) = interval_lebesgue_integral lborel (ereal 0) (ereal (pi /
2)) (λu. ln (sin u))"
using LBINT_reflect[of 0 "pi / 2" "λu. ln (cos u)" "pi / 2"] pi_gt_zero unfolding e
by simp
show ?thesis using half doubling cos_eq unfolding I_def[symmetric] by linarith
qed
lemma norm_1_minus_cis: "norm (1 - cis θ) ^ 2 = (2 * sin (θ / 2)) ^ 2"
proof -
have a: "norm (1 - cis θ) ^ 2 = (1 - cos θ) ^ 2 + (sin θ) ^ 2"
by (simp add: cmod_power2)
have b: "cos θ = 1 - 2 * sin (θ / 2) ^ 2" using cos_double_sin[of "θ / 2"]
by simp
have c: "sin θ = 2 * sin (θ / 2) * cos (θ / 2)"
using sin_double[of "θ / 2"]
by simp
have d: "sin (θ / 2) ^ 2 + cos (θ / 2) ^ 2 = 1" by (rule sin_cos_squared_add)
have e: "(1 - (1 - 2 * sin (θ / 2) ^ 2)) ^ 2 + (2 * sin (θ / 2) * cos (θ /
2)) ^ 2 = (2 * sin (θ / 2)) ^ 2 * (sin (θ / 2) ^ 2 + cos (θ / 2) ^ 2)"
using sin_cos_squared_add[of "θ / 2"]
unfolding power2_eq_square
by argo
show ?thesis unfolding a b c e d
by simp
qed
lemma ln_norm_one_minus_cis:
assumes th: "0 < θ" "θ < 2 * pi"
shows "ln (norm (1 - cis θ)) = ln 2 + ln (sin (θ / 2))"
proof -
have s: "0 < sin (θ / 2)" using th sin_gt_zero[of "θ / 2"]
by simp
have n: "norm (1 - cis θ) = 2 * sin (θ / 2)" using norm_1_minus_cis[of θ] s
using power2_eq_iff_nonneg[of "norm (1 - cis θ)" "2 * sin (θ / 2)"]
by simp
show ?thesis unfolding n using s ln_mult[of 2 "sin (θ / 2)"]
by simp
qed
text ‹@{text "∫_0^{2π} log|1 - e^{iθ}| dθ = 0"}: the singular case
of the circle average.›
lemma circle_log_one: "interval_lebesgue_integral lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (1 - cis θ))) = 0"
proof -
have c1: "interval_lebesgue_integral lborel (ereal (0)) (ereal (2 *
pi)) (λθ. ln (norm (1 - cis θ))) =
interval_lebesgue_integral lborel (ereal (0)) (ereal (2 * pi)) (λθ. ln 2 +
ln (sin (θ / 2)))" using ln_norm_one_minus_cis pi_gt_zero
by (auto intro: interval_integral_cong)
have p: "0 ≤ 2 * pi" using pi_gt_zero by simp
have gi: "interval_lebesgue_integrable lborel (ereal (0)) (ereal (2 *
pi)) (λθ. ln (sin (θ / 2)))"
using LBINT_affine_int[of 2 0 "2 * pi" "λθ. ln (sin (θ / 2))" 0,
OF _ p] ln_sin_integrable
by simp
have gv: "interval_lebesgue_integral lborel (ereal (0)) (ereal (2 *
pi)) (λθ. ln (sin (θ / 2))) = 2 * (- pi * ln 2)"
using LBINT_affine[of 2 0 "2 * pi" "λθ. ln (sin (θ / 2))" 0,
OF _ p] ln_sin_integral
by simp
have c2: "interval_lebesgue_integral lborel (ereal (0)) (ereal (2 *
pi)) (λθ. ln 2 + ln (sin (θ / 2))) =
ln 2 * (2 * pi - 0) + interval_lebesgue_integral lborel (ereal (0)) (ereal (2 *
pi)) (λθ. ln (sin (θ / 2)))" using gi
by simp
show ?thesis using c1 c2 gv
by argo
qed
lemma circle_log_one_integrable: "interval_lebesgue_integrable lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (1 - cis θ)))"
proof -
have p: "0 ≤ 2 * pi" using pi_gt_zero by simp
have "interval_lebesgue_integrable lborel (ereal (0)) (ereal (2 *
pi)) (λθ. ln (sin (θ / 2)))"
using LBINT_affine_int[of 2 0 "2 * pi" "λθ. ln (sin (θ / 2))" 0,
OF _ p] ln_sin_integrable
by simp
hence "interval_lebesgue_integrable lborel (ereal 0) (ereal (2 * pi)) (λθ. ln 2 +
ln (sin (θ / 2)))"
by simp
hence s2: "set_integrable lborel {0<..<2 * pi} (λθ. ln 2 + ln (sin (θ /
2)))" using pi_gt_zero unfolding interval_lebesgue_integrable_def
by simp
have "set_integrable lborel {0<..<2 * pi} (λθ. ln (norm (1 - cis θ)))"
using set_integrable_cong[of lborel lborel "{0<..<2 * pi}" "{0<..<2 *
pi}" "λθ. ln (norm (1 - cis θ))" "λθ. ln 2 +
ln (sin (θ / 2))"] ln_norm_one_minus_cis s2
by simp
thus ?thesis using pi_gt_zero unfolding interval_lebesgue_integrable_def
by simp
qed
text ‹Mean value of the holomorphic @{text "Ln (1 - z/a)"} on the unit circle,
@{text "|a| > 1"}.›
lemma circle_log_gt:
assumes "1 < norm a"
shows "interval_lebesgue_integral lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (cis θ - a))) = 2 * pi * ln (norm a)"
proof -
define f where "f = (λz. Ln (1 - z / a))"
have a0: "a ≠ 0" using assms by auto
have nr: "1 - z / a ∉ ℝ⇩≤⇩0" if "norm z < norm a" for z
proof -
have "norm (z / a) < 1" using that a0
by (simp add: norm_divide field_simps)
hence "Re (z / a) < 1" using complex_Re_le_cmod[of "z / a"] by linarith
thus ?thesis
by (simp add: complex_nonpos_Reals_iff)
qed
have hol: "f holomorphic_on ball 0 (norm a)" unfolding f_def using nr a0
by (fastforce intro: holomorphic_intros)
have sb: "cball 0 1 ⊆ ball (0 :: complex) (norm a)" using assms
by auto
have sb2: "ball 0 1 ⊆ ball (0 :: complex) (norm a)" using sb ball_subset_cball
by blast
have cont: "continuous_on (cball 0 1) f" using holomorphic_on_imp_continuous_on[OF hol] sb
by (blast intro: continuous_on_subset)
have cauchy: "((λu. f u / (u - 0)) has_contour_integral (2 * of_real pi * 𝗂 *
f 0)) (circlepath 0 1)"
using Cauchy_integral_circlepath [OF cont holomorphic_on_subset [OF hol sb2], of 0]
by simp
have f0: "f 0 = 0" by (simp add: f_def)
have mean: "interval_lebesgue_integral lborel (ereal 0) (ereal (2 *
pi)) (λθ. Re (f (cis θ))) = 0"
proof -
have cx: "circlepath 0 1 x = cis (2 * pi * x)" for x
by (simp add: circlepath cis_conv_exp mult_ac)
have m1: "((λx. f (circlepath 0 1 x) / (circlepath 0 1 x - 0) *
vector_derivative (circlepath 0 1) (at x within {0..1})) has_integral 0) {0..1}"
using cauchy f0 unfolding has_contour_integral_def
by simp
have m2: "f (circlepath 0 1 x) / (circlepath 0 1 x - 0) *
vector_derivative (circlepath 0 1) (at x within {0..1}) =
2 * pi * 𝗂 * f (cis (2 * pi * x))" if "x ∈ {0..1}" for x
using vector_derivative_circlepath01[of x 0 1] that unfolding cx
by (simp add: cis_conv_exp field_simps)
have m3: "((λx. 2 * pi * 𝗂 * f (cis (2 * pi * x))) has_integral 0) {0..1}"
using m1 has_integral_cong[of "{0..1}", OF m2]
by fast
have cnz: "complex_of_real (2 * pi) * 𝗂 ≠ 0"
by simp
have m4: "((λx. f (cis (2 * pi * x))) has_integral 0) {0..1}"
using m3 has_integral_mult_right_iff[of "2 * pi * 𝗂" "λx. f (cis (2 * pi *
x))" 0 "{0..1}"] cnz
by simp
have m5: "((λx. Re (f (cis (2 * pi * x)))) has_integral 0) {0..1}"
using has_integral_linear[OF m4 bounded_linear_Re]
by (simp add: o_def)
have g1: "continuous_on UNIV (λθ. Re (f (cis θ)))"
using continuous_on_compose2[OF cont, of UNIV cis]
by (fastforce intro: continuous_intros)
have g2: "continuous_on {0..1} (λx. Re (f (cis (0 + 2 * pi * x))))"
using continuous_on_compose2[OF g1, of "{0..1}" "λx. 0 + 2 * pi * x"]
by (fast intro: continuous_intros)
have si: "set_integrable lborel {0..1} (λx. Re (f (cis (0 + 2 * pi * x))))"
using borel_integrable_compact[OF compact_Icc g2] unfolding set_integrable_def
by fastforce
have ie: "interval_lebesgue_integral lborel (ereal 0) (ereal 1) (λx. Re (f (cis (0 + 2 *
pi * x)))) = integral {0..1} (λx. Re (f (cis (0 + 2 * pi * x))))"
using interval_integral_eq_integral[OF _ si]
by argo
have iz: "integral {0..1} (λx. Re (f (cis (0 + 2 * pi * x)))) = 0" using m5
by (auto intro: integral_unique)
have af: "interval_lebesgue_integral lborel (ereal 0) (ereal (2 *
pi)) (λθ. Re (f (cis θ))) =
2 * pi * interval_lebesgue_integral lborel (ereal 0) (ereal 1) (λx. Re (f (cis (0 +
2 * pi * x))))"
using LBINT_affine[of "2 * pi" 0 "2 *
pi" "λθ. Re (f (cis θ))" 0] pi_gt_zero
by simp
show ?thesis using af ie iz
by simp
qed
have pt: "ln (norm (cis θ - a)) = ln (norm a) + Re (f (cis θ))" for θ
proof -
have nz: "1 - cis θ / a ≠ 0"
proof
assume "1 - cis θ / a = 0"
hence "cis θ = a" using a0
by (simp add: field_simps)
thus False using assms
by auto
qed
have eq: "norm (cis θ - a) = norm a * norm (1 - cis θ / a)"
proof -
have "cis θ - a = - (a * (1 - cis θ / a))" using a0
by (simp add: field_simps)
thus ?thesis
by (simp add: norm_mult)
qed
show ?thesis unfolding eq f_def using nz a0 ln_mult[of "norm a" "norm (1 - cis θ / a)"]
by simp
qed
have c1: "continuous_on UNIV (λθ. f (cis θ))"
using continuous_on_compose2[OF cont, of UNIV cis]
by (fastforce intro: continuous_intros)
have c2: "continuous_on {0..2 * pi} (λθ. Re (f (cis θ)))"
using continuous_on_Re[OF c1]
by (blast intro: continuous_on_subset)
have ii: "interval_lebesgue_integrable lborel (ereal 0) (ereal (2 *
pi)) (λθ. Re (f (cis θ)))"
using interval_integrable_continuous_on[OF _ c2] pi_gt_zero
by simp
show ?thesis unfolding pt using ii mean
by simp
qed
lemma circle_log_lt:
assumes "norm a < 1"
shows "interval_lebesgue_integral lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (cis θ - a))) = 0"
proof (cases "a = 0")
case True
thus ?thesis by simp
next
case False
define b where "b = 1 / cnj a"
have nb: "norm b = 1 / norm a" and b1: "1 < norm b" using False assms
by (auto simp: b_def norm_divide)
have pt: "ln (norm (cis θ - a)) = ln (norm a) + ln (norm (cis θ - b))" for θ
proof -
have c1: "cnj (cnj a * cis θ - 1) = cis (- θ) * (a - cis θ)"
by (simp add: cis_cnj algebra_simps cis_mult)
have "norm (cnj a * cis θ - 1) = norm (a - cis θ)"
using arg_cong[where f = norm, OF c1] unfolding complex_mod_cnj norm_mult
by auto
hence e1: "norm (cis θ - a) = norm (cnj a * cis θ - 1)"
using norm_minus_commute[of a "cis θ"]
by simp
have e2: "norm (cnj a * cis θ - 1) = norm a * norm (cis θ - b)"
proof -
have "cnj a * cis θ - 1 = cnj a * (cis θ - b)" using False unfolding b_def
by (simp add: field_simps)
thus ?thesis by (simp add: norm_mult)
qed
have nz: "cis θ - b ≠ 0" using b1
by auto
show ?thesis unfolding e1 e2 using False nz ln_mult[of "norm a" "norm (cis θ - b)"]
by simp
qed
have nzb: "norm (cis θ - b) ≠ 0" for θ using b1
by auto
have cb: "continuous_on {0..2 * pi} (λθ. ln (norm (cis θ - b)))" using nzb
by (fast intro: continuous_intros)
have ib: "interval_lebesgue_integrable lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (cis θ - b)))"
using interval_integrable_continuous_on[OF _ cb] pi_gt_zero
by simp
show ?thesis unfolding pt using ib circle_log_gt[OF b1] nb False
by (simp add: ln_div)
qed
text ‹A point of the unit circle as @{text "cis φ"} with
@{text "φ ∈ [0, 2π]"}.›
lemma cis_of_norm_one:
assumes "norm a = 1"
obtains φ where "a = cis φ" "0 ≤ φ" "φ ≤ 2 * pi"
proof -
have c: "a = cis (Arg a)" using rcis_cmod_Arg[of a] assms
by (simp add: rcis_def)
show ?thesis
proof (cases "0 ≤ Arg a")
case True
thus ?thesis using that[of "Arg a"] c Arg_bounded[of a]
by linarith
next
case False
have "cis (Arg a + 2 * pi) = cis (Arg a)"
by (simp add: cis_mult[symmetric])
thus ?thesis using that[of "Arg a + 2 * pi"] c Arg_bounded[of a] False
by simp
qed
qed
lemma norm_cis_minus_cis: "norm (cis θ - cis φ) = norm (1 - cis (θ - φ))"
proof -
have q: "cis θ - cis φ = cis φ * (cis (θ - φ) - 1)"
by (simp add: cis_mult algebra_simps)
show ?thesis unfolding q norm_mult
using norm_minus_commute[of "cis (θ - φ)" 1]
by simp
qed
lemma circle_log_eq:
assumes "norm a = 1"
shows "interval_lebesgue_integral lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (cis θ - a))) = 0"
proof -
obtain φ where phi: "a = cis φ" and p0: "0 ≤ φ" "φ ≤ 2 * pi"
by (rule cis_of_norm_one[OF assms])
define h where "h u = ln (norm (1 - cis u))" for u
have per: "h (x + 2 * pi) = h x" for x unfolding h_def
by (simp add: cis_mult[symmetric])
have ih: "interval_lebesgue_integrable lborel (ereal 0) (ereal (2 * pi)) h"
using circle_log_one_integrable unfolding h_def[abs_def] .
have pt: "ln (norm (cis θ - a)) = h (θ - φ)" for θ
using norm_cis_minus_cis[of θ φ] unfolding phi h_def by simp
show ?thesis unfolding pt using periodic_shift_eq[of h φ, OF per ih p0] circle_log_one
unfolding h_def[abs_def]
by simp
qed
lemma circle_log_eq_integrable:
assumes "norm a = 1"
shows "interval_lebesgue_integrable lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (cis θ - a)))"
proof -
obtain φ where phi: "a = cis φ" and p0: "0 ≤ φ" "φ ≤ 2 * pi"
by (rule cis_of_norm_one[OF assms])
define h where "h u = ln (norm (1 - cis u))" for u
have per: "h (x + 2 * pi) = h x" for x unfolding h_def
by (simp add: cis_mult[symmetric])
have ih: "interval_lebesgue_integrable lborel (ereal 0) (ereal (2 * pi)) h"
using circle_log_one_integrable unfolding h_def[abs_def] .
have pt: "ln (norm (cis θ - a)) = h (θ - φ)" for θ
using norm_cis_minus_cis[of θ φ] unfolding phi h_def by simp
show ?thesis unfolding pt using periodic_shift_int[of h φ, OF per ih p0]
unfolding h_def[abs_def]
by simp
qed
theorem circle_avg_log:
"interval_lebesgue_integral lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (cis θ - a))) = 2 * pi * ln (max 1 (norm a))"
proof (cases "norm a" "1 :: real" rule: linorder_cases)
case less thus ?thesis using circle_log_lt[OF less] by (simp add: max_def)
next
case equal thus ?thesis using circle_log_eq[OF equal] by (simp add: max_def)
next
case greater thus ?thesis using circle_log_gt[OF greater] by (simp add: max_def)
qed
lemma circle_log_integrable:
"interval_lebesgue_integrable lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (cis θ - a)))"
proof (cases "norm a = 1")
case True
thus ?thesis by (rule circle_log_eq_integrable)
next
case False
have nz: "norm (cis θ - a) ≠ 0" for θ using False
by auto
have cb: "continuous_on {0..2 * pi} (λθ. ln (norm (cis θ - a)))" using nz
by (fast intro: continuous_intros)
show ?thesis using interval_integrable_continuous_on[OF _ cb] pi_gt_zero
by simp
qed
text ‹Normalised arclength on the circle of radius @{text ε} about @{text c}.›
definition circ :: "complex ⇒ real ⇒ complex measure" where
"circ c ε = distr (density lborel (λθ. ennreal (indicator {0..2 *
pi} θ / (2 * pi)))) borel
(λθ. c + of_real ε * cis θ)"
text ‹The circle average of @{text "log|z - a|"} over the circle of radius @{text ε}
about @{text c}: @{text "log max(ε, |c - a|)"}.›
lemma circ_log:
assumes "0 < ε"
shows "integral⇧L (circ c ε) (λz. ln (norm (z - a))) =
ln (max ε (norm (c - a)))"
proof -
have "integral⇧L (circ c ε) (λz. ln (norm (z - a)))
= (1 / (2 * pi)) * interval_lebesgue_integral lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (c + of_real ε * cis θ - a)))"
proof -
have mg0: "(λθ. c + of_real ε * cis θ) ∈
borel_measurable borel"
by (fast intro: borel_measurable_continuous_onI continuous_intros)
have mF: "(λz. ln (norm (z - a))) ∈ borel_measurable borel"
by simp
have i1: "integral⇧L (distr (density lborel (λθ. ennreal (indicator {0..2 *
pi} θ / (2 * pi)))) borel (λθ. c + of_real ε *
cis θ)) (λz. ln (norm (z - a))) =
integral⇧L (density lborel (λθ. ennreal (indicator {0..2 * pi} θ /
(2 * pi)))) (λθ. ln (norm (c + of_real ε * cis θ - a)))"
using integral_distr[of "λθ. c + of_real ε *
cis θ" "(density lborel (λθ. ennreal (indicator {0..2 * pi} θ /
(2 * pi))))" borel "λz. ln (norm (z - a))"] mg0 mF
by fastforce
have mG: "(λθ. ln (norm (c + of_real ε * cis θ - a))) ∈
borel_measurable borel" using measurable_compose[OF mg0 mF]
by simp
have i2: "integral⇧L (density lborel (λθ. ennreal (indicator {0..2 *
pi} θ / (2 * pi)))) (λθ. ln (norm (c + of_real ε *
cis θ - a))) = (∫θ. (indicator {0..2 * pi} θ / (2 *
pi)) *⇩R (λθ. ln (norm (c + of_real ε * cis θ -
a))) θ ∂lborel)"
using integral_density[of "(λθ. ln (norm (c + of_real ε *
cis θ - a)))" lborel "λθ. indicator {0..2 * pi} θ / (2 *
pi)"] mG
by fastforce
have i3a: "(λθ. (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 i3b: "(∫θ. (1 / (2 * pi)) * (indicator {0..2 *
pi} θ *⇩R (λθ. ln (norm (c + of_real ε * cis θ -
a))) θ) ∂lborel) =
(1 / (2 * pi)) * (∫θ. indicator {0..2 *
pi} θ *⇩R (λθ. ln (norm (c + of_real ε * cis θ -
a))) θ ∂lborel)"
by (fast intro: integral_mult_right_zero)
have i3c: "(∫θ. indicator {0..2 *
pi} θ *⇩R (λθ. ln (norm (c + of_real ε * cis θ -
a))) θ ∂lborel) = interval_lebesgue_integral lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (c + of_real ε * cis θ - a)))"
using interval_integral_Icc[of 0 "2 * pi" "(λθ. ln (norm (c +
of_real ε * cis θ - a)))"] pi_gt_zero unfolding set_lebesgue_integral_def
by linarith
show ?thesis unfolding circ_def using i1 i2 i3a i3b i3c
by presburger
qed
also have "… = (1 / (2 * pi)) * interval_lebesgue_integral lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln ε + ln (norm (cis θ - (a - c) /
of_real ε)))"
proof -
define w where "w = (a - c) / of_real ε"
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
have null: "{θ. cis θ = w} ∈ null_sets lborel"
using countable_imp_null_set_lborel countable_subset[OF bad]
by fast
have pw: "ln (norm (c + of_real ε * cis θ - a)) =
ln ε + ln (norm (cis θ - w))" if nw: "cis θ ≠ w" for θ
proof -
have e: "c + of_real ε * cis θ - a = of_real ε * (cis θ - w)"
using assms unfolding w_def
by (simp add: field_simps)
show ?thesis unfolding e norm_mult
using assms nw ln_mult[of ε "norm (cis θ - w)"]
by simp
qed
have n1: "(λθ. norm (c + of_real ε * cis θ - a)) ∈
borel_measurable borel"
by (fast intro: borel_measurable_continuous_onI continuous_intros)
have n2: "(λθ. norm (cis θ - w)) ∈ borel_measurable borel"
by (fast intro: borel_measurable_continuous_onI continuous_intros)
have m3: "(λθ. ln (norm (c + of_real ε * cis θ - a))) ∈
borel_measurable borel" using borel_measurable_ln[OF n1]
by simp
have m4: "(λθ. ln ε + ln (norm (cis θ - w))) ∈
borel_measurable borel" using borel_measurable_ln[OF n2]
by (auto intro: borel_measurable_add)
have ae: "AE θ in lborel. θ ∈
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))) θ"
using AE_I'[OF null, 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 eqI: "interval_lebesgue_integral lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln (norm (c + of_real ε * cis θ - a))) =
interval_lebesgue_integral lborel (ereal 0) (ereal (2 *
pi)) (λθ. ln ε + ln (norm (cis θ - w)))"
using interval_integral_cong_AE[OF m3 m4 ae]
by fastforce
show ?thesis unfolding w_def[symmetric] using eqI
by simp
qed
also have "… = (1 / (2 * pi)) * (2 * pi * ln ε + 2 * pi * ln (max 1 (norm ((a -
c) / of_real ε))))"
using circle_log_integrable[of "(a - c) / of_real ε"] circle_avg_log[of "(a - c) /
of_real ε"]
by simp
also have "… = ln (max ε (norm (c - a)))"
proof -
have nd: "norm ((a - c) / of_real ε) = norm (c - a) / ε" using assms
by (simp add: norm_divide norm_minus_commute)
have k: "ln ε + ln (max 1 (norm (c - a) / ε)) =
ln (max ε (norm (c - a)))"
proof (cases "norm (c - a) ≤ ε")
case True
thus ?thesis using assms
by (simp add: max_def)
next
case False
thus ?thesis using assms ln_div[of "norm (c - a)" ε]
by (auto simp: max_def)
qed
have e: "(1 / (2 * pi)) * (2 * pi * ln ε + 2 * pi * ln (max 1 (norm (c - a) /
ε)))
= ln ε + ln (max 1 (norm (c - a) / ε))"
by (simp add: field_simps)
show ?thesis unfolding nd e k ..
qed
finally show ?thesis .
qed
end