Alphabeta Math
ExampleConstruction: Literature-sourcedVerification: AI-adaptedPipeline-generated
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.

A mixture of straight Gaussian paths has a nonlinear marginal velocity

Example

Assume the Axiom of Choice and fix a>0 and σmin⁡>0. Let the endpoint law assign probability 1/2 to each endpoint x1=−a and x1=a. For each endpoint, use the one-dimensional Gaussian path with σt=1−(1−σmin⁡)t,Xt=σtZ+tx1,Z∼N(0,1). For either endpoint and each fixed Z=z, the conditional particle trajectory is a straight line. The marginal density is pt(x)=122π σt[exp⁡ ⁣(−(x−ta)22σt2)+exp⁡ ⁣(−(x+ta)22σt2)], and its marginal velocity field, defined by averaging the conditional velocity against the endpoint density at fixed (t,x), is utm(x)=σmin⁡−1σtx+aσttanh⁡ ⁣(atxσt2),tanh⁡(y):=exp⁡(y)−exp⁡(−y)exp⁡(y)+exp⁡(−y). The denominator in the definition of tanh⁡ is positive for every real input. The density is strictly positive, and ∂tpt(x)+∂x(pt(x)utm(x))=0 on (0,1)×R. For every t∈(0,1), x↦utm(x) is nonlinear.

Facts & Assumptions

Given: AC, a>0, σmin⁡>0, the two-point endpoint law, and the Gaussian conditional path in the Example.

[A1]

The Axiom of Choice is the assertion that every family of nonempty sets has a choice function (The Axiom of Choice); it is required by the Gaussian-law and density suppliers used by [F1].

[F1]

The Gaussian conditional affine map is quadratic-cost optimal: under AC, for each fixed endpoint x1 the mean-linear Gaussian path has the displayed density and affine conditional velocity, and its density and flux satisfy the conditional continuity equation.

[F2]

Probability paths and velocity fields: the marginal density is pt(x)=∫ρt(x∣x1) π(dx1) and its velocity, where 0<pt(x)<∞ and the flux is finite, is utm(x)=∫ρtutc dπ/pt(x).

[F3]

A conditional mixture is a probability path: the endpoint mixture of normalized conditional densities is a probability density at each time.

[F5]

Conditional continuity equations pass to the marginal path: if the conditional PDE derivatives admit the stated local integrable endpoint majorant, then the marginal density and flux satisfy the continuity equation.

[F6]

The real exponential function and the number e by a power series: the real exponential is defined on every real input by its convergent power series.

[F7]

The exponential addition formula exp⁡(x+y)=exp⁡(x)exp⁡(y): exp⁡(r+s)=exp⁡(r)exp⁡(s) for all real r,s.

[F8]

The exponential function is strictly increasing: r<s implies exp⁡(r)<exp⁡(s).

[F9]

The exponential is positive and satisfies exp⁡(−x)=1/exp⁡(x): exp⁡(−r)=1/exp⁡(r) and exp⁡(r)>0 for every real r.

Verification

Given: The hypotheses in the Example.

1.1givenA1F1F3F4F5

Apply [F1] to the two endpoints x1=a and x1=−a. Their conditional densities are positive and continuous in (t,x), as are their time derivatives, fluxes, and spatial flux derivatives; σt>0 throughout [0,1]. Hence for each compact K⊂(0,1)×R the finitely many such functions are bounded on K by [F4]. Taking a common bound as the constant function GK gives an element of L1(π) because π has total mass one. Thus [F5] applies. The mixture density is normalized by [F3] and is strictly positive because it is a sum of two positive Gaussian densities.

1.2givenF2F6F7F9algebra

Put A+(t,x):=exp⁡ ⁣(−(x−ta)22σt2),A−(t,x):=exp⁡ ⁣(−(x+ta)22σt2). The common Gaussian normalizing factor cancels in the endpoint-weighted mean, so [F2] gives mt(x):=∫x1ρt(x∣x1) π(dx1)pt(x)=aA+(t,x)−A−(t,x)A+(t,x)+A−(t,x). Expanding the two squares gives A+/A−=exp⁡(2atx/σt2) by [F7] and [F9]. Multiplying numerator and denominator by exp⁡(−atx/σt2) therefore yields mt(x)=atanh⁡(atx/σt2).

2.1step 1.2F1F2algebra

For endpoint x1∈{−a,a}, [F1] gives utc(x∣x1)=cx+(1−tc)x1,c:=σmin⁡−1σt. Taking the endpoint-weighted mean and using step 1.2 gives utm(x)=cx+(1−tc)mt(x). Since σt=1+t(σmin⁡−1), we have σt−t(σmin⁡−1)=1 and hence 1−tc=1/σt. Substitution gives the marginal velocity formula in the Example.

3.1step 2.1F6F7F8F9algebra∎

Fix t∈(0,1) and put β:=a/σt>0 and k:=at/σt2>0. The formula for tanh⁡, the addition formula [F7], and the reciprocal identity [F9] give tanh⁡(−y)=−tanh⁡(y), so utm is odd. For y>0, [F7] gives exp⁡(0)=exp⁡(0)2, and positivity [F9] therefore gives exp⁡(0)=1; strict increase [F8] now yields r:=exp⁡(2y)>1. Put s:=(r−1)/(r+1)∈(0,1). Rewriting tanh⁡(y) and tanh⁡(2y) using [F7, F9] gives tanh⁡(y)=s,tanh⁡(2y)=r2−1r2+1=2s1+s2<2s. Thus for every x>0, step 2.1 gives utm(2x)−2utm(x)=β(tanh⁡(2kx)−2tanh⁡(kx))<0. An odd affine function must be linear through the origin, and every such function has u(2x)−2u(x)=0. Hence utm is not affine and is nonlinear.

Source notes

The cited sources give the straight conditional Gaussian paths and the conditional-to-marginal velocity formula. The explicit two-endpoint mixture calculation is local. Its conclusion concerns nonlinearity of the marginal velocity; it makes no claim that the marginal field is a globally optimal transport field.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

63 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