How statement and proof provenance work
The first chip identifies the source of the statement or construction; the second identifies the source of its local proof or verification.
- Literature-sourced: the exact statement appears in a cited source; only wording and notation differ.
- AI-adapted: a semantically identical restatement of literature-sourced material, modulo indexing, notation, and boundary cases adopted by the library.
- AI-generated: a genuinely novel statement formulated by AI, with no source for the claim itself.
These labels describe origin, not correctness: citations and verification chips remain separate evidence.
Cauchy–Kovalevskaya for first-order analytic systems
Statement
Let , let be analytic near zero, and let F be analytic near . Then , has a unique real analytic solution germ at . Existence holds on a nonempty neighborhood; uniqueness is among analytic germs.
Facts & Assumptions
Given: An analytic first-order normal system with analytic initial data and a right side analytic at the actual initial value and spatial jet, as specified in the statement.
Subtracting g gives an analytic zero-data system. (Subtracting analytic Cauchy jets).
First-order analytic zero-data systems have a unique formal solution. (Formal recursion for solved analytic normal equations).
The positive Goursat system dominates the zero-data formal solution. (Positive majorants dominate the Cauchy recursion).
The specified positive system has a convergent analytic solution with the required origin jet. (Convergence of the Goursat majorant).
Geometric coefficient bounds give convergence and termwise differentiation. (An absolutely convergent multi-indexed power series is holomorphic and differentiates termwise).
Proof
By F1 set to obtain with zero data. Put and . Its equation is , where K is analytic and K(0)=0. Its initial data remain zero. All substitutions stay inside the original analytic neighborhood after a finite shrinking.
F2 gives a unique formal z. Choose a common positive-radius coefficient bound M,r for the finite analytic family K (equivalently bound the absolute series on a smaller polydisc). F4 constructs the convergent positive Goursat majorant for these constants; F3 gives . Choose a positive polyradius s strictly inside the convergence region of U. If , then every coefficient of z is at most .
F5 makes z an analytic sum on a smaller polydisc and permits its spatial and time derivatives to be taken termwise. Shrink once more so the absolute sums of z and its spatial derivatives are inside the convergence radii of K. Expanding K then gives an absolutely convergent substitution, whose Taylor coefficients agree with the formal substitution in F2. Each coefficient of is zero by the recursion; hence this function is identically zero there. All coefficients are real, so the restriction is a real analytic solution. Adding tc and g reverses step 1.1 and supplies the prescribed trace.
Any other analytic solution undergoes the same subtraction in step 1.1; its Taylor series solves the identical zero-data formal problem. F2 forces equality of every coefficient with z. On a common smaller neighborhood both analytic functions equal their series and therefore coincide. Reversing the subtraction proves uniqueness of the original germ.
Source notes
Gantumur, §4 Theorem 18, printed pp. 9–10; Corollary 20 proof, p. 11, for nonzero analytic data.
Depends on
Used by
Dependency tree · two levels
34 results within two dependency steps of this one, each drawn at its shortest distance from it. An arrow runs from a result to what uses it, so the chart reads left to right and ends at this result, which carries a heavier outline. Every node is a link to that result. Click elsewhere on the chart to enlarge it.
Sources
- Gantumur, Math 580 Lecture Notes 2: The Cauchy-Kovalevskaya Theorem (standard reference, not scraped)
- Ageno, Part III: Analysis of Partial Differential Equations (standard reference, not scraped)