Theory Analysis_More
section ‹Library Additions›
theory Analysis_More
imports "HOL-Analysis.Equivalence_Lebesgue_Henstock_Integration"
"HOL-Library.Function_Algebras"
"HOL-Types_To_Sets.Linear_Algebra_On"
begin
lemma openin_open_Int'[intro]:
"open S ⟹ openin (top_of_set U) (S ∩ U)"
by (auto simp: openin_open)
subsection ‹Parametricity rules for topology›
text ‹TODO: also check with theory ‹Transfer_Euclidean_Space_Vector› in AFP/ODE...›
context includes lifting_syntax begin
lemma Sigma_transfer[transfer_rule]:
"(rel_set A ===> (A ===> rel_set B) ===> rel_set (rel_prod A B)) Sigma Sigma"
unfolding Sigma_def
by transfer_prover
lemma filterlim_transfer[transfer_rule]:
"((A ===> B) ===> rel_filter B ===> rel_filter A ===> (=)) filterlim filterlim"
if [transfer_rule]: "bi_unique B"
unfolding filterlim_iff
by transfer_prover
lemma nhds_transfer[transfer_rule]:
"(A ===> rel_filter A) nhds nhds"
if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
unfolding nhds_def
by transfer_prover
lemma at_within_transfer[transfer_rule]:
"(A ===> rel_set A ===> rel_filter A) at_within at_within"
if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
unfolding at_within_def
by transfer_prover
lemma continuous_on_transfer[transfer_rule]:
"(rel_set A ===> (A ===> B) ===> (=)) continuous_on continuous_on"
if [transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
"bi_unique B" "bi_total B" "(rel_set B ===> (=)) open open"
unfolding continuous_on_def
by transfer_prover
lemma continuous_on_transfer_right_total[transfer_rule]:
"(rel_set A ===> (A ===> B) ===> (=)) (λX::'a::t2_space set. continuous_on (X ∩ Collect AP)) (λY::'b::t2_space set. continuous_on Y)"
if DomainA: "Domainp A = AP"
and [folded DomainA, transfer_rule]: "bi_unique A" "right_total A" "(rel_set A ===> (=)) (openin (top_of_set (Collect AP))) open"
"bi_unique B" "bi_total B" "(rel_set B ===> (=)) open open"
unfolding DomainA[symmetric]
proof (intro rel_funI)
fix X Y f g
assume H[transfer_rule]: "rel_set A X Y" "(A ===> B) f g"
from H(1) have XA: "x ∈ X ⟹ Domainp A x" for x
by (auto simp: rel_set_def)
then have *: "X ∩ Collect (Domainp A) = X" by auto
have "openin (top_of_set (Collect (Domainp A))) (Collect (Domainp A))" by auto
show " continuous_on (X ∩ Collect (Domainp A)) f = continuous_on Y g"
unfolding continuous_on_eq_continuous_within continuous_within_topological *
apply transfer
apply safe
subgoal for x B
apply (drule bspec, assumption, drule spec, drule mp, assumption, drule mp, assumption)
apply clarsimp
subgoal for AA
apply (rule exI[where x="AA ∩ Collect (Domainp A)"])
by (auto intro: XA)
done
subgoal using XA by (force simp: openin_subtopology)
done
qed
lemma continuous_on_transfer_right_total2[transfer_rule]:
"(rel_set A ===> (A ===> B) ===> (=)) (λX::'a::t2_space set. continuous_on X) (λY::'b::t2_space set. continuous_on Y)"
if DomainB: "Domainp B = BP"
and [folded DomainB, transfer_rule]: "bi_unique A" "bi_total A" "(rel_set A ===> (=)) open open"
"bi_unique B" "right_total B" "(rel_set B ===> (=)) ((openin (top_of_set (Collect BP)))) open"
unfolding DomainB[symmetric]
proof (intro rel_funI)
fix X Y f g
assume H[transfer_rule]: "rel_set A X Y" "(A ===> B) f g"
show "continuous_on X f = continuous_on Y g"
unfolding continuous_on_eq_continuous_within continuous_within_topological
apply transfer
apply safe
subgoal for x C
apply (clarsimp simp: openin_subtopology)
apply (drule bspec, assumption, drule spec, drule mp, assumption, drule mp, assumption)
apply clarsimp
by (meson Domainp_applyI H(1) H(2) rel_setD1)
subgoal for x C
proof -
let ?sub = "top_of_set (Collect (Domainp B))"
assume cont: "∀x∈X. ∀Ba∈{A. Ball A (Domainp B)}.
openin (top_of_set (Collect (Domainp B))) Ba ⟶ f x ∈ Ba ⟶ (∃Aa. open Aa ∧ x ∈ Aa ∧ (∀y∈X. y ∈ Aa ⟶ f y ∈ Ba))"
and x: "x ∈ X" "open C" "f x ∈ C"
let ?B = "C ∩ Collect (Domainp B)"
have "?B ∈ {A. Ball A (Domainp B)}" by auto
have "openin ?sub (Collect (Domainp B))" by auto
then have "openin ?sub ?B" using ‹open C› by auto
moreover have "f x ∈ ?B" using x
apply transfer apply auto
by (meson Domainp_applyI H(1) H(2) rel_setD1)
ultimately obtain D where "open D ∧ x ∈ D ∧ (∀y∈X. y ∈ D ⟶ f y ∈ ?B)"
using cont x
by blast
then show "∃A. open A ∧ x ∈ A ∧ (∀y∈X. y ∈ A ⟶ f y ∈ C)" by auto
qed
done
qed
lemma generate_topology_transfer[transfer_rule]:
includes lifting_syntax
assumes [transfer_rule]: "right_total A" "bi_unique A"
shows "(rel_set (rel_set A) ===> rel_set A ===> (=)) (generate_topology o (insert (Collect (Domainp A)))) generate_topology"
proof (intro rel_funI)
fix B C X Y assume t[transfer_rule]: "rel_set (rel_set A) B C" "rel_set A X Y"
then have "X ⊆ Collect (Domainp A)" by (auto simp: rel_set_def)
with t have rI: "rel_set A (X ∩ Collect (Domainp A)) Y"
by (auto simp: inf_absorb1)
have eq_UNIV_I: "Z = UNIV" if [transfer_rule]: "rel_set A {a. Domainp A a} Z" for Z
using that assms
apply (auto simp: right_total_def rel_set_def)
using bi_uniqueDr by fastforce
show "(generate_topology ∘ insert (Collect (Domainp A))) B X = generate_topology C Y"
unfolding o_def
proof (rule iffI)
fix x
assume "generate_topology (insert (Collect (Domainp A)) B) X"
then show "generate_topology C Y" unfolding o_def
using rI
proof (induction X arbitrary: Y)
case [transfer_rule]: UNIV
with eq_UNIV_I[of Y] show ?case
by (simp add: generate_topology.UNIV)
next
case (Int a b)
note [transfer_rule] = Int(5)
obtain a' where a'[transfer_rule]: "rel_set A (a ∩ Collect (Domainp A)) a'"
by (metis Domainp_iff Domainp_set Int_Collect)
obtain b' where b'[transfer_rule]: "rel_set A (b ∩ Collect (Domainp A)) b'"
by (metis Domainp_iff Domainp_set Int_Collect)
from Int.IH(1)[OF a'] Int.IH(2)[OF b']
have "generate_topology C a'" "generate_topology C b'" by auto
from generate_topology.Int[OF this] have "generate_topology C (a' ∩ b')" .
also have "a' ∩ b' = Y"
by transfer auto
finally show ?case
by (simp add: generate_topology.Int)
next
case (UN K)
note [transfer_rule] = UN(3)
have "∃K'. ∀k. rel_set A (k ∩ Collect (Domainp A)) (K' k)"
by (rule choice) (metis Domainp_iff Domainp_set Int_Collect)
then obtain K' where K': "⋀k. rel_set A (k ∩ Collect (Domainp A)) (K' k)" by metis
from UN.IH[OF _ this] have "generate_topology C k'" if "k' ∈ K'`K" for k' using that by auto
from generate_topology.UN[OF this] have "generate_topology C (⋃(K' ` K))" .
also
from K' have [transfer_rule]: "(rel_set (=) ===> rel_set A) (λx. x ∩ Collect (Domainp A)) K'"
by (fastforce simp: rel_fun_def rel_set_def)
have "⋃(K' ` K) = Y"
by transfer auto
finally show ?case
by (simp add: generate_topology.UN)
next
case (Basis s)
from this(1) show ?case
proof
assume "s = Collect (Domainp A)"
with eq_UNIV_I[of Y] Basis(2)
show ?case
by (simp add: generate_topology.UNIV)
next
assume "s ∈ B"
with Basis(2) obtain t where [transfer_rule]: "rel_set A (s ∩ Collect (Domainp A)) t" by auto
from Basis(1) t(1) have s: "s ∩ Collect (Domainp A) = s"
by (force simp: rel_set_def)
have "t ∈ C" using ‹s ∈ B› s
by transfer auto
also note [transfer_rule] = Basis(2)
have "t = Y"
by transfer auto
finally show ?case
by (rule generate_topology.Basis)
qed
qed
next
assume "generate_topology C Y"
then show "generate_topology (insert (Collect (Domainp A)) B) X"
using ‹rel_set A X Y›
proof (induction arbitrary: X)
case [transfer_rule]: UNIV
have "UNIV = (UNIV::'b set)" by auto
then have "X = {a. Domainp A a}" by transfer
then show ?case by (intro generate_topology.Basis) auto
next
case (Int a b)
obtain a' b' where [transfer_rule]: "rel_set A a' a" "rel_set A b' b"
by (meson assms(1) right_total_def right_total_rel_set)
from generate_topology.Int[OF Int.IH(1)[OF this(1)] Int.IH(2)[OF this(2)]]
have "generate_topology (insert {a. Domainp A a} B) (a' ∩ b')" by simp
also
define I where "I = a ∩ b"
from ‹rel_set A X (a ∩ b)› have [transfer_rule]: "rel_set A X I" by (simp add: I_def)
from I_def
have "a' ∩ b' = X" by transfer simp
finally show ?case .
next
case (UN K)
have "∃K'. ∀k. rel_set A (K' k) k"
by (rule choice) (meson assms(1) right_total_def right_total_rel_set)
then obtain K' where K': "⋀k. rel_set A (K' k) k" by metis
from UN.IH[OF _ this] have "generate_topology (insert {a. Domainp A a} B) k"
if "k ∈ K'`K" for k using that by auto
from generate_topology.UN[OF this]
have "generate_topology (insert {a. Domainp A a} B) (⋃(K'`K))" by auto
also
from K' have [transfer_rule]: "(rel_set (=) ===> rel_set A) K' id"
by (fastforce simp: rel_fun_def rel_set_def)
define U where "U = (⋃(id ` K))"
from ‹rel_set A X _› have [transfer_rule]: "rel_set A X U" by (simp add: U_def)
from U_def have "⋃(K' ` K) = X" by transfer simp
finally show ?case .
next
case (Basis s)
note [transfer_rule] = ‹rel_set A X s›
from ‹s ∈ C› have "X ∈ B" by transfer
then show ?case by (intro generate_topology.Basis) auto
qed
qed
qed
end
subsection ‹Miscellaneous›
lemmas [simp del] = mem_ball
lemma in_closureI[intro, simp]: "x ∈ X ⟹ x ∈ closure X"
using closure_subset by auto
lemmas open_continuous_vimage = continuous_on_open_vimage[THEN iffD1, rule_format]
lemma open_continuous_vimage': "open s ⟹ continuous_on s f ⟹ open B ⟹ open (s ∩ f -` B)"
using open_continuous_vimage[of s f B] by (auto simp: Int_commute)
lemma support_on_mono: "support_on carrier f ⊆ support_on carrier g"
if "⋀x. x ∈ carrier ⟹ f x ≠ 0 ⟹ g x ≠ 0"
using that
by (auto simp: support_on_def)
lemma image_prod: "(λ(x, y). (f x, g y)) ` (A × B) = f ` A × g ` B" by auto
subsection ‹Closed support›
definition "csupport_on X S = closure (support_on X S)"
lemma closed_csupport_on[intro, simp]: "closed (csupport_on carrier φ)"
by (auto simp: csupport_on_def)
lemma not_in_csupportD: "x ∉ csupport_on carrier φ ⟹ x ∈ carrier ⟹ φ x = 0"
by (auto simp: csupport_on_def support_on_def)
lemma csupport_on_mono: "csupport_on carrier f ⊆ csupport_on carrier g"
if "⋀x. x ∈ carrier ⟹ f x ≠ 0 ⟹ g x ≠ 0"
unfolding csupport_on_def
apply (rule closure_mono)
using that
by (rule support_on_mono)
subsection ‹Homeomorphism›
lemma homeomorphism_empty[simp]:
"homeomorphism {} t f f' ⟷ t = {}"
"homeomorphism s {} f f' ⟷ s = {}"
by (auto simp: homeomorphism_def)
lemma homeomorphism_add:
"homeomorphism UNIV UNIV (λx. x + c) (λx. x - c)"
for c::"_::real_normed_vector"
unfolding homeomorphism_def
by (auto simp: algebra_simps continuous_intros intro!: image_eqI[where x="x - c" for x])
lemma in_range_scaleR_iff: "x ∈ range ((*⇩R) c) ⟷ c = 0 ⟶ x = 0"
for x::"_::real_vector"
by (auto simp: intro!: image_eqI[where x="x /⇩R c"])
lemma homeomorphism_scaleR:
"homeomorphism UNIV UNIV (λx. c *⇩R x::_::real_normed_vector) (λx. x /⇩R c)"
if "c ≠ 0"
using that
unfolding homeomorphism_def
by (auto simp: in_range_scaleR_iff algebra_simps intro!: continuous_intros)
lemma homeomorphism_prod:
"homeomorphism (a × b) (c × d) (λ(x, y). (f x, g y)) (λ(x, y). (f' x, g' y))"
if "homeomorphism a c f f'"
"homeomorphism b d g g'"
using that by (simp add: homeomorphism_def image_prod)
(auto simp add: split_beta intro!: continuous_intros elim: continuous_on_compose2)
subsection ‹Generalizations›
lemma openin_subtopology_eq_generate_topology:
"openin (top_of_set S) x = generate_topology (insert S ((λB. B ∩ S) ` BB)) x"
if open_gen: "open = generate_topology BB" and subset: "x ⊆ S"
proof -
have "generate_topology (insert S ((λB. B ∩ S) ` BB)) (T ∩ S)"
if "generate_topology BB T"
for T
using that
proof (induction)
case UNIV
then show ?case by (auto intro!: generate_topology.Basis)
next
case (Int a b)
have "generate_topology (insert S ((λB. B ∩ S) ` BB)) (a ∩ S ∩ (b ∩ S))"
by (rule generate_topology.Int) (use Int in auto)
then show ?case by (simp add: ac_simps)
next
case (UN K)
then have "generate_topology (insert S ((λB. B ∩ S) ` BB)) (⋃k∈K. k ∩ S)"
by (intro generate_topology.UN) auto
then show ?case by simp
next
case (Basis s)
then show ?case
by (intro generate_topology.Basis) auto
qed
moreover
have "∃T. generate_topology BB T ∧ x = T ∩ S"
if "generate_topology (insert S ((λB. B ∩ S) ` BB)) x" "x ≠ UNIV"
using that
proof (induction)
case UNIV
then show ?case by simp
next
case (Int a b)
then show ?case
using generate_topology.Int
by auto
next
case (UN K)
from UN.IH have "∀k∈K-{UNIV}. ∃T. generate_topology BB T ∧ k = T ∩ S" by auto
from this[THEN bchoice] obtain T where T: "⋀k. k ∈ T ` (K - {UNIV}) ⟹ generate_topology BB k" "⋀k. k ∈ K - {UNIV} ⟹ k = (T k) ∩ S"
by auto
from generate_topology.UN[OF T(1)]
have "generate_topology BB (⋃(T ` (K - {UNIV})))" by auto
moreover have "⋃K = (⋃(T ` (K - {UNIV}))) ∩ S" if "UNIV ∉ K" using T(2) UN that by auto
ultimately show ?case
apply (cases "UNIV ∈ K") subgoal using UN by auto
subgoal by auto
done
next
case (Basis s)
then show ?case
using generate_topology.UNIV generate_topology.Basis by blast
qed
moreover
have "∃T. generate_topology BB T ∧ UNIV = T ∩ S" if "generate_topology (insert S ((λB. B ∩ S) ` BB)) x"
"x = UNIV"
proof -
have "S = UNIV"
using that ‹x ⊆ S›
by auto
then show ?thesis by (simp add: generate_topology.UNIV)
qed
ultimately show ?thesis
by (metis open_gen open_openin openin_open_Int' openin_subtopology)
qed
subsection ‹Equal topologies›
lemma topology_eq_iff: "t = s ⟷ (topspace t = topspace s ∧
(∀x⊆topspace t. openin t x = openin s x))"
by (metis (full_types) openin_subset topology_eq)
subsection ‹Finer topologies›
definition finer_than (infix "(finer'_than)" 50)
where "T1 finer_than T2 ⟷ continuous_map T1 T2 (λx. x)"
lemma finer_than_iff_nhds:
"T1 finer_than T2 ⟷ (∀X. openin T2 X ⟶ openin T1 (X ∩ topspace T1)) ∧ (topspace T1 ⊆ topspace T2)"
by (auto simp: finer_than_def continuous_map_alt)
lemma continuous_on_finer_topo:
"continuous_map s t f"
if "continuous_map s' t f" "s finer_than s'"
using that
by (auto simp: finer_than_def o_def dest: continuous_map_compose)
lemma continuous_on_finer_topo2:
"continuous_map s t f"
if "continuous_map s t' f" "t' finer_than t"
using that
by (auto simp: finer_than_def o_def dest: continuous_map_compose)
lemma antisym_finer_than: "S = T" if "S finer_than T" "T finer_than S"
using that
by (metis finer_than_iff_nhds openin_subtopology subset_antisym subtopology_topspace topology_eq_iff)
lemma subtopology_finer_than[simp]: "top_of_set X finer_than euclidean"
by (auto simp: finer_than_iff_nhds openin_subtopology)
subsection ‹Support›
lemma support_on_nonneg_sum:
"support_on X (λx. ∑i∈S. f i x) = (⋃i∈S. support_on X (f i))"
if "finite S" "⋀x i . x ∈ X ⟹ i ∈ S ⟹ f i x ≥ 0"
for f::"_⇒_⇒_::ordered_comm_monoid_add"
using that by (auto simp: support_on_def sum_nonneg_eq_0_iff)
lemma support_on_nonneg_sum_subset:
"support_on X (λx. ∑i∈S. f i x) ⊆ (⋃i∈S. support_on X (f i))"
for f::"_⇒_⇒_::ordered_comm_monoid_add"
by (cases "finite S") (auto simp: support_on_def, meson sum.neutral)
lemma support_on_nonneg_sum_subset':
"support_on X (λx. ∑i∈S x. f i x) ⊆ (⋃x∈X. (⋃i∈S x. support_on X (f i)))"
for f::"_⇒_⇒_::ordered_comm_monoid_add"
by (auto simp: support_on_def, meson sum.neutral)
subsection ‹Final topology (Bourbaki, General Topology I, 4.)›
definition "final_topology X Y f =
topology (λU. U ⊆ X ∧
(∀i. openin (Y i) (f i -` U ∩ topspace (Y i))))"
lemma openin_final_topology:
"openin (final_topology X Y f) =
(λU. U ⊆ X ∧ (∀i. openin (Y i) (f i -` U ∩ topspace (Y i))))"
unfolding final_topology_def
apply (rule topology_inverse')
unfolding istopology_def
proof safe
fix S T i
assume "∀i. openin (Y i) (f i -` S ∩ topspace (Y i))"
"∀i. openin (Y i) (f i -` T ∩ topspace (Y i))"
then have "openin (Y i) (f i -` S ∩ topspace (Y i) ∩ (f i -` T ∩ topspace (Y i)))"
(is "openin _ ?I")
by auto
also have "?I = f i -` (S ∩ T) ∩ topspace (Y i)"
(is "_ = ?R")
by auto
finally show "openin (Y i) ?R" .
next
fix K i
assume "∀U∈K. U ⊆ X ∧ (∀i. openin (Y i) (f i -` U ∩ topspace (Y i)))"
then have "openin (Y i) (⋃X∈K. f i -` X ∩ topspace (Y i))"
by (intro openin_Union) auto
then show "openin (Y i) (f i -` ⋃K ∩ topspace (Y i))"
by (auto simp: vimage_Union)
qed force+
lemma topspace_final_topology:
"topspace (final_topology X Y f) = X"
if "⋀i. f i ∈ topspace (Y i) → X"
proof -
have *: "f i -` X ∩ topspace (Y i) = topspace (Y i)" for i
using that
by auto
show ?thesis
unfolding topspace_def
unfolding openin_final_topology
apply (rule antisym)
apply force
apply (rule subsetI)
apply (rule UnionI[where X=X])
using that
by (auto simp: *)
qed
lemma continuous_on_final_topologyI2:
"continuous_map (Y i) (final_topology X Y f) (f i)"
if "⋀i. f i ∈ topspace (Y i) → X"
using that
by (auto simp: openin_final_topology continuous_map_alt topspace_final_topology)
lemma continuous_on_final_topologyI1:
"continuous_map (final_topology X Y f) Z g"
if hyp: "⋀i. continuous_map (Y i) Z (g o f i)"
and that: "⋀i. f i ∈ topspace (Y i) → X" "g ∈ X → topspace Z"
unfolding continuous_map_alt
proof safe
fix V assume V: "openin Z V"
have oV: "openin (Y i) (f i -` g -` V ∩ topspace (Y i))"
for i
using hyp[rule_format, of i] V
by (auto simp: continuous_map_alt vimage_comp dest!: spec[where x=V])
have *: "f i -` g -` V ∩ f i -` X ∩ topspace (Y i) =
f i -` g -` V ∩ topspace (Y i)"
(is "_ = ?rhs i")
for i using that
by auto
show "openin (final_topology X Y f) (g -` V ∩ topspace (final_topology X Y f))"
by (auto simp: openin_final_topology oV topspace_final_topology that *)
qed (use that in ‹auto simp: topspace_final_topology›)
lemma continuous_on_final_topology_iff:
"continuous_map (final_topology X Y f) Z g ⟷ (∀i. continuous_map (Y i) Z (g o f i))"
if "⋀i. f i ∈ topspace (Y i) → X" "g ∈ X → topspace Z"
using that
by (auto intro!: continuous_on_final_topologyI1[OF _ that]
intro: continuous_map_compose[OF continuous_on_final_topologyI2[OF that(1)]])
subsection ‹Quotient topology›
definition map_topology :: "('a ⇒ 'b) ⇒ 'a topology ⇒ 'b topology" where
"map_topology p X = final_topology (p ` topspace X) (λ_. X) (λ(_::unit). p)"
lemma openin_map_topology:
"openin (map_topology p X) = (λU. U ⊆ p ` topspace X ∧ openin X (p -` U ∩ topspace X))"
by (auto simp: map_topology_def openin_final_topology)
lemma topspace_map_topology[simp]: "topspace (map_topology f T) = f ` topspace T"
unfolding map_topology_def
by (subst topspace_final_topology) auto
lemma continuous_on_map_topology:
"continuous_map T (map_topology f T) f"
unfolding continuous_map_alt openin_map_topology
by auto
lemma continuous_map_composeD:
"continuous_map T X (g ∘ f) ⟹ g ∈ f ` topspace T → topspace X"
by (auto simp: continuous_map_def)
lemma continuous_on_map_topology2:
"continuous_map T X (g ∘ f) ⟷ continuous_map (map_topology f T) X g"
unfolding map_topology_def
apply safe
subgoal
apply (rule continuous_on_final_topologyI1)
subgoal by assumption
subgoal by force
subgoal by (rule continuous_map_composeD)
done
subgoal
apply (erule continuous_map_compose[rotated])
apply (rule continuous_on_final_topologyI2)
by force
done
lemma map_sub_finer_than_commute:
"map_topology f (subtopology T (f -` X)) finer_than subtopology (map_topology f T) X"
by (auto simp: finer_than_def continuous_map_def openin_subtopology openin_map_topology
topspace_subtopology)
lemma sub_map_finer_than_commute:
"subtopology (map_topology f T) X finer_than map_topology f (subtopology T (f -` X))"
if "openin T (f -` X)"
unfolding finer_than_def continuous_map_alt
proof (rule conjI, clarsimp)
fix U
assume "openin (map_topology f (subtopology T (f -` X))) U"
then obtain W where W: "U ⊆ f ` (topspace T ∩ f -` X)" "openin T W" "f -` U ∩ (topspace T ∩ f -` X) = W ∩ f -` X"
by (auto simp: topspace_subtopology openin_subtopology openin_map_topology)
have "(f -` f ` W ∩ f -` X) ∩ topspace T = W ∩ topspace T ∩ f -` X"
apply auto
by (metis Int_iff W(3) vimage_eq)
also have "openin T …"
by (auto intro!: W that)
finally show "openin (subtopology (map_topology f T) X) (U ∩ (f ` topspace T ∩ X))"
using W
unfolding topspace_subtopology topspace_map_topology openin_subtopology openin_map_topology
by (intro exI[where x="(f ` W ∩ X)"]) auto
qed auto
lemma subtopology_map_topology:
"subtopology (map_topology f T) X = map_topology f (subtopology T (f -` X))"
if "openin T (f -` X)"
apply (rule antisym_finer_than)
using sub_map_finer_than_commute[OF that] map_sub_finer_than_commute[of f T X]
by auto
lemma quotient_map_map_topology:
"quotient_map X (map_topology f X) f"
by (auto simp: quotient_map_def openin_map_topology ac_simps)
(simp_all add: vimage_def Int_def)
lemma topological_space_quotient: "class.topological_space (openin (map_topology f euclidean))"
if "surj f"
apply standard
apply auto
using that
by (auto simp: openin_map_topology)
lemma t2_space_quotient: "class.t2_space (open::'b set ⇒ bool)"
if open_def: "open = (openin (map_topology (p::'a::t2_space⇒'b::topological_space) euclidean))"
"surj p" and open_p: "⋀X. open X ⟹ open (p ` X)" and "closed {(x, y). p x = p y}" (is "closed ?R")
apply (rule class.t2_space.intro)
subgoal by (unfold open_def, rule topological_space_quotient; fact)
proof standard
fix a b::'b
obtain x y where a_def: "a = p x" and b_def: "b = p y" using ‹surj p› by fastforce
assume "a ≠ b"
with ‹closed ?R› have "open (-?R)" "(x, y) ∈ -?R" by (auto simp add: a_def b_def)
from open_prod_elim[OF this]
obtain N⇩x N⇩y where "open N⇩x" "open N⇩y" "(x, y) ∈ N⇩x × N⇩y" "N⇩x × N⇩y ⊆ -?R" .
then have "p ` N⇩x ∩ p ` N⇩y = {}" by auto
moreover
from ‹open N⇩x› ‹open N⇩y› have "open (p ` N⇩x)" "open (p ` N⇩y)"
using open_p by blast+
moreover have "a ∈ p ` N⇩x" "b ∈ p ` N⇩y" using ‹(x, y) ∈ _ × _› by (auto simp: a_def b_def)
ultimately show "∃U V. open U ∧ open V ∧ a ∈ U ∧ b ∈ V ∧ U ∩ V = {}" by blast
qed
lemma second_countable_topology_quotient: "class.second_countable_topology (open::'b set ⇒ bool)"
if open_def: "open = (openin (map_topology (p::'a::second_countable_topology⇒'b::topological_space) euclidean))"
"surj p" and open_p: "⋀X. open X ⟹ open (p ` X)"
apply (rule class.second_countable_topology.intro)
subgoal by (unfold open_def, rule topological_space_quotient; fact)
proof standard
have euclidean_def: "euclidean = map_topology p euclidean"
by (simp add: openin_inverse open_def)
have continuous_on: "continuous_on UNIV p"
using continuous_map_iff_continuous2 continuous_on_map_topology euclidean_def by fastforce
from ex_countable_basis[where 'a='a] obtain A::"'a set set" where "countable A" "topological_basis A"
by auto
define B where "B = (λX. p ` X) ` A"
have "countable (B::'b set set)"
by (auto simp: B_def intro!: ‹countable A›)
moreover have "topological_basis B"
proof (rule topological_basisI)
fix B' assume "B' ∈ B" then show "open B'" using ‹topological_basis A›
by (auto simp: B_def topological_basis_open intro!: open_p)
next
fix x::'b and O' assume "open O'" "x ∈ O'"
have "open (p -` O')"
using ‹open O'›
by (rule open_vimage) (auto simp: continuous_on)
obtain y where y: "y ∈ p -` {x}"
using ‹x ∈ O'›
by auto (metis UNIV_I open_def(2) rangeE)
then have "y ∈ p -` O'" using ‹x ∈ O'› by auto
from topological_basisE[OF ‹topological_basis A› ‹open (p -` O')› this]
obtain C where "C ∈ A" "y ∈ C" "C ⊆ p -` O'" .
let ?B' = "p ` C"
have "?B' ∈ B"
using ‹C ∈ A› by (auto simp: B_def)
moreover
have "x ∈ ?B'" using y ‹y ∈ C› ‹x ∈ O'›
by auto
moreover
have "?B' ⊆ O'"
using ‹C ⊆ _› by auto
ultimately show "∃B'∈B. x ∈ B' ∧ B' ⊆ O'" by metis
qed
ultimately show "∃B::'b set set. countable B ∧ open = generate_topology B"
by (auto simp: topological_basis_imp_subbasis)
qed
subsection ‹Closure›
lemma closure_Union: "closure (⋃X) = (⋃x∈X. closure x)" if "finite X"
using that
by (induction X) auto
subsection ‹Compactness›
lemma compact_if_closed_subset_of_compact:
"compact S" if "closed S" "compact T" "S ⊆ T"
proof (rule compactI)
fix UU assume UU: "∀t∈UU. open t" "S ⊆ ⋃UU"
have "T ⊆ ⋃(insert (- S) (UU))" "⋀B. B ∈ insert (- S) UU ⟹ open B"
using UU ‹S ⊆ T›
by (auto simp: open_Compl ‹closed S›)
from compactE[OF ‹compact T› this]
obtain 𝒯' where 𝒯: "𝒯' ⊆ insert (- S) UU" "finite 𝒯'" "T ⊆ ⋃𝒯'"
by metis
show "∃C'⊆UU. finite C' ∧ S ⊆ ⋃C'"
apply (rule exI[where x="𝒯' - {-S}"])
using 𝒯 UU
apply auto
proof -
fix x assume "x ∈ S"
with 𝒯 ‹S ⊆ T› obtain U where "x ∈ U" "U ∈ 𝒯'" using 𝒯
by auto
then show "∃X∈𝒯' - {- S}. x ∈ X"
using 𝒯 UU ‹x ∈ S›
apply -
apply (rule bexI[where x=U])
by auto
qed
qed
subsection ‹Locally finite›
definition "locally_finite_on X I U ⟷ (∀p∈X. ∃N. p∈N ∧ open N ∧ finite {i∈I. U i ∩ N ≠ {}})"
lemmas locally_finite_onI = locally_finite_on_def[THEN iffD2, rule_format]
lemma locally_finite_onE:
assumes "locally_finite_on X I U"
assumes "p ∈ X"
obtains N where "p ∈ N" "open N" "finite {i∈I. U i ∩ N ≠ {}}"
using assms
by (auto simp: locally_finite_on_def)
lemma locally_finite_onD:
assumes "locally_finite_on X I U"
assumes "p ∈ X"
shows "finite {i∈I. p ∈ U i}"
apply (rule locally_finite_onE[OF assms])
apply (rule finite_subset)
by auto
lemma locally_finite_on_open_coverI: "locally_finite_on X I U"
if fin: "⋀j. j ∈ I ⟹ finite {i∈I. U i ∩ U j ≠ {}}"
and open_cover: "X ⊆ (⋃i∈I. U i)" "⋀i. i ∈ I ⟹ open (U i)"
proof (rule locally_finite_onI)
fix p assume "p ∈ X"
then obtain i where i: "i ∈ I" "p ∈ U i" "open (U i)"
using open_cover
by blast
show "∃N. p ∈ N ∧ open N ∧ finite {i ∈ I. U i ∩ N ≠ {}}"
by (intro exI[where x="U i"] conjI i fin)
qed
lemma locally_finite_compactD:
"finite {i∈I. U i ∩ V ≠ {}}"
if lf: "locally_finite_on X I U"
and compact: "compact V"
and subset: "V ⊆ X"
proof -
have "∃N. ∀p ∈ X. p ∈ N p ∧ open (N p) ∧ finite {i∈I. U i ∩ N p ≠ {}}"
by (rule bchoice) (auto elim!: locally_finite_onE[OF lf, rule_format])
then obtain N where N: "⋀p. p ∈ X ⟹ p ∈ N p"
"⋀p. p ∈ X ⟹ open (N p)"
"⋀p. p ∈ X ⟹ finite {i∈I. U i ∩ N p ≠ {}}"
by blast
have "V ⊆ (⋃p∈X. N p)" "⋀B. B ∈ N ` X ⟹ open B"
using N subset by force+
from compactE[OF compact this]
obtain C where C: "C ⊆ X" "finite C" "V ⊆ ⋃(N ` C)"
by (metis finite_subset_image)
then have "{i∈I. U i ∩ V ≠ {}} ⊆ {i∈I. U i ∩ ⋃(N ` C) ≠ {}}"
by force
also have "… ⊆ (⋃c∈C. {i∈I. U i ∩ N c ≠ {}})"
by force
also have "finite …"
apply (rule finite_Union)
using C by (auto intro!: C N)
finally (finite_subset) show ?thesis .
qed
lemma closure_Int_open_eq_empty: "open S ⟹ (closure T ∩ S) = {} ⟷ T ∩ S = {}"
by (auto simp: open_Int_closure_eq_empty ac_simps)
lemma locally_finite_on_subset:
assumes "locally_finite_on X J U"
assumes "⋀i. i ∈ I ⟹ V i ⊆ U i" "I ⊆ J"
shows "locally_finite_on X I V"
proof (rule locally_finite_onI)
fix p assume "p ∈ X"
from locally_finite_onE[OF assms(1) this]
obtain N where "p ∈ N" "open N" "finite {i ∈ J. U i ∩ N ≠ {}}" .
then show "∃N. p ∈ N ∧ open N ∧ finite {i ∈ I. V i ∩ N ≠ {}}"
apply (intro exI[where x=N])
using assms
by (auto elim!: finite_subset[rotated])
qed
lemma locally_finite_on_closure:
"locally_finite_on X I (λx. closure (U x))"
if "locally_finite_on X I U"
proof (rule locally_finite_onI)
fix p assume "p ∈ X"
from locally_finite_onE[OF that this] obtain N
where "p ∈ N" "open N" "finite {i ∈ I. U i ∩ N ≠ {}}" .
then show "∃N. p ∈ N ∧ open N ∧ finite {i ∈ I. closure (U i) ∩ N ≠ {}}"
by (auto intro!: exI[where x=N] simp: closure_Int_open_eq_empty)
qed
lemma locally_finite_on_closedin_Union_closure:
"closedin (top_of_set X) (⋃i∈I. closure (U i))"
if "locally_finite_on X I U" "⋀i. i ∈ I ⟹ closure (U i) ⊆ X"
unfolding closedin_def
apply safe
subgoal using that(2) by auto
subgoal
apply (subst openin_subopen)
proof clarsimp
fix x
assume x: "x ∈ X" "∀i∈I. x ∉ closure (U i)"
from locally_finite_onE[OF that(1) ‹x ∈ X›]
obtain N where N: "x ∈ N" "open N" "finite {i ∈ I. U i ∩ N ≠ {}}" (is "finite ?I").
define N' where "N' = N - (⋃i ∈ ?I. closure (U i))"
have "open N'"
by (auto simp: N'_def intro!: N)
then have "openin (top_of_set X) (X ∩ N')"
by (rule openin_open_Int)
moreover
have "x ∈ X ∩ N'" using x
by (auto simp: N'_def N)
moreover
have "X ∩ N' ⊆ X - (⋃i∈I. closure (U i))"
using x that(2)
apply (auto simp: N'_def)
by (meson N(2) closure_iff_nhds_not_empty dual_order.refl)
ultimately show "∃T. openin (top_of_set X) T ∧ x ∈ T ∧ T ⊆ X - (⋃i∈I. closure (U i))"
by auto
qed
done
lemma closure_subtopology_minimal:
"S ⊆ T ⟹ closedin (top_of_set X) T ⟹ closure S ∩ X ⊆ T"
apply (auto simp: closedin_closed)
using closure_minimal by blast
lemma locally_finite_on_closure_Union:
"(⋃i∈I. closure (U i)) = closure (⋃i∈I. (U i)) ∩ X"
if "locally_finite_on X I U" "⋀i. i ∈ I ⟹ closure (U i) ⊆ X"
proof (rule antisym)
show "(⋃i∈I. closure (U i)) ⊆ closure (⋃i∈I. U i) ∩ X"
using that
apply auto
by (metis (no_types, lifting) SUP_le_iff closed_closure closure_minimal closure_subset subsetCE)
show "closure (⋃i∈I. U i) ∩ X ⊆ (⋃i∈I. closure (U i))"
apply (rule closure_subtopology_minimal)
apply auto
using that
by (auto intro!: locally_finite_on_closedin_Union_closure)
qed
subsection ‹Refinement of cover›
definition refines :: "'a set set ⇒ 'a set set ⇒ bool" (infix "refines" 50)
where "A refines B ⟷ (∀s∈A. (∃t. t ∈ B ∧ s ⊆ t))"
lemma refines_subset: "x refines y" if "z refines y" "x ⊆ z"
using that by (auto simp: refines_def)
subsection ‹Functions as vector space›
instantiation "fun" :: (type, scaleR) scaleR begin
definition scaleR_fun :: "real ⇒ ('a ⇒ 'b) ⇒ 'a ⇒ 'b" where
"scaleR_fun r f = (λx. r *⇩R f x)"
lemma scaleR_fun_beta[simp]: "(r *⇩R f) x = r *⇩R f x"
by (simp add: scaleR_fun_def)
instance ..
end
instance "fun" :: (type, real_vector) real_vector
by standard (auto simp: scaleR_fun_def algebra_simps)
subsection ‹Additional lemmas›
lemmas [simp del] = vimage_Un vimage_Int
lemma finite_Collect_imageI: "finite {U ∈ f ` X. P U}" if "finite {x∈X. P (f x)}"
proof -
have "{d ∈ f ` X. P d} ⊆ f ` {c ∈ X. P (f c)}"
by blast
then show ?thesis
using finite_surj that by blast
qed
lemma plus_compose: "(x + y) ∘ f = (x ∘ f) + (y ∘ f)"
by auto
lemma mult_compose: "(x * y) ∘ f = (x ∘ f) * (y ∘ f)"
by auto
lemma scaleR_compose: "(c *⇩R x) ∘ f = c *⇩R (x ∘ f)"
by (auto simp:)
lemma image_scaleR_ball:
fixes a :: "'a::real_normed_vector"
shows "c ≠ 0 ⟹ (*⇩R) c ` ball a r = ball (c *⇩R a) (abs c *⇩R r)"
proof (auto simp: mem_ball dist_norm, goal_cases)
case (1 b)
have "norm (c *⇩R a - c *⇩R b) = abs c * norm (a - b)"
by (auto simp: norm_scaleR[symmetric] algebra_simps simp del: norm_scaleR)
also have "… < abs c * r"
apply (rule mult_strict_left_mono)
using 1 by auto
finally show ?case .
next
case (2 x)
have "norm (a - x /⇩R c) < r"
proof -
have "norm (a - x /⇩R c) = abs c *⇩R norm (a - x /⇩R c) /⇩R abs c"
using 2 by auto
also have "abs c *⇩R norm (a - x /⇩R c) = norm (c *⇩R a - x)"
using 2
by (auto simp: norm_scaleR[symmetric] algebra_simps simp del: norm_scaleR)
also have "… < ¦c¦ * r"
by fact
also have "¦c¦ * r /⇩R ¦c¦ = r" using 2 by auto
finally show ?thesis using 2 by auto
qed
then have xdc: "x /⇩R c ∈ ball a r"
by (auto simp: mem_ball dist_norm)
show ?case
apply (rule image_eqI[OF _ xdc])
using 2 by simp
qed
subsection ‹Continuity›
lemma continuous_within_topologicalE:
assumes "continuous (at x within s) f"
"open B" "f x ∈ B"
obtains A where "open A" "x ∈ A" "⋀y. y ∈ s ⟹ y ∈ A ⟹ f y ∈ B"
using assms continuous_within_topological by metis
lemma continuous_within_topologicalE':
assumes "continuous (at x) f"
"open B" "f x ∈ B"
obtains A where "open A" "x ∈ A" "f ` A ⊆ B"
using assms continuous_within_topologicalE[OF assms]
by (metis UNIV_I image_subsetI)
lemma continuous_on_inverse: "continuous_on S f ⟹ 0 ∉ f ` S ⟹ continuous_on S (λx. inverse (f x))"
for f::"_⇒_::real_normed_div_algebra"
by (auto simp: continuous_on_def intro!: tendsto_inverse)
subsection ‹@{term "(has_derivative)"}›
lemma has_derivative_plus_fun[derivative_intros]:
"(x + y has_derivative x' + y') (at a within A)"
if [derivative_intros]:
"(x has_derivative x') (at a within A)"
"(y has_derivative y') (at a within A)"
by (auto simp: plus_fun_def intro!: derivative_eq_intros)
lemma has_derivative_scaleR_fun[derivative_intros]:
"(x *⇩R y has_derivative x *⇩R y') (at a within A)"
if [derivative_intros]:
"(y has_derivative y') (at a within A)"
by (auto simp: scaleR_fun_def intro!: derivative_eq_intros)
lemma has_derivative_times_fun[derivative_intros]:
"(x * y has_derivative (λh. x a * y' h + x' h * y a)) (at a within A)"
if [derivative_intros]:
"(x has_derivative x') (at a within A)"
"(y has_derivative y') (at a within A)"
for x y::"_⇒'a::real_normed_algebra"
by (auto simp: times_fun_def intro!: derivative_eq_intros)
lemma real_sqrt_has_derivative_generic:
"x ≠ 0 ⟹ (sqrt has_derivative (*) ((if x > 0 then 1 else -1) * inverse (sqrt x) / 2)) (at x within S)"
apply (rule has_derivative_at_withinI)
using DERIV_real_sqrt_generic[of x "(if x > 0 then 1 else -1) * inverse (sqrt x) / 2"] at_within_open[of x "UNIV - {0}"]
by (auto simp: has_field_derivative_def open_delete ac_simps split: if_splits)
lemma sqrt_has_derivative:
"((λx. sqrt (f x)) has_derivative (λxa. (if 0 < f x then 1 else - 1) / (2 * sqrt (f x)) * f' xa)) (at x within S)"
if "(f has_derivative f') (at x within S)" "f x ≠ 0"
by (rule has_derivative_eq_rhs[OF has_derivative_compose[OF that(1) real_sqrt_has_derivative_generic, OF that(2)]])
(auto simp: divide_simps)
lemmas has_derivative_norm_compose[derivative_intros] = has_derivative_compose[OF _ has_derivative_norm]
subsection ‹Differentiable›
lemmas differentiable_on_empty[simp]
lemma differentiable_transform_eventually: "f differentiable (at x within X)"
if "g differentiable (at x within X)"
"f x = g x"
"∀⇩F x in (at x within X). f x = g x"
using that
apply (auto simp: differentiable_def)
subgoal for D
apply (rule exI[where x=D])
apply (auto simp: has_derivative_within)
by (simp add: eventually_mono Lim_transform_eventually)
done
lemma differentiable_within_eqI: "f differentiable at x within X"
if "g differentiable at x within X" "⋀x. x ∈ X ⟹ f x = g x"
"x ∈ X" "open X"
apply (rule differentiable_transform_eventually)
apply (rule that)
apply (auto simp: that)
proof -
have "∀⇩F x in at x within X. x ∈ X"
using ‹open X›
using eventually_at_topological by blast
then show " ∀⇩F x in at x within X. f x = g x"
by eventually_elim (auto simp: that)
qed
lemma differentiable_eqI: "f differentiable at x"
if "g differentiable at x" "⋀x. x ∈ X ⟹ f x = g x" "x ∈ X" "open X"
using that
unfolding at_within_open[OF that(3,4), symmetric]
by (rule differentiable_within_eqI)
lemma differentiable_on_eqI:
"f differentiable_on S"
if "g differentiable_on S" "⋀x. x ∈ S ⟹ f x = g x" "open S"
using that differentiable_eqI[of g _ S f]
by (auto simp: differentiable_on_eq_differentiable_at)
lemma differentiable_on_comp: "(f o g) differentiable_on S"
if "g differentiable_on S" "f differentiable_on (g ` S)"
using that
by (auto simp: differentiable_on_def intro: differentiable_chain_within)
lemma differentiable_on_comp2: "(f o g) differentiable_on S"
if "f differentiable_on T" "g differentiable_on S" "g ` S ⊆ T"
apply (rule differentiable_on_comp)
apply (rule that)
apply (rule differentiable_on_subset)
apply (rule that)
apply (rule that)
done
lemmas differentiable_on_compose2 = differentiable_on_comp2[unfolded o_def]
lemma differentiable_on_openD: "f differentiable at x"
if "f differentiable_on X" "open X" "x ∈ X"
using differentiable_on_eq_differentiable_at that by blast
lemma differentiable_on_add_fun[intro, simp]:
"x differentiable_on UNIV ⟹ y differentiable_on UNIV ⟹ x + y differentiable_on UNIV"
by (auto simp: plus_fun_def)
lemma differentiable_on_mult_fun[intro, simp]:
"x differentiable_on UNIV ⟹ y differentiable_on UNIV ⟹ x * y differentiable_on UNIV"
for x y::"_⇒'a::real_normed_algebra"
by (auto simp: times_fun_def)
lemma differentiable_on_scaleR_fun[intro, simp]:
"y differentiable_on UNIV ⟹ x *⇩R y differentiable_on UNIV"
by (auto simp: scaleR_fun_def)
lemma sqrt_differentiable:
"(λx. sqrt (f x)) differentiable (at x within S)"
if "f differentiable (at x within S)" "f x ≠ 0"
using that
using sqrt_has_derivative[of f _ x S]
by (auto simp: differentiable_def)
lemma sqrt_differentiable_on: "(λx. sqrt (f x)) differentiable_on S"
if "f differentiable_on S" "0 ∉ f ` S"
using sqrt_differentiable[of f _ S] that
by (force simp: differentiable_on_def)
lemma differentiable_on_inverse: "f differentiable_on S ⟹ 0 ∉ f ` S ⟹ (λx. inverse (f x)) differentiable_on S"
for f::"_⇒_::real_normed_field"
by (auto simp: differentiable_on_def intro!: differentiable_inverse)
lemma differentiable_on_openI:
"f differentiable_on S"
if "open S" "⋀x. x ∈ S ⟹ ∃f'. (f has_derivative f') (at x)"
using that
by (auto simp: differentiable_on_def at_within_open[where S=S] differentiable_def)
lemmas differentiable_norm_compose_at = differentiable_compose[OF differentiable_norm_at]
lemma differentiable_on_Pair:
"f differentiable_on S ⟹ g differentiable_on S ⟹ (λx. (f x, g x)) differentiable_on S"
unfolding differentiable_on_def
using differentiable_Pair[of f _ S g] by auto
lemma differentiable_at_fst:
"(λx. fst (f x)) differentiable at x within X" if "f differentiable at x within X"
using that
by (auto simp: differentiable_def dest!: has_derivative_fst)
lemma differentiable_at_snd:
"(λx. snd (f x)) differentiable at x within X" if "f differentiable at x within X"
using that
by (auto simp: differentiable_def dest!: has_derivative_snd)
lemmas frechet_derivative_worksI = frechet_derivative_works[THEN iffD1]
lemma sin_differentiable_at: "(λx. sin (f x::real)) differentiable at x within X"
if "f differentiable at x within X"
using differentiable_def has_derivative_sin that by blast
lemma cos_differentiable_at: "(λx. cos (f x::real)) differentiable at x within X"
if "f differentiable at x within X"
using differentiable_def has_derivative_cos that by blast
subsection ‹Frechet derivative›
lemmas frechet_derivative_transform_within_open_ext =
fun_cong[OF frechet_derivative_transform_within_open]
lemmas frechet_derivative_at' = frechet_derivative_at[symmetric]
lemma frechet_derivative_plus_fun:
"x differentiable at a ⟹ y differentiable at a ⟹
frechet_derivative (x + y) (at a) =
frechet_derivative x (at a) + frechet_derivative y (at a)"
by (rule frechet_derivative_at')
(auto intro!: derivative_eq_intros frechet_derivative_worksI)
lemmas frechet_derivative_plus = frechet_derivative_plus_fun[unfolded plus_fun_def]
lemma frechet_derivative_zero_fun: "frechet_derivative 0 (at a) = 0"
by (auto simp: frechet_derivative_const zero_fun_def)
lemma frechet_derivative_sin:
"frechet_derivative (λx. sin (f x)) (at x) = (λxa. frechet_derivative f (at x) xa * cos (f x))"
if "f differentiable (at x)"
for f::"_⇒real"
by (rule frechet_derivative_at'[OF has_derivative_sin[OF frechet_derivative_worksI[OF that]]])
lemma frechet_derivative_cos:
"frechet_derivative (λx. cos (f x)) (at x) = (λxa. frechet_derivative f (at x) xa * - sin (f x))"
if "f differentiable (at x)"
for f::"_⇒real"
by (rule frechet_derivative_at'[OF has_derivative_cos[OF frechet_derivative_worksI[OF that]]])
lemma differentiable_sum_fun:
"(⋀i. i ∈ I ⟹ (f i differentiable at a)) ⟹ sum f I differentiable at a"
by (induction I rule: infinite_finite_induct) (auto simp: zero_fun_def plus_fun_def)
lemma frechet_derivative_sum_fun:
"(⋀i. i ∈ I ⟹ (f i differentiable at a)) ⟹
frechet_derivative (∑i∈I. f i) (at a) = (∑i∈I. frechet_derivative (f i) (at a))"
by (induction I rule: infinite_finite_induct)
(auto simp: frechet_derivative_zero_fun frechet_derivative_plus_fun differentiable_sum_fun)
lemma sum_fun_def: "(∑i∈I. f i) = (λx. ∑i∈I. f i x)"
by (induction I rule: infinite_finite_induct) auto
lemmas frechet_derivative_sum = frechet_derivative_sum_fun[unfolded sum_fun_def]
lemma frechet_derivative_times_fun:
"f differentiable at a ⟹ g differentiable at a ⟹
frechet_derivative (f * g) (at a) =
(λx. f a * frechet_derivative g (at a) x + frechet_derivative f (at a) x * g a)"
for f g::"_⇒'a::real_normed_algebra"
by (rule frechet_derivative_at') (auto intro!: derivative_eq_intros frechet_derivative_worksI)
lemmas frechet_derivative_times = frechet_derivative_times_fun[unfolded times_fun_def]
lemma frechet_derivative_scaleR_fun:
"y differentiable at a ⟹
frechet_derivative (x *⇩R y) (at a) =
x *⇩R frechet_derivative y (at a)"
by (rule frechet_derivative_at')
(auto intro!: derivative_eq_intros frechet_derivative_worksI)
lemmas frechet_derivative_scaleR = frechet_derivative_scaleR_fun[unfolded scaleR_fun_def]
lemma frechet_derivative_compose:
"frechet_derivative (f o g) (at x) = frechet_derivative (f) (at (g x)) o frechet_derivative g (at x)"
if "g differentiable at x" "f differentiable at (g x)"
by (meson diff_chain_at frechet_derivative_at' frechet_derivative_works that)
lemma frechet_derivative_compose_eucl:
"frechet_derivative (f o g) (at x) =
(λv. ∑i∈Basis. ((frechet_derivative g (at x) v) ∙ i) *⇩R frechet_derivative f (at (g x)) i)"
(is "?l = ?r")
if "g differentiable at x" "f differentiable at (g x)"
proof (rule ext)
fix v
interpret g: linear "frechet_derivative g (at x)"
using that(1)
by (rule linear_frechet_derivative)
interpret f: linear "frechet_derivative f (at (g x))"
using that(2)
by (rule linear_frechet_derivative)
have "frechet_derivative (f o g) (at x) v =
frechet_derivative f (at (g x)) (∑i∈Basis. (frechet_derivative g (at x) v ∙ i) *⇩R i)"
unfolding frechet_derivative_compose[OF that] o_apply
by (simp add: euclidean_representation)
also have "… = ?r v"
by (auto simp: g.sum g.scaleR f.sum f.scaleR)
finally show "?l v = ?r v" .
qed
lemma frechet_derivative_works_on_open:
"f differentiable_on X ⟹ open X ⟹ x ∈ X ⟹
(f has_derivative frechet_derivative f (at x)) (at x)"
and frechet_derivative_works_on:
"f differentiable_on X ⟹ x ∈ X ⟹
(f has_derivative frechet_derivative f (at x within X)) (at x within X)"
by (auto simp: differentiable_onD differentiable_on_openD frechet_derivative_worksI)
lemma frechet_derivative_inverse: "frechet_derivative (λx. inverse (f x)) (at x) =
(λh. - 1 / (f x)⇧2 * frechet_derivative f (at x) h)"
if "f differentiable at x" "f x ≠ 0" for f::"_⇒_::real_normed_field"
apply (rule frechet_derivative_at')
using that
by (auto intro!: derivative_eq_intros frechet_derivative_worksI
simp: divide_simps algebra_simps power2_eq_square)
lemma frechet_derivative_sqrt: "frechet_derivative (λx. sqrt (f x)) (at x) =
(λv. (if f x > 0 then 1 else -1) / (2 * sqrt (f x)) * frechet_derivative f (at x) v)"
if "f differentiable at x" "f x ≠ 0"
apply (rule frechet_derivative_at')
apply (rule sqrt_has_derivative[THEN has_derivative_eq_rhs])
by (auto intro!: frechet_derivative_worksI that simp: divide_simps)
lemma frechet_derivative_norm: "frechet_derivative (λx. norm (f x)) (at x) =
(λv. frechet_derivative f (at x) v ∙ sgn (f x))"
if "f differentiable at x" "f x ≠ 0"
for f::"_⇒_::real_inner"
apply (rule frechet_derivative_at')
by (auto intro!: derivative_eq_intros frechet_derivative_worksI that simp: divide_simps)
lemma (in bounded_linear) frechet_derivative:
"frechet_derivative f (at x) = f"
apply (rule frechet_derivative_at')
apply (rule has_derivative_eq_rhs)
apply (rule has_derivative)
by (auto intro!: derivative_eq_intros)
bundle no_matrix_mult begin
no_notation matrix_matrix_mult (infixl "**" 70)
end
lemma (in bounded_bilinear) frechet_derivative:
includes no_matrix_mult
shows
"x differentiable at a ⟹ y differentiable at a ⟹
frechet_derivative (λa. x a ** y a) (at a) =
(λh. x a ** frechet_derivative y (at a) h + frechet_derivative x (at a) h ** y a)"
by (rule frechet_derivative_at') (auto intro!: FDERIV frechet_derivative_worksI)
lemma frechet_derivative_divide: "frechet_derivative (λx. f x / g x) (at x) =
(λh. frechet_derivative f (at x) h / (g x) -frechet_derivative g (at x) h * f x / (g x)⇧2)"
if "f differentiable at x" "g differentiable at x" "g x ≠ 0" for f::"_⇒_::real_normed_field"
using that
by (auto simp: divide_inverse_commute bounded_bilinear.frechet_derivative[OF bounded_bilinear_mult]
frechet_derivative_inverse)
lemma frechet_derivative_pair:
"frechet_derivative (λx. (f x, g x)) (at x) = (λv. (frechet_derivative f (at x) v, frechet_derivative g (at x) v))"
if "f differentiable (at x)" "g differentiable (at x)"
by (metis (no_types) frechet_derivative_at frechet_derivative_works has_derivative_Pair that)
lemma frechet_derivative_fst:
"frechet_derivative (λx. fst (f x)) (at x) = (λxa. fst (frechet_derivative f (at x) xa))"
if "(f differentiable at x)"
for f::"_⇒(_::real_normed_vector × _::real_normed_vector)"
by (metis frechet_derivative_at frechet_derivative_works has_derivative_fst that)
lemma frechet_derivative_snd:
"frechet_derivative (λx. snd (f x)) (at x) = (λxa. snd (frechet_derivative f (at x) xa))"
if "(f differentiable at x)"
for f::"_⇒(_::real_normed_vector × _::real_normed_vector)"
by (metis frechet_derivative_at frechet_derivative_worksI has_derivative_snd that)
lemma frechet_derivative_eq_vector_derivative_1:
assumes "f differentiable at t"
shows "frechet_derivative f (at t) 1 = vector_derivative f (at t)"
by (simp add: assms frechet_derivative_eq_vector_derivative)
subsection ‹Linear algebra›
lemma (in vector_space) dim_pos_finite_dimensional_vector_spaceE:
assumes "dim (UNIV::'b set) > 0"
obtains basis where "finite_dimensional_vector_space scale basis"
proof -
from assms obtain b where b: "local.span b = local.span UNIV" "local.independent b"
by (auto simp: dim_def split: if_splits)
then have "dim UNIV = card b"
by (rule dim_eq_card)
with assms have "finite b" by (auto simp: card_ge_0_finite)
then have "finite_dimensional_vector_space scale b"
by unfold_locales (auto simp: b)
then show ?thesis ..
qed
context vector_space_on begin
context includes lifting_syntax assumes "∃(Rep::'s ⇒ 'b) (Abs::'b ⇒ 's). type_definition Rep Abs S" begin
interpretation local_typedef_vector_space_on S scale "TYPE('s)" by unfold_locales fact
lemmas_with [var_simplified explicit_ab_group_add,
unoverload_type 'd,
OF type.ab_group_add_axioms type_vector_space_on_with,
folded dim_S_def,
untransferred,
var_simplified implicit_ab_group_add]:
lt_dim_pos_finite_dimensional_vector_spaceE = vector_space.dim_pos_finite_dimensional_vector_spaceE
end
lemmas_with [cancel_type_definition,
OF S_ne,
folded subset_iff',
simplified pred_fun_def, folded finite_dimensional_vector_space_on_with,
simplified]:
dim_pos_finite_dimensional_vector_spaceE = lt_dim_pos_finite_dimensional_vector_spaceE
end
subsection ‹Extensional function space›
text ‹f is zero outside A. We use such functions to canonically represent
functions whose domain is A›
definition extensional0 :: "'a set ⇒ ('a ⇒ 'b::zero) ⇒ bool"
where "extensional0 A f = (∀x. x ∉ A ⟶ f x = 0)"
lemma extensional0_0[intro, simp]: "extensional0 X 0"
by (auto simp: extensional0_def)
lemma extensional0_UNIV[intro, simp]: "extensional0 UNIV f"
by (auto simp: extensional0_def)
lemma ext_extensional0:
"f = g" if "extensional0 S f" "extensional0 S g" "⋀x. x ∈ S ⟹ f x = g x"
using that by (force simp: extensional0_def fun_eq_iff)
lemma extensional0_add[intro, simp]:
"extensional0 S f ⟹ extensional0 S g ⟹ extensional0 S (f + g::_⇒'a::comm_monoid_add)"
by (auto simp: extensional0_def)
lemma extensinoal0_mult[intro, simp]:
"extensional0 S x ⟹ extensional0 S y ⟹ extensional0 S (x * y)"
for x y::"_⇒'a::mult_zero"
by (auto simp: extensional0_def)
lemma extensional0_scaleR[intro, simp]: "extensional0 S f ⟹ extensional0 S (c *⇩R f::_⇒'a::real_vector)"
by (auto simp: extensional0_def)
lemma extensional0_outside: "x ∉ S ⟹ extensional0 S f ⟹ f x = 0"
by (auto simp: extensional0_def)
lemma subspace_extensional0: "subspace (Collect (extensional0 X))"
by (auto simp: subspace_def)
text ‹Send the function f to its canonical representative as a function with domain A›
definition restrict0 :: "'a set ⇒ ('a ⇒ 'b::zero) ⇒ 'a ⇒ 'b"
where "restrict0 A f x = (if x ∈ A then f x else 0)"
lemma restrict0_UNIV[simp]: "restrict0 UNIV = (λx. x)"
by (intro ext) (auto simp: restrict0_def)
lemma extensional0_restrict0[intro, simp]: "extensional0 A (restrict0 A f)"
by (auto simp: extensional0_def restrict0_def)
lemma restrict0_times: "restrict0 A (x * y) = restrict0 A x * restrict0 A y"
for x::"'a⇒'b::mult_zero"
by (auto simp: restrict0_def[abs_def])
lemma restrict0_apply_in[simp]: "x ∈ A ⟹ restrict0 A f x = f x"
by (auto simp: restrict0_def)
lemma restrict0_apply_out[simp]: "x ∉ A ⟹ restrict0 A f x = 0"
by (auto simp: restrict0_def)
lemma restrict0_scaleR: "restrict0 A (c *⇩R f::_⇒'a::real_vector) = c *⇩R restrict0 A f"
by (auto simp: restrict0_def[abs_def])
lemma restrict0_add: "restrict0 A (f + g::_⇒'a::real_vector) = restrict0 A f + restrict0 A g"
by (auto simp: restrict0_def[abs_def])
lemma restrict0_restrict0: "restrict0 X (restrict0 Y f) = restrict0 (X ∩ Y) f"
by (auto simp: restrict0_def)
end