OAI/Computability/PerfectCompleteness/Sampling/CutSamplerReplayTransportLemmas.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.PerfectCompleteness.CutSamplerReplayTransport.squareEquiv_symm_apply line 24
  2. theorem OAI.PerfectCompleteness.CutSamplerReplayTransport.squareEquiv_symm_eval_of_agree line 31
  3. def OAI.PerfectCompleteness.CutSamplerReplayTransport.transport line 42
  4. theorem OAI.PerfectCompleteness.CutSamplerReplayTransport.evaluate_transport line 58
  5. def OAI.PerfectCompleteness.LocalReconstruction.Recipe.map line 117
  6. theorem OAI.PerfectCompleteness.LocalReconstruction.Recipe.evaluate_map line 123
  7. def OAI.PerfectCompleteness.LocalReconstruction.Recipe.sumList line 132
  8. theorem OAI.PerfectCompleteness.LocalReconstruction.Recipe.evaluate_sumList line 136
  9. def OAI.PerfectCompleteness.LocalReconstruction.Recipe.sumIndexed line 143
  10. theorem OAI.PerfectCompleteness.LocalReconstruction.Recipe.evaluate_sumIndexed line 146
  11. def OAI.PerfectCompleteness.StoppedSamplerRecipe.ordinaryTag line 165
  12. def OAI.PerfectCompleteness.StoppedSamplerRecipe.factorTag line 168
  13. def OAI.PerfectCompleteness.StoppedSamplerRecipe.recipe line 172
  14. def OAI.PerfectCompleteness.StoppedSamplerRecipe.atoms line 183
  15. theorem OAI.PerfectCompleteness.StoppedSamplerRecipe.evaluate_recipe line 197
  16. theorem OAI.PerfectCompleteness.StoppedSamplerRecipe.evaluate_factors line 223
  17. theorem OAI.PerfectCompleteness.UniformConditioning.uniform_transport line 246
  18. theorem OAI.PerfectCompleteness.UniformConditioning.uniform_probability_equiv line 253
  19. theorem OAI.PerfectCompleteness.UniformConditioning.uniform_probability line 258
  20. theorem OAI.PerfectCompleteness.UniformConditioning.uniform_probability_pos line 270
  21. theorem OAI.PerfectCompleteness.UniformConditioning.uniform_subtype_pushforward_weight line 276
  22. theorem OAI.PerfectCompleteness.UniformConditioning.condition_uniform line 296
  23. theorem OAI.PerfectCompleteness.UniformConditioning.probability_condition_uniform line 313