OAI/Probability/FreeIsing/Estimates/RandomIndexSampling.lean

GitHub source file

12 declarations, 0 contain sorry, 0 declared as axioms

  1. theorem OAI.Problem367.RandomIndexSampling.card_image_eq_of_same_fibers line 12
  2. theorem OAI.Problem367.RandomIndexSampling.measurable_select line 45
  3. theorem OAI.Problem367.RandomIndexSampling.measurePreserving_select line 53
  4. theorem OAI.Problem367.RandomIndexSampling.map_select line 67
  5. def OAI.Problem367.RandomIndexSampling.Consistent line 76
  6. theorem OAI.Problem367.RandomIndexSampling.consistent_iff_of_same_fibers line 81
  7. theorem OAI.Problem367.RandomIndexSampling.finite_cylinder_of_consistent line 93
  8. theorem OAI.Problem367.RandomIndexSampling.finite_cylinder_eq_zero_of_not_consistent line 121
  9. theorem OAI.Problem367.RandomIndexSampling.finite_cylinder line 136
  10. theorem OAI.Problem367.RandomIndexSampling.finite_cylinder_congr line 152
  11. theorem OAI.Problem367.RandomIndexSampling.random_finite_cylinder line 164
  12. theorem OAI.Problem367.RandomIndexSampling.map_select_of_indep line 181