OAI/Probability/PosteriorReplicas/Regression/SupportVolume.lean

GitHub source file

23 declarations, 0 contain sorry, 0 declared as axioms

  1. def OAI.PosteriorRegression.coordinateNorm line 15
  2. lemma OAI.PosteriorRegression.continuous_coordinateNorm line 17
  3. lemma OAI.PosteriorRegression.coordinateNorm_sq line 22
  4. lemma OAI.PosteriorRegression.coordinateNorm_smul line 26
  5. def OAI.PosteriorRegression.coordinateBall line 30
  6. lemma OAI.PosteriorRegression.measurableSet_coordinateBall line 33
  7. lemma OAI.PosteriorRegression.coordinateBall_smul line 37
  8. lemma OAI.PosteriorRegression.volume_coordinateBall_smul line 51
  9. lemma OAI.PosteriorRegression.gaussianPDF_le_exp line 57
  10. lemma OAI.PosteriorRegression.lintegral_quarterGaussian_le line 67
  11. lemma OAI.PosteriorRegression.gaussian_density_pair_bound line 85
  12. lemma OAI.PosteriorRegression.measurable_coordinateVolume line 113
  13. lemma OAI.PosteriorRegression.gaussian_expected_coordinate_volume line 125
  14. lemma OAI.PosteriorRegression.stdGaussian_inner_map line 172
  15. lemma OAI.PosteriorRegression.rows_inner_map line 187
  16. lemma OAI.PosteriorRegression.rows_expected_coordinate_volume line 197
  17. def OAI.PosteriorRegression.rowOperator line 215
  18. lemma OAI.PosteriorRegression.rowOperator_apply line 220
  19. def OAI.PosteriorRegression.netProjectionSupport line 225
  20. lemma OAI.PosteriorRegression.measurableSet_netProjectionSupport line 229
  21. lemma OAI.PosteriorRegression.netProjectionSupport_volume line 235
  22. lemma OAI.PosteriorRegression.opNorm_le_twice_net line 263
  23. theorem OAI.PosteriorRegression.exists_projection_support line 290