OAI/Probability/SphericalField/Positivity/Duplication.lean

GitHub source file

21 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.SphericalPerceptron.duplicateEvent line 13
  2. lemma OAI.SphericalPerceptron.duplicateEvent_measurable line 17
  3. lemma OAI.SphericalPerceptron.duplicateEvent_relabel line 22
  4. lemma OAI.SphericalPerceptron.duplicateEvent_null_future line 30
  5. lemma OAI.SphericalPerceptron.star_unique_bound_of_no_duplication line 47
  6. lemma OAI.SphericalPerceptron.edge_probability_swap line 78
  7. theorem OAI.SphericalPerceptron.gg_duplicate_last line 86
  8. def OAI.SphericalPerceptron.relabelBlock line 115
  9. def OAI.SphericalPerceptron.replaceIndex line 118
  10. def OAI.SphericalPerceptron.replaceBlock line 121
  11. def OAI.SphericalPerceptron.replaceEvent line 124
  12. lemma OAI.SphericalPerceptron.relabelBlock_measurable line 127
  13. lemma OAI.SphericalPerceptron.replaceBlock_measurable line 132
  14. lemma OAI.SphericalPerceptron.fin_swap_val line 137
  15. lemma OAI.SphericalPerceptron.relabelBlock_swap line 141
  16. lemma OAI.SphericalPerceptron.relabelArray_swap_swap line 147
  17. lemma OAI.SphericalPerceptron.relabelBlock_swap_swap line 152
  18. lemma OAI.SphericalPerceptron.replaceBlock_last line 157
  19. lemma OAI.SphericalPerceptron.replaceBlock_swap line 164
  20. lemma OAI.SphericalPerceptron.block_event_swap line 183
  21. theorem OAI.SphericalPerceptron.gg_duplicate_index line 198