Theory Negative_Association_Definition

section ‹Definition›

text ‹This section introduces the concept of negatively associated random variables (RVs). The
definition follows, as closely as possible, the original description by
Joag-Dev and Proschan~\cite{joagdev1983}.


However, the following modifications have been made:

Singleton and empty sets of random variables are considered negatively associated. This is useful
because it simplifies many of the induction proofs. The second modification is that the RV's don't
have to be real valued.
Instead the range can be into any linearly ordered space with the borel $\sigma$-algebra. This is a
major enhancement compared to the original work, as well as results by following
authors~\cite{dubhashi2007, dubhashi1998, dubhashi1996, lisawadi2011, permantle2000}.›

theory Negative_Association_Definition
  imports
    Concentration_Inequalities.Bienaymes_Identity
    Negative_Association_Util
begin

context prob_space
begin

definition neg_assoc :: "('i ⇒ 'a ⇒ 'c :: {linorder_topology}) ⇒ 'i set ⇒ bool"
  where "neg_assoc X I = (
    (∀i ∈ I. random_variable borel (X i)) ∧
    (∀(f::nat ⇒ ('i ⇒ 'c) ⇒ real) J. J ⊆ I ∧
      (∀ι<2. bounded (range (f ι)) ∧ mono(f ι) ∧ depends_on (f ι) ([J,I-J]!ι) ∧
      f ι ∈ PiM ([J,I-J]!ι) (λ_. borel) →⇩M borel) ⟶
      covariance (f 0 ∘ flip X) (f 1 ∘ flip X) ≤ 0))"

lemma neg_assocI:
  assumes "⋀i. i ∈ I ⟹ random_variable borel (X i)"
  assumes "⋀f g J. J ⊆ I
    ⟹ depends_on f J ⟹ depends_on g (I-J)
    ⟹ mono f ⟹ mono g
    ⟹ bounded (range f::real set) ⟹ bounded (range g)
    ⟹ f ∈ PiM J (λ_. borel) →⇩M borel ⟹ g ∈ PiM (I-J) (λ_. borel) →⇩M borel
    ⟹ covariance (f ∘ flip X) (g ∘ flip X) ≤ 0"
  shows "neg_assoc X I"
  using assms unfolding neg_assoc_def by (auto simp:numeral_eq_Suc All_less_Suc)

lemma neg_assocI2:
  assumes [measurable]: "⋀i. i ∈ I ⟹ random_variable borel (X i)"
  assumes "⋀f g J. J ⊆ I
    ⟹ depends_on f J ⟹ depends_on g (I-J)
    ⟹ mono f ⟹ mono g
    ⟹ bounded (range f) ⟹ bounded (range g)
    ⟹ f ∈ PiM J (λ_. borel) →⇩M (borel :: real measure)
    ⟹ g ∈ PiM (I-J) (λ_. borel) →⇩M (borel :: real measure)
    ⟹ (∫ω. f(λi. X i ω) * g(λi. X i ω) ∂M)≤(∫ω. f(λi. X i ω)∂M)*(∫ω. g(λi. X i ω) ∂M)"
  shows "neg_assoc X I"
proof (rule neg_assocI,goal_cases)
  case (1 i) thus ?case using assms(1) by auto
next
  case (2 f g J)

  note [measurable] = 2(8,9)
  note bounded = integrable_bounded bounded_intros

  have [measurable]: "random_variable borel (λω. f (λi. X i ω))"
    using subsetD[OF 2(1)] by (subst depends_onD[OF 2(2)]) measurable
  moreover have [measurable]: "random_variable borel (λω. g (λi. X i ω))"
    by (subst depends_onD[OF 2(3)]) measurable
  moreover have "integrable M (λω. ((f ∘ (λx y. X y x)) ω)⇧2)"
    unfolding comp_def by (intro bounded bounded_subset[OF 2(6)]) auto
  moreover have "integrable M (λω. ((g ∘ (λx y. X y x)) ω)⇧2)"
    unfolding comp_def by (intro bounded bounded_subset[OF 2(7)]) auto
  ultimately show ?case using assms(2)[OF 2(1-9)]
    by (subst covariance_eq) (auto simp:comp_def)
qed

lemma neg_assoc_empty:
  "neg_assoc X {}"
proof (intro neg_assocI2, goal_cases)
  case (1 i)
  then show ?case by simp
next
  case (2 f g J)
  define fc gc where fc:"fc = f undefined" and gc:"gc = g undefined"

  have "depends_on f {}" "depends_on g {}" using 2 by auto
  hence fg_simps: "f = (λx. fc)" "g = (λx. gc)" unfolding fc gc using depends_on_empty by auto
  then show ?case unfolding fg_simps by (simp add:prob_space)
qed

lemma neg_assoc_singleton:
  assumes "random_variable borel (X i)"
  shows "neg_assoc X {i}"
proof (rule neg_assocI2, goal_cases)
  case (1 i)
  then show ?case using assms by auto
next
  case (2 f g J)
  show ?case
  proof (cases "J = {}")
    case True
    define fc where "fc = f undefined"
    have f:"f = (λ_. fc)"
      unfolding fc_def by (intro ext depends_onD2[OF 2(2)]) (auto simp:True)
    then show ?thesis unfolding f by (simp add:prob_space)
  next
    case False
    hence J: "J = {i}" using 2(1) by auto
    define gc where "gc = g undefined"
    have g:"g = (λ_. gc)"
      unfolding gc_def by (intro ext depends_onD2[OF 2(3)]) (auto simp:J)
    then show ?thesis unfolding g by (simp add:prob_space)
  qed
qed

lemma neg_assoc_imp_measurable:
  assumes "neg_assoc X I"
  assumes "i ∈ I"
  shows "random_variable borel (X i)"
  using assms unfolding neg_assoc_def by auto

text ‹Even though the assumption was that defining property is true for pairs of monotone functions
over the random variables, it is also true for pairs of anti-monotone functions.›

lemma neg_assoc_imp_mult_mono_bounded:
  fixes f g :: "('i ⇒ 'c::linorder_topology) ⇒ real"
  assumes "neg_assoc X I"
  assumes "J ⊆ I"
  assumes "bounded (range f)" "bounded (range g)"
  assumes "monotone (≤) (≤≥⇘η⇙) f" "monotone (≤) (≤≥⇘η⇙) g"
  assumes "depends_on f J" "depends_on g (I-J)"
  assumes [measurable]: "f ∈ borel_measurable (Pi⇩M J (λ_. borel))"
  assumes [measurable]: "g ∈ borel_measurable (Pi⇩M (I-J) (λ_. borel))"
  shows
    "covariance (f ∘ flip X) (g ∘ flip X) ≤ 0"
    "(∫ω. f (λi. X i ω) * g (λi. X i ω) ∂M) ≤ expectation (λx. f(λy. X y x)) * expectation (λx. g(λy. X y x))"
      (is "?L ≤ ?R")
proof -
  define q where "q ι = (if ι = 0 then f else g)" for ι :: nat
  define h where "h ι = ((*) (±⇘η⇙)) ∘ (q ι)" for ι :: nat

  note [measurable] = neg_assoc_imp_measurable[OF assms(1)]
  note bounded = integrable_bounded bounded_intros

  have 1:"bounded (range ((*) (±⇘η⇙) ∘ q ι))" "depends_on (q ι) ([J,I-J]!ι)"
    "q ι ∈ PiM ([J,I-J]!ι) (λ_. borel) →⇩M borel" "mono ((*) (±⇘η⇙) ∘ q ι)" if "ι ∈ {0,1}" for ι
    using that assms unfolding q_def conv_rel_to_sign by (auto intro:bounded_mult_comp)

  have 2: "((*) (±⇘η⇙::real)) ∈ borel →⇩M borel" by simp

  have 3:"∀ι<Suc (Suc 0). bounded (range (h ι))∧mono(h ι) ∧ depends_on (h ι) ([J,I-J]!ι) ∧
    h ι ∈ PiM ([J,I-J]!ι) (λ_. borel) →⇩M borel" unfolding All_less_Suc h_def
    by (intro conjI 1 depends_on_comp measurable_comp[OF _ 2]) auto

  have "covariance (f ∘ flip X) (g ∘ flip X) = covariance (q 0 ∘ flip X) (q 1 ∘ flip X)"
    unfolding q_def by simp
  also have "… = covariance (h 0 ∘ flip X) (h 1 ∘ flip X)"
    unfolding h_def covariance_def comp_def by (cases η) (auto simp:algebra_simps)
  also have "... ≤ 0" using 3 assms(1,2) numeral_2_eq_2 unfolding neg_assoc_def by metis
  finally show "covariance (f ∘ flip X) (g ∘ flip X) ≤ 0" by simp

  moreover have m_f: "random_variable borel (λx. f(λi. X i x))"
    using subsetD[OF assms(2)] by (subst depends_onD[OF assms(7)]) measurable
  moreover have m_g: "random_variable borel (λx. g(λi. X i x))"
    by (subst depends_onD[OF assms(8)]) measurable
  moreover have "integrable M (λω. ((f ∘ (λx y. X y x)) ω)⇧2)" unfolding comp_def
    by (intro bounded bounded_subset[OF assms(3)] measurable_compose[OF m_f]) auto
  moreover have "integrable M (λω. ((g ∘ (λx y. X y x)) ω)⇧2)" unfolding comp_def
    by (intro bounded bounded_subset[OF assms(4)] measurable_compose[OF m_g]) auto

  ultimately show  "?L ≤ ?R" by (subst (asm) covariance_eq) (auto simp:comp_def)
qed

lemma lim_min_n: "(λn. min (real n) x) ⇢ x"
proof -
  define m where "m = nat ⌈x⌉"
  have "min (real (n+m)) x = x" for n unfolding m_def by (intro min_absorb2) linarith
  hence "(λn. min (real (n+m)) x) ⇢ x" by simp
  thus ?thesis using LIMSEQ_offset[where k="m"] by fast
qed

lemma lim_clamp_n: "(λn. clamp (-real n) (real n) x) ⇢ x"
proof -
  define m where "m = nat ⌈¦x¦⌉"
  have "clamp (-real (n+m)) (real (n+m)) x = x" for n unfolding m_def
    by (intro clamp_eqI[symmetric]) linarith
  hence "(λn. clamp (-real (n+m)) (real (n+m)) x) ⇢ x" by simp
  thus ?thesis using LIMSEQ_offset[where k="m"] by fast
qed

lemma neg_assoc_imp_mult_mono:
  fixes f g :: "('i ⇒ 'c::linorder_topology) ⇒ real"
  assumes "neg_assoc X I"
  assumes "J ⊆ I"
  assumes "square_integrable M (f ∘ flip X)" "square_integrable M (g ∘ flip X)"
  assumes "monotone (≤) (≤≥⇘η⇙) f" "monotone (≤) (≤≥⇘η⇙) g"
  assumes "depends_on f J" "depends_on g (I-J)"
  assumes [measurable]: "f ∈ borel_measurable (Pi⇩M J (λ_. borel))"
  assumes [measurable]: "g ∈ borel_measurable (Pi⇩M (I-J) (λ_. borel))"
    shows "(∫ω. f (λi. X i ω) * g (λi. X i ω) ∂M) ≤ (∫x. f(λy. X y x)∂M) * (∫x. g(λy. X y x)∂M)"
      (is "?L ≤ ?R")
proof -
  let ?cf = "λn x. clamp (-real n) (real n) (f x)"
  let ?cg = "λn x. clamp (-real n) (real n) (g x)"

  note [measurable] = neg_assoc_imp_measurable[OF assms(1)]

  have m_f: "random_variable borel (λx. f(λi. X i x))"
    using subsetD[OF assms(2)] by (subst depends_onD[OF assms(7)]) measurable

  have m_g: "random_variable borel (λx. g(λi. X i x))"
    by (subst depends_onD[OF assms(8)]) measurable

  note intro_rules = borel_measurable_times measurable_compose[OF _ clamp_borel] AE_I2
    measurable_compose[OF _ borel_measurable_norm] lim_clamp_n m_f m_g

  have a: "(λn. (∫ω. ?cf n (λi. X i ω) * ?cg n (λi. X i ω) ∂M)) ⇢ ?L" using assms(3,4)
    by (intro integral_dominated_convergence[where w="λω. norm (f(λi. X i ω))*norm (g(λi. X i ω))"]
        intro_rules tendsto_mult cauchy_schwartz(1)[where M="M"])
       (auto intro!: clamp_abs_le mult_mono simp add:comp_def abs_mult)

  have "(λn. (∫x. ?cf n (λy. X y x)∂M)) ⇢ (∫x. f(λy. X y x)∂M)"
    using square_integrable_imp_integrable[OF m_f] assms(3) unfolding comp_def
    by (intro integral_dominated_convergence[where w = "λω. norm (f(λi. X i ω))"] intro_rules)
      (simp_all add:clamp_abs_le)

  moreover have "(λn. (∫x. ?cg n (λy. X y x)∂M)) ⇢ (∫x. g(λy. X y x)∂M)"
    using square_integrable_imp_integrable[OF m_g] assms(4) unfolding comp_def
    by (intro integral_dominated_convergence[where w = "λω. norm (g(λi. X i ω))"] intro_rules)
      (simp_all add:clamp_abs_le)

  ultimately have b: "(λn. (∫x. ?cf n (λy. X y x)∂M) * (∫x. ?cg n (λy. X y x) ∂M)) ⇢ ?R"
    by (rule tendsto_mult)

  show ?thesis
    by (intro lim_mono[OF _ a b, where N="0"] bounded_clamp_alt assms(5,6,9,10) monotone_clamp
        neg_assoc_imp_mult_mono_bounded[OF assms(1,2), where η="η"] depends_on_comp_2[OF assms(7)]
        measurable_compose[OF _ clamp_borel] depends_on_comp_2[OF assms(8)])
qed

text ‹Property P4~\cite{joagdev1983}›
lemma neg_assoc_subset:
  assumes "J ⊆ I"
  assumes "neg_assoc X I"
  shows "neg_assoc X J"
proof (rule neg_assocI,goal_cases)
  case (1 i)
  then show ?case using neg_assoc_imp_measurable[OF assms(2)] assms(1) by auto
next
  case (2 f g K)
  have a:"K ⊆ I" using 2 assms(1) by auto

  have "g = g ∘ (λm. restrict m (J-K))"
    using 2 depends_onD unfolding comp_def by (intro ext) auto
  also have "... ∈ borel_measurable (Pi⇩M (I - K) (λ_. borel))"
    using 2 assms(1) by (intro measurable_comp[OF measurable_restrict_subset]) auto
  finally have "g ∈ borel_measurable (Pi⇩M (I - K) (λ_. borel))" by simp
  moreover have "depends_on g (I-K)" using depends_on_mono assms(1) 2
    by (metis Diff_mono dual_order.eq_iff)
  ultimately show "covariance (f ∘ flip X) (g ∘ flip X) ≤ 0"
    using 2 by (intro neg_assoc_imp_mult_mono_bounded[OF assms(2) a, where η="Fwd"]) simp_all
qed

lemma neg_assoc_imp_mult_mono_nonneg:
  fixes f g :: "('i ⇒ 'c::linorder_topology) ⇒ real"
  assumes "neg_assoc X I" "J ⊆ I"
  assumes "range f ⊆ {0..}" "range g ⊆ {0..}"
  assumes "integrable M (f ∘ flip X)" "integrable M (g ∘ flip X)"
  assumes "monotone (≤) (≤≥⇘η⇙) f" "monotone (≤) (≤≥⇘η⇙) g"
  assumes "depends_on f J" "depends_on g (I-J)"
  assumes "f ∈ borel_measurable (Pi⇩M J (λ_. borel))" "g ∈ borel_measurable (Pi⇩M (I-J) (λ_. borel))"
  shows "has_int_that M (λω. f (flip X ω) * g (flip X ω))
    (λr. r ≤ expectation (f ∘ flip X) * expectation (g ∘ flip X))"
proof -
  let ?cf = "(λn x. min (real n) (f x))"
  let ?cg = "(λn x. min (real n) (g x))"

  define u where "u = (λω. f (λi. X i ω) * g (λi. X i ω))"
  define h where "h n ω = ?cf n  (λi. X i ω) * ?cg n (λi. X i ω)" for n ω
  define x where "x = (SUP n. expectation (h n))"

  note borel_intros = borel_measurable_times borel_measurable_const borel_measurable_min
    borel_measurable_power
  note bounded_intros' = integrable_bounded bounded_intros bounded_const_min

  have f_meas: "random_variable borel (λx. f (λi. X i x))"
    using borel_measurable_integrable[OF assms(5)] by (simp add:comp_def)
  have g_meas: "random_variable borel (λx. g (λi. X i x))"
    using borel_measurable_integrable[OF assms(6)] by (simp add:comp_def)

  have h_int: "integrable M (h n)" for n
    unfolding h_def using assms(3,4) by (intro bounded_intros' borel_intros f_meas g_meas) fast+

  have exp_h_le_R: "expectation (h n) ≤ expectation (f∘flip X) * expectation (g∘flip X)" for n
  proof -
    have "square_integrable M ((λa. min (real n) (f a)) ∘ (λx y. X y x))"
      using assms(3) unfolding comp_def
      by (intro bounded_intros' bdd_belowI[where m="0"] borel_intros f_meas) auto
    moreover have "square_integrable M ((λa. min (real n) (g a)) ∘ (λx y. X y x))"
      using assms(4) unfolding comp_def
      by (intro bounded_intros' bdd_belowI[where m="0"] borel_intros g_meas) auto
    moreover have "monotone (≤) (≤≥⇘η⇙) ((λa. min (real n) (f a)))"
      using monotoneD[OF assms(7)] unfolding comp_def min_mult_distrib_left
      by (intro monotoneI) (cases "η", fastforce+)
    moreover have "monotone (≤) (≤≥⇘η⇙) ((λa. min (real n) (g a)))"
      using monotoneD[OF assms(8)] unfolding comp_def min_mult_distrib_left
      by (intro monotoneI) (cases η, fastforce+)
    ultimately have "expectation (h n) ≤ expectation (?cf n∘flip X) * expectation (?cg n∘flip X)"
      unfolding h_def comp_def
      by (intro neg_assoc_imp_mult_mono[OF assms(1-2)] borel_intros assms(11,12)
          depends_on_comp_2[OF assms(10)] depends_on_comp_2[OF assms(9)]) (auto simp:comp_def)
    also have "... ≤ expectation (f∘flip X) * expectation (g∘flip X)"
      using assms(3,4) by (intro mult_mono integral_nonneg_AE AE_I2 integral_mono' assms(5,6)) auto
    finally show ?thesis by simp
  qed

  have h_mono_ptw: "AE ω in M. mono (λn. h n ω)"
    using assms(3,4) unfolding h_def by (intro AE_I2 monoI mult_mono) auto
  have h_mono: "mono (λn. expectation (h n))"
    by (intro monoI integral_mono_AE AE_mp[OF h_mono_ptw AE_I2] h_int) (simp add:mono_def)

  have "random_variable borel u" using f_meas g_meas unfolding u_def by (intro borel_intros)
  moreover have "AE ω in M. (λn. h n ω) ⇢ u ω"
    unfolding h_def u_def by (intro tendsto_mult lim_min_n AE_I2)
  moreover have "bdd_above (range (λn. expectation (h n)))"
    using exp_h_le_R by (intro bdd_aboveI) auto
  hence "(λn. expectation (h n)) ⇢ x"
    using LIMSEQ_incseq_SUP[OF _ h_mono] unfolding x_def by simp
  ultimately have "has_bochner_integral M u x" using h_int h_mono_ptw
    by (intro has_bochner_integral_monotone_convergence[where f="h"])
  moreover have "x ≤ expectation (f∘flip X) * expectation (g∘flip X)"
    unfolding x_def by (intro cSUP_least exp_h_le_R) simp
  ultimately show ?thesis unfolding has_bochner_integral_iff u_def has_int_that_def by auto
qed

text ‹Property P2~\cite{joagdev1983}›
lemma neg_assoc_imp_prod_mono:
  fixes f :: "'i ⇒ ('c::linorder_topology) ⇒ real"
  assumes "finite I"
  assumes "neg_assoc X I"
  assumes "⋀i. i ∈ I ⟹ integrable M (λω. f i (X i ω))"
  assumes "⋀i. i ∈ I ⟹ monotone (≤) (≤≥⇘η⇙) (f i)"
  assumes "⋀i. i ∈ I ⟹ range (f i)⊆{0..}"
  assumes "⋀i. i ∈ I ⟹ f i ∈ borel_measurable borel"
  shows "has_int_that M (λω. (∏i∈I. f i (X i ω))) (λr. r≤(∏i∈ I. expectation (λω. f i (X i ω))))"
  using assms
proof (induction I rule:finite_induct)
  case empty then show ?case by (simp add:has_int_that_def)
next
  case (insert x F)

  define g where "g v = f x (v x)" for v
  define h where "h v = (∏i∈F. f i (v i))" for v

  have 0: "{x} ⊆ insert x F" by auto

  have ran_g: "range g ⊆ {0..}" using insert(7) unfolding g_def by auto

  have "True = has_int_that M (λω. ∏i∈F. f i(X i ω)) (λr. r≤(∏i∈F. expectation(λω. f i(X i ω))))"
    by (intro true_eq_iff insert neg_assoc_subset[OF _ insert(4)]) auto
  also have "... = has_int_that M (h ∘ flip X) (λr. r ≤ (∏i∈F. expectation (λω. f i (X i ω))))"
    unfolding h_def by (intro arg_cong2[where f="has_int_that M"] refl)(simp add:comp_def)
  finally have 2: "has_int_that M (h ∘ flip X) (λr. r ≤ (∏i∈F. expectation (λω. f i (X i ω))))"
    by simp

  have "(∏i∈F. f i (v i)) ≥ 0" for v using insert(7) by (intro prod_nonneg) auto
  hence "range h ⊆ {0..}" unfolding h_def by auto
  moreover have "integrable M (g ∘ flip X)" unfolding g_def using insert(5) by (auto simp:comp_def)
  moreover have 3:"monotone (≤) (≤≥⇘η⇙) (f x)" using insert(6) by simp
  have "monotone (≤) (≤≥⇘η⇙) g" using monotoneD[OF 3]
    unfolding g_def by (intro monotoneI) (auto simp:comp_def le_fun_def)
  moreover have 4:"monotone (≤) (≤≥⇘η⇙) (f i)" "⋀x. f i x ≥ 0" if "i ∈ F" for i
    using that insert(6,7) by force+
  hence "monotone (≤) (≤≥⇘η⇙) h" using monotoneD[OF 4(1)] unfolding h_def
    by (intro monotoneI) (cases η, auto intro:prod_mono simp:comp_def le_fun_def)
  moreover have "depends_on g {x}" unfolding g_def by (intro depends_onI) force
  moreover have "depends_on h F"
    unfolding h_def by (intro depends_onI prod.cong refl) force
  hence "depends_on h (F - {x})" using insert(2) by simp
  moreover have "g ∈ borel_measurable (Pi⇩M {x} (λ_. borel))" unfolding g_def
    by (intro measurable_compose[OF _ insert(8)] measurable_component_singleton) auto
  moreover have "h ∈ borel_measurable (Pi⇩M F (λ_. borel))"
    unfolding h_def by (intro borel_measurable_prod measurable_compose[OF _ insert(8)]
        measurable_component_singleton) auto
  hence "h ∈ borel_measurable (Pi⇩M (F - {x}) (λ_. borel))" using insert(2) by simp
  ultimately have "True = has_int_that M (λω. g (flip X ω) * h (flip X ω))
    (λr. r ≤ expectation (g ∘ flip X) * expectation (h ∘ flip X))"
    by (intro true_eq_iff neg_assoc_imp_mult_mono_nonneg[OF insert(4) 0, where η="η"]
        ran_g has_int_thatD[OF 2]) simp_all
  also have "… = has_int_that M (λω. (∏i∈insert x F. f i (X i ω)))
    (λr. r ≤ expectation (g ∘ flip X) * expectation (h ∘ flip X))"
    unfolding g_def h_def using insert(1,2) by (intro arg_cong2[where f="has_int_that M"] refl) simp
  also have "… ≤ has_int_that M (λω. (∏i∈insert x F. f i (X i ω)))
    (λr. r ≤ expectation (g ∘ flip X) * (∏i ∈ F. expectation (f i ∘ X i)))"
    using ran_g has_int_thatD[OF 2] by (intro has_int_that_mono le_trans mult_left_mono
        integral_nonneg_AE AE_I2) (auto simp: comp_def)
  also have "… = has_int_that M
    (λω. ∏i∈insert x F. f i (X i ω)) (λr. r ≤ (∏i∈insert x F. expectation (f i ∘ X i)))"
    using insert(1,2) by (intro arg_cong2[where f="has_int_that M"] refl) (simp add:g_def comp_def)
  finally show ?case using le_boolE by (simp add:comp_def)
qed

text ‹Property P5~\cite{joagdev1983}›
lemma neg_assoc_compose:
  fixes f :: "'j ⇒ ('i ⇒ ('c::linorder_topology)) ⇒ ('d ::linorder_topology)"
  assumes "finite I"
  assumes "neg_assoc X I"
  assumes "⋀j. j ∈ J ⟹ deps j ⊆ I"
  assumes "⋀j1 j2. j1 ∈ J ⟹ j2 ∈ J ⟹ j1 ≠ j2 ⟹ deps j1 ∩ deps j2 = {}"
  assumes "⋀j. j ∈ J ⟹ monotone (≤) (≤≥⇘η⇙) (f j)"
  assumes "⋀j. j ∈ J ⟹ depends_on (f j) (deps j)"
  assumes "⋀j. j ∈ J ⟹ f j ∈ borel_measurable (PiM (deps j) (λ_. borel))"
  shows "neg_assoc (λj ω. f j (λi. X i ω)) J"
proof (rule neg_assocI, goal_cases)
  case (1 i)
  note [measurable] = neg_assoc_imp_measurable[OF assms(2)] assms(7)[OF 1]
  note 3 = assms(3)[OF 1]
  have 2: "f i (λi. X i ω) = f i (λi∈deps i. X i ω)" for ω
    using 3 by (intro depends_onD2[OF assms(6)] 1) fastforce
  show ?case unfolding 2 by measurable (rule subsetD[OF 3])
next
  case (2 g h K)

  let ?g = "(λω. g (λj. f j ω))"
  let ?h = "(λω. h (λj. f j ω))"

  note dep_f = depends_onD[OF depends_on_mono[OF _ assms(6)],symmetric]

  have g_alt_1: "?g = (λω. g (λj ∈ J. f j ω))"
    using 2(1) by (intro ext depends_onD[OF depends_on_mono[OF _ 2(2)]]) auto
  have g_alt_2: "?g = (λω. g (λj ∈ K. f j ω))"
    by (intro ext depends_onD[OF 2(2)])
  have g_alt_3: "?g = (λω. g (λj ∈ K. f j (restrict ω (deps j))))" unfolding g_alt_2 using 2(1)
    by (intro restrict_ext ext arg_cong[where f="g"] depends_onD[OF assms(6)]) auto

  have h_alt_1: "?h = (λω. h (λj ∈ J. f j ω))"
    by (intro ext depends_onD[OF depends_on_mono[OF _ 2(3)]]) auto
  have h_alt_2: "?h = (λω. h (λj ∈ J-K. f j ω))"
    by (intro ext depends_onD[OF 2(3)])
  have h_alt_3: "?h = (λω. h (λj ∈ J-K. f j (restrict ω (deps j))))" unfolding h_alt_2
    by (intro restrict_ext ext arg_cong[where f="h"] depends_onD[OF assms(6)]) auto

  have 3: "⋃ (deps ` (J-K)) ⊆ I - ⋃ (deps ` K)" using assms(3,4) 2(1) by blast

  have "⋃ (deps ` K) ⊆ I" using 2(1) assms(3) by auto
  moreover have "bounded (range ?g)" "bounded (range ?h)"
    using 2(6,7) by (auto intro: bounded_subset)
  moreover have "monotone (≤) (≤≥⇘η⇙) ?g"
    unfolding g_alt_1 using monotoneD[OF assms(5)]
    by (intro monotoneI) (cases η, auto intro!:monoD[OF 2(4)] le_funI)
  moreover have "monotone (≤) (≤≥⇘η⇙) ?h"
    unfolding h_alt_1 using monotoneD[OF assms(5)]
    by (intro monotoneI) (cases η, auto intro!:monoD[OF 2(5)] le_funI)
  moreover have "depends_on ?g (⋃ (deps ` K))"
    using 2(1) unfolding g_alt_2
    by (intro depends_onI arg_cong[where f="g"] restrict_ext depends_onD2[OF assms(6)]) auto
  moreover have "depends_on ?h (⋃ (deps ` (J-K)))"
    unfolding h_alt_2
    by (intro depends_onI arg_cong[where f="h"] restrict_ext depends_onD2[OF assms(6)]) auto
  hence "depends_on ?h (I - ⋃ (deps ` K))" using depends_on_mono[OF 3] by auto
  moreover have "?g ∈ borel_measurable (Pi⇩M (⋃ (deps ` K)) (λ_. borel))"
    unfolding g_alt_3 using 2(1)
    by (intro measurable_compose[OF _ 2(8)] measurable_compose[OF _ assms(7)]
        measurable_restrict measurable_component_singleton) auto
  moreover have "?h ∈ borel_measurable (Pi⇩M (I - ⋃ (deps ` K)) (λ_. borel))"
    unfolding h_alt_3 using 3
    by (intro measurable_compose[OF _ 2(9)] measurable_compose[OF _ assms(7)] measurable_restrict
        measurable_component_singleton) auto
  ultimately have "covariance (?g ∘ flip X) (?h ∘ flip X) ≤ 0"
    by (rule neg_assoc_imp_mult_mono_bounded[OF assms(2), where J="⋃(deps ` K)" and η="η"])
  thus "covariance (g ∘ (λx y. f y (λi. X i x))) (h ∘ (λx y. f y (λi. X i x))) ≤ 0"
    by (simp add:comp_def)
qed

lemma neg_assoc_compose_simple:
  fixes f :: "'i ⇒ ('c::linorder_topology) ⇒ ('d ::linorder_topology)"
  assumes "finite I"
  assumes "neg_assoc X I"
  assumes "⋀i. i ∈ I ⟹ monotone (≤) (≤≥⇘η⇙) (f i)"
  assumes [measurable]: "⋀i. i ∈ I ⟹ f i ∈ borel_measurable borel"
  shows "neg_assoc (λi ω. f i (X i ω)) I"
proof -
  have "depends_on (λω. f i (ω i)) {i}" if "i ∈ I" for i
    by (intro depends_onI) auto
  moreover have "monotone (≤) (≤≥⇘η⇙) (λω. f i (ω i))" if "i ∈ I" for i
    using monotoneD[OF assms(3)[OF that]] by (intro monotoneI) (cases η, auto dest:le_funE)
  ultimately show ?thesis
    by (intro neg_assoc_compose[OF assms(1,2), where deps="λi. {i}" and η="η"]) simp_all
qed

lemma covariance_distr:
  fixes f g :: "'b ⇒ real"
  assumes [measurable]: "φ ∈ M →⇩M N"  "f ∈ borel_measurable N"  "g ∈ borel_measurable N"
  shows "prob_space.covariance (distr M N φ) f g = covariance (f ∘ φ) (g ∘ φ)" (is "?L = ?R")
proof -
  let ?M' = "distr M N φ"
  have ps_distr: "prob_space ?M'" by (intro prob_space_distr) measurable
  interpret p2: prob_space ?M'
    using ps_distr by auto
  have "?L = expectation (λx. (f(φ x)-expectation (λx. f(φ x)))*(g(φ x)-expectation (λx. g(φ x))))"
    unfolding p2.covariance_def by (subst (1 2 3) integral_distr) measurable
  also have "… = ?R"
    unfolding covariance_def comp_def by simp
  finally show ?thesis by simp
qed

lemma neg_assoc_iff_distr:
  assumes [measurable]: "⋀i. i ∈ I ⟹ X i ∈ borel_measurable M"
  shows "neg_assoc X I ⟷
    prob_space.neg_assoc (distr M (PiM I (λ_. borel)) (λω. λi∈I. X i ω)) (flip id) I"
    (is "?L ⟷ ?R")
proof
  let ?M' = "distr M (Pi⇩M I (λ_. borel))  (λω. λi∈I. X i ω)"
  have ps_distr: "prob_space ?M'"
    by (intro prob_space_distr) measurable

  interpret p2: prob_space ?M'
    using ps_distr by auto

  show "?R" if "?L"
  proof (rule p2.neg_assocI, goal_cases)
    case (1 i)
    thus ?case using assms that unfolding id_def by measurable
  next
    case (2 f g J)

    have dep_I: "depends_on f I" "depends_on g I"
      using depends_on_mono[OF Diff_subset[of I J]] depends_on_mono[OF 2(1)] 2(2-3) by auto

    have f_meas[measurable]: "(λx. f x) ∈ borel_measurable (Pi⇩M I (λ_. borel))"
      by (subst depends_onD[OF 2(2)]) (intro 2 measurable_compose[OF measurable_restrict_subset])

    have g_meas[measurable]: "(λx. g x) ∈ borel_measurable (Pi⇩M I (λ_. borel))"
      by (subst depends_onD[OF 2(3)])
        (intro 2 measurable_compose[OF measurable_restrict_subset], auto)

    have "covariance (f ∘ id ∘ (λω. λi∈I. X i ω)) (g ∘ id ∘ (λω. λi∈I. X i ω)) =
      covariance (f ∘ flip X) (g ∘ flip X)"
      using depends_onD[OF dep_I(2)] depends_onD[OF dep_I(1)] by (simp add:comp_def)
    also have "… ≤ 0"
      using 2 by (intro neg_assoc_imp_mult_mono_bounded[OF that 2(1,6,7), where η="Fwd"]) simp_all
    finally have "covariance (f ∘ id ∘ (λω. λi∈I. X i ω)) (g ∘ id ∘ (λω. λi∈I. X i ω)) ≤ 0" by simp
    thus ?case by (subst covariance_distr) measurable
  qed

  show "?L" if "?R"
  proof (rule neg_assocI, goal_cases)
    case (1 i)
    then show ?case by measurable
  next
    case (2 f g J)

    have dep_I: "depends_on f I" "depends_on g I"
      using depends_on_mono[OF Diff_subset[of I J]] depends_on_mono[OF 2(1)] 2(2-3) by auto

    have f_meas[measurable]: "(λx. f x) ∈ borel_measurable (Pi⇩M I (λ_. borel))"
      by (subst depends_onD[OF 2(2)]) (intro 2 measurable_compose[OF measurable_restrict_subset])

    have g_meas[measurable]: "(λx. g x) ∈ borel_measurable (Pi⇩M I (λ_. borel))"
      by (subst depends_onD[OF 2(3)])
        (intro 2 measurable_compose[OF measurable_restrict_subset], auto)

    note [measurable] = 2(8,9)
    have "covariance (f ∘ (λx y. X y x)) (g ∘ (λx y. X y x)) =
      covariance (f ∘ (λω. λi∈I. X i ω)) (g ∘ (λω. λi∈I. X i ω))"
      using depends_onD[OF dep_I(2)] depends_onD[OF dep_I(1)] by (simp add:comp_def)
    also have "… =  p2.covariance (f ∘ id) (g ∘ id)" by (subst covariance_distr) measurable
    also have "… ≤ 0"
      using 2 by (intro p2.neg_assoc_imp_mult_mono_bounded[OF that 2(1), where η="Fwd"])
        (simp_all add:comp_def)
    finally show ?case by simp
  qed
qed

lemma neg_assoc_cong:
  assumes "finite I"
  assumes [measurable]: "⋀i. i ∈ I ⟹ Y i ∈ borel_measurable M"
  assumes "neg_assoc X I" "⋀i. i ∈ I ⟹ AE ω in M. X i ω = Y i ω"
  shows "neg_assoc Y I"
proof -
  have [measurable]: "⋀i. i ∈ I ⟹ X i ∈ borel_measurable M"
    using neg_assoc_imp_measurable[OF assms(3)] by auto

  let ?B = "(λ_. borel)"
  have a:"AE x in M. (∀i∈I. (X i x = Y i x))" by (intro AE_finite_allI assms)
  have "AE x in M. (λi∈I. X i x) = (λi∈I. Y i x)" by (intro AE_mp[OF a AE_I2]) auto
  hence b:"distr M (PiM I ?B) (λω. λi∈I. X i ω) = distr M (PiM I ?B) (λω. λi∈I. Y i ω)"
    by (intro distr_cong_AE refl) measurable
  have "prob_space.neg_assoc (distr M (PiM I (λ_. borel)) (λω. λi∈I. X i ω)) (flip id) I"
    using assms(2,3) by (intro iffD1[OF neg_assoc_iff_distr]) measurable
  thus ?thesis unfolding b using assms(2)
    by (intro iffD2[OF neg_assoc_iff_distr[where I="I"]])  auto
qed

lemma neg_assoc_reindex_aux:
  assumes "inj_on h I"
  assumes "neg_assoc X (h ` I)"
  shows "neg_assoc (λk. X (h k)) I"
proof (rule neg_assocI, goal_cases)
  case (1 i) thus ?case using neg_assoc_imp_measurable[OF assms(2)] by simp
next
  case (2 f g J)
  let ?f = "(λω. f (compose J ω h))"
  let ?g = "(λω. g (compose (I-J) ω h))"

  note neg_assoc_imp_mult_mono_intros =
    neg_assoc_imp_mult_mono_bounded(1)[OF assms(2), where J="h`J" and η="Fwd"]
    measurable_compose[OF _ 2(8)] measurable_compose[OF _ 2(9)]
    measurable_compose[OF _ measurable_finmap_compose]
    bounded_range_imp[OF 2(6)] bounded_range_imp[OF 2(7)]

  have [simp]:"h ` I - h ` J =  h ` (I-J)"
    using assms(1) 2(1) by (simp add: inj_on_image_set_diff)

  have "covariance (f∘(λx y. X(h y)x)) (g∘(λx y. X(h y)x)) = covariance (?f ∘ flip X) (?g ∘ flip X)"
    unfolding comp_def
    by (intro arg_cong2[where f="covariance"] ext depends_onD2[OF 2(2)] depends_onD2[OF 2(3)])
     (auto simp:compose_def)
  also have "… ≤ 0" using 2(1)
    by (intro neg_assoc_imp_mult_mono_intros monotoneI depends_onI) (auto intro!:
        monoD[OF 2(4)] monoD[OF 2(5)] simp:le_fun_def compose_def restrict_def cong:if_cong)
  finally show ?case by simp
qed

lemma neg_assoc_reindex:
  assumes "inj_on h I" "finite I"
  shows "neg_assoc X (h ` I) ⟷ neg_assoc (λk. X (h k)) I" (is "?L ⟷ ?R")
proof
  assume ?L
  thus ?R using neg_assoc_reindex_aux[OF assms(1)] by blast
next
  note inv_h_inj = inj_on_the_inv_into[OF assms(1)]
  assume a:?R
  hence b:"neg_assoc (λk. X (h (the_inv_into I h k))) (h ` I)"
    using the_inv_into_onto[OF assms(1)] by (intro neg_assoc_reindex_aux[OF inv_h_inj]) auto
  show ?L
    using f_the_inv_into_f[OF assms(1)] neg_assoc_imp_measurable[OF a] assms(2)
    by (intro neg_assoc_cong[OF _ _ b]) auto
qed

lemma measurable_compose_merge_1:
  assumes "depends_on h K"
  assumes "h ∈ PiM K M' →⇩M N" "K ⊆ I ∪ J"
  assumes "(λx. restrict (fst (f x)) (K ∩ I)) ∈ A →⇩M PiM (K ∩ I) M'"
  assumes "(λx. restrict (snd (f x)) (K ∩ J)) ∈ A →⇩M PiM (K ∩ J) M'"
  shows "(λx. h(merge I J (f x))) ∈ A →⇩M N"
proof -
  let ?f1 = "λx. fst (f x)"
  let ?f2 = "λx. snd (f x)"
  let ?g1 = "λx. restrict (fst (f x)) (K ∩ I)"
  let ?g2 = "λx. restrict (snd (f x)) (K ∩ J)"

  have a1:"(λx. merge I J (?g1 x, ?g2 x) i) ∈ A →⇩M M' i" if "i ∈ K ∩ I" for i
    using that measurable_compose[OF assms(4) measurable_component_singleton[OF that]]
    by (simp add:merge_def)

  have a2:"(λx. merge I J (?g1 x, ?g2 x) i) ∈ A →⇩M M' i" if "i ∈ K ∩ J" "i ∉ I" for i
    using that measurable_compose[OF assms(5) measurable_component_singleton[OF that(1)]]
    by (simp add:merge_def)

  have a:"(λx. merge I J (?g1 x, ?g2 x) i) ∈ A →⇩M M' i" if "i ∈ K" for i
    using assms(3) a1 a2 that by auto

  have "(λx. h(merge I J (f x))) = (λx. h(merge I J (?f1 x, ?f2 x)))" by simp
  also have "… = (λx. h(λi ∈ K. merge I J (?f1 x, ?f2 x) i))"
    using depends_onD[OF assms(1)] by simp
  also have "… = (λx. h(λi ∈ K. merge I J (?g1 x, ?g2 x) i))"
    by (intro ext arg_cong[where f="h"]) (auto simp:comp_def restrict_def merge_def case_prod_beta)
  also have "… ∈ A →⇩M N"
    by (intro measurable_compose[OF _ assms(2)] measurable_restrict a)
  finally show ?thesis by simp
qed

lemma measurable_compose_merge_2:
  assumes "depends_on h K" "h ∈ PiM K M' →⇩M N" "K ⊆ I ∪ J"
  assumes "(λx. restrict (f x) (K ∩ I)) ∈ A →⇩M PiM (K ∩ I) M'"
  assumes "(λx. restrict (g x) (K ∩ J)) ∈ A →⇩M PiM (K ∩ J) M'"
  shows "(λx. h(merge I J (f x, g x))) ∈ A →⇩M N"
  using assms by (intro measurable_compose_merge_1[OF assms(1-3)]) simp_all

lemma neg_assoc_combine:
  fixes I I1 I2 :: "'i set"
  fixes X :: "'i ⇒ 'a ⇒ ('b::linorder_topology)"
  assumes "finite I" "I1 ∪ I2 = I" "I1 ∩ I2 = {}"
  assumes "indep_var (PiM I1 (λ_. borel)) (λω. λi∈I1. X i ω) (PiM I2 (λ_. borel)) (λω. λi∈I2. X i ω)"
  assumes "neg_assoc X I1"
  assumes "neg_assoc X I2"
  shows "neg_assoc X I"
proof -
  define X' where "X' i = (if i ∈ I then X i else (λ_. undefined))" for i

  have X_measurable: "random_variable borel (X i)" if "i ∈ I" for i
    using that assms(2) neg_assoc_imp_measurable[OF assms(5)]
      neg_assoc_imp_measurable[OF assms(6)] by auto

  have rv[measurable]: "random_variable borel (X' i)" for i
    unfolding X'_def using X_measurable by auto

  have na_I1: "neg_assoc X' I1" using neg_assoc_cong
    unfolding X'_def using assms(1,2) neg_assoc_imp_measurable[OF assms(5)]
    by (intro neg_assoc_cong[OF _ _ assms(5)] AE_I2) auto

  have na_I2: "neg_assoc X' I2" using neg_assoc_cong
    unfolding X'_def using assms(1,2) neg_assoc_imp_measurable[OF assms(6)]
    by (intro neg_assoc_cong[OF _ _ assms(6)] AE_I2) auto

  have iv:"indep_var(PiM I1 (λ_. borel))(λω. λi∈I1. X' i ω)(PiM I2 (λ_. borel))(λω. λi∈I2. X' i ω)"
    using assms(2,4) unfolding indep_var_def X'_def by (auto simp add:restrict_def cong:if_cong)

  let ?N = "Pi⇩M I1 (λ_. borel) ⨂⇩M Pi⇩M I2 (λ_. borel)"
  let ?A = "distr M (Pi⇩M I1 (λ_. borel)) (λω. λi∈I1. X' i ω)"
  let ?B = "distr M (Pi⇩M I2 (λ_. borel)) (λω. λi∈I2. X' i ω)"
  let ?H = "distr M ?N (λω. (λi∈I1. X' i ω, λi∈I2. X' i ω))"

  have indep: "?H = (?A ⨂⇩M ?B)"
    and rvs: "random_variable (Pi⇩M I1 (λ_. borel)) (λω. λi∈I1. X' i ω)"
             "random_variable (Pi⇩M I2 (λ_. borel)) (λω. λi∈I2. X' i ω)"
    using iffD1[OF indep_var_distribution_eq iv] by auto

  interpret pa: prob_space ?A by (intro prob_space_distr rvs)
  interpret pb: prob_space ?B by (intro prob_space_distr rvs)
  interpret pair_sigma_finite ?A ?B
    using pa.sigma_finite_measure pb.sigma_finite_measure by (intro pair_sigma_finite.intro)

  interpret pab: prob_space "(?A ⨂⇩M ?B)"
    by (intro prob_space_pair pa.prob_space_axioms pb.prob_space_axioms)

  have pa_na: "pa.neg_assoc (λx y. y x) I1"
    using assms(2) iffD1[OF neg_assoc_iff_distr na_I1] by fastforce

  have pb_na: "pb.neg_assoc (λx y. y x) I2"
    using assms(2) iffD1[OF neg_assoc_iff_distr na_I2] by fastforce

  have na_X': "neg_assoc X' I"
  proof (rule neg_assocI2, goal_cases)
    case (1 i) thus ?case by measurable
  next
    case (2 f g K)

    note bounded_intros =
      bounded_range_imp[OF 2(6)] bounded_range_imp[OF 2(7)] pa.integrable_bounded
      pb.integrable_bounded pab.integrable_bounded bounded_intros pb.finite_measure_axioms

    have [measurable]:
      "restrict x I ∈ space (Pi⇩M I (λ_. borel))" for x :: "('i ⇒ 'b)" and I by (simp add:space_PiM)

    have a: "K ⊆ I1 ∪ I2" using 2 assms(2) by auto
    have b: "I-K ⊆ I1 ∪ I2" using assms(2) by auto

    note merge_1 = measurable_compose_merge_2[OF 2(2,8) a] measurable_compose_merge_2[OF 2(3,9) b]
    note merge_2 = measurable_compose_merge_1[OF 2(2,8) a] measurable_compose_merge_1[OF 2(3,9) b]

    have merge_mono:
      "merge I1 I2 (w, y) ≤ merge I1 I2 (x, z)" if "w ≤ x" "y ≤ z" for w x y z :: "'i ⇒ 'b"
      using le_funD[OF that(1)] le_funD[OF that(2)] unfolding merge_def by (intro le_funI) auto

    have split_h: "h ∘ flip X' = (λω. h (merge I1 I2 (λi∈I1. X' i ω, λi∈I2. X' i ω)))"
      if "depends_on h I" for h :: "_ ⇒ real"
      using assms(2) unfolding comp_def
      by (intro ext depends_onD2[OF that]) (auto simp:restrict_def merge_def)

    have "depends_on f I" "depends_on g I"
      using 2(1) by (auto intro:depends_on_mono[OF _ 2(2)] depends_on_mono[OF _ 2(3)])
    note split = split_h[OF this(1)] split_h[OF this(2)]

    have step_1: "(∫y. f (merge I1 I2 (x, y)) * g (merge I1 I2 (x, y)) ∂?B) ≤
      (∫y. f (merge I1 I2 (x, y))∂ ?B) * (∫y. g (merge I1 I2 (x, y)) ∂?B)" (is "?L1 ≤ ?R1")
       for x
    proof -
      have step1_1: "monotone (≤) (≤≥⇘Fwd⇙) (λa. f (merge I1 I2 (x, a)))"
        unfolding dir_le by (intro monoI monoD[OF 2(4)] merge_mono) simp
      have step1_2: "monotone (≤) (≤≥⇘Fwd⇙) (λa. g (merge I1 I2 (x, a)))"
        unfolding dir_le by (intro monoI monoD[OF 2(5)] merge_mono) simp
      have step1_3: "depends_on (λa. f (merge I1 I2 (x, a))) (K ∩ I2)"
        by (subst depends_onD[OF 2(2)])
          (auto intro:depends_onI simp:merge_def restrict_def cong:if_cong)
      have step1_4: "depends_on (λa. g (merge I1 I2 (x, a))) (I2 - K ∩ I2)"
        by (subst depends_onD[OF 2(3)])
          (auto intro:depends_onI simp:merge_def restrict_def cong:if_cong)
      show ?thesis
        by (intro pb.neg_assoc_imp_mult_mono_bounded(2)[OF pb_na, where η="Fwd" and J="K ∩ I2"]
            bounded_intros merge_1 step1_1 step1_2 step1_3 step1_4) measurable
    qed

    have step2_1: "monotone (≤) (≤≥⇘Fwd⇙) (λa. pb.expectation (λy. f (merge I1 I2 (a,y))))"
      unfolding dir_le
      by (intro monoI integral_mono bounded_intros merge_1 monoD[OF 2(4)] merge_mono) measurable

    have step2_2: "monotone (≤) (≤≥⇘Fwd⇙) (λa. pb.expectation (λy. g (merge I1 I2 (a,y))))"
      unfolding dir_le
      by (intro monoI integral_mono bounded_intros merge_1 monoD[OF 2(5)] merge_mono) measurable

    have step2_3: "depends_on (λa. pb.expectation (λy. f (merge I1 I2 (a, y)))) (K ∩ I1)"
      by (subst depends_onD[OF 2(2)])
        (auto intro:depends_onI simp:merge_def restrict_def cong:if_cong)

    have step2_4: "depends_on (λa. pb.expectation (λy. g (merge I1 I2 (a, y)))) (I1-K∩I1)"
      by (subst depends_onD[OF 2(3)])
        (auto intro:depends_onI simp:merge_def restrict_def cong:if_cong)

    have "(∫ω. (f∘flip X') ω * (g∘flip X') ω ∂M) = (∫ω. f (merge I1 I2 ω) * g(merge I1 I2 ω) ∂?H)"
      unfolding split by (intro integral_distr[symmetric] merge_2 borel_measurable_times) measurable
    also have "… = (∫ω. f(merge I1 I2 ω) * g(merge I1 I2 ω) ∂ (?A ⨂⇩M ?B))"
      unfolding indep by simp
    also have "… = (∫x. (∫y. f(merge I1 I2 (x,y)) * g(merge I1 I2 (x,y)) ∂?B) ∂?A)"
      by (intro integral_fst'[symmetric] bounded_intros merge_2 borel_measurable_times)
        measurable
    also have "… ≤ (∫x. (∫y. f(merge I1 I2 (x,y)) ∂?B) * (∫y. g(merge I1 I2 (x,y)) ∂?B) ∂?A)"
      by (intro integral_mono_AE bounded_intros step_1 AE_I2 pb.borel_measurable_lebesgue_integral
          borel_measurable_times iffD2[OF measurable_split_conv] merge_2) measurable
    also have "… ≤(∫x.(∫y. f(merge I1 I2 (x,y))∂?B)∂?A)*(∫x.(∫y. g(merge I1 I2(x,y))∂?B)∂?A)"
      by (intro pa.neg_assoc_imp_mult_mono_bounded[OF pa_na, where η="Fwd" and J="K ∩ I1"]
          bounded_intros pb.borel_measurable_lebesgue_integral iffD2[OF measurable_split_conv]
          merge_2 step2_1 step2_2 step2_3 step2_4) measurable
    also have "… = (∫ω. f(merge I1 I2 ω) ∂(?A ⨂⇩M ?B)) * (∫ω. g(merge I1 I2 ω) ∂(?A ⨂⇩M ?B))"
      by (intro arg_cong2[where f="(*)"] integral_fst' merge_2 bounded_intros) measurable
    also have "… = (∫ω. f(merge I1 I2 ω) ∂?H) * (∫ω. g(merge I1 I2 ω) ∂?H)"
      unfolding indep by simp
    also have "… = (∫ω. (f∘flip X') ω ∂M) * (∫ω. (g∘flip X') ω ∂M)"
      unfolding split by (intro arg_cong2[where f="(*)"] integral_distr merge_2) measurable
    finally show ?case by (simp add:comp_def)
  qed
  show ?thesis by (intro neg_assoc_cong[OF assms(1) X_measurable na_X']) (simp_all add:X'_def)
qed

text ‹Property P7~\cite{joagdev1983}›
lemma neg_assoc_union:
  fixes I :: "'i set"
  fixes p :: "'j ⇒ 'i set"
  fixes X :: "'i ⇒ 'a ⇒ ('b::linorder_topology)"
  assumes "finite I" "⋃(p ` J) = I"
  assumes "indep_vars (λj. PiM (p j) (λ_. borel)) (λj ω. λi ∈ p j. X i ω) J"
  assumes "⋀j. j ∈ J ⟹ neg_assoc X (p j)"
  assumes "disjoint_family_on p J"
  shows "neg_assoc X I"
proof -
  let ?B = "(λ_. borel)"
  define T where "T = {j ∈ J. p j ≠ {}}"

  define g where "g i = (THE j. j ∈ J ∧ i ∈ p j)" for i
  have g: "g i = j" if "i ∈ p j" "j ∈ J" for i j unfolding g_def
  proof (rule the1_equality)
    show "∃!j. j ∈ J ∧ i ∈ p j"
      using assms(5) that unfolding bex1_def disjoint_family_on_def by auto
    show "j ∈ J ∧ i ∈ p j" using that by auto
  qed

  have ran_T: "T ⊆ J" unfolding T_def by simp
  hence "disjoint_family_on p T" using assms(5) disjoint_family_on_mono by metis
  moreover have "finite (⋃(p ` T))" using ran_T assms(1,2)
    by (meson Union_mono finite_subset image_mono)
  moreover have "⋀i. i ∈ T ⟹ p i ≠ {}" unfolding T_def by auto
  ultimately have fin_T: "finite T" using infinite_disjoint_family_imp_infinite_UNION by auto

  have "neg_assoc X (⋃(p ` T))"
    using fin_T ran_T
  proof (induction T rule:finite_induct)
    case empty thus ?case using neg_assoc_empty by simp
  next
    case (insert x F)

    note r = indep_var_compose[OF indep_var_restrict[OF assms(3), where A="F" and B="{x}"] _]

    have a: "(λω. λi∈⋃(p`F). X i ω) = (λω. λi∈⋃(p`F). ω (g i) i) ∘ (λω. λi∈F. λi∈p i. X i ω)"
      using insert(4) g by (intro restrict_ext ext) auto
    have b: "(λω. λi∈p x. X i ω) = (λω i. ω x i) ∘ (λω. λi∈{x}. λi∈p i. X i ω)"
      by (simp add:comp_def restrict_def)

    have c:"(λx. x (g i) i) ∈ borel_measurable (Pi⇩M F (λj. Pi⇩M (p j) ?B))" if "i ∈ (⋃(p`F))" for i
    proof -
      have h: "i ∈ p (g i)" and q: "g i ∈ F" using g that insert(4) by auto
      thus ?thesis
        by (intro measurable_compose[OF measurable_component_singleton[OF q]]) measurable
    qed

    have "finite (⋃ (p ` insert x F))" using assms(1,2) insert(4)
      by (meson Sup_subset_mono image_mono infinite_super)
    moreover have "⋃ (p ` F) ∪ p x = ⋃ (p ` insert x F)" by auto
    moreover have "⋃ (p ` F) ∩ p x = {}"
      using assms(5) insert(2,4) unfolding disjoint_family_on_def by fast
    moreover have
      "indep_var (PiM (⋃(p`F)) ?B) (λω. λi∈⋃(p`F). X i ω) (PiM (p x) ?B) (λω. λi∈p x. X i ω)"
      unfolding a b using insert(1,2,4) by (intro r measurable_restrict c) simp_all
    moreover have "neg_assoc X (⋃ (p ` F))" using insert(4) by (intro insert(3)) auto
    moreover have "neg_assoc X (p x)" using insert(4) by (intro assms(4)) auto
    ultimately show ?case by (rule neg_assoc_combine)
  qed
  moreover have "(⋃(p ` T)) = I" using assms(2) unfolding T_def by auto
  ultimately show ?thesis by auto
qed

text ‹Property P5~\cite{joagdev1983}›
lemma indep_imp_neg_assoc:
  assumes "finite I"
  assumes "indep_vars (λ_. borel) X I"
  shows "neg_assoc X I"
proof -
  have a:"neg_assoc X {i}" if "i ∈ I" for i
    using that assms(2) unfolding indep_vars_def
    by (intro neg_assoc_singleton) auto
  have b: "(⋃j∈I. {j}) = I" by auto
  have c: "indep_vars (λj. Pi⇩M {j} (λ_. borel)) (λj ω. λi∈{j}. X j ω) I"
    by (intro indep_vars_compose2[OF assms(2)]) measurable
  have d: "indep_vars (λj. Pi⇩M {j} (λ_. borel)) (λj ω. λi∈{j}. X i ω) I"
    by (intro iffD2[OF indep_vars_cong c] restrict_ext ext) auto
  show ?thesis by (intro neg_assoc_union[OF assms(1) b d a]) (auto simp:disjoint_family_on_def)
qed

end

lemma neg_assoc_map_pmf:
  shows "measure_pmf.neg_assoc (map_pmf f p) X I = measure_pmf.neg_assoc p (λi ω. X i (f ω)) I"
    (is "?L ⟷ ?R")
proof -
  let ?d1 = "distr (measure_pmf (map_pmf f p)) (Pi⇩M I (λ_. borel)) (λω. λi∈I. X i ω)"
  let ?d2 = "distr (measure_pmf p) (Pi⇩M I (λ_. borel)) (λω. λi∈I. X i (f ω))"

  have "emeasure ?d1 A = emeasure ?d2 A" if "A ∈ sets (Pi⇩M I (λ_. borel))" for A
  proof -
    have "emeasure ?d1 A = emeasure (measure_pmf p) {x. (λi∈I. X i (f x)) ∈ A}"
      using that by (subst emeasure_distr) (simp_all add:vimage_def space_PiM)
    also have "… = emeasure ?d2 A"
      using that by (subst emeasure_distr) (simp_all add:space_PiM vimage_def)
    finally show ?thesis by simp
  qed

  hence a:"?d1 = ?d2" by (intro measure_eqI) auto

  have "?L ⟷ prob_space.neg_assoc ?d1 (λx y. y x) I"
    by (subst measure_pmf.neg_assoc_iff_distr) auto
  also have "… ⟷ prob_space.neg_assoc ?d2 (λx y. y x) I"
    unfolding a by simp
  also have "… ⟷ ?R"
    by (subst measure_pmf.neg_assoc_iff_distr) auto
  finally show ?thesis by simp
qed

end