OAI/Probability/LogConcave/LowerBounds/RevealRotation.lean

GitHub source file

40 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.LogConcaveSampling.LowerBound.revealRotation line 19
  2. theorem OAI.LogConcaveSampling.LowerBound.measurable_revealRotation line 23
  3. theorem OAI.LogConcaveSampling.LowerBound.revealRotation_sends line 30
  4. theorem OAI.LogConcaveSampling.LowerBound.revealRotation_law line 36
  5. theorem OAI.LogConcaveSampling.LowerBound.haar_single_vector_revelation line 83
  6. def OAI.LogConcaveSampling.LowerBound.subspaceStabilizer line 102
  7. theorem OAI.LogConcaveSampling.LowerBound.mem_subspaceStabilizer line 113
  8. theorem OAI.LogConcaveSampling.LowerBound.subspaceStabilizer_isClosed line 116
  9. instance OAI.LogConcaveSampling.LowerBound.subspaceStabilizer_compactSpace line 126
  10. instance OAI.LogConcaveSampling.LowerBound.subspaceStabilizer_secondCountable line 130
  11. instance OAI.LogConcaveSampling.LowerBound.subspaceStabilizer_measurableMul line 135
  12. instance OAI.LogConcaveSampling.LowerBound.subspaceStabilizer_measurableInv line 138
  13. def OAI.LogConcaveSampling.LowerBound.subspaceHaar line 141
  14. instance OAI.LogConcaveSampling.LowerBound.subspaceHaar_probability line 145
  15. instance OAI.LogConcaveSampling.LowerBound.subspaceHaar_isHaar line 148
  16. instance OAI.LogConcaveSampling.LowerBound.subspaceHaar_rightInvariant line 153
  17. lemma OAI.LogConcaveSampling.LowerBound.stabilizer_map_orthogonal line 168
  18. def OAI.LogConcaveSampling.LowerBound.complementIsometry line 177
  19. theorem OAI.LogConcaveSampling.LowerBound.complementIsometry_apply_coe line 193
  20. theorem OAI.LogConcaveSampling.LowerBound.continuous_complementIsometry_apply line 197
  21. lemma OAI.LogConcaveSampling.LowerBound.sphereSection_mem_subspaceStabilizer line 205
  22. def OAI.LogConcaveSampling.LowerBound.complementSection line 212
  23. theorem OAI.LogConcaveSampling.LowerBound.measurable_complementSection line 216
  24. lemma OAI.LogConcaveSampling.LowerBound.complementSection_sends line 224
  25. theorem OAI.LogConcaveSampling.LowerBound.complementIsometry_mul line 229
  26. theorem OAI.LogConcaveSampling.LowerBound.complementIsometry_inv line 235
  27. lemma OAI.LogConcaveSampling.LowerBound.complement_haar_orbit_eq line 239
  28. theorem OAI.LogConcaveSampling.LowerBound.complementary_gaussian_radius_haar_direction line 255
  29. lemma OAI.LogConcaveSampling.LowerBound.stabilizer_sup_line line 281
  30. def OAI.LogConcaveSampling.LowerBound.residualInclusion line 289
  31. theorem OAI.LogConcaveSampling.LowerBound.continuous_residualInclusion line 293
  32. theorem OAI.LogConcaveSampling.LowerBound.residualInclusion_mul line 297
  33. lemma OAI.LogConcaveSampling.LowerBound.residualInclusion_fixes line 301
  34. def OAI.LogConcaveSampling.LowerBound.complementCocycle line 308
  35. theorem OAI.LogConcaveSampling.LowerBound.measurable_complementSection_left line 327
  36. def OAI.LogConcaveSampling.LowerBound.revealComplement line 333
  37. theorem OAI.LogConcaveSampling.LowerBound.measurable_revealComplement line 338
  38. lemma OAI.LogConcaveSampling.LowerBound.revealComplement_sends line 345
  39. theorem OAI.LogConcaveSampling.LowerBound.revealComplement_law line 351
  40. theorem OAI.LogConcaveSampling.LowerBound.haar_complement_single_vector_revelation line 412