OAI/Probability/LogConcave/OraclePrograms/FullTape.lean

GitHub source file

26 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.OracleCompiler.ReservedProgram.fullTape line 19
  2. lemma OAI.LogConcaveSampling.OracleCompiler.ReservedProgram.fullTape_preserving line 22
  3. lemma OAI.LogConcaveSampling.OracleCompiler.ReservedProgram.full_fixedSeed line 28
  4. lemma OAI.LogConcaveSampling.OracleCompiler.ReservedProgram.anchor_squared line 37
  5. theorem OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanFrom_squared line 94
  6. theorem OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleFrom_squared line 195
  7. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.depthBound line 285
  8. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanTree_depth line 287
  9. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleTree_depth line 291
  10. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.depthBound_pos line 301
  11. lemma OAI.LogConcaveSampling.OracleCompiler.ReservedProgram.full_fixedSeed_lip line 317
  12. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleFrom_lipschitz line 327
  13. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanFrom_lipschitz line 356
  14. lemma OAI.LogConcaveSampling.OracleCompiler.mean_error_envelope line 415
  15. lemma OAI.LogConcaveSampling.OracleCompiler.sample_error_envelope line 437
  16. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.compilerError line 448
  17. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanError line 451
  18. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleError line 454
  19. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.physical_mean_factor line 457
  20. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanCenter_scaled line 486
  21. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.sampleCenter_scaled line 494
  22. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.physical_small_of_scaled line 501
  23. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.MeanNumericalReady line 513
  24. def OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.SampleNumericalReady line 520
  25. lemma OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.compilerError_mono line 532
  26. theorem OAI.LogConcaveSampling.OracleCompiler.CircuitParameters.meanFrom_correct line 554