OAI/Probability/LogConcave/OraclePrograms/Expression.lean

GitHub source file

38 declarations, 0 contain sorry, 0 declared as axioms

  1. inductive OAI.LogConcaveSampling.OracleCompiler.Expression line 14
  2. def OAI.LogConcaveSampling.OracleCompiler.Expression.slots line 24
  3. def OAI.LogConcaveSampling.OracleCompiler.Expression.calls line 28
  4. def OAI.LogConcaveSampling.OracleCompiler.Expression.leftBlock line 32
  5. def OAI.LogConcaveSampling.OracleCompiler.Expression.middleBlock line 34
  6. def OAI.LogConcaveSampling.OracleCompiler.Expression.rightBlock line 36
  7. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.measurable_leftBlock line 39
  8. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.measurable_middleBlock line 42
  9. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.measurable_rightBlock line 45
  10. def OAI.LogConcaveSampling.OracleCompiler.Expression.compile line 49
  11. def OAI.LogConcaveSampling.OracleCompiler.Expression.eval line 69
  12. theorem OAI.LogConcaveSampling.OracleCompiler.Expression.compile_run line 75
  13. theorem OAI.LogConcaveSampling.OracleCompiler.Expression.measurable_eval line 83
  14. structure OAI.LogConcaveSampling.OracleCompiler.Program.Equivariant line 107
  15. theorem OAI.LogConcaveSampling.OracleCompiler.Program.Equivariant.history line 114
  16. theorem OAI.LogConcaveSampling.OracleCompiler.Program.Equivariant.run line 124
  17. theorem OAI.LogConcaveSampling.OracleCompiler.Program.Equivariant.executed_query line 129
  18. theorem OAI.LogConcaveSampling.OracleCompiler.Program.Equivariant.seq line 134
  19. theorem OAI.LogConcaveSampling.OracleCompiler.Program.Equivariant.seedMap line 147
  20. theorem OAI.LogConcaveSampling.OracleCompiler.Program.Equivariant.map line 155
  21. lemma OAI.LogConcaveSampling.OracleCompiler.Program.pure_equivariant line 165
  22. lemma OAI.LogConcaveSampling.OracleCompiler.Program.oneQuery_equivariant line 173
  23. def OAI.LogConcaveSampling.OracleCompiler.Expression.shiftSlots line 197
  24. def OAI.LogConcaveSampling.OracleCompiler.Expression.moveSeed line 200
  25. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.leftBlock_shift line 203
  26. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.middleBlock_shift line 208
  27. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.rightBlock_shift line 213
  28. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.noise_equivariant line 219
  29. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.add_equivariant line 227
  30. def OAI.LogConcaveSampling.OracleCompiler.Expression.FixedSeedLip line 292
  31. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.noise_fixedSeed_lip line 295
  32. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.add_fixedSeed_lip line 303
  33. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.FixedSeedLip.compiled line 321
  34. lemma OAI.LogConcaveSampling.SeedCompiler.terminalMean_fixedSeed_lip line 333
  35. lemma OAI.LogConcaveSampling.SeedCompiler.terminalSample_fixedSeed_lip line 341
  36. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.split_slots_preserving line 366
  37. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.three_blocks_preserving line 376
  38. lemma OAI.LogConcaveSampling.OracleCompiler.Expression.three_blocks_with_anchor line 388