■スターリング型不等式の証明と漸近評価(その7)

【1】別解

 オイラー関数f(x)は

  f(x)=x^f(x)

で定義される.z=we^wにおけるwの主要解を与えるPrpductLog[z]を用いるて,a=x^aを解くと

  a=PrpductLog[-Log[x]]/Log[x]

z>-1/eのとき,PrpductLog[z]は実数である.これでオイラー関数はwell-definedであり,x→0まで解析接続できること=xの定義域は(0,e^(1/e)]であることがわかったが,それでも[e^(-e),e^(1/e)]であるという結論までには至っていない.

===================================

【2】阪本ひろむ氏による解説

 ProductLogを含む関数は,あくまでもMathematicaが計算してくれた関数である.(要するに,Mathematicaがたまたまこの関数をサポートしてくれたから,Solveで解がもとまった)

 その定義は陰関数で定義される.この関数は多価関数であるが,我々の考察の範囲では分岐点はないので,このまま答えを信じてよいのである.

 0<x<1のとき,0≦f_n(x)≦1である.したがって,0≦limsup f_n(x)≦liminf f_n(x)≦1

limsup f_n(x)=aも,liminf f_n(x)=bも,x=a^(1/a), x=b^(1/b)の条件を満たすが, x=a^(1/a)はaに関する狭義単調増加関数(0<a≦1)であるから, x=a^(1/a)をみたすaは一意的に決まる.つまり,a=bである.

→lim f_n(x)は存在する.

→x \in (0,1]に対して a=a(x)は定義できる.

→x^x^x....の定義域は(0,1]を含む.

 さらに,Mathematicaでこの関数

f[x_]:=-(ProductLog[-Log[x]]/Log[x])

が求められた.x→0のとき,f(x)→0であるから,x=0のとき,好みによりx^x^.... = 0としてもよいし,0^0=1であるからf(0)=1(不連続点)にしてもよいのである.

===================================

【3】今後の方針

  lim inf f_n = lim sup f_n

で収束することの証明にはなっているのであるが,直接数列がコーシー列であることに帰着して収束することを証明できればそのほうがよい.

 f_nの対数,もしくは対数の対数をとって,うまく数列がコーシー列に帰着できるかもしれない.このとき,等比級数の収束条件から,E^(-E)≦xという条件が導き出せるかもしれない.上記検討されたし.

===================================