OAI/Probability/GaussianPropeller/Dual.lean

GitHub source file

49 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.GaussianPropeller.Reduction.Tuple line 12
  2. def OAI.GaussianPropeller.Reduction.scoreMax line 16
  3. def OAI.GaussianPropeller.Reduction.width line 19
  4. theorem OAI.GaussianPropeller.Reduction.le_scoreMax line 21
  5. theorem OAI.GaussianPropeller.Reduction.scoreMax_le_iff line 25
  6. theorem OAI.GaussianPropeller.Reduction.exists_scoreMax line 29
  7. theorem OAI.GaussianPropeller.Reduction.continuous_scoreMax line 34
  8. theorem OAI.GaussianPropeller.Reduction.norm_scoreMax_le line 37
  9. theorem OAI.GaussianPropeller.Reduction.integrable_scoreMax line 44
  10. theorem OAI.GaussianPropeller.Reduction.scoreMax_sub_le line 50
  11. theorem OAI.GaussianPropeller.Reduction.norm_scoreMax_sub_le line 61
  12. theorem OAI.GaussianPropeller.Reduction.width_lipschitz_bound line 68
  13. theorem OAI.GaussianPropeller.Reduction.continuous_width line 79
  14. def OAI.GaussianPropeller.Reduction.scoreCell line 87
  15. theorem OAI.GaussianPropeller.Reduction.measurable_scoreCell line 91
  16. theorem OAI.GaussianPropeller.Reduction.exists_unique_scoreCell line 107
  17. theorem OAI.GaussianPropeller.Reduction.scoreCell_partition line 137
  18. theorem OAI.GaussianPropeller.Reduction.scoreCell_score line 140
  19. def OAI.GaussianPropeller.Reduction.moments line 144
  20. theorem OAI.GaussianPropeller.Reduction.norm_moments_sq line 148
  21. theorem OAI.GaussianPropeller.Reduction.pairing_integral line 152
  22. theorem OAI.GaussianPropeller.Reduction.pairing_le_width line 164
  23. theorem OAI.GaussianPropeller.Reduction.pairing_scoreCell line 180
  24. theorem OAI.GaussianPropeller.Reduction.width_nonneg line 193
  25. theorem OAI.GaussianPropeller.Reduction.exists_max_width line 201
  26. theorem OAI.GaussianPropeller.Reduction.norm_moments_le line 212
  27. theorem OAI.GaussianPropeller.Reduction.exists_optimal_partition line 229
  28. def OAI.GaussianPropeller.Reduction.Optimal line 246
  29. def OAI.GaussianPropeller.Reduction.activeLabels line 249
  30. def OAI.GaussianPropeller.Reduction.activeCount line 252
  31. def OAI.GaussianPropeller.Reduction.MinimalOptimal line 254
  32. theorem OAI.GaussianPropeller.Reduction.exists_minimal_optimal line 257
  33. def OAI.GaussianPropeller.Reduction.merge line 269
  34. theorem OAI.GaussianPropeller.Reduction.merge_partition line 273
  35. theorem OAI.GaussianPropeller.Reduction.centroid_union line 314
  36. theorem OAI.GaussianPropeller.Reduction.value_merge line 330
  37. theorem OAI.GaussianPropeller.Reduction.activeCount_merge_lt line 353
  38. theorem OAI.GaussianPropeller.Reduction.negative_inner_of_minimal line 375
  39. theorem OAI.GaussianPropeller.Reduction.width_moments_of_optimal line 388
  40. theorem OAI.GaussianPropeller.Reduction.centroid_eq_zero_of_null line 404
  41. theorem OAI.GaussianPropeller.Reduction.assigned_le_scoreMax line 408
  42. theorem OAI.GaussianPropeller.Reduction.optimal_winning_ae line 420
  43. theorem OAI.GaussianPropeller.Reduction.two_nonzero_centroids line 456
  44. theorem OAI.GaussianPropeller.Reduction.active_centroid_ne_zero line 476
  45. theorem OAI.GaussianPropeller.Reduction.active_centroid_ne_other line 489
  46. theorem OAI.GaussianPropeller.Reduction.gaussian_hyperplane_null line 502
  47. def OAI.GaussianPropeller.Reduction.closedCell line 523
  48. theorem OAI.GaussianPropeller.Reduction.measurableSet_closedCell line 527
  49. theorem OAI.GaussianPropeller.Reduction.active_eq_closedCell_ae line 534