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 moving uniform support contributes a missing score boundary term
Example
For , let and use constant payoff . The objective is , so . The pathwise representation , , has derivative estimator . The interior score is , so ; it misses the moving endpoint contribution .
Facts & Assumptions
Given: , the density with respect to Lebesgue measure, and the constant payoff .
The Axiom of Choice: every family of nonempty sets has a choice function; AC is inherited by the score definition.
Score and Fisher information: on the positive-density set the score is .
Pathwise and reparameterized simulation-gradient estimators: in a representation using a fixed random input , the pathwise estimator is the derivative with held fixed.
Simulation objectives and unbiased payoff oracles: an objective is the expectation of its integrable simulation payoff.
Integrating against a density agrees with integrating the product: expectation under density is integration of the payoff times against Lebesgue measure.
Expectation of a nonnegative or integrable random variable: the expectation of an integrable constant random variable is that constant.
Verification
The density is normalized because . By [F3] and [F4], the constant payoff has , hence . In the representation , for every , so its pathwise derivative is zero by [F2].
On , , so [F1] gives almost surely under . Since , the score product is the constant almost surely, and [F5] gives . This differs from , so the fixed-support score identity does not apply.
The integral is . Differentiating this product gives the interior density-derivative contribution and the moving-endpoint contribution , where is the left limit of the density. Their sum is zero, exactly from step 1.1; the interior score term alone omits this boundary correction.
Depends on
Used by
Nothing in the library uses this result yet.
Dependency tree · two levels
29 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.