Theory Constructive_Chernoff_Bound
subsection ‹Constructive Chernoff Bound\label{sec:constructive_chernoff_bound}›
text ‹This section formalizes Theorem~5 by Impagliazzo and Kabanets~\cite{impagliazzo2010}. It is
a general result with which Chernoff-type tail bounds for various kinds of weakly dependent random
variables can be obtained. The results here are general and will be applied in
Section~\ref{sec:random_walks} to random walks in expander graphs.›
theory Constructive_Chernoff_Bound
imports
"HOL-Probability.Probability_Measure"
Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
Weighted_Arithmetic_Geometric_Mean.Weighted_Arithmetic_Geometric_Mean
begin
lemma powr_mono_rev:
fixes x :: real
assumes "a ≤ b" and "x > 0" "x ≤ 1"
shows "x powr b ≤ x powr a"
proof -
have "x powr b = (1/x) powr (-b)"
using assms by (simp add: powr_divide powr_minus_divide)
also have "... ≤ (1/x) powr (-a)"
using assms by (intro powr_mono) auto
also have "... = x powr a"
using assms by (simp add: powr_divide powr_minus_divide)
finally show ?thesis by simp
qed
lemma exp_powr: "(exp x) powr y = exp (x*y)" for x :: real
unfolding powr_def by simp
lemma integrable_pmf_iff_bounded:
fixes f :: "'a ⇒ real"
assumes "⋀x. x ∈ set_pmf p ⟹ abs (f x) ≤ C"
shows "integrable (measure_pmf p) f"
proof -
obtain x where "x ∈ set_pmf p"
using set_pmf_not_empty by fast
hence "C ≥ 0" using assms(1) by fastforce
hence " (∫⇧+ x. ennreal (abs (f x)) ∂measure_pmf p) ≤ (∫⇧+ x. C ∂measure_pmf p)"
using assms ennreal_le_iff
by (intro nn_integral_mono_AE AE_pmfI) auto
also have "... = C"
by simp
also have "... < Orderings.top"
by simp
finally have "(∫⇧+ x. ennreal (abs (f x)) ∂measure_pmf p) < Orderings.top" by simp
thus ?thesis
by (intro iffD2[OF integrable_iff_bounded]) auto
qed
lemma split_pair_pmf:
"measure_pmf.prob (pair_pmf A B) S = integral⇧L A (λa. measure_pmf.prob B {b. (a,b) ∈ S})"
(is "?L = ?R")
proof -
have a:"integrable (measure_pmf A) (λx. measure_pmf.prob B {b. (x, b) ∈ S})"
by (intro integrable_pmf_iff_bounded[where C="1"]) simp
have "?L = (∫⇧+x. indicator S x ∂(measure_pmf (pair_pmf A B)))"
by (simp add: measure_pmf.emeasure_eq_measure)
also have "... = (∫⇧+x. (∫⇧+y. indicator S (x,y) ∂B) ∂A)"
by (simp add: nn_integral_pair_pmf')
also have "... = (∫⇧+x. (∫⇧+y. indicator {b. (x,b) ∈ S} y ∂B) ∂A)"
by (simp add:indicator_def)
also have "... = (∫⇧+x. (measure_pmf.prob B {b. (x,b) ∈ S}) ∂A)"
by (simp add: measure_pmf.emeasure_eq_measure)
also have "... = ?R"
using a
by (subst nn_integral_eq_integral) auto
finally show ?thesis by simp
qed
lemma split_pair_pmf_2:
"measure(pair_pmf A B) S = integral⇧L B (λa. measure_pmf.prob A {b. (b,a) ∈ S})"
(is "?L = ?R")
proof -
have "?L = measure (pair_pmf B A) {ω. (snd ω, fst ω) ∈ S}"
by (subst pair_commute_pmf) (simp add:vimage_def case_prod_beta)
also have "... = ?R"
unfolding split_pair_pmf by simp
finally show ?thesis by simp
qed
definition KL_div :: "real ⇒ real ⇒ real"
where "KL_div p q = p * ln (p/q) + (1-p) * ln ((1-p)/(1-q))"
theorem impagliazzo_kabanets_pmf:
fixes Y :: "nat ⇒ 'a ⇒ bool"
fixes p :: "'a pmf"
assumes "n > 0"
assumes "⋀i. i ∈ {..<n} ⟹ δ i ∈ {0..1}"
assumes "⋀S. S ⊆ {..<n} ⟹ measure p {ω. (∀i ∈ S. Y i ω)} ≤ (∏i ∈ S. δ i)"
defines "δ_avg ≡ (∑i∈ {..<n}. δ i)/n"
assumes "γ ∈ {δ_avg..1}"
assumes "δ_avg > 0"
shows "measure p {ω. real (card {i ∈ {..<n}. Y i ω}) ≥ γ * n} ≤ exp (-real n * KL_div γ δ_avg)"
(is "?L ≤ ?R")
proof -
let ?n = "real n"
define q :: real where "q = (if γ = 1 then 1 else (γ-δ_avg)/(γ*(1-δ_avg)))"
define g where "g ω = card {i. i < n ∧ ¬Y i ω}" for ω
let ?E = "(λω. real (card {i. i < n ∧ Y i ω}) ≥ γ * n)"
let ?Ξ = "prod_pmf {..<n} (λ_. bernoulli_pmf q)"
have q_range:"q ∈{0..1}"
proof (cases "γ < 1")
case True
then show ?thesis
using assms(5,6)
unfolding q_def by (auto intro!:divide_nonneg_pos simp add:algebra_simps)
next
case False
hence "γ = 1" using assms(5) by simp
then show ?thesis unfolding q_def by simp
qed
have abs_pos_le_1I: "abs x ≤ 1" if "x ≥ 0" "x ≤ 1" for x :: real
using that by auto
have γ_n_nonneg: "γ*?n ≥ 0"
using assms(1,5,6) by simp
define r where "r = n - nat ⌈γ*n⌉"
have 2:"(1-q) ^ r ≤ (1-q)^ g ω" if "?E ω" for ω
proof -
have "g ω = card ({i. i < n} - {i. i < n ∧ Y i ω})"
unfolding g_def by (intro arg_cong[where f="λx. card x"]) auto
also have "... = card {i. i < n} - card {i. i < n ∧ Y i ω}"
by (subst card_Diff_subset, auto)
also have "... ≤ card {i. i < n} - nat ⌈γ*n⌉"
using that γ_n_nonneg by (intro diff_le_mono2) simp
also have "... = r"
unfolding r_def by simp
finally have "g ω ≤ r" by simp
thus "(1-q) ^ r ≤ (1-q) ^ (g ω)"
using q_range by (intro power_decreasing) auto
qed
have γ_gt_0: "γ > 0"
using assms(5,6) by simp
have q_lt_1: "q < 1" if "γ < 1"
proof -
have "δ_avg < 1" using assms(5) that by simp
hence "(γ - δ_avg) / (γ * (1 - δ_avg)) < 1"
using γ_gt_0 assms(6) that
by (subst pos_divide_less_eq) (auto simp add:algebra_simps)
thus "q < 1"
unfolding q_def using that by simp
qed
have 5: "(δ_avg * q + (1-q)) / (1-q) powr (1-γ) = exp (- KL_div γ δ_avg)" (is "?L1 = ?R1")
if "γ < 1"
proof -
have δ_avg_range: "δ_avg ∈ {0<..<1}"
using that assms(5,6) by simp
have "?L1 = (1 - (1-δ_avg) * q) / (1-q) powr (1-γ)"
by (simp add:algebra_simps)
also have "... = (1 - (γ-δ_avg) / γ ) / (1-q) powr (1-γ)"
unfolding q_def using that γ_gt_0 δ_avg_range by simp
also have "... = (δ_avg / γ) / (1-q) powr (1-γ)"
using γ_gt_0 by (simp add:divide_simps)
also have "... = (δ_avg / γ) * (1/(1-q)) powr (1-γ)"
using q_lt_1[OF that] by (subst powr_divide, simp_all)
also have "... = (δ_avg / γ) * (1/((γ*(1-δ_avg)-(γ-δ_avg))/(γ*(1-δ_avg)))) powr (1-γ)"
using γ_gt_0 δ_avg_range unfolding q_def by (simp add:divide_simps)
also have "... = (δ_avg / γ) * ((γ / δ_avg) *((1-δ_avg)/(1-γ))) powr (1-γ)"
by (simp add:algebra_simps)
also have "... = (δ_avg / γ) * (γ / δ_avg) powr (1-γ) *((1-δ_avg)/(1-γ)) powr (1-γ)"
using γ_gt_0 δ_avg_range that by (subst powr_mult, auto)
also have "... = (δ_avg / γ) powr 1 * (δ_avg / γ) powr -(1-γ) *((1-δ_avg)/(1-γ)) powr (1-γ)"
using γ_gt_0 δ_avg_range that unfolding powr_minus_divide by (simp add:powr_divide)
also have "... = (δ_avg / γ) powr γ *((1-δ_avg)/(1-γ)) powr (1-γ)"
by (subst powr_add[symmetric]) simp
also have "... = exp ( ln ((δ_avg / γ) powr γ *((1-δ_avg)/(1-γ)) powr (1-γ)))"
using γ_gt_0 δ_avg_range that by (intro exp_ln[symmetric] mult_pos_pos) auto
also have "... = exp ((ln ((δ_avg / γ) powr γ) + ln (((1 - δ_avg) / (1 - γ)) powr (1-γ))))"
using γ_gt_0 δ_avg_range that by (subst ln_mult) auto
also have "... = exp ((γ * ln (δ_avg / γ) + (1 - γ) * ln ((1 - δ_avg) / (1 - γ))))"
using γ_gt_0 δ_avg_range that by (simp add:ln_powr algebra_simps)
also have "... = exp (- (γ * ln (γ / δ_avg) + (1 - γ) * ln ((1 - γ) / (1 - δ_avg))))"
using γ_gt_0 δ_avg_range that by (simp add: ln_div algebra_simps)
also have "... = ?R1"
unfolding KL_div_def by simp
finally show ?thesis by simp
qed
have 3: "(δ_avg * q + (1-q)) ^ n / (1-q) ^ r ≤ exp (- ?n* KL_div γ δ_avg)" (is "?L1 ≤ ?R1")
proof (cases "γ < 1")
case True
have "γ * real n ≤ 1 * real n"
using True by (intro mult_right_mono) auto
hence "r = real n - real (nat ⌈γ * real n⌉)"
unfolding r_def by (subst of_nat_diff) auto
also have "... = real n - ⌈γ * real n⌉"
using γ_n_nonneg by (subst of_nat_nat, auto)
also have "... ≤ ?n - γ * ?n"
by (intro diff_mono) auto
also have "... = (1-γ) *?n" by (simp add:algebra_simps)
finally have r_bound: "r ≤ (1-γ)*n" by simp
have "?L1 = (δ_avg * q + (1-q)) ^ n / (1-q) powr r"
using q_lt_1[OF True] assms(1) by (simp add: powr_realpow)
also have "... = (δ_avg * q + (1-q)) powr n / (1-q) powr r"
using q_lt_1[OF True] assms(6) q_range
by (subst powr_realpow[symmetric], auto intro!:add_nonneg_pos)
also have "... ≤ (δ_avg * q + (1-q)) powr n / (1-q) powr ((1-γ)*n)"
using q_range q_lt_1[OF True] by (intro divide_left_mono powr_mono_rev r_bound) auto
also have "... = (δ_avg * q + (1-q)) powr n / ((1-q) powr (1-γ)) powr n"
unfolding powr_powr by simp
also have "... = ((δ_avg * q + (1-q)) / (1-q) powr (1-γ)) powr n"
using assms(6) q_range by (subst powr_divide) auto
also have "... = exp (- KL_div γ δ_avg) powr real n"
unfolding 5[OF True] by simp
also have "... = ?R1"
unfolding exp_powr by simp
finally show ?thesis by simp
next
case False
hence γ_eq_1: "γ=1" using assms(5) by simp
have "?L1 = δ_avg ^ n"
using γ_eq_1 r_def q_def by simp
also have "... = exp( - KL_div 1 δ_avg) ^ n"
unfolding KL_div_def using assms(6) by (simp add:ln_div)
also have "... = ?R1"
using γ_eq_1 by (simp add: powr_realpow[symmetric] exp_powr)
finally show ?thesis by simp
qed
have 4: "(1 - q) ^ r > 0"
proof (cases "γ < 1")
case True
then show ?thesis using q_lt_1[OF True] by simp
next
case False
hence "γ=1" using assms(5) by simp
hence "r=0" unfolding r_def by simp
then show ?thesis by simp
qed
have "(1-q) ^ r * ?L = (∫ω. indicator {ω. ?E ω} ω * (1-q) ^ r ∂p)"
by simp
also have "... ≤ (∫ω. indicator {ω. ?E ω} ω * (1-q) ^ g ω ∂p)"
using q_range 2 by (intro integral_mono_AE integrable_pmf_iff_bounded[where C="1"]
abs_pos_le_1I mult_le_one power_le_one AE_pmfI) (simp_all split:split_indicator)
also have "... = (∫ω. indicator {ω. ?E ω} ω * (∏i ∈ {i. i < n ∧ ¬Y i ω}. (1-q)) ∂p)"
unfolding g_def using q_range
by (intro integral_cong_AE AE_pmfI, simp_all add:powr_realpow)
also have "... = (∫ω. indicator {ω. ?E ω} ω * measure ?Ξ ({j. j < n ∧ ¬Y j ω} → {False}) ∂p)"
using q_range by (subst prob_prod_pmf') (auto simp add:measure_pmf_single)
also have "... = (∫ω. measure ?Ξ {ξ. ?E ω ∧ (∀i∈{j. j < n ∧ ¬Y j ω}. ¬ξ i)} ∂p)"
by (intro integral_cong_AE AE_pmfI, simp_all add:Pi_def split:split_indicator)
also have "... = (∫ω. measure ?Ξ {ξ. ?E ω ∧ (∀i∈{..<n}. ξ i ⟶ Y i ω)} ∂p)"
by (intro integral_cong_AE AE_pmfI measure_eq_AE) auto
also have "... = measure (pair_pmf p ?Ξ) {φ.?E (fst φ)∧(∀i ∈ {..<n}. snd φ i ⟶ Y i (fst φ))}"
unfolding split_pair_pmf by simp
also have "... ≤ measure (pair_pmf p ?Ξ) {φ. (∀i ∈ {j. j < n ∧ snd φ j}. Y i (fst φ))}"
by (intro pmf_mono, auto)
also have "... = (∫ξ. measure p {ω. ∀i∈{j. j< n ∧ ξ j}. Y i ω} ∂ ?Ξ)"
unfolding split_pair_pmf_2 by simp
also have "... ≤ (∫a. (∏i ∈ {j. j < n ∧ a j}. δ i) ∂ ?Ξ)"
using assms(2) by (intro integral_mono_AE AE_pmfI assms(3) subsetI prod_le_1 prod_nonneg
integrable_pmf_iff_bounded[where C="1"] abs_pos_le_1I) auto
also have "... = (∫a. (∏i ∈ {..<n}. δ i^ of_bool(a i)) ∂ ?Ξ)"
unfolding of_bool_def by (intro integral_cong_AE AE_pmfI)
(auto simp add:if_distrib prod.If_cases Int_def)
also have "... = (∏i<n. (∫a. (δ i ^ of_bool a) ∂(bernoulli_pmf q)))"
using assms(2) by (intro expectation_prod_Pi_pmf integrable_pmf_iff_bounded[where C="1"]) auto
also have "... = (∏i<n. δ i * q + (1-q))"
using q_range by simp
also have "... = (root (card {..<n}) (∏i<n. δ i * q + (1-q))) ^ (card {..<n})"
using assms(1,2) q_range by (intro real_root_pow_pos2[symmetric] prod_nonneg) auto
also have "... ≤ ((∑i<n. δ i * q + (1-q))/card{..<n})^(card {..<n})"
using assms(1,2) q_range by (intro power_mono arithmetic_geometric_mean)
(auto intro: prod_nonneg)
also have "... = ((∑i<n. δ i * q)/n + (1-q))^n"
using assms(1) by (simp add:sum.distrib divide_simps mult.commute)
also have "... = (δ_avg * q + (1-q))^n"
unfolding δ_avg_def by (simp add: sum_distrib_right[symmetric])
finally have "(1-q) ^ r * ?L ≤ (δ_avg * q + (1-q)) ^ n" by simp
hence "?L ≤ (δ_avg * q + (1-q)) ^ n / (1-q) ^ r"
using 4 by (subst pos_le_divide_eq) (auto simp add:algebra_simps)
also have "... ≤ ?R"
by (intro 3)
finally show ?thesis by simp
qed
text ‹The distribution of a random variable with a countable range is a discrete probability space,
i.e., induces a PMF. Using this it is possible to generalize the previous result to arbitrary
probability spaces.›
lemma (in prob_space) establish_pmf:
fixes f :: "'a ⇒ 'b"
assumes rv: "random_variable discrete f"
assumes "countable (f ` space M)"
shows "distr M discrete f ∈ {M. prob_space M ∧ sets M = UNIV ∧ (AE x in M. measure M {x} ≠ 0)}"
proof -
define N where "N = {x ∈ space M.¬ prob (f -` {f x} ∩ space M) ≠ 0}"
define I where "I = {z ∈ (f ` space M). prob (f -` {z} ∩ space M) = 0}"
have countable_I: " countable I"
unfolding I_def by (intro countable_subset[OF _ assms(2)]) auto
have disj: "disjoint_family_on (λy. f -` {y} ∩ space M) I"
unfolding disjoint_family_on_def by auto
have N_alt_def: "N = (⋃y ∈ I. f -` {y} ∩ space M)"
unfolding N_def I_def by (auto simp add:set_eq_iff)
have "emeasure M N = ∫⇧+ y. emeasure M (f -` {y} ∩ space M) ∂count_space I"
using rv countable_I unfolding N_alt_def
by (subst emeasure_UN_countable) (auto simp add:disjoint_family_on_def)
also have "... = ∫⇧+ y. 0 ∂count_space I"
unfolding I_def using emeasure_eq_measure ennreal_0
by (intro nn_integral_cong) auto
also have "... = 0" by simp
finally have 0:"emeasure M N = 0" by simp
have 1:"N ∈ events"
unfolding N_alt_def using rv
by (intro sets.countable_UN'' countable_I) simp
have " AE x in M. prob (f -` {f x} ∩ space M) ≠ 0"
using 0 1 by (subst AE_iff_measurable[OF _ N_def[symmetric]])
hence " AE x in M. measure (distr M discrete f) {f x} ≠ 0"
by (subst measure_distr[OF rv], auto)
hence "AE x in distr M discrete f. measure (distr M discrete f) {x} ≠ 0"
by (subst AE_distr_iff[OF rv], auto)
thus ?thesis
using prob_space_distr rv by auto
qed
lemma singletons_image_eq:
"(λx. {x}) ` T ⊆ Pow T"
by auto
theorem (in prob_space) impagliazzo_kabanets:
fixes Y :: "nat ⇒ 'a ⇒ bool"
assumes "n > 0"
assumes "⋀i. i ∈ {..<n} ⟹ random_variable discrete (Y i)"
assumes "⋀i. i ∈ {..<n} ⟹ δ i ∈ {0..1}"
assumes "⋀S. S ⊆ {..<n} ⟹ 𝒫(ω in M. (∀i ∈ S. Y i ω)) ≤ (∏i ∈ S. δ i)"
defines "δ_avg ≡ (∑i∈ {..<n}. δ i)/n"
assumes "γ ∈ {δ_avg..1}" "δ_avg > 0"
shows "𝒫(ω in M. real (card {i ∈ {..<n}. Y i ω}) ≥ γ * n) ≤ exp (-real n * KL_div γ δ_avg)"
(is "?L ≤ ?R")
proof -
define f where "f = (λω i. if i < n then Y i ω else False)"
define g where "g = (λω i. if i < n then ω i else False)"
define T where "T = {ω. (∀i. ω i ⟶ i < n)}"
have g_idem: "g ∘ f = f" unfolding f_def g_def by (simp add:comp_def)
have f_range: " f ∈ space M → T"
unfolding T_def f_def by simp
have "T = PiE_dflt {..<n} False (λ_. UNIV)"
unfolding T_def PiE_dflt_def by auto
hence "finite T"
using finite_PiE_dflt by auto
hence countable_T: "countable T"
by (intro countable_finite)
moreover have "f ` space M ⊆ T"
using f_range by auto
ultimately have countable_f: "countable (f ` space M)"
using countable_subset by auto
have "f -` y ∩ space M ∈ events" if t:"y ∈ (λx. {x}) ` T" for y
proof -
obtain t where "y = {t}" and t_range: "t ∈ T" using t by auto
hence "f -` y ∩ space M = {ω ∈ space M. f ω = t}"
by (auto simp add:vimage_def)
also have "... = {ω ∈ space M. (∀i < n. Y i ω = t i)}"
using t_range unfolding f_def T_def by auto
also have "... = (⋂i ∈ {..<n}. {ω ∈ space M. Y i ω = t i})"
using assms(1) by auto
also have "... ∈ events"
using assms(1,2)
by (intro sets.countable_INT) auto
finally show ?thesis by simp
qed
hence "random_variable (count_space T) f"
using sigma_sets_singletons[OF countable_T] singletons_image_eq f_range
by (intro measurable_sigma_sets[where Ω="T" and A=" (λx. {x}) ` T"]) simp_all
moreover have "g ∈ measurable discrete (count_space T)"
unfolding g_def T_def by simp
ultimately have "random_variable discrete (g ∘ f)"
by simp
hence rv:"random_variable discrete f"
unfolding g_idem by simp
define M' :: "(nat ⇒ bool) measure"
where "M' = distr M discrete f"
define Ω where "Ω = Abs_pmf M'"
have a:"measure_pmf (Abs_pmf M') = M'"
unfolding M'_def
by (intro Abs_pmf_inverse[OF establish_pmf] rv countable_f)
have b:"{i. (i < n ⟶ Y i x) ∧ i < n} = {i. i < n ∧ Y i x}" for x
by auto
have c: "measure Ω {ω. ∀i∈S. ω i} ≤ prod δ S" (is "?L1 ≤ ?R1") if "S ⊆ {..<n}" for S
proof -
have d: "i ∈ S ⟹ i < n" for i
using that by auto
have "?L1 = measure M' {ω. ∀i∈S. ω i}"
unfolding Ω_def a by simp
also have "... = 𝒫(ω in M. (∀i ∈ S. Y i ω))"
unfolding M'_def using that d
by (subst measure_distr[OF rv]) (auto simp add:f_def Int_commute Int_def)
also have "... ≤ ?R1"
using that assms(4) by simp
finally show ?thesis by simp
qed
have "?L = measure M' {ω. real (card {i. i < n ∧ ω i}) ≥ γ * n}"
unfolding M'_def by (subst measure_distr[OF rv])
(auto simp add:f_def algebra_simps Int_commute Int_def b)
also have "... = measure_pmf.prob Ω {ω. real (card {i ∈ {..<n}. ω i}) ≥ γ * n}"
unfolding Ω_def a by simp
also have "... ≤ ?R"
using assms(1,3,6,7) c unfolding δ_avg_def
by (intro impagliazzo_kabanets_pmf) auto
finally show ?thesis by simp
qed
text ‹Bounds and properties of @{term "KL_div"}›
lemma KL_div_mono_right_aux_1:
assumes "0 ≤ p" "p ≤ q" "q ≤ q'" "q' < 1"
shows "KL_div p q-2*(p-q)^2 ≤ KL_div p q'-2*(p-q')^2"
proof (cases "p = 0")
case True
define f' :: "real ⇒ real" where "f' = (λx. 1/(1-x) - 4 * x)"
have deriv: "((λq. ln (1/(1-q)) - 2*q^2) has_real_derivative (f' x)) (at x)"
if "x ∈ {q..q'}" for x
proof -
have "x ∈ {0..<1}" using assms that by auto
thus ?thesis unfolding f'_def by (auto intro!: derivative_eq_intros)
qed
have deriv_nonneg: "f' x ≥ 0" if "x ∈ {q..q'}" for x
proof -
have 0:"x ∈ {0..<1}" using assms that by auto
have "4 * x*(1-x) = 1 - 4*(x-1/2)^2" by (simp add:power2_eq_square field_simps)
also have "... ≤ 1" by simp
finally have "4*x*(1-x) ≤ 1" by simp
hence "1/(1-x) ≥ 4*x" using 0 by (simp add: pos_le_divide_eq)
thus ?thesis unfolding f'_def by auto
qed
have "ln (1 / (1 - q)) - 2 * q^2 ≤ ln (1 / (1 - q')) - 2 * q'^2"
using deriv deriv_nonneg by (intro DERIV_nonneg_imp_nondecreasing[OF assms(3)]) auto
thus ?thesis using True unfolding KL_div_def by simp
next
case False
hence p_gt_0: "p > 0" using assms by auto
define f' :: "real ⇒ real" where "f' = (λx. (1-p)/(1-x) - p/x + 4 * (p-x))"
have deriv: "((λq. KL_div p q - 2*(p-q)^2) has_real_derivative (f' x)) (at x)" if "x ∈ {q..q'}"
for x
proof -
have "0 < p /x" " 0 < (1 - p) / (1 - x)" using that assms p_gt_0 by auto
thus ?thesis unfolding KL_div_def f'_def by (auto intro!: derivative_eq_intros)
qed
have f'_part_nonneg: "(1/(x*(1-x)) - 4) ≥ 0" if "x ∈ {0<..<1}" for x :: real
proof -
have "4 * x * (1-x) = 1 - 4 * (x-1/2)^2" by (simp add:power2_eq_square algebra_simps)
also have "... ≤ 1" by simp
finally have "4 * x * (1-x) ≤ 1" by simp
hence "1/(x*(1-x)) ≥ 4" using that by (subst pos_le_divide_eq) auto
thus ?thesis by simp
qed
have f'_alt: "f' x = (x-p)*(1/(x*(1-x)) - 4)" if "x ∈ {0<..<1}" for x
proof -
have "f' x = (x-p)/(x*(1-x)) + 4 * (p-x)" using that unfolding f'_def by (simp add:field_simps)
also have "... = (x-p)*(1/(x*(1-x)) - 4)" by (simp add:algebra_simps)
finally show ?thesis by simp
qed
have deriv_nonneg: "f' x ≥ 0" if "x ∈ {q..q'}" for x
proof -
have "x ∈ {0<..<1}" using assms that p_gt_0 by auto
have "f' x =(x-p)*(1/(x*(1-x)) - 4)" using that assms p_gt_0 by (subst f'_alt) auto
also have "... ≥ 0" using that f'_part_nonneg assms p_gt_0 by (intro mult_nonneg_nonneg) auto
finally show ?thesis by simp
qed
show ?thesis using deriv deriv_nonneg
by (intro DERIV_nonneg_imp_nondecreasing[OF assms(3)]) auto
qed
lemma KL_div_swap: "KL_div (1-p) (1-q) = KL_div p q"
unfolding KL_div_def by auto
lemma KL_div_mono_right_aux_2:
assumes "0 < q'" "q' ≤ q" "q ≤ p" "p ≤ 1"
shows "KL_div p q-2*(p-q)^2 ≤ KL_div p q'-2*(p-q')^2"
proof -
have "KL_div (1-p) (1-q)-2*((1-p)-(1-q))^2 ≤ KL_div (1-p) (1-q')-2*((1-p)-(1-q'))^2"
using assms by (intro KL_div_mono_right_aux_1) auto
thus ?thesis unfolding KL_div_swap by (auto simp:algebra_simps power2_commute)
qed
lemma KL_div_mono_right_aux:
assumes "(0 ≤ p ∧ p ≤ q ∧ q ≤ q' ∧ q' < 1) ∨ (0 < q' ∧ q' ≤ q ∧ q ≤ p ∧ p ≤ 1)"
shows "KL_div p q-2*(p-q)^2 ≤ KL_div p q'-2*(p-q')^2"
using KL_div_mono_right_aux_1 KL_div_mono_right_aux_2 assms by auto
lemma KL_div_mono_right:
assumes "(0 ≤ p ∧ p ≤ q ∧ q ≤ q' ∧ q' < 1) ∨ (0 < q' ∧ q' ≤ q ∧ q ≤ p ∧ p ≤ 1)"
shows "KL_div p q ≤ KL_div p q'" (is "?L ≤ ?R")
proof -
consider (a) "0 ≤ p" "p ≤ q" "q ≤ q'" "q' < 1" | (b) "0 < q'" "q' ≤ q" "q ≤ p" "p ≤ 1"
using assms by auto
hence 0: "(p - q)⇧2 ≤ (p - q')⇧2"
proof (cases)
case a
hence "(q-p)^2 ≤ (q' - p)^2" by auto
thus ?thesis by (simp add: power2_commute)
next
case b thus ?thesis by simp
qed
have "?L = (KL_div p q - 2*(p-q)^2) + 2 * (p-q)^2" by simp
also have "... ≤ (KL_div p q' - 2*(p-q')^2) + 2 * (p-q')^2"
by (intro add_mono KL_div_mono_right_aux assms mult_left_mono 0) auto
also have "... = ?R" by simp
finally show ?thesis by simp
qed
lemma KL_div_lower_bound:
assumes "p ∈ {0..1}" "q ∈ {0<..<1}"
shows "2*(p-q)^2 ≤ KL_div p q"
proof -
have "0 ≤ KL_div p p - 2 * (p-p)^2" unfolding KL_div_def by simp
also have "... ≤ KL_div p q - 2 * (p-q)^2" using assms by (intro KL_div_mono_right_aux) auto
finally show ?thesis by simp
qed
end