Cauchy–Kovalevskaya theorem

cauchy_kovalevskaya

Submitter: Kim Morrison.

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) := byd:ℕ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
  sorryAll goals completed! 🐙

Solved by

Not yet solved.