# 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)"
qed

lemma real_pair_basis: "Basis = {(1::real,0::real), (0::real,1::real)}"

(*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"

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
```