Cauchy–Kovalevskaya theorem

AbbreviationModel space \(\mathbb{R}^d\) of the Cauchy–Kovalevskaya problem#✓fully proved

For a natural number \(d\), this is the real Euclidean space \(\mathbb{R}^d\) of dimension \(d\), with the Euclidean inner product and norm.

abbrev E (d : ℕ) := EuclideanSpace ℝ (Fin d)

Used by 1

Used byCauchy–Kovalevskaya theorem

TheoremCauchy–Kovalevskaya theorem#●ready to prove

Let \(d\) be a natural number, write \(\mathbb{R}^d\) for real Euclidean \(d\)-space, and let \(F : \mathbb{R}^d \times \mathbb{R} \times \mathbb{R} \to \mathbb{R}^d\), \(f : \mathbb{R}^d \times \mathbb{R} \times \mathbb{R} \to \mathbb{R}\) and \(u_0 : \mathbb{R}^d \to \mathbb{R}\) be real analytic at every point. Then for every \(x_0 \in \mathbb{R}^d\) there are an open set \(U \subseteq \mathbb{R}^d \times \mathbb{R}\) containing \((x_0, 0)\) and a function \(u : \mathbb{R}^d \times \mathbb{R} \to \mathbb{R}\), real analytic on \(U\), such that \(u(x, 0) = u_0(x)\) whenever \((x, 0) \in U\) and

\[\partial_t u(x, t) = F(x, t, u(x, t)) \cdot \nabla_x u(x, t) + f(x, t, u(x, t))\]

for every \((x, t) \in U\), where \(\partial_t u\) is the partial derivative of \(u\) in \(t\) and \(\nabla_x u\) is its gradient in \(x\). Moreover, every function \(v : \mathbb{R}^d \times \mathbb{R} \to \mathbb{R}\) that is real analytic on \(U\), satisfies \(v(x, 0) = u_0(x)\) whenever \((x, 0) \in U\), and satisfies the same equation at every point of \(U\) agrees with \(u\) on \(U\).

MathlibExt.Analysis.CauchyKovalevskayaWanted.Analysis.cauchy_kovalevskaya · 16 lines

public theorem_wanted cauchy_kovalevskaya {d : ℕ}
    (F : E d × ℝ × ℝ → E d) (f : E d × ℝ × ℝ → ℝ) (u₀ : E d → ℝ)
    (_hF : AnalyticOnNhd ℝ F univ) (_hf : AnalyticOnNhd ℝ f univ)
    (_hu₀ : AnalyticOnNhd ℝ u₀ univ) (x₀ : E d) :
    ∃ (U : Set (E d × ℝ)) (u : E d × ℝ → ℝ),
      (x₀, (0 : ℝ)) ∈ U ∧ IsOpen U ∧ AnalyticOnNhd ℝ u U ∧
      (∀ x : E d, (x, (0 : ℝ)) ∈ U → u (x, 0) = u₀ x) ∧
      (∀ p ∈ U,
        fderiv ℝ u p ((0 : E d), (1 : ℝ)) =
          fderiv ℝ u p (F (p.1, p.2, u p), (0 : ℝ)) + f (p.1, p.2, u p)) ∧
      (∀ v : E d × ℝ → ℝ, AnalyticOnNhd ℝ v U →
        (∀ x : E d, (x, (0 : ℝ)) ∈ U → v (x, 0) = u₀ x) →
        (∀ p ∈ U,
          fderiv ℝ v p ((0 : E d), (1 : ℝ)) =
            fderiv ℝ v p (F (p.1, p.2, v p), (0 : ℝ)) + f (p.1, p.2, v p)) →
        ∀ p ∈ U, u p = v p)

Sources

• A.-L. Cauchy (1842) and S. Kovalevskaya (1875). Listed as §32 in O. Knill, Some Fundamental Theorems in Mathematics (https://people.math.harvard.edu/~knill/graphgeometry/papers/fundamental.pdf). Problem cauchy_kovalevskaya of the lean-eval benchmark.

Uses 1

Statement usesModel space \(\mathbb{R}^d\) of the Cauchy–Kovalevskaya problem

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.