OAI/Probability/LogConcave/OraclePrograms/CircuitParameters.lean

GitHub source file

15 declarations, 0 contain sorry, 0 declared as axioms

  1. structure OAI.LogConcaveSampling.OracleCompiler.CircuitParameters line 15
  2. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanEndpoint line 38
  3. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanTree line 41
  4. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanDrift line 44
  5. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanDrift_spec line 47
  6. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleEndpoint line 52
  7. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleTree line 57
  8. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleDrift line 60
  9. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanCenterBudget line 66
  10. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleCenterBudget line 67
  11. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleFinalBudget line 68
  12. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanFrom line 70
  13. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleFrom line 83
  14. def OAI.LogConcaveSampling.OracleCompiler.RoutineValue line 94
  15. def OAI.LogConcaveSampling.OracleCompiler.constructRoutine line 98