text【微分方程式 y' = -e^(-xy) (y(0) > 0) の有限時間発散の厳密な証明】

この方程式の解が、有限の x で「必ず -∞ に発散（爆発現象）する」ことの証明の大筋です。
論理は以下の2ステップで完結します。

1. 負の領域への進入（背理法）
すべての x >= 0 で y(x) >= 0（正のまま存在）と仮定します。
このとき積は常に xy >= 0 なので、指数関数の性質から e^(-xy) <= 1 です。
元の式に当てはめると、導関数の上界は常に y' <= -1 となります。
これを 0 から x まで積分すると、 y(x) <= y(0) - x が得られます。
右辺は直線的に減少するため、x > y(0) では y(x) < 0 となり、最初の仮定に矛盾します。
したがって、解は永遠に正のままではいられず、有限の x で必ず 0 を通過して負の領域に入ります。

2. 有限時間での発散（比較定理）
解が負になったある点を (x0, y0) [ただし x0 > 0, y0 < 0] とします。
x >= x0 かつ y <= y0 < 0 の領域では、双方の符号が負であることから、
-xy >= -x0 * y が成り立ちます。
これを元の式に適用すると、次の微分不等式が作れます。
y' = -e^(-xy) <= -e^(-x0 * y)

ここで、右辺を等号とした比較方程式「z' = -e^(-x0 * z)」を導入します。
比較定理より、元の解は常にこの比較解以下（y(x) <= z(x)）になります。
この比較方程式は変数分離形なので厳密に解くことができ、以下の解が得られます。
z(x) = (1 / x0) * ln[ e^(x0 * y0) - x0 * (x - x0) ]

対数関数 ln(X) は、中身が +0 に近づくとき -∞ に発散します。
上式のカッコの中身が 0 になるのは、以下の有限の x_max のときです。
x_max = x0 + (e^(x0 * y0) / x0)

元の解 y(x) は、この z(x) よりも常に小さいため、遅くともこの有限の値 x_max に達する前に必ず -∞ へと発散（爆発）することが数学的に厳密に証明されます。