OAI/Probability/ProjectionMoments/Frames.lean

GitHub source file

32 declarations, 0 contain sorry, 0 declared as axioms

  1. instance OAI.ProjectionMoments.rotationLaw_probability line 15
  2. instance OAI.ProjectionMoments.rotationLaw_haar line 20
  3. instance OAI.ProjectionMoments.rotationLaw_right line 26
  4. lemma OAI.ProjectionMoments.rotation_transitive line 40
  5. lemma OAI.ProjectionMoments.measurable_rotateRows line 68
  6. lemma OAI.ProjectionMoments.measurable_rotateRows_left line 75
  7. lemma OAI.ProjectionMoments.measurable_rotateRows_right line 79
  8. lemma OAI.ProjectionMoments.rotateRows_mul line 84
  9. lemma OAI.ProjectionMoments.rotationLaw_orbit_eq line 87
  10. lemma OAI.ProjectionMoments.gaussianRows_rotation_invariant line 100
  11. lemma OAI.ProjectionMoments.coordinateMap_apply line 119
  12. def OAI.ProjectionMoments.rowJacobian line 124
  13. lemma OAI.ProjectionMoments.rowJacobian_pos line 128
  14. lemma OAI.ProjectionMoments.rows_factor line 131
  15. lemma OAI.ProjectionMoments.norm_rowMap_le line 169
  16. lemma OAI.ProjectionMoments.rowJacobian_le line 181
  17. lemma OAI.ProjectionMoments.coordinateMap_rotateRows line 188
  18. lemma OAI.ProjectionMoments.measurable_coordinateDensity line 206
  19. lemma OAI.ProjectionMoments.rowMap_eq_toLp_coordinateMap line 211
  20. lemma OAI.ProjectionMoments.coordinateDensity_is_density line 214
  21. def OAI.ProjectionMoments.labelMoment line 228
  22. lemma OAI.ProjectionMoments.measurable_labelMoment line 231
  23. lemma OAI.ProjectionMoments.labelMoment_factor line 235
  24. instance OAI.ProjectionMoments.frameLaw_probability line 261
  25. lemma OAI.ProjectionMoments.frameLaw_eq line 264
  26. def OAI.ProjectionMoments.orbitMoment line 267
  27. lemma OAI.ProjectionMoments.measurable_orbitMoment line 270
  28. lemma OAI.ProjectionMoments.orbitMoment_eq_frame line 275
  29. lemma OAI.ProjectionMoments.orbitMoment_factor line 280
  30. lemma OAI.ProjectionMoments.gaussian_lintegral_orbitMoment line 304
  31. lemma OAI.ProjectionMoments.gaussian_labelMoment_bound line 318
  32. theorem OAI.ProjectionMoments.frame_gaussian_comparison line 332