MathLabs

解法: 区間演算による厳密な計算機支援証明、Tucker(1999年)

ステップ 3/8: 難しい部分を厳密に解く:鞍点付近の標準形
ざっくり言うと

原点で線形化されたLorenz系の固有値は、三つの具体的な実数である:一つは正(λ1\lambda_1、外向きの方向)、二つは負(λ2,λ3\lambda_2,\lambda_3、内向きの方向)であり、λ1>0>λ3>λ2\lambda_1 > 0 > \lambda_3 > \lambda_2 を満たす。これら三つの数は偶然の整数線形関係(「共鳴」)を満たさないため、古典的な定理は、原点付近の非線形系を、自明に解ける三つの独立した方程式 x˙=λ1x\dot x=\lambda_1 x、y˙=λ2y\dot y=\lambda_2 y、z˙=λ3z\dot z=\lambda_3 z に正確に見えるようにする滑らかな座標変換を保証する。

この新しい座標において、軌道が小さな立方体 U0U_0 に出入りするのにかかる正確な時間、そして正確にどこから出るかは、近似ではなく明示的な公式で書き下すことができる—系全体の中で最も危険な部分を、コンピュータではなく紙とペンだけで解ける唯一の部分に変えるのである。

x˙=λ1x, y˙=λ2y, z˙=λ3z  (normal form near 0),λ1>0>λ3>λ2\dot{x} = \lambda_1 x, \ \dot{y} = \lambda_2 y, \ \dot{z} = \lambda_3 z \ \ (\text{normal form near } 0), \quad \lambda_1 > 0 > \lambda_3 > \lambda_2
詳しい解説

古典的パラメータにおいて、原点で線形化されたLorenzベクトル場は λ1>0>λ3>λ2\lambda_1 > 0 > \lambda_3 > \lambda_2(具体的には λ1≈11.83\lambda_1 \approx 11.83、λ2≈−22.83\lambda_2 \approx -22.83、λ3=−β=−8/3\lambda_3 = -\beta = -8/3)を満たす三つの実固有値を持ち、原点を二次元の安定多様体と一次元の不安定多様体を持つ鞍点にしている。これらの固有値が非共鳴条件(自明なもの以外、それらの小さな整数線形結合が零にならない)を満たすため、Sternbergの線形化定理は、原点の近傍における滑らかな(実際には十分に微分可能な)座標変換の存在を保証し、非線形の流れをその線形部分 x˙=λ1x, y˙=λ2y, z˙=λ3z\dot{x}=\lambda_1 x,\ \dot y=\lambda_2 y,\ \dot z=\lambda_3 z に共役させる。

Tuckerはこの古典的な存在定理を実効的なものにする:この線形化座標において原点周りの小さな立方体 U0U_0 の内部で作業し、U0U_0 の面を通る流入・流出の時刻と位置を、線形系の直接的で閉じた形の積分によって計算し、すべての近似誤差(線形化によって無視された高次項、および座標変換自体によるもの)を、関連するTaylor展開に区間演算を用いて厳密に評価する。

これにより、原点の安定多様体近くに入る初期条件の小さなパッチを流れがどのように運び、不安定多様体の方向によって二つに分割して再注入し、次の段階の数値的Poincaré写像が引き継ぐ領域へと戻すかを正確に記述する、明示的で厳密に検証された公式が生み出される。

このステップで使う知識
よくある間違い. 鞍点付近の線形化座標変換の存在は、(1950年代のSternbergに遡る)古典的で純粋に定性的な事実である;この段階でのTuckerの貢献は、この存在定理自体ではなく、評価を定量的に明示的かつ厳密に評価されたものにすることであり、これこそが証明の数値的部分へ引き継ぐために実際に必要とされるものである。