774: エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）|T.B.P.日本語版

<このシリーズの前の記事 | このシリーズの目次 | このシリーズの次の記事>

エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）の記述/証明

話題

About: $C^{\infty}$ マニフォールド（多様体）

開始コンテキスト

読者は、 $C^{\infty}$ マニフォールド（多様体）、バウンダリー（境界）付き、のエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、の定義を知っている。
読者は、ユークリディアンセット（集合）上のスライシングマップ（写像）の定義を知っている。
読者は、ユークリディアンセット（集合）上のスライシングアンドハーフ化マップ（写像）の定義を知っている。
読者は、ユークリディアンセット（集合）たち間プロジェクション（射影）の定義を知っている。

ターゲットコンテキスト

読者は、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションのフォーマライゼーション（定式化）は妥当であるという命題の記述および証明を得る。

オリエンテーション

本サイトにてこれまで議論された定義たちの一覧があります。

本サイトにてこれまで議論された命題たちの一覧があります。

本体

1: 構造化された記述

ここに'構造化された記述'のルールたちがある。

エンティティ（実体）たち:

M^{'}

\in {the d^{'} ディメンショナル（次元） C^{\infty} マニフォールド（多様体）たち}

S

\subseteq M^{'}

J

\subseteq {1, . . ., d^{'}}

で、

| J | = d

を満たすもの

k

\in J

s

\in S

λ_{J, r^{'}}

: P o w (R^{d^{'}}) \to P o w (R^{d^{'}})

= 当該スライシングマップ（写像）

、ここで、

r^{'} \in R^{d^{'}}

は任意のもの

λ_{J, r^{'}, k}

: P o w (R^{d^{'}}) \to P o w (R^{d^{'}})

= 当該スライシングアンドハーフ化マップ（写像）

、ここで、

r^{'} \in R^{d^{'}}

は任意のもの

π_{J}

: R^{d^{'}} \to R^{d}

= 当該プロジェクション（射影）

//

ステートメント（言明）たち:
(

S

は、

s

において、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションを満たす

⟺

\exists (U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'}) \in {s の周りの M^{'} の全てのチャートたち} (ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})))

⟹

(

(U_{s} = U_{s}^{'} \cap S, ϕ_{s} = π_{J} \circ ϕ_{s}^{'} |_{U_{s}})

は、対応するアダプティングチャート

\land

ϕ_{s} (U_{s}) = π_{J} \circ ϕ_{s}^{'} (U_{s}) = π_{J} \circ λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'}))

)
)

\land

(

S

は、

s

において、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションを満たす

⟺

\exists (U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'}) \in {s の周りの M^{'} の全てのチャートたち} (ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})) \lor (ϕ_{s}^{'} (s)^{k} = 0 \land ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'}))))

⟹

(

(U_{s} = U_{s}^{'} \cap S, ϕ_{s} = π_{J} \circ ϕ_{s}^{'} |_{U_{s}})

は、対応するアダプティングチャート

\land

ϕ_{s} (U_{s}) = π_{J} \circ ϕ_{s}^{'} (U_{s}) = π_{J} \circ λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})) or π_{J} \circ λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'}))

)
)
//

2: 自然言語記述

任意の

d^{'}

ディメンショナル（次元）

C^{\infty}

マニフォールド（多様体）

M^{'}

、任意のサブセット（部分集合）

S \subseteq M^{'}

、以下を満たす任意のサブセット（部分集合）

J \subseteq {1, . . ., d^{'}}

、つまり、

| J | = d

、任意の

k \in J

、任意のポイント

s \in S

、スライシングマップ（写像）

λ_{J, r^{'}} : P o w (R^{d^{'}}) \to P o w (R^{d^{'}})

、ここで、

r^{'} \in R^{d^{'}}

は任意のもの、スライシングアンドハーフ化マップ（写像）

λ_{J, r^{'}, k} : P o w (R^{d^{'}}) \to P o w (R^{d^{'}})

、ここで、

r^{'} \in R^{d^{'}}

は任意のもの、プロジェクション（射影）

π_{J} : R^{d^{'}} \to R^{d}

に対して、

S

は、

s

において、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションを満たす、もしも、

s

の周りに以下を満たすあるチャート

(U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'})

、つまり、

ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'}))

、がある場合、そしてその場合に限って、そして、もしも、そうである場合、対応するアダプティングチャートは

(U_{s} = U_{s}^{'} \cap S, ϕ_{s} = π_{J} \circ ϕ_{s}^{'} |_{U_{s}})

であり、

ϕ_{s} (U_{s}) = π_{J} \circ ϕ_{s}^{'} (U_{s}) = π_{J} \circ λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'}))

;

S

は、

s

において、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションを満たす、もしも、

s

の周りに以下を満たすあるチャート

(U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'})

、つまり、

ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'}))

または

ϕ_{s}^{'} (s)^{k} = 0 \land ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'}))

、がある場合、そしてその場合に限って、そして、そうである場合、対応するアダプティングチャートは

(U_{s} = U_{s}^{'} \cap S, ϕ_{s} = π_{J} \circ ϕ_{s}^{'} |_{U_{s}})

であり、

ϕ_{s} (U_{s}) = π_{J} \circ ϕ_{s}^{'} (U_{s}) = π_{J} \circ λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})) または π_{J} \circ λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'}))

。

3: 注

本命題に対するモチベーションは、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションまたはエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションは通常自然言語たちで記述されるが、そうした記述は、当該コンディションへの整合や当該コンディションの帰結たちをチェックするのに便利でないこと。

"証明"は、'

S

はエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）無しまたはバウンダリー（境界）付き、である、もしも、

S

はローカルスライスコンディションを満たす場合、そして、その場合に限って'という命題の証明ではなく、当該フォーマライゼーション（定式化）が妥当であることの証明である。

バウンダリー（境界）付きケースに対して

ϕ_{s}^{'} (s)^{k} = 0

を指定する必要がある理由は、そうでなければ、

π_{J} \circ ϕ_{s}^{'} (U_{s}^{'} \cap S)

は

H^{d}

のオープンサブセット（開部分集合）ではないことになること; その指定は重要事ではない、なぜなら、それは、単に、もしも、

ϕ_{s}^{'} (s)^{k} \neq 0

であったら、当該チャートマップ（写像）を平行移動すればよいだけのこと; 実のところ、大抵の場合、

ϕ_{s}^{'}

は、

ϕ_{s}^{'} (s) = 0

であるように選ばれる。

4: 証明

全体戦略: ステップ1:

s

における、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションは当該フォーマライゼーション（定式化）に等しいことを見る; ステップ2: 当該アダプティングチャートは当該帰結たちを満たすことを見る; ステップ3:

s

における、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションは当該フォーマライゼーション（定式化）に等しいことを見る; ステップ4: 当該アダプティングチャートは当該帰結たちを満たすことを見る。

ステップ1:

Let us suppose that

S

は、

s

における、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションを満たすと仮定しよう。

s

の周りに以下を満たすあるチャート

(U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'})

、つまり、

ϕ_{s}^{'} (U_{s}^{'} \cap S) = {r \in ϕ_{s}^{'} (U_{s}^{'}) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = c^{j})}

、何らかのコンスタント

c^{j} \in R

たちに対して、がある。

s \in U_{s}^{'} \cap S

であるので、

ϕ_{s}^{'} (s) \in ϕ_{s}^{'} (U_{s}^{'} \cap S) = {r \in ϕ_{s}^{'} (U_{s}^{'}) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = c^{j})}

、それが含意するのは、

\forall j \in {1, . . ., d^{'}} ∖ J (ϕ_{s}^{'} (s)^{j} = c^{j})

、それが意味するのは、

{r \in ϕ_{s}^{'} (U_{s}^{'}) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = c^{j})} = {r \in ϕ_{s}^{'} (U_{s}^{'}) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = ϕ_{s}^{'} (s)^{j})} = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'}))

。

したがって、

ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})))

。

S

は、

\exists (U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'}) \in {the charts around s of M'} (ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})))

を満たすと仮定しよう。

λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})) = {r \in ϕ_{s}^{'} (U_{s}^{'})) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = ϕ_{s}^{'} (s)^{j})}

。

c^{j} := ϕ_{s}^{'} (s)^{j}

たちはコンスタントたちであるので、

S

は、

s

における、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションを満たす。

ステップ2:

S

は、

s

における、エンベッデッドサブマニフォールド（部分多様体）に対するローカルスライスコンディションを満たすと仮定する。

対応するアダプティングチャートは

(U_{s} = U_{s}^{'} \cap S, ϕ_{s} = π_{J} \circ ϕ_{s}^{'} |_{U_{s}})

（私たちは、それが本当にエンベッデッドサブマニフォールド（部分多様体）に対するチャートであること（それは、'

S

はエンベッデッドサブマニフォールド（部分多様体）である、もしも、

S

はローカルスライスコンディションを満たす場合、そして、その場合に限って'という命題の中で証明されるものである）をここで証明するつもりはない）。

ϕ_{s} (U_{s}) = π_{J} \circ ϕ_{s}^{'} |_{U_{s}} (U_{s}) = π_{J} \circ ϕ_{s}^{'} (U_{s}) = π_{J} \circ ϕ_{s}^{'} (U_{s}^{'} \cap S) = π_{J} \circ λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'}))

。

ステップ3:

S

は、

s

における、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションを満たすと仮定しよう。

s

の周りに以下を満たすチャート

(U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'})

、つまり、

ϕ_{s}^{'} (U_{s}^{'} \cap S) = {r \in ϕ_{s}^{'} (U_{s}^{'}) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = c^{j})}

または

ϕ_{s}^{'} (s)^{k} = 0 \land ϕ_{s}^{'} (U_{s}^{'} \cap S) = {r \in ϕ_{s}^{'} (U_{s}^{'}) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = c^{j}) \land 0 \leq r^{k}}

、何らかのコンスタント

c^{j} \in R

たちに対して、がある。

s \in U_{s}^{'} \cap S

であるから、

ϕ_{s}^{'} (s) \in ϕ_{s}^{'} (U_{s}^{'} \cap S) = {r \in ϕ_{s}^{'} (U_{s}^{'}) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = c^{j})} または {r \in ϕ_{s}^{'} (U_{s}^{'}) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = c^{j}) \land 0 \leq r^{k}}

、それが含意するのは、

\forall j \in {1, . . ., d^{'}} ∖ J (ϕ_{s}^{'} (s)^{j} = c^{j})

、それが意味するのは、

{r \in ϕ_{s}^{'} (U_{s}^{'}) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = c^{j})} = {r \in ϕ_{s}^{'} (U_{s}^{'}) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = ϕ_{s}^{'} (s)^{j})} = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})))

および

{r \in ϕ_{s}^{'} (U_{s}^{'}) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = c^{j}) \land ϕ_{s}^{'} (s)^{k} \leq r^{k}} = {r \in ϕ_{s}^{'} (U_{s}^{'}) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = ϕ_{s}^{'} (s)^{j}) \land ϕ_{s}^{'} (s)^{k} \leq r^{k}} = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'})))

。

したがって、

ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})) または ϕ_{s}^{'} (s)^{k} = 0 \land ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'}))

。

S

は、

\exists (U_{s}^{'} \subseteq M^{'}, ϕ_{s}^{'}) \in {s の周りの M^{'} の全てのチャートたち} (ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})) または ϕ_{s}^{'} (s)^{k} = 0 \land ϕ_{s}^{'} (U_{s}^{'} \cap S) = λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'})))

を満たすと仮定する。

λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'}))) = {r \in ϕ_{s}^{'} (U_{s}^{'})) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = ϕ_{s}^{'} (s)^{j})}

および

λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'}))) = {r \in ϕ_{s}^{'} (U_{s}^{'})) | \forall j \in {1, . . ., d^{'}} ∖ J (r^{j} = ϕ_{s}^{'} (s)^{j}) \land ϕ_{s}^{'} (s)^{k} \leq r^{k}}

。

c^{j} := ϕ_{s}^{'} (s)^{j}

たちはコンスタントたちであり、

ϕ_{s}^{'} (s)^{k} = 0

は

ϕ_{s}^{'} (s)^{k} \leq r^{k}

を

0 \leq r^{k}

であるとするので、

S

は、

s

における、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションを満たす。

ステップ4:

S

は、

s

における、エンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するローカルスライスコンディションを満たすと仮定しよう。

対応するアダプティングチャートは

(U_{s} = U_{s}^{'} \cap S, ϕ_{s} = π_{J} \circ ϕ_{s}^{'} |_{U_{s}})

である（私たちは、それが本当にエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、に対するチャートであること（それは、'

S

はエンベッデッドサブマニフォールド（部分多様体）、バウンダリー（境界）付き、である、もしも、

S

ϕ_{s} (U_{s}) = π_{J} \circ ϕ_{s}^{'} |_{U_{s}} (U_{s}) = π_{J} \circ ϕ_{s}^{'} (U_{s}) = π_{J} \circ ϕ_{s}^{'} (U_{s}^{'} \cap S) = π_{J} \circ λ_{J, ϕ_{s}^{'} (s)} (ϕ_{s}^{'} (U_{s}^{'})) または π_{J} \circ λ_{J, ϕ_{s}^{'} (s), k} (ϕ_{s}^{'} (U_{s}^{'}))

。

参考資料

<このシリーズの前の記事 | このシリーズの目次 | このシリーズの次の記事>

バイアス惑星
定義たちと命題たち
学校数学をより高い視点から
わかりにくい用語や説明をひもとく
情報テーブル群
LibreOfficeまたはOpenOfficeを活用する
Javaプログラミング言語を暴く
C++を暴く
Pythonを暴く
C#を暴く
Gradleを暴く
Gitを暴く
UNOディスパッチコマンドたち

2024年9月15日日曜日

話題

この記事の目次

開始コンテキスト

ターゲットコンテキスト

オリエンテーション

本体

1: 構造化された記述

2: 自然言語記述

3: 注

4: 証明

参考資料