OAI/Probability/LogConcave/OraclePrograms/Shape.lean

GitHub source file

34 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.LogConcaveSampling.OracleCompiler.source_anchor_radius line 14
  2. theorem OAI.LogConcaveSampling.OracleCompiler.literal_recursive_budget_order line 30
  3. lemma OAI.LogConcaveSampling.OracleCompiler.derivativeBudget_rate line 83
  4. theorem OAI.LogConcaveSampling.OracleCompiler.actualCoefficient_rate line 90
  5. lemma OAI.LogConcaveSampling.OracleCompiler.source_angle_square line 123
  6. theorem OAI.LogConcaveSampling.OracleCompiler.exists_source_configuration line 129
  7. theorem OAI.LogConcaveSampling.OracleCompiler.exists_subpower_routine_configuration line 158
  8. structure OAI.LogConcaveSampling.OracleCompiler.SourceShape line 187
  9. def OAI.LogConcaveSampling.OracleCompiler.sourceA line 200
  10. def OAI.LogConcaveSampling.OracleCompiler.sourceAf line 206
  11. lemma OAI.LogConcaveSampling.OracleCompiler.sourceAf_pos line 208
  12. lemma OAI.LogConcaveSampling.OracleCompiler.SourceShape.A line 214
  13. lemma OAI.LogConcaveSampling.OracleCompiler.SourceShape.Af line 221
  14. lemma OAI.LogConcaveSampling.OracleCompiler.SourceShape.depth line 226
  15. lemma OAI.LogConcaveSampling.OracleCompiler.sourceA_rate line 230
  16. lemma OAI.LogConcaveSampling.OracleCompiler.exists_source_shape line 238
  17. def OAI.LogConcaveSampling.OracleCompiler.meanFinalSize line 256
  18. def OAI.LogConcaveSampling.OracleCompiler.sampleFinalSize line 259
  19. def OAI.LogConcaveSampling.OracleCompiler.internalSize line 261
  20. def OAI.LogConcaveSampling.OracleCompiler.anchorSize line 264
  21. lemma OAI.LogConcaveSampling.OracleCompiler.meanFinalSize_rate line 266
  22. lemma OAI.LogConcaveSampling.OracleCompiler.sampleFinalSize_rate line 273
  23. lemma OAI.LogConcaveSampling.OracleCompiler.internalSize_rate line 277
  24. lemma OAI.LogConcaveSampling.OracleCompiler.anchorSize_rate line 294
  25. lemma OAI.LogConcaveSampling.OracleCompiler.small_coefficient_rate line 302
  26. lemma OAI.LogConcaveSampling.OracleCompiler.parent_intrinsic_rate line 308
  27. lemma OAI.LogConcaveSampling.OracleCompiler.meanError_rate line 313
  28. lemma OAI.LogConcaveSampling.OracleCompiler.sampleError_rate line 328
  29. def OAI.LogConcaveSampling.OracleCompiler.RoutineLabel.Admissible line 351
  30. lemma OAI.LogConcaveSampling.OracleCompiler.RoutineLabel.Admissible.b_lower line 354
  31. lemma OAI.LogConcaveSampling.OracleCompiler.RoutineLabel.Admissible.child line 359
  32. lemma OAI.LogConcaveSampling.OracleCompiler.RoutineLabel.Admissible.rank_bound line 375
  33. lemma OAI.LogConcaveSampling.OracleCompiler.topLabel_admissible line 383
  34. theorem OAI.LogConcaveSampling.OracleCompiler.exists_uniform_routine_mesh line 401