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: "(∀i∈Basis. ∃f'::('a::{euclidean_space}⇒real). P i f') ⟷
   (∃f'::('a::euclidean_space⇒'b::euclidean_space). ∀i∈Basis. 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. (∑i∈Basis. ((f''  i) x) *⇩R i))"
    { fix i::"'b::euclidean_space"
      assume ass: "i∈Basis"
      then have "P i (f'' i)"
        using f''
        by metis
      then have "P i (λx.(?x x) ∙ i)" using ass by auto
    }
    hence *: "∀i∈Basis. P i (λx.(?x x) ∙ i)" by auto
    then have ?rhs
      apply auto
    proof
      let ?f'6 = ?x
      show " ∀i∈Basis. P i (λx. ?f'6 x ∙ i)" using * by auto
    qed}
  ultimately show ?thesis by metis
qed

lemma lambda_skolem_euclidean_explicit: "(∀i∈Basis. ∃f'::('a::{euclidean_space}⇒real). P i f') ⟷
   (∃f'::('a::{euclidean_space}⇒'a). ∀i∈Basis. 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. (∑i∈Basis. ((f''  i) x) *⇩R i))"
    { fix i::"'a::euclidean_space"
      assume ass: "i∈Basis"
      then have "P i (f'' i)"
        using f''
        by metis
      then have "P i (λx.(?x x) ∙ i)" using ass by auto
    }
    hence *: "∀i∈Basis. P i (λx.(?x x) ∙ i)" by auto
    then have ?rhs
      apply auto
    proof
      let ?f'6 = ?x
      show " ∀i∈Basis. 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"
    "∀x∈s. 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