Theory General_Utils

theory General_Utils
  imports "HOL-Analysis.Analysis"
begin

lemma lambda_skolem_gen: "(i. f'::('a ^ 'n)  'a. P i f') 
   (f'::('a ^ 'n)  ('a ^ 'n). i. P i ((λx. (f' x) $ i)))" (is "?lhs  ?rhs")
  (*using choice_iff lambda_skolem*)
proof -
  { assume H: "?rhs"
    then have ?lhs by auto }
  moreover
  { assume H: "?lhs"
    then obtain f'' where f'':"i. P i (f'' i)" unfolding choice_iff
      by metis
    let ?x = "(λx. (χ i. (f''  i) x))"
    { fix i
      from f'' have "P i (f'' i)" by metis
      then have "P i (λx.(?x x) $ i)" by auto
    }
    hence "i. P i (λx.(?x x) $ i)" by metis
    hence ?rhs by metis}
  ultimately show ?thesis by metis
qed

lemma lambda_skolem_euclidean: "(iBasis. f'::('a::{euclidean_space}real). P i f') 
   (f'::('a::euclidean_space'b::euclidean_space). iBasis. P i ((λx. (f' x)  i)))" (is "?lhs  ?rhs")
  (*using choice_iff lambda_skolem*)
proof -
  { assume H: "?rhs"
    then have ?lhs by auto }
  moreover
  { assume H: "?lhs"
    then obtain f'' where f'':"i::('b::euclidean_space)Basis. P i (f'' i)" unfolding choice_iff
      by metis
    let ?x = "(λx. (iBasis. ((f''  i) x) *R i))"
    { fix i::"'b::euclidean_space"
      assume ass: "iBasis"
      then have "P i (f'' i)"
        using f''
        by metis
      then have "P i (λx.(?x x)  i)" using ass by auto
    }
    hence *: "iBasis. P i (λx.(?x x)  i)" by auto
    then have ?rhs
      apply auto
    proof
      let ?f'6 = ?x
      show " iBasis. P i (λx. ?f'6 x  i)" using * by auto
    qed}
  ultimately show ?thesis by metis
qed

lemma lambda_skolem_euclidean_explicit: "(iBasis. f'::('a::{euclidean_space}real). P i f') 
   (f'::('a::{euclidean_space}'a). iBasis. P i ((λx. (f' x)  i)))" (is "?lhs  ?rhs")
  (*using choice_iff lambda_skolem*)
proof -
  { assume H: "?rhs"
    then have ?lhs by auto }
  moreover
  { assume H: "?lhs"
    then obtain f'' where f'':"i::('a::euclidean_space)Basis. P i (f'' i)" unfolding choice_iff
      by metis
    let ?x = "(λx. (iBasis. ((f''  i) x) *R i))"
    { fix i::"'a::euclidean_space"
      assume ass: "iBasis"
      then have "P i (f'' i)"
        using f''
        by metis
      then have "P i (λx.(?x x)  i)" using ass by auto
    }
    hence *: "iBasis. P i (λx.(?x x)  i)" by auto
    then have ?rhs
      apply auto
    proof
      let ?f'6 = ?x
      show " iBasis. P i (λx. ?f'6 x  i)" using * by auto
    qed}
  ultimately show ?thesis by metis
qed

lemma indic_ident:
  " (f::'a  real) s. (λx. (f x) * indicator s x) = (λx. if x  s then f x else 0)"
proof
  fix f::"'a  real"
  fix s::"'a set"
  fix x:: 'a
  show " f x * indicator s x = (if x  s then f x else 0)"
    by (simp add: indicator_def)
qed

lemma real_pair_basis: "Basis = {(1::real,0::real), (0::real,1::real)}"
  by (simp add: Basis_prod_def insert_commute)


(*AE_measure_singleton*)

lemma real_singleton_in_borel:
  shows "{a::real}  sets borel"
  using Borel_Space.cbox_borel[of "a" "a"]
  apply auto
  done

lemma real_singleton_in_lborel:
  shows "{a::real}  sets lborel"
  using real_singleton_in_borel
  apply auto
  done

lemma cbox_diff:
  shows "{0::real..1} - {0,1} = box 0 1"
  by (auto simp add: cbox_def)

lemma sum_bij:
  assumes "bij F"
    "xs. f x = g (F x)"
  shows "t. F ` s =  t  sum f s = sum g t"
  by (metis assms bij_betw_def bij_betw_subset subset_UNIV sum.reindex_cong)

abbreviation surj_on where
  "surj_on s f  s  range f"

lemma surj_on_image_vimage_eq: "surj_on s f  f ` (f -` s) = s"
  by fastforce

end