Theory Negative_Association_Util

section ‹Preliminary Definitions and Lemmas›

theory Negative_Association_Util
  imports
    Concentration_Inequalities.Concentration_Inequalities_Preliminary
    Universal_Hash_Families.Universal_Hash_Families_More_Product_PMF
begin

(* From Joe Watt *)
abbreviation (input) flip :: ‹('a ⇒ 'b ⇒ 'c) ⇒ 'b ⇒ 'a ⇒ 'c› where
  ‹flip f x y ≡ f y x›

text ‹Additional introduction rules for boundedness:›

(*
  Note to editors: I will move these to (in afp-devel)
  Concentration_Inequalities.Concentration_Inequalities_Preliminary
*)

lemma bounded_const_min:
  fixes f :: "'a ⇒ real"
  assumes "bdd_below (f ` M)"
  shows "bounded ((λx. min c (f x)) ` M)"
proof -
  obtain h where "⋀x. x ∈ M ⟹ f x ≥ h" using assms(1) unfolding bdd_below_def by auto
  thus ?thesis by (intro boundedI[where B="max ¦c¦ ¦-h¦"]) force
qed

lemma bounded_prod:
  fixes f :: "'i ⇒ 'a ⇒ real"
  assumes "finite I"
  assumes "⋀i. i ∈ I ⟹ bounded (f i ` T)"
  shows "bounded ((λx. (∏ i ∈ I. f i x)) ` T)"
  using assms by (induction I) (auto intro:bounded_mult_comp bounded_const)

lemma bounded_vec_mult_comp:
  fixes f g :: "'a ⇒ real"
  assumes "bounded (f ` T)" "bounded (g ` T)"
  shows "bounded ((λx. (f x) *⇩R (g x)) ` T)"
  using bounded_mult_comp[OF assms] by simp

lemma bounded_max:
  fixes f :: "'a ⇒ real"
  assumes "bounded ((λx. f x) ` T)"
  shows "bounded ((λx. max c (f x)) ` T)"
proof -
  obtain m where "norm (f x) ≤ m" if "x ∈ T" for x
    using assms unfolding bounded_iff by auto

  thus ?thesis by (intro boundedI[where B="max m c"]) fastforce
qed

lemma bounded_of_bool: "bounded (range of_bool)" by auto

lemma bounded_range_imp:
  assumes "bounded (range f)"
  shows "bounded ((λω. f (h ω)) ` S)"
  by (intro bounded_subset[OF assms]) auto

text ‹The following allows to state integrability and conditions about the integral simultaneously,
e.g. @{term "has_int_that M f (λx. x ≤ c)"} says f is integrable on M and the integral smaller or
equal to @{term "c"}.›

definition has_int_that where
  "has_int_that M f P = (integrable M f ∧ (P (∫ω. f ω ∂M)))"

lemma true_eq_iff: "P ⟹ True = P" by auto
lemma le_trans: "y ≤ z ⟹ x ≤ y ⟶ x ≤ (z :: 'a :: order)" by auto

lemma has_int_that_mono:
  assumes "⋀x. P x ⟶ Q x"
  shows "has_int_that M f P ≤ has_int_that M f Q"
  using assms unfolding has_int_that_def by auto

lemma has_int_thatD:
  assumes "has_int_that M f P"
  shows "integrable M f" "P (integral⇧L M f)"
  using assms has_int_that_def by auto

text ‹This is useful to specify which components a functional depends on.›

definition depends_on :: "(('a ⇒ 'b) ⇒ 'c) ⇒ 'a set ⇒ bool"
  where "depends_on f I = (∀x y. restrict x I = restrict y I ⟶ f x = f y)"

lemma depends_onI:
  assumes "⋀x.  f x = f (λi. if i ∈ I then (x i) else undefined)"
  shows "depends_on f I"
proof -
  have "f x = f y" if "restrict x I = restrict y I" for x y
  proof -
    have "f x = f (restrict x I)" using assms unfolding restrict_def by simp
    also have "... = f (restrict y I)" using that by simp
    also have "... = f y" using assms unfolding restrict_def by simp
    finally show ?thesis by simp
  qed
  thus ?thesis unfolding depends_on_def by blast
qed

lemma depends_on_comp:
  assumes "depends_on f I"
  shows "depends_on (g ∘ f) I"
  using assms unfolding depends_on_def by (metis o_apply)

lemma depends_on_comp_2:
  assumes "depends_on f I"
  shows "depends_on (λx. g (f x)) I"
  using assms unfolding depends_on_def by metis

lemma depends_onD:
  assumes "depends_on f I"
  shows "f ω = f (λi∈I. (ω i))"
  using assms unfolding depends_on_def by (metis extensional_restrict restrict_extensional)

lemma depends_onD2:
  assumes "depends_on f I" "restrict x I = restrict y I"
  shows "f x = f y"
  using assms unfolding depends_on_def by metis

lemma depends_on_empty:
  assumes "depends_on f {}"
  shows "f ω = f undefined"
  by (intro depends_onD2[OF assms]) auto

lemma depends_on_mono:
  assumes "I ⊆ J" "depends_on f I"
  shows "depends_on f J"
  using assms unfolding depends_on_def by (metis restrict_restrict Int_absorb1)

abbreviation "square_integrable M f ≡ integrable M ((power2 :: real ⇒ real) ∘ f)"

text ‹There are many results in the field of negative association, where a statement is true
for simultaneously monotone or anti-monotone functions. With the below construction, we introduce
a mechanism where we can parameterize on the direction of a relation:›

datatype RelDirection = Fwd | Rev

definition dir_le :: "RelDirection ⇒ (('d::order) ⇒ ('d :: order) ⇒ bool)"  (infixl "≤≥ı" 60)
  where "dir_le η = (if η = Fwd then (≤) else (≥))"

lemma dir_le[simp]:
  "(≤≥⇘Fwd⇙) = (≤)"
  "(≤≥⇘Rev⇙) = (≥)"
  by (auto simp:dir_le_def)

definition dir_sign :: "RelDirection ⇒ 'a::{one,uminus}" ("±ı")
  where "dir_sign η = (if η = Fwd then 1 else (-1))"

lemma dir_le_refl: "x ≤≥⇘η⇙ x"
  by (cases η) auto

lemma dir_sign[simp]:
  "(±⇘Fwd⇙) = (1)"
  "(±⇘Rev⇙) = (-1)"
  by (auto simp:dir_sign_def)

lemma conv_rel_to_sign:
  fixes f :: "'a::order ⇒ real"
  shows "monotone (≤) (≤≥⇘η⇙) f = mono ((*)(±⇘η⇙) ∘ f)"
  by (cases "η") (simp_all add:monotone_def)

instantiation RelDirection :: times
begin
definition times_RelDirection :: "RelDirection ⇒ RelDirection ⇒ RelDirection" where
  times_RelDirection_def: "times_RelDirection x y = (if x = y then Fwd else Rev)"

instance by standard
end

lemmas rel_dir_mult[simp] = times_RelDirection_def

lemma dir_mult_hom: "(±⇘σ * τ⇙) = (±⇘σ⇙) * ((±⇘τ⇙)::real)"
  unfolding dir_sign_def times_RelDirection_def by (cases σ,auto intro:RelDirection.exhaust)

text ‹Additional lemmas about clamp for the specific case on reals.›

lemma clamp_eqI2:
  assumes "x ∈ {a..b::real}"
  shows "x = clamp a b x"
  using assms unfolding clamp_def by simp

lemma clamp_eqI:
  assumes "¦x¦ ≤ (a::real)"
  shows "x = clamp (-a) a x"
  using assms by (intro clamp_eqI2) auto

lemma clamp_real_def:
  fixes x :: real
  shows "clamp a b x = max a (min x b)"
proof -
  consider (i) "x < a" | (ii) "x ≥ a" "x ≤ b" | (iii) "x > b" by linarith
  thus ?thesis unfolding clamp_def by (cases) auto
qed

lemma clamp_range:
  assumes "a ≤ b"
  shows "⋀x. clamp a b x ≥ a" "⋀x. clamp a b x ≤ b" "range (clamp a b) ⊆ {a..b::real}"
  using assms by (auto simp: clamp_real_def)

lemma clamp_abs_le:
  assumes "a ≥ (0::real)"
  shows "¦clamp (-a) a x¦ ≤ ¦x¦"
  using assms unfolding clamp_real_def by simp

lemma bounded_clamp:
  fixes a b :: real
  shows "bounded ((clamp a b ∘ f) ` S)"
proof (cases "a ≤ b")
  case True
  show ?thesis using clamp_range[OF True] bounded_closed_interval bounded_subset
    by (metis image_comp image_mono subset_UNIV)
next
  case False
  hence "clamp a b (f x) = a" for x unfolding clamp_def by (simp add: max_def)
  hence "(clamp a b ∘ f) ` S ⊆ {a..a}" by auto
  thus ?thesis using bounded_subset bounded_closed_interval by metis
qed

lemma bounded_clamp_alt:
  fixes a b :: real
  shows "bounded ((λx. clamp a b (f x)) ` S)"
  using bounded_clamp by (auto simp:comp_def)

lemma clamp_borel[measurable]:
  fixes a b :: "'a::{euclidean_space,second_countable_topology}"
  shows "clamp a b ∈ borel_measurable borel"
  unfolding clamp_def by measurable

lemma monotone_clamp:
  assumes "monotone (≤) (≤≥⇘η⇙) f"
  shows "monotone (≤) (≤≥⇘η⇙) (λω. clamp a (b::real) (f ω))"
  using assms unfolding monotone_def clamp_real_def by (cases η) force+

text ‹This part introduces the term @{term "KL_div"} as the Kullback-Leibler divergence between a
pair of Bernoulli random variables. The expression is useful to express some of the Chernoff bounds
more concisely~\cite[Th.~1]{impagliazzo2010}.›

lemma radon_nikodym_pmf:
  assumes "set_pmf p ⊆ set_pmf q"
  defines "f ≡ (λx. ennreal (pmf p x / pmf q x))"
  shows
    "AE x in measure_pmf q. RN_deriv q p x = f x" (is "?R1")
    "AE x in measure_pmf p. RN_deriv q p x = f x" (is "?R2")
proof -
  have "pmf p x = 0" if "pmf q x = 0" for x
    using assms(1) that by (meson pmf_eq_0_set_pmf subset_iff)
  hence a:"(pmf q x * (pmf p x / pmf q x)) = pmf p x" for x by simp
  have "emeasure (density q f) A = emeasure p A" (is "?L = ?R") for A
  proof -
    have "?L = set_nn_integral (measure_pmf q) A f"
      by (subst emeasure_density) auto
    also have "… =  (∫⇧+ x∈A. ennreal (pmf q x) * f x ∂count_space UNIV)"
      by (simp add: ac_simps nn_integral_measure_pmf)
    also have "… = (∫⇧+x∈A. ennreal (pmf p x) ∂count_space UNIV)"
      using a unfolding f_def by (subst ennreal_mult'[symmetric]) simp_all
    also have "… = emeasure (bind_pmf p return_pmf) A"
      unfolding emeasure_bind_pmf nn_integral_measure_pmf by simp
    also have "… = ?R" by simp
    finally show ?thesis by simp
  qed
  hence "density (measure_pmf q) f = measure_pmf p" by (intro measure_eqI) auto
  hence "AE x in measure_pmf q. f x = RN_deriv q p x" by (intro measure_pmf.RN_deriv_unique) simp
  thus ?R1 unfolding AE_measure_pmf_iff by auto
  thus ?R2 using assms unfolding AE_measure_pmf_iff by auto
qed

lemma KL_divergence_pmf:
  assumes "set_pmf q ⊆ set_pmf p"
  shows "KL_divergence b (measure_pmf p) (measure_pmf q) = (∫x. log b (pmf q x / pmf p x) ∂q)"
  unfolding KL_divergence_def entropy_density_def
  by (intro integral_cong_AE AE_mp[OF radon_nikodym_pmf(2)[OF assms(1)] AE_I2]) auto

definition KL_div :: "real ⇒ real ⇒ real" where
  "KL_div p q = KL_divergence (exp 1) (bernoulli_pmf q) (bernoulli_pmf p)"

lemma KL_div_eq:
  assumes "q ∈ {0<..<1}" "p ∈ {0..1}"
  shows "KL_div p q = p * ln (p/q) + (1-p) * ln ((1-p)/(1-q))" (is "?L = ?R")
proof -
  have "set_pmf (bernoulli_pmf p) ⊆ set_pmf (bernoulli_pmf q)"
    using assms(1) set_pmf_bernoulli by auto
  hence "?L = (∫x. ln (pmf (bernoulli_pmf p) x / pmf (bernoulli_pmf q) x) ∂bernoulli_pmf p)"
    unfolding KL_div_def by (subst KL_divergence_pmf) (simp_all add:log_ln[symmetric])
  also have "… = ?R"
    using assms(1,2) by (subst integral_bernoulli_pmf) auto
  finally show ?thesis by simp
qed

lemma KL_div_swap:
  assumes "q ∈ {0<..<1}" "p ∈ {0..1}"
  shows "KL_div p q = KL_div (1-p) (1-q)"
  using assms by (subst (1 2) KL_div_eq) auto

text ‹A few results about independent random variables:›

lemma (in prob_space) indep_vars_const:
  assumes "⋀i. i ∈ I ⟹ c i ∈ space (N i)"
  shows "indep_vars N (λi _. c i) I"
proof -
  have rv: " random_variable (N i) (λ_. c i)" if "i ∈ I" for i  using assms[OF that] by simp
  have b:"indep_sets (λi. {space M, {}}) I"
  proof (intro indep_setsI, goal_cases)
    case (1 i) thus ?case by simp
  next
    case (2 A J)
    show ?case
    proof (cases "∀j ∈ J. A j = space M")
      case True thus ?thesis using 2(1) by (simp add:prob_space)
    next
      case False
      then obtain i where i:"A i = {}" "i ∈ J" using 2 by auto
      hence "prob (⋂ (A ` J)) = prob {}" by (intro arg_cong[where f="prob"]) auto
      also have "… = 0" by simp
      also have "… =  (∏j∈J. prob (A j))"
        using i by (intro prod_zero[symmetric] 2 bexI[where x="i"]) auto
      finally show ?thesis by simp
    qed
  qed
  have "{(λ_. c i) -` A ∩ space M |A. A ∈ sets (N i)} = {space M, {}}" (is "?L = ?R") if "i ∈ I" for i
  proof
    show "?L ⊆ ?R" by auto
  next
    have "(λA. (λ_. c i) -` A ∩ space M) {} = {}" "{} ∈ N i" by auto
    hence "{} ∈ ?L" unfolding image_Collect[symmetric] by blast
    moreover have "(λA. (λ_. c i) -` A ∩ space M) (space (N i)) = space M" "space (N i) ∈ N i"
      using assms[OF that] by auto
    hence "space M ∈ ?L" unfolding image_Collect[symmetric] by blast
    ultimately show "?R ⊆ ?L" by simp
  qed
  hence "indep_sets (λi. {(λ_. c i) -` A ∩ space M |A. A ∈ sets (N i)}) I"
    using iffD2[OF indep_sets_cong b] b by simp
  thus ?thesis unfolding indep_vars_def2 by (intro conjI rv ballI)
qed

lemma indep_vars_map_pmf:
  assumes "prob_space.indep_vars (measure_pmf p) (λ_. discrete) (λi. X i ∘ f) I"
  shows  "prob_space.indep_vars (map_pmf f p) (λ_. discrete) X I"
  using assms unfolding map_pmf_rep_eq by (intro measure_pmf.indep_vars_distr) auto

lemma indep_var_pair_pmf:
  fixes x y :: "'a pmf"
  shows "prob_space.indep_var (pair_pmf x y) discrete fst discrete snd"
proof -
  have split_bool_univ: "UNIV = insert True {False}" by auto

  have pair_prod: "pair_pmf x y = map_pmf (λω. (ω True, ω False)) (prod_pmf UNIV (case_bool x y))"
    unfolding split_bool_univ by (subst Pi_pmf_insert)
      (simp_all add:map_pmf_comp Pi_pmf_singleton pair_map_pmf2 case_prod_beta)

  have case_bool_eq: "case_bool discrete discrete = (λ_. discrete)"
    by (intro ext) (simp add: bool.case_eq_if)

  have "prob_space.indep_vars (prod_pmf UNIV (case_bool x y)) (λ_. discrete) (λi ω. ω i) UNIV"
    by (intro indep_vars_Pi_pmf) auto
  moreover have "(λi. (case_bool fst snd i) ∘ (λω. ((ω True)::'a, ω False))) = (λi ω. ω i)"
    by (auto intro!:ext split:bool.splits)
  ultimately show ?thesis
    unfolding prob_space.indep_var_def[OF prob_space_measure_pmf] pair_prod case_bool_eq
    by (intro indep_vars_map_pmf) simp
qed

lemma measure_pair_pmf: "measure (pair_pmf p q) (A × B) = measure p A * measure q B" (is "?L = ?R")
proof -
  have "?L = measure (pair_pmf p q) ((A ∩ set_pmf p) × (B ∩ set_pmf q))"
    by (intro measure_eq_AE AE_pmfI) auto
  also have "… = measure p (A ∩ set_pmf p) * measure q (B ∩ set_pmf q)"
    by (intro measure_pmf_prob_product) auto
  also have "… = ?R" by (intro arg_cong2[where f="(*)"] measure_eq_AE AE_pmfI) auto
  finally show ?thesis by simp
qed

instance bool :: second_countable_topology
proof
  show "∃B::bool set set. countable B ∧ open = generate_topology B"
    by (intro exI[of _ "range lessThan ∪ range greaterThan"]) (auto simp: open_bool_def)
qed

end