Alphabeta MathHow 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.
Forward Euler has first-order global error and preserves a margin tube for the regularized SPH ODE
Statement
Use the state norm ||z||#=max_i{|q_i|,|v_i|,|e_i|} on the finite-dimensional state space, and dist#(z,Kᶜ)=inf_{y∉K}||z−y||#. Let T>0 and let z(t), 0≤t≤T, be the unique solution from Local well-posedness of the regularized finite-particle SPH system. Let K⊂U be a nonempty compact convex set, with dist#(z(t),Kᶜ)≥δ>0 for every t. Assume B,L≥0, ||F(w)||#≤B for every w∈K, and Lip#(F|K)≤L. For an integer n≥1 set h=T/n, Z₀=z(0), and Z_{k+1}=Z_k+hF(Z_k). Put E_h=(Bh/2)(exp(LT)−1), which is zero when L=0. If E_h<δ, then every Euler state Z_k lies in K and
The tube margin and exact-path hypothesis are explicit. This result makes no energy- or momentum-conservation claim for the Euler time discretization.
Facts & Assumptions
Given: The regularized SPH vector field F, an exact solution on [0,T] with the stated margin in K, finite B,L, a positive step h=T/n, and exact initial data.
Local well-posedness of the regularized finite-particle SPH system: F has a unique local solution on the positive-density open state domain.
A first-order initial value problem is equivalent to its Volterra integral equation: a C¹ solution of ż=F(z) satisfies z(t+s)=z(t)+∫₀ˢF(z(t+r))dr.
Explicit local Lipschitz bound for the regularized SPH vector field: F is L-Lipschitz on K and has the stated bound B when assumed in the Given clause.
for every real , hence : 1+x≤exp(x) for every real x.
The exponential addition formula : exp(x+y)=exp(x)exp(y).
Cauchy-Schwarz with its equality case, the triangle inequality for , the parallelogram law and polarisation: each Euclidean position/velocity block norm satisfies the triangle and homogeneity axioms; the real internal-energy blocks have the same properties, and taking a finite maximum preserves them. Thus ||·||# is a norm.
For and integrable when , ; for , is integrable: applying the integral norm inequality to each Euclidean state block, then taking the finite maximum, gives ||∫g||#≤∫||g||# on a time interval.
Proof
The local defect from an exact start is z(t+h)−z(t)−hF(z(t))=∫₀ʰ(F(z(t+s))−F(z(t)))ds by [F2]. Since z(t)∈K and ||F(w)||#≤B for every w∈K, ||ż(t)||#≤B; applying [F7] to the Volterra formula gives ||z(t+s)−z(t)||#≤Bs. Then [F3] bounds the defect integrand by LBs. A second application of [F7] and integration of LBs give the local defect norm bound LBh²/2.
Suppose Z_k∈K. By convexity of K the segment from Z_k to z(kh) lies in K, so [F3] gives ||Z_k+hF(Z_k)−(z(kh)+hF(z(kh)))||#≤(1+hL)||Z_k−z(kh)||#. The triangle and homogeneity properties in [F6], together with the defect from step 1.1, yield e_{k+1}≤(1+hL)e_k+LBh²/2, where e_k=||Z_k−z(kh)||#.
Starting with e₀=0 and iterating step 2.1 gives e_k≤(Bh/2)((1+hL)^k−1) when L>0, by the finite geometric-sum identity; when L=0 the defect is zero and e_k=0. Since 1+hL≤exp(hL) by [F4] and exp(khL)=exp(Lkh) by repeated [F5], e_k≤E_h for k≤n.
Initially Z₀=z(0)∈K. If Z₀,…,Z_k∈K, steps 2.1–3.1 give e_{k+1}≤E_h<δ. The exact state z((k+1)h) is at distance at least δ from Kᶜ, so Z_{k+1}∈K. Induction proves all Euler states remain in K and the bound holds for every k.
Depends on
- Fixed-width regularized conservative SPH particle system
- Explicit local Lipschitz bound for the regularized SPH vector field
- Local well-posedness of the regularized finite-particle SPH system
- $1+x\le\exp(x)$ for every real $x$, hence $(1-p)^m\le\exp(-mp)$
- The exponential addition formula $\exp(x+y)=\exp(x)\exp(y)$
- A first-order initial value problem is equivalent to its Volterra integral equation
- Cauchy-Schwarz $\lvert\langle x,y\rangle\rvert \le \lVert x\rVert_2\lVert y\rVert_2$ with its equality case, the triangle inequality for $\lVert\cdot\rVert_2$, the parallelogram law and polarisation
- For $a \le b$ and $f : [a,b] \to \mathbb{R}^m$ integrable when $a<b$, $\bigl\lVert\int_a^b f\bigr\rVert_2 \le \int_a^b \lVert f\rVert_2$; for $a<b$, $\lVert f\rVert_2$ is integrable
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
62 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
- Volker Springel, Smoothed Particle Hydrodynamics in Astrophysics, Annual Review of Astronomy and Astrophysics 48 (2010), author full text (standard reference, not scraped)
- Benjamin Seibold, MIT OpenCourseWare 18.336, Numerical Methods for Partial Differential Equations, Lecture 25: Particle Methods (Spring 2009) (standard reference, not scraped)