OAI/Probability/LogConcave/OraclePrograms/ShiftInvariant.lean

GitHub source file

7 declarations, 0 contain sorry, 0 declared as axioms

1. lemma OAI.LogConcaveSampling.OracleCompiler.MeanBudget.shiftInvariant line 15
2. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanCompiled_squared line 23
3. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleCompiled_squared line 66
4. lemma OAI.LogConcaveSampling.OracleCompiler.physicalCoefficient_bound line 125
5. lemma OAI.LogConcaveSampling.OracleCompiler.physicalError_bound line 149
6. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanCompiled_scaled line 172
7. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleCompiled_scaled line 206