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 2,569 curated research declarations and 119,070 complete package declarations. Search 10,000 more complete Mathlib declarations.
Showing 1,849 to 1,854 of 2,569 results.
OracleComp.someOutputSatisfiesWhen_iff_supportWhen
Mathematical 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
Mathematical 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
Mathematical 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
Mathematical 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.
OracleComp.transcript_countQ_le_of_isPerIndexQueryBound
Mathematical statement
Per-index query bound. If oa respects a per-index budget qb, then for every oracle index t the transcript contains at most qb t queries to t.
Source project: VCVio
Person-level attribution pending.
OracleComp.transcript_countQ_le_of_isQueryBoundP
Mathematical statement
Predicate query bound. If oa makes at most n queries matching p, the transcript contains at most n p-matching entries (QueryLog.countQ).
Source project: VCVio
Person-level attribution pending.