数学の微分方程式論において、ピカール＝リンデレーフの定理（Picard?Lindelof theorem）、ピカールの存在定理（Picard's existence theorem）、コーシー＝リプシッツの定理（Cauchy?Lipschitz theorem）、または解の存在と一意性の定理（かいのそんざいといちいせいのていり、existence and uniqueness theorem）とは、初期値問題の解が一意に存在するための十分条件を与える定理である。

定理の名前は、エミール・ピカール、エルンスト・レオナルド・リンデレーフ（英語版）、オーギュスタン＝ルイ・コーシー、ルドルフ・リプシッツに因む。

次の初期値問題を考える。 y ′ ( t ) = f ( t , y ( t ) ) , y ( t 0 ) = y 0 {\displaystyle y'(t)=f(t,y(t)),\qquad y(t_{0})=y_{0}}

関数  f  が y に一様にリプシッツ連続（リプシッツ定数が t に依らないことを意味する）であり、かつ、 t に連続しているとすると、ある値 ε > 0 に対して、区間 [ t 0 − ε , t 0 + ε ] {\displaystyle [t_{0}-\varepsilon ,t_{0}+\varepsilon ]} 上で初期値問題の唯一の解 y(t) が存在する[1][要検証 – ノート]。
証明の概略

この定理の証明は、微分方程式を変換し、不動点定理を応用することで行われる。両辺を積分すれば、その微分方程式を満たす関数は、積分方程式 y ( t ) − y ( t 0 ) = ∫ t 0 t f ( s , y ( s ) ) d s {\displaystyle y(t)-y(t_{0})=\int _{t_{0}}^{t}f(s,y(s))\,ds}

をも満たすことになる。解の存在と一意性の証明は、ピカールの逐次近似法によって得られる。この方法はピカール反復(Picard iteration)とも呼ばれる。

ここで関数列 φk を φ 0 ( t ) = y 0 , {\displaystyle \varphi _{0}(t)=y_{0},} φ k + 1 ( t ) = y 0 + ∫ t 0 t f ( s , φ k ( s ) ) d s {\displaystyle \varphi _{k+1}(t)=y_{0}+\int _{t_{0}}^{t}f(s,\varphi _{k}(s))\,ds}

と定義する。バナッハの不動点定理を用いることで、関数列 φk が一様収束し、その極限関数が初期値問題の解であることを示すことができる。グロンウォールの補題を |φ(t) ? ψ(t)。（ φ と ψ は2つの解）に適用すると、 φ(t) = ψ(t) となり、大域的な一意性が証明される（局所的な一意性は、バナッハ不動点の一意性の結果である）。
ピカール反復の例

解として y ( t ) = tan ⁡ ( t ) {\displaystyle y(t)=\tan(t)} を持つ初期値問題 y ′ ( t ) = 1 + y ( t ) 2 , y ( 0 ) = 0 {\displaystyle y'(t)=1+y(t)^{2},\qquad y(0)=0}

に関して実際にピカール反復を計算してみる。 φ n ( t ) → y ( t ) {\displaystyle \varphi _{n}(t)\to y(t)} となるように φ 0 ( t ) = 0 {\displaystyle \varphi _{0}(t)=0} から始めて、 φ k + 1 ( t ) = ∫ 0 t ( 1 + ( φ k ( s ) ) 2 ) d s {\displaystyle \varphi _{k+1}(t)=\int _{0}^{t}(1+(\varphi _{k}(s))^{2})\,ds}

と反復すると、次のようになる。 φ 1 ( t ) = ∫ 0 t ( 1 + 0 2 ) d s = t φ 2 ( t ) = ∫ 0 t ( 1 + s 2 ) d s = t + t 3 3 φ 3 ( t ) = ∫ 0 t ( 1 + ( s + s 3 3 ) 2 ) d s = t + t 3 3 + 2 t 5 15 + t 7 63 {\displaystyle {\begin{aligned}\varphi _{1}(t)&=\int _{0}^{t}(1+0^{2})\,ds=t\\\varphi _{2}(t)&=\int _{0}^{t}(1+s^{2})\,ds=t+{\frac {t^{3}}{3}}\\\varphi _{3}(t)&=\int _{0}^{t}\left(1+\left(s+{\frac {s^{3}}{3}}\right)^{2}\right)\,ds=t+{\frac {t^{3}}{3}}+{\frac {2t^{5}}{15}}+{\frac {t^{7}}{63}}\end{aligned}}}

明らかに、これは既知の解 y ( t ) = tan ⁡ ( t ) {\displaystyle y(t)=\tan(t)} のテイラー級数展開を計算している。 tan {\displaystyle \tan } は ± π / 2 {\displaystyle \pm \pi /2} に極を持つので、これは R 全体ではなく、 。 t 。 < π / 2 {\displaystyle |t|<\pi /2} の範囲でのみ局所解に収束する。
非一意性の例

解の一意性を理解するために、次のような例を考えてみよう[2]。微分方程式は停留点（英語版）を持つことができる。例えば、方程式 .mw-parser-output .sfrac{white-space:nowrap}.mw-parser-output .sfrac.tion,.mw-parser-output .sfrac .tion{display:inline-block;vertical-align:-0.5em;font-size:85%;text-align:center}.mw-parser-output .sfrac .num,.mw-parser-output .sfrac .den{display:block;line-height:1em;margin:0 0.1em}.mw-parser-output .sfrac .den{border-top:1px solid}.mw-parser-output .sr-only{border:0;clip:rect(0,0,0,0);height:1px;margin:-1px;overflow:hidden;padding:0;position:absolute;width:1px}dy/dt = ay ( a < 0 {\displaystyle a<0} ) の定常解は y(t) = 0 であり、これは初期条件 y(0) = 0 で得られる。別の初期条件 y(0) = y0 ≠ 0 から始まる解 y(t) は停留点に向かっていくが、到達には無限時間を要するので、（全ての有限時間に対する）解の一意性が保証されている。

しかし、有限時間内で定常解に到達するような方程式では、一意性は成立しない。例えば、dy/dt = ay 2/3 という方程式の場合、初期条件 y(0) = 0 に対応する解が y(t) = 0 または y ( t ) = { ( a t 3 ) 3 t < 0         0 t ≥ 0 {\displaystyle y(t)={\begin{cases}\left({\tfrac {at}{3}}\right)^{3}&t<0\\\ \ \ \ 0&t\geq 0\end{cases}}}