OAI/MeasureTheory/CompactFactors/Centers.lean

GitHub source file

95 declarations, 0 contain sorry, 0 declared as axioms

  1. abbrev OAI.EuclideanFiveColor.Location.Ambient line 35
  2. def OAI.EuclideanFiveColor.Location.lift line 37
  3. theorem OAI.EuclideanFiveColor.Location.lift_fst line 39
  4. theorem OAI.EuclideanFiveColor.Location.lift_snd line 40
  5. theorem OAI.EuclideanFiveColor.Location.lift_ne_zero line 42
  6. theorem OAI.EuclideanFiveColor.Location.norm_lift line 47
  7. theorem OAI.EuclideanFiveColor.Location.lift_sub line 50
  8. theorem OAI.EuclideanFiveColor.Location.norm_lift_sub line 54
  9. theorem OAI.EuclideanFiveColor.Location.lift_affine line 57
  10. theorem OAI.EuclideanFiveColor.Location.not_sameRay_smul_lift line 64
  11. theorem OAI.EuclideanFiveColor.Location.strictConvex_norm_lift line 77
  12. def OAI.EuclideanFiveColor.Location.kernel line 86
  13. def OAI.EuclideanFiveColor.Location.objective line 88
  14. theorem OAI.EuclideanFiveColor.Location.kernel_formula line 90
  15. theorem OAI.EuclideanFiveColor.Location.continuous_kernel line 94
  16. theorem OAI.EuclideanFiveColor.Location.kernel_bound line 98
  17. theorem OAI.EuclideanFiveColor.Location.kernel_diff_bound line 102
  18. theorem OAI.EuclideanFiveColor.Location.integrable_kernel line 106
  19. theorem OAI.EuclideanFiveColor.Location.objective_zero line 111
  20. theorem OAI.EuclideanFiveColor.Location.objective_lipschitz line 114
  21. theorem OAI.EuclideanFiveColor.Location.continuous_objective line 129
  22. theorem OAI.EuclideanFiveColor.Location.kernel_strict_convex line 132
  23. theorem OAI.EuclideanFiveColor.Location.objective_strict_convex line 153
  24. theorem OAI.EuclideanFiveColor.Location.norm_lift_le line 172
  25. theorem OAI.EuclideanFiveColor.Location.kernel_lower line 177
  26. theorem OAI.EuclideanFiveColor.Location.exists_ball_mass line 185
  27. theorem OAI.EuclideanFiveColor.Location.objective_lower line 205
  28. theorem OAI.EuclideanFiveColor.Location.linear_norm_coercive line 232
  29. theorem OAI.EuclideanFiveColor.Location.objective_coercive line 238
  30. theorem OAI.EuclideanFiveColor.Location.exists_unique_minimizer line 247
  31. def OAI.EuclideanFiveColor.Location.center line 255
  32. theorem OAI.EuclideanFiveColor.Location.center_minimizes line 258
  33. theorem OAI.EuclideanFiveColor.Location.center_unique line 262
  34. def OAI.EuclideanFiveColor.Location.universalKernel line 266
  35. theorem OAI.EuclideanFiveColor.Location.measurable_objective line 269
  36. theorem OAI.EuclideanFiveColor.Location.denseSeq_inf_eq_min line 274
  37. def OAI.EuclideanFiveColor.Location.minValue line 285
  38. theorem OAI.EuclideanFiveColor.Location.measurable_minValue line 288
  39. theorem OAI.EuclideanFiveColor.Location.minValue_eq line 291
  40. theorem OAI.EuclideanFiveColor.Location.exists_min_on_closed line 295
  41. theorem OAI.EuclideanFiveColor.Location.measurable_center line 304
  42. theorem OAI.EuclideanFiveColor.Location.kernel_translate line 333
  43. theorem OAI.EuclideanFiveColor.Location.objective_translate line 340
  44. theorem OAI.EuclideanFiveColor.Location.center_translate line 349
  45. theorem OAI.EuclideanFiveColor.Location.kernel_orthogonal line 360
  46. theorem OAI.EuclideanFiveColor.Location.objective_orthogonal line 364
  47. theorem OAI.EuclideanFiveColor.Location.center_orthogonal line 370
  48. structure OAI.EuclideanFiveColor.CosetCenter.Embedding line 386
  49. def OAI.EuclideanFiveColor.CosetCenter.Embedding.j line 394
  50. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.j_zero line 396
  51. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.j_add line 397
  52. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.j_neg line 398
  53. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.j_sub line 399
  54. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.j_injective line 401
  55. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.measurable_j line 403
  56. def OAI.EuclideanFiveColor.CosetCenter.Embedding.ordinary line 405
  57. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.mem_ordinary_iff line 407
  58. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.range_j line 409
  59. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.measurableSet_ordinary line 411
  60. def OAI.EuclideanFiveColor.CosetCenter.Embedding.coordinate line 414
  61. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.measurable_coordinate line 416
  62. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.coordinate_j line 419
  63. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.j_coordinate line 422
  64. def OAI.EuclideanFiveColor.CosetCenter.Embedding.coset line 428
  65. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.measurableSet_coset line 430
  66. def OAI.EuclideanFiveColor.CosetCenter.Embedding.frequencyMeasure line 433
  67. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.frequencyMeasure_apply line 436
  68. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.frequencyMeasure_univ line 449
  69. def OAI.EuclideanFiveColor.CosetCenter.Embedding.parameterKernel line 456
  70. instance OAI.EuclideanFiveColor.CosetCenter.Embedding.parameterKernel_markov line 459
  71. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.measurable_frequencyMeasure line 462
  72. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.measurable_mass line 487
  73. def OAI.EuclideanFiveColor.CosetCenter.Embedding.frequencyLaw line 495
  74. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.frequencyLaw_measure line 503
  75. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.measurable_frequencyLaw line 513
  76. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.coset_mul_j line 526
  77. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.coordinate_div_j line 540
  78. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.frequencyMeasure_shift line 544
  79. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.frequencyLaw_shift line 557
  80. def OAI.EuclideanFiveColor.CosetCenter.Embedding.center line 570
  81. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.measurable_center line 573
  82. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.center_mem_coset line 579
  83. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.center_mul_j line 585
  84. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.center_eq_of_mem_coset line 592
  85. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.quotient_center line 601
  86. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.center_eq_iff line 605
  87. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.center_mem_ordinary_iff line 616
  88. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.preimage_center_singleton line 620
  89. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.measurable_center_fixed line 626
  90. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.equiv_mem_ordinary_iff line 635
  91. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.preimage_coset_equiv line 647
  92. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.coordinate_equiv line 654
  93. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.frequencyMeasure_equiv line 660
  94. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.frequencyLaw_equiv line 677
  95. theorem OAI.EuclideanFiveColor.CosetCenter.Embedding.center_equivariant line 692