OAI/Probability/GaussianReplacement/KernelGeometry.lean

GitHub source file

27 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.CurrentProjection.rowSpan line 18
  2. def OAI.CurrentProjection.rowProjectionL line 21
  3. lemma OAI.CurrentProjection.rowProjectionL_eq line 26
  4. lemma OAI.CurrentProjection.measurable_rowProjectionL line 45
  5. lemma OAI.CurrentProjection.rowSpan_isometry line 57
  6. lemma OAI.CurrentProjection.rowProjectionL_isometry line 63
  7. lemma OAI.CurrentProjection.rowProjectionL_contraction line 69
  8. lemma OAI.CurrentProjection.rowProjectionL_perpendicular line 75
  9. lemma OAI.CurrentProjection.rowProjectionL_infDist line 81
  10. lemma OAI.CurrentProjection.gaussianRowIsometry_preserving line 91
  11. lemma OAI.CurrentProjection.rowProjection_smallBall_eq line 97
  12. lemma OAI.CurrentProjection.stdGaussian_submodule_null line 117
  13. lemma OAI.CurrentProjection.gaussianRows_ae_gramSchmidt_ne_zero line 146
  14. lemma OAI.CurrentProjection.gaussianRows_ae_rowSpan_finrank line 179
  15. lemma OAI.CurrentProjection.sphereLaw_submodule_tube line 199
  16. lemma OAI.CurrentProjection.sphereLaw_rowProjection line 231
  17. lemma OAI.CurrentProjection.measurable_rowProjection_pair line 250
  18. lemma OAI.CurrentProjection.gaussian_rowProjection_smallBall line 257
  19. lemma OAI.CurrentProjection.exists_unit_sphere_net line 290
  20. lemma OAI.CurrentProjection.exists_unit_projection_le_distance line 312
  21. lemma OAI.CurrentProjection.kernel_selected_smallBall_raw line 366
  22. def OAI.CurrentProjection.kernelSmallBallConstant line 421
  23. lemma OAI.CurrentProjection.kernelSmallBallConstant_ge_two line 423
  24. lemma OAI.CurrentProjection.kernelSmallBall_coefficient line 426
  25. lemma OAI.CurrentProjection.kernel_selected_scaled_smallBall line 460
  26. lemma OAI.CurrentProjection.inverse_moment_of_scaled_smallBall line 503
  27. lemma OAI.CurrentProjection.kernel_selected_inverse_step line 554