Source-pinned research
Search theorem names, mathematical ideas, modules, topics, projects, and role-labelled researchers. Open a result for its complete indexed Lean declaration and source record.
This index contains 169 research declarations. Search 10,000 more complete Mathlib declarations.
169 results
Clear filtersOracleComp.simulateQ_run_preservesInv
Plain-language statement
If impl preserves Inv, then simulating any oracle computation with simulateQ impl preserves Inv on the final state (support-wise).
Source project: VCVio
Person-level attribution pending.
OracleComp.simulateQ_run_writerPreservesInv
Plain-language statement
If impl preserves the writer invariant Inv, then simulating any oracle computation with simulateQ impl preserves Inv on the final accumulated writer (support-wise).
Source project: VCVio
Person-level attribution pending.
OracleComp.someOutputSatisfiesWhen_iff_supportWhen
Plain-language statement
Some output of oa reachable under possibleOutputs satisfies outputPred exactly when outputPred holds at some point of oa.supportWhen possibleOutputs.
Source project: VCVio
Person-level attribution pending.
OracleComp.sq_probOutput_map_le_observedForkPair
Plain-language statement
Fixed-index observed success squares under two independent completions of the selected occurrence context.
Source project: VCVio
Person-level attribution pending.
OracleComp.support_liftComp
Plain-language statement
Support is preserved by liftComp: lifting a computation to a larger oracle spec does not change which outputs are reachable. This is the support analogue of evalDist_liftComp.
Source project: VCVio
Person-level attribution pending.
OracleComp.support_simulateQ_run'_subset
Plain-language statement
Simulating an OracleComp through a stateful implementation in monad m can only shrink the support: any output reachable after simulation was already reachable in the original computation (where oracle queries may return any value). This is the support-level analogue of evalDist_simulateQ_run'_eq_evalDist.
Source project: VCVio
Person-level attribution pending.