Cauchy–Kovalevskaya theorem
Problem statement
Notes: §32 of Oliver Knill's 'Some Fundamental Theorems in Mathematics'. The quasi-linear scalar Cauchy problem with real-analytic data has a unique local analytic solution. Stated with off-the-shelf mathlib (AnalyticOnNhd, fderiv, EuclideanSpace); the PDE is encoded through the Fréchet derivative, with fderiv u p (0,1) the time derivative and fderiv u p (v,0) the spatial directional derivative. Mathlib has no Cauchy-Kovalevskaya theorem, and no formalization of it was found in any other proof assistant.
Source: 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).
Informal solution: Construct the solution as a formal power series in (x, t) whose coefficients are determined recursively by differentiating the PDE and using the initial data; prove convergence by the method of majorants — bound the analytic data F, f, u₀ by geometric majorants for which the majorant Cauchy problem has an explicitly convergent closed-form solution, so the formal series converges on a neighborhood and is analytic there. Uniqueness holds because the power-series coefficients of any analytic solution with the given initial data are forced by the equation.
theorem declaration uses `sorry`cauchy_kovalevskaya {d : ℕ}
(F : LeanEval.Analysis.E d × ℝ × ℝ → LeanEval.Analysis.E d) (f : LeanEval.Analysis.E d × ℝ × ℝ → ℝ) (u₀ : LeanEval.Analysis.E d → ℝ)
(_hF : AnalyticOnNhd ℝ F univ) (_hf : AnalyticOnNhd ℝ f univ)
(_hu₀ : AnalyticOnNhd ℝ u₀ univ) (x₀ : LeanEval.Analysis.E d) :
∃ (U : Set (LeanEval.Analysis.E d × ℝ)) (u : LeanEval.Analysis.E d × ℝ → ℝ),
(x₀, (0 : ℝ)) ∈ U ∧ IsOpen U ∧ AnalyticOnNhd ℝ u U ∧
(∀ x : LeanEval.Analysis.E d, (x, (0 : ℝ)) ∈ U → u (x, 0) = u₀ x) ∧
(∀ p ∈ U,
fderiv ℝ u p ((0 : LeanEval.Analysis.E d), (1 : ℝ)) =
fderiv ℝ u p (F (p.1, p.2, u p), (0 : ℝ)) + f (p.1, p.2, u p)) ∧
(∀ v : LeanEval.Analysis.E d × ℝ → ℝ, AnalyticOnNhd ℝ v U →
(∀ x : LeanEval.Analysis.E d, (x, (0 : ℝ)) ∈ U → v (x, 0) = u₀ x) →
(∀ p ∈ U,
fderiv ℝ v p ((0 : LeanEval.Analysis.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) := d:ℕF:E d × ℝ × ℝ → E df:E d × ℝ × ℝ → ℝu₀:E d → ℝ_hF:AnalyticOnNhd ℝ F univ_hf:AnalyticOnNhd ℝ f univ_hu₀:AnalyticOnNhd ℝ u₀ univx₀:E d⊢ ∃ U u,
(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, 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, 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
All goals completed! 🐙