OAI/Probability/LogConcave/LowerBounds/RotationIsometry.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.LowerBound.rotationIsometry line 21
  2. theorem OAI.LogConcaveSampling.LowerBound.rotationIsometry_apply line 25
  3. def OAI.LogConcaveSampling.LowerBound.rotationFromIsometry line 28
  4. theorem OAI.LogConcaveSampling.LowerBound.rotationIsometry_from line 34
  5. theorem OAI.LogConcaveSampling.LowerBound.rotationIsometry_mul line 43
  6. theorem OAI.LogConcaveSampling.LowerBound.continuous_rotation_apply line 49
  7. theorem OAI.LogConcaveSampling.LowerBound.exists_rotation_of_norm_eq line 54
  8. instance OAI.LogConcaveSampling.LowerBound.rotationHaar_rightInvariant line 59
  9. theorem OAI.LogConcaveSampling.LowerBound.haar_orbit_eq line 73
  10. theorem OAI.LogConcaveSampling.LowerBound.rotationIsometry_one line 92
  11. theorem OAI.LogConcaveSampling.LowerBound.rotationIsometry_inv_apply line 96
  12. theorem OAI.LogConcaveSampling.LowerBound.haar_inverse_orbit_eq line 102
  13. theorem OAI.LogConcaveSampling.LowerBound.gaussian_radius_haar_direction line 117
  14. def OAI.LogConcaveSampling.LowerBound.vectorStabilizer line 146
  15. theorem OAI.LogConcaveSampling.LowerBound.mem_vectorStabilizer line 159
  16. theorem OAI.LogConcaveSampling.LowerBound.vectorStabilizer_isClosed line 162
  17. instance OAI.LogConcaveSampling.LowerBound.vectorStabilizer_compactSpace line 166
  18. def OAI.LogConcaveSampling.LowerBound.vectorStabilizerHaar line 170
  19. instance OAI.LogConcaveSampling.LowerBound.vectorStabilizerHaar_probability line 174
  20. instance OAI.LogConcaveSampling.LowerBound.vectorStabilizerHaar_isHaar line 179
  21. def OAI.LogConcaveSampling.LowerBound.sphereSection line 184
  22. theorem OAI.LogConcaveSampling.LowerBound.sphereSection_apply line 187
  23. theorem OAI.LogConcaveSampling.LowerBound.sphereSection_sends line 194
  24. theorem OAI.LogConcaveSampling.LowerBound.rotation_entry_eq line 199
  25. theorem OAI.LogConcaveSampling.LowerBound.measurable_sphereSection line 204
  26. theorem OAI.LogConcaveSampling.LowerBound.measurable_sphereSection_left line 222
  27. def OAI.LogConcaveSampling.LowerBound.sectionCocycle line 232