Theory Partition_Of_Unity
section ‹Partitions Of Unity›
theory Partition_Of_Unity
imports Bump_Function Differentiable_Manifold
begin
subsection ‹Regular cover›
context c_manifold begin
text ‹A cover is regular if, in addition to being countable and locally finite,
the codomain of every chart is the open ball of radius 3, such that the
inverse image of open balls of radius 1 also cover the manifold.›
definition "regular_cover I (ψ::'i⇒('a, 'b) chart) ⟷
countable I ∧
carrier = (⋃i∈I. domain (ψ i)) ∧
locally_finite_on carrier I (domain o ψ) ∧
(∀i∈I. codomain (ψ i) = ball 0 3) ∧
carrier = (⋃i∈I. inv_chart (ψ i) ` ball 0 1)"
text ‹Every covering has a refinement that is a regular cover.›
lemma reguler_refinementE:
fixes 𝒳::"'i ⇒ 'a set"
assumes cover: "carrier ⊆ (⋃i∈I. 𝒳 i)" and open_cover: "⋀i. i ∈ I ⟹ open (𝒳 i)"
obtains N::"nat set" and ψ::"nat ⇒ ('a, 'b) chart"
where "⋀i. i ∈ N ⟹ ψ i ∈ atlas" "(domain o ψ) ` N refines 𝒳 ` I" "regular_cover N ψ"
proof -
from precompact_locally_finite_open_coverE
obtain V::"nat⇒_" where V:
"carrier = (⋃i. V i)"
"⋀i. open (V i)"
"⋀i. compact (closure (V i))"
"⋀i. closure (V i) ⊆ carrier"
"locally_finite_on carrier UNIV V"
by auto
define intersecting where "intersecting v = {i. V i ∩ v ≠ {}}" for v
have intersecting_closure: "intersecting (closure x) = intersecting x" for x
using open_Int_closure_eq_empty[OF V(2), of _ x]
by (auto simp: intersecting_def)
from locally_finite_compactD[OF V(5) V(3) V(4)]
have "finite (intersecting (closure (V x)))" for x
by (simp add: intersecting_def)
then have finite_intersecting: "finite (intersecting (V x))" for x
by (simp add: intersecting_closure)
have "∃ψ::('a, 'b) chart.
ψ ∈ atlas ∧
codomain ψ = ball 0 3 ∧
(∃c∈I. domain ψ ⊆ 𝒳 c) ∧
(∀j. p ∈ V j ⟶ domain ψ ⊆ V j) ∧
p ∈ domain ψ ∧
ψ p = 0"
if "p ∈ carrier" for p
proof -
from cover that open_cover obtain c where c: "p ∈ 𝒳 c" "open (𝒳 c)" "c ∈ I"
by force
define VS where "VS = {U. p ∈ V U}"
have open_VS: "⋀T. T ∈ VS ⟹ open (V T)"
by (auto simp: VS_def V)
from locally_finite_onD[OF V(5) that]
have "finite VS" by (simp add: VS_def)
from atlasE[OF that] obtain ψ' where ψ': "ψ' ∈ atlas" "p ∈ domain ψ'" .
define W where "W = (⋂i∈VS. V i) ∩ domain ψ' ∩ 𝒳 c"
have "open W"
by (force simp: W_def open_VS intro!: c ‹finite VS›)
have "p ∈ W" by (auto simp: W_def c ψ' VS_def)
have "W ⊆ carrier"
using ψ'
by (auto simp: W_def)
have "0 < (3::real)" by auto
from open_centered_ball_chartE[OF ‹p ∈ W› ‹open W› ‹W ⊆ carrier› ‹0 < 3›]
obtain ψ where ψ: "ψ ∈ atlas" "p ∈ domain ψ" "ψ p = 0" "domain ψ ⊆ W" "codomain ψ = ball 0 3"
by auto
moreover have "∃x∈I. domain ψ ⊆ 𝒳 x"
using c ψ by (auto simp: W_def)
moreover have "p ∈ V j ⟹ domain ψ ⊆ V j" for j
using c ψ by (auto simp: W_def VS_def)
ultimately show ?thesis
by (intro exI[where x=ψ]) auto
qed
then have "∀p2 ∈ carrier.
∃ψ::('a, 'b) chart. ψ ∈ atlas ∧ codomain ψ = ball 0 3 ∧
(∃c∈I. domain ψ ⊆ 𝒳 c) ∧ (∀j. p2 ∈ V j ⟶ domain ψ ⊆ V j) ∧ p2 ∈ domain ψ ∧
apply_chart ψ p2 = 0"
by blast
then obtain ψ::"'a ⇒ ('a, 'b) chart" where ψ:
"⋀p. p ∈ carrier ⟹ codomain (ψ p) = ball 0 3"
"⋀p. p ∈ carrier ⟹ (∃c∈I. domain (ψ p) ⊆ 𝒳 c)"
"⋀p j. p ∈ V j ⟹ domain (ψ p) ⊆ V j"
"⋀p j. p ∈ carrier ⟹ p ∈ domain (ψ p)"
"⋀p. p ∈ carrier ⟹ (ψ p) p = 0"
"⋀p. p ∈ carrier ⟹ ψ p ∈ atlas"
unfolding bchoice_iff
apply atomize_elim
apply auto
subgoal for f
apply (rule exI[where x=f])
using V
by auto
done
define U where "U p = inv_chart (ψ p) ` ball 0 1" for p
have U_open: "open (U p)" if "p ∈ carrier" for p
using that ψ
by (auto simp: U_def)
have U_subset_domain: "x ∈ U p ⟹ x ∈ domain (ψ p)" if "p ∈ carrier" for x p
using ψ(1) that
by (auto simp: U_def)
have "∃M. M ⊆ closure (V l) ∧ finite M ∧ closure (V l) ⊆ ⋃(U ` M)" for l
proof -
have clcover: "closure (V l) ⊆ ⋃(U ` closure (V l))"
using ψ
apply (auto simp: U_def)
apply (rule bexI)
prefer 2 apply assumption
apply (rule image_eqI)
apply (rule inv_chart_inverse[symmetric])
apply (rule ψ)
apply auto
using V(4) apply force
by (metis V(4) less_irrefl norm_numeral norm_one norm_zero one_less_numeral_iff subsetCE
zero_less_norm_iff zero_neq_numeral)
have "B ∈ U ` closure (V l) ⟹ open B" for B
using V(4) by (auto intro!: U_open)
from compactE[OF V(3) clcover this]
obtain Um where Um: "Um ⊆ U ` closure (V l)" "finite Um" "closure (V l) ⊆ ⋃Um"
by auto
from Um(1) have "∀t∈Um. ∃p∈closure (V l). t = U p"
by auto
then obtain p_of where p_of: "⋀t. t ∈ Um ⟹ p_of t ∈ closure (V l)"
"⋀t. t ∈ Um ⟹ t = U (p_of t)"
by metis
have "p_of ` Um ⊆ closure (V l)"
using p_of
by auto
moreover have "finite (p_of ` Um)" using ‹finite Um› by auto
moreover have "closure (V l) ⊆ ⋃(U ` p_of ` Um)"
using Um p_of by auto
ultimately show ?thesis by blast
qed
then obtain M' where M': "⋀l. M' l ⊆ closure (V l)" "⋀l. finite (M' l)" "⋀l. closure (V l) ⊆ ⋃(U ` M' l)"
by metis
define M where "M v = M' (LEAST l. V l = v)" for v
have V_Least: "V (LEAST la. V la = V l) = V l" for l
by (rule LeastI_ex) auto
have M: "M (V l) ⊆ closure (V l)" "finite (M v)" "closure (V l) ⊆ ⋃(U ` M (V l))" for v l
subgoal
unfolding M_def
apply (rule order_trans)
apply (rule M')
by (auto simp: V_Least)
subgoal using M' by (auto simp: M_def)
subgoal
unfolding M_def
apply (subst V_Least[symmetric])
by (rule M')
done
from M(1) V(4) have M_carrier: "x ∈ M (V l) ⟹ x ∈ carrier" for x l by auto
have "countable (⋃l. M (V l))"
using M(2) by (auto simp: countable_finite)
from countableE_bij[OF this]
obtain m and N::"nat set" where n: "bij_betw m N (⋃l. M (V l))" .
define m' where "m' = the_inv_into N m"
have m_inverse[simp]: "⋀i. i ∈ N ⟹ m' (m i) = i"
and m'_inverse[simp]: "⋀x l. x ∈ M (V l) ⟹ m (m' x) = x"
using n
by (force simp: bij_betw_def m'_def the_inv_into_f_f)+
have m_in: "m i ∈ (⋃l. M (V l))" if "i ∈ N" for i
using n that
by (auto dest!: bij_betwE)
have m'_in: "m' x ∈ N" if "x ∈ M (V l)" for x l
using that n
by (auto simp: m'_def bij_betw_def intro!: the_inv_into_into)
from m_in have m_in_carrier: "m i ∈ carrier" if "i ∈ N" for i
using that M_carrier
by auto
then have "⋀i. i ∈ N ⟹ ψ (m i) ∈ atlas"
by (rule ψ(6))
moreover
have "(domain o (λi. (ψ (m i)))) ` N refines 𝒳 ` I"
by (auto simp: refines_def dest!: m_in_carrier ψ(2))
moreover
have "regular_cover N (λi. ψ (m i))"
proof -
have "countable N" by simp
moreover
have carrier_subset: "carrier ⊆ (⋃i ∈ N. inv_chart (ψ (m i)) ` ball 0 1)"
unfolding V
proof safe
fix x i
assume "x ∈ V i"
with M obtain p where p: "p ∈ M (V i)" "x ∈ U p" by blast
from p show "x ∈ (⋃i∈N. inv_chart (ψ (m i)) ` ball 0 1)"
by (auto simp: U_def intro!: bexI[where x="m' p"] m'_in)
qed
have carrier_eq_W: "carrier = (⋃i∈N. domain (ψ (m i)))" (is "_ = ?W")
proof (rule antisym)
note carrier_subset
also have "… ⊆ ?W"
using U_subset_domain ψ(1) M_carrier m_in
by (force simp: V)
finally show "carrier ⊆ ?W"
by auto
show "?W ⊆ carrier" using M_carrier ψ(6)
by (auto dest!: m_in)
qed
moreover have "locally_finite_on carrier N (λi. domain (ψ (m i)))"
proof (rule locally_finite_on_open_coverI)
show "open (domain (ψ (m i)))" for i by auto
show "carrier ⊆ (⋃i∈N. domain (ψ (m i)))"
unfolding carrier_eq_W by auto
fix ki
assume "ki ∈ N"
from m_in[OF this]
obtain k where k: "m ki ∈ M (V k)" by auto
have pkc: "m ki ∈ closure (V k)"
using k M(1) by force
obtain j where j: "m ki ∈ V j"
using M_carrier[of "m ki" k] V(1) k by force
have kj: "V k ∩ V j ≠ {}"
using open_Int_closure_eq_empty[OF V(2)]
using pkc j by auto
then have jinterk: "j ∈ intersecting (V k)" by (auto simp: intersecting_def)
have 1: "compact (closure (V k))" by (rule V)
have 2: "closure (V k) ⊆ ⋃(range V)" unfolding V(1)[symmetric] by (rule V)
have 3: "B ∈ range V ⟹ open B" for B by (auto simp: V)
from compactE[OF 1 2 3]
obtain Vj where "Vj ⊆ range V" "finite Vj" "closure (V k) ⊆ ⋃Vj" by auto
then obtain J where "finite J" "closure (V k) ⊆ ⋃(V ` J)"
apply atomize_elim
by (metis finite_subset_image)
{
fix ki' assume "ki' ∈ N"
assume H: "domain (ψ (m ki')) ∩ domain (ψ (m ki)) ≠ {}"
obtain k' where ki': "m ki' ∈ M (V k')" using m_in[OF ‹ki' ∈ N›] by auto
have k': "domain (ψ (m ki')) ∩ domain (ψ (m ki)) ≠ {}" "m ki' ∈ M (V k')"
using ki' H by auto
have pkc': "m ki' ∈ closure (V k')"
using k' M(1) by force
obtain j' where j': "m ki' ∈ V j'"
using M_carrier V(1) k' by force
have kj': "(V k') ∩ V j' ≠ {}"
using open_Int_closure_eq_empty[OF V(2)]
using pkc' j' by auto
then have j'interk': "k' ∈ intersecting (V j')" by (auto simp: intersecting_def)
have j'interj: "j' ∈ intersecting (V j)"
using k' ψ(3)[OF j'] ψ(3)[OF j]
by (auto simp: intersecting_def)
have "k' ∈ ⋃(intersecting ` V ` ⋃(intersecting ` V ` intersecting (V k)))"
using jinterk j'interk' j'interj
by blast
then have "m ki' ∈ ⋃((λx. M (V x)) ` ⋃(intersecting ` V ` ⋃(intersecting ` V ` intersecting (V k))))"
using ki'
by auto
from m_inverse[symmetric] this have "ki' ∈ m' ` ⋃((λx. M (V x)) ` ⋃(intersecting ` V ` ⋃(intersecting ` V ` intersecting (V k))))"
by (rule image_eqI) fact
} note * = this
show "finite {i ∈ N. domain (ψ (m i)) ∩ domain (ψ (m ki)) ≠ {}}"
apply (rule finite_subset[where B="m' ` ⋃((λx. M (V x)) ` ⋃(intersecting ` V ` ⋃(intersecting ` V ` intersecting (V k))))"])
apply clarsimp
subgoal by (drule *, assumption, force)
using finite_intersecting intersecting_def M by auto
qed
moreover have "(∀i ∈ N. codomain (ψ (m i)) = ball 0 3)"
using ψ(1) M_carrier m_in
by force
moreover have "carrier = (⋃i ∈ N. inv_chart (ψ (m i)) ` ball 0 1)"
proof (rule antisym)
show "(⋃i∈N. inv_chart (ψ (m i)) ` ball 0 1) ⊆ carrier"
using ψ(6)[OF M_carrier] M_carrier m_in
by (force simp: ψ(1))
qed (rule carrier_subset)
ultimately show ?thesis
by (auto simp: regular_cover_def o_def)
qed
ultimately
show ?thesis ..
qed
lemma diff_apply_chart:
"diff k (charts_submanifold (domain ψ)) charts_eucl ψ" if "ψ ∈ atlas"
proof -
interpret submanifold charts k "domain ψ"
by unfold_locales auto
show ?thesis
proof (unfold_locales)
fix x assume x: "x ∈ sub.carrier"
show "∃c1∈sub.atlas.
∃c2∈manifold_eucl.dest.atlas.
x ∈ domain c1 ∧ ψ ` domain c1 ⊆ domain c2 ∧ k-smooth_on (codomain c1) (c2 ∘ ψ ∘ inv_chart c1)"
apply (rule bexI[where x = "restrict_chart (domain ψ) ψ"])
apply (rule bexI[where x = "chart_eucl"])
subgoal
proof safe
show "x ∈ domain (restrict_chart (domain ψ) ψ)"
using x ‹ψ ∈ atlas›
by auto
show "k-smooth_on (codomain (restrict_chart (domain ψ) ψ)) (chart_eucl ∘ ψ ∘ inv_chart (restrict_chart (domain ψ) ψ))"
apply (auto simp: o_def)
apply (rule smooth_on_cong[where g="λx. x"])
by (auto intro!: open_continuous_vimage' continuous_on_codomain)
qed simp
subgoal by auto
subgoal by (rule submanifold_atlasI) fact
done
qed
qed
lemma diff_inv_chart:
"diff k (manifold_eucl.charts_submanifold (codomain c)) charts (inv_chart c)" if "c ∈ atlas"
proof -
interpret submanifold charts_eucl k "codomain c"
by unfold_locales auto
show ?thesis
proof (unfold_locales)
fix x assume x: "x ∈ sub.carrier"
show "∃c1∈sub.atlas.
∃c2∈atlas.
x ∈ domain c1 ∧ inv_chart c ` domain c1 ⊆ domain c2 ∧
k-smooth_on (codomain c1) (c2 ∘ inv_chart c ∘ inv_chart c1)"
apply (rule bexI[where x = "restrict_chart (codomain c) chart_eucl"])
apply (rule bexI[where x = c])
subgoal
proof safe
show "x ∈ domain (restrict_chart (codomain c) chart_eucl)"
using x ‹c ∈ atlas›
by auto
show "k-smooth_on (codomain (restrict_chart (codomain c) chart_eucl)) (c ∘ inv_chart c ∘ inv_chart (restrict_chart (codomain c) chart_eucl))"
apply (auto simp: o_def)
apply (rule smooth_on_cong[where g="λx. x"])
by (auto intro!: open_continuous_vimage' continuous_on_codomain)
qed simp
subgoal using that by simp
subgoal
by (rule submanifold_atlasI) auto
done
qed
qed
lemma chart_inj_on [simp]:
fixes c :: "('a, 'b) chart"
assumes "x ∈ domain c" "y ∈ domain c"
shows "c x = c y ⟷ x = y"
proof -
have "inj_on c (domain c)" by (rule inj_on_apply_chart)
with assms show ?thesis by (auto simp: inj_on_def)
qed
subsection ‹Partition of unity by smooth functions›
text‹
Given any open cover ‹X› indexed by a set ‹A›, there exists a family of
smooth functions ‹φ› indexed by ‹A›, such that ‹0 ≤ φ ≤ 1›, the (closed) support
of each ‹φ i› is contained in ‹X i›, the supports are locally finite, and the
sum of ‹φ i› is the constant function ‹1›.›
theorem partitions_of_unityE:
fixes A::"'i set" and X::"'i ⇒ 'a set"
assumes "carrier ⊆ (⋃i∈A. X i)"
assumes "⋀i. i ∈ A ⟹ open (X i)"
obtains φ::"'i ⇒ 'a ⇒ real"
where "⋀i. i ∈ A ⟹ diff_fun k charts (φ i)"
and "⋀i x. i ∈ A ⟹ x ∈ carrier ⟹ 0 ≤ φ i x"
and "⋀i x. i ∈ A ⟹ x ∈ carrier ⟹ φ i x ≤ 1"
and "⋀x. x ∈ carrier ⟹ (∑i∈{i∈A. φ i x ≠ 0}. φ i x) = 1"
and "⋀i. i ∈ A ⟹ csupport_on carrier (φ i) ∩ carrier ⊆ X i"
and "locally_finite_on carrier A (λi. csupport_on carrier (φ i))"
proof -
from reguler_refinementE[OF assms]
obtain N and ψ::"nat ⇒ ('a, 'b) chart" where ψ:
"⋀i. i ∈ N ⟹ ψ i ∈ atlas"
"(domain o ψ) ` N refines X ` A"
"regular_cover N ψ" by blast
define U where "U i = inv_chart (ψ i) ` ball 0 1" for i::nat
define V where "V i = inv_chart (ψ i) ` ball 0 2" for i::nat
define W where "W i = inv_chart (ψ i) ` ball 0 3" for i::nat
from ‹regular_cover N ψ› have regular_cover:
"countable N"
"(⋃i∈N. U i) = (⋃i∈N. domain (ψ i))"
"locally_finite_on carrier N (domain ∘ ψ)"
"⋀i. i ∈ N ⟹ codomain (ψ i) = ball 0 3"
"carrier = (⋃i∈N. U i)"
by (auto simp: regular_cover_def U_def)
have open_W: "open (W i)" if "i ∈ N" for i
using that
by (auto simp: W_def regular_cover)
have W_eq: "domain (ψ i) = W i" if "i ∈ N" for i
using W_def regular_cover(4) that by force
have carrier_W: "carrier = (⋃i∈N. W i)"
by (auto simp: regular_cover W_eq)
have V_subset_W: "closure (V i) ⊆ W i" if "i ∈ N" for i
proof -
have "closure (V i) ⊆ closure (inv_chart (ψ i) ` cball 0 2)"
unfolding V_def
by (rule closure_mono) auto
also have "… = inv_chart (ψ i) ` cball 0 2"
apply (rule closure_closed)
apply (rule compact_imp_closed)
apply (rule compact_continuous_image)
by (auto intro!: continuous_intros simp: regular_cover that)
also have "… ⊆ W i"
by (auto simp: W_def)
finally show ?thesis .
qed
have carrier_V: "carrier = (⋃i∈N. V i)"
apply (rule antisym)
subgoal unfolding regular_cover(5) by (auto simp: U_def V_def)
subgoal unfolding carrier_W using V_subset_W by auto
done
define f where "f i x = (if x ∈ W i then H (ψ i x) else 0)" for i x
have f_simps: "x ∈ W i ⟹ f i x = H (ψ i x)"
"x ∉ W i ⟹ f i x = 0"
for i x
by (auto simp: f_def)
have f_eq_one: "f j y = 1" if "j ∈ N" "y ∈ U j" for j y
proof -
from that have "y ∈ W j" by (auto simp: U_def W_def)
from ‹y ∈ U j› have "norm (ψ j y) ≤ 1"
by (auto simp: U_def W_eq[symmetric] ‹j ∈ N› regular_cover(4))
then show ?thesis
by (auto simp: f_def ‹y ∈ W j› intro!: H_eq_one)
qed
have f_diff: "diff_fun k charts (f i)" if i: "i ∈ N" for i
proof (rule manifold_eucl.diff_open_Un, unfold diff_fun_def[symmetric])
note W_eq = W_eq[OF that]
have "W i ⊆ carrier"
unfolding W_eq[symmetric] regular_cover using that by auto
interpret W: submanifold _ _ "W i"
by unfold_locales (auto simp: open_W i)
have "diff_fun k (charts_submanifold (W i)) (H ∘ (ψ i))"
apply (rule diff_fun_compose[where ?M2.0 = charts_eucl])
apply (rule diff_apply_chart[of "ψ i", unfolded W_eq])
subgoal using ψ ‹i ∈ N› by auto
apply (rule diff_fun_charts_euclI)
by (rule H_smooth_on)
then show "diff_fun k (charts_submanifold (W i)) (f i)"
by (rule diff_fun.diff_fun_cong) (auto simp: f_def)
interpret V': submanifold _ _ "carrier - closure (V i)"
by unfold_locales auto
have "diff_fun k (charts_submanifold (carrier - closure (V i))) 0"
by (rule V'.sub.diff_fun_zero)
then show "diff_fun k (charts_submanifold (carrier - closure (V i))) (f i)"
apply (rule diff_fun.diff_fun_cong)
unfolding f_def
apply auto
apply (rule H_eq_zero)
unfolding V_def by (metis W_eq image_eqI in_closureI inv_chart_inverse)
show "open (W i)" by (auto simp: W_def regular_cover i)
show "open (carrier - closure (V i))" by auto
show "carrier ⊆ W i ∪ (carrier - closure (V i))"
using V_subset_W[OF i] by auto
qed
define g where "g ψ x = f ψ x / (∑i∈{j∈N. x ∈ W j}. f i x)" for ψ x
have "∀p∈carrier. ∃I. p ∈ I ∧ open I ∧finite {i ∈ N. W i ∩ I ≠ {}}"
(is "∀p∈carrier. ?P p")
proof (rule ballI)
fix p assume "p ∈ carrier"
from locally_finite_onE[OF regular_cover(3) this]
obtain I where "p ∈ I" "open I" "finite {i ∈ N. (domain ∘ ψ) i ∩ I ≠ {}}".
moreover have "{i ∈ N. (domain ∘ ψ) i ∩ I ≠ {}} = {i ∈ N. W i ∩ I ≠ {}}"
by (auto simp: W_eq)
ultimately show "?P p" by auto
qed
from bchoice[OF this] obtain I where I:
"⋀x. x ∈ carrier ⟹ x ∈ I x"
"⋀x. x ∈ carrier ⟹ open (I x)"
"⋀x. x ∈ carrier ⟹ finite {i ∈ N. W i ∩ I x ≠ {}}"
by blast
have subset_W: "{j ∈ N. y ∈ W j} ⊆ {j ∈ N. W j ∩ I x ≠ {}}" if "y ∈ I x" "x ∈ carrier" for x y
by (auto simp: that W_eq)
have finite_W: "finite {j ∈ N. y ∈ W j}" if "y ∈ carrier" for y
apply (rule finite_subset)
apply (rule subset_W[OF _ that])
apply (rule I[OF that])
apply (rule I[unfolded o_def, OF that])
done
have g: "diff_fun k charts (g i)" if i: "i ∈ N" for i
proof (rule manifold_eucl.diff_localI, unfold diff_fun_def[symmetric])
fix x assume x: "x ∈ carrier"
show "open (I x)" "x ∈ I x" using I x by auto
then interpret submanifold _ _ "I x"
by unfold_locales
interpret df: diff_fun k charts "f i" by (rule f_diff) fact
have "diff_fun k (charts_submanifold (I x)) (λy. f i y / (∑j∈{j∈N. W j ∩ I x ≠ {}}. f j y))"
apply (rule sub.diff_fun_divide)
subgoal
apply (rule df.diff_submanifold[folded diff_fun_def])
by (rule I) fact
subgoal
proof (rule sub.diff_fun_sum, clarsimp)
fix j assume "j ∈ N" "W j ∩ I x ≠ {}"
interpret df': diff_fun k charts "f j" by (rule f_diff) fact
show "diff_fun k (charts_submanifold (I x)) (f j)"
apply (rule df'.diff_fun_submanifold)
by (rule I) fact
qed
subgoal for y
apply (subst sum_nonneg_eq_0_iff)
subgoal using I(3)[OF x] by auto
subgoal using H_range by (auto simp: f_def)
subgoal
proof clarsimp
assume y: "y ∈ I x" "y ∈ carrier"
then obtain j where "j ∈ N" "y ∈ U j"
unfolding regular_cover(5) by auto
then have "y ∈ W j"
by (auto simp: U_def W_def)
moreover
have "W j ∩ I x ≠ {}"
using W_eq ‹j ∈ N› ‹open (I x)› ‹y ∈ W j› ‹y ∈ carrier› ‹y ∈ I x›
by auto
moreover
note f_eq_one[OF ‹j ∈ N› ‹y ∈ U j›]
ultimately show "∃xa. xa ∈ N ∧ W xa ∩ I x ≠ {} ∧ f xa y ≠ 0"
by (intro exI[where x=j]) (auto simp: ‹j ∈ N›)
qed
done
done
then show "diff_fun k (charts_submanifold (I x)) (g i)"
apply (rule diff_fun.diff_fun_cong)
unfolding g_def
apply simp
apply (rule disjI2)
apply (rule sum.mono_neutral_right)
subgoal using I[OF ‹x ∈ carrier›] unfolding o_def by simp
subgoal for y
apply (rule subset_W)
using carrier_submanifold I ‹x ∈ carrier› by auto
subgoal by (auto simp: f_def)
done
qed
have f_nonneg: "0 ≤ f i x" for i x
by (auto simp: f_def H_range intro!: sum_nonneg)
have U_sub_W: "x ∈ U i ⟹ x ∈ W i" for x i
by (auto simp: U_def W_def)
have sumf_pos: "(∑i∈{j ∈ N. x ∈ W j}. f i x) > 0" if "x ∈ carrier" for x
using that
apply (auto simp: regular_cover(5))
subgoal for i
apply (rule sum_pos2[where i=i])
using finite_W[OF that]
by (auto simp: f_nonneg f_eq_one U_sub_W )
done
have sumf_nonneg: "(∑i∈{j ∈ N. x ∈ W j}. f i x) ≥ 0" for x
by (auto simp: f_nonneg intro!: sum_nonneg)
have g_nonneg: "0 ≤ g i x" if "i ∈ N" "x ∈ carrier" for i x
by (auto simp: g_def intro!: divide_nonneg_nonneg sumf_nonneg f_nonneg)
have g_le_one: "g i x ≤ 1" if "i ∈ N" "x ∈ carrier" for i x
apply (auto simp add: g_def)
apply (cases "(∑i∈{j ∈ N. x ∈ W j}. f i x) = 0")
subgoal by simp
apply (subst divide_le_eq_1_pos)
subgoal using sumf_nonneg[of x] by auto
apply (cases "x ∈ W i")
subgoal
apply (rule member_le_sum)
subgoal using ‹i ∈ N› by simp
subgoal by (rule f_nonneg)
using sum.infinite by blast
subgoal by (simp add: f_simps sum_nonneg H_range)
done
have sum_g: "(∑i | i ∈ N ∧ x ∈ W i. g i x) = 1" if "x ∈ carrier" for x
unfolding g_def
apply (subst sum_divide_distrib[symmetric])
using sumf_pos[OF that]
by auto
have "∃a. ∀i∈N. W i ⊆ X (a i) ∧ a i ∈ A"
using ψ(2) by (intro bchoice) (auto simp: refines_def W_eq)
then obtain a where a: "⋀i. i ∈ N ⟹ W i ⊆ X (a i)" "⋀i. i ∈ N ⟹ a i ∈ A"
by force
define φ where "φ α x = (∑i | i ∈ N ∧ a i = α ∧ x ∈ W i. g i x)" for α x
have "diff_fun k charts (φ α)" if "α ∈ A" for α
proof (rule manifold_eucl.diff_localI, unfold diff_fun_def[symmetric])
fix x assume x: "x ∈ carrier"
show "open (I x)" "x ∈ I x" using I x by auto
then interpret submanifold _ _ "I x"
by unfold_locales
have "diff_fun k (charts_submanifold (I x)) (λy. (∑i | i ∈ N ∧ a i = α ∧ W i ∩ I x ≠ {}. g i y))"
apply (rule sub.diff_fun_sum, clarsimp)
subgoal premises prems for i
proof -
interpret dg: diff_fun k charts "g i" by (rule g) fact
show ?thesis
apply (rule dg.diff_fun_submanifold)
by (rule I) fact
qed
done
then show "diff_fun k (charts_submanifold (I x)) (φ α)"
apply (rule diff_fun.diff_fun_cong)
unfolding φ_def
apply (rule sum.mono_neutral_right)
subgoal using _ I(3)[OF ‹x ∈ carrier›] by (rule finite_subset) (auto simp:)
subgoal using ‹open (I x)› carrier_submanifold by auto
subgoal by (auto simp: g_def f_def)
done
qed
moreover
have "0 ≤ φ α x" if "x ∈ carrier" for α x
by (auto simp: φ_def intro!: sum_nonneg g_nonneg that)
moreover
have "φ α x ≤ 1" if "α ∈ A" "x ∈ carrier" for α x
proof -
have "φ α x ≤ (∑i | i ∈ N ∧ x ∈ W i. g i x)"
unfolding φ_def
by (rule sum_mono2[OF finite_W]) (auto simp: intro!: g_nonneg ‹x ∈ carrier›)
also have "… = 1"
by (rule sum_g) fact
finally show ?thesis .
qed
moreover
have "(∑α∈{α∈A. φ α x ≠ 0}. φ α x) = 1" if "x ∈ carrier" for x
proof -
have "(∑α | α ∈ A ∧ φ α x ≠ 0. φ α x) =
(∑α | α ∈ A ∧ φ α x ≠ 0. ∑i | i ∈ N ∧ a i = α ∧ x ∈ W i. g i x)"
unfolding φ_def ..
also have "… = (∑(α, i)∈(SIGMA xa:{α ∈ A. φ α x ≠ 0}. {i ∈ N. a i = xa ∧ x ∈ W i}). g i x)"
apply (rule sum.Sigma)
subgoal
apply (rule finite_subset[where B="a ` {j ∈ N. x ∈ W j}"])
subgoal
apply (auto simp: φ_def)
apply (subst (asm) sum_nonneg_eq_0_iff)
subgoal using _ finite_W[OF ‹x ∈ carrier›] by (rule finite_subset) auto
subgoal by (rule g_nonneg[OF _ ‹x ∈ carrier›]) auto
subgoal by auto
done
subgoal
using finite_W[OF ‹x ∈ carrier›] by (rule finite_imageI)
done
subgoal
apply (auto)
using _ finite_W[OF ‹x ∈ carrier›]
by (rule finite_subset) auto
done
also have "… = (∑i∈snd ` (SIGMA xa:{α ∈ A. φ α x ≠ 0}. {i ∈ N. a i = xa ∧ x ∈ W i}). g i x)"
apply (rule sum.reindex_cong[where l="λi. (a i, i)"])
subgoal by (auto simp: inj_on_def)
subgoal
apply (auto simp: a)
apply (auto simp: φ_def)
apply (subst (asm) sum_nonneg_eq_0_iff)
subgoal
using _ finite_W[OF ‹x ∈ carrier›]
by (rule finite_subset) auto
subgoal by (auto intro!: g_nonneg ‹x ∈ carrier›)
subgoal for i
apply auto
subgoal for yy
apply (rule imageI)
apply (rule image_eqI[where x="(a i, i)"])
apply (auto intro!: a)
apply (subst (asm) sum_nonneg_eq_0_iff)
subgoal using _ finite_W[OF ‹x ∈ carrier›] by (rule finite_subset) auto
subgoal by (rule g_nonneg[OF _ ‹x ∈ carrier›]) auto
subgoal by auto
done
done
done
subgoal by auto
done
also have "… = (∑i | i ∈ N ∧ x ∈ W i. g i x)"
apply (rule sum.mono_neutral_left)
subgoal by (rule finite_W) fact
subgoal by auto
subgoal
apply (auto simp: Sigma_def image_iff a)
apply (auto simp: φ_def)
subgoal
apply (subst (asm) sum_nonneg_eq_0_iff)
subgoal using _ finite_W[OF ‹x ∈ carrier›] by (rule finite_subset) auto
subgoal by (rule g_nonneg[OF _ ‹x ∈ carrier›]) auto
subgoal by auto
done
done
done
also have "… = 1" by (rule sum_g) fact
finally show ?thesis .
qed
moreover
have g_supp_le_V: "support_on carrier (g i) ⊆ V i" if "i ∈ N" for i
apply (auto simp: support_on_def g_def f_def V_def dest!: H_neq_zeroD)
apply (rule image_eqI[OF ])
apply (rule inv_chart_inverse[symmetric])
apply (simp add: W_eq that)
apply simp
done
then have clsupp_g_le_W: "closure (support_on carrier (g i)) ⊆ W i" if "i ∈ N" for i
unfolding csupport_on_def
using V_subset_W closure_mono that
by blast
then have csupp_g_le_W: "csupport_on carrier (g i) ⊆ W i" if "i ∈ N" for i
using that
by (auto simp: csupport_on_def)
have *: "{i ∈ N. domain (ψ i) ∩ Na ≠ {}} = {i ∈ N. W i ∩ Na ≠ {}}" for Na
by (auto simp: W_eq)
then have lfW: "locally_finite_on carrier N W"
using regular_cover(3) by (simp add: locally_finite_on_def)
then have lf_supp_g: "locally_finite_on carrier {i ∈ N. a i = α} (λi. support_on carrier (g i))" if "α ∈ A" for α
apply (rule locally_finite_on_subset)
using g_supp_le_V V_subset_W
by force+
have "csupport_on carrier (φ α) ∩ carrier ⊆ X α" if "α ∈ A" for α
proof -
have *: "closure (⋃i∈{i ∈ N. a i = α}. support_on carrier (g i)) ⊆ closure (⋃i∈N. V i)"
by (rule closure_mono) (use g_supp_le_V in auto)
have "support_on carrier (φ α) ⊆ (⋃i∈{i ∈ N. a i = α}. support_on carrier (g i))"
unfolding φ_def[abs_def]
apply (rule order_trans)
apply (rule support_on_nonneg_sum_subset')
using g_supp_le_V
by (auto simp: carrier_V)
then have "csupport_on carrier (φ α) ∩ carrier ⊆ closure … ∩ carrier"
unfolding csupport_on_def using closure_mono by auto
also have "… = (⋃i∈{i ∈ N. a i = α}. closure (support_on carrier (g i)))"
apply (rule locally_finite_on_closure_Union[OF lf_supp_g[OF that], symmetric])
using closure_mono[OF g_supp_le_V] V_subset_W
by (force simp: carrier_W)
also have "… ⊆ (⋃i∈{i ∈ N. a i = α}. W i)"
apply (rule UN_mono)
using clsupp_g_le_W
by auto
also have "… ⊆ X α"
using a
by auto
finally show ?thesis .
qed
moreover
have "locally_finite_on carrier A (λi. support_on carrier (φ i))"
proof (rule locally_finite_onI)
fix p assume "p ∈ carrier"
from locally_finite_onE[OF lfW this] obtain Nhd where Nhd: "p ∈ Nhd" "open Nhd" "finite {i ∈ N. W i ∩ Nhd ≠ {}}" .
show "∃Nhd. p ∈ Nhd ∧ open Nhd ∧ finite {i ∈ A. support_on carrier (φ i) ∩ Nhd ≠ {}}"
apply (rule exI[where x=Nhd])
apply (auto simp: Nhd)
apply (rule finite_subset[where B="a ` {i ∈ N. W i ∩ Nhd ≠ {}}"])
subgoal
apply (auto simp: support_on_def φ_def)
apply (subst (asm) sum_nonneg_eq_0_iff)
apply (auto simp: intro!: g_nonneg)
using _ finite_W by (rule finite_subset) auto
by (rule finite_imageI) fact
qed
then have "locally_finite_on carrier A (λi. csupport_on carrier (φ i))"
unfolding csupport_on_def
by (rule locally_finite_on_closure)
ultimately show ?thesis ..
qed
text ‹Given ‹A ⊆ U ⊆ carrier›, where ‹A› is closed and ‹U› is open, there exists
a differentiable function ‹ψ› such that ‹0 ≤ ψ ≤ 1›, ‹ψ = 1› on ‹A›, and the
support of ‹ψ› is contained in ‹U›.›
lemma smooth_bump_functionE:
assumes "closedin (top_of_set carrier) A"
and "A ⊆ U" "U ⊆ carrier" "open U"
obtains ψ::"'a ⇒ real" where
"diff_fun k charts ψ"
"⋀x. x ∈ carrier ⟹ 0 ≤ ψ x"
"⋀x. x ∈ carrier ⟹ ψ x ≤ 1"
"⋀x. x ∈ A ⟹ ψ x = 1"
"csupport_on carrier ψ ∩ carrier ⊆ U"
proof -
define V where "V x = (if x = 0 then U else carrier - A)" for x::nat
have "open (carrier - A)"
using assms
by (metis closedin_def open_Int open_carrier openin_open topspace_euclidean_subtopology)
then have V: "carrier ⊆ (⋃i∈{0, 1}. V i)" "i ∈ {0, 1} ⟹ open (V i)" for i
using assms
by (auto simp: V_def)
obtain φ::"nat ⇒ 'a ⇒ real" where φ:
"(⋀i. i ∈ {0, 1} ⟹ diff_fun k charts (φ i))"
"(⋀i x. i ∈ {0, 1} ⟹ x ∈ carrier ⟹ 0 ≤ φ i x)"
"(⋀i x. i ∈ {0, 1} ⟹ x ∈ carrier ⟹ φ i x ≤ 1)"
"(⋀x. x ∈ carrier ⟹ (∑i | i ∈ {0, 1} ∧ φ i x ≠ 0. φ i x) = 1)"
"(⋀i. i ∈ {0, 1} ⟹ csupport_on carrier (φ i) ∩ carrier ⊆ V i)"
"locally_finite_on carrier {0, 1} (λi. csupport_on carrier (φ i))"
by (rule partitions_of_unityE[OF V]) auto
from this(1-3,5)[of 0] this(6)
have "diff_fun k charts (φ 0)"
"⋀x. x ∈ carrier ⟹ 0 ≤ φ 0 x"
"⋀x. x ∈ carrier ⟹ φ 0 x ≤ 1"
"csupport_on carrier (φ 0) ∩ carrier ⊆ U"
by (auto simp: V_def)
moreover have "φ 0 x = 1" if "x ∈ A" for x
proof -
from that have "x ∈ carrier" using assms by auto
from φ(4)[OF this]
have "1 = (∑i | i ∈ {0, 1} ∧ φ i x ≠ 0. φ i x)"
by auto
moreover have "{i. i ∈ {0, 1} ∧ φ i x ≠ 0} =
(if φ 0 x ≠ 0 then {0} else {}) ∪ (if φ 1 x ≠ 0 then {1} else {})"
apply auto
using neq0_conv by blast
moreover have "x ∉ V 1"
using that
by (auto simp: V_def)
then have "φ (Suc 0) x = 0"
using φ(5)[of 1] assms that
by (auto simp: support_on_def csupport_on_def)
ultimately show ?thesis by (auto split: if_splits)
qed
ultimately show ?thesis by (blast intro: that)
qed
definition "diff_fun_on A f ⟷
(∃W. A ⊆ W ∧ W ⊆ carrier ∧ open W ∧
(∃f'. diff_fun k (charts_submanifold W) f' ∧ (∀x∈A. f x = f' x)))"
lemma diff_fun_onE:
assumes "diff_fun_on A f"
obtains W f' where
"A ⊆ W" "W ⊆ carrier" "open W" "diff_fun k (charts_submanifold W) f'"
"⋀x. x ∈ A ⟹ f x = f' x"
using assms by (auto simp: diff_fun_on_def)
lemma diff_fun_onI:
assumes "A ⊆ W" "W ⊆ carrier" "open W" "diff_fun k (charts_submanifold W) f'"
"⋀x. x ∈ A ⟹ f x = f' x"
shows "diff_fun_on A f"
using assms by (auto simp: diff_fun_on_def)
text ‹Extension lemma:
Given ‹A ⊆ U ⊆ carrier›, where ‹A› is closed and ‹U› is open, and a differentiable
function ‹f› on ‹A›, there exists a differentiable function ‹f'› agreeing with ‹f›
on ‹A›, and where the support of ‹f'› is contained in ‹U›.›
lemma extension_lemmaE:
fixes f::"'a ⇒ 'e::euclidean_space"
assumes "closedin (top_of_set carrier) A"
assumes "diff_fun_on A f" "A ⊆ U" "U ⊆ carrier" "open U"
obtains f' where
"diff_fun k charts f'"
"⋀x. x ∈ A ⟹ f' x = f x"
"csupport_on carrier f' ∩ carrier ⊆ U"
proof -
from diff_fun_onE[OF assms(2)]
obtain W' f' where W': "A ⊆ W'" "W' ⊆ carrier" "open W'" "diff_fun k (charts_submanifold W') f'"
"(⋀x. x ∈ A ⟹ f x = f' x)"
by blast
define W where "W = W' ∩ U"
interpret W': diff_fun k "charts_submanifold W'" f' using W' by auto
have *: "open (W' ∩ U)"
using W' assms by auto
with W'.diff_fun_submanifold[of W]
have "diff_fun k (W'.src.charts_submanifold (W' ∩ U)) f'"
by (auto simp: W_def)
also have "W'.src.charts_submanifold (W' ∩ U) = charts_submanifold (W' ∩ U)"
unfolding W'.src.charts_submanifold_def
unfolding charts_submanifold_def
using W' *
by (auto simp: image_image restrict_chart_restrict_chart ac_simps)
finally have "diff_fun k (charts_submanifold (W' ∩ U)) f'" .
with W' assms
have W: "A ⊆ W" "W ⊆ carrier" "open W" "diff_fun k (charts_submanifold W) f'"
"(⋀x. x ∈ A ⟹ f x = f' x)"
by (auto simp: W_def)
interpret submanifold _ _ W by unfold_locales fact
interpret W: diff_fun k "(charts_submanifold W)" f' using W by auto
have [simp]: "sub.carrier = W" using ‹W ⊆ carrier› by auto
have "W ⊆ U" by (auto simp: W_def)
from smooth_bump_functionE[OF assms(1) ‹A ⊆ W› ‹W ⊆ carrier› ‹open W›]
obtain φ::"'a⇒real" where φ: "diff_fun k charts φ"
"(⋀x. x ∈ carrier ⟹ 0 ≤ φ x)" "(⋀x. x ∈ carrier ⟹ φ x ≤ 1)" "(⋀x. x ∈ A ⟹ φ x = 1)"
"csupport_on carrier φ ∩ carrier ⊆ W" by blast
interpret φ: diff_fun k charts φ by fact
define g where "g p = (if p ∈ W then φ p *⇩R f' p else 0)" for p
thm sub.diff_fun_scaleR
have "diff_fun k charts g"
proof (rule manifold_eucl.diff_open_Un, unfold diff_fun_def[symmetric])
have "diff_fun k (charts_submanifold W) (λp. φ p *⇩R f' p)"
by (auto intro!: sub.diff_fun_scaleR φ.diff_fun_submanifold W)
then show "diff_fun k (charts_submanifold W) g"
by (rule diff_fun.diff_fun_cong) (auto simp: g_def)
interpret C: submanifold _ _ "carrier - csupport_on carrier φ"
by unfold_locales auto
have sub_carrier[simp]: "C.sub.carrier = carrier - csupport_on carrier φ"
by auto
have "diff_fun k (charts_submanifold (carrier - csupport_on carrier φ)) 0"
by (rule C.sub.diff_fun_zero)
then show "diff_fun k (charts_submanifold (carrier - csupport_on carrier φ)) g"
by (rule diff_fun.diff_fun_cong) (auto simp: g_def not_in_csupportD)
show "open W" by fact
show "open (carrier - csupport_on carrier φ)"
by (auto)
show "carrier ⊆ W ∪ (carrier - csupport_on carrier φ)"
using φ
by auto
qed
moreover have "⋀x. x ∈ A ⟹ g x = f x"
using ‹A ⊆ W›
by (auto simp: g_def φ W')
moreover have "csupport_on carrier g ∩ carrier ⊆ U"
proof -
have "csupport_on carrier g ⊆ csupport_on carrier φ"
by (rule csupport_on_mono) (auto simp: g_def[abs_def] split: if_splits)
also have "… ∩ carrier ⊆ U"
using φ(5) ‹W ⊆ U› ‹W ⊆ carrier› ‹U ⊆ carrier›
by auto
finally show ?thesis by auto
qed
ultimately show ?thesis ..
qed
end
end