Theory Differentiable_Manifold
section ‹Differentiable/Smooth Manifolds›
theory Differentiable_Manifold
imports
Smooth
Topological_Manifold
begin
subsection ‹Smooth compatibility›
definition smooth_compat::"enat ⇒ ('a::topological_space, 'e::euclidean_space)chart⇒('a, 'e)chart⇒bool"
(‹_-smooth'_compat› [1000])
where
"smooth_compat k c1 c2 ⟷
(k-smooth_on (c1 ` (domain c1 ∩ domain c2)) (c2 ∘ inv_chart c1) ∧
k-smooth_on (c2 ` (domain c1 ∩ domain c2)) (c1 ∘ inv_chart c2) )"
lemma smooth_compat_D1:
"k-smooth_on (c1 ` (domain c1 ∩ domain c2)) (c2 ∘ inv_chart c1)"
if "k-smooth_compat c1 c2"
proof -
have "open (c1 ` (domain c1 ∩ domain c2))"
by (rule open_chart_image) auto
moreover have "k-smooth_on (c1 ` (domain c1 ∩ domain c2)) (c2 ∘ inv_chart c1)"
using that(1) by (auto simp: smooth_compat_def)
ultimately show ?thesis by blast
qed
lemma smooth_compat_D2:
"k-smooth_on (c2 ` (domain c1 ∩ domain c2)) (c1 ∘ inv_chart c2)"
if "k-smooth_compat c1 c2"
proof -
have "open (c2 ` (domain c1 ∩ domain c2))"
by (rule open_chart_image) auto
moreover have "k-smooth_on (c2 ` (domain c1 ∩ domain c2)) (c1 ∘ inv_chart c2) "
using that(1) by (auto simp: smooth_compat_def)
ultimately show ?thesis by blast
qed
lemma smooth_compat_refl: "k-smooth_compat x x"
unfolding smooth_compat_def
by (auto intro: smooth_on_cong[where g="λx. x"] simp: smooth_on_id)
lemma smooth_compat_commute: "k-smooth_compat x y ⟷ k-smooth_compat y x"
by (auto simp: smooth_compat_def inf_commute)
lemma smooth_compat_restrict_chartI:
"k-smooth_compat (restrict_chart S c) c'"
if "k-smooth_compat c c'"
using that
by (auto simp: smooth_compat_def domain_restrict_chart_if intro: smooth_on_subset)
lemma smooth_compat_restrict_chartI2:
"k-smooth_compat c' (restrict_chart S c)"
if "k-smooth_compat c' c"
using smooth_compat_restrict_chartI[of k c c'] that
by (auto simp: smooth_compat_commute)
lemma smooth_compat_restrict_chartD:
"domain c1 ⊆ U ⟹ open U ⟹ k-smooth_compat c1 (restrict_chart U c2) ⟹ k-smooth_compat c1 c2"
by (auto simp: smooth_compat_def domain_restrict_chart_if intro: smooth_on_subset)
lemma smooth_compat_restrict_chartD2:
"domain c1 ⊆ U ⟹ open U ⟹ k-smooth_compat (restrict_chart U c2) c1 ⟹ k-smooth_compat c2 c1"
using smooth_compat_restrict_chartD[of c1 U k c2]
by (auto simp: smooth_compat_commute)
lemma smooth_compat_le:
"l-smooth_compat c1 c2" if "k-smooth_compat c1 c2" "l ≤ k"
using that
by (auto simp: smooth_compat_def smooth_on_le)
subsection ‹‹C^k›-Manifold›
locale c_manifold = manifold +
fixes k::enat
assumes pairwise_compat: "c1 ∈ charts ⟹ c2 ∈ charts ⟹ k-smooth_compat c1 c2"
begin
subsubsection ‹Atlas›
definition atlas :: "('a, 'b) chart set" where
"atlas = {c. domain c ⊆ carrier ∧ (∀c' ∈ charts. k-smooth_compat c c')}"
lemma charts_subset_atlas: "charts ⊆ atlas"
by (auto simp: atlas_def pairwise_compat)
lemma in_charts_in_atlas[intro]: "x ∈ charts ⟹ x ∈ atlas"
by (auto simp: atlas_def pairwise_compat)
lemma maximal_atlas:
"c ∈ atlas"
if "⋀c'. c' ∈ atlas ⟹ k-smooth_compat c c'"
"domain c ⊆ carrier"
using that charts_subset_atlas
by (auto simp: atlas_def)
lemma chart_compose_lemma:
fixes c1 c2
defines [simp]: "U ≡ domain c1"
defines [simp]: "V ≡ domain c2"
assumes subsets: "U ∩ V ⊆ carrier"
assumes "⋀c. c ∈ charts ⟹ k-smooth_compat c1 c"
"⋀c. c ∈ charts ⟹ k-smooth_compat c2 c"
shows "k-smooth_on (c1 ` (U ∩ V)) (c2 ∘ inv_chart c1)"
proof (rule smooth_on_open_subsetsI)
fix w' assume "w' ∈ c1 ` (U ∩ V)"
then obtain w where w': "w' = c1 w" and "w ∈ U" "w ∈ V" by auto
then have "w ∈ carrier" using subsets
by auto
then obtain c3 where c3: "w ∈ domain c3" "c3 ∈ charts"
by (rule carrierE)
then have c13: "k-smooth_compat c1 c3" and c23: "k-smooth_compat c2 c3"
using assms by auto
define W where [simp]: "W = domain c3"
have diff1: "k-smooth_on (c1 ` (U ∩ W)) (c3 ∘ inv_chart c1)"
proof -
have 1: "open (c1 ` (U ∩ W))"
by (rule open_chart_image) auto
have 2: "w' ∈ c1 ` (U ∩ W)"
using ‹w ∈ U› by (auto simp: c3 w')
from c13 show ?thesis
by (auto simp: smooth_compat_def)
qed
define y where "y = (c3 ∘ inv_chart c1) w'"
have diff2: "k-smooth_on (c3 ` (V ∩ W)) (c2 ∘ inv_chart c3)"
proof -
have 1: "open (c3 ` (V ∩ W))"
by (rule open_chart_image) auto
have 2: "y ∈ c3 ` (V ∩ W)"
using ‹w ∈ U› ‹w ∈ V› by (auto simp: y_def c3 w')
from c23 show ?thesis
by (auto simp: smooth_compat_def)
qed
have "k-smooth_on (c1 ` (U ∩ V ∩ W)) ((c2 ∘ inv_chart c3) o (c3 ∘ inv_chart c1))"
using diff2 diff1
by (rule smooth_on_compose2) auto
then have "k-smooth_on (c1 ` (U ∩ V ∩ W)) (c2 ∘ inv_chart c1)"
by (rule smooth_on_cong) auto
moreover have "w' ∈ c1 ` (U ∩ V ∩ W)" "open (c1 ` (U ∩ V ∩ W))"
using ‹w ∈ U› ‹w ∈ V›
by (auto simp: w' c3)
ultimately show "∃T. w' ∈ T ∧ open T ∧ k-smooth_on T (apply_chart c2 ∘ inv_chart c1)"
by (intro exI[where x="c1 ` (U ∩ V ∩ W)"]) simp
qed
lemma smooth_compat_trans: "k-smooth_compat c1 c2"
if "⋀c. c ∈ charts ⟹ k-smooth_compat c1 c"
"⋀c. c ∈ charts ⟹ k-smooth_compat c2 c"
"domain c1 ∩ domain c2 ⊆ carrier"
unfolding smooth_compat_def
proof
show "k-smooth_on (c1 ` (domain c1 ∩ domain c2)) (c2 ∘ inv_chart c1)"
by (auto intro!: that chart_compose_lemma)
show "k-smooth_on (c2 ` (domain c1 ∩ domain c2)) (c1 ∘ inv_chart c2)"
using that
by (subst inf_commute) (auto intro!: chart_compose_lemma)
qed
lemma maximal_atlas':
"c ∈ atlas"
if "⋀c'. c' ∈ charts ⟹ k-smooth_compat c c'"
"domain c ⊆ carrier"
proof (rule maximal_atlas)
fix c' assume "c' ∈ atlas"
show "k-smooth_compat c c'"
apply (rule smooth_compat_trans)
apply (rule that(1)) apply assumption
using atlas_def ‹c' ∈ atlas› by auto
qed fact
lemma atlas_is_atlas: "k-smooth_compat a1 a2"
if "a1 ∈ atlas" "a2 ∈ atlas"
using that atlas_def smooth_compat_trans by blast
lemma domain_atlas_subset_carrier: "c ∈ atlas ⟹ domain c ⊆ carrier"
and in_carrier_atlasI[intro, simp]: "c ∈ atlas ⟹ x ∈ domain c ⟹ x ∈ carrier"
by (auto simp: atlas_def)
lemma atlasE:
assumes "x ∈ carrier"
obtains c where "c ∈ atlas" "x ∈ domain c"
using carrierE[OF assms] charts_subset_atlas
by blast
lemma restrict_chart_in_atlas: "restrict_chart S c ∈ atlas" if "c ∈ atlas"
proof (rule maximal_atlas)
fix c' assume "c' ∈ atlas"
then have "k-smooth_compat c c'" using ‹c ∈ atlas› by (auto simp: atlas_is_atlas)
then show "k-smooth_compat (restrict_chart S c) c'"
by (rule smooth_compat_restrict_chartI)
next
have "domain (restrict_chart S c) ⊆ domain c"
by (simp add: domain_restrict_chart_if)
also have "… ⊆ carrier"
using that
by (rule domain_atlas_subset_carrier)
finally
show "domain (restrict_chart S c) ⊆ carrier"
by auto
qed
lemma atlas_restrictE:
assumes "x ∈ carrier" "x ∈ X" "open X"
obtains c where "c ∈ atlas" "x ∈ domain c" "domain c ⊆ X"
proof -
from assms(1) obtain c where c: "c ∈ atlas" "x ∈ domain c"
by (blast elim!: carrierE)
define d where "d = restrict_chart X c"
from c have "d ∈ atlas" "x ∈ domain d" "domain d ⊆ X"
using assms(2,3)
by (auto simp: d_def restrict_chart_in_atlas)
then show ?thesis ..
qed
lemma open_ball_chartE:
assumes "x ∈ U" "open U" "U ⊆ carrier"
obtains c r where
"c ∈ atlas"
"x ∈ domain c" "domain c ⊆ U" "codomain c = ball (c x) r" "r > 0"
proof -
from assms have "x ∈ carrier" by auto
from carrierE[OF this] obtain c where c: "c ∈ charts" "x ∈ domain c" by auto
then have "x ∈ domain c ∩ U" using assms by auto
then have "open (apply_chart c ` (domain c ∩ U))" "c x ∈ c ` (domain c ∩ U)"
by (auto intro!: assms)
from openE[OF this]
obtain e where e: "0 < e" "ball (c x) e ⊆ c ` (domain c ∩ U)"
by auto
define C where "C = inv_chart c ` ball (c x) e"
have "open C"
using e
by (auto simp: C_def)
define c' where "c' = restrict_chart C c"
from c have "c ∈ atlas" by auto
then have "c' ∈ atlas" by (auto simp: c'_def restrict_chart_in_atlas)
moreover
have "x ∈ C"
using c ‹e > 0›
unfolding C_def
by (auto intro!: image_eqI[where x="apply_chart c x"])
have "x ∈ domain c'"
by (auto simp: c'_def ‹open C› c ‹x ∈ C›)
moreover
have "C ⊆ U"
using e by (auto simp: C_def)
then have "domain c' ⊆ U"
by (auto simp: c'_def ‹open C›)
moreover have "codomain c' = ball (c' x) e"
using e ‹open C›
by (force simp: c'_def codomain_restrict_chart_if C_def)
moreover
have "e > 0"
by fact
ultimately show ?thesis ..
qed
lemma smooth_compat_compose_chart:
fixes c'
assumes "k-smooth_compat c c'"
assumes diffeo: "diffeomorphism k UNIV UNIV p p'"
shows "k-smooth_compat (compose_chart p p' c) c'"
proof -
note dD[simp] = diffeomorphismD[OF diffeo]
note homeo[simp] = diffeomorphism_imp_homeomorphism[OF diffeo]
from assms(1) have c: "k-smooth_on (apply_chart c ` (domain c ∩ domain c')) (apply_chart c' ∘ inv_chart c)"
and c': "k-smooth_on (apply_chart c' ` (domain c ∩ domain c')) (apply_chart c ∘ inv_chart c')"
by (auto simp: smooth_compat_def)
from homeo have *: "open (p ` apply_chart c ` (domain c ∩ domain c'))"
by (rule homeomorphism_UNIV_imp_open_map) auto
have "k-smooth_on ((p ∘ apply_chart c) ` (domain c ∩ domain c')) (apply_chart c' ∘ inv_chart c ∘ p')"
apply (rule smooth_on_compose2) prefer 2
apply (rule dD)
apply (rule c)
apply (auto simp add: assms image_comp [symmetric] * cong del: image_cong_simp)
done
moreover
have "k-smooth_on (apply_chart c' ` (domain c ∩ domain c')) (p ∘ (apply_chart c ∘ inv_chart c'))"
apply (rule smooth_on_compose2)
apply (rule dD)
apply fact
by (auto simp: assms image_comp[symmetric])
ultimately show ?thesis
unfolding smooth_compat_def
by (auto intro!: simp: o_assoc)
qed
lemma compose_chart_in_atlas:
assumes "c ∈ atlas"
assumes diffeo: "diffeomorphism k UNIV UNIV p p'"
shows "compose_chart p p' c ∈ atlas"
proof (rule maximal_atlas)
note [simp] = diffeomorphism_imp_homeomorphism[OF diffeo]
show "domain (compose_chart p p' c) ⊆ carrier"
using assms
by auto
fix c' assume "c' ∈ atlas"
with ‹c ∈ atlas› have "k-smooth_compat c c'"
by (rule atlas_is_atlas)
then show "k-smooth_compat (compose_chart p p' c) c'"
using diffeo
by (rule smooth_compat_compose_chart)
qed
lemma open_centered_ball_chartE:
assumes "x ∈ U" "open U" "U ⊆ carrier" "e > 0"
obtains c where
"c ∈ atlas" "x ∈ domain c" "c x = x0" "domain c ⊆ U" "codomain c = ball x0 e"
proof -
from open_ball_chartE[OF assms(1-3)] obtain c r where c:
"c ∈ atlas"
"x ∈ domain c" "domain c ⊆ U" "codomain c = ball (c x) r"
and r: "r > 0"
by auto
have nz: "e / r ≠ 0" using ‹e > 0› ‹r > 0› by auto
have 1: "diffeomorphism k UNIV UNIV (λy. y + (- c x)) (λy. y - (- c x))"
using diffeomorphism_add[of k "(- c x)"] by auto
have 2: "diffeomorphism k UNIV UNIV (λy. (e / r) *⇩R y) (λy. y /⇩R (e / r))"
using diffeomorphism_scaleR[of "e / r" k] ‹e > 0› ‹r > 0› by auto
have 3: "diffeomorphism k UNIV UNIV (λy. y + x0) (λy. y - x0)"
using diffeomorphism_add[of k x0] by auto
define t where "t = (λy. (e / r) *⇩R (y + - c x) + x0)"
define t' where "t' = (λy. (y - x0) /⇩R (e / r) + c x)"
from diffeomorphism_compose[OF diffeomorphism_compose[OF 1 2] 3, unfolded o_def]
have diffeo: "diffeomorphism k UNIV UNIV t t'"
by (auto simp: t_def t'_def o_def)
from compose_chart_in_atlas[OF ‹c ∈ atlas› this]
have "compose_chart t t' c ∈ atlas" .
moreover
note [simp] = diffeomorphism_imp_homeomorphism[OF diffeo]
have "x ∈ domain (compose_chart t t' c)" by (auto simp: ‹x ∈ domain c›)
moreover
have "t (c x) = x0"
by (auto simp: t_def)
then have "compose_chart t t' c x = x0"
by simp
moreover have "domain (compose_chart t t' c) ⊆ U"
using ‹domain c ⊆ U›
by auto
moreover
have "t ` codomain c = ball x0 e"
proof -
have "t ` codomain c = (+) x0 ` (*⇩R) (e / r) ` (λy. - apply_chart c x + y) ` ball (c x) r"
by (auto simp add: c t_def image_image)
also have "… = ball x0 e"
using ‹e > 0› ‹r > 0›
unfolding image_add_ball image_scaleR_ball[OF nz]
by simp
finally show ?thesis .
qed
then have "codomain (compose_chart t t' c) = ball x0 e"
by auto
ultimately show ?thesis ..
qed
end
subsubsection ‹Submanifold›
definition (in manifold) "charts_submanifold S = (restrict_chart S ` charts)"
locale c_manifold' = c_manifold
locale submanifold = c_manifold' charts k
for charts::"('a::{t2_space,second_countable_topology}, 'b::euclidean_space) chart set" and k +
fixes S::"'a set"
assumes open_submanifold: "open S"
begin
lemma charts_submanifold: "c_manifold (charts_submanifold S) k"
by unfold_locales
(auto simp: charts_submanifold_def atlas_is_atlas in_charts_in_atlas restrict_chart_in_atlas)
sublocale sub: c_manifold "(charts_submanifold S)" k
by (rule charts_submanifold)
lemma carrier_submanifold[simp]: "sub.carrier = S ∩ carrier"
using open_submanifold
by (auto simp: manifold.carrier_def charts_submanifold_def domain_restrict_chart_if split: if_splits)
lemma restrict_chart_carrier[simp]:
"restrict_chart carrier x = x"
if "x ∈ charts"
using that
by (auto intro!: chart_eqI)
lemma charts_submanifold_carrier[simp]: "charts_submanifold carrier = charts"
by (force simp: charts_submanifold_def)
lemma charts_submanifold_Int_carrier:
"charts_submanifold (S ∩ carrier) = charts_submanifold S"
using open_submanifold
by (force simp: charts_submanifold_def restrict_chart_restrict_chart[symmetric])
lemma submanifold_atlasE:
assumes "c ∈ sub.atlas"
shows "c ∈ atlas"
proof (rule maximal_atlas')
have dc: "domain c ⊆ S ∩ carrier"
using assms sub.domain_atlas_subset_carrier
by auto
then show "domain c ⊆ carrier"
using open_submanifold by auto
fix c' assume "c' ∈ charts"
then have "restrict_chart S c' ∈ (charts_submanifold S)"
by (auto simp: charts_submanifold_def)
then have "restrict_chart S c' ∈ sub.atlas"
by auto
have "k-smooth_compat c (restrict_chart S c')"
by (rule sub.atlas_is_atlas) fact+
show "k-smooth_compat c c'"
apply (rule smooth_compat_restrict_chartD[where U=S])
subgoal using dc by auto
subgoal by (rule open_submanifold)
subgoal by fact
done
qed
lemma submanifold_atlasI:
"restrict_chart S c ∈ sub.atlas"
if "c ∈ atlas"
proof (rule sub.maximal_atlas')
fix c' assume "c' ∈ (charts_submanifold S)"
then obtain c'' where c'': "c' = restrict_chart S c''" "c'' ∈ charts"
unfolding charts_submanifold_def by auto
show "k-smooth_compat (restrict_chart S c) c'"
unfolding c''
apply (rule smooth_compat_restrict_chartI)
apply (rule smooth_compat_restrict_chartI2)
apply (rule atlas_is_atlas)
apply fact using ‹c'' ∈ charts› by auto
next
show "domain (restrict_chart S c) ⊆ sub.carrier"
using domain_atlas_subset_carrier[OF that]
by (auto simp: open_submanifold )
qed
end
lemma (in c_manifold) restrict_chart_carrier[simp]:
"restrict_chart carrier x = x"
if "x ∈ charts"
using that
by (auto intro!: chart_eqI)
lemma (in c_manifold) charts_submanifold_carrier[simp]: "charts_submanifold carrier = charts"
by (force simp: charts_submanifold_def)
subsection ‹Differentiable maps›
locale c_manifolds =
src: c_manifold charts1 k +
dest: c_manifold charts2 k for k charts1 charts2
locale diff = c_manifolds k charts1 charts2
for k
and charts1 :: "('a::{t2_space,second_countable_topology}, 'e::euclidean_space) chart set"
and charts2 :: "('b::{t2_space,second_countable_topology}, 'f::euclidean_space) chart set"
+
fixes f :: "('a ⇒ 'b)"
assumes exists_smooth_on: "x ∈ src.carrier ⟹
∃c1∈src.atlas. ∃c2∈dest.atlas.
x ∈ domain c1 ∧
f ` domain c1 ⊆ domain c2 ∧
k-smooth_on (codomain c1) (c2 ∘ f ∘ inv_chart c1)"
begin
lemma defined: "f ` src.carrier ⊆ dest.carrier"
using exists_smooth_on
by auto
end
context c_manifolds begin
lemma diff_iff: "diff k charts1 charts2 f ⟷
(∀x∈src.carrier. ∃c1∈src.atlas. ∃c2∈dest.atlas.
x ∈ domain c1 ∧
f ` domain c1 ⊆ domain c2 ∧
k-smooth_on (codomain c1) (apply_chart c2 ∘ f ∘ inv_chart c1))"
(is "?l ⟷ (∀x∈_. ?r x)")
proof safe
assume ?l
interpret diff k charts1 charts2 f by fact
show "x ∈ src.carrier ⟹ ?r x" for x
by (rule exists_smooth_on)
next
assume "∀x∈src.carrier. ?r x"
then show ?l
by unfold_locales auto
qed
end
context diff begin
lemma diffE:
assumes "x ∈ src.carrier"
obtains c1::"('a, 'e) chart"
and c2::"('b, 'f) chart"
where
"c1 ∈ src.atlas" "c2 ∈ dest.atlas" "x ∈ domain c1" "f ` domain c1 ⊆ domain c2"
"k-smooth_on (codomain c1) (apply_chart c2 ∘ f ∘ inv_chart c1)"
using exists_smooth_on assms by force
lemma continuous_at: "continuous (at x within T) f" if "x ∈ src.carrier"
proof -
from that obtain c1 c2 where "c1 ∈ src.atlas" "c2 ∈ dest.atlas" "x ∈ domain c1"
"f ` domain c1 ⊆ domain c2"
"k-smooth_on (codomain c1) (apply_chart c2 ∘ f ∘ inv_chart c1)"
by (rule diffE)
from smooth_on_imp_continuous_on[OF this(5)]
have "continuous_on (codomain c1) (apply_chart c2 ∘ f ∘ inv_chart c1)" .
then have "continuous_on (c1 ` domain c1) (f ∘ inv_chart c1)"
using ‹f ` domain c1 ⊆ domain c2› continuous_on_chart_inv by (fastforce simp: image_domain_eq)
then have "continuous_on (domain c1) f"
by (rule continuous_on_chart_inv') simp
then have "isCont f x"
using ‹x ∈ domain c1›
unfolding continuous_on_eq_continuous_at[OF open_domain]
by auto
then show "continuous (at x within T) f"
by (simp add: ‹isCont f x› continuous_at_imp_continuous_within)
qed
lemma continuous_on: "continuous_on src.carrier f"
unfolding continuous_on_eq_continuous_within
by (auto intro: continuous_at)
lemmas continuous_on_intro[continuous_intros] = continuous_on_compose2[OF continuous_on _]
lemmas continuous_within[continuous_intros] = continuous_within_compose3[OF continuous_at]
lemmas tendsto[tendsto_intros] = isCont_tendsto_compose[OF continuous_at]
lemma diff_chartsD:
assumes "d1 ∈ src.atlas" "d2 ∈ dest.atlas"
shows "k-smooth_on (codomain d1 ∩ inv_chart d1 -` (src.carrier ∩ f -` domain d2))
(apply_chart d2 ∘ f ∘ inv_chart d1)"
proof (rule smooth_on_open_subsetsI)
fix y assume "y ∈ codomain d1 ∩ inv_chart d1 -` (src.carrier ∩ f -` domain d2)"
then have y: "f (inv_chart d1 y) ∈ domain d2" "y ∈ codomain d1"
by auto
then obtain x where x: "d1 x = y" "x ∈ domain d1"
by force
then have "x ∈ src.carrier" using assms by force
obtain c1 c2 where "c1 ∈ src.atlas" "c2 ∈ dest.atlas"
and fc1: "f ` domain c1 ⊆ domain c2"
and xc1: "x ∈ domain c1"
and d: "k-smooth_on (codomain c1) (apply_chart c2 ∘ f ∘ inv_chart c1)"
using diffE[OF ‹x ∈ src.carrier›]
by metis
have [simp]: "x ∈ domain c1 ⟹ f x ∈ domain c2" for x using fc1 by auto
have r1: "k-smooth_on (d1 ` (domain d1 ∩ domain c1)) (c1 ∘ inv_chart d1)"
using src.atlas_is_atlas[OF ‹d1 ∈ src.atlas› ‹c1 ∈ src.atlas›, THEN smooth_compat_D1] .
have r2: "k-smooth_on (c2 ` (domain d2 ∩ domain c2)) (d2 ∘ inv_chart c2)"
using dest.atlas_is_atlas[OF ‹d2 ∈ dest.atlas› ‹c2 ∈ dest.atlas›, THEN smooth_compat_D2] .
define T where "T = (d1 ` (domain d1 ∩ domain c1) ∩ inv_chart d1 -` (src.carrier ∩ (f -` domain d2)))"
have "open T"
unfolding T_def
by (rule open_continuous_vimage')
(auto intro!: continuous_intros open_continuous_vimage' src.open_carrier)
have T_subset: "T ⊆ apply_chart d1 ` (domain d1 ∩ domain c1)"
by (auto simp: T_def)
have opens: "open (c1 ` inv_chart d1 ` T)" "open (c2 ` (domain d2 ∩ domain c2))"
using fc1 ‹open T›
by (force simp: T_def)+
have "k-smooth_on ((apply_chart c1 ∘ inv_chart d1) ` T) (d2 ∘ inv_chart c2 ∘ (c2 ∘ f ∘ inv_chart c1))"
using r2 d opens
unfolding image_comp[symmetric]
by (rule smooth_on_compose2) (auto simp: T_def)
from this r1 ‹open T› opens(1) have "k-smooth_on T
((d2 ∘ inv_chart c2) ∘ (c2 ∘ f ∘ inv_chart c1) ∘ (c1 ∘ inv_chart d1))"
unfolding image_comp[symmetric]
by (rule smooth_on_compose2) (force simp: T_def)+
then have "k-smooth_on T (d2 ∘ f ∘ inv_chart d1)"
using ‹open T›
by (rule smooth_on_cong) (auto simp: T_def)
moreover have "y ∈ T"
using x xc1 fc1 y ‹c1 ∈ src.atlas›
by (auto simp: T_def)
ultimately show "∃T. y ∈ T ∧ open T ∧ k-smooth_on T (apply_chart d2 ∘ f ∘ inv_chart d1)"
using ‹open T›
by metis
qed
lemma diff_between_chartsE:
assumes "d1 ∈ src.atlas" "d2 ∈ dest.atlas"
assumes "y ∈ domain d1" "y ∈ src.carrier" "f y ∈ domain d2"
obtains X where
"k-smooth_on X (apply_chart d2 ∘ f ∘ inv_chart d1)"
"d1 y ∈ X"
"open X"
"X = codomain d1 ∩ inv_chart d1 -` (src.carrier ∩ f -` domain d2)"
proof -
define X where "X = (codomain d1 ∩ inv_chart d1 -` (src.carrier ∩ f -` domain d2))"
from diff_chartsD[OF assms(1,2)]
have "k-smooth_on X (apply_chart d2 ∘ f ∘ inv_chart d1)"
by (simp add: X_def)
moreover have "d1 y ∈ X"
using assms(3-5)
by (auto simp: X_def)
moreover have "open X"
unfolding X_def
by (auto intro!: open_continuous_vimage' continuous_intros src.open_carrier)
moreover note X_def
ultimately show ?thesis ..
qed
end
lemma diff_compose:
"diff k M1 M3 (g ∘ f)"
if "diff k M1 M2 f" "diff k M2 M3 g"
proof -
interpret f: diff k M1 M2 f by fact
interpret g: diff k M2 M3 g by fact
interpret fg: c_manifolds k M1 M3 by unfold_locales
show ?thesis
unfolding fg.diff_iff
proof safe
fix x assume "x ∈ f.src.carrier"
then obtain c1 c2 where c1: "c1 ∈ f.src.atlas"
and c2: "c2 ∈ f.dest.atlas"
and fc1: "f ` domain c1 ⊆ domain c2"
and x: "x ∈ domain c1"
and df: "k-smooth_on (codomain c1) (apply_chart c2 ∘ f ∘ inv_chart c1)"
using f.diffE by metis
have "f x ∈ f.dest.carrier" using f.defined ‹x ∈ f.src.carrier› by auto
then obtain c2' c3 where c2': "c2' ∈ f.dest.atlas"
and c3: "c3 ∈ g.dest.atlas"
and gc2': "g ` domain c2' ⊆ domain c3"
and fx: "f x ∈ domain c2'"
and dg: "k-smooth_on (codomain c2') (apply_chart c3 ∘ g ∘ inv_chart c2')"
using g.diffE by metis
define D where "D = (g ∘ f) -` domain c3 ∩ domain c1"
have "open D"
using f.defined c1
by (auto intro!: continuous_intros open_continuous_vimage simp: D_def)
have "x ∈ D"
using fc1 fx gc2'
by (auto simp: D_def ‹x ∈ domain c1›)
define d1 where "d1 = restrict_chart D c1"
have "d1 ∈ f.src.atlas"
by (auto simp: d1_def intro!: f.src.restrict_chart_in_atlas c1)
moreover have "c3 ∈ g.dest.atlas" by fact
moreover have "x ∈ domain d1" by (auto simp: d1_def ‹open D› ‹x ∈ D› x)
moreover have sub_c3: "(g ∘ f) ` domain d1 ⊆ domain c3"
using ‹open D› by (auto simp: d1_def D_def)
moreover have "k-smooth_on (codomain d1) (c3 ∘ (g ∘ f) ∘ inv_chart d1)"
proof (rule smooth_on_open_subsetsI)
fix y assume y: "y ∈ codomain d1"
then obtain iy where y_def: "y = d1 iy" and iy: "iy ∈ domain d1" by force
note iy
also note f.src.domain_atlas_subset_carrier[OF ‹d1 ∈ f.src.atlas›]
finally have iS: "iy ∈ f.src.carrier" .
then have "f iy ∈ f.dest.carrier"
using f.defined by (auto simp: d1_def)
with f.dest.atlasE obtain d2 where d2: "d2 ∈ f.dest.atlas"
and fy: "f iy ∈ domain d2"
by blast
from f.diff_between_chartsE[OF ‹d1 ∈ f.src.atlas› ‹d2 ∈ f.dest.atlas› iy iS fy]
obtain T where 1: "k-smooth_on T (apply_chart d2 ∘ f ∘ inv_chart d1)"
and T: "d1 iy ∈ T" "open T"
and T_def: "T = codomain d1 ∩ inv_chart d1 -` (f.src.carrier ∩ f -` domain d2)"
by auto
have gf: "g (f (iy)) ∈ domain c3" using sub_c3 iy by auto
from iS f.defined have "f (iy) ∈ f.dest.carrier" by auto
from g.diff_between_chartsE[OF ‹d2 ∈ f.dest.atlas› ‹c3 ∈ g.dest.atlas› fy this gf]
obtain X where 2: "k-smooth_on X (apply_chart c3 ∘ g ∘ inv_chart d2)"
and X: "apply_chart d2 (f iy) ∈ X" "open X"
and X_def: "X = codomain d2 ∩ inv_chart d2 -` (f.dest.carrier ∩ g -` domain c3)"
by auto
have "y ∈ T" using T by (simp add: y_def)
moreover
note ‹open T›
moreover
have "k-smooth_on T (apply_chart c3 ∘ g ∘ inv_chart d2 ∘ (apply_chart d2 ∘ f ∘ inv_chart d1))"
using 2 1 ‹open T› ‹open X›
by (rule smooth_on_compose) (use sub_c3 f.defined in ‹force simp: T_def X_def›)
then have "k-smooth_on T (apply_chart c3 ∘ (g ∘ f) ∘ inv_chart d1)"
using ‹open T›
by (rule smooth_on_cong) (auto simp: T_def)
ultimately show "∃T. y ∈ T ∧ open T ∧ k-smooth_on T (apply_chart c3 ∘ (g ∘ f) ∘ inv_chart d1)"
by metis
qed
ultimately show "∃c1∈f.src.atlas.
∃c2∈g.dest.atlas.
x ∈ domain c1 ∧
(g ∘ f) ` domain c1 ⊆ domain c2 ∧ k-smooth_on (codomain c1) (apply_chart c2 ∘ (g ∘ f) ∘ inv_chart c1)"
by blast
qed
qed
context diff begin
lemma diff_submanifold: "diff k (src.charts_submanifold S) charts2 f"
if "open S"
proof -
interpret submanifold charts1 k S
by unfold_locales (auto intro!: that)
show ?thesis
unfolding that src.charts_submanifold_def[symmetric]
proof unfold_locales
fix x assume "x ∈ sub.carrier"
then have "x ∈ src.carrier" "x ∈ S" using that
by auto
from diffE[OF ‹x ∈ src.carrier›] obtain c1 c2 where c1c2:
"c1 ∈ src.atlas" "c2 ∈ dest.atlas" "x ∈ domain c1"
"f ` domain c1 ⊆ domain c2" "k-smooth_on (codomain c1) (apply_chart c2 ∘ f ∘ inv_chart c1)"
by auto
have rc1: "restrict_chart S c1 ∈ sub.atlas"
using c1c2(1) by (rule submanifold_atlasI)
show "∃c1∈sub.atlas. ∃c2∈dest.atlas. x ∈ domain c1 ∧ f ` domain c1 ⊆ domain c2 ∧
k-smooth_on (codomain c1) (c2 ∘ f ∘ inv_chart c1)"
using rc1
apply (rule rev_bexI)
using c1c2(2)
apply (rule rev_bexI)
using c1c2 ‹x ∈ S› ‹open S›
by (auto simp: smooth_on_subset)
qed
qed
lemma diff_submanifold2: "diff k charts1 (dest.charts_submanifold S) f"
if "open S" "f ` src.carrier ⊆ S"
proof -
interpret submanifold charts2 k S
by unfold_locales (auto intro!: that)
show ?thesis
unfolding that src.charts_submanifold_def[symmetric]
proof unfold_locales
fix x assume "x ∈ src.carrier"
from diffE[OF this]
obtain c1 c2 where c1c2:
"c1 ∈ src.atlas" "c2 ∈ dest.atlas" "x ∈ domain c1"
"f ` domain c1 ⊆ domain c2" "k-smooth_on (codomain c1) (apply_chart c2 ∘ f ∘ inv_chart c1)"
by auto
have r: "restrict_chart S c2 ∈ sub.atlas"
using c1c2(2) by (rule submanifold_atlasI)
show "∃c1∈src.atlas. ∃c2∈sub.atlas. x ∈ domain c1 ∧ f ` domain c1 ⊆ domain c2 ∧
k-smooth_on (codomain c1) (c2 ∘ f ∘ inv_chart c1)"
using c1c2(1)
apply (rule rev_bexI)
using r
apply (rule rev_bexI)
using c1c2 ‹open S› that(2)
by (auto simp: smooth_on_subset)
qed
qed
end
context c_manifolds begin
lemma diff_localI: "diff k charts1 charts2 f"
if "⋀x. x ∈ src.carrier ⟹ diff k (src.charts_submanifold (U x)) charts2 f"
"⋀x. x ∈ src.carrier ⟹ open (U x)"
"⋀x. x ∈ src.carrier ⟹ x ∈ (U x)"
proof unfold_locales
fix x assume x: "x ∈ src.carrier"
have open_U[simp]: "open (U x)" by (rule that) fact
have in_U[simp]: "x ∈ U x" by (rule that) fact
interpret submanifold charts1 k "U x"
using that x
by unfold_locales auto
from x interpret l: diff k "src.charts_submanifold (U x)" charts2 f
by (rule that)
have "x ∈ sub.carrier" using x
by auto
from l.diffE[OF this] obtain c1 c2 where c1c2: "c1 ∈ sub.atlas"
"c2 ∈ dest.atlas" "x ∈ domain c1" "f ` domain c1 ⊆ domain c2"
"k-smooth_on (codomain c1) (apply_chart c2 ∘ f ∘ inv_chart c1)"
by auto
have "c1 ∈ src.atlas"
by (rule submanifold_atlasE[OF c1c2(1)])
show "∃c1∈src.atlas. ∃c2∈dest.atlas. x ∈ domain c1 ∧ f ` domain c1 ⊆ domain c2 ∧
k-smooth_on (codomain c1) (apply_chart c2 ∘ f ∘ inv_chart c1)"
by (intro bexI[where x=c1] bexI[where x=c2] conjI ‹c1 ∈ src.atlas› ‹c2 ∈ dest.atlas› c1c2)
qed
lemma diff_open_coverI: "diff k charts1 charts2 f"
if diff: "⋀u. u ∈ U ⟹ diff k (src.charts_submanifold u) charts2 f"
and op: "⋀u. u ∈ U ⟹ open u"
and cover: "src.carrier ⊆ ⋃U"
proof -
obtain V where V: "∀x∈src.carrier. V x ∈ U ∧ x ∈ V x"
apply (atomize_elim, rule bchoice)
using cover
by blast
have "diff k (src.charts_submanifold (V x)) charts2 f"
"open (V x)"
"x ∈ V x"
if "x ∈ src.carrier" for x
using that diff op V
by auto
then show ?thesis
by (rule diff_localI)
qed
lemma diff_open_Un: "diff k charts1 charts2 f"
if "diff k (src.charts_submanifold U) charts2 f"
"diff k (src.charts_submanifold V) charts2 f"
and "open U" "open V" "src.carrier ⊆ U ∪ V"
using diff_open_coverI[of "{U, V}" f] that
by auto
end
context c_manifold begin
sublocale self: c_manifolds k charts charts
by unfold_locales
lemma diff_id: "diff k charts charts (λx. x)"
by (force simp: self.diff_iff elim!: atlasE intro: smooth_on_cong)
lemma c_manifold_order_le: "c_manifold charts l" if "l ≤ k"
by unfold_locales (use pairwise_compat smooth_compat_le[OF _ ‹l ≤ k›] in blast)
lemma in_atlas_order_le: "c ∈ c_manifold.atlas charts l" if "l ≤ k" "c ∈ atlas"
proof -
interpret l: c_manifold charts l
using ‹l ≤ k›
by (rule c_manifold_order_le)
show ?thesis
using that
by (auto simp: l.atlas_def atlas_def smooth_compat_le[OF _ ‹l ≤ k›])
qed
end
context c_manifolds begin
lemma c_manifolds_order_le: "c_manifolds l charts1 charts2" if "l ≤ k"
by unfold_locales
(use src.pairwise_compat dest.pairwise_compat smooth_compat_le[OF _ that] in blast)+
end
context diff begin
lemma diff_order_le: "diff l charts1 charts2 f" if "l ≤ k"
proof -
interpret l: c_manifolds l charts1 charts2
by (rule c_manifolds_order_le) fact
show "diff l charts1 charts2 f"
using diff_axioms
unfolding l.diff_iff diff_iff
by (auto dest!: smooth_on_le[OF _ that] src.in_atlas_order_le[OF that]
dest.in_atlas_order_le[OF that] dest!: bspec)
qed
end
subsection ‹Differentiable functions›
lift_definition chart_eucl::"('a::euclidean_space, 'a) chart" is
"(UNIV, UNIV, λx. x, λx. x)"
by (auto simp: homeomorphism_def)
abbreviation "charts_eucl ≡ {chart_eucl}"
lemma chart_eucl_simps[simp]:
"domain chart_eucl = UNIV"
"codomain chart_eucl = UNIV"
"apply_chart chart_eucl = (λx. x)"
"inv_chart chart_eucl = (λx. x)"
by (transfer, simp)+
locale diff_fun = diff k charts charts_eucl f
for k charts and f::"'a::{t2_space,second_countable_topology} ⇒ 'b::euclidean_space"
lemma diff_fun_compose:
"diff_fun k M1 (g ∘ f)"
if "diff k M1 M2 f" "diff_fun k M2 g"
unfolding diff_fun_def
by (rule diff_compose[OF that[unfolded diff_fun_def]])
lemma c1_manifold_atlas_eucl: "c_manifold charts_eucl k"
by unfold_locales (auto simp: smooth_compat_refl)
interpretation manifold_eucl: c_manifold "charts_eucl" k
by (rule c1_manifold_atlas_eucl)
lemma chart_eucl_in_atlas[intro,simp]: "chart_eucl ∈ manifold_eucl.atlas k"
using manifold_eucl.charts_subset_atlas
by auto
lemma apply_chart_smooth_on:
"k-smooth_on (domain c) c" if "c ∈ manifold_eucl.atlas k"
proof -
have "k-smooth_compat c chart_eucl"
using that
by (auto intro!: manifold_eucl.atlas_is_atlas)
from smooth_compat_D2[OF this]
show ?thesis
by (auto simp: o_def)
qed
lemma inv_chart_smooth_on: "k-smooth_on (codomain c) (inv_chart c)" if "c ∈ manifold_eucl.atlas k"
proof -
have "k-smooth_compat c chart_eucl"
using that
by (auto intro!: manifold_eucl.atlas_is_atlas)
from smooth_compat_D1[OF this]
show ?thesis
by (auto simp: o_def image_domain_eq)
qed
lemma smooth_on_chart_inv:
fixes c::"('a::euclidean_space, 'a) chart"
assumes "k-smooth_on X (apply_chart c ∘ f)"
assumes "continuous_on X f"
assumes "c ∈ manifold_eucl.atlas k" "open X" "f ` X ⊆ domain c"
shows "k-smooth_on X f"
proof -
have "k-smooth_on X (inv_chart c ∘ (apply_chart c ∘ f))"
using assms
by (auto intro!: smooth_on_compose inv_chart_smooth_on)
with assms show ?thesis
by (force intro!: open_continuous_vimage intro: smooth_on_cong)
qed
lemma smooth_on_chart_inv2:
fixes c::"('a::euclidean_space, 'a) chart"
assumes "k-smooth_on (c ` X) (f o inv_chart c)"
assumes "c ∈ manifold_eucl.atlas k" "open X" "X ⊆ domain c"
shows "k-smooth_on X f"
proof -
have "k-smooth_on X ((f o inv_chart c) ∘ apply_chart c)"
using assms(1) apply_chart_smooth_on
by (rule smooth_on_compose2) (auto simp: assms)
with assms show ?thesis
by (force intro!: open_continuous_vimage intro: smooth_on_cong)
qed
context diff_fun begin
lemma diff_fun_order_le: "diff_fun l charts f" if "l ≤ k"
using diff_order_le[OF that]
by (simp add: diff_fun_def)
end
subsection ‹Diffeormorphism›
locale diffeomorphism = diff k charts1 charts2 f + inv: diff k charts2 charts1 f'
for k charts1 charts2 f f' +
assumes f_inv[simp]: "⋀x. x ∈ src.carrier ⟹ f' (f x) = x"
and f'_inv[simp]: "⋀y. y ∈ dest.carrier ⟹ f (f' y) = y"
context c_manifold begin
sublocale manifold_eucl: c_manifolds k charts "{chart_eucl}"
rewrites "diff k charts {chart_eucl} = diff_fun k charts"
by unfold_locales (simp add: diff_fun_def[abs_def])
lemma diff_funI:
"diff_fun k charts f"
if "(⋀x. x∈carrier ⟹ ∃c1∈atlas. x ∈ domain c1 ∧ (k-smooth_on (codomain c1) (f ∘ inv_chart c1)))"
unfolding manifold_eucl.diff_iff
by (auto dest!: that intro!: bexI[where x=chart_eucl] simp: o_def)
end
lemma (in diff) diff_cong: "diff k charts1 charts2 g" if "⋀x. x ∈ src.carrier ⟹ f x = g x"
unfolding diff_iff
proof (rule ballI)
fix x assume "x ∈ src.carrier"
from diff_axioms[unfolded diff_iff, rule_format, OF this]
obtain c1::"('a, 'e) chart" and c2::"('b, 'f) chart" where
"c1∈src.atlas" "c2 ∈ dest.atlas"
"x ∈ domain c1" "f ` domain c1 ⊆ domain c2" "k-smooth_on (codomain c1) (apply_chart c2 ∘ f ∘ inv_chart c1)"
by auto
then show "∃c1∈src.atlas. ∃c2∈dest.atlas.
x ∈ domain c1 ∧ g ` domain c1 ⊆ domain c2 ∧ k-smooth_on (codomain c1) (apply_chart c2 ∘ g ∘ inv_chart c1)"
using that
by (intro bexI[where x=c1] bexI[where x=c2]) (auto simp: intro: smooth_on_cong)
qed
context diff_fun begin
lemma diff_fun_cong: "diff_fun k charts g" if "⋀x. x ∈ src.carrier ⟹ f x = g x"
using diff_cong[OF that]
by (auto simp: diff_fun_def)
lemma diff_funD:
"∃c1∈src.atlas. x ∈ domain c1 ∧ (k-smooth_on (codomain c1) (f ∘ inv_chart c1))"
if x: "x ∈ src.carrier"
proof -
from diff_fun_axioms[unfolded src.manifold_eucl.diff_iff, rule_format, OF x]
obtain c1 c2 where a: "c1 ∈ src.atlas" "c2 ∈ manifold_eucl.atlas k" "x ∈ domain c1" "f ` domain c1 ⊆ domain c2"
and s: "k-smooth_on (codomain c1) (apply_chart c2 ∘ (f ∘ inv_chart c1))"
by (auto simp: o_assoc)
from smooth_on_chart_inv[OF s] a
show ?thesis
by (force intro!: bexI[where x=c1] a continuous_intros)
qed
lemma diff_funE:
assumes "x ∈ src.carrier"
obtains c1 where
"c1∈src.atlas" "x ∈ domain c1" "k-smooth_on (codomain c1) (f ∘ inv_chart c1)"
using diff_funD[OF assms]
by blast
lemma diff_fun_between_chartsD:
assumes "c ∈ src.atlas" "x ∈ domain c"
shows "k-smooth_on (codomain c) (f ∘ inv_chart c)"
proof -
have "x ∈ src.carrier" "f x ∈ domain chart_eucl" using assms by auto
from diff_between_chartsE[OF assms(1) chart_eucl_in_atlas assms(2) this]
obtain X where s: "k-smooth_on X (f ∘ inv_chart c)"
and X_def: "X = codomain c ∩ inv_chart c -` (src.carrier ∩ f -` UNIV)"
by (auto simp: o_def)
then have X_def: "X = codomain c" using assms
by (auto simp: X_def)
with s show ?thesis by auto
qed
lemma diff_fun_submanifold: "diff_fun k (src.charts_submanifold S) f"
if [simp]: "open S"
using diff_submanifold
unfolding diff_fun_def
by simp
end
context c_manifold begin
lemma diff_fun_zero: "diff_fun k charts 0"
by (rule diff_funI) (auto simp: o_def elim!: carrierE)
lemma diff_fun_const: "diff_fun k charts (λx. c)"
by (rule diff_funI) (auto simp: o_def elim!: carrierE)
lemma diff_fun_add: "diff_fun k charts (a + b)" if "diff_fun k charts a" "diff_fun k charts b"
proof (rule diff_funI)
fix x
assume x: "x ∈ carrier"
interpret a: diff_fun k charts a by fact
interpret b: diff_fun k charts b by fact
from a.diff_funE[OF x]
obtain c where ca: "c ∈ atlas" "x ∈ domain c" "k-smooth_on (codomain c) (a ∘ inv_chart c)"
by blast
show "∃c1∈atlas. x ∈ domain c1 ∧ k-smooth_on (codomain c1) (a + b ∘ inv_chart c1)"
using ca
by (auto intro!: bexI[where x=c] ca smooth_on_add_fun simp: plus_compose b.diff_fun_between_chartsD)
qed
lemma diff_fun_sum: "diff_fun k charts (λx. ∑i∈S. f i x)" if "⋀i. i ∈ S ⟹ diff_fun k charts (f i)"
using that
apply (induction S rule: infinite_finite_induct)
subgoal by (simp add: diff_fun_const)
subgoal by (simp add: diff_fun_const)
subgoal by (simp add: diff_fun_add[unfolded plus_fun_def])
done
lemma diff_fun_scaleR: "diff_fun k charts (λx. a x *⇩R b x)"
if "diff_fun k charts a" "diff_fun k charts b"
proof (rule diff_funI)
fix x
assume x: "x ∈ carrier"
interpret a: diff_fun k charts a by fact
interpret b: diff_fun k charts b by fact
from a.diff_funE[OF x]
obtain c where ca: "c ∈ atlas" "x ∈ domain c" "k-smooth_on (codomain c) (a ∘ inv_chart c)"
by blast
have *: "(λx. a x *⇩R b x) ∘ inv_chart c = (λx. (a o inv_chart c) x *⇩R (b o inv_chart c) x)"
by auto
show "∃c1∈atlas. x ∈ domain c1 ∧ k-smooth_on (codomain c1) ((λx. a x *⇩R b x) ∘ inv_chart c1)"
using ca
by (auto intro!: bexI[where x=c] smooth_on_scaleR
simp: mult_compose b.diff_fun_between_chartsD[unfolded o_def] * o_def)
qed
lemma diff_fun_scaleR_left: "diff_fun k charts (c *⇩R b)"
if "diff_fun k charts b"
by (auto simp: scaleR_fun_def intro!: diff_fun_scaleR that diff_fun_const)
lemma diff_fun_times: "diff_fun k charts (a * b)" if "diff_fun k charts a" "diff_fun k charts b"
for a b::"_ ⇒ _::real_normed_algebra"
proof (rule diff_funI)
fix x
assume x: "x ∈ carrier"
interpret a: diff_fun k charts a by fact
interpret b: diff_fun k charts b by fact
from a.diff_funE[OF x]
obtain c where ca: "c ∈ atlas" "x ∈ domain c" "k-smooth_on (codomain c) (a ∘ inv_chart c)"
by blast
show "∃c1∈atlas. x ∈ domain c1 ∧ k-smooth_on (codomain c1) (a * b ∘ inv_chart c1)"
using ca
by (auto intro!: bexI[where x=c] ca smooth_on_times_fun simp: mult_compose b.diff_fun_between_chartsD)
qed
lemma diff_fun_divide: "diff_fun k charts (λx. a x / b x)"
if "diff_fun k charts a" "diff_fun k charts b"
and nz: "⋀x. x ∈ carrier ⟹ b x ≠ 0"
for a b::"_ ⇒ _::real_normed_field"
proof (rule diff_funI)
fix x
assume x: "x ∈ carrier"
interpret a: diff_fun k charts a by fact
interpret b: diff_fun k charts b by fact
from a.diff_funE[OF x]
obtain c where ca: "c ∈ atlas" "x ∈ domain c" "k-smooth_on (codomain c) (a ∘ inv_chart c)"
by blast
show "∃c1∈atlas. x ∈ domain c1 ∧ k-smooth_on (codomain c1) ((λx. a x / b x) ∘ inv_chart c1)"
using ca nz
by (auto intro!: bexI[where x=c] ca smooth_on_mult smooth_on_inverse
dest: b.diff_fun_between_chartsD
simp: mult_compose o_def
divide_inverse)
qed
lemma subspace_Collect_diff_fun:
"subspace (Collect (diff_fun k charts))"
by (auto simp: subspace_def diff_fun_zero diff_fun_add diff_fun_scaleR_left)
end
lemma manifold_eucl_carrier[simp]: "manifold_eucl.carrier = UNIV"
by (simp add: manifold_eucl.carrier_def)
lemma diff_fun_charts_euclD: "k-smooth_on UNIV g" if "diff_fun k charts_eucl g"
proof (rule smooth_on_open_subsetsI)
fix x::'a
interpret diff_fun k charts_eucl g by fact
have "x ∈ manifold_eucl.carrier" by simp
from diff_funE[OF this] obtain c1
where c: "c1 ∈ manifold_eucl.atlas k" "x ∈ domain c1"
"k-smooth_on (codomain c1) (g ∘ inv_chart c1)" by auto
have "k-smooth_on (domain c1) g"
apply (rule smooth_on_chart_inv2)
apply (rule smooth_on_subset)
apply (rule c)
using c by auto
then show "∃T. x ∈ T ∧ open T ∧ k-smooth_on T g"
using c by auto
qed
lemma diff_fun_charts_euclI: "diff_fun k charts_eucl g" if "k-smooth_on UNIV g"
apply (rule manifold_eucl.diff_funI)
apply auto
apply (rule bexI[where x=chart_eucl])
using that
by (auto simp: o_def)
end