ExampleConstruction: AI-generatedVerification: AI-generatedPipeline-generatedprecheck pass

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.

Common random numbers can remove finite-difference noise

Example

Assume AC and fix $c > 0$ . Let $Z \sim N (0, 1)$ and let one simulation output be $Y (θ, Z) = θ + Z$ , so $J (θ) = θ$ . Using the same $Z$ at $θ + c$ and $θ - c$ gives a central-difference estimate identically equal to $1$ . Using independent $Z_{+}$ and $Z_{-}$ gives variance $1 / (2 c^{2})$ .

Facts & Assumptions

Given: AC, a radius $c > 0$ , a standard normal noise variable and the simulator $Y (θ, Z) = θ + Z$ .

[F1]

Coupled finite-difference simulation-gradient estimator: the paired estimate is $(Y^{+} - Y^{-}) / (2 c)$ , with the joint law fixed by the coupling.

[F2]

Coupled finite differences have a covariance-controlled variance: the variance is $(Var Y^{+} + Var Y^{-} - 2 Cov (Y^{+}, Y^{-})) / (4 c^{2})$ .

[F3]

Standard normal and normal laws, The Axiom of Choice, AC implies DC implies countable choice, The Axiom of Countable Choice ( ${A C}_{ω}$ ) and A C^1 diffeomorphism satisfies the change-of-variables formula for nonnegative Lebesgue measurable functions: AC implies Countable Choice, and reflection $z \mapsto - z$ preserves Lebesgue measure; since the density $ϕ (z)$ is even, the standard normal law is symmetric.

[F4]

Expectations factor over finite products of independent random variables: independent integrable random variables have factorized product expectation.

[F5]

Gaussian even moments for Brownian increments gives $E Z^{2} = 1$ ; Change of variables for expectation and symmetry in [F3] then give $E Z = 0$ . Linearity, monotonicity, and the modulus bound for expectation gives linearity of expectation.

[F6]

Moments, variance, and covariance on a probability space and Variance and covariance identities for random variables: $Var (Z) = E [Z^{2}] - (E Z)^{2}$ .

Verification

1.1givenF1F3F5F6algebra

By [F5], $2 ∣ Z ∣ \leq 1 + Z^{2}$ gives integrability, and symmetry in [F3] implies $E Z = E [- Z] = - E Z$ , hence $E Z = 0$ . Therefore [F5] gives $J (θ) = E [θ + Z] = θ$ , as stated; [F5] and [F6] also give $Var (Z) = 1$ . With a shared $Z$ , $Y (θ + c, Z) - Y (θ - c, Z) = 2 c$ for every outcome. Thus the coupled estimate is exactly $1$ and has variance zero.

1.2F3F4F5F6algebra

With independent $Z_{+}, Z_{-}$ , the estimate is $1 + (Z_{+} - Z_{-}) / (2 c)$ . Each noise has the same mean zero and variance one just proved; by [F4] their product expectation factors, so their covariance is zero.

2.1F2step 1.1step 1.2algebra∎

Applying [F2] gives variance $(1 + 1) / (4 c^{2}) = 1 / (2 c^{2})$ . The variance contrast is caused by the coupling covariance; common random numbers do not guarantee this benefit for every payoff.

Depends on

Used by

Nothing in the library uses this result yet.

Dependency tree · two levels

66 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.