Theory Tangent_Space
section‹Tangent Space›
theory Tangent_Space
imports Partition_Of_Unity
begin
lemma linear_imp_linear_on: "linear_on A B scaleR scaleR f" if "linear f"
"subspace A" "subspace B"
proof -
interpret linear f by fact
show ?thesis using that
by unfold_locales (auto simp: add scaleR algebra_simps subspace_def)
qed
lemma (in vector_space_pair_on)
linear_sum':
"∀x. x ∈ S1 ⟶ f x ∈ S2 ⟹
∀x. x ∈ S ⟶ g x ∈ S1 ⟹
linear_on S1 S2 scale1 scale2 f ⟹
f (sum g S) = (∑a∈S. f (g a))"
using linear_sum[of f "λx. if x ∈ S then g x else 0" S]
by (auto simp: if_distrib if_distribR m1.mem_zero cong: if_cong)
subsection ‹Real vector (sub)spaces›
locale real_vector_space_on = fixes S assumes subspace: "subspace S"
begin
sublocale vector_space_on S scaleR
rewrites span_eq_real: "local.span = real_vector.span"
and dependent_eq_real: "local.dependent = real_vector.dependent"
and subspace_eq_real: "local.subspace = real_vector.subspace"
proof -
show "vector_space_on S (*⇩R)"
by unfold_locales (use subspace[unfolded subspace_def] in ‹auto simp: algebra_simps›)
then interpret subspace: vector_space_on S scaleR .
show 1: "subspace.span = span"
unfolding subspace.span_on_def span_explicit by auto
show 2: "subspace.dependent = dependent"
unfolding subspace.dependent_on_def dependent_explicit by auto
show 3: "subspace.subspace = subspace"
unfolding subspace.subspace_on_def subspace_def by auto
qed
lemma dim_eq: "local.dim X = real_vector.dim X" if "X ⊆ S"
proof -
have *: "b ⊆ S ∧ independent b ∧ span b = span X ⟷ independent b ∧ span b = span X"
for b
using that
by auto (metis local.subspace_UNIV real_vector.span_base real_vector.span_eq_iff real_vector.span_mono subsetCE)
show ?thesis
using that
unfolding local.dim_def real_vector.dim_def *
by auto
qed
end
locale real_vector_space_pair_on = vs1: real_vector_space_on S + vs2: real_vector_space_on T for S T
begin
sublocale vector_space_pair_on S T scaleR scaleR
rewrites span_eq_real1: "module_on.span scaleR = vs1.span"
and dependent_eq_real1: "module_on.dependent scaleR = vs1.dependent"
and subspace_eq_real1: "module_on.subspace scaleR = vs1.subspace"
and span_eq_real2: "module_on.span scaleR = vs2.span"
and dependent_eq_real2: "module_on.dependent scaleR = vs2.dependent"
and subspace_eq_real2: "module_on.subspace scaleR = vs2.subspace"
by unfold_locales (simp_all add: vs1.span_eq_real vs1.dependent_eq_real vs1.subspace_eq_real
vs2.span_eq_real vs2.dependent_eq_real vs2.subspace_eq_real)
end
locale finite_dimensional_real_vector_space_on = real_vector_space_on S for S +
fixes basis :: "'a set"
assumes finite_dimensional_basis: "finite basis" "¬ dependent basis" "span basis = S" "basis ⊆ S"
begin
sublocale finite_dimensional_vector_space_on S scaleR basis
rewrites span_eq_real: "local.span = real_vector.span"
and dependent_eq_real: "local.dependent = real_vector.dependent"
and subspace_eq_real: "local.subspace = real_vector.subspace"
by unfold_locales (simp_all add: finite_dimensional_basis dependent_eq_real span_eq_real)
end
locale finite_dimensional_real_vector_space_pair_1_on =
vs1: finite_dimensional_real_vector_space_on S1 basis +
vs2: real_vector_space_on S2
for S1 S2 basis
begin
sublocale finite_dimensional_vector_space_pair_1_on S1 S2 scaleR scaleR basis
rewrites span_eq_real1: "module_on.span scaleR = vs1.span"
and dependent_eq_real1: "module_on.dependent scaleR = vs1.dependent"
and subspace_eq_real1: "module_on.subspace scaleR = vs1.subspace"
and span_eq_real2: "module_on.span scaleR = vs2.span"
and dependent_eq_real2: "module_on.dependent scaleR = vs2.dependent"
and subspace_eq_real2: "module_on.subspace scaleR = vs2.subspace"
apply unfold_locales
subgoal using real_vector_space_on.span_eq_real vs1.real_vector_space_on_axioms by blast
subgoal using real_vector_space_on.dependent_eq_real vs1.real_vector_space_on_axioms by blast
subgoal using real_vector_space_on.subspace_eq_real vs1.real_vector_space_on_axioms by blast
subgoal using real_vector_space_on.span_eq_real vs2.real_vector_space_on_axioms by blast
subgoal using real_vector_space_on.dependent_eq_real vs2.real_vector_space_on_axioms by blast
subgoal using real_vector_space_on.subspace_eq_real vs2.real_vector_space_on_axioms by blast
done
end
locale finite_dimensional_real_vector_space_pair_on =
vs1: finite_dimensional_real_vector_space_on S1 Basis1 +
vs2: finite_dimensional_real_vector_space_on S2 Basis2
for S1 S2 Basis1 Basis2
begin
sublocale finite_dimensional_real_vector_space_pair_1_on S1 S2 Basis1
by unfold_locales
sublocale finite_dimensional_vector_space_pair_on S1 S2 scaleR scaleR Basis1 Basis2
rewrites "module_on.span scaleR = vs1.span"
and "module_on.dependent scaleR = vs1.dependent"
and "module_on.subspace scaleR = vs1.subspace"
and "module_on.span scaleR = vs2.span"
and "module_on.dependent scaleR = vs2.dependent"
and "module_on.subspace scaleR = vs2.subspace"
apply unfold_locales
subgoal by (simp add: span_eq_real1)
subgoal by (simp add: dependent_eq_real1)
subgoal by (simp add: subspace_eq_real1)
subgoal by (simp add: span_eq_real2)
subgoal by (simp add: dependent_eq_real2)
subgoal by (simp add: subspace_eq_real2)
done
end
subsection ‹Derivations›
context c_manifold begin
text ‹Set of ‹C^k› differentiable functions on carrier, where the smooth structure
is given by charts. We assume ‹f› is zero outside carrier›
definition diff_fun_space :: "('a ⇒ real) set" where
"diff_fun_space = {f. diff_fun k charts f ∧ extensional0 carrier f}"
lemma diff_fun_spaceD: "diff_fun k charts f" if "f ∈ diff_fun_space"
using that by (auto simp: diff_fun_space_def)
lemma diff_fun_space_order_le: "diff_fun_space ⊆ c_manifold.diff_fun_space charts l" if "l ≤ k"
proof -
interpret l: c_manifold charts l
by (rule c_manifold_order_le) fact
show ?thesis
unfolding diff_fun_space_def l.diff_fun_space_def
using diff_fun.diff_fun_order_le[OF _ that]
by auto
qed
lemma diff_fun_space_extensionalD:
"g ∈ diff_fun_space ⟹ extensional0 carrier g"
by (auto simp: diff_fun_space_def)
lemma diff_fun_space_eq: "diff_fun_space = {f. diff_fun k charts f} ∩ {f. extensional0 carrier f}"
by (auto simp: diff_fun_space_def)
lemma subspace_diff_fun_space[intro, simp]:
"subspace diff_fun_space"
unfolding diff_fun_space_eq
by (intro subspace_inter subspace_Collect_diff_fun subspace_extensional0)
lemma diff_fun_space_times: "f * g ∈ diff_fun_space"
if "f ∈ diff_fun_space" "g ∈ diff_fun_space"
using that by (auto simp: diff_fun_space_def intro!: diff_fun_times)
lemma diff_fun_space_add: "f + g ∈ diff_fun_space"
if "f ∈ diff_fun_space" "g ∈ diff_fun_space"
using that by (auto simp: diff_fun_space_def intro!: diff_fun_add)
text ‹Set of differentiable functions is a vector space›