Theory Logarithmic_Energy
theory Logarithmic_Energy
imports Laplace_Sin_Cot_Series
begin
section ‹Logarithmic energy of measures on ‹ℂ› and the zero-mass energy
inequality›
text ‹The mutual logarithmic energy ‹I(μ, ν) =
∫∫ ln |z - w| dμ(z) dν(w)› of finite measures on
‹ℂ›, the
two-dimensional Gaussian integral ‹∫⇩ℂ exp(-b|v|⇧2) dv =
π/b›, the non-negativity of the energy of Gaussian
kernels, the truncated kernels ‹K⇩n → ln |z - w|› obtained
by integrating the Gaussian against ‹ds/s›
(Frullani), and the main result @{text log_energy_zero_mass_nonpos}:
for measures ‹ν⇩1, ν⇩2 ≤ η› of equal mass with
‹ln |z - w|› integrable on ‹η ⊗ η› and a null
diagonal, ‹I(ν⇩1) - 2 I(ν⇩1, ν⇩2) + I(ν⇩2) ≤
0›.›
text ‹Mutual logarithmic energy @{text "integral integral log|z - w| dmu(z) dν(w)"} on
‹ℂ›.›
definition logEnergyC :: "complex measure ⇒ complex measure ⇒ real" where
"logEnergyC μ ν = integral⇧L μ (λz. integral⇧L ν (λw.
ln (norm (z - w))))"
text ‹Lemma 6.2 (zero-mass logarithmic energy), in the corrected form of the Lean proof:
for finite
measures @{text "ν_1, ν_2 ≤ η"} on ‹ℂ› of equal mass,
with @{text "log|z-w|"} integrable for
@{text "η ⊗ η"} and the diagonal @{text "η ⊗ η"}-null,
@{text "I(ν_1) - 2 I(ν_1,ν_2) + I(ν_2) ≤ 0"}. (The literal statement with
@{text "log 0 = 0"} is false
for point masses; the diagonal hypothesis is what the paper uses.)
Proof: Gaussian kernels @{text "e^{-s|z-w|^2}"} have nonnegative energy (Fubini), integrate in
@{text s} against @{text "ds/s"} to reach @{text "log"} (dominated convergence).›
text ‹The Gaussian integral on @{text ℂ}:
@{text "∫ e^{-b|v|^2} dv = π/b"}.›
lemma gauss_nn_C:
fixes b :: real
assumes b: "0 < b"
shows "(∫⇧+ v. ennreal (exp (- b * (norm (v :: complex)) ^ 2)) ∂lborel) =
ennreal (pi / b)"
proof -
define h :: "real ⇒ real" where "h r = 2 * b * r * exp (- b * r ^ 2)" for r
have hm: "h ∈ borel_measurable borel" unfolding h_def
by simp
have p2: "filterlim (λr :: real. r ^ 2) at_top at_top"
using filterlim_pow_at_top[OF _ filterlim_ident, of 2]
by simp
have l0: "((λr :: real. exp (- (b * r ^ 2))) ⤏ 0) at_top"
using filterlim_compose[OF exp_neg_lim[OF b] p2]
by simp
have l1: "((λr :: real. exp (- (b * r ^ 2)) * (∑ k ≤
1. (b * r ^ 2) ^ k / fact k)) ⤏ 0) at_top"
using filterlim_compose[OF gam_lim[OF b, of 1] p2]
by simp
have lim1: "((λr :: real. - exp (- b * r ^ 2)) ⤏ 0) at_top"
using tendsto_minus[OF l0]
by simp
have step1: "ennreal (exp (- b * (norm v) ^ 2)) =
(∫⇧+ r. ennreal (h r) * indicator {norm v..} r ∂lborel)"
for v :: complex
proof -
have D: "DERIV (λr :: real. - exp (- b * r ^ 2)) r :> h r" for r unfolding h_def
by (intro derivative_eq_intros, (rule refl)+) (simp add: algebra_simps power2_eq_square)
have nn: "0 ≤ h r" if "norm v ≤ r" for r
proof -
have r0: "0 ≤ r" using that norm_ge_zero[of v]
by linarith
show ?thesis unfolding h_def using r0 b
using mult_nonneg_nonneg by simp
qed
have "(∫⇧+ r. ennreal (h r) * indicator {norm v..} r ∂lborel) =
ennreal (0 - (- exp (- b * (norm v) ^ 2)))"
using nn_integral_FTC_atLeast[OF hm D nn lim1] .
thus ?thesis
by simp
qed
have ps: "pair_sigma_finite (lborel :: complex measure) (lborel :: real measure)"
by (simp add: pair_sigma_finite_def sigma_finite_lborel)
have jm: "(λ(v :: complex, r :: real). ennreal (h r) * indicator {norm v..} r) ∈
borel_measurable (lborel ⨂⇩M lborel)"
proof -
have e: "(λ(v :: complex, r :: real). ennreal (h r) * indicator {norm v..} r) =
(λp. ennreal (h (snd p)) * indicator {p. norm (fst p) ≤ snd p} p)"
by (simp add: fun_eq_iff indicator_def)
have mf2: "(λp :: complex × real. snd p - norm (fst p)) ∈
borel_measurable (lborel ⨂⇩M lborel)"
by simp
have eq: "{p :: complex × real. norm (fst p) ≤ snd p} =
(λp. snd p - norm (fst p)) -` {0..} ∩ space (lborel ⨂⇩M lborel)"
by (auto simp: space_pair_measure)
have S: "{p :: complex × real. norm (fst p) ≤ snd p} ∈
sets (lborel ⨂⇩M lborel)" unfolding eq using measurable_sets[OF mf2, of "{0..}"]
by simp
show ?thesis unfolding e using S hm
by simp
qed
have inner: "(∫⇧+ v. ennreal (h r) *
indicator {norm v..} r ∂(lborel :: complex measure)) =
ennreal (pi * h r * r ^ 2) * indicator {0..} r" for r :: real
proof (cases "0 ≤ r")
case True
have hn: "0 ≤ h r" unfolding h_def using True b
by simp
have ind: "(λv :: complex. ennreal (h r) * indicator {norm v..} r) =
(λv. ennreal (h r) * indicator (cball 0 r) v)"
by (simp add: fun_eq_iff indicator_def)
have i1: "(∫⇧+ v. ennreal (h r) *
indicator (cball 0 r) v ∂(lborel :: complex measure)) =
ennreal (h r) * emeasure lborel (cball (0 :: complex) r)"
using nn_integral_cmult_indicator[of "cball (0 :: complex) r" lborel "ennreal (h r)"] by simp
have i2: "emeasure lborel (cball (0 :: complex) r) = ennreal (pi * r ^ 2)"
using emeasure_cball[where c = "0 :: complex" and r = r] True
by (simp add: unit_ball_vol_2)
show ?thesis unfolding ind i1 i2 using True hn
by (simp add: ennreal_mult["symmetric"] mult_ac)
next
case False
have "(λv :: complex. ennreal (h r) * indicator {norm v..} r) = (λv. 0)"
proof -
have "¬ norm (v :: complex) ≤ r" for v using False norm_ge_zero[of v]
by linarith
thus ?thesis
by (simp add: fun_eq_iff indicator_def)
qed
thus ?thesis using False
by simp
qed
have "(∫⇧+ v. ennreal (exp (- b * (norm (v :: complex)) ^ 2)) ∂lborel) =
(∫⇧+ v. (∫⇧+ r. ennreal (h r) *
indicator {norm (v :: complex)..} r ∂lborel) ∂lborel)"
unfolding step1 ..
also have "… = (∫⇧+ r. (∫⇧+ v. ennreal (h r) *
indicator {norm (v :: complex)..} r ∂lborel) ∂lborel)"
using pair_sigma_finite.Fubini'[OF ps jm]
by (simp add: split_beta)
also have "… = (∫⇧+ r. ennreal (pi * h r * r ^ 2) *
indicator {0..} r ∂lborel)" unfolding inner ..
also have "… = ennreal (pi / b)"
proof -
define F :: "real ⇒ real" where "F r = - pi * (r ^ 2 + 1 / b) * exp (- b * r ^ 2)"
for r
have gm: "(λr. pi * h r * r ^ 2) ∈ borel_measurable borel" using hm
by simp
have D2: "DERIV F r :> pi * h r * r ^ 2" for r unfolding F_def h_def
by (intro derivative_eq_intros, (rule refl)+) (use b in ‹simp add: algebra_simps
power2_eq_square›)
have nn2: "0 ≤ pi * h r * r ^ 2" if "0 ≤ r" for r unfolding h_def using that b
by simp
have e: "(λr. - pi * (r ^ 2 + 1 / b) * exp (- b * r ^ 2)) =
(λr. (- pi / b) * (exp (- (b * r ^ 2)) * (∑ k ≤
1. (b * r ^ 2) ^ k / fact k)))"
using b by (simp add: fun_eq_iff algebra_simps)
have lim2: "(F ⤏ 0) at_top" unfolding F_def e
using tendsto_mult_left[OF l1, of "- pi / b"]
by simp
have "(∫⇧+ r. ennreal (pi * h r * r ^ 2) * indicator {0..} r ∂lborel) =
ennreal (0 - F 0)"
using nn_integral_FTC_atLeast[OF gm D2 nn2 lim2] .
also have "0 - F 0 = pi / b" unfolding F_def
by simp
finally show ?thesis .
qed
finally show ?thesis .
qed
lemma gauss_integral_C:
assumes "0 < b"
shows "integral⇧L lborel (λv :: complex. exp (- b * (norm v) ^ 2)) = pi / b"
proof -
have m: "(λv :: complex. exp (- b * (norm v) ^ 2)) ∈ borel_measurable lborel"
by simp
have "integral⇧L lborel (λv :: complex. exp (- b * (norm v) ^ 2)) =
enn2real (∫⇧+ v. ennreal (exp (- b *
(norm (v :: complex)) ^ 2)) ∂lborel)"
using integral_eq_nn_integral[OF m]
by simp
also have "… = pi / b" unfolding gauss_nn_C[OF assms] using assms
by (simp add: enn2real_ennreal)
finally show ?thesis .
qed
text ‹Convolution of two Gaussians:
@{text "∫ e^{-2s|z-u|^2} e^{-2s|w-u|^2} du = π/(4s) e^{-s|z-w|^2}"}.›
lemma gauss_conv:
assumes "0 < s"
shows "integral⇧L lborel (λu :: complex. exp (- 2 * s * (norm (z - u)) ^ 2) *
exp (- 2 * s * (norm (w - u)) ^ 2)) = pi / (4 * s) * exp (- s * (norm (z - w)) ^ 2)"
proof -
define m where "m = (z + w) / 2"
have par: "2 * (norm (z - u)) ^ 2 + 2 * (norm (w - u)) ^ 2 =
4 * (norm (u - m)) ^ 2 + (norm (z - w)) ^ 2" for u
unfolding m_def cmod_power2
by (simp add: power2_eq_square field_simps)
have pt: "exp (- 2 * s * (norm (z - u)) ^ 2) * exp (- 2 * s * (norm (w - u)) ^ 2) =
exp (- s * (norm (z - w)) ^ 2) * exp (- (4 * s) * (norm (u - m)) ^ 2)" for u
proof -
have "- 2 * s * (norm (z - u)) ^ 2 + - 2 * s * (norm (w - u)) ^ 2 =
- s * (norm (z - w)) ^ 2 + - (4 * s) * (norm (u - m)) ^ 2"
using arg_cong[OF par[of u], of "λx. - s * x"]
by (simp add: algebra_simps)
thus ?thesis
by (simp add: mult_exp_exp)
qed
have tr: "integral⇧L lborel (λu :: complex. exp (- (4 * s) * (norm (u - m)) ^ 2)) =
integral⇧L lborel (λu :: complex. exp (- (4 * s) * (norm u) ^ 2))"
proof -
have mf: "(λu :: complex. exp (- (4 * s) * (norm (u - m)) ^ 2)) ∈
borel_measurable borel"
by simp
have "integral⇧L lborel (λu :: complex. exp (- (4 * s) * (norm (u - m)) ^ 2)) =
integral⇧L (distr lborel borel ((+) m)) (λu :: complex. exp (- (4 * s) *
(norm (u - m)) ^ 2))"
using lborel_distr_plus[of m]
by simp
also have "… = integral⇧L lborel (λu :: complex. exp (- (4 * s) * (norm (m +
u - m)) ^ 2))"
using integral_distr[OF _ mf, of "(+) m" lborel]
by simp
finally show ?thesis
by simp
qed
have s4: "0 < 4 * s" using assms
by simp
have "integral⇧L lborel (λu :: complex. exp (- 2 * s * (norm (z - u)) ^ 2) *
exp (- 2 * s * (norm (w - u)) ^ 2))
= integral⇧L lborel (λu :: complex. exp (- s * (norm (z - w)) ^ 2) * exp (- (4 *
s) * (norm (u - m)) ^ 2))"
unfolding pt ..
also have "… = exp (- s * (norm (z - w)) ^ 2) *
integral⇧L lborel (λu :: complex. exp (- (4 * s) * (norm (u - m)) ^ 2))"
by simp
also have "… = exp (- s * (norm (z - w)) ^ 2) * (pi / (4 * s))"
unfolding tr gauss_integral_C[OF s4] ..
finally show ?thesis
by (simp add: mult_ac)
qed
definition gPhi :: "real ⇒ complex measure ⇒ complex ⇒ real"
where
"gPhi s μ u = integral⇧L μ (λz. exp (- 2 * s * (norm (z - u)) ^ 2))"
definition Eform :: "complex measure ⇒ complex measure ⇒ (complex ×
complex ⇒ real) ⇒ real" where
"Eform ν1 ν2 k = integral⇧L (ν1 ⨂⇩M ν1) k - 2 *
integral⇧L (ν1 ⨂⇩M ν2) k +
integral⇧L (ν2 ⨂⇩M ν2) k"
lemma gPhi_nn:
fixes μ :: "complex measure"
assumes fm: "finite_measure μ" and sm: "sets μ = sets borel" and s: "0 ≤ s"
shows "ennreal (gPhi s μ u) = (∫⇧+ z. ennreal (exp (- 2 * s * (norm (z -
u)) ^ 2)) ∂μ)"
proof -
have m: "(λz :: complex. exp (- 2 * s * (norm (z - u)) ^ 2)) ∈
borel_measurable μ" unfolding measurable_cong_sets[OF sm refl]
by simp
have "norm (exp (- 2 * s * (norm (z - u)) ^ 2)) ≤ 1" for z :: complex using s
by simp
hence b: "AE z in μ. norm (exp (- 2 * s * (norm (z - u)) ^ 2)) ≤ 1"
by simp
have i: "integrable μ (λz :: complex. exp (- 2 * s * (norm (z - u)) ^ 2))"
using finite_measure.integrable_const_bound[OF fm b m] .
show ?thesis unfolding gPhi_def using nn_integral_eq_integral[OF i]
by simp
qed
lemma gPhi_nonneg: "0 ≤ gPhi s μ u"
unfolding gPhi_def
by simp
lemma gPhi_meas:
fixes μ :: "complex measure"
assumes fm: "finite_measure μ" and sm: "sets μ = sets borel"
shows "gPhi s μ ∈ borel_measurable borel"
proof -
have sf: "sigma_finite_measure μ" using fm
by (simp add: finite_measure_def)
have j: "(λ(u, z). exp (- 2 * s * (norm (z - u)) ^ 2)) ∈
borel_measurable (borel ⨂⇩M μ)"
unfolding measurable_cong_sets[OF sets_pair_measure_cong[OF refl sm] refl]
by simp
show ?thesis unfolding gPhi_def[abs_def]
using sigma_finite_measure.borel_measurable_lebesgue_integral[OF sf,
of "λu z. exp (- 2 * s * (norm (z - u)) ^ 2)" borel] j
by simp
qed
lemma par_exp:
fixes z w u :: complex
shows "exp (- 2 * s * (norm (z - u)) ^ 2) * exp (- 2 * s * (norm (w - u)) ^ 2) =
exp (- s * (norm (z - w)) ^ 2) * exp (- (4 * s) * (norm (u - (z + w) / 2)) ^ 2)"
proof -
have par: "2 * (norm (z - u)) ^ 2 + 2 * (norm (w - u)) ^ 2 =
4 * (norm (u - (z + w) / 2)) ^ 2 + (norm (z - w)) ^ 2"
unfolding cmod_power2
by (simp add: power2_eq_square field_simps)
have "- 2 * s * (norm (z - u)) ^ 2 + - 2 * s * (norm (w - u)) ^ 2 =
- s * (norm (z - w)) ^ 2 + - (4 * s) * (norm (u - (z + w) / 2)) ^ 2"
using arg_cong[OF par, of "λx. - s * x"]
by (simp add: algebra_simps)
thus ?thesis
by (simp add: mult_exp_exp)
qed
lemma gauss_shift_nn:
fixes b :: real and m :: complex
assumes b: "0 < b"
shows "(∫⇧+ u. ennreal (exp (- b * (norm (u - m)) ^ 2)) ∂lborel) =
ennreal (pi / b)"
proof -
have mf: "(λu :: complex. ennreal (exp (- b * (norm (u - m)) ^ 2))) ∈
borel_measurable borel"
by simp
have "(∫⇧+ u. ennreal (exp (- b * (norm (u - m)) ^ 2)) ∂lborel) =
(∫⇧+ u. ennreal (exp (- b * (norm (u -
m)) ^ 2)) ∂(distr lborel borel ((+) m)))"
using lborel_distr_plus[of m]
by simp
also have "… = (∫⇧+ u. ennreal (exp (- b * (norm (m + u -
m)) ^ 2)) ∂lborel)"
using nn_integral_distr[of "(+) m" lborel borel "λu. ennreal (exp (- b * (norm (u -
m)) ^ 2))"] mf
by simp
also have "… = ennreal (pi / b)" using gauss_nn_C[OF b]
by simp
finally show ?thesis .
qed
lemma conv_nn:
fixes z w :: complex
assumes s: "0 < s"
shows "(∫⇧+ u. ennreal (exp (- 2 * s * (norm (z - u)) ^ 2) * exp (- 2 * s *
(norm (w - u)) ^ 2)) ∂lborel) =
ennreal (pi / (4 * s) * exp (- s * (norm (z - w)) ^ 2))"
proof -
have s4: "0 < 4 * s" using s
by simp
have "(∫⇧+ u. ennreal (exp (- 2 * s * (norm (z - u)) ^ 2) * exp (- 2 * s *
(norm (w - u)) ^ 2)) ∂lborel)
= (∫⇧+ u. ennreal (exp (- s * (norm (z - w)) ^ 2)) * ennreal (exp (- (4 * s) *
(norm (u - (z + w) / 2)) ^ 2)) ∂lborel)"
unfolding par_exp
by (simp add: ennreal_mult)
also have "… = ennreal (exp (- s * (norm (z - w)) ^ 2)) *
(∫⇧+ u. ennreal (exp (- (4 * s) * (norm (u - (z + w) /
2)) ^ 2)) ∂lborel)"
by (simp add: nn_integral_cmult)
also have "… = ennreal (exp (- s * (norm (z - w)) ^ 2)) * ennreal (pi / (4 * s))"
unfolding gauss_shift_nn[OF s4] ..
also have "… = ennreal (pi / (4 * s) * exp (- s * (norm (z - w)) ^ 2))" using s
by (simp add: ennreal_mult["symmetric"] mult_ac)
finally show ?thesis .
qed
text ‹Gaussian kernels have nonnegative energy:
@{text "E(e^{-s|p_1 - p_2|^2}) = (4s/π) ∫ (Φ_1 - Φ_2)^2 ≥ 0"}.›
lemma gauss_pair_nn:
fixes μ ν :: "complex measure"
assumes fm: "finite_measure μ" and fn: "finite_measure ν" and sm: "sets μ =
sets borel" and sn: "sets ν = sets borel" and s: "0 < s"
shows "(∫⇧+ u. ennreal (gPhi s μ u * gPhi s ν u) ∂lborel) =
ennreal (pi / (4 * s)) * (∫⇧+ z. ∫⇧+ w. ennreal (exp (- s *
(norm (z - w)) ^ 2)) ∂ν ∂μ)"
proof -
have s0: "0 ≤ s" using s
by simp
have sfm: "sigma_finite_measure μ" using fm
by (simp add: finite_measure_def)
have sfn: "sigma_finite_measure ν" using fn
by (simp add: finite_measure_def)
have p1: "pair_sigma_finite μ (lborel :: complex measure)" using sfm
by (simp add: pair_sigma_finite_def sigma_finite_lborel)
have p2: "pair_sigma_finite ν (lborel :: complex measure)" using sfn
by (simp add: pair_sigma_finite_def sigma_finite_lborel)
have S1: "ennreal (gPhi s μ u * gPhi s ν u) =
(∫⇧+ z. ∫⇧+ w. ennreal (exp (- 2 * s * (norm (z - u)) ^ 2)) *
ennreal (exp (- 2 * s * (norm (w - u)) ^ 2)) ∂ν ∂μ)" for u :: complex
proof -
have mf: "(λz. ennreal (exp (- 2 * s * (norm (z - u)) ^ 2))) ∈
borel_measurable μ" unfolding measurable_cong_sets[OF sm refl]
by simp
have mg: "(λw. ennreal (exp (- 2 * s * (norm (w - u)) ^ 2))) ∈
borel_measurable ν" unfolding measurable_cong_sets[OF sn refl]
by simp
have "ennreal (gPhi s μ u * gPhi s ν u) =
ennreal (gPhi s μ u) * ennreal (gPhi s ν u)" using gPhi_nonneg
by (simp add: ennreal_mult)
also have "… = (∫⇧+ z. ennreal (exp (- 2 * s * (norm (z -
u)) ^ 2)) ∂μ) * (∫⇧+ w. ennreal (exp (- 2 * s * (norm (w -
u)) ^ 2)) ∂ν)"
unfolding gPhi_nn[OF fm sm s0] gPhi_nn[OF fn sn s0] ..
also have "… = (∫⇧+ z. ennreal (exp (- 2 * s * (norm (z - u)) ^ 2)) *
(∫⇧+ w. ennreal (exp (- 2 * s * (norm (w -
u)) ^ 2)) ∂ν) ∂μ)"
using nn_integral_multc[OF mf, of "∫⇧+ w. ennreal (exp (- 2 * s * (norm (w -
u)) ^ 2)) ∂ν"]
by simp
also have "… = (∫⇧+ z. ∫⇧+ w. ennreal (exp (- 2 * s *
(norm (z - u)) ^ 2)) * ennreal (exp (- 2 * s * (norm (w -
u)) ^ 2)) ∂ν ∂μ)"
using nn_integral_cmult[OF mg]
by simp
finally show ?thesis .
qed
have m1: "(λ(z, u). ∫⇧+ w. ennreal (exp (- 2 * s * (norm (z - u)) ^ 2)) *
ennreal (exp (- 2 * s * (norm (w - u)) ^ 2)) ∂ν) ∈
borel_measurable (μ ⨂⇩M lborel)"
proof -
have jm0: "(λp :: (complex × complex) × complex. ennreal (exp (- 2 * s *
(norm (fst (fst p) - snd (fst p))) ^ 2)) * ennreal (exp (- 2 * s * (norm (snd p -
snd (fst p))) ^ 2))) ∈ borel_measurable ((borel ⨂⇩M lborel)
⨂⇩M borel)"
by simp
have e: "(λ((z :: complex, u :: complex),
w :: complex). ennreal (exp (- 2 * s * (norm (z - u)) ^ 2)) * ennreal (exp (- 2 * s *
(norm (w - u)) ^ 2))) = (λp. ennreal (exp (- 2 * s * (norm (fst (fst p) -
snd (fst p))) ^ 2)) * ennreal (exp (- 2 * s * (norm (snd p - snd (fst p))) ^ 2)))"
by (simp add: fun_eq_iff)
have jm: "(λ((z, u), w). ennreal (exp (- 2 * s * (norm (z - u)) ^ 2)) *
ennreal (exp (- 2 * s * (norm (w - u)) ^ 2))) ∈
borel_measurable ((μ ⨂⇩M lborel) ⨂⇩M ν)"
unfolding measurable_cong_sets[OF sets_pair_measure_cong[OF sets_pair_measure_cong[OF sm refl]
sn] refl]
unfolding e using jm0 .
show ?thesis using sigma_finite_measure.borel_measurable_nn_integral[OF sfn, of "λ(z,
u) w. ennreal (exp (- 2 * s * (norm (z - u)) ^ 2)) * ennreal (exp (- 2 * s * (norm (w -
u)) ^ 2))" "μ ⨂⇩M lborel"] jm
by (simp add: split_beta case_prod_beta)
qed
have m2: "(λ(w, u). ennreal (exp (- 2 * s * (norm (z - u)) ^ 2)) * ennreal (exp (- 2 * s *
(norm (w - u)) ^ 2))) ∈ borel_measurable (ν ⨂⇩M lborel)" for z :: complex
unfolding measurable_cong_sets[OF sets_pair_measure_cong[OF sn refl] refl]
by simp
have "(∫⇧+ u. ennreal (gPhi s μ u * gPhi s ν u) ∂lborel) =
(∫⇧+ u. ∫⇧+ z. ∫⇧+ w. ennreal (exp (- 2 * s *
(norm (z - u)) ^ 2)) * ennreal (exp (- 2 * s * (norm (w -
u)) ^ 2)) ∂ν ∂μ ∂lborel)"
unfolding S1 ..
also have "… = (∫⇧+ z. ∫⇧+ u. ∫⇧+ w. ennreal
(exp (- 2 * s * (norm (z - u)) ^ 2)) * ennreal (exp (- 2 * s * (norm (w -
u)) ^ 2)) ∂ν ∂lborel ∂μ)"
using pair_sigma_finite.Fubini'[OF p1 m1]
by simp
also have "… = (∫⇧+ z. ∫⇧+ w. ∫⇧+ u. ennreal
(exp (- 2 * s * (norm (z - u)) ^ 2)) * ennreal (exp (- 2 * s * (norm (w -
u)) ^ 2)) ∂lborel ∂ν ∂μ)"
proof (rule nn_integral_cong)
fix z assume "z ∈ space μ"
show "(∫⇧+ u. ∫⇧+ w. ennreal (exp (- 2 * s * (norm (z -
u)) ^ 2)) * ennreal (exp (- 2 * s * (norm (w - u)) ^ 2)) ∂ν ∂lborel) =
(∫⇧+ w. ∫⇧+ u. ennreal (exp (- 2 * s * (norm (z - u)) ^ 2)) *
ennreal (exp (- 2 * s * (norm (w - u)) ^ 2)) ∂lborel ∂ν)"
using pair_sigma_finite.Fubini'[OF p2 m2[of z]]
by simp
qed
also have "… = (∫⇧+ z. ∫⇧+ w. ennreal (pi / (4 * s)) *
ennreal (exp (- s * (norm (z - w)) ^ 2)) ∂ν ∂μ)"
proof -
have c: "(∫⇧+ u. ennreal (exp (- 2 * s * (norm (z - u)) ^ 2)) *
ennreal (exp (- 2 * s * (norm (w - u)) ^ 2)) ∂lborel) =
ennreal (pi / (4 * s)) * ennreal (exp (- s * (norm (z - w)) ^ 2))" for z w :: complex
using conv_nn[OF s, of z w] s
by (simp add: ennreal_mult["symmetric"])
show ?thesis unfolding c ..
qed
also have "… = ennreal (pi / (4 * s)) *
(∫⇧+ z. ∫⇧+ w. ennreal (exp (- s * (norm (z -
w)) ^ 2)) ∂ν ∂μ)"
proof -
have in1: "(∫⇧+ w. ennreal (pi / (4 * s)) * ennreal (exp (- s * (norm (z -
w)) ^ 2)) ∂ν) = ennreal (pi / (4 * s)) *
(∫⇧+ w. ennreal (exp (- s * (norm (z - w)) ^ 2)) ∂ν)"
for z :: complex
using nn_integral_cmult[of "λw. ennreal (exp (- s * (norm (z -
w)) ^ 2))" ν "ennreal (pi / (4 * s))"] unfolding measurable_cong_sets[OF sn refl]
by simp
have jm: "(λ(z, w). ennreal (exp (- s * (norm (z - w)) ^ 2))) ∈
borel_measurable (μ ⨂⇩M ν)"
unfolding measurable_cong_sets[OF sets_pair_measure_cong[OF sm sn] refl]
by simp
have mz: "(λz. ∫⇧+ w. ennreal (exp (- s * (norm (z -
w)) ^ 2)) ∂ν) ∈ borel_measurable μ"
using sigma_finite_measure.borel_measurable_nn_integral[OF sfn jm] .
show ?thesis unfolding in1 using nn_integral_cmult[OF mz, of "ennreal (pi / (4 * s))"] .
qed
finally show ?thesis .
qed
lemma gauss_pair:
assumes "finite_measure μ" "finite_measure ν" "sets μ = sets borel" "sets ν =
sets borel" "0 < s"
shows "integral⇧L (μ ⨂⇩M ν) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2)) = 4 * s / pi * integral⇧L lborel (λu. gPhi s μ u *
gPhi s ν u)"
proof -
have sfn: "sigma_finite_measure ν" using assms(2)
by (simp add: finite_measure_def)
have gm: "(λp :: complex × complex. exp (- s * (norm (fst p - snd p)) ^ 2)) ∈
borel_measurable (μ ⨂⇩M ν)"
unfolding measurable_cong_sets[OF sets_pair_measure_cong[OF assms(3,4)] refl]
by simp
have X: "(∫⇧+ p. ennreal (exp (- s * (norm (fst p -
snd p)) ^ 2)) ∂(μ ⨂⇩M ν)) =
(∫⇧+ z. ∫⇧+ w. ennreal (exp (- s * (norm (z -
w)) ^ 2)) ∂ν ∂μ)"
using sigma_finite_measure.nn_integral_fst[OF sfn,
of "λp. ennreal (exp (- s * (norm (fst p - snd p)) ^ 2))" μ] gm
by simp
have L: "integral⇧L (μ ⨂⇩M ν) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2)) = enn2real (∫⇧+ z. ∫⇧+ w. ennreal (exp (- s *
(norm (z - w)) ^ 2)) ∂ν ∂μ)"
unfolding X[symmetric] using integral_eq_nn_integral[OF gm]
by simp
have pm: "(λu. gPhi s μ u * gPhi s ν u) ∈ borel_measurable lborel"
using gPhi_meas[OF assms(1,3)] gPhi_meas[OF assms(2,4)]
by simp
have R: "integral⇧L lborel (λu. gPhi s μ u * gPhi s ν u) =
enn2real (∫⇧+ u. ennreal (gPhi s μ u * gPhi s ν u) ∂lborel)"
using integral_eq_nn_integral[OF pm] gPhi_nonneg
by simp
show ?thesis unfolding L R gauss_pair_nn[OF assms] using assms(5)
by (simp add: enn2real_mult)
qed
lemma gPhi_prod_int:
fixes μ ν :: "complex measure"
assumes fm: "finite_measure μ" and fn: "finite_measure ν" and sm: "sets μ =
sets borel" and sn: "sets ν = sets borel" and s: "0 < s"
shows "integrable lborel (λu. gPhi s μ u * gPhi s ν u)"
proof -
have m: "(λu. gPhi s μ u * gPhi s ν u) ∈ borel_measurable lborel"
using gPhi_meas[OF fm sm] gPhi_meas[OF fn sn]
by simp
have le1: "(∫⇧+ w. ennreal (exp (- s * (norm (z - w)) ^ 2)) ∂ν) ≤
emeasure ν (space ν)" for z :: complex
proof -
have "(∫⇧+ w. ennreal (exp (- s * (norm (z - w)) ^ 2)) ∂ν) ≤
(∫⇧+ w. 1 ∂ν)" using s
by (fastforce intro: nn_integral_mono)
thus ?thesis
by simp
qed
have le2: "(∫⇧+ z. ∫⇧+ w. ennreal (exp (- s * (norm (z -
w)) ^ 2)) ∂ν ∂μ) ≤
(∫⇧+ z. emeasure ν (space ν) ∂μ)"
using le1
by (blast intro: nn_integral_mono)
have "emeasure ν (space ν) ≠ ∞" using fn
by (simp add: finite_measure.emeasure_finite)
moreover have "emeasure μ (space μ) ≠ ∞" using fm
by (simp add: finite_measure.emeasure_finite)
ultimately have fin: "(∫⇧+ z. emeasure ν (space ν) ∂μ) <
∞"
by (simp add: ennreal_mult_less_top less_top)
have fin2: "(∫⇧+ u. ennreal (gPhi s μ u * gPhi s ν u) ∂lborel) <
∞"
proof -
have fin3: "(∫⇧+ z. ∫⇧+ w. ennreal (exp (- s * (norm (z -
w)) ^ 2)) ∂ν ∂μ) < ∞" using le2 fin
by simp
show ?thesis unfolding gauss_pair_nn[OF fm fn sm sn s] using fin3
by (simp add: ennreal_mult_less_top less_top)
qed
have e: "(λu. ennreal (norm (gPhi s μ u * gPhi s ν u))) =
(λu. ennreal (gPhi s μ u * gPhi s ν u))" using gPhi_nonneg
by (simp add: fun_eq_iff)
show ?thesis unfolding integrable_iff_bounded e using m fin2
by simp
qed
lemma Eform_gauss_nonneg:
assumes "finite_measure ν1" "finite_measure ν2" "sets ν1 = sets borel" "sets ν2 =
sets borel" "0 < s"
shows "0 ≤ Eform ν1 ν2 (λp. exp (- s * (norm (fst p - snd p)) ^ 2))"
proof -
have i11: "integrable lborel (λu. gPhi s ν1 u * gPhi s ν1 u)"
by (rule gPhi_prod_int[OF assms(1,1,3,3,5)])
have i12: "integrable lborel (λu. gPhi s ν1 u * gPhi s ν2 u)"
by (rule gPhi_prod_int[OF assms(1,2,3,4,5)])
have i22: "integrable lborel (λu. gPhi s ν2 u * gPhi s ν2 u)"
by (rule gPhi_prod_int[OF assms(2,2,4,4,5)])
have "Eform ν1 ν2 (λp. exp (- s * (norm (fst p - snd p)) ^ 2)) =
4 * s / pi * (integral⇧L lborel (λu. gPhi s ν1 u * gPhi s ν1 u) - 2 *
integral⇧L lborel (λu. gPhi s ν1 u * gPhi s ν2 u) +
integral⇧L lborel (λu. gPhi s ν2 u * gPhi s ν2 u))"
unfolding Eform_def gauss_pair[OF assms(1,1,3,3,5)] gauss_pair[OF assms(1,2,3,4,5)]
gauss_pair[OF assms(2,2,4,4,5)]
by (simp add: algebra_simps)
also have "integral⇧L lborel (λu. gPhi s ν1 u * gPhi s ν1 u) - 2 *
integral⇧L lborel (λu. gPhi s ν1 u * gPhi s ν2 u) +
integral⇧L lborel (λu. gPhi s ν2 u * gPhi s ν2 u) =
integral⇧L lborel (λu. (gPhi s ν1 u - gPhi s ν2 u) ^ 2)"
proof -
have "integral⇧L lborel (λu. (gPhi s ν1 u - gPhi s ν2 u) ^ 2) =
integral⇧L lborel (λu. gPhi s ν1 u * gPhi s ν1 u - 2 *
(gPhi s ν1 u * gPhi s ν2 u) + gPhi s ν2 u * gPhi s ν2 u)"
by (simp add: power2_eq_square algebra_simps)
also have "… = integral⇧L lborel (λu. gPhi s ν1 u * gPhi s ν1 u) -
2 * integral⇧L lborel (λu. gPhi s ν1 u * gPhi s ν2 u) +
integral⇧L lborel (λu. gPhi s ν2 u * gPhi s ν2 u)"
using i11 i12 i22
by (simp add: Bochner_Integration.integral_diff Bochner_Integration.integral_add)
finally show ?thesis ..
qed
finally have E: "Eform ν1 ν2 (λp. exp (- s * (norm (fst p - snd p)) ^ 2)) =
4 * s / pi * integral⇧L lborel (λu. (gPhi s ν1 u - gPhi s ν2 u) ^ 2)" .
have "0 ≤ integral⇧L lborel (λu. (gPhi s ν1 u - gPhi s ν2 u) ^ 2)"
by simp
thus ?thesis unfolding E using assms(5)
by (simp add: zero_le_mult_iff)
qed
text ‹Frullani-type kernel: @{text "K_n(p) =
(1/2)(∫_{1/(n+1)}^{n+1} e^{-s}/s ds - ∫_{1/(n+1)}^{n+1} e^{-s|p_1 -
p_2|^2}/s ds) ⟶ log|p_1 - p_2|"}.›
definition Kn :: "nat ⇒ complex × complex ⇒ real" where
"Kn n p = 1 / 2 * (interval_lebesgue_integral lborel (ereal (1 / (real n + 1))) (ereal (real n +
1)) (λs. exp (- s) / s)
- interval_lebesgue_integral lborel (ereal (1 / (real n + 1))) (ereal (real n +
1)) (λs. exp (- s * (norm (fst p - snd p)) ^ 2) / s))"
text ‹Helpers on @{text "∫ e^{-u}/u du"} for the kernels @{text "K_n"}.›
lemma ed_int:
fixes x y :: real
assumes "0 < x" "0 < y"
shows "interval_lebesgue_integrable lborel (ereal x) (ereal y) (λu. exp (- u) / u)"
and "interval_lebesgue_integrable lborel (ereal x) (ereal y) (λu. 1 / u)"
proof -
have p: "0 < u" if "min x y ≤ u" for u using that assms
by simp
show "interval_lebesgue_integrable lborel (ereal x) (ereal y) (λu. exp (- u) / u)"
by (rule interval_integrable_isCont) (use p in ‹auto intro!: continuous_intros›)
show "interval_lebesgue_integrable lborel (ereal x) (ereal y) (λu. 1 / u)"
by (rule interval_integrable_isCont) (use p in ‹auto intro!: continuous_intros›)
qed
lemma inv_ftc:
fixes x y :: real
assumes x: "0 < x" and y: "0 < y"
shows "interval_lebesgue_integral lborel (ereal (x)) (ereal (y)) (λu. 1 / u) =
ln y - ln x"
proof (rule interval_integral_FTC_finite)
show "continuous_on {min x y..max x y} (λu. 1 / u)" using x y
by (force intro: continuous_intros)
fix u assume "min x y ≤ u" "u ≤ max x y"
hence u: "0 < u" using x y
by simp
show "(ln has_vector_derivative 1 / u) (at u within {min x y..max x y})"
using has_vector_derivative_at_within[OF DERIV_ln_divide[OF u,
unfolded has_real_derivative_iff_has_vector_derivative]]
by simp
qed
lemma ed_le:
fixes x y :: real
assumes x: "0 < x" and xy: "x ≤ y"
shows "0 ≤ interval_lebesgue_integral lborel (ereal (x)) (ereal (y)) (λu. exp (- u) /
u)" and "interval_lebesgue_integral lborel (ereal (x)) (ereal (y)) (λu. exp (- u) /
u) ≤ ln y - ln x"
proof -
have y: "0 < y" using x xy
by simp
have e1: "interval_lebesgue_integral lborel (ereal (x)) (ereal (y)) (λu. exp (- u) / u) =
set_lebesgue_integral lborel {x<..<y} (λu. exp (- u) / u)"
using xy
by (simp add: interval_lebesgue_integral_le_eq)
have e2: "interval_lebesgue_integral lborel (ereal (x)) (ereal (y)) (λu. 1 / u) =
set_lebesgue_integral lborel {x<..<y} (λu. 1 / u)"
using xy
by (simp add: interval_lebesgue_integral_le_eq)
have i1: "set_integrable lborel {x<..<y} (λu. exp (- u) / u)" using ed_int(1)[OF x y] xy
by (simp add: interval_lebesgue_integrable_def)
have i2: "set_integrable lborel {x<..<y} (λu. 1 / u)" using ed_int(2)[OF x y] xy
by (simp add: interval_lebesgue_integrable_def)
have pt: "exp (- u) / u ≤ 1 / u" if "u ∈ {x<..<y}" for u
proof -
have u: "0 < u" using that x
by simp
show ?thesis using u
by (simp add: divide_right_mono)
qed
show "0 ≤ interval_lebesgue_integral lborel (ereal (x)) (ereal (y)) (λu. exp (- u) /
u)" unfolding e1 set_lebesgue_integral_def using x
using Bochner_Integration.integral_nonneg by (simp add: indicator_def)
show "interval_lebesgue_integral lborel (ereal (x)) (ereal (y)) (λu. exp (- u) / u) ≤
ln y - ln x" unfolding e1 inv_ftc[OF x y, symmetric] e2
using set_integral_mono[OF i1 i2 pt] .
qed
lemma ed_abs:
fixes x r :: real
assumes x: "0 < x" and r: "0 < r"
shows "¦interval_lebesgue_integral lborel (ereal (x)) (ereal (x *
r)) (λu. exp (- u) / u)¦ ≤ ¦ln r¦"
proof -
have xr: "0 < x * r" using x r
by simp
have l: "ln (x * r) = ln x + ln r" using x r
by (simp add: ln_mult)
show ?thesis
proof (cases "1 ≤ r")
case True
have "x ≤ x * r" using True x
by simp
thus ?thesis using ed_le[OF x] l True
by force
next
case False
have "x * r ≤ x" using False x
by simp
hence "0 ≤ interval_lebesgue_integral lborel (ereal (x *
r)) (ereal (x)) (λu. exp (- u) /
u)" and "interval_lebesgue_integral lborel (ereal (x *
r)) (ereal (x)) (λu. exp (- u) / u) ≤ ln x - ln (x * r)"
using ed_le[OF xr] by auto
thus ?thesis using interval_integral_endpoints_reverse[of "ereal x" "ereal (x *
r)" "λu. exp (- u) / u"] l False r
by simp
qed
qed
lemma lbint_bound:
fixes x y C :: real and g :: "real ⇒ real"
assumes gi: "interval_lebesgue_integrable lborel (ereal x) (ereal y) g" and b: "⋀u. min x y
≤ u ⟹ u ≤ max x y ⟹ ¦g u¦ ≤ C"
shows "¦interval_lebesgue_integral lborel (ereal (x)) (ereal (y)) (g)¦ ≤
C * ¦y - x¦"
proof -
have aux: "¦interval_lebesgue_integral lborel (ereal (a)) (ereal (c)) (g)¦ ≤
C * (c - a)"
if ac: "a ≤ c" and ga: "interval_lebesgue_integrable lborel (ereal a) (ereal c) g" and ba:
"⋀u. a ≤ u ⟹ u ≤ c ⟹ ¦g u¦ ≤ C"
for a c
proof -
have e: "interval_lebesgue_integral lborel (ereal (a)) (ereal (c)) (h) =
set_lebesgue_integral lborel {a<..<c} h" for h :: "real ⇒ real" using ac
by (simp add: interval_lebesgue_integral_le_eq)
have ig: "set_integrable lborel {a<..<c} g" using ga ac
by (simp add: interval_lebesgue_integrable_def)
have ic: "set_integrable lborel {a<..<c} (λ_. k)" for k :: real
using interval_integral_const(1)[of a c k] ac
by (simp add: interval_lebesgue_integrable_def)
have vc: "set_lebesgue_integral lborel {a<..<c} (λ_. k) = k * (c - a)" for k :: real
using interval_integral_const(2)[of a c k] e[of "λ_. k"]
by simp
have up: "set_lebesgue_integral lborel {a<..<c} g ≤
set_lebesgue_integral lborel {a<..<c} (λ_. C)"
proof (rule set_integral_mono[OF ig ic])
fix u assume "u ∈ {a<..<c}"
thus "g u ≤ C" using ba[of u]
by simp
qed
have lo: "set_lebesgue_integral lborel {a<..<c} (λ_. - C) ≤
set_lebesgue_integral lborel {a<..<c} g"
proof (rule set_integral_mono[OF ic ig])
fix u assume "u ∈ {a<..<c}"
thus "- C ≤ g u" using ba[of u]
by simp
qed
show ?thesis unfolding e using up lo vc[of C] vc[of "- C"]
by (simp add: abs_le_iff)
qed
show ?thesis
proof (cases "x ≤ y")
case True
show ?thesis using aux[OF True gi] b True
by simp
next
case False
have gi': "interval_lebesgue_integrable lborel (ereal y) (ereal x) g"
using gi interval_integrable_endpoints_reverse
by auto
have "¦interval_lebesgue_integral lborel (ereal (y)) (ereal (x)) (g)¦ ≤
C * (x - y)" using aux[OF _ gi'] b False
by simp
thus ?thesis using interval_integral_endpoints_reverse[of "ereal x" "ereal y" g] False
by simp
qed
qed
lemma Kn_eq:
assumes "fst p ≠ snd p"
shows "2 * Kn n p = interval_lebesgue_integral lborel (ereal (1 / (real n + 1))) (ereal (1 /
(real n + 1) * (norm (fst p - snd p)) ^ 2)) (λu. exp (- u) / u) -
interval_lebesgue_integral lborel (ereal (real n + 1)) (ereal ((real n + 1) * (norm (fst p -
snd p)) ^ 2)) (λu. exp (- u) / u)"
proof -
define a :: real where "a = 1 / (real n + 1)"
define b :: real where "b = real n + 1"
define r :: real where "r = (norm (fst p - snd p)) ^ 2"
have r0: "0 < r" unfolding r_def using assms
by simp
have a0: "0 < a" unfolding a_def
by simp
have b0: "0 < b" unfolding b_def
by simp
have ab: "a ≤ b"
proof -
have one: "1 ≤ real n + 1"
by simp
have "1 / (real n + 1) ≤ 1" using one
by simp
thus ?thesis unfolding a_def b_def using one
by linarith
qed
have ar: "0 < a * r" using a0 r0
by simp
have br: "0 < b * r" using b0 r0
by simp
have sub0: "interval_lebesgue_integral lborel (ereal (a)) (ereal (b)) (λx. r *⇩R exp
(- (x * r)) / (x * r)) = interval_lebesgue_integral lborel (ereal (a * r)) (ereal (b *
r)) (λu. exp (- u) / u)"
proof -
have d: "((λs. s * r) has_real_derivative r) (at x within {a..b})" for x
by (auto intro: derivative_eq_intros)
have img: "(λs. s * r) ` {a..b} ⊆ {0<..}" using a0 r0
by auto
have c0: "continuous_on {0<..} (λu :: real. exp (- u) / u)"
by (fast intro: continuous_intros)
have ci: "continuous_on ((λs. s * r) ` {a..b}) (λu. exp (- u) / u)"
using continuous_on_subset[OF c0 img] .
show ?thesis using interval_integral_substitution_finite[OF ab,
of "λs. s * r" "λ_. r" "λu. exp (- u) / u", OF d ci]
by simp
qed
have cg: "interval_lebesgue_integral lborel (ereal (a)) (ereal (b)) (λs. exp (- s * r) /
s) = interval_lebesgue_integral lborel (ereal (a)) (ereal (b)) (λx. r *⇩R exp (-
(x * r)) / (x * r))"
proof (rule interval_integral_cong)
fix x assume "x ∈ einterval (min (ereal a) (ereal b)) (max (ereal a) (ereal b))"
hence "0 < x" using a0 ab
by simp
thus "exp (- x * r) / x = r *⇩R exp (- (x * r)) / (x * r)" using r0
by (simp add: field_simps)
qed
have sum1: "interval_lebesgue_integral lborel (ereal (a)) (ereal (a * r)) (λu. exp (- u) /
u) + interval_lebesgue_integral lborel (ereal (a * r)) (ereal (b)) (λu. exp (- u) / u) =
interval_lebesgue_integral lborel (ereal (a)) (ereal (b)) (λu. exp (- u) / u)"
using interval_integral_sum[of "ereal a" "ereal (a * r)" "ereal b" "λu. exp (- u) /
u"] ed_int(1)[of "min a (min (a * r) b)" "max a (max (a * r) b)"] a0 ar b0
by simp
have sum2: "interval_lebesgue_integral lborel (ereal (a * r)) (ereal (b)) (λu. exp (- u) /
u) + interval_lebesgue_integral lborel (ereal (b)) (ereal (b * r)) (λu. exp (- u) / u) =
interval_lebesgue_integral lborel (ereal (a * r)) (ereal (b * r)) (λu. exp (- u) / u)"
using interval_integral_sum[of "ereal (a * r)" "ereal b" "ereal (b *
r)" "λu. exp (- u) / u"] ed_int(1)[of "min (a * r) (min b (b * r))" "max (a *
r) (max b (b * r))"] ar b0 br
by simp
have k: "2 * Kn n p = interval_lebesgue_integral lborel (ereal (a)) (ereal (b)) (λu. exp
(- u) / u) - interval_lebesgue_integral lborel (ereal (a)) (ereal (b)) (λs. exp (- s *
r) / s)"
unfolding Kn_def a_def b_def r_def
by simp
have "2 * Kn n p = interval_lebesgue_integral lborel (ereal (a)) (ereal (a *
r)) (λu. exp (- u) / u) - interval_lebesgue_integral lborel (ereal (b)) (ereal (b *
r)) (λu. exp (- u) / u)"
unfolding k cg sub0 using sum1 sum2
by simp
thus ?thesis unfolding a_def b_def r_def .
qed
lemma ed_near:
fixes x r :: real
assumes x: "0 < x" and r: "0 < r"
shows "¦interval_lebesgue_integral lborel (ereal (x)) (ereal (x *
r)) (λu. exp (- u) / u) - ln r¦ ≤ x * ¦r - 1¦"
proof -
have xr: "0 < x * r" using x r
by simp
have l: "interval_lebesgue_integral lborel (ereal (x)) (ereal (x * r)) (λu. 1 / u) =
ln r" using inv_ftc[OF x xr] x r
by (simp add: ln_mult)
have d: "interval_lebesgue_integral lborel (ereal (x)) (ereal (x * r)) (λu. exp (- u) /
u) - interval_lebesgue_integral lborel (ereal (x)) (ereal (x * r)) (λu. 1 / u) =
interval_lebesgue_integral lborel (ereal (x)) (ereal (x * r)) (λu. exp (- u) / u - 1 /
u)"
using interval_lebesgue_integral_diff(2)[OF ed_int(1)[OF x xr] ed_int(2)[OF x xr]] ..
have di: "interval_lebesgue_integrable lborel (ereal x) (ereal (x * r)) (λu. exp (- u) /
u - 1 / u)"
using interval_lebesgue_integral_diff(1)[OF ed_int(1)[OF x xr] ed_int(2)[OF x xr]] .
have b: "¦exp (- u) / u - 1 / u¦ ≤ 1"
if "min x (x * r) ≤ u" "u ≤ max x (x * r)" for u
proof -
have u: "0 < u" using that x xr
by simp
have e1: "1 - u ≤ exp (- u)" using exp_ge_add_one_self[of "- u"]
by simp
have e2: "exp (- u) ≤ 1" using u
by simp
have "¦exp (- u) / u - 1 / u¦ = (1 - exp (- u)) / u" using u e2
by (simp add: field_simps)
also have "… ≤ 1" using u e1
by (simp add: divide_le_eq)
finally show ?thesis .
qed
have "¦interval_lebesgue_integral lborel (ereal (x)) (ereal (x * r)) (λu. exp (- u) /
u - 1 / u)¦ ≤ 1 * ¦x * r - x¦"
by (rule lbint_bound[OF di b])
moreover have "1 * ¦x * r - x¦ = x * ¦r - 1¦"
proof -
have "x * r - x = x * (r - 1)"
by (simp add: algebra_simps)
thus ?thesis using x
by (simp add: abs_mult)
qed
ultimately show ?thesis unfolding d[symmetric] l
by simp
qed
lemma ed_far:
fixes b r :: real
assumes b: "0 < b" and r: "0 < r"
shows "¦interval_lebesgue_integral lborel (ereal (b)) (ereal (b *
r)) (λu. exp (- u) / u)¦ ≤ ¦r - 1¦ / (b * (min 1 r) ^ 2)"
proof -
have br: "0 < b * r" using b r
by simp
have m0: "0 < b * min 1 r" using b r
by simp
have bd: "¦exp (- u) / u¦ ≤ 1 / (b * min 1 r) ^ 2"
if "min b (b * r) ≤ u" "u ≤ max b (b * r)" for u
proof -
have mu: "b * min 1 r ≤ u" using that b r
by (auto simp: min_def)
have u: "0 < u" using mu m0
by simp
have e1: "exp (- u) ≤ 1 / u"
proof -
have "u ≤ exp u" using exp_ge_add_one_self[of u]
by linarith
thus ?thesis using u
by (simp add: exp_minus field_simps)
qed
have "¦exp (- u) / u¦ = exp (- u) / u" using u
by simp
also have "… ≤ 1 / u / u" using e1 u
using divide_right_mono[OF e1, of u] by simp
also have "… = 1 / u ^ 2"
by (simp add: power2_eq_square)
also have "… ≤ 1 / (b * min 1 r) ^ 2"
using power_mono[OF mu less_imp_le[OF m0], of 2] m0
using u mu m0 by (metis ‹1 / u / u =
1 / u⇧2› pos_divide_le_eq pos_le_divide_eq power2_eq_square
times_divide_eq_left mult_1 zero_compare_simps(6))
finally show ?thesis .
qed
have "¦interval_lebesgue_integral lborel (ereal (b)) (ereal (b * r)) (λu. exp (- u) /
u)¦ ≤ 1 / (b * min 1 r) ^ 2 * ¦b * r - b¦"
by (rule lbint_bound[OF ed_int(1)[OF b br] bd])
also have "… = ¦r - 1¦ / (b * (min 1 r) ^ 2)"
proof -
have "b * r - b = b * (r - 1)"
by (simp add: algebra_simps)
hence ab: "¦b * r - b¦ = b * ¦r - 1¦" using b
by (simp add: abs_mult)
show ?thesis unfolding ab using b
by (simp add: power2_eq_square field_simps)
qed
finally show ?thesis .
qed
lemma Kn_bound: "fst p ≠ snd p ⟹
¦Kn n p¦ ≤ 2 * ¦ln (norm (fst p - snd p))¦"
proof -
assume ne: "fst p ≠ snd p"
have r0: "0 < (norm (fst p - snd p)) ^ 2" using ne
by simp
have a0: "0 < 1 / (real n + 1)"
by simp
have b0: "0 < real n + 1"
by simp
have e: "2 * Kn n p = interval_lebesgue_integral lborel (ereal (1 / (real n + 1))) (ereal (1 /
(real n + 1) * (norm (fst p - snd p)) ^ 2)) (λu. exp (- u) / u) -
interval_lebesgue_integral lborel (ereal (real n + 1)) (ereal ((real n + 1) * (norm (fst p -
snd p)) ^ 2)) (λu. exp (- u) / u)" by (rule Kn_eq[OF ne])
have hA: "¦interval_lebesgue_integral lborel (ereal (1 / (real n + 1))) (ereal (1 / (real n +
1) * (norm (fst p - snd p)) ^ 2)) (λu. exp (- u) / u)¦ ≤
¦ln ((norm (fst p - snd p)) ^ 2)¦" by (rule ed_abs[OF a0 r0])
have hB: "¦interval_lebesgue_integral lborel (ereal (real n + 1)) (ereal ((real n + 1) *
(norm (fst p - snd p)) ^ 2)) (λu. exp (- u) / u)¦ ≤
¦ln ((norm (fst p - snd p)) ^ 2)¦" by (rule ed_abs[OF b0 r0])
have lr: "ln ((norm (fst p - snd p)) ^ 2) = 2 * ln (norm (fst p - snd p))"
by (simp add: ln_realpow)
show "¦Kn n p¦ ≤ 2 * ¦ln (norm (fst p - snd p))¦" using e hA hB
unfolding lr
by simp
qed
lemma Kn_tendsto: "fst p ≠ snd p ⟹
((λn. Kn n p) ⤏ ln (norm (fst p - snd p))) at_top"
proof -
assume ne: "fst p ≠ snd p"
define r where "r = (norm (fst p - snd p)) ^ 2"
define K where "K = (¦r - 1¦ + ¦r - 1¦ / (min 1 r) ^ 2) / 2"
have r0: "0 < r" unfolding r_def using ne
by simp
have lr: "ln r = 2 * ln (norm (fst p - snd p))" unfolding r_def
by (simp add: ln_realpow)
have bd: "norm (Kn n p - ln (norm (fst p - snd p))) ≤ K * inverse (real (Suc n))" for n
proof -
have a0: "0 < 1 / (real n + 1)"
by simp
have b0: "0 < real n + 1"
by simp
have e: "2 * Kn n p = interval_lebesgue_integral lborel (ereal (1 / (real n + 1))) (ereal (1 /
(real n + 1) * (norm (fst p - snd p)) ^ 2)) (λu. exp (- u) / u) -
interval_lebesgue_integral lborel (ereal (real n + 1)) (ereal ((real n + 1) * (norm (fst p -
snd p)) ^ 2)) (λu. exp (- u) / u)" by (rule Kn_eq[OF ne])
have hA: "¦interval_lebesgue_integral lborel (ereal (1 / (real n + 1))) (ereal (1 /
(real n + 1) * (norm (fst p - snd p)) ^ 2)) (λu. exp (- u) / u) - ln r¦ ≤
1 / (real n + 1) * ¦r - 1¦" using ed_near[OF a0 r0] unfolding r_def .
have hB: "¦interval_lebesgue_integral lborel (ereal (real n + 1)) (ereal ((real n + 1) *
(norm (fst p - snd p)) ^ 2)) (λu. exp (- u) / u)¦ ≤
¦r - 1¦ / ((real n + 1) * (min 1 r) ^ 2)" using ed_far[OF b0 r0] unfolding r_def .
have "¦Kn n p - ln (norm (fst p - snd p))¦ ≤
(1 / (real n + 1) * ¦r - 1¦ + ¦r - 1¦ / ((real n + 1) * (min 1 r) ^ 2)) /
2"
using e hA hB lr
by argo
also have "… = K * inverse (real (Suc n))"
proof -
have m: "0 < (min 1 r) ^ 2" using r0
by simp
have N: "inverse (real (Suc n)) = 1 / (real n + 1)"
by (simp add: inverse_eq_divide)
show ?thesis unfolding K_def N using m
using field_simps by argo
qed
finally show ?thesis
by simp
qed
have z: "((λn. K * inverse (real (Suc n))) ⤏ 0) sequentially"
using tendsto_mult_right_zero[OF LIMSEQ_inverse_real_of_nat, of K]
by simp
have ev: "eventually (λn. norm (Kn n p - ln (norm (fst p - snd p))) ≤
K * inverse (real (Suc n))) sequentially"
using bd by (simp add: always_eventually)
have "((λn. Kn n p - ln (norm (fst p - snd p))) ⤏ 0) sequentially"
using Lim_null_comparison[OF ev z] .
thus "((λn. Kn n p) ⤏ ln (norm (fst p - snd p))) sequentially"
by (simp add: LIM_zero_iff)
qed
lemma Kn_int_P:
fixes P :: "(complex × complex) measure"
assumes fP: "finite_measure P" and sP: "sets P = sets (borel ⨂⇩M borel)"
shows "integral⇧L P (Kn n) = 1 / 2 * (interval_lebesgue_integral lborel (ereal (1 /
(real n + 1))) (ereal (real n + 1)) (λs. exp (- s) / s) * measure P (space P) -
integral⇧L lborel (λs. indicator {1 / (real n + 1)<..<real n + 1} s / s *
integral⇧L P (λp. exp (- s * (norm (fst p - snd p)) ^ 2))))"
and "integrable lborel (λs. indicator {1 / (real n + 1)<..<real n + 1} s / s *
integral⇧L P (λp. exp (- s * (norm (fst p - snd p)) ^ 2)))"
proof -
define a :: real where "a = 1 / (real n + 1)"
define b :: real where "b = real n + 1"
define g where "g p s = indicator {a<..<b} s * (exp (- s * (norm (fst p - snd p)) ^ 2) / s)"
for p :: "complex × complex" and s :: real
have a0: "0 < a" unfolding a_def
by simp
have ab: "a ≤ b"
proof -
have one: "1 ≤ real n + 1"
by simp
have "1 / (real n + 1) ≤ 1" using one
by simp
thus ?thesis unfolding a_def b_def using one
by linarith
qed
have H: "interval_lebesgue_integral lborel (ereal a) (ereal b) (λs. exp (- s *
(norm (fst p - snd p)) ^ 2) / s) = integral⇧L lborel (g p)" for p
unfolding g_def using ab
by (simp add: interval_lebesgue_integral_le_eq set_lebesgue_integral_def)
have Kg: "Kn n p = 1 / 2 * (interval_lebesgue_integral lborel (ereal (1 / (real n +
1))) (ereal (real n + 1)) (λs. exp (- s) / s) - integral⇧L lborel (g p))" for p
unfolding Kn_def H[symmetric] a_def b_def ..
have "sigma_finite_measure P" using fP
by (simp add: finite_measure_def)
hence ps: "pair_sigma_finite P lborel"
by (simp add: pair_sigma_finite_def sigma_finite_lborel)
have gm: "(λx. g (fst x) (snd x)) ∈ borel_measurable (P ⨂⇩M lborel)"
unfolding g_def measurable_cong_sets[OF sets_pair_measure_cong[OF sP refl] refl]
by simp
have gb: "¦g p s¦ ≤ indicator {a<..<b} s * (1 / a)" for p s
proof (cases "s ∈ {a<..<b}")
case True
have s0: "0 < s" using True a0
by simp
have "exp (- s * (norm (fst p - snd p)) ^ 2) ≤ 1" using s0
by simp
hence "¦exp (- s * (norm (fst p - snd p)) ^ 2) / s¦ ≤ 1 / s" using s0
by (simp add: divide_right_mono)
also have "1 / s ≤ 1 / a" using True a0
by (simp add: divide_left_mono)
finally show ?thesis unfolding g_def using True
by simp
next
case False
thus ?thesis unfolding g_def
by simp
qed
have wint: "integrable (P ⨂⇩M lborel) (λx. indicator {a<..<b} (snd x) * (1 /
a))"
proof -
have m: "(λx. indicator {a<..<b} (snd x) * (1 / a)) ∈
borel_measurable (P ⨂⇩M lborel)"
unfolding measurable_cong_sets[OF sets_pair_measure_cong[OF sP refl] refl]
by simp
have e: "(∫⇧+ x. ennreal (norm (indicator {a<..<b} (snd x) * (1 /
a))) ∂(P ⨂⇩M lborel)) =
(∫⇧+ p. ∫⇧+ s. ennreal (indicator {a<..<b} s * (1 /
a)) ∂lborel ∂P)"
using lborel.nn_integral_fst[of "λx. ennreal (norm (indicator {a<..<b} (snd x) * (1 /
a)))" P] m a0
by (simp add: split_beta)
have i: "(∫⇧+ s. ennreal (indicator {a<..<b} s * (1 / a)) ∂lborel) =
ennreal (1 / a) * emeasure lborel {a<..<b}"
proof -
have eqf: "(λs. ennreal (indicator {a<..<b} s * (1 / a))) =
(λs. ennreal (1 / a) * indicator {a<..<b} s)"
by (simp add: fun_eq_iff indicator_def)
show ?thesis unfolding eqf
by (simp add: nn_integral_cmult_indicator)
qed
have f1: "emeasure lborel {a<..<b} ≠ ∞"
using ab by simp
have f2: "emeasure P (space P) ≠ ∞" using fP
by (simp add: finite_measure.emeasure_finite)
have "(∫⇧+ x. ennreal (norm (indicator {a<..<b} (snd x) * (1 /
a))) ∂(P ⨂⇩M lborel)) < ∞" unfolding e i using f1 f2
by (simp add: ennreal_mult_less_top less_top)
thus ?thesis unfolding integrable_iff_bounded using m
by simp
qed
have gint: "integrable (P ⨂⇩M lborel) (case_prod g)"
proof -
have gm': "(λ(x, y). g x y) ∈ borel_measurable (P ⨂⇩M lborel)"
using gm
by (simp add: split_beta)
have ae: "AE x in P ⨂⇩M lborel. norm (case x of (y, z) ⇒ g y z) ≤
norm (indicator {a<..<b} (snd x) * (1 / a) :: real)"
using gb a0 by (simp add: split_beta abs_mult)
show ?thesis using Bochner_Integration.integrable_bound[OF wint gm' ae] .
qed
have Fub: "integral⇧L lborel (λs. integral⇧L P (λp. g p s)) =
integral⇧L P (λp. integral⇧L lborel (g p))"
using pair_sigma_finite.Fubini_integral[OF ps gint]
by simp
have Hint: "integrable P (λp. integral⇧L lborel (g p))"
using pair_sigma_finite.integrable_fst'[OF ps gint]
by simp
have Sint: "integrable lborel (λs. integral⇧L P (λp. g p s))"
using pair_sigma_finite.integrable_snd[OF ps gint]
by simp
have inner: "integral⇧L P (λp. g p s) =
indicator {a<..<b} s / s * integral⇧L P (λp. exp (- s * (norm (fst p -
snd p)) ^ 2))" for s
unfolding g_def
by simp
have ci: "integrable P (λp. interval_lebesgue_integral lborel (ereal (1 / (real n +
1))) (ereal (real n + 1)) (λs. exp (- s) / s))" using fP
by (simp add: finite_measure.integrable_const)
show "integrable lborel (λs. indicator {1 / (real n + 1)<..<real n + 1} s / s *
integral⇧L P (λp. exp (- s * (norm (fst p - snd p)) ^ 2)))" using Sint
unfolding inner a_def b_def .
have "integral⇧L P (Kn n) = integral⇧L P (λp. 1 / 2 *
(interval_lebesgue_integral lborel (ereal (1 / (real n + 1))) (ereal (real n +
1)) (λs. exp (- s) / s) - integral⇧L lborel (g p)))"
unfolding Kg ..
also have "… = 1 / 2 * (interval_lebesgue_integral lborel (ereal (1 / (real n +
1))) (ereal (real n + 1)) (λs. exp (- s) / s) * measure P (space P) -
integral⇧L P (λp. integral⇧L lborel (g p)))"
using ci Hint
by (simp add: Bochner_Integration.integral_diff)
finally show "integral⇧L P (Kn n) =
1 / 2 * (interval_lebesgue_integral lborel (ereal (1 / (real n + 1))) (ereal (real n +
1)) (λs. exp (- s) / s) * measure P (space P) -
integral⇧L lborel (λs. indicator {1 / (real n + 1)<..<real n + 1} s / s *
integral⇧L P (λp. exp (- s * (norm (fst p - snd p)) ^ 2))))"
unfolding Fub[symmetric] inner a_def b_def .
qed
lemma Eform_Kn_nonpos:
assumes "finite_measure ν1" "finite_measure ν2" "sets ν1 = sets borel" "sets ν2 =
sets borel" "emeasure ν1 UNIV = emeasure ν2 UNIV"
shows "Eform ν1 ν2 (Kn n) ≤ 0"
proof -
have f11: "finite_measure (ν1 ⨂⇩M ν1)"
using finite_measure_pair_measure[OF assms(1,1)] .
have f12: "finite_measure (ν1 ⨂⇩M ν2)"
using finite_measure_pair_measure[OF assms(2,1)] .
have f22: "finite_measure (ν2 ⨂⇩M ν2)"
using finite_measure_pair_measure[OF assms(2,2)] .
have s11: "sets (ν1 ⨂⇩M ν1) = sets (borel ⨂⇩M borel)"
using sets_pair_measure_cong[OF assms(3,3)] .
have s12: "sets (ν1 ⨂⇩M ν2) = sets (borel ⨂⇩M borel)"
using sets_pair_measure_cong[OF assms(3,4)] .
have s22: "sets (ν2 ⨂⇩M ν2) = sets (borel ⨂⇩M borel)"
using sets_pair_measure_cong[OF assms(4,4)] .
have mP: "measure (μ ⨂⇩M ν) (space (μ ⨂⇩M ν)) =
measure μ (space μ) * measure ν (space ν)"
if "finite_measure μ" "finite_measure ν" for μ ν :: "complex measure"
proof -
have sf: "sigma_finite_measure ν" using that(2)
by (simp add: finite_measure_def)
have "emeasure (μ ⨂⇩M ν) (space μ × space ν) =
emeasure μ (space μ) * emeasure ν (space ν)"
using sigma_finite_measure.emeasure_pair_measure_Times[OF sf,
of "space μ" μ "space ν"]
by simp
thus ?thesis unfolding measure_def space_pair_measure
by (simp add: enn2real_mult)
qed
have "space ν1 = UNIV" using sets_eq_imp_space_eq[OF assms(3)]
by simp
moreover have "space ν2 = UNIV" using sets_eq_imp_space_eq[OF assms(4)]
by simp
ultimately have m12: "measure ν1 (space ν1) = measure ν2 (space ν2)"
using assms(5)
by (simp add: measure_def)
note I11 = Kn_int_P[OF f11 s11, of n] and I12 = Kn_int_P[OF f12 s12, of n] and I22 =
Kn_int_P[OF f22 s22, of n]
have nn: "0 ≤ integral⇧L lborel (λs. indicator {1 / (real n + 1)<..<real n +
1} s / s * (integral⇧L (ν1 ⨂⇩M ν1) (λp. exp (- s *
(norm (fst p - snd p)) ^ 2)) - 2 * integral⇧L (ν1 ⨂⇩M ν2)
(λp. exp (- s * (norm (fst p - snd p)) ^ 2)) +
integral⇧L (ν2 ⨂⇩M ν2) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2))))"
proof (rule Bochner_Integration.integral_nonneg)
fix s :: real
show "0 ≤ indicator {1 / (real n + 1)<..<real n + 1} s / s *
(integral⇧L (ν1 ⨂⇩M ν1) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2)) - 2 * integral⇧L (ν1 ⨂⇩M ν2) (λp. exp (- s *
(norm (fst p - snd p)) ^ 2)) + integral⇧L (ν2 ⨂⇩M ν2) (λp.
exp (- s * (norm (fst p - snd p)) ^ 2)))"
proof (cases "s ∈ {1 / (real n + 1)<..<real n + 1}")
case True
have p0: "0 < 1 / (real n + 1)"
by simp
have "1 / (real n + 1) < s" using True
by (simp add: greaterThanLessThan_iff)
hence s0: "0 < s" using p0
by linarith
have "0 ≤ Eform ν1 ν2 (λp. exp (- s * (norm (fst p - snd p)) ^ 2))"
by (rule Eform_gauss_nonneg[OF assms(1-4) s0])
thus ?thesis unfolding Eform_def using s0 True
by simp
next
case False
thus ?thesis
by simp
qed
qed
have split: "integral⇧L lborel (λs. indicator {1 / (real n + 1)<..<real n + 1} s /
s * integral⇧L (ν1 ⨂⇩M ν1) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2))) - 2 * integral⇧L lborel (λs. indicator {1 / (real n +
1)<..<real n + 1} s / s * integral⇧L (ν1 ⨂⇩M ν2) (λp. exp (-
s * (norm (fst p - snd p)) ^ 2))) + integral⇧L lborel (λs. indicator {1 /
(real n + 1)<..<real n + 1} s / s * integral⇧L (ν2 ⨂⇩M ν2)
(λp. exp (- s * (norm (fst p - snd p)) ^ 2)))
= integral⇧L lborel (λs. indicator {1 / (real n + 1)<..<real n + 1} s / s *
(integral⇧L (ν1 ⨂⇩M ν1) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2)) - 2 * integral⇧L (ν1 ⨂⇩M ν2) (λp. exp (- s
* (norm (fst p - snd p)) ^ 2)) +
integral⇧L (ν2 ⨂⇩M ν2) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2))))"
proof -
have a: "integral⇧L lborel (λs. indicator {1 / (real n + 1)<..<real n + 1} s / s *
integral⇧L (ν1 ⨂⇩M ν1) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2)) - 2 * (indicator {1 / (real n + 1)<..<real n + 1} s / s *
integral⇧L (ν1 ⨂⇩M ν2) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2))) + indicator {1 / (real n + 1)<..<real n + 1} s / s *
integral⇧L (ν2 ⨂⇩M ν2) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2))) = integral⇧L lborel (λs. indicator {1 / (real n + 1)<..<real n +
1} s / s * integral⇧L (ν1 ⨂⇩M ν1) (λp. exp (- s *
(norm (fst p - snd p)) ^ 2))) - 2 * integral⇧L lborel (λs. indicator {1 /
(real n + 1)<..<real n + 1} s / s *
integral⇧L (ν1 ⨂⇩M ν2) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2))) + integral⇧L lborel (λs. indicator {1 / (real n + 1)<..<real n +
1} s / s * integral⇧L (ν2 ⨂⇩M ν2) (λp. exp (- s *
(norm (fst p - snd p)) ^ 2)))"
using Bochner_Integration.integral_add[OF Bochner_Integration.integrable_diff[OF I11(2)
integrable_mult_right[where c = 2, OF I12(2)]] I22(2)]
Bochner_Integration.integral_diff[OF I11(2) integrable_mult_right[where c = 2, OF I12(2)]]
Bochner_Integration.integral_mult_right[where c = 2, OF I12(2)] by simp
have b: "(λs. indicator {1 / (real n + 1)<..<real n + 1} s / s *
integral⇧L (ν1 ⨂⇩M ν1) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2)) - 2 * (indicator {1 / (real n + 1)<..<real n + 1} s / s *
integral⇧L (ν1 ⨂⇩M ν2) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2))) + indicator {1 / (real n + 1)<..<real n + 1} s / s *
integral⇧L (ν2 ⨂⇩M ν2) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2))) = (λs. indicator {1 / (real n + 1)<..<real n + 1} s / s *
(integral⇧L (ν1 ⨂⇩M ν1) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2)) - 2 * integral⇧L (ν1 ⨂⇩M ν2) (λp. exp (- s *
(norm (fst p - snd p)) ^ 2)) + integral⇧L (ν2 ⨂⇩M ν2) (λp.
exp (- s * (norm (fst p - snd p)) ^ 2))))"
by (simp add: fun_eq_iff algebra_simps)
show ?thesis using a unfolding b by simp
qed
have "Eform ν1 ν2 (Kn n) = - 1 / 2 * (integral⇧L lborel (λs. indicator {1 /
(real n + 1)<..<real n + 1} s / s * integral⇧L (ν1 ⨂⇩M ν1)
(λp. exp (- s * (norm (fst p - snd p)) ^ 2))) - 2 *
integral⇧L lborel (λs. indicator {1 / (real n + 1)<..<real n + 1} s / s *
integral⇧L (ν1 ⨂⇩M ν2) (λp. exp (- s * (norm (fst p -
snd p)) ^ 2))) + integral⇧L lborel (λs. indicator {1 / (real n + 1)<..<real n +
1} s / s * integral⇧L (ν2 ⨂⇩M ν2) (λp. exp (- s *
(norm (fst p - snd p)) ^ 2))))"
unfolding Eform_def I11(1) I12(1) I22(1) mP[OF assms(1,1)] mP[OF assms(1,2)] mP[OF assms(2,2)]
m12
by (simp add: algebra_simps)
thus ?thesis unfolding split using nn
by simp
qed
text ‹Integrability passes to a smaller measure with the same sets.›
lemma integrable_le_measure:
fixes f :: "'a ⇒ real"
assumes PQ: "P ≤ Q" and s: "sets P = sets Q" and fi: "integrable Q f"
shows "integrable P f"
proof -
have m: "f ∈ borel_measurable P" using borel_measurable_integrable[OF fi]
measurable_cong_sets[OF s refl]
by auto
have le: "(∫⇧+ x. ennreal (norm (f x)) ∂P) ≤
(∫⇧+ x. ennreal (norm (f x)) ∂Q)"
using nn_integral_mono_measure[OF s PQ]
by simp
have "(∫⇧+ x. ennreal (norm (f x)) ∂Q) < ∞" using fi
unfolding integrable_iff_bounded
by simp
thus ?thesis using m le unfolding integrable_iff_bounded
by simp
qed
lemma Kn_meas: "Kn n ∈ borel_measurable (borel ⨂⇩M borel :: (complex ×
complex) measure)"
unfolding Kn_def interval_lebesgue_integral_def set_lebesgue_integral_def
by simp
text ‹Dominated convergence: @{text "∫ K_n dP ⟶
∫ log|p_1 - p_2| dP"} for @{text "P ≤
Q"} with @{text log} @{text Q}-integrable and the diagonal @{text Q}-null.›
lemma Kn_integral_tendsto:
assumes "P ≤ Q" "sets P = sets (borel ⨂⇩M borel)" "sets Q =
sets (borel ⨂⇩M borel)"
and "integrable Q (λp :: complex × complex. ln (norm (fst p -
snd p)))" "emeasure Q {p. fst p = snd p} = 0"
shows "((λn. integral⇧L P (Kn n)) ⤏ integral⇧L P
(λp. ln (norm (fst p - snd p)))) at_top"
proof -
define D where "D = {p :: complex × complex. fst p = snd p}"
have sPQ: "sets P = sets Q" using assms(2,3) by simp
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)
have Dm: "D ∈ sets P" unfolding D_def assms(2) eq using measurable_sets[OF mf, of "{0}"]
by simp
have "emeasure P D = 0" using le_measureD3[OF assms(1) sPQ, of D] assms(5) unfolding D_def
by simp
hence ns: "D ∈ null_sets P" using Dm
by (simp add: null_sets_def)
have AE_off: "AE p in P. fst p ≠ snd p"
using AE_I'[OF ns, of "λp. fst p ≠ snd p"] unfolding D_def
by auto
have intQ: "integrable Q (λp. 2 * ¦ln (norm (fst p - snd p))¦)" using assms(4)
by simp
have intP: "integrable P (λp. 2 * ¦ln (norm (fst p - snd p))¦)"
by (rule integrable_le_measure[OF assms(1) sPQ intQ])
have fm: "(λp. ln (norm (fst p - snd p))) ∈ borel_measurable P"
using borel_measurable_integrable[OF integrable_le_measure[OF assms(1) sPQ assms(4)]] .
have sm: "Kn n ∈ borel_measurable P" for n
using Kn_meas[of n] measurable_cong_sets[OF assms(2) refl]
by auto
have lim: "AE p in P. (λn. Kn n p) ⇢ ln (norm (fst p - snd p))"
using AE_off Kn_tendsto
by (auto elim: AE_mp)
have bd: "AE p in P. norm (Kn n p) ≤ 2 * ¦ln (norm (fst p - snd p))¦" for n
using AE_off Kn_bound
by (auto elim: AE_mp)
show ?thesis by (rule integral_dominated_convergence[OF fm sm intP lim bd])
qed
lemma finite_le_measure:
assumes "ν ≤ η" "sets ν = sets η" "finite_measure η"
shows "finite_measure ν"
proof (rule finite_measureI)
have fe: "emeasure η (space η) ≠ ∞" using assms(3)
by (simp add: finite_measure.emeasure_finite)
have le: "emeasure ν (space ν) ≤ emeasure η (space ν)"
using le_measureD3[OF assms(1,2)] .
have sp: "space ν = space η" using sets_eq_imp_space_eq[OF assms(2)] .
show "emeasure ν (space ν) ≠ ∞" using le fe unfolding sp
by (auto simp: top.extremum_unique)
qed
lemma pair_measure_mono:
assumes "ν ≤ η" "ν' ≤ η" "sets ν = sets borel" "sets ν' =
sets borel" "sets η = sets borel" "finite_measure η"
shows "(ν ⨂⇩M ν') ≤ (η ⨂⇩M η)"
proof -
have s1: "sets (ν ⨂⇩M ν') = sets (η ⨂⇩M η)"
using assms(3,4,5)
using sets_pair_measure_cong by simp
have sp: "space (ν ⨂⇩M ν') = space (η ⨂⇩M η)"
using sets_eq_imp_space_eq[OF s1] .
have "finite_measure ν'" using finite_le_measure[OF assms(2) _ assms(6)] assms(4,5)
by simp
hence sfn': "sigma_finite_measure ν'"
by (simp add: finite_measure_def)
have sfe: "sigma_finite_measure η" using assms(6)
by (simp add: finite_measure_def)
have em: "emeasure (ν ⨂⇩M ν') X ≤
emeasure (η ⨂⇩M η) X" for X
proof (cases "X ∈ sets (ν ⨂⇩M ν')")
case True
have X2: "X ∈ sets (η ⨂⇩M η)" using True s1
by simp
have "emeasure (ν ⨂⇩M ν') X =
(∫⇧+ x. ∫⇧+ y. indicator X (x,
y) ∂ν' ∂ν)"
using sigma_finite_measure.emeasure_pair_measure[OF sfn' True] .
also have "… ≤ (∫⇧+ x. ∫⇧+ y. indicator X (x,
y) ∂η ∂ν)"
using nn_integral_mono_measure[of ν' η] assms(2,4,5)
by (auto intro: nn_integral_mono)
also have "… ≤ (∫⇧+ x. ∫⇧+ y. indicator X (x,
y) ∂η ∂η)"
using nn_integral_mono_measure[of ν η] assms(1,3,5)
using nn_integral_mono by simp
also have "… = emeasure (η ⨂⇩M η) X"
using sigma_finite_measure.emeasure_pair_measure[OF sfe X2]
by simp
finally show ?thesis .
next
case False
have "emeasure (ν ⨂⇩M ν') X = 0" using False
by (simp add: emeasure_notin_sets)
thus ?thesis
by simp
qed
show ?thesis unfolding le_measure_iff using s1 sp em
by (simp add: le_fun_def)
qed
lemma logEnergyC_prod:
fixes μ ν :: "complex measure"
assumes fm: "finite_measure μ" and fn: "finite_measure ν" and int: "integrable (μ
⨂⇩M ν) (λp. ln (norm (fst p - snd p)))"
shows "logEnergyC μ ν = integral⇧L (μ ⨂⇩M ν) (λp. ln
(norm (fst p - snd p)))"
proof -
have ps: "pair_sigma_finite μ ν" using fm fn
by (simp add: pair_sigma_finite_def finite_measure_def)
show ?thesis unfolding logEnergyC_def using pair_sigma_finite.integral_fst'[OF ps int]
by simp
qed
theorem log_energy_zero_mass_nonpos:
fixes ν1 ν2 η :: "complex measure"
assumes "finite_measure η" "sets ν1 = sets borel" "sets ν2 =
sets borel" "sets η = sets borel"
and "ν1 ≤ η" "ν2 ≤ η" "emeasure ν1 UNIV = emeasure ν2 UNIV"
and "integrable (η ⨂⇩M η) (λzw. ln (norm (fst zw - snd zw)))"
and "emeasure (η ⨂⇩M η) {zw. fst zw = snd zw} = 0"
shows "logEnergyC ν1 ν1 - 2 * logEnergyC ν1 ν2 + logEnergyC ν2 ν2 ≤ 0"
proof -
have f1: "finite_measure ν1" and f2: "finite_measure ν2"
proof -
have fe: "emeasure η (space η) ≠ ∞" using assms(1)
by (simp add: finite_measure.emeasure_finite)
show "finite_measure ν1"
proof (rule finite_measureI)
have le: "emeasure ν1 (space ν1) ≤ emeasure η (space ν1)"
using le_measureD3[OF assms(5)] assms(2,4)
by simp
have sp: "space ν1 = space η" using sets_eq_imp_space_eq assms(2,4)
by auto
show "emeasure ν1 (space ν1) ≠ ∞" using le fe unfolding sp
by (auto simp: top.extremum_unique)
qed
show "finite_measure ν2"
proof (rule finite_measureI)
have le: "emeasure ν2 (space ν2) ≤ emeasure η (space ν2)"
using le_measureD3[OF assms(6)] assms(3,4)
by simp
have sp: "space ν2 = space η" using sets_eq_imp_space_eq assms(3,4)
by auto
show "emeasure ν2 (space ν2) ≠ ∞" using le fe unfolding sp
by (auto simp: top.extremum_unique)
qed
qed
have E: "logEnergyC ν1 ν1 - 2 * logEnergyC ν1 ν2 + logEnergyC ν2 ν2 =
Eform ν1 ν2 (λp. ln (norm (fst p - snd p)))"
proof -
have i: "integrable (μ ⨂⇩M ν) (λp. ln (norm (fst p - snd p)))"
if "μ ≤ η" "ν ≤ η" "sets μ = sets borel" "sets ν =
sets borel" for μ ν :: "complex measure"
proof (rule integrable_le_measure[OF pair_measure_mono[OF that assms(4,1)] _ assms(8)])
show "sets (μ ⨂⇩M ν) = sets (η ⨂⇩M η)"
using that assms(4)
using sets_pair_measure_cong by simp
qed
have e11: "logEnergyC ν1 ν1 =
integral⇧L (ν1 ⨂⇩M ν1) (λp. ln (norm (fst p - snd p)))"
by (rule logEnergyC_prod[OF f1 f1 i[OF assms(5,5,2,2)]])
have e12: "logEnergyC ν1 ν2 =
integral⇧L (ν1 ⨂⇩M ν2) (λp. ln (norm (fst p - snd p)))"
by (rule logEnergyC_prod[OF f1 f2 i[OF assms(5,6,2,3)]])
have e22: "logEnergyC ν2 ν2 =
integral⇧L (ν2 ⨂⇩M ν2) (λp. ln (norm (fst p - snd p)))"
by (rule logEnergyC_prod[OF f2 f2 i[OF assms(6,6,3,3)]])
show ?thesis unfolding e11 e12 e22 Eform_def ..
qed
have lim: "((λn. Eform ν1 ν2 (Kn n)) ⤏ Eform ν1 ν2
(λp. ln (norm (fst p - snd p)))) at_top"
unfolding Eform_def
by (intro tendsto_intros Kn_integral_tendsto[OF pair_measure_mono[OF _ _ _ _ assms(4,1)]] assms)
(simp_all add: assms sets_pair_measure)
have nonpos: "⋀n. Eform ν1 ν2 (Kn n) ≤ 0"
by (rule Eform_Kn_nonpos[OF f1 f2 assms(2,3,7)])
show ?thesis unfolding E by (rule tendsto_upperbound[OF lim]) (simp_all add: nonpos)
qed
end