Theory Misc

(*
 * Copyright (C) 2014 NICTA
 * All rights reserved.
 *)

(* Author: David Cock - David.Cock@nicta.com.au *)

section ‹Miscellaneous Mathematics›

theory Misc 
imports 
  "HOL-Analysis.Multivariate_Analysis"
begin

text_raw ‹\label{s:misc}›

lemma sum_UNIV:
  fixes S::"'a::finite set"
  assumes complete: "⋀x. x∉S ⟹ f x = 0"
  shows "sum f S = sum f UNIV"
proof -
  from complete have "sum f S = sum f (UNIV - S) + sum f S" by(simp)
  also have "... = sum f UNIV"
    by(auto intro: sum.subset_diff[symmetric])
  finally show ?thesis .
qed

lemma cInf_mono:
  fixes A::"'a::conditionally_complete_lattice set"
  assumes lower: "⋀b. b ∈ B ⟹ ∃a∈A. a ≤ b"
      and bounded: "⋀a. a ∈ A ⟹ c ≤ a"
      and ne: "B ≠ {}"
  shows "Inf A ≤ Inf B"
proof(rule cInf_greatest[OF ne])
  fix b assume bin: "b ∈ B"
  with lower obtain a where ain: "a ∈ A" and le: "a ≤ b" by(auto)
  from ain bounded have "Inf A ≤ a" by(intro cInf_lower bdd_belowI, auto)
  also note le
  finally show "Inf A ≤ b" .
qed

lemma max_distrib:
  fixes c::real
  assumes nn: "0 ≤ c"
  shows "c * max a b = max (c * a) (c * b)"
proof(cases "a ≤ b")
  case True
  moreover with nn have "c * a ≤ c * b" by(auto intro:mult_left_mono)
  ultimately show ?thesis by(simp add:max.absorb2)
next
  case False then have "b ≤ a" by(auto)
  moreover with nn have "c * b ≤ c * a" by(auto intro:mult_left_mono)
  ultimately show ?thesis by(simp add:max.absorb1)
qed

lemma mult_div_mono_left:
  fixes c::real
  assumes nnc: "0 ≤ c" and nzc: "c ≠ 0"
      and inv: "a ≤ inverse c * b"
  shows "c * a ≤ b"
proof -
  from nnc inv have "c * a ≤ (c * inverse c) * b"
    by(auto simp:mult.assoc intro:mult_left_mono)
  also from nzc have "... = b" by(simp)
  finally show "c * a ≤ b" .
qed

lemma mult_div_mono_right:
  fixes c::real
  assumes nnc: "0 ≤ c" and nzc: "c ≠ 0"
      and inv: "inverse c * a ≤ b"
  shows "a ≤ c * b"
proof -
  from nzc have "a = (c * inverse c) * a " by(simp)
  also from nnc inv have "(c * inverse c) * a ≤ c * b"
    by(auto simp:mult.assoc intro:mult_left_mono)
  finally show "a ≤ c * b" .
qed

lemma min_distrib:
  fixes c::real
  assumes nnc: "0 ≤ c"
  shows "c * min a b = min (c * a) (c * b)"
proof(cases "a ≤ b")
  case True moreover with nnc have "c * a ≤ c * b"
    by(blast intro:mult_left_mono)
  ultimately show ?thesis by(auto)
next
  case False hence "b ≤ a" by(auto)
  moreover with nnc have "c * b ≤ c * a"
    by(blast intro:mult_left_mono)
  ultimately show ?thesis by(simp add:min.absorb2)
qed

lemma finite_set_least:
  fixes S::"'a::linorder set"
  assumes finite: "finite S"
      and ne: "S ≠ {}"
  shows "∃x∈S. ∀y∈S. x ≤ y"
proof -
  have "S = {} ∨ (∃x∈S. ∀y∈S. x ≤ y)"
  proof(rule finite_induct, simp_all add:assms)
    fix x::'a and S::"'a set"
    assume IH: "S = {} ∨ (∃x∈S. ∀y∈S. x ≤ y)"
    show "(∀y∈S. x ≤ y) ∨ (∃x'∈S. x' ≤ x ∧ (∀y∈S. x' ≤ y))"
    proof(cases "S={}")
      case True then show ?thesis by(auto)
    next
      case False with IH have "∃x∈S. ∀y∈S. x ≤ y" by(auto)
      then obtain z where zin: "z ∈ S" and zmin: "∀y∈S. z ≤ y" by(auto)
      thus ?thesis by(cases "z ≤ x", auto)
    qed
  qed
  with ne show ?thesis by(auto)
qed

lemma cSup_add:
  fixes c::real
  assumes ne: "S ≠ {}"
      and bS: "⋀x. x∈S ⟹ x ≤ b"
  shows "Sup S + c = Sup {x + c |x. x ∈ S}"
proof(rule antisym)
  from ne bS show "Sup {x + c |x. x ∈ S} ≤ Sup S + c"
    by(auto intro!:cSup_least add_right_mono cSup_upper bdd_aboveI)

  have "Sup S ≤ Sup {x + c |x. x ∈ S} - c"
  proof(intro cSup_least ne)
    fix x assume xin: "x ∈ S"
    from bS have "⋀x. x∈S ⟹ x + c ≤ b + c" by(auto intro:add_right_mono)
    hence "bdd_above {x + c |x. x ∈ S}" by(intro bdd_aboveI, blast)
    with xin have "x + c ≤ Sup {x + c |x. x ∈ S}" by(auto intro:cSup_upper)
    thus "x ≤ Sup {x + c |x. x ∈ S} - c" by(auto)
  qed
  thus "Sup S + c ≤ Sup {x + c |x. x ∈ S}" by(auto)
qed

lemma cSup_mult:
  fixes c::real
  assumes ne: "S ≠ {}"
      and bS: "⋀x. x∈S ⟹ x ≤ b"
      and nnc: "0 ≤ c"
  shows "c * Sup S = Sup {c * x |x. x ∈ S}"
proof(cases)
  assume "c = 0"
  moreover from ne have "∃x. x ∈ S" by(auto)
  ultimately show ?thesis by(simp)
next
  assume cnz: "c ≠ 0"
  show ?thesis
  proof(rule antisym)
    from bS have baS: "bdd_above S" by(intro bdd_aboveI, auto)
    with ne nnc show "Sup {c * x |x. x ∈ S} ≤ c * Sup S"
      by(blast intro!:cSup_least mult_left_mono[OF cSup_upper])
    have "Sup S ≤ inverse c * Sup {c * x |x. x ∈ S}"
    proof(intro cSup_least ne)
      fix x assume xin: "x∈S"
      moreover from bS nnc have "⋀x. x∈S ⟹ c * x ≤ c * b" by(auto intro:mult_left_mono)
      ultimately have "c * x ≤ Sup {c * x |x. x ∈ S}"
        by(auto intro!:cSup_upper bdd_aboveI)
      moreover from nnc have "0 ≤ inverse c" by(auto)
      ultimately have "inverse c * (c * x) ≤ inverse c * Sup {c * x |x. x ∈ S}"
        by(auto intro:mult_left_mono)
      with cnz show "x ≤ inverse c * Sup {c * x |x. x ∈ S}"
        by(simp add:mult.assoc[symmetric])
    qed
    with nnc have "c * Sup S ≤ c * (inverse c * Sup {c * x |x. x ∈ S})"
      by(auto intro:mult_left_mono)
    with cnz show "c * Sup S ≤ Sup {c * x |x. x ∈ S}"
      by(simp add:mult.assoc[symmetric])
  qed
qed

lemma closure_contains_Sup:
  fixes S :: "real set"
  assumes neS: "S ≠ {}" and bS: "∀x∈S. x ≤ B"
  shows "Sup S ∈ closure S"
proof -
  let ?T = "uminus ` S"
  from neS have neT: "?T ≠ {}" by(auto)
  from bS have bT: "∀x∈?T. -B ≤ x" by(auto)
  hence bbT: "bdd_below ?T" by(intro bdd_belowI, blast)

  have "Sup S = - Inf ?T"
  proof(rule antisym)
    from neT bbT
    have "⋀x. x∈S ⟹ Inf (uminus ` S) ≤ -x"
      by(blast intro:cInf_lower)
    hence "⋀x. x∈S ⟹ -1 * -x ≤ -1 * Inf (uminus ` S)"
      by(rule mult_left_mono_neg, auto)
    hence lenInf: "⋀x. x∈S ⟹ x ≤ - Inf (uminus ` S)"
      by(simp)
    with neS bS show "Sup S ≤ - Inf ?T"
      by(blast intro:cSup_least)

    have "- Sup S ≤ Inf ?T"
    proof(rule cInf_greatest[OF neT])
      fix x assume "x ∈ uminus ` S"
      then obtain y where yin: "y ∈ S" and rwx: "x = -y" by(auto)
      from yin bS have "y ≤ Sup S"
        by(intro cSup_upper bdd_belowI, auto)
      hence "-1 * Sup S ≤ -1 * y"
        by(simp add:mult_left_mono_neg)
      with rwx show "- Sup S ≤ x" by(simp)
    qed
    hence "-1 * Inf ?T ≤ -1 * (- Sup S)"
      by(simp add:mult_left_mono_neg)
    thus "- Inf ?T ≤ Sup S" by(simp)
  qed
  also {
    from neT bbT have "Inf ?T ∈ closure ?T" by(rule closure_contains_Inf)
    hence "- Inf ?T ∈ uminus ` closure ?T" by(auto)
  }
  also {
    have "linear uminus" by(auto intro:linearI)
    hence "uminus ` closure ?T ⊆ closure (uminus ` ?T)"
      by(rule closure_linear_image_subset)
  }
  also {
    have "uminus ` ?T ⊆ S" by(auto)
    hence "closure (uminus ` ?T) ⊆ closure S" by(rule closure_mono)
  }
  finally show "Sup S ∈ closure S" .
qed

lemma tendsto_min:
  fixes x y::real
  assumes ta: "a ⇢ x"
      and tb: "b ⇢ y"
  shows "(λi. min (a i) (b i)) ⇢ min x y"
proof(rule LIMSEQ_I, simp)
  fix e::real assume pe: "0 < e"

  from ta pe obtain noa where balla: "∀n≥noa. abs (a n - x) < e"
    by(auto dest:LIMSEQ_D)
  from tb pe obtain nob where ballb: "∀n≥nob. abs (b n - y) < e"
    by(auto dest:LIMSEQ_D)

  {
    fix n
    assume ge: "max noa nob ≤ n"
    hence gea: "noa ≤ n" and geb: "nob ≤ n" by(auto)
    have "abs (min (a n) (b n) - min x y) < e"
    proof cases
      assume le: "min (a n) (b n) ≤ min x y"
      show ?thesis
      proof cases
        assume "a n ≤ b n"
        hence rwmin: "min (a n) (b n) = a n" by(auto)
        with le have "a n ≤ min x y" by(simp)
        moreover from gea balla have "abs (a n - x) < e" by(simp)
        moreover have "min x y ≤ x" by(auto)
        ultimately have "abs (a n - min x y) < e" by(auto)
        with rwmin show "abs (min (a n) (b n) - min x y) < e" by(simp)
      next
        assume "¬ a n ≤ b n"
        hence "b n ≤ a n" by(auto)
        hence rwmin: "min (a n) (b n) = b n" by(auto)
        with le have "b n ≤ min x y" by(simp)
        moreover from geb ballb have "abs (b n - y) < e" by(simp)
        moreover have "min x y ≤ y" by(auto)
        ultimately have "abs (b n - min x y) < e" by(auto)
        with rwmin show "abs (min (a n) (b n) - min x y) < e" by(simp)
      qed
    next
      assume "¬ min (a n) (b n) ≤ min x y"
      hence le: "min x y ≤ min (a n) (b n)" by(auto)
      show ?thesis
      proof cases
        assume "x ≤ y"
        hence rwmin: "min x y = x" by(auto)
        with le have "x ≤ min (a n) (b n)" by(simp)
        moreover from gea balla have "abs (a n - x) < e" by(simp)
        moreover have "min (a n) (b n) ≤ a n" by(auto)
        ultimately have "abs (min (a n) (b n) - x) < e" by(auto)
        with rwmin show "abs (min (a n) (b n) - min x y) < e" by(simp)
      next
        assume "¬ x ≤ y"
        hence "y ≤ x" by(auto)
        hence rwmin: "min x y = y" by(auto)
        with le have "y ≤ min (a n) (b n)" by(simp)
        moreover from geb ballb have "abs (b n - y) < e" by(simp)
        moreover have "min (a n) (b n) ≤ b n" by(auto)
        ultimately have "abs (min (a n) (b n) - y) < e" by(auto)
        with rwmin show "abs (min (a n) (b n) - min x y) < e" by(simp)
      qed
    qed
  }
  thus "∃no. ∀n≥no. ¦min (a n) (b n) - min x y¦ < e" by(blast)
qed

definition supp :: "('s ⇒ real) ⇒ 's set"
where "supp f = {x. f x ≠ 0}"

definition dist_remove :: "('s ⇒ real) ⇒ 's ⇒ 's ⇒ real"
where "dist_remove p x = (λy. if y=x then 0 else p y / (1 - p x))"

lemma supp_dist_remove:
  "p x ≠ 0 ⟹ p x ≠ 1 ⟹ supp (dist_remove p x) = supp p - {x}"
  by(auto simp:dist_remove_def supp_def)

lemma supp_empty:
  "supp f = {} ⟹ f x = 0"
  by(simp add:supp_def)

lemma nsupp_zero:
  "x ∉ supp f ⟹ f x = 0"
  by(simp add:supp_def)

lemma sum_supp:
  fixes f::"'a::finite ⇒ real"
  shows "sum f (supp f) = sum f UNIV"
proof -
  have "sum f (UNIV - supp f) = 0"
    by(simp add:supp_def)
  hence "sum f (supp f) = sum f (UNIV - supp f) + sum f (supp f)"
    by(simp)
  also have "... = sum f UNIV"
    by(simp add:sum.subset_diff[symmetric])
  finally show ?thesis .
qed

subsection ‹Truncated Subtraction›
text_raw ‹\label{s:trunc_sub}›

definition
  tminus :: "real ⇒ real ⇒ real" (infixl ‹⊖› 60)
where
  "x ⊖ y = max (x - y) 0"

lemma minus_le_tminus[intro!,simp]:
  "a - b ≤ a ⊖ b"
  unfolding tminus_def by(auto)

lemma tminus_cancel_1:
  "0 ≤ a ⟹ a + 1 ⊖ 1 = a"
  unfolding tminus_def by(simp)

lemma tminus_zero_imp_le:
  "x ⊖ y ≤ 0 ⟹ x ≤ y"
  by(simp add:tminus_def)

lemma tminus_zero[simp]:
  "0 ≤ x ⟹ x ⊖ 0 = x"
  by(simp add:tminus_def)

lemma tminus_left_mono:
  "a ≤ b ⟹ a ⊖ c ≤ b ⊖ c"
  unfolding tminus_def
  by(case_tac "a ≤ c", simp_all)

lemma tminus_less:
  "⟦ 0 ≤ a; 0 ≤ b ⟧ ⟹ a ⊖ b ≤ a"
  unfolding tminus_def by(force)

lemma tminus_left_distrib:
  assumes nna: "0 ≤ a"
  shows "a * (b ⊖ c) = a * b ⊖ a * c"
proof(cases "b ≤ c")
  case True note le = this
  hence "a * max (b - c) 0 = 0" by(simp add:max.absorb2)
  also {
    from nna le have "a * b ≤ a * c" by(blast intro:mult_left_mono)
    hence "0 = max (a * b - a * c) 0" by(simp add:max.absorb1)
  }
  finally show ?thesis by(simp add:tminus_def)
next
  case False hence le: "c ≤ b" by(auto)
  hence "a * max (b - c) 0 = a * (b - c)" by(simp only:max.absorb1)
  also {
    from nna le have "a * c ≤ a * b" by(blast intro:mult_left_mono)
    hence "a * (b - c) = max (a * b - a * c) 0" by(simp add:max.absorb1 field_simps)
  }
  finally show ?thesis by(simp add:tminus_def)
qed

lemma tminus_le[simp]:
  "b ≤ a ⟹ a ⊖ b = a - b"
  unfolding tminus_def by(simp)

lemma tminus_le_alt[simp]:
  "a ≤ b ⟹ a ⊖ b = 0"
  by(simp add:tminus_def)

lemma tminus_nle[simp]:
  "¬b ≤ a ⟹ a ⊖ b = 0"
  unfolding tminus_def by(simp)

lemma tminus_add_mono:
  "(a+b) ⊖ (c+d) ≤ (a⊖c) + (b⊖d)"
proof(cases "0 ≤ a - c")
  case True note pac = this
  show ?thesis
  proof(cases "0 ≤ b - d")
    case True note pbd = this
    from pac and pbd have "(c + d) ≤ (a + b)" by(simp)
    with pac and pbd show ?thesis by(simp)
  next
    case False with pac show ?thesis
      by(cases "c + d ≤ a + b", auto)
  qed
next
  case False note nac = this
  show ?thesis
  proof(cases "0 ≤ b - d")
    case True with nac show ?thesis
      by(cases "c + d ≤ a + b", auto)
  next
    case False note nbd = this
    with nac have "¬(c + d) ≤ (a + b)" by(simp)
    with nac and nbd show ?thesis by(simp)
  qed
qed

lemma tminus_sum_mono:
  assumes fS: "finite S"
  shows "sum f S ⊖ sum g S ≤ sum (λx. f x ⊖ g x) S"
        (is "?X S")
proof(rule finite_induct)
  from fS show "finite S" .

  show "?X {}" by(simp)

  fix x and F
  assume fF: "finite F" and xniF: "x ∉ F"
     and IH: "?X F"
  have "f x + sum f F ⊖ g x + sum g F ≤
        (f x ⊖ g x) + (sum f F ⊖ sum g F)"
    by(rule tminus_add_mono)
  also from IH have "... ≤ (f x ⊖ g x) + (∑x∈F. f x ⊖ g x)"
    by(rule add_left_mono)
  finally show "?X (insert x F)"
    by(simp add:sum.insert[OF fF xniF])
qed

lemma tminus_nneg[simp,intro]:
  "0 ≤ a ⊖ b"
  by(cases "b ≤ a", auto)

lemma tminus_right_antimono:
  assumes clb: "c ≤ b"
  shows "a ⊖ b ≤ a ⊖ c"
proof(cases "b ≤ a")
  case True
  moreover with clb have "c ≤ a" by(auto)
  moreover note clb
  ultimately show ?thesis by(simp)
next
  case False then show ?thesis by(simp)
qed

lemma min_tminus_distrib:
  "min a b ⊖ c = min (a ⊖ c) (b ⊖ c)"
  unfolding tminus_def by(auto)

end