OAI/Probability/ProjectionMoments/Polar.lean

GitHub source file

24 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.ProjectionMoments.realMatrixMeasurableSpace line 17
  2. instance OAI.ProjectionMoments.realMatrixBorelSpace line 19
  3. lemma OAI.ProjectionMoments.mixRows_mul line 23
  4. lemma OAI.ProjectionMoments.mixRows_one line 30
  5. lemma OAI.ProjectionMoments.gram_mixRows line 35
  6. lemma OAI.ProjectionMoments.continuous_polarRadial line 47
  7. lemma OAI.ProjectionMoments.measurable_matrix_inverse line 53
  8. lemma OAI.ProjectionMoments.measurable_rawPolarRows line 63
  9. lemma OAI.ProjectionMoments.polarRadial_squared line 75
  10. lemma OAI.ProjectionMoments.polarRadial_pos line 80
  11. lemma OAI.ProjectionMoments.polarRadial_isUnit line 83
  12. lemma OAI.ProjectionMoments.rawPolarRows_orthonormal line 88
  13. lemma OAI.ProjectionMoments.polar_reconstruction line 102
  14. lemma OAI.ProjectionMoments.gram_rotateRows line 108
  15. lemma OAI.ProjectionMoments.polarRadial_rotateRows line 113
  16. lemma OAI.ProjectionMoments.rawPolarRows_rotateRows line 117
  17. lemma OAI.ProjectionMoments.measurableSet_linearIndependent line 122
  18. lemma OAI.ProjectionMoments.measurable_polarRows line 129
  19. lemma OAI.ProjectionMoments.polarRows_orthonormal line 133
  20. lemma OAI.ProjectionMoments.polarRows_rotateRows line 139
  21. lemma OAI.ProjectionMoments.lintegral_polarRows_eq_frame line 148
  22. lemma OAI.ProjectionMoments.polarRows_law line 182
  23. lemma OAI.ProjectionMoments.euclidean_gaussian_integral line 193
  24. lemma OAI.ProjectionMoments.unit_ball_volume_bound line 214