OAI/Probability/ProjectionMoments/FrameMoments.lean

GitHub source file

16 declarations, 0 contain sorry, 0 declared as axioms

  1. lemma OAI.ProjectionMoments.replicaConstant_real_le line 19
  2. theorem OAI.ProjectionMoments.frame_moment_unit line 31
  3. lemma OAI.ProjectionMoments.lintegral_inv_smul_label line 48
  4. lemma OAI.ProjectionMoments.ballAverage_label_scaled line 55
  5. theorem OAI.ProjectionMoments.ballAverage_integrated_scaled line 68
  6. theorem OAI.ProjectionMoments.lowerDensity_integrated_scaled line 93
  7. theorem OAI.ProjectionMoments.gaussian_labelMoment_scaled line 114
  8. theorem OAI.ProjectionMoments.frame_moment_scaled line 132
  9. lemma OAI.ProjectionMoments.frame_cost_power line 149
  10. lemma OAI.ProjectionMoments.ennreal_root_bound line 204
  11. lemma OAI.ProjectionMoments.frame_cost_root line 213
  12. lemma OAI.ProjectionMoments.measure_eq_zero_of_allBall_zero line 240
  13. lemma OAI.ProjectionMoments.lowerDensity_zero line 253
  14. lemma OAI.ProjectionMoments.coordinateDensity_zero line 257
  15. lemma OAI.ProjectionMoments.coordinateDensity_frame_support line 260
  16. theorem OAI.ProjectionMoments.integrated_frame_moment line 270